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

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

f => x => f(f(x))

И на Python:

lambda f: lambda x: f(f(x))

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

Эта статья не про вычисления (они дальше по треку), а про чтение. Цель — чтобы к концу вы могли взять любое выражение, за пятнадцать секунд расставить в нём скобки, сказать вслух, что оно делает, и записать эквивалент на своём рабочем языке.

Зачем вообще отдельная нотация

Резонный вопрос: если это те же стрелочные функции, зачем учить чужой синтаксис?

Потому что языки программирования — грязные. В JavaScript у функции есть this, arguments, hoisting, разница между function и =>, значения по умолчанию, деструктуризация, async. Всё это полезно в работе и абсолютно мешает, когда вы хотите доказать что-то о вычислениях вообще. Чёрч в 1930-х искал минимальный язык, в котором можно выразить любое вычисление и при этом рассуждать о нём формально. Получилось три правила. Не десять, не сто — три.

Минимализм имеет цену: чтобы записать «два» или «истину», придётся выкручиваться (этим займёмся в статьях про числа Чёрча и булевы значения). Зато любое утверждение о языке доказывается перебором трёх случаев, а не тысячи страниц спецификации ECMAScript.

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

Три кирпича

Грамматика целиком — четыре строки. Термы (так называют выражения лямбда-исчисления) строятся так:

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

Всё. Больше в чистом лямбда-исчислении ничего нет. Ни констант, ни операторов, ни объявлений.

Разберём каждый кирпич отдельно и сразу с кодом.

Переменная

Переменная — это имя. x, y, f, foo. Ничего с ней не сделаешь и ничего в ней не хранится: она либо будет заменена на что-то при вызове функции, либо так и останется висеть как «неизвестное». Переменная в лямбда-исчислении ближе к параметру функции или к математическому «пусть x», чем к переменной в C, куда можно присвоить.

Важный момент: присваивания в языке нет. Ни x = 5, ни let, ни мутаций. Единственный способ «дать значение» переменной — применить к аргументу функцию, у которой эта переменная стоит параметром.

Абстракция — определение функции

λx. M читается: «функция, которая принимает x и возвращает M». Точка отделяет параметр от тела.

λx. x          -- функция тождества: вернуть аргумент как есть
λx. y          -- функция, которая игнорирует аргумент и всегда возвращает y
λx. x x        -- функция, применяющая аргумент к самому себе

Параллельно:

const id       = x => x;         // λx. x
const constY   = x => y;         // λx. y   (y берётся откуда-то извне)
const selfApp  = x => x(x);      // λx. x x

id_       = lambda x: x          # λx. x
const_y   = lambda x: y          # λx. y
self_app  = lambda x: x(x)       # λx. x x

Обратите внимание: λ в записи ровно там же, где lambda в Python, а точка — там же, где двоеточие. Соответствие буквальное:

Слово «абстракция» здесь означает «абстрагирование от конкретного значения»: в теле x x мы не знаем, что такое x, и именно поэтому получаем функцию, а не результат.

Аппликация — вызов функции

M N (просто два терма через пробел) означает «применить M к N». В обычных языках вы пишете M(N); в лямбда-исчислении скобки не нужны, аппликация обозначается соседством.

f x            -- f(x)
(λx. x) y      -- (x => x)(y)
f (g x)        -- f(g(x))

Это первое, обо что спотыкаются: пробел — это оператор. f x — не «две вещи рядом», а вызов. Как умножение в 2ab у математиков.

f(x);
(x => x)(y);
f(g(x));

f(x)
(lambda x: x)(y)
f(g(x))

Два соглашения о скобках

Полная грамматика требует скобок вокруг каждой абстракции и каждой аппликации, но никто так не пишет — получается частокол. Поэтому приняты два соглашения, и именно они делают выражения нечитаемыми для новичка. Выучите их — и половина проблемы исчезнет.

Соглашение 1: аппликация левоассоциативна

f x y z   ≡   (((f x) y) z)

То есть f применяется к x, результат применяется к y, результат — к z. Это НЕ «функция f от трёх аргументов» и не f(x, y, z) — в лямбда-исчислении вообще нет функций от нескольких аргументов, о чём ниже.

Проверьте себя на JS — там ровно то же самое:

f(x)(y)(z)   // именно так, а не f(x, y, z)

Соглашение 2: тело абстракции тянется вправо как можно дальше

λx. f x y   ≡   λx. ((f x) y)     -- а НЕ ((λx. f) x) y

Точка «открывает скобку», которая закрывается в конце выражения или на ближайшей закрывающей скобке. Хотите оборвать тело раньше — ставьте скобки руками:

