形式陈述

Church–Rosser 定理说明 β-归约具有合流性：若 $t\to_\beta^*u$$t{\to }_{\beta }^{\ast }u$ 且 $t\to_\beta^*v$$t{\to }_{\beta }^{\ast }v$，则存在 $w$$w$ 使 $u\to_\beta^*w$$u{\to }_{\beta }^{\ast }w$ 且 $v\to_\beta^*w$$v{\to }_{\beta }^{\ast }w$。因此若一个项存在 β-正规形，该正规形在 α-等价意义下唯一。定理不保证正规形存在，也不保证任意策略终止。

直觉

不同归约顺序可能暂时分叉，但只要继续归约就能重新汇合；计算结果不会因局部选择而产生两个不同正规终点。

例子与边界

一个项既可先归约外层也可先归约实参，合流性保证可汇合。$\Omega$$\mathrm{\Omega }$ 没有正规形，却不违反定理。加入有副作用或非合流重写规则后，Church–Rosser 结论不能直接沿用，必须重新证明临界对可汇合。

推论与应用

合流性支撑 λ 演算一致的等式理论、重写系统设计和证明助理中的正规化判等。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Parts I–XVIII。
• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chs. 3–30。