我如何误解按需求评估？

Question

首先，我从来没有研究过这些东西，或任何东西，所以我可能会问很无聊的问题，这我很抱歉，请去容易对我:)

我玩弄实施演算，并根据需求进行评估。我试图按照this paper关于这个问题，其中有关位似乎是第28页上描述的自然语义。

无论如何，我不明白这个评估策略是，据我了解，实际替代只发生在评估变量时。抽象评估自己，因为这些是值，应用程序只会将新条目添加到缓存中。

但考虑到，究竟是如何一个去评价像

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

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

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

Answer 1

你的减少是正确的。关键在于该论文提出的按需呼叫战略只是一个弱策略，从某种意义上说，它不会在lambda表达式下减少。这在图1中很明显，其中表达式\ x.M是一个值。

在缩减结束时，如果您想明确获取lambda项，您仍然需要展开缓存（在文献中经常称为环境），这相当于替代术语内缓存中的关联：

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

如预期的那样。