(λx. f x) y     -- вот здесь тело — только «f x», а y применяется снаружи

Это соглашение — источник примерно 90% ошибок при чтении. Всякий раз, увидев λ, мысленно ставьте открывающую скобку сразу после точки и ищите, где она закроется.

Соглашение 3 (сокращение): склейка параметров

λx y z. M   ≡   λx. λy. λz. M

Иногда пишут λxyz. M — то же самое, если имена односимвольные. Это чистая экономия чернил, никакой новой сущности.

Каррирование: почему аргумент всегда один

В лямбда-исчислении каждая функция принимает ровно один аргумент. Функцию «двух аргументов» изображают функцией, которая берёт первый и возвращает функцию, ждущую второй. Приём называется каррированием — в честь Хаскелла Карри (хотя придумал его Мозес Шёнфинкель).

λx. λy. x       -- «взять x, вернуть функцию, которая игнорирует y и отдаёт x»

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

(λx. λy. x) a b
  ≡ ((λx. λy. x) a) b        -- шаг 0: расставили скобки по соглашению 1
  → (λy. a) b                -- шаг 1: подставили a вместо x в тело «λy. x»
  → a                        -- шаг 2: подставили b вместо y в тело «a»; y там не встречается

Второй аргумент просто выброшен — это и есть функция K (в кодировании Чёрча она же true).

const K = x => y => x;
K(1)(2);        // 1
const always1 = K(1);   // частичное применение: осталась функция y => 1
always1(999);   // 1

K = lambda x: lambda y: x
K(1)(2)          # 1
always1 = K(1)   # y => 1
always1(999)     # 1

Частичное применение, которое во фреймворках подают как продвинутый приём, — просто побочный эффект того, что аргумент всегда один.

Практическая сторона каррирования и композиции подробно разобрана в треке функционального программирования: Композиция и каррирование.

Как читать выражение: алгоритм

Когда выражение длинное, полезен механический порядок действий, а не «вглядываться».

Прогоним на живом примере: λf. λx. f (f x).

Шаг 1. Первая λ — λf., её тело тянется до конца: λf. (λx. f (f x)).

Шаг 2. Внутри — λx., её тело тоже до конца фрагмента: λf. (λx. (f (f x))).

Шаг 3. Аппликации: внутренняя f x уже в скобках, внешняя f (...) — тоже. Группировать нечего.

Шаг 4. Читаем вслух: «функция от f, возвращающая функцию от x, которая применяет f к результату применения f к x». То есть «применить f дважды».

Шаг 5. Записываем кодом:

const twice = f => x => f(f(x));
twice(n => n + 1)(0);   // 2

twice = lambda f: lambda x: f(f(x))
twice(lambda n: n + 1)(0)   # 2

Это, кстати, число 2 в кодировании Чёрча: «сделай что-нибудь дважды». Числа в этой системе — глаголы, а не существительные.

Дерево разбора

Любой терм — это дерево с тремя видами узлов. Полезно держать эту картинку в голове: скобки лишь описывают форму дерева, а дерево — настоящий объект.

Вот λf. λx. f (f x):

А вот структура типов такого дерева — то, что вы напишете, если решите реализовать интерпретатор:

Реализация на Python — тридцать строк, включая печать со скобками по соглашениям:

from dataclasses import dataclass

# Три конструктора термов — ровно три класса
@dataclass(frozen=True)
class Var:
    name: str

@dataclass(frozen=True)
class Abs:
    param: str
    body: "Term"

@dataclass(frozen=True)
class App:
    func: "Term"
    arg: "Term"

Term = Var | Abs | App

def show(t: Term, top: bool = True) -> str:
    """Печать терма с минимальным набором скобок."""
    match t:
        case Var(name):
            return name
        case Abs(param, body):
            s = f"\\{param}.{show(body)}"
            # абстракция берётся в скобки, если она не на верхнем уровне
            return s if top else f"({s})"
        case App(f, a):
            # аргумент скобим, если он сам аппликация или абстракция
            left = show(f, top=False) if isinstance(f, Abs) else show(f, top=True)
            right = show(a, top=False) if isinstance(a, (Abs, App)) else show(a)
            return f"{left} {right}"

two = Abs("f", Abs("x", App(Var("f"), App(Var("f"), Var("x")))))
print(show(two))   # \f.\x.f (f x)

Сложность печати — O(n) по времени и O(глубина) по памяти на стек рекурсии, где n — число узлов. То же на TypeScript:

