Кодирование Чёрча: истина, ложь и условия из одних функций

В прошлой статье мы закончили с полным набором правил игры: альфа, бета, эта. У нас есть язык, в котором ровно три конструкции — переменная, абстракция, аппликация — и три преобразования. Красиво, минималистично и совершенно бесполезно на вид. Потому что в этом языке нет ничего: ни чисел, ни строк, ни true, ни false, ни if.

И вот здесь начинается самая интересная часть трека. Оказывается, всё это не нужно добавлять — всё это уже там. Не в смысле «можно приделать сбоку расширение языка», а буквально: истина, ложь, if, &&, || и ! записываются существующими средствами, из одних лямбд, и работают в точности как ожидается. Приём называется кодированием Чёрча (Church encoding), и он же лежит в основе чисел, пар, списков и вообще всех структур данных дальше по треку.

Прежде чем выписывать формулы, стоит задать правильный вопрос. Он звучит не «как записать истину функцией», а гораздо проще.

Зачем булеву значению вообще существовать

Возьмите свой рабочий код и честно ответьте: что вы делаете с булевыми значениями? Не «что они такое», а что вы с ними делаете.

if (isAdmin) { showPanel() } else { showError() }
const label = isActive ? "включено" : "выключено";
const rate = isPremium ? 0.05 : 0.15;

Практически всегда одно и то же: выбираете одну из двух веток. Булево значение — это не «данные», которые вы храните и разглядываете. Это развилка. Единственная его работа — решить, какой из двух вариантов пойдёт дальше.

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

Это и есть вся идея кодирования Чёрча в одном предложении:

Мы не спрашиваем «что такое истина». Мы спрашиваем «что истина делает» — и делаем её этим.

Такой ход в философии называется бихевиористским, а в программировании вы его знаете под именем «полиморфизм вместо switch»: вместо того чтобы снаружи проверять тип объекта и ветвиться, вы вызываете метод, а объект сам знает, что делать. Разница только в том, что здесь у нас нет объектов — только функции.

Истина и ложь

Итак, булево значение принимает два аргумента и возвращает один из них. Вариантов ровно два, и оба записываются в одну строчку:

TRUE  = λx. λy. x
FALSE = λx. λy. y

TRUE — функция двух аргументов (через каррирование, как всегда), которая возвращает первый. FALSE — которая возвращает второй. Всё. Никакого скрытого содержания в этих термах нет: они отличаются одной буквой в теле.

На рабочих языках это выглядит так же дословно:

const TRUE  = x => y => x;
const FALSE = x => y => y;

TRUE("да")("нет");   // "да"
FALSE("да")("нет");  // "нет"

TRUE  = lambda x: lambda y: x
FALSE = lambda x: lambda y: y

TRUE("да")("нет")    # 'да'
FALSE("да")("нет")   # 'нет'

Запустите — оно работает. Это не иллюстрация «примерно как в лямбда-исчислении», это ровно те же термы, записанные синтаксисом JavaScript и Python.

Пара наблюдений, которые пригодятся дальше:

• TRUE — это известный комбинатор K (от немецкого Konstante): функция, которая по значению x возвращает константную функцию, всегда отдающую x. Тот самый const из комбинаторной логики и из Haskell.
• FALSE — это K I, где I = λx. x — тождественная функция. Проверим: K I = (λx. λy. x) (λx. x), бета-редукция по x := λx. x даёт λy. λx. x. Тело игнорирует y и возвращает тождество — а λy. λx. x после альфа-переименования это λx. λy. y… стоп, нет: λy. (λx. x) берёт два аргумента и возвращает второй, потому что внутреннее λx. x применится ко второму аргументу и вернёт его. Эта-эквивалентно FALSE. Разберём аккуратно ниже, в упражнениях.
• FALSE буквально совпадает с числом Чёрча «ноль» (λf. λx. x) с точностью до имён переменных. Это не ошибка кодирования, а следствие бестипового мира: смысл терму придаёт контекст, в котором его применяют. К этому вернёмся в статье про числа Чёрча.

