Looking at https://text.marvinborner.de/2023-04-06-01.html helped me understand the syntax a bit (though I'm just a non-theoretical programmer).

I was confused about what <4> = \lambda ^ 5 4 meant, since it already seemed to have a "4" in it.

The trick is that the 4 seems to be similar to a positional argument index, but numbered inside out.

IOW, in this encoding, <4> is a function that can be called 5 times (the exponent on the lambda) and upon the fifth call will resolve to whatever was passed in 1st (which because of the inside-out ordering is labeled "4").

(For a simpler example, 0 is a function that can be called once and returns its argument.)

So succ is 3-ary; it says, give me a function (index 2, outermost call); next, give me its first argument (index 1, second-outermost call); when you call that (index 0, dropped, innermost call), I'll apply the function to the argument.

But note that if index 2 is a numeral <N>, the outermost call returns a function that will "remember" the next thing passed in and return it after 1 (succ's innermost call) + N + 1 (<N>'s contract) calls.

> 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)

Just use Scott-Mogensen encoding, seriously.

    Zero = z. s. z
    Succ = n. z. s. s n

    isZero = n. n True (_. False)
    pred   = n. n Zero (r. r)

Addition requires explicit recursion, however (since numbers aren't folds), so I guess you'll have to either use Y combinator or closure-convert manually:

    add' = add'. m. n. m n (r. Succ (add' add' r n))
    add = add' add'

In any case, arithmetic operations can't be made fully constant-time for obvious reasons so whether your prefer this to Church numerals is a matter of taste. However, for lists/tuples the ability to execute head/tail/cons in constant time is much more important in practice than being able to do append in constant time.

If you’re “into” de Bruijn numerals or Project Euler then you might be familiar with this little treat:

https://projecteuler.net/problem=941

Otherwise, have a go and don’t spoil it! (I have failed thus far.)