type Term =
  | { kind: "var"; name: string }
  | { kind: "abs"; param: string; body: Term }
  | { kind: "app"; func: Term; arg: Term };

const v = (name: string): Term => ({ kind: "var", name });
const abs = (param: string, body: Term): Term => ({ kind: "abs", param, body });
const app = (func: Term, arg: Term): Term => ({ kind: "app", func, arg });

function show(t: Term, top = true): string {
  switch (t.kind) {
    case "var":
      return t.name;
    case "abs": {
      const s = `\\${t.param}.${show(t.body)}`;
      return top ? s : `(${s})`;
    }
    case "app": {
      const left = t.func.kind === "abs" ? show(t.func, false) : show(t.func);
      const right = t.arg.kind === "var" ? show(t.arg) : show(t.arg, false);
      return `${left} ${right}`;
    }
  }
}

// \f.\x.f (f x)
console.log(show(abs("f", abs("x", app(v("f"), app(v("f"), v("x")))))));

Заметьте: в коде вместо λ обычно пишут \ — так принято в Haskell и в большинстве текстовых нотаций, потому что греческую букву неудобно набирать.

Редекс: где именно «есть что вычислять»

Ещё одно слово, которое понадобится дальше. Редекс (от reducible expression) — это кусок вида (λx. M) N: абстракция, применённая к аргументу. Именно редексы можно упрощать.

(λx. x) y            -- редекс, весь терм целиком
f ((λx. x) y)        -- редекс внутри аргумента
λz. (λx. x) y        -- редекс внутри тела
x y                  -- редексов нет, вычислять нечего

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

(λx. x x) (λx. x x)
  → (x x)[x := λx. x x]
  ≡ (λx. x x) (λx. x x)      -- вернулись ровно туда же

Этот терм зовут Ω, и он редуцируется в себя бесконечно — лямбда-версия while (true) {}. На JS это буквально мгновенное переполнение стека:

const omega = (x => x(x))(x => x(x));   // RangeError: Maximum call stack size exceeded

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

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

1. Считать f x y вызовом с двумя аргументами. Это (f x) y. Если f — функция одного аргумента, возвращающая не-функцию, выражение бессмысленно (в бестиповом исчислении — просто застревает, в типизированном — не пройдёт проверку типов).

2. Обрывать тело абстракции раньше времени. λx. x y — это λx. (x y), а не (λx. x) y. Разница принципиальная: первое — функция, второе редуцируется к y.

λx. x y          -- функция; в JS: x => x(y)
(λx. x) y        -- вызов; → y

3. Путать λx. λy. M и «функцию двух аргументов». Формально это разные вещи, хотя ведут себя похоже. Как только вы примените такой терм к одному аргументу, получится функция — и это законный, полезный объект.

4. Думать, что имена переменных что-то значат. λx. x и λy. y — одна и та же функция, просто параметр назван иначе. Формально это фиксируется альфа-эквивалентностью, см. статью о редукциях.

5. Забывать, что скобки вокруг аргумента обязательны. f g x — это (f g) x, то есть f применяется к g, потом к x. Если вы имели в виду f(g(x)), пишите f (g x). Один пробел и пара скобок полностью меняют смысл — как в JS f(g)(x) против f(g(x)).

Соглашения об именах, которые встретите в литературе

Не часть языка, но помогает читать чужие тексты:

• x, y, z — обычные переменные;
• f, g, h — переменные, играющие роль функций;
• M, N, P — метапеременные, то есть «любой терм» (в самом языке их нет, это часть языка описания);
• заглавные жирные или прописные имена вроде I, K, S, Y, TRUE, SUCC — общепринятые сокращения для конкретных термов. Это чистые макросы: везде, где стоит I, подставьте λx. x.

I ≡ λx. x                    -- identity
K ≡ λx. λy. x                -- константа / true
S ≡ λf. λg. λx. f x (g x)    -- «распределитель» аргумента

