# How to reduce Untyped λ-Calculus to Normal Form?

I have an assignment to do which involves reducing an Untyped λ-Calculus expression to Normal Form. I am struggling to come to terms with Lambda Calculus though.

For example, one small part of the expression is:

((λ n f x . n f (f x)) (λ f x . x))


Does this mean that we substitute (λ f x . x) in for every n, f and x? Giving us the following:

((λ n f x . (λ f x . x) (λ f x . x) ((λ f x . x) (λ f x . x))))


If so, can this be reduced further? I know I am probably way off with this, but I just do not understand it; any help would be appreciated.

EDIT: Thanks to @ljedrz Comment.

Before doing the reduction is worth noting that: $$(\lambda n f x . n ~ f (f ~ x)) = (\lambda n f x .((n f) (f ~ x)))$$ This is a convention, the parenthesis always associate to the left

It can be reduced further, but I advise you to change the second expression to an $\alpha$-equivalent one.

$$\Big(\big(\lambda n f x . (n ~ f) (f ~ x) \big) ~ (\lambda h y . y) \Big)$$

This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if some free variables got captured.

\begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) ~ f ~ (f~x) \big)\\ \Big( \lambda f x. \big((\lambda \color{red}{h} y. y) ~ \color{red}{f}\big) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ f \big]\big(\lambda y.y\big) ~ (f ~ x) \Big)\\ \Big( \lambda f x. ((\lambda y. y)) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[y ~ / ~ (f ~ x)\big]y\Big)\\ &\rightarrow_{\alpha} \Big(\lambda f x. (f ~ x) \Big) \end{align*}

Which cannot be reduced further.

• Thank you, I understand most of this, but just at the end when you substitute[h/(f(fx))] Does this just become nothing because there is no h on the right side of the dot? Jan 12 '18 at 13:04
• Yes, in this case this is just a function that consumes it's argument and does nothing, since there's no bound $h$ to actually do the substitution. Jan 12 '18 at 14:18
• @ljedrz Oh yes, these annoying parenthesis. That's what I get for doing directly on LaTeX. I'm going to fix it, thank you for spotting the mistake! Jan 12 '18 at 16:43
• There's a typo, I think. The last $\to_\beta$ should lead to $\lambda f x . [y/fx] y$, without the $\lambda y$. Please check.
– chi
Jan 12 '18 at 23:12

You might find it easier (I do) to practice β-reductions using De Bruijn indices, as they make α-conversions unnecessary and the indices help keep track of the substitution order.

Using them, the reduction (normal order) of your expression would look as follows ($\color{blue}{abstraction\ to\ drop}$, $\color{red}{bound\ variable\ to\ substitute}$, $\color{green}{the\ substitute\ expression}$):

\begin{align} (\color{blue}{λ}λλ\color{red}{3}2(21))\color{green}{(λλ1)}\\ λλ(\color{blue}{λ}λ1)\color{red}{2}(21)\\ λλ(\color{blue}{λ}\color{red}{1})\color{green}{(21)}\\ λλ21 \end{align}