– функция перестановки
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?) ?>? – терм
• Других термов нет.
Типизация накладывает ограничение на то, какие выражения мы можем комбинировать. В этом есть
плюсы и минусы. Теперь наша система является строго нормализуемой, это означает, что любой терм име-
ет нормальную форму. Но теперь мы не можем выразить все функции на числах. Например мы не можем
составить Y -комбинатор, поскольку теперь самоприменение ( ee) невозможно.
Мы ввели типы, но лишились рекурсии. Как нам быть? Эта проблема решается с помощью введения
специальной константы Y ( ?>?) >?
?
, которая обозначает комбинатор неподвижной точки. Правило редукции
для Y :
( Y? f ?>? ) ? = ( f ?>? ( Y? f ?>? )) ?
Можно убедиться в том, что это правило роходит проверку типов. Типизированное лямбда-исчисление
дополненное комбинатором неподвижной точки способно выразить все числовые функции.
14.4 Краткое содержание
В этой главе мы познакомились с лямбда-исчислением и комбинаторной логикой, двумя конструктив-
ными теориями функций. Конструктивными в том смысле, что определение функции содержит не набор
значений, а рецепт получения этих значений. В лямбда-исчислении мы видим как функция была построена,
из каких простейших частей она состоит. Редукция термов позволяет вычислять функции.
Мы узнали, что функциями можно кодировать логические значения и числа. Узнали, что все численные
функции могут быть закодированы лямбда-термами.
14.5 Упражнения
• С помощью редукции убедитесь в том, что верны формулы (в терминах Карри) :
B
=
S( KS) S
C
=
S( BBS)( KK)
Bxyz
=
xzy
Cxyz
=
x( yz)
• Попробуйте закодировать пары с помощью лямбда термов. Вам необходимо построить три функции:
P air, F st, Snd, которые обладают свойствами:
Лямбда-исчисление с типами | 225
F st ( P air a b)
=
a
Snd ( P air a b)
=
b
• в комбинаторной логике тоже есть комбинатор неподвижной точки, найдите его с помощью алгоритма
приведения термов лямбда исчисления к термам комбинаторной логики. Для краткости лучше вместо
SKK писать просто I.
• Напишите типы Lam и App, которые описывают лямбда-термы и термы комбинаторной логики в Haskell.
Напишите функции перевода из значений Lam в App и обратно.
226 | Глава 14: Лямбда-исчисление
Глава 15
Теория категорий
Многие понятия в Haskell позаимствованы из теории категорий, например это функторы, монады. Теория
категорий – это скорее язык, математический жаргон, она настолько общая, что кажется ей нет никакого
применения. Возможно это и так, но в этом языке многие сущности, которые лишь казались родственными
и было смутное интуитивное ощущение их близости, становятся тождественными.
Теория категорий занимается описанием функций. В лямбда-исчислении основной операцией была под-
становка значения в функцию, а в теории категорий мы сосредоточимся на операции композиции. Мы будем
соединять различные объекты так, чтобы структура объектов сохранялась. Структура объекта будет опреде-
ляться свойствами, которые продолжают выполнятся после преобразования объекта.
15.1 Категория
Мы будем говорить об объектах и связях между ними. Связи принято называть “стрелками” или “мор-
физмами”. Далее мы будем пользоваться термином стрелка. У стрелки есть начальный объект, его называют
доменом (domain) и конечный объект, его называют кодоменом (codomain).
f
A
B
В этой записи стрелка f соединяет объекты A и B, в тексте мы будем писать это так f : A > B, словно
стрелка это функция, а объекты это типы. Мы будем обозначать объекты большими буквами A, B, C, …, а
стрелки – маленькими буквами f, g, h, … Для того чтобы связи было интереснее изучать мы введём такое
правило:
f
A
B
g
f ; g
C
Если конец стрелки f указывает на начало стрелки g, то должна быть такая стрелка f ; g, которая обозна-