ные и константы. Для констант мы можем определять специальные правила редукции. Например мы можем
дополнить исчисление константами:
+ , ∗, 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 )