Теорема Чёрча — Россера

Все дороги ведут в Рим. Точно? На это есть теорема Чёрча — Россера, которая гарантирует единственность нормальной формы, какими бы путями мы к ней ни шли. Конечно, надо заметить, что в Тьюринг-полном языке мы можем такой нормальной формы и не достичь, но вот если достигаем, то она единственна, то есть каким путём ни иди, всегда придёшь именно в Рим.

Если $M$ $\twoheadrightarrow_\beta N$ и $M$ $\twoheadrightarrow_\beta K$, то найдётся $L$ такой, что $N$ $\twoheadrightarrow_\beta L$ и $K$ $\twoheadrightarrow_\beta L$. Иначе говоря, $\twoheadrightarrow_\beta$ обладает свойством ромба (сходимостью):

Доказательство удобно вести через параллельную редукцию. Нам понадобятся три оператора редукции над термами:

• $\to_\beta$ — обычная, одношаговая β-редукция: $M$ $\to_\beta N$ значит, что в $M$ выбрали ровно один редекс и стянули его (один шаг — один редекс);
• $\Rightarrow$ — параллельная редукция: $M$ $\Rightarrow N$ значит, что стянули произвольный набор редексов, уже присутствующих в $M$ (нуль, один, два — сколько угодно), каждый не более одного раза, и только имеющиеся, а не их будущие копии;
• $\twoheadrightarrow_\beta$ — многошаговая редукция (рефлексивно-транзитивное замыкание $\to_\beta$): $M$ $\twoheadrightarrow_\beta N$ значит, что есть цепочка $M$ $\to_\beta \dots$ $\to_\beta N$ любой длины, в том числе нулевой.

Одношаговая редукция — частный случай параллельной, а та — частный случай многошаговой:

Почему свойство ромба не доказывается прямо для одношаговой редукции $\to_\beta$ (рис. 1.1, а)? Мешает копирование редексов. Возьмём терм, в котором два редекса — внешний и внутренний:

Стянем внешний редекс — внутренний при подстановке удвоится: получим $\bigl((\lambda y.y)\,z\bigr)\,\bigl((\lambda y.y)\,z\bigr)$. Стянем внутренний — получим $(\lambda x.x\,x)\,z$. Пути разошлись на один шаг, а вот сойтись за один шаг уже не могут: из второго терма $z\,z$ получается сразу, а из первого — только за два шага, по шагу на каждую копию. Значит, одношаговое свойство ромба для $\to_\beta$ попросту ложно.

Параллельная редукция $\Rightarrow$ лечит ровно эту болезнь: размножившиеся копии редекса она стягивает все разом, за один тик. Для неё свойство ромба уже верно (рис. 1.1, б), и доказывается оно приёмом Такахаси — через полную развёртку.

Полной развёрткой $M^{*}$ назовём терм, в котором одновременно стянуты все редексы, видимые в $M$, — самый жадный из возможных параллельных шагов. Определение — индукцией по строению терма:

Первое правило: $x^{*}$ $= x$ — переменная развёртывается в себя.

Второе правило: $(\lambda x.P)^{*}$ $= \lambda x.P^{*}$ — развёртка проходит под абстракцию.

Третье правило: $(P\,Q)^{*}$ $= P^{*}\,Q^{*}$, если $P\,Q$ — не редекс ($P$ — не абстракция): части развёртываются независимо.

Четвёртое правило: $\bigl((\lambda x.P)\,Q\bigr)^{*}$ $= P^{*}[x\!:=\!Q^{*}]$ — сам редекс стягивается, а его части ещё и развёртываются.

Развернём терм из контрпримера по этим правилам:

• $\bigl((\lambda x.x\,x)\,((\lambda y.y)\,z)\bigr)^{*}$ $= (x\,x)^{*}[x\!:=\!((\lambda y.y)\,z)^{*}]$ — весь терм есть редекс, работает четвёртое правило: внешний редекс стянут, обе его части ушли в развёртку;
• $(x\,x)^{*}$ $= x^{*}\,x^{*}$ $= x\,x$ — применение $x\,x$ — не редекс: третье правило, затем первое для каждой переменной;
• $((\lambda y.y)\,z)^{*}$ $= y^{*}[y\!:=\!z^{*}]$ $= y[y\!:=\!z]$ $= z$ — внутренний редекс: четвёртое правило, затем дважды первое;
• $(x\,x)[x\!:=\!z]$ $= z\,z$ — осталось выполнить подстановку.

