Лямбда-исчисление на пальцах
За последние месяцы перечитал несколько книг по теории языков программированию, реализации Лиспов и основам функционального программирования. В какой-то момент я понял, что некоторые базовые вещи, связанные с лямбда-исчислением ("\(\lambda\)-исчисление"), у меня постоянно вылетают из головы. Этим постом я постараюсь прояснить для себя и немногочисленных читателей основные идеи, на которые опирается теория функциональных языков программирования.
Функции на функциях от функций к функциям
Начнем, собственно, с лямбда-исчисления. Использовать я буду не авторскую нотацию, а подмножество языка 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
Если редексов в выражении больше нет, то он приведен к нормальной форме. Один из ключевых результатов теории лямбда-исчислениея - теорема Черча-Россера, в которой показано, что у каждого лямбда-выражения есть только одна нормальная форма.
Порядок выбора редексов определяется стратегией вычисления, из которых выделяют две главные:
- аппликативная стратегия, где вычисления начинаются с самого левого редекса, не содержащего других редексов.
- нормальная стратегия, вычисления по которой начинаем с самого левого внешнего редекса.
Другой важный результат - Теорема Карри - показывает, что если у терма есть нормальная форма, то нормальная стратегия приведет к ней. Но это никак не касается аппликативной стратегии, вычисления по которой могут зацикливаться даже при существовании нормальной формы.
В большинстве популярных языках программирования, кстати говоря, используется технически более эффективная аппликативная стратегия; нормальная же - в ленивых функциональных языках, вроде Haskell.
Упрощение выражений: \(\eta\)-преобразование
Самым простым и очевидным преобразованием является \(\eta\)-преобразование:
(lambda (x) (f x)) -> f
Здесь f - выражение, где нет свободных вхождений x, или, например, какая-нибудь именованная функцию. Т.е. если функция просто применяет другую функцию или выражение к своему аргументу, то мы можем ее заменить на ту же функцию (или выражение).
К чему это все?
Лямбда-исчисление и связанные с ним результаты регулярно упоминаются в контексте функциональных языков и их компиляторов; и смысл некоторых приемов техник невозможно освоить, не понимая основы теории. Например, знаменитый Y-комбинатор, волшебству которого я до сих пор не перестаю удивляться.
К тому же Лиспы и Схемы - почти дословная реализация лямбда-исчисления, что видно хотя бы даже и из приведенных здесь примеров на Scheme, и я, как пользователь Емакса, просто обязан понимать истоки этой традиции языков.