Лямбда-исчисление Чёрча: зачем оно программисту и что это вообще такое

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

Звучит как шутка или как соревнование «кто напишет самый бесполезный язык». Но это не шутка: на таком языке можно вычислить всё, что вычислимо на вашем ноутбуке, на суперкомпьютере и на любой машине, которую вообще можно построить. Именно это доказал Алонзо Чёрч в 1936 году — за десять лет до появления первого электронного компьютера.

Этот язык называется лямбда-исчисление. И вы им уже пользуетесь: каждый раз, когда пишете arr.map(x => x * 2) или sorted(xs, key=lambda p: p.age), вы пишете лямбда-термы. Просто с сахаром, числами и стандартной библиотекой сверху.

Зачем это программисту, а не только математику

Честный ответ: чтобы читать основание, на котором стоит половина инструментов, которыми вы пользуетесь. Конкретно:

Замыкания и каррирование перестают быть магией. Почему f(a)(b) работает и почему функция «помнит» переменную из внешней области видимости — это ровно бета-редукция.
Функциональные языки становятся читаемыми. Haskell, OCaml, Elm, Elixir, Clojure — все строятся поверх этой модели. GHC буквально компилирует Haskell в промежуточный язык Core, который есть типизированное лямбда-исчисление с десятком расширений.
Система типов перестаёт быть набором заклинаний. Generics, Option<T>, вывод типов Хиндли-Милнера, «почему TypeScript не может это вывести» — всё это про типизированное лямбда-исчисление (см. https://courses.digitable.life/post/lambda-calculus/09-typed-lambda/).
Понятие «вычислимо» получает точный смысл. Почему задача останова неразрешима, почему не бывает универсального анализатора кода без ложных срабатываний — это тезис Чёрча-Тьюринга.
Компиляторы и интерпретаторы. CPS-преобразование, инлайнинг, ленивые вычисления, оптимизация хвостовых вызовов — все эти техники описываются как преобразования лямбда-термов.

Плюс побочный эффект: после лямбда-исчисления код на любом языке начинаешь читать как выражения, а не как последовательность команд. Это ощутимо меняет то, как вы проектируете API.

Идея на одной аналогии

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

Деталь — функция. Единственная операция — «применить функцию к аргументу». Всё остальное (числа, логика, списки, циклы, рекурсия) не встроено, а закодировано через функции. Как в электронике: у вас есть только элемент NAND, а из него вы собираете весь процессор.

Три конструкции — и это весь язык

Синтаксис лямбда-исчисления помещается в три строки. Терм — это одно из:

терм ::= x                 (1) переменная
       | λx. терм          (2) абстракция  — определение функции
       | (терм терм)       (3) аппликация  — вызов функции

Разберём:

Переменная x — просто имя. Никакого значения за ним не стоит, это чистый символ.
Абстракция λx. M — функция с параметром x и телом M. Читается: «функция, которая берёт x и возвращает M». На JS это x => M, на Python — lambda x: M.
Аппликация M N — применить M к N. На JS и Python это M(N).

Анатомия лямбда-выражения

Два соглашения о скобках, которые надо запомнить сразу, иначе выражения будут выглядеть как шум:

Аппликация левоассоциативна: f a b c означает (((f a) b) c), а не f (a (b c)).
Тело абстракции тянется вправо до упора: λx. x y — это λx. (x y), а не (λx. x) y.

Подробный разбор нотации со всеми ловушками — в следующей статье трека, https://courses.digitable.life/post/lambda-calculus/01-syntax/.

Три термина, которые встретятся везде

I = λx. x            — тождество: возвращает свой аргумент
K = λx. λy. x        — «константа»: берёт два аргумента, возвращает первый
S = λf. λg. λx. f x (g x)   — «распределитель»

Первые два выглядят бессмысленно. На практике K — это функция const из lodash и Function.constant из любой функциональной библиотеки, а I — identity. А комбинации S и K достаточно, чтобы выразить любой лямбда-терм вообще без переменных (это называется SKI-исчисление комбинаторов).

Один и тот же терм на трёх языках

// I = λx. x
const I = x => x;

// K = λx. λy. x
const K = x => y => x;

// S = λf. λg. λx. f x (g x)
const S = f => g => x => f(x)(g(x));

console.log(S(K)(K)(42)); // 42 — SKK ведёт себя как I

# I = λx. x
I = lambda x: x

# K = λx. λy. x
K = lambda x: lambda y: x

# S = λf. λg. λx. f x (g x)
S = lambda f: lambda g: lambda x: f(x)(g(x))

print(S(K)(K)(42))  # 42 — SKK ведёт себя как I

Обратите внимание: в лямбда-исчислении все функции одноаргументные. Функции двух аргументов не существует — есть функция, которая возвращает функцию. Это и есть каррирование, и в JS/Python оно записывается ровно так же: x => y => .... Если вы когда-нибудь писали connect(mapState)(Component) в Redux — вы применяли каррированную функцию.

Вычисление: бета-редукция

Единственное правило вычисления называется бета-редукцией. Формулируется так:

(λx. M) N   →β   M[x := N]

«Применили функцию λx. M к аргументу N — значит, в теле M заменяем каждое вхождение x на N и выбрасываем саму лямбду». Ровно то, что делает интерпретатор при вызове функции.

Шаг бета-редукции

Разберём полностью, шаг за шагом, без «очевидно, получаем». Терм:

(λx. λy. x) a b

Шаг 0. Расставим скобки по правилу левоассоциативности:

((λx. λy. x) a) b

Шаг 1. Редекс (то, что можно редуцировать) — внутренняя пара (λx. λy. x) a. Здесь M = λy. x, N = a, подставляем x := a в тело:

(λy. a) b

Шаг 2. Снова редекс: M = a, N = b, подставляем y := b. Но y в теле a не встречается, поэтому тело остаётся как есть:

Шаг 3. Редексов больше нет. Терм в нормальной форме. Ответ: a.

Тот же расчёт в коде — можно запустить и убедиться:

const K = x => y => x;
K("a")("b"); // "a"

K = lambda x: lambda y: x
K("a")("b")  # 'a'

Ещё один разбор, чуть длиннее — здесь важно не потерять ни одного шага:

(λf. λx. f (f x)) (λn. n) q

Шаг 1. Внешний редекс: подставляем f := (λn. n)
        → (λx. (λn. n) ((λn. n) x)) q

Шаг 2. Редекс: подставляем x := q
        → (λn. n) ((λn. n) q)

Шаг 3. Редуцируем внутренний вызов: (λn. n) q → q
        → (λn. n) q

Шаг 4. Ещё раз: (λn. n) q → q
        → q

Нормальная форма — q. Функция λf. λx. f (f x) применила f дважды; так как f оказалась тождеством, дважды применённое тождество тоже тождество. Забегая вперёд: это число 2 в кодировке Чёрча (см. https://courses.digitable.life/post/lambda-calculus/05-numerals/).

flowchart TD A["Терм"] --> B{"Есть редекс вида
(λx. M) N ?"} B -- "нет" --> C["Нормальная форма
вычисление окончено"] B -- "да" --> D["Выбрать редекс
по стратегии вычисления"] D --> E["Проверить захват имён
при необходимости α-переименовать"] E --> F["Подставить: M[x := N]"] F --> A B -- "редекс всегда есть" --> G["Расходимость
вычисление не завершается"]

Ветка «расходимость» — не теоретическая экзотика. Вот терм, который редуцируется сам в себя:

Ω = (λx. x x) (λx. x x)

Шаг 1. Подставляем x := (λx. x x) в тело (x x):
        → (λx. x x) (λx. x x)

Шаг 2. Ровно то же самое. И так бесконечно.

Это лямбда-исчисленческий эквивалент while (true) {}. Его существование — не баг, а признак полноты по Тьюрингу: язык, в котором любая программа гарантированно завершается, заведомо не может выразить все вычислимые функции.

Где числа, булевы значения и списки?

Их нет. Совсем. Их кодируют функциями — и это самая красивая часть теории.

Булевы значения по Чёрчу — это функции выбора из двух вариантов:

TRUE  = λt. λf. t      — берёт две ветки, возвращает первую
FALSE = λt. λf. f      — берёт две ветки, возвращает вторую
IF    = λb. λt. λf. b t f

Проверим IF TRUE a b полностью:

IF TRUE a b
= ((((λb. λt. λf. b t f) TRUE) a) b)

Шаг 1. b := TRUE
        → (λt. λf. TRUE t f) a b
Шаг 2. t := a
        → (λf. TRUE a f) b
Шаг 3. f := b
        → TRUE a b
Шаг 4. Разворачиваем TRUE = λt. λf. t, подставляем t := a
        → (λf. a) b
Шаг 5. f := b, в теле `a` переменной f нет
        → a

Условный оператор получился из ничего, кроме функций. В коде:

const TRUE  = t => f => t;
const FALSE = t => f => f;
const IF    = b => t => f => b(t)(f);

console.log(IF(TRUE)("да")("нет"));  // "да"
console.log(IF(FALSE)("да")("нет")); // "нет"

TRUE  = lambda t: lambda f: t
FALSE = lambda t: lambda f: f
IF    = lambda b: lambda t: lambda f: b(t)(f)

print(IF(TRUE)("да")("нет"))   # да
print(IF(FALSE)("да")("нет"))  # нет

Числа кодируются как «сколько раз применить функцию»:

0 = λf. λx. x            — не применять
1 = λf. λx. f x          — применить один раз
2 = λf. λx. f (f x)      — два раза
3 = λf. λx. f (f (f x))  — три раза

const two = f => x => f(f(x));
const inc = n => n + 1;
console.log(two(inc)(0)); // 2 — «раскодировали» число Чёрча в обычное

two = lambda f: lambda x: f(f(x))
inc = lambda n: n + 1
print(two(inc)(0))  # 2

Сложение, умножение, вычитание, сравнение — всё выводится отсюда, и всё разбирается в https://courses.digitable.life/post/lambda-calculus/05-numerals/. Пары и списки — в https://courses.digitable.life/post/lambda-calculus/06-pairs-and-lists/. Рекурсия без имён через комбинатор Y — в https://courses.digitable.life/post/lambda-calculus/07-recursion-and-y/.

Одна ловушка, о которой надо знать сразу

Подстановка «заменить x на N» звучит просто, но есть случай, где наивная замена даёт неправильный ответ. Возьмём:

(λx. λy. x) y

Наивно подставляем x := y:

→ λy. y      ← НЕВЕРНО

Что произошло: внешняя y была свободной переменной (ссылкой на что-то извне), а после подстановки она попала под λy и стала связанной. Смысл поменялся: была «функция, всегда возвращающая внешнее y», стало тождество. Это называется захват переменной.

Правильно — сначала переименовать связанную переменную (это α-преобразование):

(λx. λy. x) y
= (λx. λz. x) y      α-переименование y → z внутри абстракции
→ λz. y              теперь подстановка безопасна

Захват имён — единственная реальная сложность в механике лямбда-исчисления, и ровно из-за него в компиляторах используют индексы де Брёйна и генерацию свежих имён. Полный разбор — https://courses.digitable.life/post/lambda-calculus/02-variables-and-substitution/ и https://courses.digitable.life/post/lambda-calculus/03-reductions/.

Немного истории: откуда это взялось

timeline title От проблемы разрешения до стрелочных функций 1928 : Гильберт формулирует Entscheidungsproblem — существует ли алгоритм, решающий любое математическое утверждение 1932 : Чёрч предлагает лямбда-исчисление как основание математики 1936 : Чёрч доказывает неразрешимость Entscheidungsproblem ; Тьюринг независимо публикует машину Тьюринга 1937 : Тьюринг доказывает эквивалентность лямбда-исчисления и машин Тьюринга 1958 : Маккарти создаёт Lisp — первый язык с лямбдами 1978 : Milner ML и вывод типов Хиндли-Милнера 1990 : Haskell 1.0 — ленивое вычисление в мейнстриме 2015 : ES6 приносит стрелочные функции в JavaScript

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

Это тезис, а не теорема: понятие «интуитивно вычислимо» нельзя формализовать, поэтому доказать его невозможно. Но за 90 лет ни одна предложенная модель вычислений (включая квантовую) не вышла за границы вычислимости по Тьюрингу — квантовые компьютеры меняют сложность, но не класс вычислимых функций. Тема вычислимости подробнее разбирается в треке https://courses.digitable.life/post/mathematics/00-overview/.

Что мы получаем: карта области

mindmap root(("λ-исчисление")) Синтаксис переменная абстракция аппликация Преобразования "α — переименование" "β — вычисление" "η — расширение" Кодирование данных булевы значения числа Чёрча пары и списки рекурсия через Y Стратегии нормальный порядок аппликативный порядок ленивость Типы просто типизированное "Карри-Ховард" "System F и generics" Практика Lisp и Scheme "ML, Haskell, OCaml" стрелочные функции

Типичные заблуждения

«Это то же самое, что функциональное программирование». Нет. ФП — стиль разработки на реальных языках с типами, IO, библиотеками и производительностью. Лямбда-исчисление — формальная модель, в которой нет ни IO, ни эффектов, ни времени выполнения. ФП стоит на нём, но не равно ему. Практическая сторона — трек https://courses.digitable.life/post/functional-programming/00-overview/.

«λ-функции в моём языке — это те самые лямбды». Почти. Разница существенная: в чистом лямбда-исчислении нет побочных эффектов, все функции одноаргументные, и порядок вычисления не фиксирован. x => console.log(x) — уже не лямбда-терм в чистом смысле.

«Раз всё кодируется функциями, так и надо программировать». Категорически нет. Числа Чёрча — это унарная арифметика: сложение чисел n и m требует O(n) применений функции, а не одну инструкцию процессора. Кодировки — доказательство выразительной мощи, а не рецепт для прода.

«Нормальная форма есть всегда». Нет: Ω не имеет нормальной формы. Более того, у терма может быть нормальная форма, до которой одна стратегия вычисления доходит, а другая — нет. Об этом — https://courses.digitable.life/post/lambda-calculus/08-evaluation-strategies/.

Упражнения

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

(λx. x) (λy. y)
(λx. λy. y x) a (λz. z)
(λf. f (f a)) (λx. x)
(λx. x x) (λy. y)
(λx. λy. x) y — осторожно, здесь ловушка
(λp. λq. p q p) (λt. λf. t) (λt. λf. f)

Ответы

1. Один редекс, подставляем x := (λy. y):

(λx. x) (λy. y) → λy. y

2. Скобки: ((λx. λy. y x) a) (λz. z).

Шаг 1. x := a          → (λy. y a) (λz. z)
Шаг 2. y := (λz. z)    → (λz. z) a
Шаг 3. z := a          → a

Шаг 1. f := (λx. x)    → (λx. x) ((λx. x) a)
Шаг 2. внутренний:     → (λx. x) a
Шаг 3.                 → a

4. Похоже на Ω, но аргумент другой — расходимости не будет:

Шаг 1. x := (λy. y)    → (λy. y) (λy. y)
Шаг 2. y := (λy. y)    → λy. y

5. Ловушка на захвате. Наивная подстановка даёт λy. y — это неверно, свободная y превратилась бы в связанную. Правильно:

Шаг 1. α-переименование связанной y → z:   (λx. λz. x) y
Шаг 2. x := y                              → λz. y

Ответ: λz. y — функция, игнорирующая аргумент и возвращающая внешнюю y.

6. Это AND TRUE FALSE в кодировке Чёрча. Обозначим T = λt. λf. t, F = λt. λf. f.

Шаг 1. p := T          → (λq. T q T) F
Шаг 2. q := F          → T F T
Шаг 3. Раскрываем T = λt. λf. t, подставляем t := F   → (λf. F) T
Шаг 4. f := T, в теле F переменной f нет (после α-переименования внутри F имена не конфликтуют)
                       → F = λt. λf. f

Ответ: FALSE. Терм λp. λq. p q p — это логическое «И».

Мини-итог

Лямбда-исчисление — язык из трёх конструкций: переменная, абстракция λx. M, аппликация M N.
Единственное правило вычисления — бета-редукция: (λx. M) N → M[x := N].
Всё остальное — числа, логика, структуры данных, рекурсия — кодируется функциями.
Оно полно по Тьюрингу: выражает ровно то же, что машина Тьюринга, включая незавершающиеся вычисления.
Единственная механическая сложность — захват имён при подстановке; лечится α-переименованием.
Практическая ценность для разработчика: замыкания, каррирование, системы типов, устройство компиляторов и функциональных языков перестают быть чёрными ящиками.

Источники

Alonzo Church. An Unsolvable Problem of Elementary Number Theory, 1936 — https://www.jstor.org/stable/2371045
Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics — канонический справочник: https://www.cs.ru.nl/~henk/
Benjamin C. Pierce. Types and Programming Languages, MIT Press — https://www.cis.upenn.edu/~bcpierce/tapl/ (глава 5 — бестиповое лямбда-исчисление)
Raúl Rojas. A Tutorial Introduction to the Lambda Calculus — https://arxiv.org/abs/1503.09060 (короткое и очень понятное введение)
Stanford Encyclopedia of Philosophy, The Lambda Calculus — https://plato.stanford.edu/entries/lambda-calculus/
Интерактивный редуктор в браузере, чтобы проверять свои шаги — https://lambdacalc.io/

Что дальше

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

Нотация: переменная, абстракция, аппликация и как читать выражения

Нашли неточность? Выделите фрагмент текста — рядом появится жучок.

Лямбда-исчисление Чёрча: зачем оно программисту и что это вообще такое

Лямбда-исчисление Чёрча: зачем оно программисту и что это вообще такое

Зачем это программисту, а не только математику

Идея на одной аналогии

Три конструкции — и это весь язык

Три термина, которые встретятся везде

Один и тот же терм на трёх языках

Вычисление: бета-редукция

Где числа, булевы значения и списки?

Одна ловушка, о которой надо знать сразу

Немного истории: откуда это взялось

Что мы получаем: карта области

Типичные заблуждения

Упражнения

Ответы

Мини-итог

Источники

Что дальше

Нужен разбор именно вашей ситуации?

К заявке приложится контекст статьи

Что здесь нужно исправить?