Условный оператор

Теперь if. Определение:

IF = λb. λt. λe. b t e

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

Раскрутим IF TRUE M N полностью, шаг за шагом, без пропусков. Напомню про скобки из статьи о синтаксисе: аппликация левоассоциативна, поэтому IF TRUE M N означает ((IF TRUE) M) N.

    IF TRUE M N

    -- подставляем определение IF
=   ((λb. λt. λe. b t e) TRUE) M N

    -- шаг 1: бета-редукция, b := TRUE
->  (λt. λe. TRUE t e) M N

    -- шаг 2: бета-редукция, t := M
->  (λe. TRUE M e) N

    -- шаг 3: бета-редукция, e := N
->  TRUE M N

    -- подставляем определение TRUE
=   ((λx. λy. x) M) N

    -- шаг 4: бета-редукция, x := M
->  (λy. M) N

    -- шаг 5: бета-редукция, y := N (y в теле не встречается — аргумент отбрасывается)
->  M

Пять шагов, и от всей конструкции остаётся ровно ветка M. Аргумент N отброшен на последнем шаге функцией λy. M, которая своего параметра просто не использует.

То же самое с FALSE:

    IF FALSE M N

=   ((λb. λt. λe. b t e) FALSE) M N

    -- шаг 1: b := FALSE
->  (λt. λe. FALSE t e) M N

    -- шаг 2: t := M
->  (λe. FALSE M e) N

    -- шаг 3: e := N
->  FALSE M N

=   ((λx. λy. y) M) N

    -- шаг 4: x := M (в теле λy. y переменной x нет, M отбрасывается)
->  (λy. y) N

    -- шаг 5: y := N
->  N

Обратите внимание на симметрию: в первом случае отбрасывается N, во втором — M, и происходит это по одной и той же механике — переменная, которой нет в теле, теряет свой аргумент.

IF на самом деле не нужен

Раз IF b t e за три шага сводится к b t e, то и писать IF необязательно — можно сразу применять условие к веткам:

TRUE  M N  ->* M
FALSE M N  ->* N

IF существует только ради читаемости: IF cond then else понятнее, чем cond then else. Ровно как в Smalltalk, где ifTrue:ifFalse: — обычное сообщение объекту-булеву, а не синтаксис языка. Это не совпадение: Smalltalk сделан по той же идее.

const IF = b => t => e => b(t)(e);

IF(TRUE)("панель")("ошибка");   // "панель"
IF(FALSE)("панель")("ошибка");  // "ошибка"

// и без IF — то же самое
TRUE("панель")("ошибка");       // "панель"

IF = lambda b: lambda t: lambda e: b(t)(e)

IF(TRUE)("панель")("ошибка")    # 'панель'
IF(FALSE)("панель")("ошибка")   # 'ошибка'

Ловушка строгих языков: обе ветки вычисляются

Вот здесь код на JavaScript и Python начинает расходиться с чистым лямбда-исчислением, и это важнейший практический нюанс всей статьи.

const boom = () => { throw new Error("сюда не должны были попасть") };
IF(TRUE)("ок")(boom());   // Error!

В настоящем if ветка else не выполняется, если условие истинно. А здесь boom() вычисляется до вызова IF, потому что JavaScript и Python — языки со строгим (аппликативным) порядком вычисления: аргументы считаются раньше, чем передаются в функцию.

В лямбда-исчислении такой проблемы нет, если редуцировать в нормальном порядке — сначала внешний редекс. Тогда IF TRUE M N схлопнется до M, а N вообще никогда не будет тронуто, чем бы оно ни было — хоть бесконечно расходящимся термом (λx. x x) (λx. x x). Именно поэтому «настоящий» IF в чистом исчислении корректен, а его наивный перенос в JS — нет.

Лечится это упаковкой веток в функции без аргументов (thunk-и, «отложенные вычисления»):

// ветки — функции, вызываем только выбранную
const IF_LAZY = b => t => e => b(t)(e)();

