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
Связь с лямбда-исчислением
Комбинаторная логика и лямбда-исчисление тесно связаны между собой. Можно определить функцию