• Arithmetic

• Hybrid

• Projections assumptions in this post

• understanding of pure lambda calculus

• zero-based de Bruijn indices instead of named variables

• nn consecutive lambdas are written as λn\lambda^n

• ⟨n⟩e\langle n\rangle_e encodes n∈N0n\in\mathbb{N}_0 as a lambda calculus term of encoding ee

• S(n)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 nn-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:

⟨n⟩d=λS(n)n\langle n\rangle_d=\lambda^{S(n)}n

For example, the decimal number 44 would be encoded as ⟨4⟩d=λ54\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 ⟨n⟩e=λknEn,\langle n\rangle_e=\lambda^{k_n}E_n, with EnE_n being a normal form and knk_n increasing indefinitely with nn. And, to be fair, it makes sense: An increasing nn will require an increasing number of applications scaling with knk_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 succ=λ32 1=b k\texttt{succ}=\lambda^32\ 1=\texttt{b}\ \texttt{k}

Proof

To prove: ∀n∈N0:succ ⟨n⟩d⇝∗⟨S(n)⟩d\forall n\in\mathbb{N}_0: \texttt{succ}\ \langle n\rangle_d\overset{*}{\leadsto}\langle S(n)\rangle_d

Proof by β\beta-reduction (⇝{\leadsto}): succ ⟨n⟩d= (λ32 1) λS(n)n⇝ λ2(λS(n)n) 1⇝ λ2λnS(n)=λS(S(n))S(n)=⟨S(n)⟩d \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: pred=λ21 0 0=w\texttt{pred}=\lambda^21\ 0\ 0=\texttt{w}

Proof

To prove: ∀n∈N0:pred ⟨S(n)⟩d⇝∗⟨n⟩d\forall n\in\mathbb{N}_0: \texttt{pred}\ \langle S(n)\rangle_d\overset{*}{\leadsto}\langle n\rangle_d

Proof by β\beta-reduction (⇝{\leadsto}): pred ⟨S(n)⟩d= (λ21 0 0) λS(S(n))S(n)⇝ λ(λS(S(n))S(n)) 0 0⇝ λ(λS(n)S(n)) 0⇝ λλnn=λS(n)n=⟨n⟩d \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 ⟨0⟩d\langle0\rangle_d. Optimally, pred should probably return λ10\lambda^10 again, but in this case the ω\texttt{ω} combinator λ10 0\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: add=λ32 (1 0)=b\texttt{add}=\lambda^32\ (1\ 0)=\texttt{b}

Proof

To prove: ∀a,b∈N0:add ⟨a⟩d ⟨b⟩d⇝∗⟨a+b⟩d\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}): add ⟨a⟩d ⟨b⟩d= (λ32 (1 0)) (λS(a)a) λS(b)b⇝ (λ2(λS(a)a) (1 0)) λS(b)b⇝ λ1(λS(a)a) (λS(b)b 0)⇝ λ1(λS(a)a) (λbb)⇝ λ1λaλb[a+b]=λS(a+b)[a+b]=⟨a+b⟩d \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:

⟨n⟩c=λ10∘⋯∘0⏞n \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:

conv=λ0 k=t k \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−1n-1 times on k=⟨1⟩d\texttt{k}=\langle1\rangle_d, as succ=b k\texttt{succ}=\texttt{b}\ \texttt{k}.

Proof

To prove: ∀n∈N0:conv ⟨n⟩c⇝∗⟨n⟩d\forall n\in\mathbb{N}_0: \texttt{conv}\ \langle n\rangle_c\overset{*}{\leadsto}\langle n\rangle_d

Proof by beta reduction (⇝\leadsto): conv ⟨n⟩c= (λ0 k) λ0∘⋯∘0⏞n⇝ (λ0∘⋯∘0⏞n) k⇝ k∘⋯∘k⏞n=b k (b k (… (b k ⟨1⟩d)…)⇝succ λS(n)n=⟨n⟩d \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*}

Proof by induction:

• Base: n=0n=0\

(conv* ⟨0⟩e)= ((fix (λ3(((zero?* 0) 1) ((2 (succ 1)) (pred* 0))) ⟨0⟩d)) ⟨0⟩e)⇝ ((λ2(((zero?* 0) 1) ((rec (succ 1)) (pred* 0))) ⟨0⟩d) ⟨0⟩e)⇝ (((zero?* ⟨0⟩e) ⟨0⟩d) ((rec (succ ⟨0⟩d)) (pred* ⟨0⟩e)))⇝ ((λ21 ⟨0⟩d) ((rec (succ ⟨0⟩d)) (pred* ⟨0⟩e)))⇝ ⟨0⟩d \begin{align*} (\texttt{conv*}\ \langle 0\rangle_e)=&\ ((\texttt{fix}\ (\lambda^3(((\texttt{zero?*}\ 0)\ 1)\ ((2\ (\texttt{succ}\ 1))\ (\texttt{pred*}\ 0)))\ \langle 0\rangle_d))\ \langle 0\rangle_e)\ \leadsto&\ ((\lambda^2(((\texttt{zero?*}\ 0)\ 1)\ ((\texttt{rec}\ (\texttt{succ}\ 1))\ (\texttt{pred*}\ 0)))\ \langle 0\rangle_d)\ \langle 0\rangle_e)\ \leadsto&\ (((\texttt{zero?*}\ \langle 0\rangle_e)\ \langle 0\rangle_d)\ ((\texttt{rec}\ (\texttt{succ}\ \langle 0\rangle_d))\ (\texttt{pred*}\ \langle 0\rangle_e)))\ \leadsto&\ ((\lambda^21\ \langle 0\rangle_d)\ ((\texttt{rec}\ (\texttt{succ}\ \langle 0\rangle_d))\ (\texttt{pred*}\ \langle 0\rangle_e)))\ \leadsto&\ \langle 0\rangle_d \end{align*}

