The number representation proposed by the author is one I've never seen before:
|0| = λx. x
|n+1| = λ_. |n|
In other words, 0 is identity, and successor is the const function. This makes the predecessor function easy to define. Just apply Succ n to anything to get n back. The article fails to answer the most crucial question about these numerals though:
Can we write a function that tests if a numeral represents 0?
I.e. a function f such that
f |0| = True
f |n+1| = False
Equivalently, we can ask if it's possible to convert these numerals to Church numerals, the standard number representation in lambda calculus.
If one cannot, then these numerals don't seem to be useful in any way, and don't deserve to be called a number representation.
This reminds me of someone proposing to represent the number n in combinatory logic with basis {S,K} as simply S^n K, i.e. using K as Zero and S as Successor. That one does turn out to be convertible to Church numerals [1].
[1] https://john-tromp.medium.com/sk-numerals-9ad1b5634b28
Can we write a function that tests if a numeral represents 0? I.e. a function f such that
Equivalently, we can ask if it's possible to convert these numerals to Church numerals, the standard number representation in lambda calculus. If one cannot, then these numerals don't seem to be useful in any way, and don't deserve to be called a number representation.This reminds me of someone proposing to represent the number n in combinatory logic with basis {S,K} as simply S^n K, i.e. using K as Zero and S as Successor. That one does turn out to be convertible to Church numerals [1].
[1] https://john-tromp.medium.com/sk-numerals-9ad1b5634b28