Sequencing or continuation-passing in pure lambda-calculus

Question

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?

Answer 1

I do not think you will find what you are looking for in the pure lambda calculus. The key is this statement you made:

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

Well, models of the lambda calculus are supposed to be like:

$$U \cong U^U$$

And the point of this is that every semantic value $u \in U$ may be applied to something. So it makes no sense to talk about something being "applied to all its arguments." There is no value that cannot be applied to more arguments in the pure lambda calculus.

I don't know off hand of a model/argument that this representation of naturals makes it impossible to implement IsZero, although some thinking about it makes it seem unlikely. However, if it is to be possible in the pure lambda calculus, it will have to make sense semantically, and not be based on notions that are only syntactic.

Edit: here is a sketch of an argument. A definition of $\mathsf{IsZero}$ must eventually reduce like:

$$\mathsf{IsZero}\ n \rightsquigarrow^* n \overrightarrow v$$

The reason is that applying to some number of values is the only mechanism in the lambda calculus to actually distinguish between numerals. It needs to be the case that: $$0 \overrightarrow v = \mathsf{true} \\ \mathsf{s}n \overrightarrow v = \mathsf{false}$$ However, for every $\overrightarrow v$ it is the case that: $$||\overrightarrow v| + k|\overrightarrow v = |k|$$ (where $|\overrightarrow v|$ is the length of $\overrightarrow v$). But only $|1| = \mathsf{false}$ (if that is the convention chosen). In English, there is no bound on the number of terms required to get a boolean by applying a numeral. So there cannot be a $\overrightarrow v$ that satisfies the equations for all numerals, and thus $\mathsf{IsZero}$ cannot be defined.

Answer 2

The most straightforward way to define addition in lambda-calculus is to treat the numbers as if they were linked lists, and catenate the lists. To do this right, it is necessary to use extra variables to replace the outer variables of each number, so the resulting expression for the second number can be substituted for the inner variable of the resulting expression for the first number. This yields the following expression for addition:

  λw.λx.λy.λz.w y (x y z)