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)$?

  • 2
    $\begingroup$ 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. $\endgroup$ – 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.

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).

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)$

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$.

  • $\begingroup$ Why don't we use α conversion to avoid confusion with multiple f and x ? $\endgroup$ – n0unc3 Sep 7 '18 at 23:15
  • $\begingroup$ 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. $\endgroup$ – Sandro Lovnički Sep 7 '18 at 23:30
  • $\begingroup$ 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. $\endgroup$ – n0unc3 Sep 7 '18 at 23:53

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.