Альфа, бета и эта: три преобразования, из которых всё состоит

Зачем вообще какие-то «преобразования»

Пока что лямбда-выражение — это просто текст. λx. x — набор символов. Чтобы из текста получилось вычисление, нужны правила, которые говорят: «вот этот кусок текста можно переписать вот в этот».

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

Аналогия из школы: упрощение алгебраического выражения. 2 * (3 + 4) → 2 * 7 → 14. Вы не «выполняете программу», вы переписываете формулу по правилам, пока переписывать больше нечего. Лямбда-исчисление устроено ровно так же, только правил всего три, и одно из них делает всю работу.

Вот эти три правила:

Дальше — каждое подробно, с полной раскруткой всех шагов. Если нотация λx. x y пока читается тяжело, вернитесь к статьям Нотация: переменная, абстракция и аппликация и Свободные и связанные переменные — здесь мы на них опираемся.

Быстрый словарь: редекс, нормальная форма, шаг

Три термина, без которых дальше не поговорить.

Редекс (redex, от reducible expression) — кусок выражения, к которому применимо правило. Для беты редекс выглядит всегда одинаково: абстракция, применённая к чему-то, то есть (λx. тело) аргумент. Если вы видите открывающую скобку, за ней лямбду, а после закрывающей — ещё один терм, это редекс.

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

Нормальная форма — выражение, в котором редексов больше нет. Переписывать нечего, вычисление закончилось. Это и есть «ответ».

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

Альфа-преобразование: имя параметра ничего не значит

Начнём с самого простого правила, потому что оно почти ничего не делает — но без него сломается всё остальное.

Возьмите функцию тождества:

λx. x

и её же, но с другим именем параметра:

λy. y

Это одна и та же функция. Приняли что-то — вернули это же. Имя параметра — просто дырка, в которую подставят аргумент; как её зовут, никого не касается.

Формально:

λx. M   →α→   λy. M[x := y]     при условии, что y не встречается свободно в M

Читается: «в абстракции по x можно переименовать x в y, заменив все связанные вхождения x в теле на y — если только y не занято».

В вашем коде это буквально Rename Symbol.

// Эти две функции неразличимы для вызывающего кода
const id1 = (x) => x;
const id2 = (y) => y;

console.log(id1(42), id2(42)); // 42 42

# То же самое на Python
id1 = lambda x: x
id2 = lambda y: y

print(id1(42), id2(42))  # 42 42

Где альфа ломается: условие «y не занято»

Условие про свободные вхождения — не формальность. Смотрите:

λx. x z

Функция: «принять x, применить его к внешнему z». Попробуем переименовать x в z:

λz. z z       ← НЕПРАВИЛЬНО

Получилось совсем другое: функция самоприменения. Внешнее z, которое было свободным (ссылалось «наружу»), проглотил связыватель λz. Смысл уничтожен.

Тот же баг в JavaScript:

const z = "внешнее значение";

const good = (x) => [x, z];       // ["арг", "внешнее значение"]
const bad  = (z) => [z, z];       // ["арг", "арг"]  ← переименовали в занятое имя

console.log(good("арг")); // [ 'арг', 'внешнее значение' ]
console.log(bad("арг"));  // [ 'арг', 'арг' ]

Это ровно то, что в компиляторах называется shadowing и за что линтер выдаёт no-shadow. Альфа-преобразование — легально; переименование в занятое имя — не альфа-преобразование, а ошибка.

Альфа-эквивалентность

Два выражения альфа-эквивалентны, если одно получается из другого переименованиями связанных переменных. λx.λy. x и λa.λb. a — альфа-эквивалентны. На практике их считают просто равными и записывают λx.λy. x ≡α λa.λb. a.

Радикальное решение проблемы имён — индексы де Брёйна: вместо имени пишем число, показывающее, через сколько связывателей наружу искать. λx.λy. x становится λ.λ. 2. Альфа-эквивалентные термы получают буквально одинаковую запись, и альфа-преобразование исчезает как понятие. Так устроены внутренности многих реальных компиляторов и proof-ассистентов (см. описание в Wikipedia: De Bruijn index).

Бета-редукция: главное правило

Вот оно — единственное правило, которое реально вычисляет.

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

«Абстракция по x, применённая к N, переписывается в тело M, где каждое свободное вхождение x заменено на N».

