плюсы и минусы. Теперь наша система является строго нормализуемой, это означает, что любой терм име-
ет нормальную форму. Но теперь мы не можем выразить все функции на числах. Например мы не можем
составить 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
Теория категорий