1

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

点名

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

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

4

1 回答 1

1

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

是的你是对的。

等等，如果我应用正常顺序，结果会是什么？

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

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

为了进一步澄清，让我再做一次，重命名变量以符合Barendregt 变量约定: λx.(λx.x)x =α λx.(λy.y)x:

λx.(λy.y)x -> λx.[y := x](y) = λx.x
于 2016-07-06T09:26:13.017 回答