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).