=
φ( 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
– функция перестановки
Zxyz = x( yz)
– функция группировки
Sxyz = xz( yz)
– функция слияния
С помощью этих функций можно избавиться в формулах от переменных, так например свойство комму-
тативности функции A можно представить так: T A = A. Эти комбинаторы зависят друг от друга. Можно
убедиться в том, что:
I
=
SCC
Z
=
S( CS) S
T
=
S( ZZS)( CC)
Все комбинаторы выражаются через комбинаторы C и S. Ранее мы пользовались другими обозначениями
для этих комбинаторов. Обозначения K и S ввёл Хаскель Карри (Haskell Curry). Независимо от Шейнфинкеля
он переоткрыл комбинаторную логику и существенно развил её. В современной комбинаторной логике для
обозначения комбинаторов I, C, T , Z и S (по Шейнфинкелю) принято использовать имена I, K, C, B, S
(по Карри).
224 | Глава 14: Лямбда-исчисление
14.3 Лямбда-исчисление с типами
Мы можем добавить в лямбда-исчисление типы. Предположим, что у нас есть множество V базовых типов.
Тогда тип это:
T = V | T → T
Тип может быть либо одним элементом из множества базовых типов. Либо стрелочным (функциональ-
ным) типом. Выражение “терм M имеет тип α” принято писать так: Mα. Стрелочный тип α → β как и в