λ-исчисление. Часть вторая: практика

Идею, короткий план и ссылки на основные источники для этой статьи мне подал хабраюзер z6Dabrata, за что ему огромнейшее спасибо.

Первая часть дала нам теоретическое представление о том, что есть лямбда-исчисление. В этой статье мы последуем неофициальной його-заповеди «Practice-practice-practice» и увидим его в действии.

Булевы константы Чёрча

Как уже говорилось ранее, в чистом бестиповом лямбда-исчислении отсутствует всё, кроме функций. Так что даже такие элементарные вещи, как числа или булевы значения необходимо реализовывать самим. Точнее, надо создать некие активные сущности, которые будут вести себя подобно необходимым нам объектам. И, естественно, процесс кодирования будет заключаться в написании соответствующих функций.

Начнём мы с самого простого: True и False. Два терма, воплощающие поведение этих констант, выглядят следующим образом:

tru = λt.λf.t	Двухаргументная функция, всегда возвращающая первый аргумент
fls = λt.λf.f	Двухаргументная функция, всегда возвращающая второй аргумент

Оператор if под такие булевы константы будет имеет вид:
if = λb. λx. λy.b x y
Здесь b — tru или fls, x — ветка then, y — ветка else.

Посмотрим, как это будет работать:
if fls t e

Поскольку условие if ложно (fls), то должно возвращаться выражение из ветки else (e в нашем случае).

(λb. λx. λy. b x y) fls t e	по определению if
(λx. λy. fls x y) t e	редукция подчёркнутого выражения из предыдущей строки
(λy. fls t y) e	редукция подчёркнутого выражения из предыдущей строки
fls t e	редукция подчёркнутого выражения из предыдущей строки
(λt.λf. f) t e	по определению fls
(λf. f) e	редукция подчёркнутого выражения из предыдущей строки
e	редукция подчёркнутого выражения из предыдущей строки

В определении основных булевых операторов тоже нет ничего сложного. Например, конъюнкция (логическое «и») будет выглядеть так:
and = λx. λy. x y fls

and получает два булевых значения x и y. Первым подставляется x (каррирование). Если он является tru (tru y fls после редукции), то вернётся y, который затем тоже «проверится» на истинность. Таким образом, итоговое tru мы получим только в случае, когда и x, и y «истинны». Во всех других вариантах ответом будет fls.

Числа Чёрча

Мы с вами будем кодировать только натуральные числа, для чего вспомним аксиомы Пеано, определяющие их множество. В основе реализации по-прежнему будут лежать функции, ведущие себя в заданном контексте подобно единице, двойке и т.д. Собственно, это одна из особенностей лямбда-исчисления: сущности, записанные в его терминах, не обладают самодостаточностью, поскольку воплощают поведение того или иного объекта.

Итак, нам нужна функция, принимающая два аргумента: фиксированное начальное значение и функцию для определения следующего элемента (функцию следования). Число будет закодировано в количестве применений функции следования к начальному значению:

0 ≡ λs.λz. z	функция s применяется к начальному значению z нуль раз
1 ≡ λs.λz. s z	функция s применяется к начальному значению z один раз
2 ≡ λs.λz. s (s z)	функция s применяется к начальному значению z два раза
...	и так далее

Легко заметить, что нуль кодируется так же, как и логическое False. Тем не менее, не стоит делать из этого какие-либо далеко идущие выводы: это всего лишь совпадение.

Задача функции следования состоит в том, чтобы прибавить к заданному числу единицу. Т.е. в качестве аргумента она будет принимать значение, которое требуется увеличить, и которое тоже является функцией двух аргументов. Таким образом, суммарно функция (+1) имеет три аргумента: предшествующее число Чёрча n, функцию, которую надо будет применить n+1 раз к начальному значению, и само начальное значение. Выглядит это так:
scc = λn. λs. λz. s (n s z)
Здесь n s z — n раз применённая к z функция s. Но нам нужно применить её n+1 раз, откуда и берётся явное s (n s z).

Допустим, нам надо получить из «единицы» one = λs.λz. s z «двойку» two = λs.λz. s (s z). Произойдёт это так:

