Comment by tromp

> Christopher Wadsworth analyzed different properties of numeral systems and the requirements they have to fulfill to be useful for arithmetic.

> Specifically, he calls a numeral system adequate if it allows for a successor (succ) function, predecessor (pred) function, and a zero? function yielding a true (false) encoding when a number is zero (or not).

A numeral system is adequate iff it can be converted to and from Church numerals. Converting from Church numerals requires functions N0 and Nsucc so that

    Church2Num c = c Nsucc N0

while converting to Church numerals requires functions Nzero? and Npred so that

    Num2Church n = Nzero? n C0 (Csucc (Num2Church (Npred n)))

with an implicit use of the fixpoint combinator.

An interesting adequate numeral system is what i call the tuple numerals [1], which are simply iterates of the 1-tuple function T = λxλy.y x

So N0 = id, Nsucc = λnλx.n (T x), Npred = λnλx.n x id, and Nzero? = λnλtλf. n (K t) (K f).

These tuple numerals are useful in proving lower bounds on a functional busy beaver [2].

[1] https://github.com/tromp/AIT/blob/master/numerals/tuple_nume...

[2] https://oeis.org/A333479 (see bms.lam link)