Кодирование Чёрча — λ-исчисление

В чистом λ-исчислении нет ни чисел, ни булевых значений, ни структур — только функции. Кодирование Чёрча показывает, что ничего другого и не нужно: данные — это их собственные операции обработки.

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

\displaystyle \mathbf{tru}

\displaystyle {} = \lambda t\,f.\,t,

\displaystyle \mathbf{fls}

\displaystyle {} = \lambda t\,f.\,f

(1.11)

Здесь $t$ и $f$ — это просто два аргумента (мнемоника: ветка «true» и ветка «false»): $\mathbf{tru}$ возвращает первый, а $\mathbf{fls}$ — второй. То есть само булево значение — это уже выбор одного из двух, готовый $\mathbf{if}$ .

\displaystyle \mathbf{if}

\displaystyle {} = \lambda b\,t\,e.\,b\,t\,e,

\displaystyle \mathbf{not}

\displaystyle {} = \lambda b.\,b\,\mathbf{fls}\,\mathbf{tru}

(1.12)

Здесь $\mathbf{if}$ почти ничего не делает сам: он берёт булево значение $b$ и отдаёт ему две ветки $t$ и $e$ , а $b$ уже выбирает нужную. $\mathbf{not}$ устроен так же просто: он даёт булевому значению ветки в обратном порядке, поэтому правда выбирает ложь, а ложь — правду.

\displaystyle \mathbf{and}

\displaystyle {} = \lambda p\,q.\,p\,q\,p,

\displaystyle \mathbf{or}

\displaystyle {} = \lambda p\,q.\,p\,p\,q

(1.13)

В $\mathbf{and}$ первое булево значение $p$ решает, что вернуть: если $p$ истинно, результат зависит от $q$ , а если ложно, сразу возвращается ложь. В $\mathbf{or}$ наоборот: если $p$ истинно, можно сразу вернуть правду, а если ложно, приходится смотреть на $q$ .

Подставим истину ( $1$ ${} = \mathbf{tru}$ , $0$ ${} = \mathbf{fls}$ ) и произведём редукции:

\displaystyle \mathbf{not}\;\mathbf{tru} \;

\displaystyle {} \to_\beta\; \mathbf{tru}\;\mathbf{fls}\;\mathbf{tru} \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{fls} \qquad (\lnot 1 = 0)

\displaystyle \mathbf{and}\;\mathbf{tru}\;\mathbf{tru} \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{tru}\;\mathbf{tru}\;\mathbf{tru} \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{tru} \qquad (1 \land 1 = 1)

\displaystyle \mathbf{or}\;\mathbf{tru}\;\mathbf{tru} \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{tru}\;\mathbf{tru}\;\mathbf{tru} \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{tru} \qquad (1 \lor 1 = 1)

Теперь поговорим о парах: это очень важный тип, который широко используется в Haskell. Пара — функция, хранящая два значения и ждущая «получателя»:

\displaystyle \mathbf{pair}

\displaystyle {} = \lambda x\,y\,f.\,f\,x\,y,

\displaystyle \mathbf{fst}

\displaystyle {} = \lambda p.\,p\,\mathbf{tru},

\displaystyle \mathbf{snd}

\displaystyle {} = \lambda p.\,p\,\mathbf{fls}

(1.14)

$\mathbf{fst}$ передаёт паре $\mathbf{tru}$ , а $\mathbf{snd}$ — $\mathbf{fls}$ , и та отдаёт нужную компоненту:

\displaystyle \mathbf{fst}\,(\mathbf{pair}\;a\;b) \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{tru}\;a\;b \;

\displaystyle {} \twoheadrightarrow_\beta\; a

\displaystyle \mathbf{snd}\,(\mathbf{pair}\;a\;b) \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{fls}\;a\;b \;

\displaystyle {} \twoheadrightarrow_\beta\; b

Заметьте, как интересно: функции $\mathbf{fst}$ и $\mathbf{snd}$ принимают аргумент-пару и передают ей управление — дальше она сама решает, что возвращать. Это, так сказать, функции-декораторы.

Теперь самое насущное — натуральные числа. Число $n$ — это «применить функцию $n$ раз»:

\displaystyle \overline{n}

\displaystyle {} = \lambda f\,x.\,f^{\,n}(x): \qquad \overline{0}

\displaystyle {} = \lambda f\,x.\,x,

\displaystyle \overline{1}