Это и есть вызов функции. Не «похоже на вызов», а именно он. Когда JS-движок выполняет (x => x + 1)(5), он делает концептуально то же, что бета-редукция: связывает x с 5 и вычисляет тело.

Пример 1: самый простой

Считаем (λx. x) a.

Шаг 0.  (λx. x) a
        ^^^^^^^^^ редекс: абстракция λx.x применена к a
        тело M = x, аргумент N = a
        M[x := a] = x[x := a] = a

Шаг 1.  a
        Редексов нет → нормальная форма.

Ответ: a.

Пример 2: два аргумента, каррирование

Считаем (λx. λy. x) a b.

Первым делом расставим скобки. Аппликация левоассоциативна, то есть f a b означает (f a) b:

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

Раскручиваем:

Шаг 0.  ((λx. λy. x) a) b

        Самый левый внешний редекс — это (λx. λy. x) a.
        Тело M = λy. x, аргумент N = a.
        M[x := a] = (λy. x)[x := a] = λy. a

Шаг 1.  (λy. a) b

        Редекс: (λy. a) b.
        Тело M = a, аргумент N = b.
        M[y := b] = a[y := b] = a      (в теле нет ни одного y — аргумент просто выброшен)

Шаг 2.  a
        Нормальная форма.

Ответ: a. Функция λx.λy. x — это комбинатор K: берёт два аргумента, возвращает первый, второй игнорирует. В JS/Python:

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

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

Заметьте: два шага редукции — два вызова. Каррирование в лямбда-исчислении не «фича», а единственный способ иметь несколько аргументов: абстракция всегда одноместная.

Пример 3: аргумент используется дважды

Считаем (λf. λx. f (f x)) g z, то есть ((λf. λx. f (f x)) g) z.

Шаг 0.  ((λf. λx. f (f x)) g) z

        Редекс: (λf. λx. f (f x)) g
        Тело M = λx. f (f x), N = g
        M[f := g]: заменяем ОБА свободных вхождения f
                 = λx. g (g x)

Шаг 1.  (λx. g (g x)) z

        Редекс: вся эта аппликация.
        Тело M = g (g x), N = z
        M[x := z] = g (g z)

Шаг 2.  g (g z)

        Есть ли редексы? g — переменная, не абстракция.
        Значит (g z) — не редекс, и g (g z) — не редекс.
        Нормальная форма.

Ответ: g (g z). Это число Чёрча «два» в действии — применить g к z дважды. Подробно про это в статье Числа Чёрча.

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

Пример 4: редекс внутри редекса

Считаем (λx. x x) (λy. y).

Шаг 0.  (λx. x x) (λy. y)

        Тело M = x x, N = λy. y
        M[x := λy. y] = (λy. y) (λy. y)

Шаг 1.  (λy. y) (λy. y)

        Теперь редекс — вся аппликация.
        Тело M = y, N = λy. y
        M[y := λy. y] = λy. y

Шаг 2.  λy. y
        Нормальная форма.

Ответ: λy. y. Тождество, применённое к себе, даёт тождество. Обратите внимание на шаг 0: подстановка скопировала аргумент в два места. Бета-редукция может увеличивать размер выражения — и это причина, по которой наивная реализация бывает экспоненциально медленной.

Подстановка — там, где живут баги

Запись M[x := N] в правиле беты выглядит невинно. На самом деле это самая коварная операция в лямбда-исчислении.

Три ветки, которые ломают наивные реализации:

1. λx. P — связыватель совпадает с подставляемой переменной. Внутрь идти нельзя: те x, что внутри, — это другие x, они принадлежат внутреннему связывателю.

(λx. λx. x) a
→ тело (λx. x), подставляем [x := a]
→ но связыватель λx перекрывает — внутрь не идём
→ λx. x

2. Свободная переменная не переименовывается. y[x := N] = y. Свободные переменные — это «ссылки наружу», их трогать нельзя.

3. Захват имени — та самая опасная ветка.

Захват имени, шаг за шагом

Считаем (λx. λy. x y) y. Внешняя y — свободная переменная, что-то из окружения.

Наивно (неправильно):

Шаг 0.  (λx. λy. x y) y
        M = λy. x y, N = y
        M[x := y] = λy. y y          ← ОШИБКА

Что случилось: свободная y из аргумента попала внутрь λy и стала связанной. Была ссылка на внешний мир — стал параметр. Смысл потерян: мы получили самоприменение вместо «применить внешнюю y к параметру».

