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).
UPD: It is not hard to do a CPS in lambda-calculus (details for CBV can be found here). Seems that is not enough for solving the problem.
UPD: If we have some version of quote-eval functions for the pure lambda-calculus, then there must be a function $eq$, which recognizes whether the quoted lambda-expressions are syntactically equal, and we can construct Is0 using $eq$. But I doubt that $eq$ is definable. The reason is "genericity lemma" (Barendregt book, lemma 14.3.24). If we were able to test equality on the quoted lambda-terms then ($eq$ (Quote $\Omega$) (Quote $\lambda x.x$)) would return $False$, and the genericity implies that ($eq$ (Quote $\lambda x.x$) (Quote $\lambda x.x$)) would also return $False$. Does that contradict a possibility of constructing Quote in the pure lambda-calculus?