Skip to content(if available)orjump to list(if available)

De Bruijn Numerals

De Bruijn Numerals

2 comments

·November 16, 2025
Visit

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 winning a largest output contest, with a program under 42 bytes in size [2].

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

[2] https://codegolf.stackexchange.com/questions/18028/largest-n...

emptybits

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