scc one s' z'	s' и z' — чтобы не путать подставляемые значения с именами переменных
(λn. λs. λz. s (n s z)) one s' z'	по определению scc
(λs. λz. s (one s z)) s' z'	редукция подчёркутого выражения из предыдущей строки
(λz. s' (one s' z)) z'	редукция подчёркутого выражения из предыдущей строки
s' (one s' z')	редукция подчёркутого выражения из предыдущей строки
s' ((λs.λz. s z) s' z')	по определению one
s' ((λz. s' z) z')	редукция подчёркутого выражения из предыдущей строки
s' (s' z')	редукция подчёркутого выражения из предыдущей строки
two s' z'	по определению two

Арифметические операции

Сложение

Функция, осуществляющая сложение двух чисел Чёрча, будет принимать два слагаемых: x и y, которые в свою очередь тоже имеют по два аргумента — s (функцию следования) и z (начальное значение). Сложение будет состоять в том, чтобы сначала применить s к z x раз, а потом ещё y раз.

plus = λx. λy. λs. λz. x s (y s z)

В качестве примера сложим one = λs.λz. s z и two = λs.λz. s (s z). Ответ должен будет выглядеть так: three = λs.λz. s (s (s z)).

plus one two s' z'	s' и z' — чтобы не путать подставляемые значения с именами переменных
(λx. λy. λs. λz. x s (y s z)) one two s' z'	по определению plus
one s' (two s' z')	после проведения редукции
(λs.λz. s z) s' (two s' z')	по определению one
s' (two s' z')	после проведения редукции
s' (( λs.λz. s (s z) s' z')	по определению two
s' (s' (s' z'))	после проведения редукции
three s' z'	по определению three

Умножение

Функцию для умножения можно определить через функцию сложения. В конце-концов, умножить x на y означает сложить x копий y.

times = λx. λy. x (plus y) z

Есть ещё один способ определения умножения на числах Чёрча, без использования plus. Его идея заключается в том, что для получения произведения x и y нужно x раз взять y раз применённую к начальному значению функцию s:

times' = λx.λy.λs.λz. x (y s) z

Для примера умножим two = λs.λz. s (s z) на three = λs.λz. s (s (s z)). Результат должен будет иметь вид: six = λs.λz. s (s (s (s (s (s z))))).

times' two three s' z'	s' и z' — чтобы не путать подставляемые значения с именами переменных
(λx.λy.λs.λz. x (y s) z) two three s' z'	по определению times'
two (three s') z'	после проведения редукции
(λs.λz. s (s z)) (three s') z'	по определению two
three s' ((three s') z')	после проведения редукции
(λs.λz. s (s (s z))) s' ((three s') z')	по определению three
s' (s' (s' ((three s') z')))	после проведения редукции
s' (s' (s' (((λs.λz. s (s (s z))) s') z')))	по определению three
s' (s' (s' (((λz. s' (s' (s' z))) z')))	после проведения редукции
s' (s' (s' (s' (s' (s' z')))))	редукция подчёркнутого выражения
six s' z'	по определению six

Последней нерассмотренной операцией является вычитание — не самая тривиальная вещь на числах Чёрча. Желающие могут изучить её самостоятельно, например, по книге Бенжамина Пирса «Types and Programming Languages».
Цитата для привлечения внимания из вики-конспекта по лямбда-исчислению: «Если вы ничего не поняли, не огорчайтесь. Вычитание придумал Клини, когда ему вырывали зуб мудрости. А сейчас наркоз уже не тот».

Заключение

Как видим, технически ничего сложного в лямбда-исчислении нет: всё сводится к элементарным подстановкам и редукциям. Но столь малого набора инструментов вполне хватает, чтобы при желании реализовать активные сущности, ведущие себя подобно парам, спискам, рекурсивным функциям и т.п. Они будут достаточно громоздкими, но, как уже говорилось, λ-исчисление предназначено не для написания программ, а для исследования и спецификации языков программирования и систем типов. С чем, собственно, и прекрасно справляется.

Список источников

1. «What is Lambda Calculus and should you care?», Erkki Lindpere
2. «Types and Programming Languages», Benjamin Pierce
3. Вики-конспект «Лямбда-исчисление»
4. «Учебник по Haskell», Антон Холомьёв
5. Лекции по функциональному программированию