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