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

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

Если $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}$, — иначе нарушилась бы единственность НФ; так доказываются «неравенства» термов.

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