Правильно:

Шаг 0.  (λx. λy. x y) y

        Хотим (λy. x y)[x := y].
        Проверка: связыватель тела — y. Свободные переменные аргумента: {y}.
        Пересечение непусто → УГРОЗА ЗАХВАТА.

Шаг 0а. α-переименование тела: λy. x y  →α→  λz. x z
        (z свежая, в теле не встречается)

Шаг 0б. Теперь подставляем: (λz. x z)[x := y] = λz. y z

Шаг 1.  λz. y z
        Нормальная форма.

Ответ: λz. y z. Внешняя y осталась свободной — как и должна была.

Вот тот же баг в реальном коде — он выглядит как безобидная перегрузка имени:

// Хотим "применить внешнюю y к параметру"
const y = (v) => `внешняя(${v})`;

const correct = (x) => (z) => x(z);   // параметр назвали z
console.log(correct(y)("q"));          // "внешняя(q)"

// А теперь "захват": внутренний параметр назвали y
const captured = (y) => y(y);          // y внутри — уже НЕ внешняя функция
// captured(y) вернёт "внешняя(function y)" — совсем другое поведение

y = lambda v: f"внешняя({v})"

correct = lambda x: lambda z: x(z)
print(correct(y)("q"))   # внешняя(q)

captured = lambda y: y(y)  # внутренняя y затенила внешнюю

Практический вывод. Любая реализация подстановки обязана переименовывать связыватели. Компиляторы решают это отдельным проходом «уникализации имён» (alpha-renaming pass, он же freshening), после которого каждое связанное имя в программе уникально и захват невозможен физически. Именно поэтому в промежуточных представлениях компиляторов вы видите x_17, tmp$4 и подобное.

Эта-преобразование: убираем лишнюю обёртку

Третье правило:

λx. (M x)   →η→   M     при условии, что x не встречается свободно в M

«Функция, которая принимает x и передаёт его дальше в M, — это просто M».

Интуиция очевидна для любого разработчика:

// Зачем оборачивать?
users.map(x => processUser(x));
// Когда можно так:
users.map(processUser);

# Зачем оборачивать?
list(map(lambda x: process_user(x), users))
# Когда можно так:
list(map(process_user, users))

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

Пошагово

Шаг 0.  λx. (f x)
        Проверка: свободна ли x в M = f? Нет, f — просто переменная.
        Условие выполнено.

Шаг 1.  f

А когда условие не выполнено:

λx. (x x)     ← M = x, и x свободна в M → эта НЕ применима

Если бы применили, получили бы x — совсем другой терм (переменная вместо функции).

Эта и экстенсиональность

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

Лямбда-исчисление с этой обычно обозначают λβη. Без неё — просто λβ. Формальный разбор есть у Барендрегта, The Lambda Calculus: Its Syntax and Semantics — канонический труд по теме (обзор на сайте автора).

Где эта опасна в настоящем коде

В чистом лямбда-исчислении эта безопасна всегда. В реальных языках — нет, и это классический источник багов:

// 1. this теряется
const obj = {
  name: "объект",
  greet(who) { return `${this.name} -> ${who}`; }
};
[1].map(x => obj.greet(x));  // работает
[1].map(obj.greet);          // TypeError: this.name — undefined

// 2. лишние аргументы map просачиваются
["1", "2", "3"].map(x => parseInt(x));  // [1, 2, 3]
["1", "2", "3"].map(parseInt);          // [1, NaN, NaN] — map передал ещё и индекс!

// 3. arity меняется
const f = (x) => x;
console.log(f.length, ((x) => f(x)).length);  // 1 1 — здесь совпало,
// но для (...args) => f(...args) length станет 0

# 1. позднее связывание: обёртка резолвит имя в момент ВЫЗОВА
def make_wrapped():
    return lambda x: target(x)   # target ещё не существует — и это ок

target = lambda x: x * 2
print(make_wrapped()(21))  # 42

# 2. эта-редукция ломает keyword-аргументы, если обёртка их не пробрасывает
def call(x):
    return sorted(x)

wrapped = lambda x: sorted(x)   # sorted(x, reverse=True) через wrapped уже не вызвать

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

Собираем всё вместе: как выглядит вычисление

Проверим руками:

