Кодирование структур данных
Вы наверное заметили, что пока мы составляли лишь обобщённые функции. Эти функции комбинируют
другие функции, они не выполняют никаких действий над элементами. Что если нам захочется вычислять
логические значения или воспользоваться числами?
Оказывается, что логические значения, числа, пары, списки и другие конструкции могут быть закодиро-
ваны с помощью термов лямбда-исчисления. Тезис Чёрча утверждает, что с помощью лямбда-терма можно
представить любую вычислимую числовую функцию. В 1936 году Чёрч с помощью лямбда-исчисления дока-
зал существование неразрешимых проблем в теории чисел. Из этого следовала неразрешимость арифметики
и неразрешимость исчисления логики предикатов первого порядка. Система аксиом называется разрешимой
в том случае, если существует такой алгоритм, который позволяет по виду формулы определить следует ли
она из заданных аксиом или нет.
Посмотрим как с помощью термов кодируются структуры данных. Далее для сокращения записи мы бу-
дем считать, что в лямбда исчислении можно определять синонимы с помощью знака равно. Запись N = M
говорит о том, что мы дали обозначение 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)
По этому определению мы ничего не можем сказать о внутренней структуре функции. Мы можем со-
бирать из одних функций другие с помощью подстановки значений, но мы никак не сможем понять, что
находится внутри функции. Лямбда исчисление решает эту проблему.
Расширение лямбда исчисления
Предположим, что мы решили написать язык программирования на основе лямбда-исчисления. Было бы
очень неэффективно представлять числа с помощью чисел Пеано. Ведь у нас есть процессор и мы можем
спросить у него чему равно значение и получить ответ очень быстро.
В этом случае пользуются расширенным лямбда исчислением. В нём два типа примитивов это перемен-
ные и константы. Для констант мы можем определять специальные правила редукции. Например мы можем