дополнить исчисление константами:
+ , ?, 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. Поскольку
переменная по которой мы хотим параметризовать терм (или абстрагировать) не участвует в самом терме,
мы можем проигнорировать её с помощью постоянной функции K. В последнем уравнении мы параметри-
зуем применение.
С помощью этого алгоритма можно для любого терма T , все переменные которого содержатся в
{x 1 , …xn} составить такой комбинатор D, что Dx 1 …xn = T . Для этого мы последовательно парметризуем
терм T по всем переменным:
[ x 1 , …, xn] . T = [ x 1] . ([ x 2 , …, xn] . T )
Так постепенно мы придём к выражению, считаем что скобки группируются вправо:
[ x 1] . [ x 2] . … [ xn] . T
Немного истории
Комбинаторную логику открыл Моисей Шейнфинкель. В 1920 году на докладе в Гёттингене он рассказал
основные положения этой теории. Комбинаторная логика направлена на выделение простейших строитель-
ных блоков математической логики. В этом докладе появилось понятие частичного применения. Шейнфин-
кель показал как функции многих переменных могут быть сведены к функциям одного переменного. Далее
в докладе описываются пять основных функций, называемых комбинаторами:
Ix
= x
– функция тождества
Cxy = x
– константная функция
T xyz = xzy