[ 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α. Стрелочный тип α → β как и в
Haskell говорит о том, что если у нас есть значение типа α, то с помощью операции применения мы можем
из терма с этим стрелочным типом получить терм типа β.
Опишем правила построения термов в лямбда-исчислении с типами:
• Переменные xα, yβ, zγ, … являются термами.
• Если Mα→β и Nα – термы, то ( Mα→βNα) β – терм.
• Если xα – переменная и Mβ – терм, то ( λxα. Mβ) α→β – терм
• Других термов нет.