使用beta减少(Working with beta reduce)

使用beta减少(Working with beta reduce)

我带来了Haskell书，并与beta版本进行了斗争。

我理解这个概念，但不知道，如何使用它，当我有一个lambda在我面前。 例如：

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

如何减少它？

I brought the Haskell book and struggle with beta reduce.

I do understand the concept but do not know, how to use it, when I have a lambda in front of me. For example:

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

How to reduce it?

最满意答案

首先：

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

（可以这么说，用于“活动”变量的粗体字以及用于替换的斜体字）

你因此用oparand z代替a ，现在结果是：

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

所以我们在lambda表达式的范围内替换a by，接下来我们执行了额外的减少：

(λ 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减少 - 如果需要，因为它是惰性的 - 直到得到的结果值。

First of all:

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

is short for:

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

Well given you apply beta-reduction on:

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

(boldface added for the "active" variable so to speak, and italics for its replacement)

you thus replace a with the oparand z so, now the result is:

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

So we replaced a by z in the scope of the lambda expression, next we perform an additional reduction:

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

to:

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

Now you can also use beta-reduction to inject functions as is demonstrated here:

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

Into:

((λ w v . w) z z)

So we have not ended yet. Because again there is a lambda expression in the head:

(λ w v . w) z z

into:

(λ v . z) z

and finally the book demonstrates that a variable in the head does not need a variable in the body, so the last beta-reduction has no effect on the body (but it removes the last lambda-expression):

(λ v . z) z

into:

(z)

or:

z

Beta reduction is more or less what is behind every functional programming language: Haskell calls the beta-reduction repeatedly - if needed, since it is lazy - until the resulting value is derived.