I am trying to solve the following exercise given here.

Consider the following number representation. How to define the addition?

```
|0| = λx.x
|1| = λx.λx.x
...
|n + 1| = λx.|n|
```

The successor and predecessor operators are easy to define:

```
Succ n = λx.n
Pred n = n λx.x
```

An “obvious” solution for defining the addition is to use the successor operation plus the test for zero together with the fixed point combinator, something like **(Y F)** for **F** given below (the operator **if** and booleans are defined as usual):

```
F = λf.(λm n. if (Is0 m) n (Succ (f (Pred m) n))
```

But defining **Is0** seems non-trivial. The problem is that a numeral **|N|** consumes N+1 arguments, and N arguments are simply erased by it. Hence, if I apply such a function, it seems reasonable to stop its application when it becomes clear that the numeral, e.g. is not an identity. I guess it is some sort of continuation, but I cannot imagine how to model it in the pure lambda-calculus. Maybe someone knows any tips that may help?

A sequencing operator can also help to define the addition. If an application of a numeral **|m|** is delayed until a numeral **|n|** is applied to *all* its arguments, the result will be exactly a numeral **|n+m|**. Maybe there exists a variant of such a sequencing combinator in the pure lambda-calculus?

The answer which is provided by the author of the exercise uses a non-pure operation (namely, **IsProcedure** which checks whether its argument is a function).