Шаг 0.  ((λx. λy. x y) (λz. z)) w
        Редекс: (λx. λy. x y) (λz. z)
        M = λy. x y, N = λz. z
        Угроза захвата? Связыватель y; свободные переменные N = {} — пусто. Безопасно.
        M[x := λz. z] = λy. (λz. z) y

Шаг 1.  (λy. (λz. z) y) w
        Здесь ДВА редекса:
          (a) вся аппликация (λy. ...) w
          (b) внутренний (λz. z) y
        Берём самый левый внешний — (a).
        M = (λz. z) y, N = w
        M[y := w] = (λz. z) w

Шаг 2.  (λz. z) w
        M = z, N = w
        M[z := w] = w

Шаг 3.  w
        Нормальная форма.

А что было бы, начни мы с редекса (b)?

Шаг 1'. (λy. (λz. z) y) w
        Редуцируем (b): (λz. z) y → y
Шаг 2'. (λy. y) w
Шаг 3'. w

Тот же ответ. Это не совпадение — это теорема.

Теорема Чёрча–Россера: порядок не влияет на ответ

Свойство ромба (confluence). Если из терма M можно за какое-то число шагов получить P и (другим путём) Q, то существует терм R, к которому сводятся и P, и Q.

Практический смысл огромен:

1. Нормальная форма единственна. Если она есть, разные порядки редукции дадут альфа-эквивалентные результаты. «Правильного ответа» ровно один.
2. Порядок вычисления не влияет на результат. Он влияет только на то, найдёте ли вы результат вообще и за сколько шагов.

Второй пункт — не мелочь. Смотрите:

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

Раскрутим:

Шаг 0.  (λx. x x) (λx. x x)
        M = x x, N = (λx. x x)
        M[x := λx. x x] = (λx. x x) (λx. x x)

Шаг 1.  (λx. x x) (λx. x x)      ← ровно то же самое
Шаг 2.  (λx. x x) (λx. x x)
...

Ω редуцируется сам в себя вечно. Нормальной формы нет. Это бесконечный цикл, выраженный чистым переписыванием. В JS:

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

Теперь ключевой пример. Считаем (λx. λy. x) (λz. z) Ω, то есть K I Ω:

Нормальный порядок (самый левый ВНЕШНИЙ редекс первым):

Шаг 0.  ((λx. λy. x) (λz. z)) Ω
Шаг 1.  (λy. (λz. z)) Ω          [x := λz. z]
Шаг 2.  λz. z                    [y := Ω] — но y в теле НЕТ, Ω просто выброшен
        Нормальная форма. ОТВЕТ ПОЛУЧЕН.

Аппликативный порядок (сначала вычисляем аргументы):

Шаг 0.  ((λx. λy. x) (λz. z)) Ω
        Аргумент внешней аппликации — Ω. Вычисляем его первым.
Шаг 1.  ((λx. λy. x) (λz. z)) Ω   ← Ω свёлся сам в себя
Шаг 2.  ... вечно. ОТВЕТА НЕТ.

Один и тот же терм: при нормальном порядке — ответ, при аппликативном — зависание. Теорема о стандартизации гарантирует: если нормальная форма существует, нормальный порядок её найдёт. Именно поэтому Haskell ленив, а if в строгих языках не может быть обычной функцией. Разбор стратегий — в статье Стратегии вычисления, а практика ленивости — в Ленивость и потоки.

Рабочий редуктор

Хватит бумаги — вот полная реализация нормального порядка. Термы как алгебраические типы, подстановка с защитой от захвата, пошаговая редукция.

from itertools import count

# Терм — кортеж: ('var', имя) | ('lam', параметр, тело) | ('app', функция, аргумент)
def V(n):      return ('var', n)
def L(n, b):   return ('lam', n, b)
def A(f, a):   return ('app', f, a)


def free_vars(t):
    """Множество свободных переменных терма."""
    if t[0] == 'var':
        return {t[1]}
    if t[0] == 'lam':
        return free_vars(t[2]) - {t[1]}      # параметр связан — вычитаем
    return free_vars(t[1]) | free_vars(t[2])


_counter = count(1)
def fresh(base):
    """Свежее имя, которого гарантированно нет в терме."""
    return f"{base}{next(_counter)}"


