Unknown - haskell-notes

и неразрешимость исчисления логики предикатов первого порядка. Система аксиом называется разрешимой

в том случае, если существует такой алгоритм, который позволяет по виду формулы определить следует ли

она из заданных аксиом или нет.

Посмотрим как с помощью термов кодируются структуры данных. Далее для сокращения записи мы бу-

дем считать, что в лямбда исчислении можно определять синонимы с помощью знака равно. Запись 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 )

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