Учебник по Haskell

говорит о том, что мы дали обозначение N терму M. Этой операции нет в лямбда-исчислении, но мы будем

пользоваться ею для удобства.

Логические значения

Суть логических значений заключается в операторе If, с помощью которого мы можем организовывать

ветвление алгоритма. Есть два терма T rue и F alse, которые для любых термов a и b, обладают свойствами:

If T rue a b

=

a

If F alse a b

=

b

Термы T rue, F alse и If, удовлетворяющие таким свойствам выглядят так:

T rue

=

λt f. t

F alse

=

λt f. f

If

=

λb x y. bxy

220 | Глава 14: Лямбда-исчисление

Проверим выполнение свойств:

If T rue a b ⇒ ( λb x y. bxy)( λt f. t) a b ⇒ ( λt f. t) a b ⇒ a

If F alse a b ⇒ ( λb x y. bxy)( λt f. f ) a b ⇒ ( λt f. f ) a b ⇒ b

Свойства выполнены. Логические константы кодируются постоянными функциями двух аргументов.

Функция True возвращает первый аргумент, игнорируя второй. А функция False делает то же самое, но на-

оборот. В такой интерпретации логическое отрицание можно закодировать с помощью функции flip. Также

мы можем выразить и другие логические операции:

And

=

λa b. a b F alse

Or

=

λa b. a T rue b

Мы определили логические значения не конкретными значениями, а свойствами функций. Мы построили

функции, которые ведут себя как логические значения. Этот способ определения напоминает, определение

класса типов. Мы объявили три метода T rue, F alse и If и сказали, что экземпляр класса должен удовле-

творять определённым свойствам, которые накладывают взаимные ограничения на методы класса. Ни один

из методов не имеет смысла по отдельности, важно то как они взаимодействуют.

Натуральные числа

Оказывается, что с помощью термов лямбда исчисления можно закодировать и натуральные числа с

арифметическими операциями. Мы будем кодировать числа Пеано. Для этого нам понадобится нулевой

элемент и функция определения следующего элемента. Их можно закодировать так:

Zero

=

λsz. z

Succ

=

λnsz. s( nsz)

Как и в случае логических значений числа кодируются функциями двух аргументов. Число определяется

по терму, подсчётом цепочки первых аргументов s. Например так выглядит число два:

Succ ( Succ Zero) ⇒ ( λnsz. s( nsz))( Succ Zero) ⇒ λsz. s(( Succ Zero) sz) ⇒

λsz. s(( λnsz. s( nsz)) Zero) sz ⇒ λsz. s( s( Zero s z)) ⇒ λsz. s( sz)

И мы получили два вхождения первого аргумента в теле функции. Определим сложение и умножение.

Сложение принимает две функции двух аргументов и возвращает функцию двух аргументов.

Add = λ m n s z. m s ( n s z)

В этой функции мы применяем m раз аргумент s к значению, в котором аргумент s применён n раз, так

мы и получаем m + n применений аргумента s. Сложим 3 и 2:

Add 3 2 ⇒ λs z. 3 s (2 s z) ⇒ λs z. 3 s ( s ( s z)) ⇒ λs z. s ( s ( s ( s ( s z)))) ⇒ 5

В умножении чисел m и n мы будем m раз складывать число n:

M ul = λm n s z. m ( Add n) Zero

Лямбда исчисление без типов | 221

Конструктивная математика

В конструктивной математике существование объекта может быть доказано только описанием алгорит-

ма, с помощью которого можно построить объект. Например доказательство методом “от противного” от-

вергается.

Лямбда исчисление строит конструктивное описание функции. По лямбда-терму мы можем не только

вычислять значения функции, но и понять как она была построена. В классической теории, функция это

множество пар ( x, f( x)) аргумент-значение, которое обладает свойством:

x = y ⇒ f ( x) = f ( y)

По этому определению мы ничего не можем сказать о внутренней структуре функции. Мы можем со-

бирать из одних функций другие с помощью подстановки значений, но мы никак не сможем понять, что

находится внутри функции. Лямбда исчисление решает эту проблему.

Расширение лямбда исчисления

Предположим, что мы решили написать язык программирования на основе лямбда-исчисления. Было бы

очень неэффективно представлять числа с помощью чисел Пеано. Ведь у нас есть процессор и мы можем

спросить у него чему равно значение и получить ответ очень быстро.

В этом случае пользуются расширенным лямбда исчислением. В нём два типа примитивов это перемен-

ные и константы. Для констант мы можем определять специальные правила редукции. Например мы можем

дополнить исчисление константами:

+ , ∗, 0 , 1 , 2 , ...

И ввести для них правила редукции, которые запрашивают ответ у процессора:

a + b

=

AddW ithCP U ( a, b)

a ∗ b = M ulW ithCP U ( a, b)

Так же мы можем определить и константы для логических значений:

T rue, F alse, If, N ot, And, Or

И определить правила редукции:

If T rue a b

=

a

If F alse a b

=

b

N ot T rue

=

F alse

N ot F alse

=

T rue

Add F alse a

=

F alse

Add T rue b

=

b