IF_LAZY(TRUE)(() => "ок")(() => boom());  // "ок", boom не вызывается

IF_LAZY = lambda b: lambda t: lambda e: b(t)(e)()

def boom():
    raise RuntimeError("сюда не должны были попасть")

IF_LAZY(TRUE)(lambda: "ок")(lambda: boom())   # 'ок'

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

Логические операции

Дальше всё собирается из уже имеющегося. Никаких новых механизмов не понадобится — только применение булевых значений к аргументам.

NOT

Нужно превратить TRUE в FALSE и наоборот. У нас есть значение, которое умеет выбирать из двух. Дадим ему на выбор FALSE и TRUE — именно в таком, перевёрнутом порядке:

NOT = λb. b FALSE TRUE

Раскрутка NOT TRUE:

    NOT TRUE

=   (λb. b FALSE TRUE) TRUE

    -- шаг 1: b := TRUE
->  TRUE FALSE TRUE

=   ((λx. λy. x) FALSE) TRUE

    -- шаг 2: x := FALSE
->  (λy. FALSE) TRUE

    -- шаг 3: y := TRUE, отбрасывается
->  FALSE

Раскрутка NOT FALSE:

    NOT FALSE

=   (λb. b FALSE TRUE) FALSE

    -- шаг 1: b := FALSE
->  FALSE FALSE TRUE

=   ((λx. λy. y) FALSE) TRUE

    -- шаг 2: x := FALSE, отбрасывается
->  (λy. y) TRUE

    -- шаг 3: y := TRUE
->  TRUE

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

AND

Первая идея — через IF: «если p, то результат — q, иначе FALSE».

AND = λp. λq. p q FALSE

Работает, но можно короче. Заметьте: в ветке «иначе» мы возвращаем FALSE, а мы туда попадаем только когда p и есть FALSE. Значит, вместо константы можно вернуть само p:

AND = λp. λq. p q p

Красивая экономия: терм не упоминает TRUE и FALSE вообще. Раскрутим все четыре случая — коротко, но полностью.

    AND TRUE FALSE

=   ((λp. λq. p q p) TRUE) FALSE

    -- шаг 1: p := TRUE
->  (λq. TRUE q TRUE) FALSE

    -- шаг 2: q := FALSE
->  TRUE FALSE TRUE

=   ((λx. λy. x) FALSE) TRUE

    -- шаг 3: x := FALSE
->  (λy. FALSE) TRUE

    -- шаг 4: y := TRUE, отбрасывается
->  FALSE

    AND TRUE TRUE

->  (λq. TRUE q TRUE) TRUE        -- p := TRUE
->  TRUE TRUE TRUE                -- q := TRUE
=   ((λx. λy. x) TRUE) TRUE
->  (λy. TRUE) TRUE               -- x := TRUE
->  TRUE                          -- y отбрасывается

    AND FALSE TRUE

->  (λq. FALSE q FALSE) TRUE      -- p := FALSE
->  FALSE TRUE FALSE              -- q := TRUE
=   ((λx. λy. y) TRUE) FALSE
->  (λy. y) FALSE                 -- x := TRUE, отбрасывается
->  FALSE                         -- y := FALSE

    AND FALSE FALSE

->  (λq. FALSE q FALSE) FALSE     -- p := FALSE
->  FALSE FALSE FALSE             -- q := FALSE
=   ((λx. λy. y) FALSE) FALSE
->  (λy. y) FALSE                 -- x отбрасывается
->  FALSE                         -- y := FALSE

Таблица истинности воспроизведена целиком. Заодно видно, откуда берётся короткое замыкание &&: если p = FALSE, то q в результат не попадает вообще — при нормальном порядке редукции его никто не станет вычислять. Это не оптимизация, приделанная сверху, а прямое следствие определения.

OR

Симметрично: «если p, то TRUE, иначе q», и то же сокращение — вместо TRUE подставляем p, ведь мы туда попадаем только когда p истинно.

