# lambda calculus with church numerals

today I found this term in our exercises: ((^fx.f(f(f x)) ^gy.g(g y )) ^z.z + 1) (0)

I am quit unaware how to solve this type of question. I know this is the church numeral 3 , 2 , the identity function +1 and zero. But for my understanding it lacks an operator like +-*/ as ex.

(λmn.m (succ n)) to connect two church numerals?

Some hints will be greatly appreciated.

• What does it mean to 'solve' this exercise? What do you want to do with this term? – Discrete lizard Apr 23 '19 at 16:10

Your term is the application $$3\ 2\ succ\ 0$$, where $$succ$$ is the successor function.

If you task is to reduce this term to a beta normal form:

First we can observe that for terms $$M$$ and $$N$$, the application $$MN$$ beta-reduces to the $$M$$-fold application of $$N$$, which is

• in the case of $$N$$ an operation: the $$M$$-fold application of the operation $$N$$ to whatever term $$P$$ the term $$MN$$ is applied to; i.e., $$MNP$$ is $$\underbrace{N(N(...N(}_{M\text{ times}} P)))$$,
• in the case of $$N$$ a church number: the (church number representation of the) exponentiation of $$N$$ with $$M$$; i.e, $$MN$$ with $$M,N$$ numbers is $$N^M$$.

as you can easily verify with simple numbers like $$2$$ and $$3$$.

So $$3\ 2$$ is $$2^3$$, which beta-reduces to $$8$$, and $$3\ 2\ succ$$ creates an 8-fold application of $$succ$$, which is then applied to $$0$$.
So your term is the $$2^3$$-fold = $$8$$-fold application of the $$succ$$-function to the number $$0$$, that is, $$\underbrace{succ(succ(...succ(}_{8 \text{ times}} 0)))$$, which eventually beta-reduces to the church number $$8$$, $$\lambda fx.f(f(f(f(f(f(f(f(x))))))))$$.

Essentially your term is the application $$3\ 2\ {\sf succ}\ 0$$. So we start performing beta reduction steps. Since $$3\ f\ x = f(f(f x))$$, we get $$2\ (2\ (2\ {\sf succ}))\ 0$$. From here, we get $$(2\ (2\ {\sf succ}))\ ((2\ (2\ {\sf succ}))\ 0)$$. And so on -- I'll leave the steps to you.

If I see correctly, after a long-ish sequence of beta steps we should reach the numeral $$8$$ as a normal form. Try checking that $$(2\ (2\ {\sf succ}))\ 0 = 4$$, and after that check that $$(2\ (2\ {\sf succ}))\ 4 = 8$$.