Числа Чёрча: арифметика без чисел

В прошлой статье мы выяснили, что истина и ложь — это функции выбора. Теперь вопрос посерьёзнее: а числа?

В лямбда-исчислении нет литерала 2. Нет типа int, нет цифр, нет +. Есть только переменные, λ и вызов. И тем не менее написать 2 + 3 = 5 в нём можно — и результат будет настоящим числом, а не подделкой. Как?

Ответ начинается с простого наблюдения. Спросите себя: что такое «три» в вашем коде? Чаще всего — не «значение 3», а «сделай что-то три раза»:

for (let i = 0; i < 3; i++) step();

Число здесь — не данные, а счётчик повторений. Чёрч в 1930-х развернул эту мысль до предела: если число в первую очередь означает «столько-то раз», то давайте так его и определим. Число n — это функция, которая берёт действие f и стартовое значение x и применяет f к x ровно n раз.

Никаких цифр не нужно. Нужна только способность повторять.

Определение: число — это счётчик повторений

ZERO  = λf.λx. x                -- ноль применений
ONE   = λf.λx. f x              -- одно применение
TWO   = λf.λx. f (f x)          -- два
THREE = λf.λx. f (f (f x))      -- три
FOUR  = λf.λx. f (f (f (f x)))  -- четыре

Общее правило: числу n соответствует терм λf.λx. f^n x, где f^n x — это f, применённая к x ровно n раз.

Обратите внимание на две вещи.

Во-первых, ноль — это функция, которая игнорирует f. Она просто возвращает x. Это в точности та же структура, что у FALSE = λx.λy. y из статьи про булевы значения: «взять второй аргумент, первый выбросить». ZERO и FALSE — синтаксически один и тот же терм. Это не ошибка кодирования, а следствие того, что в чистом лямбда-исчислении нет типов: смысл терму придаёт только то, как вы его используете. К вопросу «а можно ли запретить путать ноль с ложью» вернёмся в статье про типизированное лямбда-исчисление.

Во-вторых, число само по себе ничего не считает. Оно ждёт, пока ему дадут f и x. TWO — это не «двойка», а «двоение»: рецепт удвоенного применения чего угодно к чему угодно.

Тот же код на JavaScript и Python

Здесь важно не поверить на слово, а потрогать руками. Числа Чёрча — обычные стрелочные функции, они запускаются в любом браузере:

const ZERO  = f => x => x;
const ONE   = f => x => f(x);
const TWO   = f => x => f(f(x));
const THREE = f => x => f(f(f(x)));

// «Декодер»: подставляем в качестве f прибавление единицы, в качестве x — обычный 0
const toInt = n => n(k => k + 1)(0);

console.log(toInt(THREE)); // 3

ZERO  = lambda f: lambda x: x
ONE   = lambda f: lambda x: f(x)
TWO   = lambda f: lambda x: f(f(x))
THREE = lambda f: lambda x: f(f(f(x)))

to_int = lambda n: n(lambda k: k + 1)(0)

print(to_int(THREE))  # 3

Функция toInt — не часть лямбда-исчисления, а мостик наружу: она вытаскивает число Чёрча в мир, где числа уже есть. Внутри самого исчисления никакого «настоящего 3» не существует и не требуется.

Подставлять можно что угодно, не только +1:

toInt(THREE);                       // 3
THREE(s => s + "!")("ого");         // "ого!!!"
THREE(a => [...a, 0])([]);          // [0, 0, 0]

to_int(THREE)                        # 3
THREE(lambda s: s + "!")("ого")      # "ого!!!"
THREE(lambda a: a + [0])([])         # [0, 0, 0]

Число Чёрча — это свёрнутый цикл for, вынесенный в значение. Именно поэтому конструкция такая полезная: n f x — это одновременно «число n», «повторить n раз» и «свёртка списка из n элементов».

SUCC: следующее число

Первая операция — прибавление единицы. Хотим функцию SUCC, которая по n даёт n + 1.

Рассуждаем от смысла. n f x — это «f, применённая n раз к x». Чтобы получить n + 1 применений, нужно применить f ещё разок снаружи: f (n f x). Осталось обернуть это обратно в абстракцию по f и x и по самому n:

SUCC = λn.λf.λx. f (n f x)

Проверим на ONE, разворачивая каждый шаг. Сначала выпишем участников с переименованными связанными переменными (это альфа-преобразование, оно ничего не меняет, но избавляет от путаницы имён):

