Лямбда-исчисление на пальцах
За последние месяцы перечитал несколько книг по теории языков программированию, реализации Лиспов и
основам функционального программирования. В
Функции на функциях от функций к функциям
Начнем, собственно, с
В оригинальном
<expression> ::= <variable> | (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, или, например,
К чему это все?
К тому же Лиспы и Схемы — почти дословная реализация
Комментарии
Comments powered by Disqus