# How does this addition for Church numerals work with Y combinator?

I am currently preparing for an exam. In one of the old exams, you have to create a $\lambda$ expression $add$ that can add two church numerals. But the church numerals are not the usual ones, but defined like this:

\begin{align} s_0 &= &\lambda x.\ x\\ s_1 &= &\langle c_{false}, s_0 \rangle\\ s_2 &= \langle c_{false}, s_1 \rangle &= \langle c_{false}, \langle c_{false}, s_0 \rangle \rangle\\ s_3 &= \langle c_{false}, s_2 \rangle &= \langle c_{false}, \langle c_{false}, \langle c_{false}, s_0 \rangle \rangle \rangle\\ \dots \end{align}

where

\begin{align} \langle x, y \rangle &= \lambda p. \ p\ x\ y \text{ (pairs)}\\ c_{true} &= \lambda t.\ \lambda f.\ t\\ c_{false} &= \lambda t.\ \lambda f.\ f\\ \text{succ} &= \lambda n. \langle c_{false}, n \rangle\\ \text{pred} &= \lambda n.\ n\ c_{false}\\ \text{isZero} &= \lambda n.\ n\ c_{true}\\ Y &= \lambda f.\ (\lambda x.\ f\ (x\ x))\ (\lambda x.\ f\ (x\ x)) \end{align}

## The solution

They give the solution:

\begin{align} \text{Add} &= \lambda \text{add}.\ \lambda m.\ \lambda n.\ (\text{isZero } m)\ n\ (\text{succ }\ (\text{add}\ (\text{pred}\ m)\ n)\\ \text{add} &= Y\ \text{Add} \end{align}

Where $Y$ is the Y combinator.

## Question

I don't understand this answer. I can't even exactly point out what I don't understand. One problem is certainly the Y combinator. Can somebody eventually break it down to easier pieces and explain it to me?

Eventually an example ($s_0 + s_0$, $s_1 + s_0$, $s_1 + s_1$, $s_2 + s_1$) would also help.

## What I understand

I think I understood everthing above "the solution". So I understand that the number is simply how often you build pairs of $\lambda x.\ x$ and $c_{false}$. I understand that $succ$ only wraps its argument in another pair and $pred$ only returns the second part of such a pair.

## Examples

### 0 + 0

\begin{align} 0+0 &= \text{add } s_0\ s_0\\ &= (Y\ Add)\ s_0\ s_0\\ &= (\lambda f.\ (\lambda x.\ f\ (x\ x))\ (\lambda x.\ f\ (x\ x)))\ Add\ s_0\ s_0\\ &= (\lambda x.\ Add\ (x\ x))\ (\lambda x.\ Add\ (x\ x))\ s_0\ s_0\\ &= (Add\ ((\lambda x.\ Add\ (x\ x))\ (\lambda x.\ Add\ (x\ x))))\ s_0\ s_0 \end{align}

Is that correct? It seems to me as if I did something wrong there.

• Have you tried working through an example? Maybe adding 0+0, or 0+1, etc.? You should be able to apply the reduction rules you know for the lambda calculus to work out what you get for each of those cases, and work it out by hand. – D.W. Sep 13 '14 at 20:04
• @D.W.: The problem is that I don't even know what $add\ s_0\ s_0 = Y Add\ s_0\ s_0$ would be. – Martin Thoma Sep 13 '14 at 20:26
• Do you know the definition of Y combinator? Do you know how to apply reduction rules to a lambda calculus term? Sounds like your question is more basic: you are looking to learn how to evaluate lambda calculus terms by hand, i.e., how to apply the reduction rules by hand -- which has nothing to do with this particular definition of Church numerals. Is that right? If so, what studying have you done to learn this? There's lots of basic material on the lambda calculus out there. – D.W. Sep 13 '14 at 21:28
• @D.W. I've added the definition of the Y combinator. I tried $add\ s_0\ s_0$, but it seems to me that I did something wrong there. Can you help me? – Martin Thoma Sep 14 '14 at 10:00
• Hint: $\forall f. Y f = f (Y f)$ – Pseudonym Sep 14 '14 at 13:15