SUCC = λn.λf.λx. f (n f x)
ONE  = λg.λy. g y

Шаг 1 — подставляем ONE вместо n:

SUCC ONE
= (λn.λf.λx. f (n f x)) (λg.λy. g y)
→β λf.λx. f ((λg.λy. g y) f x)

Шаг 2 — внутренний редекс (λg.λy. g y) f, подставляем f вместо g:

→β λf.λx. f ((λy. f y) x)

Шаг 3 — редекс (λy. f y) x, подставляем x вместо y:

→β λf.λx. f (f x)

Это ровно TWO. Нормальная форма достигнута — редексов больше нет.

Ещё раз, на TWO, чтобы закрепить:

SUCC TWO
= (λn.λf.λx. f (n f x)) (λg.λy. g (g y))
→β λf.λx. f ((λg.λy. g (g y)) f x)
→β λf.λx. f ((λy. f (f y)) x)
→β λf.λx. f (f (f x))                       = THREE

const SUCC = n => f => x => f(n(f)(x));

toInt(SUCC(SUCC(SUCC(ZERO)))); // 3

SUCC = lambda n: lambda f: lambda x: f(n(f)(x))

to_int(SUCC(SUCC(SUCC(ZERO))))  # 3

Заметьте: теперь все натуральные числа порождаются из двух термов — ZERO и SUCC. Это буквально аксиомы Пеано, выраженные функциями.

PLUS: сложение

Есть два способа определить сложение, и оба поучительны.

Способ 1 — «применить SUCC m раз к n». Раз m умеет повторять что угодно m раз, пусть повторяет SUCC:

PLUS = λm.λn. m SUCC n

Разворачиваем PLUS TWO THREE:

PLUS TWO THREE
= (λm.λn. m SUCC n) TWO THREE
→β (λn. TWO SUCC n) THREE
→β TWO SUCC THREE
= (λf.λx. f (f x)) SUCC THREE
→β (λx. SUCC (SUCC x)) THREE
→β SUCC (SUCC THREE)
→β* SUCC FOUR
→β* FIVE

Последние два шага мы уже умеем раскручивать полностью — это два применения SUCC, каждое по три бета-шага, как выше.

Способ 2 — «склеить две цепочки». Более прямой и более красивый. Если m f x — это f^m x, то чтобы получить f^(m+n) x, достаточно взять f^n x в качестве стартового значения для m:

PLUS = λm.λn.λf.λx. m f (n f x)

Разворачиваем PLUS TWO ONE целиком. Участники:

TWO = λg.λy. g (g y)
ONE = λh.λz. h z

PLUS TWO ONE
= (λm.λn.λf.λx. m f (n f x)) TWO ONE
→β (λn.λf.λx. TWO f (n f x)) ONE                  -- подставили m := TWO
→β λf.λx. TWO f (ONE f x)                         -- подставили n := ONE

Раскрываем ONE f x:

= λf.λx. TWO f ((λh.λz. h z) f x)
→β λf.λx. TWO f ((λz. f z) x)
→β λf.λx. TWO f (f x)

Раскрываем TWO f:

= λf.λx. (λg.λy. g (g y)) f (f x)
→β λf.λx. (λy. f (f y)) (f x)
→β λf.λx. f (f (f x))                             = THREE

Три плюс… то есть два плюс один равно три. Работает.

const PLUS = m => n => f => x => m(f)(n(f)(x));

toInt(PLUS(TWO)(THREE)); // 5

PLUS = lambda m: lambda n: lambda f: lambda x: m(f)(n(f)(x))

to_int(PLUS(TWO)(THREE))  # 5

MULT: умножение — это композиция

Умножение получается ещё изящнее. m * n — это «повторить n раз, и так m раз». А «повторить n раз» для функции f — это n f. Значит нужно применить m раз функцию n f:

MULT = λm.λn.λf. m (n f)

Ни x, ни SUCC, ни PLUS — только композиция. Разворачиваем MULT TWO THREE:

TWO   = λg.λy. g (g y)
THREE = λh.λz. h (h (h z))

MULT TWO THREE
= (λm.λn.λf. m (n f)) TWO THREE
→β (λn.λf. TWO (n f)) THREE
→β λf. TWO (THREE f)

Раскрываем THREE f:

= λf. TWO ((λh.λz. h (h (h z))) f)
→β λf. TWO (λz. f (f (f z)))

