# Sequencing or continuation-passing in pure lambda-calculus

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?

• A notational remark: don't write n λx.x because it leads to trouble – always write n (λx.x) instead. – Andrej Bauer Sep 15 at 12:26
• Thank you, I've corrected the notation. – Tonita Sep 15 at 12:48
• Duplicated at stackoverflow.com/questions/63876968/… (please don't do that). – Andrej Bauer Sep 16 at 5:58
• Yes, after asking on StackOverflow I realized CS is more appropriate for such a question. I've deleted the duplicate now. – Tonita Sep 16 at 10:57
• I have thought about this a little bit and the result is that I am wondering where these lecture notes came from and what the author thinks the solution might be. I am not even sure there is a solution at this point. – Andrej Bauer Sep 18 at 5:54

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.

• Thank you for the model argument, although I am little lost with it. It seems that Is0 is not definable in the pure lambda-calculus (there is some evidence of that in Barendregt). But the proof of this fact is still unknown for me. – Tonita Sep 18 at 23:44
• I don't know what all causes notifications, so I'll add a comment. I've added a sketch of why IsZero would not be possible to implement. – Dan Doel Sep 19 at 19:19
• Thank you for the reasoning, I think now I understand why |N| is not a consistent numeral system. It seems a similar argument shows that defining plus for |N| is also impossible... – Tonita Sep 19 at 20:43

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)

• Yes, it is a standard definition of addition for Church numerals. I prefer the following notation which shows a distinction between the numerals and the cons-nil operations: λm.λn.λs.λz.m s (n s z). But the question concerns the alternative numerals defined in the other way than the classical. Namely, these numerals do not use cons operation, they can be modelled in the following way. If a numeral |N| takes an infinite list of naturals starting by 0, it return a list of natural starting by N. – Tonita Sep 15 at 17:33