принимает две функции одного аргумента и направляет выход второй функции на вход первой:
( λ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)
Сравните с выражением на языке Haskelclass="underline"
\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
В этом терме нет редексов. Это означает, что он вычислен или находится в нормальной форме.
α-преобразование
При подстановке необходимо следить за тем, чтобы у нас не появлялись лишние связывания переменных.
Например рассмотрим такой редекс: