evaluation - 我如何误解按需评估？

Question

首先，我从来没有研究过这些东西或任何东西，所以我可能会问一些非常愚蠢的问题，我很抱歉，但请放轻松:)

我正在使用按需调用评估来实现 lambda 演算。我正在尝试关注有关该主题的这篇论文，其中相关位似乎是第 28 页上描述的自然语义。

无论如何，我对这种评估策略的不理解是，据我所知，实际替换仅在评估变量时发生。抽象对自己进行评估，因为这些是值，并且应用程序只会将新条目添加到缓存中。

但考虑到这一点，一个人究竟如何评估一个像

(λx.λy.x y) λa.a

根据链接论文中描述的自然语义，第一个评估步骤是将条目添加x -> λa.a到缓存中，并在应用程序的 lhs 上评估抽象主体，即λy.x y. 但这是一个值，所以评估结束。此时我们有一个未关闭的术语和一个非空堆。虽然我们确切地知道这个术语应该评估为λy.(λa.a) y。

我有什么误解？这在实际使用这种评估策略的语言中是如何工作的？

Answer 1

你的减法是对的。关键是该论文中提到的按需调用策略只是一个弱策略，因为它永远不会在 lambda 表达式下减少。这在图 1 中很明显，其中表达式 \xM 是一个值。

在归约结束时，如果您想显式获取 lambda 项，您仍然需要展开缓存（文献中通常称为环境），这相当于替换您的项中缓存中的关联：

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

正如预期的那样。