Лямбда-исчисление на пальцах

Функции на функциях от функций к функциям

Начнем, собственно, с лямбда-исчисления. Использовать я буду не авторскую нотацию, а подмножество языка Scheme, которое, на мой взгляд, читается значительно легче.

В оригинальном лямбда-исчислении сущностей практически нет. Грамматика выражений такого языка в форме Бэкуса-Наура выражается следующим образом:

<expression> ::= <variable>
                 | (lambda (<variable>) <expression>)
                 | (<expression> <expression>)

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

Вот, например, функция, возвращающая собственный аргумент:

(lambda (a) a)

Или применение этой функции к другой функции:

((lambda (a) a) (lambda (b) b))

Результат применения последнего выражения, конечно же, это та же самая функция:

(lambda (b) b)

Переменная в теле функции называется связанной (англ. bound), если это переменная — аргумент функции. Переменные, аргументами не являющиеся, называются свободными (англ. free):

(lambda (a) c) ;; c - свободная
(lambda (b) c) ;; c - свободная
((lambda (a) (lambda (b) b)) c) ;; b - связанная, c - свободная

В этих трех примерах переменные a и b — связанные, а c — свободная.

И хотя натуральные числа в простейшем лямбда-исчислении можно выразить, ставя в соответствие числам определенные лямбда-выражения, чаще такие числа и операции над ними вводят непосредственно в сам язык:

<expression> ::= <variable>
                 | <number>
                 | <number-operations>
                 | (lambda (<variable>) <expression>)
                 | (<expression> <expression>)

То есть мы можем писать применять функции к числам:

1 -> 1
((lambda (a) 1) 2) -> 1
((+ 1) 2) -> 3

В последнем примере видно, что у нас все еще есть одно неудобное ограничение: в нашем языке функции могут иметь только один аргумент.

Несколько аргументов функции: каррирование

В лямбда-исчислении функция принимает только один аргумент. На самом деле это не проблема, т. к. мы всегда можем вложить функции одну в другую, и использовать во внутренней функции аргумент внешней:

(lambda (a) (lambda (b) (+ a b)))

Такую функцию можно применить частично, получив на выходе функцию с одним параметром, или полностью:

((lambda (a) (lambda (b) (+ a b))) 1) -> (lambda (b) (+ 1 b))
(((lambda (a) (lambda (b) (+ a b))) 1) 2) -> 3

Выходит, что при частичном применении возвращается функция, принимающая на один параметр меньше. Прием называется каррированием и позволяет выразить функции многих переменных. Такой «синтаксический сахар» часто встречается в функциональных языках, особенно в семействе ML. Используем его и в нашем варианте лямбда-исчисления:

<expression> ::= <variable>
                 | <number>
                 | <number-operations>
                 | (lambda (<variable>+) <expression>)
                 | (<expression> <expression>)

Обратите внимание, что аргументов у лямбда-выражения теперь может быть несколько.

Одинаковые функции: \(\alpha\)-эквивалентность и \(\alpha\)-преобразования

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

(lambda (a) a)
(lambda (b) b)

(lambda (a) (lambda (b) (+ a b)))
(lambda (c) (lambda (d) (+ c d)))

(lambda (a) (+ a e)) - здесь e - свободная переменная, ее эквивалентность не касается
(lambda (b) (+ b e))

Такие выражения называются \(\alpha\)-эквивалентными.

Может показаться, что здесь все просто, но есть и проблема: имена переменных могут начать пересекаться (скажем, свободные переменные станут связанными) после замены функций на составляющие тело функции выражения. Во избежание такого рода проблем можно провести \(\alpha\)-преобразования (\(\alpha\)-переименования), когда имена связанных переменных меняются так, чтобы не пересекаться со свободными.

Применение функции: \(\beta\)-редукции и нормальная форма лямбда-выражений

Выше применение функции к аргументам (подстановку аргумента) я обсуждал интуитивно. Реальный процесс подстановки аргументов функции в ее тело называется \(\beta\)-редукцией:

((lambda (x) x) 1) -> 1

Здесь мы заменили x на 1 в теле функции, и оставили только само тело функции. Правила подстановки, конечно, сформулированы подробней, и главное при этом не затронуть связанные вложенными функциями переменные, для чего может понадобиться предварительно провести \(\alpha\)-переименования.

Выражения, для которых можно провести такую подстановку, называются редексами (англ. redexes, или reducible expressions) и они соответствуют вызову функции с аргументами.

В менее тривиальных выражениях возникает вопрос выбора следующих редексов для подстановки:

((lambda (a) ((lambda (b) (+ b 1)) a)) 2)

Здесь можно применять \(\beta\)-редукции от вложенного к внешнему редексу:

((lambda (a) ((lambda (b) (+ b 1)) a)) 2) ->
((lambda (a) (+ a 1)) 2) ->
(+ 2 1) ->
3

Либо от внешнего к внутреннему:

((lambda (a) ((lambda (b) (+ b 1)) a)) 2) ->
((lambda (b) (+ b 1)) 2) ->
(+ 2 1) ->
3

Если редексов в выражении больше нет, то он приведен к нормальной форме. Один из ключевых результатов теории лямбда-исчислениея — теорема Черча-Россера, в которой показано, что у каждого лямбда-выражения есть только одна нормальная форма.

Порядок выбора редексов определяется стратегией вычисления, из которых выделяют две главные:

1. аппликативная стратегия, где вычисления начинаются с самого левого редекса, не содержащего других редексов.
2. нормальная стратегия, вычисления по которой начинаем с самого левого внешнего редекса.

Другой важный результат — Теорема Карри — показывает, что если у терма есть нормальная форма, то нормальная стратегия приведет к ней. Но это никак не касается аппликативной стратегии, вычисления по которой могут зацикливаться даже при существовании нормальной формы.

В большинстве популярных языках программирования, кстати говоря, используется технически более эффективная аппликативная стратегия; нормальная же — в ленивых функциональных языках, вроде Haskell.

Упрощение выражений: \(\eta\)-преобразование

Самым простым и очевидным преобразованием является \(\eta\)-преобразование:

(lambda (x) (f x)) -> f

Здесь f — выражение, где нет свободных вхождений x, или, например, какая-нибудь именованная функцию. Т. е. если функция просто применяет другую функцию или выражение к своему аргументу, то мы можем ее заменить на ту же функцию (или выражение).

К чему это все?

Лямбда-исчисление и связанные с ним результаты регулярно упоминаются в контексте функциональных языков и их компиляторов; и смысл некоторых приемов техник невозможно освоить, не понимая основы теории. Например, знаменитый Y-комбинатор, волшебству которого я до сих пор не перестаю удивляться.

К тому же Лиспы и Схемы — почти дословная реализация лямбда-исчисления, что видно хотя бы даже и из приведенных здесь примеров на Scheme, и я, как пользователь Емакса, просто обязан понимать истоки этой традиции языков.