def subst(t, x, s):
    """t[x := s] — подстановка, избегающая захвата имён."""
    if t[0] == 'var':
        return s if t[1] == x else t          # переменная: заменить или оставить
    if t[0] == 'app':
        return A(subst(t[1], x, s), subst(t[2], x, s))   # рекурсия в обе ветки

    _, y, body = t                            # абстракция λy. body
    if y == x:
        return t                              # x связана здесь — внутрь не идём
    if y in free_vars(s):
        z = fresh(y)                          # УГРОЗА ЗАХВАТА → α-переименование
        body = subst(body, y, V(z))
        y = z
    return L(y, subst(body, x, s))


def step(t):
    """Один β-шаг в нормальном порядке. None, если редексов нет."""
    if t[0] == 'app':
        f, a = t[1], t[2]
        if f[0] == 'lam':                     # (λx. M) N — редекс, бьём сюда
            return subst(f[2], f[1], a)
        r = step(f)                           # иначе сначала в функцию (левее)
        if r is not None:
            return A(r, a)
        r = step(a)                           # потом в аргумент
        if r is not None:
            return A(f, r)
        return None
    if t[0] == 'lam':                         # заходим под λ — это и есть
        r = step(t[2])                        # «внешний» порядок
        return L(t[1], r) if r is not None else None
    return None


def show(t):
    if t[0] == 'var':  return t[1]
    if t[0] == 'lam':  return f"(λ{t[1]}.{show(t[2])})"
    return f"({show(t[1])} {show(t[2])})"


def normalize(t, limit=1000, trace=False):
    for i in range(limit):
        if trace:
            print(f"  {i}: {show(t)}")
        r = step(t)
        if r is None:
            return t
        t = r
    raise RuntimeError("нормальная форма не найдена за отведённое число шагов")

Проверяем на наших примерах:

I    = L('x', V('x'))                                  # λx. x
K    = L('x', L('y', V('x')))                          # λx.λy. x
SUCC = L('n', L('f', L('x', A(V('f'), A(A(V('n'), V('f')), V('x'))))))
ONE  = L('f', L('x', A(V('f'), V('x'))))

print(show(normalize(A(A(K, V('a')), V('b')))))
# → a

print(show(normalize(A(L('x', L('y', A(V('x'), V('y')))), V('y')))))
# → (λy1.(y y1))     ← видно α-переименование: y стала y1, захвата не случилось

print(show(normalize(A(SUCC, ONE), trace=True)))
#   0: ((λn.(λf.(λx.(f ((n f) x))))) (λf.(λx.(f x))))
#   1: (λf.(λx.(f (((λf.(λx.(f x))) f) x))))
#   2: (λf.(λx.(f ((λx.(f x)) x))))
#   3: (λf.(λx.(f (f x))))
# → (λf.(λx.(f (f x))))    ← это число Чёрча «два»

Тот же редуктор на JavaScript — один в один, только термы объектами:

const V = (name) => ({ tag: "var", name });
const L = (param, body) => ({ tag: "lam", param, body });
const App = (fn, arg) => ({ tag: "app", fn, arg });

const freeVars = (t) => {
  if (t.tag === "var") return new Set([t.name]);
  if (t.tag === "lam") {
    const s = freeVars(t.body);
    s.delete(t.param);            // параметр связан
    return s;
  }
  return new Set([...freeVars(t.fn), ...freeVars(t.arg)]);
};

let counter = 0;
const fresh = (base) => `${base}${++counter}`;

// t[x := s] с защитой от захвата
const subst = (t, x, s) => {
  if (t.tag === "var") return t.name === x ? s : t;
  if (t.tag === "app") return App(subst(t.fn, x, s), subst(t.arg, x, s));
  if (t.param === x) return t;                    // x связана внутри — не трогаем

  let { param, body } = t;
  if (freeVars(s).has(param)) {                   // угроза захвата → α
    const z = fresh(param);
    body = subst(body, param, V(z));
    param = z;
  }
  return L(param, subst(body, x, s));
};

// один β-шаг, нормальный порядок
const step = (t) => {
  if (t.tag === "app") {
    if (t.fn.tag === "lam") return subst(t.fn.body, t.fn.param, t.arg);
    const f = step(t.fn);
    if (f) return App(f, t.arg);
    const a = step(t.arg);
    if (a) return App(t.fn, a);
    return null;
  }
  if (t.tag === "lam") {
    const b = step(t.body);
    return b ? L(t.param, b) : null;
  }
  return null;
};

