Синтаксис лямбда-исчисления

Минимальный язык из трёх правил, который оказался полной моделью вычислений.

Лямбда-исчисление — формальная система с тремя конструкциями: переменная, абстракция (функция) и аппликация (вызов); этого достаточно, чтобы выразить любое вычисление.

Зачем такой минимализм

Прежде чем добавлять типы, нужно понять, к чему они приписываются. Чёрч в 1930-е искал предельно простую модель «что такое вычислимая функция». Он выкинул всё лишнее — числа, циклы, присваивание — и оставил только функции. Получилось три правила, из которых, как из кирпичей, собирается любая программа. Это нетипизированное лямбда-исчисление — основа, на которую дальше мы наденем типы.

Три конструкции

Грамматика умещается в одну строку (символ лямбда обозначаем как \ или словом «лямбда»):

e ::= x            -- переменная
    | \x. e        -- абстракция (определение функции)
    | e e          -- аппликация (вызов)

Например, функция тождества — \x. x. Функция, всегда возвращающая первый аргумент, — \x. \y. x. Применение тождества к самому себе — (\x. x) (\y. y).

Приоритеты и скобки

Чтобы читать выражения без леса скобок, действуют два соглашения. Аппликация левоассоциативна: f a b значит (f a) b, а не f (a b) — функции одного аргумента, применяемые по очереди (каррирование). Тело абстракции тянется как можно правее: \x. x y значит \x. (x y), а не (\x. x) y.

f a b        ==  (f a) b
\x. x y      ==  \x. (x y)
\x. \y. x    ==  \x. (\y. x)

Демонстрация: разбор и печать AST

Представим выражения как дерево из трёх видов узлов и напечатаем их структуру. Это та же модель, на которую дальше навесим типы и редукцию.

def var(n):      return ("var", n)
def lam(p, b):   return ("lam", p, b)
def app(f, a):   return ("app", f, a)

def show(t):
    if t[0] == "var":
        return t[1]
    if t[0] == "lam":
        return "(\\" + t[1] + ". " + show(t[2]) + ")"
    return "(" + show(t[1]) + " " + show(t[2]) + ")"

identity = lam("x", var("x"))
const    = lam("x", lam("y", var("x")))
selfapp  = app(identity, identity)

print("identity:", show(identity))
print("const   :", show(const))
print("selfapp :", show(selfapp))

Вывод:

identity: (\x. x)
const   : (\x. (\y. x))
selfapp : ((\x. x) (\x. x))

Как работает под капотом

Любая программа в лямбда-исчислении — это конечное дерево из трёх видов узлов. Парсер языка с лямбдами строит ровно такое дерево, расставляя приоритеты по двум правилам выше. Вычисление (следующий урок) — это переписывание дерева. Типизация (раздел 4) — приписывание каждому узлу типа. Так что освоить эти три узла означает заложить фундамент всего курса.

Частые ошибки

• Думать, что функция берёт несколько аргументов. В лямбда-исчислении каждая функция строго одноместна; многоместность моделируется каррированием: \x. \y. e.
• Путать приоритет аппликации. f a b — это (f a) b; забыв левую ассоциативность, легко прочитать неверно.
• Считать переменную «ячейкой». Переменная здесь — имя для подстановки, без присваивания и изменяемого состояния.

Итоги

• Весь язык — три конструкции: переменная, абстракция, аппликация.
• Функции одноместны; много аргументов — через каррирование.
• Аппликация левоассоциативна, тело абстракции тянется вправо.
• Программа — это дерево из трёх видов узлов; на него мы навесим вычисление и типы.