ния истинности формул в общем случае не имеет решения.
В основе лямбда-исчисление лежит понятие функции. Мы можем составлять сложные функции из про-
стейших, а также подставлять в функции аргументы, которые могут быть как константами так и другими
функциями. Как только мы составили выражение мы можем передать его вычислителю. Он подставляет ар-
гументы в функции и возвращает такое выражение, в котором невозможно далее проводить подстановки
аргументов. Этот процесс проведения подстановок считается вычислением алгоритма.
В рамках теории машин Тьюринга алгоритм описывается по-другому. Машина Тьюринга имеет внут-
реннее состояние, Состояние содержит некоторое значение, которое изменяется по ходу работы машины.
Машина живёт не сама по себе, она читает ленту символов. Лента символов – это большая цепочка букв.
На каждую букву машина реагирует серией действий. Она может изменить значение состояния, обновить
букву в ленте или перейти к следующему или предыдущему символу. Есть состояния, которые обозначают
конец работы, они называются терминальными. Как только машина дойдёт до терминального состояния мы
считаем, что вычисление алгоритма закончилось. После этого мы можем считать результат из состояний
машины.
Функциональные языки программирования основаны на лямбда-исчислении. Поэтому мы будем гово-
рить именно об этом описании алгоритма.
14.1 Лямбда исчисление без типов
Составление термов
Можно считать, что лямбда исчисление это такой маленький язык программирования. В нём есть множе-
ство символов, которые считаются переменными, они что-то обозначают и неделимы. В лямбда-исчислении
программный код называется термом. Для написания программного кода у нас есть всего три правила:
• Переменные x, y, z … являются термами.
• Если M и N – термы, то ( MN) – терм.
• Если x – переменная, а M – терм, то ( ?x. M) – терм
В формальном описании добавляют ещё одно правило, оно говорит о том, что других термов нет. Первое
правило, говорит о том, что у нас есть алфавит символов, который что-то обозначает, эти символы явля-
ются базовыми строительными блоками программы. Второе и третье правила говорят о том как из базовых
элементов получаются составные. Второе правило – это правило применения функции к аргументу. В нём
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 была свободной, но после подстановки стала связанной. Необходимо исключить такие
случаи. Поскольку с ними получается, что имена связанных переменных в определении функции влияют на
её смысл. Например смысл такого выражения
