# Reducing lambda expression to normal form

Can someone explain the steps to reduce $$(\lambda n. \lambda m. \lambda f. \lambda x.\ n\ (m\ f)\ x)\ (\lambda f. \lambda x.\ f\ (f\ x))\ (\lambda f. \lambda x.\ f\ x)$$ to $\lambda y. \lambda z.\ y\ (y\ z)$?

• You should explain what you understand and what you don't, where are you stuck and why. I posted an answer, but you can expect not to get one in this community for "give me a solution" questions. – Sandro Lovnički Sep 5 '18 at 22:02

$\lambda$-calculus is a rewriting system, but it's power to express all partial recursive functions makes it equivalent to Turing machines, in the sense that it is a universal model of computation. Means of computation in $\lambda$-calculus are conversions and reductions, of which the main ones are $\beta$-reduction and $\alpha$-conversion. You can learn a lot about $\lambda$-calculus on Wikipedia alone.

$\alpha$-conversion
Take for example $\lambda$-expressions $(\lambda x. x)$ and $(\lambda y. y)$. We say they are $\alpha$-equivalent because they clearly represent the same function. In short, we can rename variables (and sometimes have to).

$\beta$-reduction
This relation is the one that "gives life" to $\lambda$-expressions and reduces them to normal forms. We use $\beta$-reduction on terms of the form $(\lambda x. M)\ N$, i.e. when applying abstraction to some term $N$, and we call that construction a redex. What this expression becomes after $\beta$-reduction is written $M[x:=N]$ and it means that we replaced all free occurrences of $x$ in $M$ with $N$. For example: $$(\lambda x. x\ x)\ N \rightarrow_\beta N\ N$$

We will be reducing leftmost outermost redex in each step. This strategy garantees that we will get to normal form if it exists.

Now let us dive into this...
Let's find a leftmost outermost redex (underlined) in your expression: $$\underline{\Bigl(\lambda n.\lambda m.\lambda f.\lambda x. n\ (m\ f)\ x\Bigr)\ \Bigl(\lambda f. \lambda x. f\ (f\ x)\Bigr)}\ (\lambda f. \lambda x. f\ x)$$

We have $\Bigl(\lambda n.\lambda m.\lambda f.\lambda x. n\ (m\ f)\ x\Bigr)$, which is an abstraction (it is of the form $\lambda n. M$), that is applied to $\Bigl(\lambda f. \lambda x. f\ (f\ x)\Bigr)$, so ($\beta$-reduction) we have to replace all free occurences of $n$ in $M$ with $\Bigl(\lambda f. \lambda x. f\ (f\ x)\Bigr)$. We get $\biggl(\lambda m.\lambda f.\lambda x. \Bigl(\lambda f. \lambda x. f\ (f\ x)\Bigr)\ (m\ f)\ x\biggr)$, so entire expression is now (where I already underlined next outermost redex): $$\underline{\biggl(\lambda m.\lambda f.\lambda x. \Bigl(\lambda f. \lambda x. f\ (f\ x)\Bigr)\ (m\ f)\ x\biggr)\ (\lambda f. \lambda x. f\ x)}$$ We now have to substitute $(\lambda f. \lambda x. f\ x)$ for $m$ in $\biggl(\lambda f.\lambda x. \Bigl(\lambda f. \lambda x. f\ (f\ x)\Bigr)\ (m\ f)\ x\biggr)$ and get $$\lambda f.\lambda x. \underline{\Bigl(\lambda f. \lambda x. f\ (f\ x)\Bigr)\ \Bigl((\lambda f. \lambda x. f\ x)\ f\Bigr)}\ x$$ Now just keep reducing $$\lambda f.\lambda x. \underline{\Bigl(\lambda x. ((\lambda f. \lambda x. f\ x)\ f)\ (((\lambda f. \lambda x. f\ x)\ f)\ x)\Bigr)\ x}$$ $$\lambda f.\lambda x. \Bigl(\underline{(\lambda f. \lambda x. f\ x)\ f}\Bigr)\ \biggl(\Bigl((\lambda f. \lambda x. f\ x)\ f\Bigr)\ x\biggr)$$ $$\lambda f.\lambda x. \underline{(\lambda x. f\ x)\ \biggl(\Bigl((\lambda f. \lambda x. f\ x)\ f\Bigr)\ x\biggr)}$$ $$\lambda f.\lambda x. f\ \biggl(\Bigl(\underline{(\lambda f. \lambda x. f\ x)\ f}\Bigr)\ x\biggr)$$ $$\lambda f.\lambda x. f\ \Bigr(\underline{(\lambda x. f\ x)\ x}\Bigr)$$ $$\lambda f.\lambda x. f\ (f\ x)$$ And now, if you are still alive, remember $\alpha$-equivalence. We can change the names of variables, say $f$ to $y$ and $x$ to $z$, and obtain your wanted solution.

What have we computed?
We computed that $2 \cdot 1 = 2$, in $\lambda$-calculus using Church numerals:

• $c_0 = \lambda f. \lambda x. x$
• $c_1 = \lambda f. \lambda x. f\ x$
• $c_2 = \lambda f. \lambda x. f\ (f\ x)$
$\vdots$

Expression $\lambda n.\lambda m.\lambda f.\lambda x. n\ (m\ f)\ x$ is the multiplication operator, and other two expressions (on which this operator was applied) are Church numerals for $2$ and $1$.

• Why don't we use α conversion to avoid confusion with multiple f and x ? – n0unc3 Sep 7 '18 at 23:15
• Where exactly? If you want to rename, for example, all $f$s in some expression, yes. It's a cool idea if you are doing a lot of these tasks manually. – Sandro Lovnički Sep 7 '18 at 23:30
• The reason I was getting confused was because of three different f and three different x so I renamed them to a,b,p and q. – n0unc3 Sep 7 '18 at 23:53