Итого $M^{*}$ $= z\,z$: развёртка стянула и внешний редекс, и внутренний — ещё до того, как тот успел размножиться. Всю конструкцию держит лемма о треугольнике.

Лемма о треугольнике. Полную развёртку нельзя обогнать: каким бы ни был параллельный шаг $M$ $\Rightarrow N$, из $N$ ровно один параллельный шаг ведёт в $M^{*}$:

Параллельный шаг не обязан стягивать все редексы — из одного $M$ шаги $\Rightarrow$ ведут в целый веер термов, и полная развёртка — лишь крайняя, самая жадная точка этого веера. Поэтому шаг $N$ $\Rightarrow M^{*}$ в общем случае настоящий; нулевым он оказывается, только когда всё уже стянуто и $N$ $= M^{*}$.

Редукция, которая сразу стягивает все видимые редексы одним разом, называется редукцией Гросса — Кнута $M$ $\Rightarrow_{\mathrm{GK}} M^{*}$. Но она нам неинтересна: в ней нет никакой вариативности — из терма такой шаг ведёт ровно в один результат. А теорема Чёрча — Россера как раз про вариативность: пути $\twoheadrightarrow_\beta$ стягивают редексы в произвольном порядке, и в жёсткие шаги Гросса — Кнута их не разложить. Нужна именно свобода стягивать любое подмножество.

Свойство ромба из треугольника получается очевидно. Пусть $M$ $\Rightarrow N$ и $M$ $\Rightarrow K$. По лемме о треугольнике $N$ $\Rightarrow M^{*}$ и $K$ $\Rightarrow M^{*}$ — берём $L$ $= M^{*}$, и обе стороны замыкаются одним шагом (рис. 1.2, справа). Общая точка одна на всех: она не зависит ни от $N$, ни от $K$.

Осталось поднять свойство ромба с одного параллельного шага на многошаговую редукцию (рис. 1.1, в). Вложения (1.32)$\displaystyle {\to_\beta}$ $\displaystyle \subseteq {\Rightarrow}$ $\displaystyle \subseteq {\twoheadrightarrow_\beta}$ позволяют читать любую цепочку $\to_\beta$-шагов как цепочку $\Rightarrow$-шагов и наоборот. Поэтому распишем $M$ $\twoheadrightarrow_\beta N$ и $M$ $\twoheadrightarrow_\beta K$ как две цепочки параллельных шагов, выложим их по сторонам сетки и достроим её клетка за клеткой — каждую клетку замыкает свойство ромба для $\Rightarrow$.

Заполнив всю сетку, в нижней вершине получаем терм $L$, в который сходятся обе цепочки. Все рёбра сетки — параллельные шаги, а ${\Rightarrow}$ $\subseteq {\twoheadrightarrow_\beta}$, поэтому $N$ $\twoheadrightarrow_\beta L$ и $K$ $\twoheadrightarrow_\beta L$. Теорема Чёрча — Россера доказана.

Из теоремы Чёрча — Россера (1.31)$\displaystyle M$ $\displaystyle \twoheadrightarrow_\beta N,\;\; M$ $\displaystyle \twoheadrightarrow_\beta K \;\;$ $\displaystyle \Longrightarrow\;\; \exists L:\; N$ $\displaystyle \twoheadrightarrow_\beta L,\;\; K$ $\displaystyle \twoheadrightarrow_\beta L$ сразу вытекает существование общего редукта: если $M$ $=_\beta N$, то найдётся $L$ с $M$ $\twoheadrightarrow_\beta L$ и $N$ $\twoheadrightarrow_\beta L$ (индукция по определению $=_\beta$). Отсюда единственность нормальной формы: у терма не больше одной β-НФ — два пути сошлись бы к общему $L$, а НФ дальше не редуцируется, поэтому $N_1$ $\equiv L$ $\equiv N_2$. Далее, редуцируемость к НФ: если $N$ — нормальная форма $M$, то $M$ $\twoheadrightarrow_\beta N$ (а не просто $M$ $=_\beta N$). Наконец, непротиворечивость: разные нормальные формы не β-равны — например $\mathrm{true}$ и $\mathrm{false}$, — иначе нарушилась бы единственность НФ; так доказываются «неравенства» термов.

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