\displaystyle {} = \lambda f\,x.\,f\,x,

\displaystyle \overline{2}

\displaystyle {} = \lambda f\,x.\,f\,(f\,x)

(1.15)

Важно: $f$ и $x$ здесь произвольные — их подставляет тот, кто пользуется числом. Нумерал фиксирует только «сколько раз применить», а не «что применять».

Скормим нумералу функцию $f$ и аргумент $x$ — и он применит $f$ ровно столько раз, сколько задаёт число:

\displaystyle \overline{0}\;f\;x \;

\displaystyle {} \twoheadrightarrow_\beta\; x

\displaystyle \overline{3}\;f\;x \;

\displaystyle {} \twoheadrightarrow_\beta\; f\,(f\,(f\,x))

Теперь научимся считать — вся арифметика вырастает из одного приёма «применить $f$ нужное число раз».

Начнём с прибавления единицы: $\mathbf{succ}$ навешивает на число ещё одно применение $f$ :

\displaystyle \mathbf{succ}

\displaystyle {} = \lambda n\,f\,x.\,f\,(n\,f\,x)

(1.16)

\displaystyle \mathbf{succ}\;\overline{n} \;

\displaystyle {} \to_\beta\; \lambda f\,x.\,f\,(\overline{n}\,f\,x) \;

\displaystyle {} \twoheadrightarrow_\beta\; \lambda f\,x.\,f\bigl(f^{\,n}(x)\bigr) \;

\displaystyle {} =\; \lambda f\,x.\,f^{\,n+1}(x) \;

\displaystyle {} =\; \overline{n+1}

Сложение продолжает эту идею — применяет $f$ сначала $\overline{n}$ раз, а потом ещё $\overline{m}$ :

\displaystyle \mathbf{add}

\displaystyle {} = \lambda m\,n\,f\,x.\,m\,f\,(n\,f\,x)

(1.17)

\displaystyle \mathbf{add}\;\overline{m}\;\overline{n} \;

\displaystyle {} \twoheadrightarrow_\beta\; \lambda f\,x.\,\overline{m}\,f\,(\overline{n}\,f\,x) \;

\displaystyle {} \twoheadrightarrow_\beta\; \lambda f\,x.\,f^{\,m}\bigl(f^{\,n}(x)\bigr) \;

\displaystyle {} =\; \overline{m+n}

Умножение — это уже повторное сложение:

\displaystyle \mathbf{mul}

\displaystyle {} = \lambda m\,n\,f.\,m\,(n\,f)

(1.18)

\displaystyle \mathbf{mul}\;\overline{m}\;\overline{n} \;

\displaystyle {} \twoheadrightarrow_\beta\; \lambda f.\,\overline{m}\,(\overline{n}\,f) \;

\displaystyle {} \twoheadrightarrow_\beta\; \lambda f\,x.\,\bigl(f^{\,n}\bigr)^{m}(x) \;

\displaystyle {} =\; \lambda f\,x.\,f^{\,mn}(x) \;

\displaystyle {} =\; \overline{mn}

Возведение в степень — повторное умножение, и в записи оно совсем короткое:

\displaystyle \mathbf{pow}

\displaystyle {} = \lambda m\,n.\,n\,m

(1.19)

\displaystyle \mathbf{pow}\;\overline{m}\;\overline{n} \;

\displaystyle {} \to_\beta\; \overline{n}\,\overline{m} \;

\displaystyle {} \twoheadrightarrow_\beta\; \overline{m^{\,n}}

В $\mathbf{pow}$ аргументы просто меняются местами: $\overline{n}\,\overline{m}$ — это $\overline{m}$ , применённое как функция $n$ раз, что и даёт $\overline{m^{\,n}}$ .

Вычитание неожиданно трудно: $\mathbf{pred}$ строится через пары — прогоняем по числу пару $(i-1,\,i)$ и берём первую компоненту:

\displaystyle \mathbf{pred}

\displaystyle {} = \lambda n.\,\mathbf{fst}\,\bigl(n\;(\lambda p.\,\mathbf{pair}\,(\mathbf{snd}\,p)\,(\mathbf{succ}\,(\mathbf{snd}\,p)))\;(\mathbf{pair}\,\overline{0}\,\overline{0})\bigr)

(1.20)

По распространённой легенде Стивен Клини придумал функцию-предшественник ( $\mathbf{pred}$ , predecessor) — ключ к вычитанию нумералов Чёрча — прямо в кресле у стоматолога.