Комбинаторы S и K замечательны тем, что из них двоих собирается любое замкнутое лямбда-выражение — это отдельная ветвь под названием комбинаторная логика. Каноническое изложение — Barendregt, «The Lambda Calculus: Its Syntax and Semantics» (https://www.elsevier.com/books/the-lambda-calculus/barendregt/978-0-444-87508-2), а для мягкого входа — глава 5 книги Пирса «Types and Programming Languages» (https://www.cis.upenn.edu/~bcpierce/tapl/).

Разберём выражение целиком, шаг за шагом

Возьмём то, что пугает: (λf. λx. f (f x)) (λy. y z) w.

Шаг 1. Расставляем скобки по соглашениям. Аппликация левоассоциативна:

((λf. λx. f (f x)) (λy. y z)) w

Внешняя структура: сначала первый терм применяется к (λy. y z), потом результат — к w.

Шаг 2. Первая бета-редукция. Редекс — (λf. λx. f (f x)) (λy. y z). Подставляем λy. y z вместо f:

(λx. f (f x))[f := λy. y z]
  ≡ λx. (λy. y z) ((λy. y z) x)

Получилось:

(λx. (λy. y z) ((λy. y z) x)) w

Шаг 3. Вторая бета-редукция. Внешний редекс: подставляем w вместо x:

(λy. y z) ((λy. y z) w)

Шаг 4. Редуцируем внутренний аргумент (λy. y z) w — подставляем w вместо y в тело y z:

(λy. y z) (w z)

Шаг 5. Последняя редукция. Подставляем w z вместо y в тело y z:

(w z) z

Шаг 6. Редексов больше нет — это нормальная форма. По соглашению пишем без лишних скобок:

w z z

Проверим кодом — а заодно убедимся, что это не абстрактная игра:

const twice = f => x => f(f(x));
const g = y => `(${y} z)`;      // моделируем «y z» как строку
console.log(twice(g)("w"));      // ((w z) z)

twice = lambda f: lambda x: f(f(x))
g = lambda y: f"({y} z)"
print(twice(g)("w"))   # ((w z) z)

Строки здесь — просто способ увидеть форму результата; лямбда-исчисление получило w z z, и код показывает ту же вложенность.

Упражнения

Сначала решайте, потом смотрите ответ. Пишите все шаги: пропущенный шаг — это место, где обычно и прячется ошибка.

1. Расставьте все скобки: λx. λy. x y z

λx. (λy. ((x y) z))

2. Расставьте все скобки: (λx. x) λy. y z

(λx. x) (λy. (y z))

3. Сведите к нормальной форме: (λx. λy. y x) a (λz. z)

((λx. λy. y x) a) (λz. z)     -- скобки
→ (λy. y a) (λz. z)           -- x := a
→ (λz. z) a                   -- y := λz. z
→ a                           -- z := a

4. Сведите к нормальной форме: (λf. f (f a)) (λx. x)

(λf. f (f a)) (λx. x)
→ (λx. x) ((λx. x) a)         -- f := λx. x
→ (λx. x) a                   -- редуцируем аргумент: x := a
→ a                           -- x := a

5. Переведите на λ-нотацию: const compose = f => g => x => f(g(x));

λf. λg. λx. f (g x)

6. Что не так с записью λ. x?

7. Сведите к нормальной форме: (λx. x x) (λy. y)

(λx. x x) (λy. y)
→ (λy. y) (λy. y)             -- x := λy. y, обе копии
→ λy. y                       -- y := λy. y

8. Сколько редексов в терме (λx. (λy. y) x) ((λz. z) a)?

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

• Peter Selinger, «Lecture Notes on the Lambda Calculus» — бесплатный, аккуратный и очень читаемый конспект: https://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf
• Стэнфордская энциклопедия философии, статья The Lambda Calculus — история и связь с логикой: https://plato.stanford.edu/entries/lambda-calculus/
• Раздел о логике и доказательствах в треке математики — Логика и доказательства; там формальные системы и правила вывода, из которых лямбда-исчисление выросло.
• Практическая сторона — Функции высшего порядка: то же самое, но на рабочем коде.

Мини-итог

• Термов ровно три вида: переменная x, абстракция λx. M, аппликация M N. Никаких констант, присваиваний и операторов.
• Аппликация — это пробел, и она левоассоциативна: f x y = (f x) y.
• Тело абстракции тянется вправо до упора: λx. f x y = λx. ((f x) y).
• Функции одноаргументные всегда; «много аргументов» — это каррирование, а частичное применение получается само собой.
• λx. M — это ровно x => M и lambda x: M. Ничего нового по сравнению с вашим ежедневным кодом; новое — только строгость.
• Редекс (λx. M) N — место, где есть что вычислять; терм без редексов находится в нормальной форме.

Синтаксис разобрали. Дальше начинается самое коварное место всего исчисления: подстановка. Она выглядит очевидной («заменить x на аргумент»), но наивная реализация ломается на именах — и именно там прячется единственный по-настоящему тонкий момент в этой теории.

Что дальше

Свободные и связанные переменные, подстановка и захват имён — узнаем, какие переменные «свои», какие «чужие», почему (λx. λy. x) y нельзя редуцировать в лоб и как альфа-переименование спасает положение.