ются базовыми строительными блоками программы. Второе и третье правила говорят о том как из базовых
элементов получаются составные. Второе правило – это правило применения функции к аргументу. В нём
M обозначает функцию, а N обозначает аргумент. Все функции являются функциями одного аргумента, но
они могут принимать и возвращать функции. Поэтому применение трёх аргументов к функции F un будет
выглядеть так:
216 | Глава 14: Лямбда-исчисление
((( F un Arg 1) Arg 2) Arg 3)
Третье правило говорит о том как создавать функции. Специальный символ лямбда ( ?) в выражении
( ?x. M ) говорит о том, что мы собираемся определить функцию с аргументом x и телом функции M . С та-
кими функциями мы уже сталкивались. Это безымянные функции. Приведём несколько примеров функций.
Начнём с самого простого, определим тождественную функцию:
( ?x. x)
Функция принимает аргумент x и тут же возвращает его в теле. Теперь посмотрим на константную функ-
цию:
( ?x. ( ?y. x))
Константная функция является функцией двух аргументов, поэтому наш терм принимает переменную
x и возвращает другой терм функцию ( ?y. x). Эта функция принимает y, а возвращает x. В Haskell мы бы
написали это так:
x -> (y -> x)
Точка сменилась на стрелку, а лямбда потеряла одну ножку. Теперь определим композицию. Композиция
принимает две функции одного аргумента и направляет выход второй функции на вход первой:
( ?f. ( ?g. ( ?x. ( f ( gx)))))
Переменные f и g – это функции, которые участвуют в композиции, а x это вход результирующей функ-
ции. Уже в таком простом выражении у нас пять скобок на конце. Давайте введём несколько соглашений,
которые облегчат написание термов:
Пишем
Подразумеваем
Опустим внешние скобки:
?x. x
( ?x. x)
В применении группируем скобки
f ghx
(( f g) h) x
влево:
Ф функциях группируем скобки
?x. ?y. x
( ?x. ( ?y. x))
вправо:
Пишем функции нескольких
?xy. x
( ?x. ( ?y. x))
аргументов с одной лямбдой:
С этими соглашениями мы можем переписать терм для композиции так:
?f gx. f ( gx)
Сравните с выражением на языке Haskell:
f g x -> f (g x)
Выражения очень похожи. Haskell иногда называют засахаренной версией лямбда исчисления. В лямбда-
исчислении мы не будем ставить пробелы для применения аргументов к функции. Мы будем считать, что
все имена однобуквенные. При этом переменные мы будем писать с маленькой буквы, а составные термы с
большой.
Определим ещё несколько функций. Например так выглядит функция flip:
?f xy. f yx
Или можно записать в более явном виде, выделим функцию двух аргументов:
?f. ?xy. f yx
Определим функцию on, она принимает функцию двух аргументов ? и функцию одного аргумента f, а
возвращает функцию двух аргументов, в которой к аргументам сначала применяется функция f, а затем они
передаются в функцию ?:
? ? f. ?x. ? ( f x)( f x)
В лямбда-исчислении есть только префиксное применение поэтому мы написали ?( fx)( fx) вместо при-
вычного ( fx) ? ( fx). Здесь операция ? это не только умножение, а любая бинарная функция.
Лямбда исчисление без типов | 217
Абстракция
Функции в лямбда-исчислении называют абстракциями. Мы берём терм M и параметризуем его по пе-
ременной x в выражении ?x.M. При этом если в терме M встречается переменная x, то она становится свя-
занной. Например в терме ?x.?y.x$ Переменная x является связанной, но в терме ?y.x, она уже не связана.
Такие переменные называют свободными. Множество связанных переменных терма M мы будем обозначать
BV ( M )$ от англ. bound variables, а множество свободных переменных мы будем обозначать F V ( M ) от англ.
free variables.
На интуитивном уровне процесс абстракции заключается в том, что мы смотрим на несколько частных
случаев и видим в них что-то общее. Это общее мы выделяем в функцию, которая параметризована частно-
стями. Например мы видим выражения:
?x. + xx,
?x. ? xx
И в том и в другом у нас есть функция двух аргументов + или ? и мы делаем из неё функцию одного
аргумента. Мы можем абстрагировать (параметризовать) это поведение в такую функцию:
?b. ?x. bxx
На Haskell мы бы записали это так:
b -> x -> b x x
Редукция. Вычисление термов
Процесс вычисления термов заключается в подстановке аргументов во все функции. Выражения вида:
( ?x. M ) N
Заменяются на
M [ x = N ]
Эта запись означает, что в терме M все вхождения x заменяются на терм N. Этот процесс называется
редукцией терма. А выражения вида ( ?x. M) N называются редексами. Проведём к примеру редукцию терма:
( ?b. ?x. bxx) ?
Для этого нам нужно в терме ( ?x. bxx) заменить все вхождения переменной b на переменную ?. После
этого мы получим терм:
?x. ? xx
В этом терме нет редексов. Это означает, что он вычислен или находится в нормальной форме.
?-преобразование
При подстановке необходимо следить за тем, чтобы у нас не появлялись лишние связывания переменных.
Например рассмотрим такой редекс:
( ?xy. x) y
После подстановки за счёт совпадения имён переменных мы получим тождественную функцию:
?y. y
Переменная y была свободной, но после подстановки стала связанной. Необходимо исключить такие
случаи. Поскольку с ними получается, что имена связанных переменных в определении функции влияют на
её смысл. Например смысл такого выражения