Раскрываем TWO, подставляя g := λz. f (f (f z)):

= λf. (λg.λy. g (g y)) (λz. f (f (f z)))
→β λf.λy. (λz. f (f (f z))) ((λz. f (f (f z))) y)

Внутренний редекс:

→β λf.λy. (λz. f (f (f z))) (f (f (f y)))

Внешний редекс:

→β λf.λy. f (f (f (f (f (f y))))))

Считаем f-ы: шесть. Это SIX. (Имя связанной переменной y вместо x роли не играет — термы альфа-эквивалентны.)

const MULT = m => n => f => m(n(f));

toInt(MULT(TWO)(THREE)); // 6

MULT = lambda m: lambda n: lambda f: m(n(f))

to_int(MULT(TWO)(THREE))  # 6

Есть и «арифметический» вариант через сложение: MULT = λm.λn. m (PLUS n) ZERO — прибавить n к нулю m раз. Он работает, но требует больше редукций.

POW: степень — это просто применение

Здесь происходит фокус, от которого обычно приятно щёлкает в голове:

POW = λm.λn. n m

Всё. Возведение в степень — это аппликация одного числа к другому.

Почему? n означает «повторить n раз». m — это операция «повторить m раз». Значит n m — это «повторить m-кратное повторение n раз», то есть m^n.

Разворачиваем POW TWO THREE (ожидаем 2^3 = 8):

POW TWO THREE
= (λm.λn. n m) TWO THREE
→β (λn. n TWO) THREE
→β THREE TWO
= (λh.λz. h (h (h z))) TWO
→β λz. TWO (TWO (TWO z))

Теперь z — это функция (мы применяем TWO к ней), переименуем в f для читаемости и раскрутим изнутри. Напомню: TWO g даёт λy. g (g y), то есть «g дважды».

TWO f              →β* λy. f (f y)                                  -- f в степени 2
TWO (TWO f)        →β* λy. (f∘f) ((f∘f) y)      = λy. f (f (f (f y)))   -- f в степени 4
TWO (TWO (TWO f))  →β* λy. f^4 (f^4 y)          = λy. f^8 y             -- f в степени 8

Итог: λf.λy. f (f (f (f (f (f (f (f y)))))))) — восемь применений. 2^3 = 8.

const POW = m => n => n(m);

toInt(POW(TWO)(THREE)); // 8

POW = lambda m: lambda n: n(m)

to_int(POW(TWO)(THREE))  # 8

Крайний случай приятно проверить руками: POW m ZERO = ZERO m = λx. x — то есть комбинатор I. А ONE = λf.λx. f x эта-редуцируется в λf. f, то есть тоже I. Значит m^0 = 1 соблюдается — с точностью до эта-преобразования.

PRED: предшественник, на котором всё ломается

Складывать, умножать, возводить в степень оказалось легко. Теперь попробуйте определить PRED n = n - 1.

Не получится «в лоб». Число Чёрча умеет только идти вперёд: оно применяет f заданное количество раз. Никакого способа «сделать на один шаг меньше» в его структуре нет — она односторонняя, как связный список без обратных ссылок.

Задача про предшественника несколько лет стояла открытой в группе Чёрча; он даже подозревал, что арифметика в лямбда-исчислении принципиально неполна. Решение нашёл Стивен Клини — по его собственному рассказу, в кресле стоматолога под закисью азота, когда ему удаляли зуб мудрости (Kleene S.C., «Origins of Recursive Function Theory», Annals of the History of Computing, 1981, doi:10.1109/MAHC.1981.10004).

Идея. Раз назад ходить нельзя, будем идти вперёд, но таскать с собой предыдущее значение. Состояние — пара (a, b), где b — текущий счётчик, а a — предыдущий. Шаг сдвигает пару:

(a, b) → (b, b + 1)

Стартуем с (0, 0) и делаем n шагов. Получаем (n-1, n). Берём левое — вот и предшественник. Для n = 0 шагов не делается вовсе, пара остаётся (0, 0), левое равно нулю: PRED 0 = 0. Отрицательных чисел у нас нет, поэтому такое «упирание в ноль» — стандартное соглашение (его называют усечённым вычитанием, monus).

Нам понадобятся пары. Подробно они в следующей статье, а пока примите на веру три терма:

PAIR = λa.λb.λs. s a b       -- пара «упаковывает» два значения в ожидание селектора
FST  = λp. p (λa.λb. a)      -- скармливаем паре селектор «взять первое»
SND  = λp. p (λa.λb. b)      -- селектор «взять второе»

Селекторы λa.λb. a и λa.λb. b — это TRUE и FALSE из статьи про булевы значения. Пара просто хранит два значения и ждёт, кого из них попросят.

Теперь шаг и сам PRED:

SHIFT = λp. PAIR (SND p) (SUCC (SND p))
PRED  = λn. FST (n SHIFT (PAIR ZERO ZERO))

Читается почти по-русски: «применить SHIFT n раз к паре (0, 0) и взять первый элемент».

Разворачиваем PRED TWO. Чтобы не утонуть в скобках, будем писать пары как (a, b) — это сокращение для PAIR a b, и на каждом шаге показывать, откуда что взялось.

PRED TWO
= (λn. FST (n SHIFT (PAIR ZERO ZERO))) TWO
→β FST (TWO SHIFT (PAIR ZERO ZERO))

Раскрываем TWO SHIFT, то есть (λf.λx. f (f x)) SHIFT:

→β FST ((λx. SHIFT (SHIFT x)) (PAIR ZERO ZERO))
→β FST (SHIFT (SHIFT (0, 0)))

Первый SHIFT:

SHIFT (0, 0)
= (λp. PAIR (SND p) (SUCC (SND p))) (0, 0)
→β PAIR (SND (0, 0)) (SUCC (SND (0, 0)))

Считаем SND (0, 0):

SND (0, 0)
= (λp. p (λa.λb. b)) ((λa.λb.λs. s a b) ZERO ZERO)
→β* (λs. s ZERO ZERO) (λa.λb. b)
→β (λa.λb. b) ZERO ZERO
→β (λb. b) ZERO
→β ZERO

Значит:

SHIFT (0, 0) →β* PAIR ZERO (SUCC ZERO) = (0, 1)

Второй SHIFT — по той же схеме, SND (0, 1) →β* ONE:

SHIFT (0, 1) →β* PAIR ONE (SUCC ONE) = (1, 2)

Осталось взять первое:

FST (1, 2)
= (λp. p (λa.λb. a)) ((λa.λb.λs. s a b) ONE TWO)
→β* (λs. s ONE TWO) (λa.λb. a)
→β (λa.λb. a) ONE TWO
→β (λb. ONE) TWO
→β ONE

PRED TWO = ONE. Работает.

const PAIR  = a => b => s => s(a)(b);
const FST   = p => p(a => b => a);
const SND   = p => p(a => b => b);
const SHIFT = p => PAIR(SND(p))(SUCC(SND(p)));
const PRED  = n => FST(n(SHIFT)(PAIR(ZERO)(ZERO)));

toInt(PRED(THREE)); // 2
toInt(PRED(ZERO));  // 0

PAIR  = lambda a: lambda b: lambda s: s(a)(b)
FST   = lambda p: p(lambda a: lambda b: a)
SND   = lambda p: p(lambda a: lambda b: b)
SHIFT = lambda p: PAIR(SND(p))(SUCC(SND(p)))
PRED  = lambda n: FST(n(SHIFT)(PAIR(ZERO)(ZERO)))

to_int(PRED(THREE))  # 2
to_int(PRED(ZERO))   # 0

Вычитание бесплатно

Раз есть PRED, вычитание получается тем же приёмом «повторить n раз»:

SUB = λm.λn. n PRED m

SUB THREE TWO = TWO PRED THREE = PRED (PRED THREE) = PRED TWO = ONE. А SUB TWO THREE даст PRED (PRED (PRED TWO)) = PRED (PRED ONE) = PRED ZERO = ZERO — усечение в ноль, как договорились.

Предикаты: сравнение чисел

Осталось научиться спрашивать. Ключевой предикат — «это ноль?»:

ISZERO = λn. n (λx. FALSE) TRUE

Логика: даём числу функцию, которая на любой вход отвечает FALSE, и стартовое значение TRUE. Если применений ноль — TRUE останется нетронутым. Если хоть одно — TRUE будет затёрто на FALSE.

Разворачиваем на нуле:

ISZERO ZERO
= (λn. n (λx. FALSE) TRUE) (λf.λy. y)
→β (λf.λy. y) (λx. FALSE) TRUE
→β (λy. y) TRUE
→β TRUE

И на двойке:

ISZERO TWO
= (λn. n (λx. FALSE) TRUE) (λf.λy. f (f y))
→β (λf.λy. f (f y)) (λx. FALSE) TRUE
→β (λy. (λx. FALSE) ((λx. FALSE) y)) TRUE
→β (λx. FALSE) ((λx. FALSE) TRUE)
→β FALSE

На последнем шаге внешняя функция игнорирует аргумент — считать внутренний редекс не потребовалось (это нормальный порядок редукции; при аппликативном порядке пришлось бы сначала свести внутреннее к FALSE, но результат тот же).

Дальше всё строится комбинированием:

LEQ = λm.λn. ISZERO (SUB m n)          -- m <= n, если m - n усеклось в ноль
GEQ = λm.λn. LEQ n m
EQ  = λm.λn. AND (LEQ m n) (LEQ n m)   -- равенство через двойное неравенство
LT  = λm.λn. AND (LEQ m n) (NOT (EQ m n))

где AND = λp.λq. p q p и NOT = λp. p FALSE TRUE — из статьи про булевы значения.

const SUB    = m => n => n(PRED)(m);
const TRUE   = a => b => a;
const FALSE  = a => b => b;
const ISZERO = n => n(_ => FALSE)(TRUE);
const AND    = p => q => p(q)(p);
const LEQ    = m => n => ISZERO(SUB(m)(n));
const EQ     = m => n => AND(LEQ(m)(n))(LEQ(n)(m));

const toBool = b => b(true)(false);

toBool(EQ(TWO)(TWO));                   // true
toBool(EQ(PLUS(ONE)(ONE))(TWO));        // true
toBool(LEQ(THREE)(TWO));                // false

SUB    = lambda m: lambda n: n(PRED)(m)
TRUE   = lambda a: lambda b: a
FALSE  = lambda a: lambda b: b
ISZERO = lambda n: n(lambda _: FALSE)(TRUE)
AND    = lambda p: lambda q: p(q)(p)
LEQ    = lambda m: lambda n: ISZERO(SUB(m)(n))
EQ     = lambda m: lambda n: AND(LEQ(m)(n))(LEQ(n)(m))

to_bool = lambda b: b(True)(False)

to_bool(EQ(TWO)(TWO))              # True
to_bool(LEQ(THREE)(TWO))           # False

Вот вся конструкция целиком — что на чём стоит:

Цена вопроса: почему так делать нельзя

Всё это работает — и всё это чудовищно неэффективно. Разберём честно.

Представление унарное. Терм для числа n содержит n вхождений f, то есть его размер — O(n). Число миллион занимает миллион узлов. Настоящий компьютер хранит его в 20 битах. Разница между унарной и позиционной записью — это разница между O(n) и O(log n), и на больших числах она смертельна.

Стоимость операций перевёрнута относительно привычной.

Обратите внимание на асимметрию: SUCC стоит константу, а PRED — линию. В железе всё наоборот: +1 и -1 — одна инструкция. Числа Чёрча оптимизированы под то, что для них естественно (итерацию), и наказывают за то, что для них противоестественно (движение назад).

Существуют альтернативы. Наиболее известная — числа Скотта, где число несёт не «сколько раз повторить», а «я ноль» либо «я последователь вот этого»:

SCOTT_ZERO = λz.λs. z
SCOTT_SUCC = λn.λz.λs. s n
SCOTT_PRED = λn. n SCOTT_ZERO (λm. m)      -- O(1)!

Здесь PRED — константа по времени, зато итерация («примени f n раз») сама по себе недоступна: её приходится строить рекурсией через комбинатор Y. Это классический размен: кодирование Чёрча делает свёртку дешёвой, кодирование Скотта — разбор случаев. Подробный разбор обоих: Jansen J.M., «Programming in the λ-Calculus: From Church to Scott and Back», 2013, doi:10.1007/978-3-642-40355-2_12.

Ещё существуют бинарные кодирования (число как список бит, где список — тоже лямбда-терм), и в них арифметика асимптотически нормальная. Но они громоздкие, и в учебниках их почти не показывают.

Зачем это знать практикующему разработчику

Соблазн отмахнуться («красиво, но бесполезно») — понятный, но преждевременный. Три реальные причины.

