Church–Rosser 定理 | Codeboy's Blog

形式陈述

在λ 演算中，完整 β-归约具有合流性。对任意项 $t,u,v$ ，若

t\to_\beta^*u \qquad\text{且}\qquad t\to_\beta^*v,

则存在项 $w$ ，使

u\to_\beta^*w \qquad\text{且}\qquad v\to_\beta^*w.

$\to_\beta^*$ 是一步关系的自反传递闭包，项按α-等价识别。等价的 Church–Rosser 形式是

t=_\beta u \Longrightarrow \exists w.\ t\to_\beta^*w\ \land\ u\to_\beta^*w,

其中 $=_\beta$ 允许正向与反向 β 步。合流性把任意 zig-zag 转换压成朝共同后继前进的两条路径。

经典证明不对普通 β-步直接套局部菱形。它先定义可同时收缩若干 redex 的平行归约 $\Rightarrow$ ，证明每个项的完全展开 $t^\star$ 满足：若 $t\Rightarrow u$ ，则 $u\Rightarrow t^\star$ 。平行归约由此具有菱形性质；再证明 $\to_\beta\subseteq\Rightarrow\subseteq\to_\beta^*$ ，便把合流性传回 β-归约。

直觉

一个项可以有多个 redex，选择不同位置会形成分叉。合流性保证每个有限分叉仍有共同未来，因而归约顺序不会制造两个不可调和的正常答案。

这项保证不含终止量词。标准循环项 $\Omega=(\lambda x.x\,x)(\lambda x.x\,x)$ 可以永远归约而不违背合流性； $(\lambda x.y)\Omega$ 也可以一条路径到 $y$ 、另一条路径一直发散。合流性回答有限结果是否兼容，正规化回答路径是否抵达终点。

同一 λ 项沿不同归约顺序最终汇合，平行归约形成局部菱形 — Church–Rosser 的归约菱形

例子与边界

令

t=(\lambda x.x)\bigl((\lambda y.y)z\bigr).

先收缩外层得到 $(\lambda y.y)z$ ，再得 $z$ ；先收缩参数得到 $(\lambda x.x)z$ ，也再得 $z$ 。两条长度均为两步的路径在 $z$ 汇合。

若 $t\to_\beta^*n_1$ 与 $t\to_\beta^*n_2$ ，且 $n_1,n_2$ 都是正规形，合流性给出共同后继 $w$ 。正规形无后继，只能有 $n_1\equiv_\alpha w\equiv_\alpha n_2$ ，这就是正规形唯一性的完整推导。

合流性还应与局部合流区分。局部合流只处理两个一步分支；在关系强正规化时，Newman 引理可由局部合流推出合流。无类型 β-归约并不强正规化，所以经典证明需要平行归约，不能直接引用 Newman 引理。加入状态写入、异常或其他次序敏感规则后，若临界分支不能汇合，扩展演算也可能失去合流性。

推论与应用

定理使 β-等价具有共同还原性质：若两个项可由 β 转换联系，就能把它们都正向归约到同一项。若两者都有正规形，比较唯一正规形便可证明一部分等价；对不可正规化项，这种方法不会给出判定过程。

标准化定理与合流性互补：前者证明存在正规形时最左最外策略能够找到，后者证明找到的正规形不会与其他路径冲突。传名调用受这一顺序启发，但语言级弱求值和完整正规序仍须区分。

在重写系统与证明论中，Church–Rosser 是更一般的合流性范例；证明化简的顺序独立性、编译优化的局部改写一致性都以类似性质为目标。

参考资料

Henk Barendregt, The Lambda Calculus: Its Syntax and Semantics, revised ed., North-Holland, 1984, Chapter 3。
J. Roger Hindley and Jonathan P. Seldin, Lambda-Calculus and Combinators: An Introduction, Cambridge University Press, 2008, Chapter 4。
Jean-Jacques Lévy, “Réductions correctes et optimales dans le lambda-calcul,” PhD thesis, Université Paris VII, 1978, residuals and developments。

形式陈述 ​

反向链接

形式陈述