There are many ways to encode numbers and do arithmetic in the pure lambda calculus, for example using unary Church numerals, various $n$-ary representations, and the Scott encoding.

A method that I have not seen yet is an encoding by reference depth. Specifically, I refer to a nested de Bruijn index that, by itself, encodes the number:

$$\langle n\rangle_d=\lambda^{S(n)}n$$

For example, the decimal number $4$ would be encoded as $\langle4\rangle_d=\lambda^54$

However, during my experiments with this encoding, I made an unfortunate discovery. While reading up on the theory behind optimal reduction in some ancient book I found in the library, I stumbled upon the work “Some Unusual Numeral Systems” by Wadsworth (1980), which was coincidentally published in the same book as Lévy’s legendary paper on optimal reduction. In this work, 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). He then went on to show that there can not exist an adequate numeral system encoding numbers as $$\langle n\rangle_e=\lambda^{k_n}E_n,$$

Unfortunately, a zero? function is required in order to convert any number from this numeral system to another system. So, even with these limitations, can the “de Bruijn numerals” still be useful for anything? What do other arithmetic operations look like?

The simplest operation is the succ function, which is minimally defined as $$\texttt{succ}=\lambda^32\ 1=\texttt{b}\ \texttt{k}$$

The pred function can be implemented similarly: $$\texttt{pred}=\lambda^21\ 0\ 0=\texttt{w}$$

They both use the fact that the outermost abstraction is always bound to the inner de Bruijn index. Substituting the index with a reference to a fresh abstraction results in incrementing/decrementing behavior (utilizing the shift procedure of $\beta$-reduction with de Bruijn indices)

One problem of pred is its application to $\langle0\rangle_d$

Now, normally further operations could be defined by recursion ending with a truthy zero?. Of course, this is not an option for this encoding.

So instead, here’s an incredibly tiny self-contained addition function: $$\texttt{add}=\lambda^32\ (1\ 0)=\texttt{b}$$

Isn’t it magical? This is one of the reasons I still like the encoding: it abuses the de Bruijn shifting so elegantly! It’s basically like a metacircular numeral system since it hijacks the host reducer’s computations!

On the other hand, I was not yet able to come up with further such elegant functions (maybe you can help?) – instead, I came up with some hybrid implementations which use multiple different numeral systems (in this case, Church’s).

A Church numeral is not that different from a de Bruijn numeral, as it turns out. It is defined like this:

$$\begin{align*} \langle n\rangle_c &= \lambda^1\overbrace{0\circ\dots\circ0}^{\mathclap{n}} \end{align*}$$

Converting (“apostatizing”) a Church numeral to a de Bruijn numeral is done using the conv function:

$$\texttt{conv}=\lambda0\ \texttt{k}=\texttt{t}\ \texttt{k}$$

With the internal structure of the Church encoding, this basically comes down to applying succ $n-1$

In general, assuming an encoding $e$ of $\langle n\rangle_e$

$$\texttt{conv*}=\texttt{fix}\ (\lambda^3\texttt{zero?*}\ 0\ 1\ (2\ (\texttt{succ}\ 1)\ (\texttt{pred*}\ 0)))\ \langle 0\rangle_d$$

The function consists of fairly typical fix-recursion using a left case $(\texttt{zero?}\ 0\ 1)$ to return the constructed term if the input number is zero and a right case $(2\ (\texttt{succ}\ 1)\ (\texttt{pred*}\ 0))$ that calls the fix-induced function recursively with the incremented de Bruijn numeral and decremented input number.

$$*\ *\ *$$

Anyway, with the insight on Church numerals, we find that the de Bruijn numerals are defined from nothing else than $$\langle a\rangle_d=\overbrace{\texttt{k}\circ\dots\circ\texttt{k}}^{\mathclap{a}}.$$

Indeed, any operation on Church numerals can now be made to return a de Bruijn numeral, simply by applying $\langle1\rangle_d$

Next, an actual problem where I use de Bruijn numerals in practice all the time!

I always found Church $n$-tuples really hard to work with. This is because selecting the $i$th element – again – requires an increasing number of abstractions! In fact their behavior is so similar that I could only now make use of them after gaining insight about de Bruijn numerals. They are defined like this: $$\texttt{tuple}_n=\lambda^{S(n)}0\ n\ [n-1]\ \ldots\ 1$$

Luckily, such a term can be constructed using de Bruijn numerals. The idea is simple: First, we apply $\langle i\rangle_d$

Finally, with this knowledge, Church $n$-tuples can be used almost like Church lists. Some further functions: $$\begin{align*} \texttt{push}&=\lambda^31\ (0\ 2)=\texttt{q''}\\ \texttt{pop}_0&=\lambda^21\ (\lambda^11)\\ \texttt{pop}_1&=\lambda^21\ (\lambda^22\ 1)\\ \texttt{pop}_n&=\lambda^31\ (2\ \texttt{b}\ \texttt{k}\ 0)\\ \texttt{move}&=\lambda^31\ (\lambda^13\ \texttt{b}\ (\lambda^10\ 1)\ 1) \end{align*}$$

where move moves the first element to the $n$th position, without knowing the size of the tuple! $$\texttt{move}\ \langle i\rangle_c\ [x_1,\dots,x_n]\overset{*}{\leadsto}[x_2,\dots,x_1,\dots x_n]$$

Notably, something like move or pop-n generally requires recursion for Church lists. At the same time for Church $n$-tuples, something as simple as counting the elements is not possible for the same reasons as a zero? function for de Bruijn numerals, as the counting function would have to ignore (and count) $n$ applied arguments.

(see also a Forth/postscript-like stack language DSL in bruijn using this stack encoding here)

$$❦$$

All presented definitions can be found in bruijn’s standard library: std/Number/Bruijn, std/Tuples.

Thanks for reading. Please let me know if you know of – or come up with! – other/better operations for de Bruijn numerals. Contact me via email. Support on Ko-fi. Subscribe on RSS. Follow on Mastodon.