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.

| cite | improve this answer | |
  • $\begingroup$ 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? $\endgroup$ – daveyjones Jan 12 '18 at 13:04
  • $\begingroup$ 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. $\endgroup$ – Aristu Jan 12 '18 at 14:18
  • $\begingroup$ @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! $\endgroup$ – Aristu Jan 12 '18 at 16:43
  • 1
    $\begingroup$ 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. $\endgroup$ – 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}

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.