OR = λp. λq. p p q

    OR FALSE TRUE

=   ((λp. λq. p p q) FALSE) TRUE

    -- шаг 1: p := FALSE
->  (λq. FALSE FALSE q) TRUE

    -- шаг 2: q := TRUE
->  FALSE FALSE TRUE

=   ((λx. λy. y) FALSE) TRUE

    -- шаг 3: x := FALSE, отбрасывается
->  (λy. y) TRUE

    -- шаг 4: y := TRUE
->  TRUE

XOR и NAND

XOR  = λp. λq. p (NOT q) q
NAND = λp. λq. p (NOT q) TRUE

XOR читается прямо: «если p, то результат — отрицание q; иначе — само q». Проверим один случай целиком, с раскрытием NOT:

    XOR TRUE TRUE

=   ((λp. λq. p (NOT q) q) TRUE) TRUE

    -- шаг 1: p := TRUE
->  (λq. TRUE (NOT q) q) TRUE

    -- шаг 2: q := TRUE
->  TRUE (NOT TRUE) TRUE

=   ((λx. λy. x) (NOT TRUE)) TRUE

    -- шаг 3: x := NOT TRUE
->  (λy. NOT TRUE) TRUE

    -- шаг 4: y отбрасывается
->  NOT TRUE

    -- дальше — уже разобранная выше цепочка
->  TRUE FALSE TRUE
->  (λy. FALSE) TRUE
->  FALSE

Полный набор в коде:

const NOT  = b => b(FALSE)(TRUE);
const AND  = p => q => p(q)(p);
const OR   = p => q => p(p)(q);
const XOR  = p => q => p(NOT(q))(q);
const NAND = p => q => p(NOT(q))(TRUE);

// декодер, чтобы видеть результат человеческими глазами
const show = b => b(true)(false);

show(AND(TRUE)(FALSE));        // false
show(OR(FALSE)(TRUE));         // true
show(XOR(TRUE)(TRUE));         // false
show(NOT(NAND(TRUE)(TRUE)));   // true

NOT  = lambda b: b(FALSE)(TRUE)
AND  = lambda p: lambda q: p(q)(p)
OR   = lambda p: lambda q: p(p)(q)
XOR  = lambda p: lambda q: p(NOT(q))(q)
NAND = lambda p: lambda q: p(NOT(q))(TRUE)

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

show(AND(TRUE)(FALSE))         # False
show(OR(FALSE)(TRUE))          # True
show(XOR(TRUE)(TRUE))          # False
show(NOT(NAND(TRUE)(TRUE)))    # True

Функция show здесь принципиальна для понимания. Сам по себе терм AND TRUE FALSE — это функция; напечатать её нельзя, console.log покажет [Function]. Чтобы «увидеть» булево значение, нужно его применить: дать ему настоящие true и false и посмотреть, что оно выберет. Кодирование Чёрча всегда работает так: значение опознаётся не по виду, а по поведению при применении.

Почему это не игрушка

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

Три ответа, от практического к теоретическому.

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

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

Пары и списки тоже стоят на этом: FST = λp. p TRUE, SND = λp. p FALSE, а признак «список пуст» — обычный булев Чёрча. Всё это разбирается в статьях про числа и пары и списки.

Во-вторых, это работающий инженерный приём. Замена данных функциями, которые их потребляют — это то, что в ООП называют паттерном «Посетитель», а в функциональных языках — final tagless / church-encoded ADT. Идея одна: вместо того чтобы разбирать структуру снаружи через switch, структура сама вызывает нужный обработчик. У приёма есть реальные плюсы: невозможно забыть ветку (типизация не даст), легко добавить новую интерпретацию одного и того же значения, не нужен pattern matching в языке, где его нет. Ровно так устроен Either/Maybe в кодировке Чёрча:

// Maybe в кодировке Чёрча: значение само знает, как себя разобрать
const Nothing  = onNothing => onJust => onNothing;
const Just = v => onNothing => onJust => onJust(v);