const show = (t) =>
  t.tag === "var" ? t.name
  : t.tag === "lam" ? `(λ${t.param}.${show(t.body)})`
  : `(${show(t.fn)} ${show(t.arg)})`;

function normalize(t, limit = 1000) {
  for (let i = 0; i < limit; i++) {
    const r = step(t);
    if (!r) return t;
    t = r;
  }
  throw new Error("нормальная форма не найдена");
}

const K = L("x", L("y", V("x")));
console.log(show(normalize(App(App(K, V("a")), V("b")))));   // a
console.log(show(normalize(App(L("x", L("y", App(V("x"), V("y")))), V("y")))));
// (λy1.(y y1))

Сложность. Один шаг step в худшем случае обходит весь терм: O(n) по времени, и subst может скопировать аргумент в каждое вхождение переменной — размер терма растёт до O(n·k). Число шагов до нормальной формы в общем случае не ограничено никакой рекурсивной функцией (иначе решалась бы проблема останова). Именно поэтому промышленные реализации не переписывают термы буквально, а используют окружения и замыкания — это подход Krivine machine и SECD-машины, где подстановка заменена на таблицу связываний, а копирование — на разделяемые ссылки.

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

Забыли, что аппликация левоассоциативна. f a b — это (f a) b, а не f (a b). Половина ошибок в упражнениях отсюда.

Забыли, что тело абстракции тянется максимально вправо. λx. f x y — это λx. ((f x) y), а не (λx. f x) y. Если хотите второе — ставьте скобки.

Подставили под совпадающий связыватель. В (λx. λx. x) a внутренняя x не имеет отношения к внешней.

Проигнорировали захват. Самая частая и самая тихая ошибка: результат выглядит правдоподобно, а смысл другой. Всегда проверяйте свободные переменные аргумента против связывателей тела.

Применили эту без проверки условия. λx. x x не сводится к x.

Решили, что редукция обязана закончиться. Нет. Ω и Y-комбинатор — контрпримеры, и именно на них держится рекурсия (см. Рекурсия без имён).

Спутали «нет редексов» с «получилось красиво». g (g z) — нормальная форма, хотя выглядит как незаконченное вычисление. Нормальная форма — синтаксическое свойство, а не эстетическое.

Упражнения

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

1. (λx. λy. y x) a (λz. z)

2. (λx. x x) (λy. y)

3. (λx. λy. x) y (обратите внимание на имена!)

4. λx. (λy. y) x — сначала бетой, потом этой; сравните результаты.

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

6. (λn. λf. λx. f (n f x)) (λf. λx. f x) — это SUCC ONE.

7. Почему (λx. λy. x) a Ω даёт a, а (λx. x x) ((λy. y) a) при аппликативном порядке ведёт себя иначе, чем при нормальном?

Ответы

1. ((λx. λy. y x) a) (λz. z)

Шаг 0.  ((λx. λy. y x) a) (λz. z)
        Редекс (λx. λy. y x) a; M = λy. y x, N = a
        Захват? связыватель y, FV(a) = {a} — безопасно.
        M[x := a] = λy. y a
Шаг 1.  (λy. y a) (λz. z)
        M = y a, N = λz. z
        M[y := λz. z] = (λz. z) a
Шаг 2.  (λz. z) a
        M = z, N = a → a
Шаг 3.  a

Ответ: a

2.

Шаг 0.  (λx. x x) (λy. y)
        M = x x, N = λy. y → (λy. y) (λy. y)
Шаг 1.  (λy. y) (λy. y)
        M = y, N = λy. y → λy. y
Шаг 2.  λy. y

Ответ: λy. y

3.

Шаг 0.  (λx. λy. x) y
        Хотим (λy. x)[x := y].
        Связыватель тела: y. FV(y) = {y}. ПЕРЕСЕЧЕНИЕ → захват!
Шаг 0а. α: λy. x  →  λw. x
Шаг 0б. (λw. x)[x := y] = λw. y
Шаг 1.  λw. y

Ответ: λw. y — константная функция, возвращающая внешнюю y. Наивный ответ λy. y (тождество) был бы неверным.

4.

Путь бета:  λx. (λy. y) x
            внутренний редекс (λy. y) x → x
            → λx. x

Путь эта:   λx. (λy. y) x
            вид λx. (M x), где M = λy. y; x свободна в M? нет.
            → λy. y

