Кодирование Чёрча

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

По распространённой легенде Стивен Клини придумал функцию-предшественник ($\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))$ — он сдвигает пару: роняет первую компоненту и наращивает вторую:

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

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

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

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

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

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

Тот же приём в 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         (свернули в сумму)

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