丘奇—罗瑟定理

丘奇—罗瑟定理（Church–Rosser theorem）是关于归约路径汇合的结果。这里以无类型λ演算的β归约为对象：λ项由变量、函数抽象λx.M与函数应用M N构成，基本计算步骤把(λx.M)N变成M[N/x]，即将N代入M中x的自由出现。

代入必须避免变量捕获，必要时先给绑定变量改名。λx.x和λy.y因此视为α等价。本文所说的归约允许在项内部选择可归约子项，不预先限定只能按某一种程序语言的求值顺序进行；换用不同演算或加入额外规则时，需要重新确认相应性质。

参考：[1]

用→*表示零步或有限多步β归约。定理说，如果M→*N且M→*P，那么存在Z，使N→*Z且P→*Z。这是合流性：分叉的两边不必当前相同，也不必各走一步就相同，但总能找到共同的进一步结果。

例如M为(λx.x)((λy.y)z)。先归约外层，得到(λy.y)z，再得到z；先归约内层，得到(λx.x)z，再得到z。两条路径在z处汇合。定理将这种现象推广到所有λ项和任意有限归约分叉，而不是仅凭这个例子证明所有情况。

参考：[1]

β正规形是已没有β可归约子项的项。假设同一M能归约到两个正规形N和P，合流性给出共同后继Z。但N、P都不能继续作真正的β步骤，所以只能通过零步到达自身；于是N与P在α等价意义下相同，不能产生两个本质不同的最终答案。

这个结论也有助于理解β等价：允许沿归约与反向展开组成有限链所得到的等价项，可以归约到共同后继。若其中一个已是正规形，另一个能够归约到它。不过，“至多一个正规形”不是“恰好有一个正规形”，更不是一个能对任意输入立即判定等价性的算法。

参考：[1]

令Ω＝(λx.x x)(λx.x x)，对它作β归约仍得到Ω，因此它没有正规形。再考虑(λx.a)Ω，其中a是变量：直接归约外层可得到正规形a；若坚持先反复归约参数Ω，则永远无法完成。这个项有正规形，却存在不终止的归约路径。

因而定理只说明已经发生的有限分叉仍有汇合的可能，不命令执行者一定选择通向汇合点的路径。最左最外的正规序在有正规形时能找到它，是有关归约策略的进一步结果，不能把这一策略保证随意推广到任意策略。带副作用、并发或其他求值规则的实际语言也不能仅凭使用λ记号就继承同样结论。

参考：[2]