λx. x и λy. y альфа-эквивалентны — это один и тот же терм. Оба пути дали один ответ, как и обещает Чёрч–Россер для λβη.

Ответ: λx. x (≡α λy. y)

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

Шаг 0.  ((λf. λx. f (f x)) (λy. y)) w
        M = λx. f (f x), N = λy. y
        Захват? связыватель x, FV(λy. y) = {} — безопасно.
        M[f := λy. y] = λx. (λy. y) ((λy. y) x)
Шаг 1.  (λx. (λy. y) ((λy. y) x)) w
        Самый левый внешний редекс — вся аппликация.
        M[x := w] = (λy. y) ((λy. y) w)
Шаг 2.  (λy. y) ((λy. y) w)
        Самый левый внешний: внешняя аппликация. M = y, N = (λy. y) w
        → (λy. y) w
Шаг 3.  (λy. y) w
        → w
Шаг 4.  w

Ответ: w

6.

Шаг 0.  (λn. λf. λx. f (n f x)) (λf. λx. f x)
        M = λf. λx. f (n f x), N = λf. λx. f x
        Захват? связыватели f и x; FV(N) = {} (все переменные N связаны) — безопасно.
        M[n := N] = λf. λx. f ((λf. λx. f x) f x)
Шаг 1.  λf. λx. f (((λf. λx. f x) f) x)
        Внутренний редекс: (λf. λx. f x) f
        Здесь связыватель совпадает с подставляемой переменной? Тело λx. f x,
        подставляем [f := f] — внешний λf уже снят, идём в тело:
        (λx. f x)[f := f] = λx. f x
Шаг 2.  λf. λx. f ((λx. f x) x)
        Редекс: (λx. f x) x
        M = f x, N = x → f x
Шаг 3.  λf. λx. f (f x)
        Нормальная форма.

Ответ: λf. λx. f (f x) — число Чёрча «два». Прибавление единицы к единице действительно дало двойку, и никаких чисел при этом не понадобилось.

7. Разбор:

• (λx. λy. x) a Ω → (λy. a) Ω → a. Аргумент Ω выброшен, не вычисляясь, потому что y не встречается в теле. При нормальном порядке это работает; при аппликативном мы бы попытались сначала посчитать Ω и зациклились.
• (λx. x x) ((λy. y) a):
  • Нормальный порядок: сначала внешний редекс → ((λy. y) a) ((λy. y) a) — аргумент скопировался, и теперь (λy. y) a надо посчитать дважды: → a ((λy. y) a) → a a. Три шага.
  • Аппликативный порядок: сначала аргумент (λy. y) a → a, затем (λx. x x) a → a a. Два шага.

Мораль: аппликативный порядок эффективнее, когда аргумент используется несколько раз (считает один раз вместо N), но зависает там, где аргумент не нужен вовсе. Нормальный порядок находит ответ всегда, когда он есть, но может дублировать работу. Компромисс между ними — вызов по необходимости (call-by-need, ленивость с мемоизацией): считаем аргумент не раньше, чем понадобится, и ровно один раз. Так работает Haskell.

Мини-итог

• Вычисление в лямбда-исчислении — это переписывание текста по трём правилам, а не движение по памяти.
• Альфа переименовывает связанные переменные. Сама по себе бесполезна, но обслуживает бету.
• Бета — единственное правило, которое вычисляет: (λx. M) N → M[x := N]. Это буквально вызов функции.
• Подстановка — место, где живут баги. Три случая: совпадающий связыватель (не идём внутрь), свободная переменная (не трогаем), угроза захвата (сначала альфа).
• Эта — экстенсиональность: λx. f x → f. В чистом исчислении безопасна, в реальных языках (this, лишние аргументы, арность, kwargs) требует проверки.
• Чёрч–Россер: нормальная форма единственна с точностью до альфа. Порядок редукции влияет не на ответ, а на то, найдёте ли вы его.
• Нормальной формы может не быть — и на этом строится рекурсия.

Источники

• H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics — каноническая монография.
• B. Pierce. Types and Programming Languages, гл. 5 — самое читаемое изложение подстановки и редукции (сайт книги).
• Stanford Encyclopedia of Philosophy, The Lambda Calculus — обзор с историческим контекстом.
• Church–Rosser theorem — формулировка и следствия.
• Логическая база (индукция, доказательства свойств редукции) — в курсе Логика и доказательства.

Что дальше

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

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