Church Numerals convert to int without language primitive

Question

Is it possible to convert a church numeral to an integer representation without using a language primitive such as add1?

All the examples I've come across use a primitive to dechurch to int

Example:

 plus1 = lambda x: x + 1
 church2int = lambda n: n(plus1)(0)

Example 2:

 (define (church-numeral->int cn)
    ((cn add1) 0))

I'm experimenting with a micro lisp intepretter (using only John McCarthy's 10 rules) and would like to understand if that can be done without adding a primitive.

Answer 1

The integer numeric type is not part of McCarthy's list of Lisp elementary primitive procedures - you only have functions at that level, no other data types exist. That's why integers would need to be represented as functions (for instance, using Church numerals) if we were to adhere strictly to such minimalistic definition of Lisp. So the answer is no. You can't convert to a data type that doesn't exist yet.

Now suppose that we add integers as atoms in the language (notice that adding a new data type to the language goes beyond the 7-10 primitive procedures mentioned). To simplify even more, suppose that we just add a single number, the number zero - then we'd still need the add1 operation to build the rest of the integers, as per Peano axioms, which require the existence of the successor operation for the natural numbers to exist. Again, we can't convert from Church numerals to integers without at least having the number zero as an atom and the add1 function.

Answer 2

No. int, as you describe it, is a primitive type of value, not a function. You can't manipulate such ints at all without primitives (without add1, how are you ever going to get to 1 from 0?).

However, you certainly can convert between two different Church-encodings of natural numbers without using primitives, as long as your language is Turing-complete without those primitives.