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: