Working with beta reduce

Question

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?

Answer 1

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.