de Bruijn Numerals

assumptions in this post

• understanding of pure lambda calculus
• zero-based de Bruijn indices instead of named variables
• $n$ consecutive lambdas are written as $\lambda^n$
• $\langle n\rangle_e$ encodes $n\in\mathbb{N}_0$ as a lambda calculus term of encoding $e$
• $S(n)$ is the Peano successor function

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$. Isn’t this just so elegant? Because I could not find a name for the encoding, I call them de Bruijn numerals.

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,$$ with $E_n$ being a normal form and $k_n$ increasing indefinitely with $n$. And, to be fair, it makes sense: An increasing $n$ will require an increasing number of applications scaling with $k_n$ – thus requiring a zero? function to know the number already. Otherwise, the increasing abstractions can not be “collapsed” to terms encoding booleans, as they must have a constant number of abstractions. (read his paper for more details)

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?

Arithmetic

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

Proof

To prove: $\forall n\in\mathbb{N}_0: \texttt{succ}\ \langle n\rangle_d\overset{*}{\leadsto}\langle S(n)\rangle_d$

Proof by $\beta$-reduction (${\leadsto}$): $$\begin{align*} \texttt{succ}\ \langle n\rangle_d=\ &(\lambda^32\ 1)\ \lambda^{S(n)}n\\ \leadsto\ &\lambda^2(\lambda^{S(n)}n)\ 1\\ \leadsto\ &\lambda^2\lambda^nS(n)=\lambda^{S(S(n))}S(n)=\langle S(n)\rangle_d \end{align*}$$

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

Proof

To prove: $\forall n\in\mathbb{N}_0: \texttt{pred}\ \langle S(n)\rangle_d\overset{*}{\leadsto}\langle n\rangle_d$

Proof by $\beta$-reduction (${\leadsto}$): $$\begin{align*} \texttt{pred}\ \langle S(n)\rangle_d=\ &(\lambda^21\ 0\ 0)\ \lambda^{S(S(n))}S(n)\\ \leadsto\ &\lambda(\lambda^{S(S(n))}S(n))\ 0\ 0\\ \leadsto\ &\lambda(\lambda^{S(n)}S(n))\ 0\\ \leadsto\ &\lambda\lambda^nn=\lambda^{S(n)}n=\langle n\rangle_d \end{align*}$$

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$. Optimally, pred should probably return $\lambda^10$ again, but in this case the $\texttt{ω}$ combinator $\lambda^10\ 0$ is returned. I’m not sure if there exists a total pred function for this encoding.

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}$$

Proof

To prove: $\forall a,b\in\mathbb{N}_0: \texttt{add}\ \langle a\rangle_d\ \langle b\rangle_d\overset{*}{\leadsto}\langle a+b\rangle_d$

Proof by $\beta$-reduction (${\leadsto}$): $$\begin{align*} \texttt{add}\ \langle a\rangle_d\ \langle b\rangle_d=\ &(\lambda^32\ (1\ 0))\ (\lambda^{S(a)}a)\ \lambda^{S(b)}b\\ \leadsto\ &(\lambda^2(\lambda^{S(a)}a)\ (1\ 0))\ \lambda^{S(b)}b\\ \leadsto\ &\lambda^1(\lambda^{S(a)}a)\ (\lambda^{S(b)}b\ 0)\\ \leadsto\ &\lambda^1(\lambda^{S(a)}a)\ (\lambda^{b}b)\\ \leadsto\ &\lambda^1\lambda^{a}\lambda^{b}[a+b]=\lambda^{S(a+b)}[a+b]=\langle a+b\rangle_d \end{align*}$$

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

Hybrid

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$ times on $\texttt{k}=\langle1\rangle_d$, as $\texttt{succ}=\texttt{b}\ \texttt{k}$.

Proof

To prove: $\forall n\in\mathbb{N}_0: \texttt{conv}\ \langle n\rangle_c\overset{*}{\leadsto}\langle n\rangle_d$

