Lambda 减少

Question

我无法理解如何将 lambda 项简化为正常形式。有人可以帮我理解如何减少这个 lambda 表达式吗？我不知道从哪里开始。

(λx. ( λa. (λx. x a)) x) 20 (λx. x+3)

提前谢谢你

Answer 1

我只关注你的表情。如需更深入的解释，您可以阅读this question的答案。

首先，让我们考虑如何在这些表达式上解释括号。考虑以下表达式：

(λx. x*x) 5 => 5*5 => 25

所以，这个表达式的评估是用括号外的值 5 替换 x 完成的。

现在，让我们在你的表达式上从左到右放置一些括号：

(((λx. ( λa. (λx. x a)) x) 20) (λx. x+3))

我们把 (λa. (λx. x a)) 称为变量 z 作为简化。所以，我们将有：

(((λx. z x) 20) (λx. x+3))

表达式现在类似于我们的第一个示例。用值 20 替换 x，我们将有：

((z 20) (λx. x+3))

等同于：

(((λa. (λx. x a)) 20) (λx. x+3))

同样，我们可以将 a 替换为 20 结果

((λx. x 20) (λx. x+3))

然后，我们可以将左侧表达式中的 x 替换为右侧的整个表达式 (λx.x+3)。

((λx. x+3) 20)

最后，我们可以将 x 替换为 20：

((λx. x+3) 20) => 20+3 = 23

Answer 2

从左到右替换：

(λx.      ( λa. (λx. x a )) x )  20  (λx. x+3)
~~
([x:= 20] ( λa. (λx. x a )) x )      (λx. x+3)
~~
          ( λa. (λx. x a )) 20       (λx. x+3)
~~
      ( [a:=20] (λx. x a ))          (λx. x+3)
~~
                (λx. x 20)           (λx. x+3)
~~
     ([x:=(λx. x+3)] x 20)
~~
          (λx. x+3)    20
~~
      ([x:=20] x+3)
~~
              20+3

没有更多的归约需要执行，因此这是原始 lambda 项的正常形式。