Или можно записать в более явном виде, выделим функцию двух аргументов:
λ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 была свободной, но после подстановки стала связанной. Необходимо исключить такие
случаи. Поскольку с ними получается, что имена связанных переменных в определении функции влияют на
её смысл. Например смысл такого выражения
( λxz. x) y
После подстановки будет совсем другим. Но мы всего лишь изменили обозначение локальной перемен-