How to evaluate an expression using β reduction in lambda calculus?

Question

I want to evaluate the following expression:

(λx.y)((λz.zz)(λw.w))

using β reduction .

The answer is:

(λx.y)((λz.zz)(λw.w)) ->
(λx.y)((λw.w)(λw.w)) ->
(λx.y)(λw.w) -> y

But I don't understand the 2nd phase:

From here: (λx.y)((λz.zz)(λw.w)) to here (λx.y)((λw.w)(λw.w))

What are we doing there? From my understanding, I need to use the α-equivalence rule.

Answer 1

Beta reduction allows a term (λx.t)s to be reduced to t[x := s]. In your problem step, x is z, t is zz, and s is λw.w. So here t[x := s] is zz[z := λw.w], which is (λw.w)(λw.w).

Answer 2

The reduction you propose, is reduction by-value.

 (λx.y) z -> y[x/z] IF z is a value.

You could reduce directly to y using the reduction by name

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

To answer your question:

(λx.y)((λz.zz)(λw.w)) -> (λx.y)((λw.w)(λw.w))  

Because

 ( (λz.zz)(λw.w) ) is not a value (as (λx.y)z is never a value.)

And because

  (zz)[z/(λw.w)] i.e.substitute every occurence of z with (λw.w) leads to 

  (λw.w)(λw.w)