is reducing to normal form simply applying beta-reduction?

Question

See example below:

reduce to normal form:

(λ c . (λ a . (λ d . (λ h . (h (d (a (a (λ z y . y))) (d (a (a (λ f x . x))) (a (a (a (λ z x . x)))))) (h (a (a (λ z y . y))) (a (a (a (λ z x . x))))))) (λ n m . n (d m) (λ z y . y))) (λ n m . n a m)) (λ n z . c (n z) z)) (λ z g x . z (g x))

Wikipedia says that to be in normal form: all reductions that can be applied have been).

I used these two calcualtors to try and get the correct reduction: http://lambda.jimpryor.net/code/lambda_evaluator/ http://lambda.jimpryor.net/code/lambda_evaluator/

both return: λz x.z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z(z x)))))))))))))))))))))))))))))))))))))))))

Can I get to this answer by only using beta-reduction? This is the only reduction I am currently trying to understand but from this example there are two more: https://stackoverflow.com/questions/34140819/lambda-calculus-reduction-steps

Answer 1

Using only $\beta$-reductions is sufficient to get to a normal form if variables are named “correctly”.

What do we mean by that?

Let’s take as an example the term $\lambda x y. x\ y$.
Informally, it is a function that takes two arguments - variables $x,y$ and gives us the application of first argument to the second - $x\ y$. Now we want to apply something to this term, say $$(\lambda x y. x\ y)\ a$$

After we perform the $\beta$-reduction, substituting $a$ for $x$ in our term, we get $\lambda y. a\ y$ and we realize that whatever we substitute for $x$, we should be left with a function that applies it to the input variable $y$.

What if we want to substitute a variable named $y$ for $x$? We would be left with $\lambda y. y\ y$ which is a function that takes a variable and applies it to itself! Not at all the function we thought we would have for any $a$.

This example demonstrates that sometimes $\alpha$-conversion is necessary as a helper tool, and I emphasize the word “conversion” because it is not per se reduction.

---

You could also check my answer on this question that has computation similar in nature to yours and maybe try pLam interpreter to see all the reduction steps with colored terms that go into reductions.