На $\mathbf{pred}$ держится всё «вычитательное»: само вычитание — это многократный $\mathbf{pred}$ , а деление — многократное вычитание. Отдельного λ-определения для деления не приводим: новой идеи там нет, тот же $\mathbf{pred}$ в цикле, только запись громоздкая.

Проверим $\mathbf{pred}$ на общем нумерале $\overline{n}$ . Обозначим шаг $\sigma$ ${} = \lambda p.\,\mathbf{pair}\,(\mathbf{snd}\,p)\,(\mathbf{succ}\,(\mathbf{snd}\,p))$ — он сдвигает пару: роняет первую компоненту и наращивает вторую:

\displaystyle \sigma\,(\mathbf{pair}\;a\;b) \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{pair}\;b\;(\mathbf{succ}\;b)

Подставляем $\overline{n}$ в определение — это значит применить $\sigma$ ровно $n$ раз к стартовой паре $\mathbf{pair}\,\overline{0}\,\overline{0}$ :

\displaystyle \mathbf{pred}\;\overline{n} \;

\displaystyle {} \to_\beta\; \mathbf{fst}\,\bigl(\overline{n}\,\sigma\,(\mathbf{pair}\,\overline{0}\,\overline{0})\bigr) \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{fst}\,\bigl(\sigma^{\,n}(\mathbf{pair}\,\overline{0}\,\overline{0})\bigr)

Пары бегут по цепочке — вторая компонента считает шаги, первая отстаёт на единицу:

\displaystyle \mathbf{pair}\,\overline{0}\,\overline{0} \;

\displaystyle {} \to\; \mathbf{pair}\,\overline{0}\,\overline{1} \;

\displaystyle {} \to\; \mathbf{pair}\,\overline{1}\,\overline{2} \;

\displaystyle {} \to\; \cdots \;

\displaystyle {} \to\; \mathbf{pair}\,\overline{n-1}\,\overline{n}

Осталось взять первую компоненту:

\displaystyle \mathbf{pred}\;\overline{n} \;

\displaystyle {} \twoheadrightarrow_\beta\; \mathbf{fst}\,(\mathbf{pair}\,\overline{n-1}\,\overline{n}) \;

\displaystyle {} \twoheadrightarrow_\beta\; \overline{n-1}

У $\overline{0}$ цепочка не двигается, поэтому $\mathbf{pred}\,\overline{0}$ ${} \twoheadrightarrow_\beta \overline{0}$ — предшественником нуля считаем нуль.

\displaystyle \mathbf{iszero}

\displaystyle {} = \lambda n.\,n\,(\lambda z.\,\mathbf{fls})\,\mathbf{tru}

(1.21)

$\mathbf{iszero}$ скармливает числу функцию, которая на каждом шаге отвечает $\mathbf{fls}$ , и старт $\mathbf{tru}$ : у нуля шагов нет — остаётся $\mathbf{tru}$ , а у любого другого числа хотя бы один шаг даёт $\mathbf{fls}$ .

Список — его собственная правая свёртка (fold-кодирование):

\displaystyle [x_1, \dots, x_n] \;

\displaystyle {} \rightsquigarrow\; \lambda c\,n.\,c\,x_1\,(c\,x_2\,(\cdots(c\,x_n\,n)))

(1.22)

Тот же приём в Haskell — тип $\mathtt{foldr}$ : список полностью определяется тем, как он сворачивается. Нумерал Чёрча — «список из $n$ одинаковых применений».

-- список строится конструктором (:) (cons) и завершается [] (nil):
[1, 2, 3]  ==  1 : (2 : (3 : []))   -- True

-- Чёрч-кодирование — та же цепочка, только (:) и [] вынесены в параметры;
-- в Haskell это ровно foldr:
foldr (:) []  [1, 2, 3]   -- 1 : (2 : (3 : [])) = [1,2,3]   (собрали список обратно)
foldr (+) 0   [1, 2, 3]   -- 1 + (2 + (3 + 0))  = 6         (свернули в сумму)

Ну ведь есть же нормальное программирование, в котором есть и числа, и даже с плавающей точкой. Зачем всё это городить? Я хотел декларативного программирования, где всё просто, а тут... На самом деле ответ простой: ребята, если вы не любите цирк, вам там нечего делать, не приходите, но если вы любите цирк...