1. Число Чёрча — это fold. Посмотрите на сигнатуру: n берёт «шаг» и «начальное значение». Это в точности reduce / foldr над списком из n одинаковых элементов. И это не совпадение, а частный случай общего рецепта: любой алгебраический тип данных можно закодировать его собственной свёрткой. Формально это кодирование Бёма-Берардуччи (Böhm C., Berarducci A., «Automatic synthesis of typed Λ-programs on term algebras», TCS, 1985, doi:10.1016/0304-3975(85)90135-5). Натуральные числа — тип с двумя конструкторами (Zero, Succ), поэтому число Чёрча принимает ровно два аргумента: по одному на конструктор. Булево значение — два конструктора без полей, поэтому TRUE/FALSE тоже берут два аргумента. Пары и списки в следующей статье будут устроены по тому же шаблону, и, увидев его один раз, вы будете узнавать его в CPS-стиле, в паттерне «посетитель», в тагless-final интерпретаторах и в церковно-закодированных Maybe/Either.

2. Это работающий тест на понимание замыканий. Если код выше кажется вам магией, значит, есть, что подтянуть в каррировании и захвате переменных. Если понятен — вы уже владеете фундаментом функционального программирования. Практическая сторона разбирается в треке функциональное программирование.

3. Это половина доказательства тезиса Чёрча-Тьюринга. Чтобы утверждать, что лямбда-исчисление вычисляет всё вычислимое, нужно сначала показать, что в нём есть натуральные числа и базовые рекурсивные функции. Числа Чёрча — этот шаг. Оригинальная работа: Church A., «An Unsolvable Problem of Elementary Number Theory», American Journal of Mathematics, 1936, doi:10.2307/2371045. Тему вычислимости продолжает трек математика.

Кстати, в типизированном виде число Чёрча получает тип Nat = ∀X. (X → X) → X → X — и это ровно та же формула, что и «принцип индукции» в логике. Об этом совпадении — статья про соответствие Карри-Ховарда.

Типичные ошибки

Путать n f x и n (f x). Аппликация левоассоциативна: n f x — это (n f) x, «сначала дать числу шаг, потом стартовое значение». n (f x) — совсем другое: вы даёте числу уже вычисленный результат в качестве шага. Правило скобок разбиралось в статье про нотацию.

Ждать, что PLUS TWO THREE само превратится в FIVE. В лямбда-исчислении нет вычислителя, который «упростит выражение». Есть только бета-редукция, и её надо применять до нормальной формы. PLUS TWO THREE и FIVE — разные термы, которые бета-эквивалентны. В JS/Python аналогично: PLUS(TWO)(THREE) — это замыкание, и пока вы не скормите ему f и x (через toInt), увидите только [Function].

Забывать переименовать связанные переменные. Если в PLUS = λm.λn.λf.λx. m f (n f x) подставить терм, у которого свои f и x, и не выполнить альфа-преобразование, произойдёт захват имён — и результат окажется бессмыслицей. В коде на JS и Python об этом заботится сам язык (замыкания корректны по построению), а вот когда редуцируете на бумаге — легко ошибиться.

Считать, что ZERO и FALSE — «одно и то же по ошибке». Они действительно один терм. Это фича бестипового исчисления, а не баг; типы появятся позже и разведут их.

Гонять большие числа в JavaScript. toInt(POW(TWO)(TWO)) посчитается мгновенно, а POW(TEN)(TEN) съест стек: рекурсия в toInt идёт на 10^10 уровней. В Python лимит рекурсии остановит вас ещё раньше. Это не недостаток теории, а прямое следствие унарности.

Упражнения

Сведите к нормальной форме и назовите результат. Ответы ниже — сначала попробуйте сами, с полной раскруткой шагов.

1. SUCC ZERO
2. PLUS ONE ONE (используйте определение PLUS = λm.λn.λf.λx. m f (n f x))
3. MULT ZERO TWO
4. POW ONE THREE
5. ISZERO (PRED ONE)
6. Определите DOUBLE (удвоение) двумя способами: через MULT и напрямую, не используя MULT.

Ответы

1. SUCC ZERO

= (λn.λf.λx. f (n f x)) (λg.λy. y)
→β λf.λx. f ((λg.λy. y) f x)
→β λf.λx. f ((λy. y) x)
→β λf.λx. f x                        = ONE

2. PLUS ONE ONE

ONE = λg.λy. g y

= (λm.λn.λf.λx. m f (n f x)) ONE ONE
→β (λn.λf.λx. ONE f (n f x)) ONE
→β λf.λx. ONE f (ONE f x)
= λf.λx. ONE f ((λg.λy. g y) f x)
→β λf.λx. ONE f ((λy. f y) x)
→β λf.λx. ONE f (f x)
= λf.λx. (λg.λy. g y) f (f x)
→β λf.λx. (λy. f y) (f x)
→β λf.λx. f (f x)                    = TWO

