HR F#: Lambda Calculus - Reductions #2

The second λ-calculus problem is following:

Reduce the following to no more than one term. If the expression cannot be reduced, enter "CAN'T REDUCE".
((λx.((λy.(x y)) x)) (λz.w))

Let's reduce the expressions:

  1. Framing parentheses are not required: (λx.((λy.(x y)) x)) (λz.w)
  2. Rewrite function body with the argument being substituted with the value: ((λy.((λz.w) y)) (λz.w)).
  3. Remove parentheses again: (λy.((λz.w) y)) (λz.w).
  4. And substitute again: (λz.w) (λz.w).
  5. Performing application gives just "free" variable w.

So the expression ((λx.((λy.(x y)) x)) (λz.w)) can be reduced to just w.