如何在lambda演算中使用β減少來評估表達式？

Question

我想評估下式：使用β減少

(λx.y)((λz.zz)(λw.w)) 

。

答案是：

(λx.y)((λz.zz)(λw.w)) -> 
(λx.y)((λw.w)(λw.w)) -> 
(λx.y)(λw.w) -> y 

但我不明白的第二階段：

從這裏：(λx.y)((λz.zz)(λw.w))到這裏(λx.y)((λw.w)(λw.w))

我們在做什麼呢？根據我的理解，我需要使用α等價規則。

Answer 1

Beta縮減允許將一個項（λx.t）s減小到t [x：= s]。在你的問題步驟中，x是z，t是zz，s是λw.w.所以這裏t [x：= s]是zz [z：=λw.w]，它是（λw.w）（λw.w）。

Answer 2

你提出的減少是價值減少。

(λx.y) z -> y[x/z] IF z is a value. 

你可以使用減少的名字

(λx.y) z -> y[x/z]. 

要回答你的問題直接降低Y：

(λx.y)((λz.zz)(λw.w)) -> (λx.y)((λw.w)(λw.w)) 

因爲

((λz.zz)(λw.w)) is not a value (as (λx.y)z is never a value.) 

而且由於

(zz)[z/(λw.w)] i.e.substitute every occurence of z with (λw.w) leads to 

    (λw.w)(λw.w)