оборот. В такой интерпретации логическое отрицание можно закодировать с помощью функции flip. Также
мы можем выразить и другие логические операции:
And
=
?a b. a b F alse
Or
=
?a b. a T rue b
Мы определили логические значения не конкретными значениями, а свойствами функций. Мы построили
функции, которые ведут себя как логические значения. Этот способ определения напоминает, определение
класса типов. Мы объявили три метода T rue, F alse и If и сказали, что экземпляр класса должен удовле-
творять определённым свойствам, которые накладывают взаимные ограничения на методы класса. Ни один
из методов не имеет смысла по отдельности, важно то как они взаимодействуют.
Натуральные числа
Оказывается, что с помощью термов лямбда исчисления можно закодировать и натуральные числа с
арифметическими операциями. Мы будем кодировать числа Пеано. Для этого нам понадобится нулевой
элемент и функция определения следующего элемента. Их можно закодировать так:
Zero
=
?sz. z
Succ
=
?nsz. s( nsz)
Как и в случае логических значений числа кодируются функциями двух аргументов. Число определяется
по терму, подсчётом цепочки первых аргументов s. Например так выглядит число два:
Succ ( Succ Zero) ? ( ?nsz. s( nsz))( Succ Zero) ? ?sz. s(( Succ Zero) sz) ?
?sz. s(( ?nsz. s( nsz)) Zero) sz ? ?sz. s( s( Zero s z)) ? ?sz. s( sz)
И мы получили два вхождения первого аргумента в теле функции. Определим сложение и умножение.
Сложение принимает две функции двух аргументов и возвращает функцию двух аргументов.
Add = ? m n s z. m s ( n s z)
В этой функции мы применяем m раз аргумент s к значению, в котором аргумент s применён n раз, так
мы и получаем m + n применений аргумента s. Сложим 3 и 2:
Add 3 2 ? ?s z. 3 s (2 s z) ? ?s z. 3 s ( s ( s z)) ? ?s z. s ( s ( s ( s ( s z)))) ? 5
В умножении чисел m и n мы будем m раз складывать число n:
M ul = ?m n s z. m ( Add n) Zero
Лямбда исчисление без типов | 221
Конструктивная математика
В конструктивной математике существование объекта может быть доказано только описанием алгорит-
ма, с помощью которого можно построить объект. Например доказательство методом “от противного” от-
вергается.
Лямбда исчисление строит конструктивное описание функции. По лямбда-терму мы можем не только
вычислять значения функции, но и понять как она была построена. В классической теории, функция это
множество пар ( x, f( x)) аргумент-значение, которое обладает свойством:
x = y ? f ( x) = f ( y)
По этому определению мы ничего не можем сказать о внутренней структуре функции. Мы можем со-
бирать из одних функций другие с помощью подстановки значений, но мы никак не сможем понять, что
находится внутри функции. Лямбда исчисление решает эту проблему.
Расширение лямбда исчисления
Предположим, что мы решили написать язык программирования на основе лямбда-исчисления. Было бы
очень неэффективно представлять числа с помощью чисел Пеано. Ведь у нас есть процессор и мы можем
спросить у него чему равно значение и получить ответ очень быстро.
В этом случае пользуются расширенным лямбда исчислением. В нём два типа примитивов это перемен-
ные и константы. Для констант мы можем определять специальные правила редукции. Например мы можем
дополнить исчисление константами:
+ , ?, 0 , 1 , 2 , …
И ввести для них правила редукции, которые запрашивают ответ у процессора:
a + b
=
AddW ithCP U ( a, b)
a ? b = M ulW ithCP U ( a, b)
Так же мы можем определить и константы для логических значений:
T rue, F alse, If, N ot, And, Or
И определить правила редукции:
If T rue a b
=
a
If F alse a b
=
b
N ot T rue
=
F alse
N ot F alse
=
T rue
Add F alse a
=
F alse
Add T rue b
=
b
. . .
Такие правила называют ?-редукцией (дельта-редукция).
14.2 Комбинаторная логика
Одновременно с лямбда-исчислением развивалась комбинаторная логика. Она отличается более ком-
пактным представлением. Есть всего лишь одно правило, это применение функции к аргументу. А функции
строятся не из произвольных термов, а из набора основных функций. Набор основных функций называют
базисом.
Рассмотрим лямбда-термы:
?x. x,
?y. y,
?z. z
Все эти термы несут один и тот же смысл. Они представляют тождественную функцию. Они равны, но с
точностью до обозначений. Эта навязчивая проблема с переобозначением аргументов была решена в комби-
наторной логике. Посмотрим как строятся термы:
222 | Глава 14: Лямбда-исчисление
• Есть набор переменных x, y, z, …. Переменная – это терм.
• Есть две константы K и S, они являются термами.
• Если M и N – термы, то ( MN) – терм.
• Других термов нет.
Определены правила редукции для базисных термов:
Kxy
=
x
Sxyz
=
xz( yz)
В этих правилах мы пользуемся соглашением о расстановки скобок. Также как и в лямбда исчислении в
применении скобки группируются влево. Когда мы пишем Kxy, мы подразумеваем (( Kx) y). Термы в ком-
бинаторной логике принято называть комбинаторами. Редукция происходит до тех пор пока мы можем за-
менять вхождения базисных комбинаторов. Так если мы видим связку KXY или SXY Z, где X, Y , Z произ-
вольные термы, то мы можем их заменить согласно правилам редукции. Такие связки называют редексами.
Если в терме нет ни одного редекса, то он находится в нормальной форме. Замену редекса принято называть
свёрткой
Интересно, что комбинаторы K и S совпадают с определением класса Applicative для функций:
instance Applicative (r-> ) where
pure a r = a
( ) a b r = a r (b r)
В этом определении у функций есть общее окружение r, из которого они могут читать значения, так же как
и в случае типа Reader. В методе pure (комбинатор K) мы игнорируем окружение (это константная функция),
а в методе (комбинатор S) передаём окружение в функцию и аргумент и составляем применение функции
в контексте окружения r к значению, которое было получено в контексте того же окружения.
Вернёмся к проблеме различного представления тождественной функции в лямбда-исчислении. В ком-
бинаторной логике тождественная функция выражается так:
I = SKK
Проверим, определяет ли этот комбинатор тождественную функцию:
Ix = SKKx = Kx( Kx) = x
Сначала мы заменили I на его определение, затем свернули по комбинатору S, затем по левому комби-
натору K. В итоге получилось, что
Ix = x
Связь с лямбда-исчислением
Комбинаторная логика и лямбда-исчисление тесно связаны между собой. Можно определить функцию
?, которая переводит термы комбинаторной логики в термы лямбда-исчисления:
?( x)
=
x
?( K)
=
?xy. x
?( S)
=
?xyz. xz( yz)
?( XY )
=
?( X) ?( Y )
В первом уравнении x – переменная. Также можно определить функцию ?, которая переводит термы
лямбда-исчисления в термы комбинаторной логики.
Комбинаторная логика | 223
?( x)
=
x
?( XY )
=
?( X) ?( Y )
?( ?x. Y )
=
[ x] . ?( Y )
Запись [ x] . T , где x – переменная, T – терм, обозначает такой терм D, из которого можно получить терм
T подстановкой переменной x, выполнено свойство:
([ x] . T ) x = T
Эта запись означает параметризацию терма T по переменной x. Терм [ x] . T можно получить с помощью
следующего алгоритма:
[ x] . x
=
SKK
[ x] . X
=
KX,
x /
? V ( X)
[ x] . XY
=
S([ x] . X)([ x] . Y )
В первом уравнении мы заменяем переменную на тождественную функцию, поскольку переменные сов-
падают. Запись V ( X) во втором уравнении обозначает множество всех переменных в терме X. Поскольку
переменная по которой мы хотим параметризовать терм (или абстрагировать) не участвует в самом терме,
