在lambda微積分值中調用

Question

我正在通過Types and Programming Languages進行工作，而針對按價值降低策略調用的皮爾斯給出了術語id (id (λz. id z))的示例。內部redex id (λz. id z)首先減少爲λz. id z，在外部redex減少爲正常形式λz. id z之前，由於第一次減少而給出id (λz. id z)。

但是，按價值順序調用的定義是'只有最外面的索引被減少'，'只有右手邊已經減少到一個值時索引才被減少'。在示例中，id (λz. id z)出現在最外面的redex的右側，並且被縮小。這是如何與只有最外層redexes減少的規則平方？

「最外層」和「最內層」僅僅是指lambda抽象的答案嗎？所以對於一個術語t在λz. t,t不能被減少，但是在一個redex s t,t減小到v如果這是可能的話，然後s v減少？

Answer 1

簡答：是的。你不能在一個lambda期限內減少，你只能從右邊開始減少外部期限。按名稱

E = [ ] | (λ.t)E | Et 

E是你可以看重的是什麼..

例如，在演算評估上下文是：

該集由值拉姆達演算評估上下文的定義如下：

E = [ ] | Et | fE 

因爲即使術語不是價值，您也可以減少應用程序。 例如(λx.x)(z λx.x)卡在價值調用中，但在通話中按名稱減少到(z λx.x)，這是一種正常形式。
在上下文語法f是正常的形式（按名稱調用）定義爲：在皮爾斯的19.5.3章節

f = λx.t | L 
L = x | L f 

你可以看到背景的另一種定義。

Answer 2

「最外」和「最內」只是指lambda抽象的答案嗎？所以對於λz中的t項。 t，t不能被減少，但是在redex s t中，如果這是可能的話，t減小到一個值v，那麼s v就減少了？

是的，這是完全正確的。