lambda - 如何在 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.

您可以使用按名称归约直接归约为 y

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

要回答您的问题：

(λ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)