Стратегии вычисления: нормальный порядок, аппликативный, ленивость

К этому моменту у нас есть всё, чтобы считать: правила редукции (https://courses.digitable.life/post/lambda-calculus/03-reductions/), числа (https://courses.digitable.life/post/lambda-calculus/05-numerals/), структуры данных (https://courses.digitable.life/post/lambda-calculus/06-pairs-and-lists/) и даже рекурсия без имён (https://courses.digitable.life/post/lambda-calculus/07-recursion-and-y/). Но во всех предыдущих статьях мы жульничали. Мы говорили «сократим вот этот редекс» — и молча выбирали удобный.

А выбор есть. В выражении обычно несколько мест, где можно применить бета-редукцию. Кто-то должен решить, какое из них следующее. Это решение называется стратегией вычисления, и оно не косметическое: от него зависит, завершится ли программа, сколько шагов она сделает и сколько памяти съест.

Эта статья — про то, откуда взялась разница между f(g()) в JavaScript и f (g ()) в Haskell, почему && в вашем языке — не обычная функция, и почему Y-комбинатор из прошлой статьи намертво вешает Python.

Зачем это программисту: три знакомые ситуации

1. Логирование, которое стоит денег.

logger.debug("Состояние: %s", dump_entire_world())

Уровень логирования — INFO, строка не попадёт никуда. Но dump_entire_world() уже вызвана: Python вычислил аргумент до входа в debug. Это аппликативный порядок в чистом виде, и это классический источник тормозов в проде.

2. Условие, которое не может быть функцией.

const result = cond ? heavyA() : heavyB();

Ровно одна из двух функций выполнится. А теперь попробуйте написать myIf(cond, heavyA(), heavyB()) — выполнятся обе, ещё до входа в myIf. В лямбда-исчислении IF — обычная функция (https://courses.digitable.life/post/lambda-calculus/04-booleans/), и она работает как надо. В JavaScript if пришлось делать синтаксической конструкцией. Разница ровно в стратегии вычисления.

3. Бесконечный список, который помещается в память.

В Haskell take 5 [1..] возвращает [1,2,3,4,5]. В Python это itertools.islice(count(), 5) — работает только потому, что генератор ленив. Обычный list(count()) повесит машину.

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

Где вообще есть выбор: редексы

Напомним: редекс (reducible expression) — это подвыражение вида (λx. M) N, то есть абстракция, применённая к аргументу. Бета-редукция превращает его в M[x := N].

Возьмём выражение:

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

Здесь два редекса:

• внешний: (λx. x x) применена к ((λy. y) w);
• внутренний: (λy. y) применена к w.

Можно начать с любого. Формально стратегия — это функция «выражение → какой редекс сокращаем следующим». Два классических варианта:

• Нормальный порядок (normal order) — самый левый, самый внешний (leftmost-outermost) редекс. Сначала подставляем аргумент в тело функции, а уже потом разбираемся, что там за аргумент.
• Аппликативный порядок (applicative order) — самый левый, самый внутренний (leftmost-innermost) редекс. Сначала доводим аргумент до нормальной формы, потом подставляем.

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

Полная раскрутка: один пример, два пути

Считаем (λx. x x) ((λy. y) w) обоими способами. Никаких «очевидно, получаем» — каждый шаг.

Аппликативный порядок

Шаг 1. Самый левый внутренний редекс — это (λy. y) w (внутри него редексов нет). Подставляем y := w в тело y:

(λx. x x) ((λy. y) w)
        ^^^^^^^^^^^  редекс
→  (λx. x x) w

Шаг 2. Теперь один редекс — внешний. Подставляем x := w в тело x x:

(λx. x x) w
→  w w

Итого: 2 шага, результат w w.

Нормальный порядок

Шаг 1. Самый левый внешний редекс — это весь терм целиком. Подставляем x := ((λy. y) w) в тело x x. Обратите внимание: аргумент подставляется невычисленным, и его два вхождения — значит, он копируется:

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

Шаг 2. Теперь два одинаковых редекса. Самый левый — первый:

((λy. y) w) ((λy. y) w)
 ^^^^^^^^^^
→  w ((λy. y) w)

Шаг 3. Остался второй:

w ((λy. y) w)
  ^^^^^^^^^^
→  w w

Итого: 3 шага, результат тот же w w.

Первый вывод: результат совпал, а работа разная. Аппликативный порядок вычислил аргумент один раз до копирования; нормальный скопировал невычисленный аргумент и потом вычислял его дважды. Если бы x встречалась в теле сто раз, нормальный порядок сделал бы сто одинаковых вычислений.

Теорема Чёрча-Россера: результат не зависит от пути

То, что оба пути привели к w w, — не совпадение. Это теорема Чёрча-Россера (свойство конфлюэнтности, confluence), одна из двух главных теорем всей теории:

Если выражение E можно свести к A и к B (разными путями, разным числом шагов), то существует C, к которому можно свести и A, и B.

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

Это огромное обещание для практики. Оно означает, что порядок вычисления в чистом языке — вопрос производительности и завершаемости, но не корректности. Именно на этом свойстве стоит автоматическое распараллеливание чистого кода: раз результат не зависит от порядка, можно считать независимые части одновременно. Подробности о самих правилах редукции — в https://courses.digitable.life/post/lambda-calculus/03-reductions/, а формальная сторона доказательств — в треке по математике (https://courses.digitable.life/post/mathematics/00-overview/).

Важная оговорка. Теорема говорит «если сойдёмся, то в одну точку». Она не говорит «любой путь дойдёт». Один путь может завершиться, а другой — крутиться вечно.

Когда путь имеет значение: бессмертный Ω

Вспомним самоприменение из https://courses.digitable.life/post/lambda-calculus/07-recursion-and-y/:

Ω = (λs. s s) (λs. s s)

Раскрутим. Это редекс: функция (λs. s s), аргумент (λs. s s). Подставляем s := (λs. s s) в тело s s:

(λs. s s) (λs. s s)
→  (λs. s s) (λs. s s)
→  (λs. s s) (λs. s s)
→  ...

Каждый шаг возвращает ровно то же выражение. У Ω нет нормальной формы — это лямбда-исчисленческий эквивалент while (true) {}.

Теперь скормим его функции, которой аргумент не нужен:

(λx. λy. y) Ω

Нормальный порядок. Самый внешний редекс — весь терм. Подставляем x := Ω в тело λy. y. Но x в теле не встречается — значит, Ω просто исчезает:

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

Один шаг, нормальная форма, готово.

Аппликативный порядок. Сначала аргумент. Аргумент — это Ω:

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

До внешнего редекса дело не дойдёт никогда.

Это второе фундаментальное утверждение — теорема о стандартизации:

Если у выражения существует нормальная форма, нормальный порядок редукции её найдёт.

Нормальный порядок называют нормализующей стратегией. Аппликативный — нет. С точки зрения теории вопрос закрыт: нормальный порядок строго лучше.

С точки зрения практики — всё наоборот, и почти все языки мира выбрали аппликативный. Разберёмся, почему.

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

Мы уже видели: подстановка невычисленного аргумента копирует его во все вхождения. Вот пример, где это дорого. Пусть SQ = λn. MUL n n (квадрат), а SLOW — какое-то тяжёлое вычисление, дающее число 5.

Аппликативный порядок:

SQ SLOW
→  SQ 5              (SLOW вычислен ОДИН раз)
→  MUL 5 5
→  25

Нормальный порядок:

SQ SLOW
→  MUL SLOW SLOW     (SLOW скопирован невычисленным)
→  MUL 5 SLOW        (первая копия вычисляется)
→  MUL 5 5           (вторая копия вычисляется ЗАНОВО)
→  25

Обобщение: если аргумент встречается в теле k раз и его вычисление стоит T, нормальный порядок платит O(k · T) вместо O(T). При вложенных вызовах k перемножается — получается экспоненциальный взрыв. Наивный интерпретатор нормального порядка на реальной программе просто ляжет.

Итого — честная таблица компромиссов:

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

Call-by-need: взять лучшее от обоих

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

Такая ячейка называется thunk, а стратегия — call-by-need (вызов по необходимости), она же ленивые вычисления (lazy evaluation).

Ключевые свойства:

• аргумент вычисляется не более одного раза (в отличие от call-by-name);
• аргумент вычисляется только если востребован (в отличие от call-by-value);
• по завершаемости call-by-need эквивалентен call-by-name: он нормализующий.

Расплата — память и предсказуемость. Каждый неразвёрнутый thunk занимает место, и в Haskell это порождает знаменитые space leaks: ленивый аккумулятор в свёртке накапливает цепочку из миллиона отложенных сложений вместо одного числа. Отсюда foldl', seq, BangPatterns и строгие поля в записях — весь арсенал «принудительной строгости».

Вот как выглядит thunk руками — сначала JavaScript:

// Ленивая ячейка: вычисляем не раньше первого обращения и ровно один раз
function lazy(compute) {
  let evaluated = false;
  let value;
  return function force() {
    if (!evaluated) {
      value = compute();
      evaluated = true;   // ставим ПОСЛЕ вычисления: если compute бросит, повторим
      compute = null;     // отпускаем замыкание, чтобы не держать ссылки
    }
    return value;
  };
}

const expensive = lazy(() => {
  console.log("считаю...");
  return 6 * 7;
});

// Здесь ещё ничего не посчитано
console.log("thunk создан");
console.log(expensive()); // "считаю..." → 42
console.log(expensive()); // 42, без пересчёта

Тот же приём в Python:

from typing import Callable, TypeVar, Generic

T = TypeVar("T")

class Lazy(Generic[T]):
    """Thunk с мемоизацией — call-by-need своими руками."""

    __slots__ = ("_compute", "_value", "_done")

    def __init__(self, compute: Callable[[], T]) -> None:
        self._compute = compute
        self._value: T | None = None
        self._done = False

    def force(self) -> T:
        if not self._done:
            self._value = self._compute()
            self._done = True
            self._compute = None  # type: ignore[assignment]
        return self._value  # type: ignore[return-value]


def expensive() -> int:
    print("считаю...")
    return 6 * 7


thunk = Lazy(expensive)
print("thunk создан")   # вычисления ещё не было
print(thunk.force())    # "считаю..." → 42
print(thunk.force())    # 42, без пересчёта

Сложность: создание thunk-а — O(1) времени и O(1) дополнительной памяти на ячейку; первое force — стоимость самого вычисления; каждое последующее — O(1). Ровно этим Haskell отличается от наивного нормального порядка.

Обещанное: как сделать ленивый if на строгом языке

Теперь у нас есть инструмент, чтобы починить пример из начала статьи. Логическое IF из https://courses.digitable.life/post/lambda-calculus/04-booleans/ выглядит так:

TRUE  = λa. λb. a
FALSE = λa. λb. b
IF    = λc. λt. λe. c t e

Раскрутим IF TRUE M N:

IF TRUE M N
→  (λc. λt. λe. c t e) TRUE M N
→  (λt. λe. TRUE t e) M N        (подставили c := TRUE)
→  (λe. TRUE M e) N              (подставили t := M)
→  TRUE M N                      (подставили e := N)
→  (λa. λb. a) M N
→  (λb. M) N                     (подставили a := M)
→  M                             (подставили b := N, b в теле нет)

В нормальном порядке N ни разу не вычислялось — оно просто выброшено на последнем шаге. Это настоящий short-circuit. В аппликативном порядке M и N были бы вычислены на первом же шаге, оба.

Лечение на строгом языке — обернуть ветки в лямбды, то есть вручную превратить значения в thunk-и:

const TRUE  = (a) => (b) => a;
const FALSE = (a) => (b) => b;
const IF    = (c) => (t) => (e) => c(t)(e);

// Строгая версия: обе ветки вычисляются ДО вызова — плохо
const bad = IF(TRUE)(heavyA())(heavyB());

// Ленивая версия: передаём НЕвычисленные ветки, forcing — в самом конце
const good = IF(TRUE)(() => heavyA())(() => heavyB())();
//                    ^^^^^^^^^^^^^^  thunk        ^^ форсируем выбранную ветку

TRUE  = lambda a: lambda b: a
FALSE = lambda a: lambda b: b
IF    = lambda c: lambda t: lambda e: c(t)(e)

# Ветки — нульарные лямбды, то есть thunk-и; вызываем только победившую
good = IF(TRUE)(lambda: heavy_a())(lambda: heavy_b())()

Это не академическое упражнение — это ровно тот приём, которым пользуются все: React.lazy, useMemo(() => expr, deps), Optional.orElseGet(supplier) вместо orElse(value) в Java, logger.debug(() -> msg) в SLF4J 2, Lazy<T> в C# (https://courses.digitable.life/post/csharp/00-overview/). Везде одно и то же: заменяем значение функцией без аргументов, чтобы отложить вычисление.

Слабые стратегии: почему настоящие языки не лезут под λ

Есть ещё одно отличие теории от практики, о котором забывают.

Чистый нормальный порядок редуцирует везде, в том числе внутри тел функций. То есть λx. (λy. y) z он сведёт к λx. z. Реальные языки так не делают: функция — это уже значение, её тело не трогают, пока её не позвали.

Отсюда три уровня «готовности» выражения:

• NF (normal form) — редексов нет нигде, включая тела всех λ.
• HNF (head normal form) — голова выражения уже не редекс, но в аргументах работа могла остаться.
• WHNF (weak head normal form) — снаружи либо λ, либо переменная с аргументами. Что внутри λ — не важно.

Примеры:

λx. (λy. y) x      — WHNF (снаружи λ), но НЕ NF (внутри есть редекс)
(λy. y) x          — не WHNF (снаружи редекс)
x ((λy. y) z)      — WHNF и HNF (голова x — переменная), но не NF
λx. x              — WHNF, HNF и NF одновременно

Практический вывод: когда в JavaScript, Python, OCaml или Haskell говорят «вычислить выражение», почти всегда имеют в виду «довести до WHNF». Поэтому стратегии реальных языков называют слабыми: call-by-value и call-by-name останавливаются, как только снаружи оказалась лямбда. Полная нормальная форма нужна там, где выражения преобразуют символически, — в системах компьютерной алгебры, в частичных вычислителях и в оптимизирующих компиляторах на этапе inline-развёртки.

Интерпретатор: две стратегии в одном коде

Лучший способ убедиться, что разница реальна, — написать обе стратегии и запустить. Ниже — маленький интерпретатор лямбда-исчисления на Python с честной подстановкой без захвата имён (механика — в https://courses.digitable.life/post/lambda-calculus/02-variables-and-substitution/).

from dataclasses import dataclass
from typing import Union

@dataclass(frozen=True)
class Var:
    name: str

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

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

Term = Union[Var, Lam, App]


def free_vars(t: Term) -> set[str]:
    if isinstance(t, Var):
        return {t.name}
    if isinstance(t, Lam):
        return free_vars(t.body) - {t.param}
    return free_vars(t.fn) | free_vars(t.arg)


def fresh(name: str, taken: set[str]) -> str:
    """Подбираем имя, которого ещё нет: x → x', x'' и так далее."""
    while name in taken:
        name += "'"
    return name


def subst(t: Term, x: str, s: Term) -> Term:
    """t[x := s] с переименованием, если иначе связанная переменная захватит свободную."""
    if isinstance(t, Var):
        return s if t.name == x else t
    if isinstance(t, App):
        return App(subst(t.fn, x, s), subst(t.arg, x, s))
    # Lam
    if t.param == x:
        return t                                    # x перекрыт — внутрь не идём
    if t.param in free_vars(s):
        new = fresh(t.param, free_vars(s) | free_vars(t.body))
        body = subst(t.body, t.param, Var(new))     # альфа-конверсия
        return Lam(new, subst(body, x, s))
    return Lam(t.param, subst(t.body, x, s))


def normal_step(t: Term) -> Term | None:
    """Один шаг нормального порядка: самый левый ВНЕШНИЙ редекс."""
    if isinstance(t, App):
        if isinstance(t.fn, Lam):                   # внешний редекс — бьём сразу
            return subst(t.fn.body, t.fn.param, t.arg)
        left = normal_step(t.fn)
        if left is not None:
            return App(left, t.arg)
        right = normal_step(t.arg)
        return App(t.fn, right) if right is not None else None
    if isinstance(t, Lam):                          # лезем под λ — это ПОЛНЫЙ нормальный порядок
        inner = normal_step(t.body)
        return Lam(t.param, inner) if inner is not None else None
    return None


def applicative_step(t: Term) -> Term | None:
    """Один шаг аппликативного порядка: самый левый ВНУТРЕННИЙ редекс."""
    if isinstance(t, Lam):
        inner = applicative_step(t.body)
        return Lam(t.param, inner) if inner is not None else None
    if isinstance(t, App):
        left = applicative_step(t.fn)               # сначала вычислим функцию
        if left is not None:
            return App(left, t.arg)
        right = applicative_step(t.arg)             # затем аргумент — до упора
        if right is not None:
            return App(t.fn, right)
        if isinstance(t.fn, Lam):                   # и только теперь подставляем
            return subst(t.fn.body, t.fn.param, t.arg)
    return None


def run(t: Term, step, limit: int = 100) -> tuple[Term, int, bool]:
    """Возвращает (результат, число шагов, дошли ли до нормальной формы)."""
    for i in range(limit):
        nxt = step(t)
        if nxt is None:
            return t, i, True
        t = nxt
    return t, limit, False

Проверим на нашем (λx. λy. y) Ω:

omega = App(Lam("s", App(Var("s"), Var("s"))),
            Lam("s", App(Var("s"), Var("s"))))
term = App(Lam("x", Lam("y", Var("y"))), omega)

print(run(term, normal_step))       # (Lam('y', Var('y')), 1, True)   — 1 шаг
print(run(term, applicative_step))  # (..., 100, False)               — упёрлись в лимит

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

Сложность самого интерпретатора: subst — O(размер терма) на вызов, free_vars пересчитывается наивно, так что честная реализация кэширует множества свободных переменных или переходит на индексы де Брёйна. Это стандартный приём в промышленных интерпретаторах: он убирает и переименования, и повторные обходы.

Почему Y-комбинатор вешает Python (и как это чинят)

В https://courses.digitable.life/post/lambda-calculus/07-recursion-and-y/ мы вывели комбинатор неподвижной точки:

Y = λf. (λx. f (x x)) (λx. f (x x))

Раскрутим Y F в нормальном порядке:

Y F
→  (λx. F (x x)) (λx. F (x x))              (подставили f := F)
→  F ((λx. F (x x)) (λx. F (x x)))          (подставили x := λx. F (x x))
→  F (Y F)

Дальше нормальный порядок бьёт внешний редекс — то есть заходит внутрь F. И если F — это тело рекурсии с условием, оно на каком-то шаге выберет базовую ветку и внутренняя башня Y F останется неразвёрнутой. Рекурсия завершается.

Теперь то же самое в аппликативном порядке. После второго шага у нас F (что-то). Аппликативный порядок обязан сначала вычислить аргумент — а аргумент (λx. F (x x)) (λx. F (x x)) редуцируется в F ((λx. F (x x)) (λx. F (x x))), то есть снова содержит себя. Раскручивается бесконечная башня F (F (F (...))), до тела F дело не доходит. Стек кончается.

Лечение — тот же трюк, что с ленивым if: обернуть самоприменение в лямбду, чтобы оно стало значением и перестало вычисляться преждевременно. Получается Z-комбинатор (он же call-by-value Y):

Z = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v))

Отличие ровно одно: x x заменено на λv. x x v. Это эта-расширение (обратная эта-редукция из https://courses.digitable.life/post/lambda-calculus/03-reductions/): семантически то же самое, но снаружи теперь лямбда — значит, WHNF, значит, аппликативный порядок останавливается и не раскручивает башню.

// Y — повесит рантайм: RangeError: Maximum call stack size exceeded
const Y = (f) => ((x) => f(x(x)))((x) => f(x(x)));

// Z — работает, потому что (v) => x(x)(v) уже является значением
const Z = (f) => ((x) => f((v) => x(x)(v)))((x) => f((v) => x(x)(v)));

const factStep = (self) => (n) => (n === 0 ? 1 : n * self(n - 1));
console.log(Z(factStep)(5)); // 120

Z = lambda f: (lambda x: f(lambda v: x(x)(v)))(lambda x: f(lambda v: x(x)(v)))

fact_step = lambda self: lambda n: 1 if n == 0 else n * self(n - 1)
print(Z(fact_step)(5))  # 120

Эта-расширение здесь — не косметика, а способ управлять моментом вычисления. Тот же приём вы применяете, когда пишете () => doThing() вместо doThing() в обработчике события.

Как это выглядит в живых языках

Конкретика, которая пригодится завтра:

• Все мейнстримные языки строгие. JavaScript, Python, Java, Go, C#, Rust вычисляют аргументы до вызова. Точнее — это call-by-value поверх ссылок, что для объектов называют call-by-sharing: копируется ссылка, а не объект.
• Операторы &&, ||, ?: — не функции. Они реализованы в синтаксисе именно потому, что функция в строгом языке не может не вычислить аргументы. В Haskell && — обычная библиотечная функция, и это возможно только благодаря лени.
• Python: генераторы и itertools. yield даёт call-by-need по элементам. Но осторожно: значения по умолчанию и аргументы функций строгие, отсюда классическая ловушка def f(x=[]).
• Scala: def f(x: => Int) — параметр по имени, то есть буквально call-by-name (пересчитывается при каждом обращении). lazy val добавляет мемоизацию и даёт call-by-need.
• Swift: @autoclosure автоматически оборачивает аргумент в замыкание — язык сам делает то, что мы выше писали руками.
• Haskell: всё лениво по умолчанию, поэтому существуют бесконечные структуры (fibs = 0 : 1 : zipWith (+) fibs (tail fibs)), но нужны foldl' и seq, чтобы не утечь по памяти.
• JavaScript: Promise — НЕ ленив. new Promise(...) начинает выполнение немедленно; отложенное вычисление — это () => promise или генератор. Частая ошибка при работе с «ленивыми» API.

Подробнее о том, как эти идеи живут в повседневном коде, — в треке по функциональному программированию (https://courses.digitable.life/post/functional-programming/00-overview/).

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

1. Считать, что «ленивый» значит «быстрый». Ленивость экономит на невостребованном, но платит за thunk-и. На массиве из миллиона чисел, который точно нужен целиком, ленивая свёртка проиграет строгой и по времени, и по памяти.
2. Путать call-by-name и call-by-need. Первый пересчитывает при каждом обращении, второй мемоизирует. Scala-шный x: => Int — это call-by-name, и три обращения к x в теле означают три вычисления.
3. Мешать лень с побочными эффектами. Отложенное выражение с print, записью в БД или мутацией выполнится неизвестно когда и, возможно, ноль раз. Именно поэтому ленивые языки чистые.
4. Ждать, что нормальный порядок «дешевле», раз он ничего лишнего не считает. Без мемоизации он дороже: дублирование съедает всю экономию.
5. Забывать про WHNF. В Haskell seq x () доводит x только до WHNF: у списка форсируется головной конструктор, а хвост остаётся thunk-ом. Для полной строгости нужен deepseq.
6. Тащить Y-комбинатор в строгий язык. Нужен Z. Симптом — мгновенное переполнение стека без единой итерации.

Упражнения

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

1. Нормальный порядок: (λx. λy. x) a ((λz. z z) (λz. z z))

(λx. λy. x) a Ω
→  (λy. a) Ω          (подставили x := a)
→  a                  (подставили y := Ω, но y в теле нет — Ω выброшен)

2. Любой порядок: (λf. f (f a)) (λx. x)

(λf. f (f a)) (λx. x)
→  (λx. x) ((λx. x) a)      (подставили f := λx. x, два вхождения)
→  (λx. x) a                (нормальный порядок: внешний редекс, подставили x := (λx. x) a... )

→  (λx. x) a
→  a

3. Посчитайте число шагов для (λx. x x x) ((λy. y) b) в обоих порядках.

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

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

4. Приведите λx. (λy. λz. z) x w к WHNF и к NF. В чём разница?

(λy. λz. z) x w
→  (λz. z) w        (подставили y := x, y в теле не встречается)
→  w                (подставили z := w)

5. Почему AND = λp. λq. p q FALSE в строгом языке не даёт short-circuit и как это исправить?

AND FALSE M
→  (λq. FALSE q FALSE) M
→  FALSE M FALSE
→  (λa. λb. b) M FALSE
→  (λb. b) FALSE
→  FALSE

6. Что вернёт run(term, applicative_step) из нашего интерпретатора для (λx. λy. y) ((λs. s s) (λs. s s)) и почему третий элемент кортежа — False?

Мини-итог

• В выражении обычно несколько редексов; стратегия вычисления — это правило, какой брать следующим.
• Теорема Чёрча-Россера: любые сошедшиеся пути дают один и тот же результат, нормальная форма единственна. Порядок не влияет на корректность.
• Теорема о стандартизации: нормальный порядок (leftmost-outermost) найдёт нормальную форму, если она есть. Аппликативный может зациклиться там, где нормальный завершается.
• Практика выбрала аппликативный порядок: он предсказуем по времени, памяти и порядку эффектов, а нормальный дублирует работу — до экспоненты.
• Call-by-need = нормальный порядок + мемоизация в thunk-ах. Даёт завершаемость нормального порядка и «не более одного раза» аппликативного, ценой памяти и space leaks.
• Реальные языки останавливаются на WHNF, а не на полной нормальной форме: под λ никто не лезет.
• Лень на строгом языке делается руками: () => expr в JS, lambda: expr в Python, => T в Scala, @autoclosure в Swift. Тем же приёмом Y-комбинатор превращается в Z-комбинатор.

Источники

• Benjamin C. Pierce, Types and Programming Languages, гл. 5 — call-by-value, call-by-name и формальные операционные семантики: https://www.cis.upenn.edu/~bcpierce/tapl/
• Henk Barendregt, The Lambda Calculus: Its Syntax and Semantics — канонический источник по Чёрчу-Россеру и теореме о стандартизации: https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/103
• John Launchbury, A Natural Semantics for Lazy Evaluation (POPL 1993) — формализация call-by-need с разделением thunk-ов: https://dl.acm.org/doi/10.1145/158511.158618
• Simon Peyton Jones, The Implementation of Functional Programming Languages — как ленивость реализуют в компиляторе: https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/
• Haskell Wiki, Lazy evaluation и Weak head normal form: https://wiki.haskell.org/Lazy_evaluation
• Scala docs, by-name parameters: https://docs.scala-lang.org/tour/by-name-parameters.html

Что дальше

Мы разобрались, как считать. Осталось понять, как заранее отсекать выражения, которые считать бессмысленно, — например, (λx. x x), порождающее Ω. Ответ на это — типы: они запрещают часть выражений и заодно, неожиданным образом, оказываются логическими утверждениями.

Типизированное лямбда-исчисление и соответствие Карри-Ховарда