3. MULT ZERO TWO

= (λm.λn.λf. m (n f)) ZERO TWO
→β (λn.λf. ZERO (n f)) TWO
→β λf. ZERO (TWO f)
= λf. (λg.λx. x) (TWO f)
→β λf.λx. x                          = ZERO

Ноль игнорирует свой первый аргумент, поэтому TWO f даже не считается. Умножение на ноль — это буквально «выбросить множитель, не глядя».

4. POW ONE THREE (ожидаем 1^3 = 1)

= (λm.λn. n m) ONE THREE
→β (λn. n ONE) THREE
→β THREE ONE
= (λh.λz. h (h (h z))) ONE
→β λz. ONE (ONE (ONE z))

Раскручиваем изнутри, помня ONE = λg.λy. g y:

ONE z              →β λy. z y
ONE (λy. z y)      = (λg.λy'. g y') (λy. z y)
                   →β λy'. (λy. z y) y'
                   →β λy'. z y'
ONE (λy'. z y')    →β* λy''. z y''

Итог: λz.λy. z y — это ONE. Заметьте, как выражение «стоит на месте»: применение единицы ничего не меняет, что и должно быть.

5. ISZERO (PRED ONE)

PRED ONE = FST (ONE SHIFT (PAIR ZERO ZERO))
         →β FST (SHIFT (0, 0))
         →β* FST (0, 1)
         →β* ZERO

ISZERO ZERO →β* TRUE            (полная раскрутка — в разделе про предикаты)

Ответ: TRUE. Предшественник единицы — ноль, и ISZERO это подтверждает.

6. DOUBLE

Через умножение:

DOUBLE = λn. MULT TWO n

Напрямую — «применить f дважды на каждом шаге», то есть подсунуть числу не f, а f∘f:

DOUBLE = λn.λf.λx. n (λy. f (f y)) x

Или короче, с эта-редукцией: DOUBLE = λn.λf. n (λy. f (f y)).

Проверка на TWO:

DOUBLE TWO
= (λn.λf.λx. n (λy. f (f y)) x) (λg.λz. g (g z))
→β λf.λx. (λg.λz. g (g z)) (λy. f (f y)) x
→β λf.λx. (λz. (λy. f (f y)) ((λy. f (f y)) z)) x
→β λf.λx. (λy. f (f y)) ((λy. f (f y)) x)
→β λf.λx. (λy. f (f y)) (f (f x))
→β λf.λx. f (f (f (f x)))            = FOUR

const DOUBLE = n => f => x => n(y => f(f(y)))(x);
toInt(DOUBLE(THREE)); // 6

Итог

• Число Чёрча — это функция «повтори f ровно n раз»: n = λf.λx. f^n x. Не значение, а свёрнутый цикл.
• SUCC оборачивает лишним применением, PLUS склеивает цепочки, MULT — это композиция, POW — просто аппликация числа к числу. Всё без единой цифры.
• PRED требует хитрости: идти вперёд, таща за собой пару (предыдущее, текущее), и в конце взять левое. Отсюда SUB и все сравнения.
• ZERO и FALSE — один и тот же терм; в бестиповом исчислении смысл задаётся использованием, а не формой.
• Практическая цена — унарность: размер O(n), PRED за O(n). Числа Чёрча доказывают, что арифметика выразима, а не предлагают на них считать.
• Общий шаблон, который стоит унести: тип данных = его собственная свёртка. Он повторится для пар, списков, деревьев и опциональных значений.

Полезное чтение: Pierce B.C., «Types and Programming Languages», глава 5 — cis.upenn.edu/~bcpierce/tapl; Barendregt H.P., «The Lambda Calculus: Its Syntax and Semantics» — исчерпывающая справка; обзорная статья Church encoding в Wikipedia — удобная шпаргалка по всем термам разом.

Что дальше

Мы уже подсмотрели PAIR, FST и SND, когда собирали PRED, — но там они были инструментом, а не темой. Пора разобрать их всерьёз и увидеть, как из двухэлементной пары вырастают списки, деревья и вообще любые структуры данных, по-прежнему без единого типа и без единого литерала.

Пары, списки и структуры данных из одних лямбд