使用beta减少

我带来了Haskell的书,并与beta减少斗争.

我确实理解这个概念,但不知道,如何使用它,当我在我面前有一个lambda.例如:

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

如何减少它？

1> Willem Van O..：

---

首先:

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

是短的:

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

好吧,给你应用beta减少:

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

(粗体表面添加了"主动"变量可以这么说,斜体替换它)

你这样a用oparand 代替z,现在的结果是:

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

因此,我们替换a通过z在λ表达式的范围,接下来我们执行额外的还原:

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

至:

(? c . c z z) (? w v . w)

现在您还可以使用beta-reduction来注入函数,如下所示:

(? c . c z z) (? w v . w)

成:

((? w v . w) z z)

所以我们还没有结束.因为头部还有一个lambda表达式:

(? w v . w) z z

成:

(? v . z) z

最后这本书证明了头部中的变量不需要体内的变量,因此最后的β减少对身体没有影响(但它删除了最后一个lambda表达式):

(? v . z) z

成:

(z)

要么:

z

Beta减少或多或少是每种函数式编程语言背后的原因:Haskell反复调用beta减少 - 如果需要,因为它是惰性的 - 直到得到的结果值.

---

z (? w v . w)

---

(? w v . w)

---

---

z

---

---

@zero_coding Benjamin Pierce的类型和编程语言是关于该主题的一个非常流行的介绍性文本.