lambda - Church-Rosser 定理是否适用于按值减少调用？

Question

我一直在研究 lambda 演算，最近看到了 Church-Rosser 定理。该定理指出，当对 lambda 演算中的项应用归约规则时，选择归约的顺序不会对最终结果产生影响（来自 wiki）。但我发现这与按值调用减少和正常订单减少不一致。例如，当遵循正常的降阶规则时，可以将 λ 项 λz.(λx.x) y 减少为 λz.z。但是当使用按值调用减少时，它不能进一步减少，因为按值减少禁止在 λ 抽象内进行减少。因此，术语 λz.(λx.x) y 不能使用不同的规则评估为相同的结果，这似乎与 Church-Rosser 定理相矛盾。这里有什么问题？请帮帮我。非常感谢！

Answer 1

我认为您对 Church-Rosser 定理不精确，这就是造成混乱的原因。

据我所知（我正在用“函数式编程语言的实现”来写这篇文章），这个定理说如下：

如果两个 lambda 表达式 E 和 F 可以通过任何归约序列相互转换，则存在表达式 G，使得 E 和 F 都可以归约为 G。

由此只能得出一个表达式不能有两种不同的范式（尽管可能根本没有范式）。但是，给定两个减少命令，一个可能会导致正常形式，而另一个可能会出现分歧——有些甚至可能会在此之前停止，例如按名称调用。

现在，在您的情况下，E = \z.z它是正常形式，并且F = \z.((\x.x) z)^*可以简化为它；这里唯一可以说的是F不能归结为 以外的任何东西E，而没有说它必须归约多少。

该定理还有另一部分，即如果存在范式，则范式会找到它。同样，与您的观察没有矛盾，因为按值调用和按名称调用最终可能与正常顺序不同。

_{^*我假设你的意思是这个 insted of \z.((\x.x) y)，因为后者没有意义。}