按名称呼叫与正常顺序

Question

我知道这个话题已经讨论过好几次了，但我仍然不清楚。 我已经阅读了这个问题applicative-order/call-by-value and normal-order/call-by-name differences，我想一劳永逸地澄清一些事情：

点名

按照正常顺序，但在抽象内部不执行缩减。例如，根据这个策略，λx.(λx.x)x 是范式，尽管它包含 redex (λx.x)x。

在按名称调用中，表达式 λx.(λx.x)x 被称为正常形式；这是因为“（λx.x）x”被认为是主体（因为λ的范围尽可能向右延伸）？等等，如果我应用正常顺序，结果会是什么？

Answer 1

在按名称调用中，表达式 λx.(λx.x)x 被称为正常形式；这是因为“(λx.x)x”被认为是body（因为λ的范围尽可能向右延伸）？

是的，你是对的。

另一方面，如果我应用正常顺序，结果会是什么？

你在体内做归约：(λx.x)x -> x，所以整个事情归约到恒等函数：

λx.(λx.x)x -> λx.x

为了进一步澄清，让我再做一次，renaming 符合Barendregt variable convention 的变量：λx.(λx.x)x =α λx.(λy.y)x：

λx.(λy.y)x -> λx.[y := x](y) = λx.x