Proof by beta reduction ($\leadsto$): $$\begin{align*} \texttt{conv}\ \langle n\rangle_c=\ &(\lambda0\ \texttt{k})\ \lambda\overbrace{0\circ\dots\circ0}^{\mathclap{n}}\\ \leadsto\ &(\lambda\overbrace{0\circ\dots\circ0}^{n})\ \texttt{k}\\ \leadsto\ &\overbrace{\texttt{k}\circ\dots\circ\texttt{k}}^{n}=\texttt{b}\ \texttt{k}\ (\texttt{b}\ \texttt{k}\ (\ldots\ (\texttt{b}\ \texttt{k}\ \langle1\rangle_d)\ldots)\\ \overset{\texttt{succ}}{\leadsto}\ &\lambda^{S(n)}n=\langle n\rangle_d \end{align*}$$

In general, assuming an encoding $e$ of $\langle n\rangle_e$ has a zero?* and pred* function, a universal conversion function conv* can be defined:

$$\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}}.$$ If we now, say, want to multiply a number with a different number $b$, this composition sequence has to be composed $b$-times. $$\texttt{mult}\ \langle a\rangle_d\ \langle a\rangle_d\overset{*}{\leadsto} \overbrace{\overbrace{\texttt{k}\circ\dots\circ\texttt{k}}^{\mathclap{a}}\circ\dots\circ\overbrace{\texttt{k}\circ\dots\circ\texttt{k}}^{\mathclap{a}}}^{\mathclap{b}}$$ And – you might have guessed it – the $n$-times composing Church encoding does exactly that: $$\langle a\rangle_c\ \langle b\rangle_d\overset{*}{\leadsto}\langle a\cdot b\rangle_d$$

Indeed, any operation on Church numerals can now be made to return a de Bruijn numeral, simply by applying $\langle1\rangle_d$. Others can be transformed internally such that they also use de Bruijn operations: $$\texttt{fac}=\lambda^10\ (\lambda^20\ (1\ (\lambda^22\ 1\ (1\ 0))))\ (\lambda^1\langle1\rangle_d)\ \texttt{i}$$ $$\texttt{fac}\ \langle5\rangle_c\overset{*}{\leadsto}\langle120\rangle_d$$ Of course – still – the resulting de Bruijn numerals can never be converted back to an encoding like Church’s.

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

Projections

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$$ $$[x_1,x_2,\dots,x_n]_c=\texttt{tuple}_n\ x_1\ \dots\ x_n\overset{*}{\leadsto}\lambda^10\ x_1\ x_2\ \ldots\ x_n$$ Retrieving the $i$th element of an $n$-tuple would then look something like this: $$\texttt{select}^i_n\ [x_1,x_2,\dots,x_n]_c\overset{*}{\leadsto}x_i,$$ which of course must reject all terms but $x_i$, therefore requiring an application of $\lambda^{S(n)}i$ to the tuple. Specifically, with Church numerals as parameters, $$\texttt{selector}\ \langle n\rangle_c\ \langle i\rangle_c\overset{*}{\leadsto}\lambda^{S(n)}i.$$

Luckily, such a term can be constructed using de Bruijn numerals. The idea is simple: First, we apply $\langle i\rangle_d$ to $\langle n\rangle_d$, such that we get $\lambda^{n}\lambda^{S(i)}i$. Then, we remove $i$ abstractions such that it yields $\lambda^{S(n)}i$. Using i to pop the abstractions, we get: $$\texttt{selector}=\lambda^20\ (\texttt{t}\ \texttt{i})\ (1\ \texttt{k}\ (0\ \texttt{k}))$$ (note that $\langle n\rangle_c\ (\texttt{t}\ a)\overset{*}{\leadsto}\lambda^10\ \overbrace{a\ a\ \dots\ a}^n$)

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.

---