使用beta減少

Question

我帶來了Haskell book並與beta減少鬥爭。

我理解這個概念，但不知道，如何使用它，當我有一個拉姆達在我面前。 例如：

(λ a b c . c b a) z z (λ w v . w) 

如何減少？

Answer 1

首先：

(λ a b c . c b a) z z (λ w v . w)

是短期的：

(λ a . (λ b . (λ c . c b a))) z z (λ w . (λ v . w))

好給你申請的β-減少上：

(λ a b c . c b a) z z (λ w v . w)

（黑體字添加了 「活性」變量可以這麼說，斜體替換）

你因此與oparand取代az所以，現在的結果是：

(λ b c . c b z) z (λ w v . w)

所以我們在lambda表達式的範圍取代a通過z，接下來我們執行額外的減少：

(λ b c . c b z) z (λ w v . w)

到：

(λ c . c z z) (λ w v . w)

現在你也可以使用β受體減少到入功能如這裏演示：

(λ c . c z z) (λ w v . w)

分爲：

((λ w v . w) z z)

因此，我們還未結束。因爲再沒有在頭一個lambda表達式：

(λ w v . w) z z

到：

(λ v . z) z

終於本書表明，在頭一個變量不需要在體內的變量，所以最後的β-減少對身體沒有影響（但它消除了最後λ-表達）：

(λ v . z) z

成：

(z)

或：

z 

測試版減少是多了還是少了什麼是每個函數式編程語言背後：哈斯克爾重複調用的β減少 - 如果需要的話，因爲它是懶惰 - 直到結果值的。