我如何誤解按需求評估？

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 

如預期的那樣。