const describe = m => m("пусто")(v => `значение ${v}`);

describe(Nothing);   // "пусто"
describe(Just(42));  // "значение 42"

Заметьте: Nothing — это буквально TRUE (берёт первый из двух), а Just — обобщённый FALSE, который ещё и протаскивает полезную нагрузку. Одна и та же идея.

В-третьих, это доказательство вычислительной полноты. Тезис Чёрча-Тьюринга утверждает, что лямбда-исчисление способно выразить любое вычислимое; чтобы это показать, нужно уметь строить из лямбд весь привычный инструментарий — начиная с логики. Булевы значения — первый камень этой конструкции. Формальную сторону вопроса (что такое вычислимость, почему все модели совпадают) хорошо разбирает трек математики, статья про логику и доказательства.

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

Путать порядок аргументов. NOT = λb. b FALSE TRUE, а не λb. b TRUE FALSE. Второй вариант — это тождественная функция на булевых: TRUE TRUE FALSE -> TRUE, FALSE TRUE FALSE -> FALSE. Полезная штука (её иногда называют TO_BOOL или просто id), но не отрицание. Проверяйте себя перебором обоих случаев — это занимает тридцать секунд.

Считать, что редукция «очевидна». Самая частая ошибка новичка — прыгнуть через два шага и подставить не туда. Особенно легко ошибиться, когда терм применяется к самому себе или когда имена переменных совпадают. Если сомневаетесь — выписывайте каждую бета-редукцию отдельной строкой с пометкой, какая переменная на что заменяется. И помните про захват имён: при подстановке терма со свободными переменными внутрь абстракции может понадобиться альфа-переименование.

Забывать про ленивость при переносе в код. Уже разбирали: в JS и Python обе ветки вычисляются до вызова. Если в ветке есть побочный эффект, деление на ноль или рекурсивный вызов — вы получите либо ошибку, либо бесконечный цикл там, где чистое исчисление спокойно даёт ответ. Особенно больно это ударит в статье про рекурсию и комбинатор Y, где без thunk-ов вообще ничего не заведётся.

Ожидать, что тип защитит. В бестиповом исчислении TRUE можно применить к чему угодно, включая число или список, и получить бессмыслицу без всякой ошибки: AND TRUE 5 спокойно отредуцируется во что-то. Дисциплину наводит типизированное лямбда-исчисление — но ценой выразительности.

Печатать значение вместо применения. console.log(AND(TRUE)(TRUE)) покажет [Function (anonymous)]. Чтобы увидеть смысл — примените к двум маркерам, как в show.

Упражнения

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

1. NOT (NOT FALSE)

    NOT (NOT FALSE)
=   (λb. b FALSE TRUE) ((λb. b FALSE TRUE) FALSE)

    -- редуцируем внутренний терм (нормальный порядок дал бы внешний,
    -- но результат тот же — исчисление конфлюэнтно)
->  (λb. b FALSE TRUE) (FALSE FALSE TRUE)      -- b := FALSE внутри
->  (λb. b FALSE TRUE) ((λy. y) TRUE)          -- x := FALSE, отброшен
->  (λb. b FALSE TRUE) TRUE                    -- y := TRUE
->  TRUE FALSE TRUE                            -- b := TRUE
->  (λy. FALSE) TRUE                           -- x := FALSE
->  FALSE

2. AND (OR FALSE TRUE) TRUE

    OR FALSE TRUE
->  (λq. FALSE FALSE q) TRUE     -- p := FALSE
->  FALSE FALSE TRUE             -- q := TRUE
->  (λy. y) TRUE                 -- x := FALSE, отброшен
->  TRUE                         -- y := TRUE

    AND TRUE TRUE
->  (λq. TRUE q TRUE) TRUE       -- p := TRUE
->  TRUE TRUE TRUE               -- q := TRUE
->  (λy. TRUE) TRUE              -- x := TRUE
->  TRUE                         -- y отброшен

3. Чему равно TRUE TRUE FALSE? А FALSE TRUE FALSE?

    TRUE TRUE FALSE
