我一直在学习lambda微积分，最近看到了Church-Rosser定理。该定理指出，当将约简规则应用于lambda演算中的项时，选择约简的顺序对最终结果没有影响(来自wiki)。但我发现这与按值调用约简和正常顺序约简不一致。例如，项λz (λx.x) y可以化简为λz。Z，当遵循正常的降阶规则时。但是，当使用按值调用约简时，它不能进一步减少，因为按值调用约简禁止在λ抽象中进行约简。所以term λz。(λx.x) y不能用不同的规则求出相同的结果，这似乎与Church-Rosser定理相矛盾。这里的问题是什么?请帮帮我。非常感谢!
我认为你对丘奇-罗瑟定理的理解不准确，这就是造成混乱的原因。
就我所理解的(我写这篇文章的时候手边有《函数式编程语言的实现》)，这个定理是这样说的:
由此只能得出一个表达式不能有两种不同的正常形式(尽管可能根本没有正常形式)。然而，给定两个还原命令，一个可能会导致正常形式，而另一个可能会发散——有些甚至可能在此之前停止，例如call-by-name。如果两个表达式E和F可以通过任意约简序列相互转换，则存在一个表达式G，使得E和F都可以约简为G
现在，在你的情况下，E = z.z是正态的，F = z.((x.x) z) *可以化为正态的;这里唯一能说的是F不能被还原成E以外的任何东西，而没有说它必须被还原多少。
这个定理还有另一部分，它说如果一个范式存在，正常的顺序会找到它。同样，这与你的观察没有矛盾，因为按值调用和按名称调用最终可能与正常顺序不同。
*我假设你指的是这个而不是z.((x.x) y)，因为后者没有意义。