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

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

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$

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

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$

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$

$$\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.

$$❦$$

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.

---