• Hypothesis: Assuming n=k≥0n=k\ge0, (conv* ⟨k⟩e)⇝⟨k⟩d(\texttt{conv*}\ \langle k\rangle_\mathrm{e})\leadsto\langle k\rangle_d
• Step: n=S(k)n=S(k)\

(conv* ⟨S(k)⟩e)⇝ (((zero?* ⟨S(k)⟩e) ⟨0⟩d) ((rec (succ ⟨0⟩d)) (pred* ⟨S(k)⟩e)))⇝ ((rec (succ ⟨0⟩d)) ⟨k⟩e)=(succ (conv* ⟨k⟩e))=IH (succ ⟨k⟩d)⇝ ⟨S(k)⟩d \begin{align*} (\texttt{conv*}\ \langle S(k)\rangle_e)\leadsto\ &(((\texttt{zero?*}\ \langle S(k)\rangle_e)\ \langle 0\rangle_d)\ ((\texttt{rec}\ (\texttt{succ}\ \langle 0\rangle_d))\ (\texttt{pred*}\ \langle S(k)\rangle_e)))\ \leadsto\ &((\texttt{rec}\ (\texttt{succ}\ \langle 0\rangle_d))\ \langle k\rangle_e)=(\texttt{succ}\ (\texttt{conv*}\ \langle k\rangle_e))\ \overset{\mathrm{IH}}{=}\ &(\texttt{succ}\ \langle k\rangle_d)\ \leadsto\ &\langle S(k)\rangle_d \end{align*}

–>

∗ ∗ ∗*\ *\ *

Anyway, with the insight on Church numerals, we find that the de Bruijn numerals are defined from nothing else than ⟨a⟩d=k∘⋯∘k⏞a.\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 bb, this composition sequence has to be composed bb-times. mult ⟨a⟩d ⟨a⟩d⇝∗k∘⋯∘k⏞a∘⋯∘k∘⋯∘k⏞a⏞b\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 nn-times composing Church encoding does exactly that: ⟨a⟩c ⟨b⟩d⇝∗⟨a⋅b⟩d\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 ⟨1⟩d\langle1\rangle_d. Others can be transformed internally such that they also use de Bruijn operations: fac=λ10 (λ20 (1 (λ22 1 (1 0)))) (λ1⟨1⟩d) i\texttt{fac}=\lambda^10\ (\lambda^20\ (1\ (\lambda^22\ 1\ (1\ 0))))\ (\lambda^1\langle1\rangle_d)\ \texttt{i} fac ⟨5⟩c⇝∗⟨120⟩d\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 nn-tuples really hard to work with. This is because selecting the iith 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: tuplen=λS(n)0 n [n−1] … 1\texttt{tuple}_n=\lambda^{S(n)}0\ n\ [n-1]\ \ldots\ 1 [x1,x2,…,xn]c=tuplen x1 … xn⇝∗λ10 x1 x2 … xn[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 iith element of an nn-tuple would then look something like this: selectni [x1,x2,…,xn]c⇝∗xi,\texttt{select}^{i_n\ [x_1,x_2,\dots,x_n]_c\overset{*}{\leadsto}x_i, which of course must reject all terms but xix_i, therefore requiring an application of λS(n)i\lambda}{S(n)}i to the tuple. Specifically, with Church numerals as parameters, selector ⟨n⟩c ⟨i⟩c⇝∗λS(n)i.\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 ⟨i⟩d\langle i\rangle_d to ⟨n⟩d\langle n\rangle_d, such that we get λnλS(i)i\lambda^{n}\lambda^{S(i)}i. Then, we remove ii abstractions such that it yields λS(n)i\lambda^{S(n)}i. Using i to pop the abstractions, we get: selector=λ20 (t i) (1 k (0 k))\texttt{selector}=\lambda^20\ (\texttt{t}\ \texttt{i})\ (1\ \texttt{k}\ (0\ \texttt{k})) (note that ⟨n⟩c (t a)⇝∗λ10 a a … a⏞n\langle n\rangle_c\ (\texttt{t}\ a)\overset{*}{\leadsto}\lambda^10\ \overbrace{a\ a\ \dots\ a}^n)

Finally, with this knowledge, Church nn-tuples can be used almost like Church lists. Some further functions: push=λ31 (0 2)=q’‘pop0=λ21 (λ11)pop1=λ21 (λ22 1)popn=λ31 (2 b k 0)move=λ31 (λ13 b (λ10 1) 1) \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 nnth position, without knowing the size of the tuple! move ⟨i⟩c [x1,…,xn]⇝∗[x2,…,x1,…xn]\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 nn-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) nn 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.

Wadsworth, Christopher. 1980. “Some Unusual λ\lambda-Calculus Numeral Systems.” To HB Curry: Essays on Combinatory Logic, Lambda Calculus; Formalism.

---