=   ((λx. λy. x) TRUE) FALSE
->  (λy. TRUE) FALSE
->  TRUE

    FALSE TRUE FALSE
=   ((λx. λy. y) TRUE) FALSE
->  (λy. y) FALSE
->  FALSE

4. Покажите, что AND p FALSE даёт FALSE для обоих значений p.

5. Определите XOR без использования NOT.

XOR = λp. λq. p (q FALSE TRUE) q

->  (λq. FALSE (q FALSE TRUE) q) TRUE     -- p := FALSE
->  FALSE (TRUE FALSE TRUE) TRUE          -- q := TRUE
->  (λy. y) TRUE                          -- x := (TRUE FALSE TRUE), отброшен
->  TRUE

6. Терм K I, где K = λx. λy. x и I = λx. x, — это FALSE?

    K I
=   (λx. λy. x) (λz. z)          -- альфа-переименовали I, чтобы не путаться
->  λy. λz. z                    -- x := λz. z

7. Что вернёт IF (ISZERO ZERO) A B, если ISZERO = λn. n (λx. FALSE) TRUE, а ZERO = λf. λx. x?

    ISZERO ZERO
=   (λn. n (λx. FALSE) TRUE) (λf. λx. x)
->  (λf. λx. x) (λx. FALSE) TRUE      -- n := ZERO
->  (λx. x) TRUE                      -- f := (λx. FALSE), отброшен
->  TRUE                              -- x := TRUE

8. Почему IF_LAZY из раздела про ленивость требует, чтобы обе ветки были функциями, а не только «опасная»?

Что читать дальше по теме

• Alonzo Church, «An Unsolvable Problem of Elementary Number Theory» (1936) — оригинальная работа, где кодирование появилось: https://www.jstor.org/stable/2371045
• Peter Selinger, «Lecture Notes on the Lambda Calculus», раздел о представлении данных: https://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf
• Raúl Rojas, «A Tutorial Introduction to the Lambda Calculus» — двадцать страниц, половина из них про булевы значения и числа: https://arxiv.org/abs/1503.09060
• Стэнфордская энциклопедия философии, The Lambda Calculus: https://plato.stanford.edu/entries/lambda-calculus/
• Практическая сторона идеи «данные как функции» — Функции высшего порядка в треке функционального программирования.

Мини-итог

• Булево значение — это не данные, а выбор из двух. Поэтому его и кодируют функцией двух аргументов: TRUE = λx. λy. x, FALSE = λx. λy. y.
• TRUE — комбинатор K, FALSE — K I (и заодно альфа-копия числа Чёрча «ноль»). Смысл терму придаёт контекст применения, а не его вид.
• IF = λb. λt. λe. b t e — синтаксический сахар: b t e работает и без него, потому что вся логика ветвления живёт внутри самого булева значения.
• Логика собирается тривиально: NOT = λb. b FALSE TRUE, AND = λp. λq. p q p, OR = λp. λq. p p q, XOR = λp. λq. p (NOT q) q.
• Короткое замыкание && и || — не оптимизация компилятора, а прямое следствие того, что при нормальном порядке неиспользованный аргумент никогда не редуцируется.
• В JS и Python эти определения работают буквально, но требуют thunk-ов: строгий порядок вычисления посчитает обе ветки до вызова.
• Чтобы «увидеть» чёрчевский булев, его надо применить к двум маркерам — напечатать нельзя, это функция.
• Доказательство свойств в бестиповом исчислении = перебор обоих значений с полной раскруткой редукций. Их всего два, это быстро.

Логика есть. Ветвление есть. Не хватает главного, ради чего вообще затевалось лямбда-исчисление — арифметики. И трюк там ровно тот же: спросить не «что такое число три», а «что число три делает».

Что дальше

Числа Чёрча: арифметика без чисел — увидим, что число это «повторить действие n раз», построим сложение, умножение и возведение в степень, а заодно поймём, почему вычитание оказалось на порядок сложнее сложения.