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^5\,4$. 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^3\,2\ 1=\texttt{b}\ \texttt{k}$$

The pred function can be implemented similarly: $$\texttt{pred}=\lambda^2\,1\ 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$. Optimally, pred should probably return $\lambda^1\,0$ again, but in this case the $\texttt{ω}$ combinator $\lambda^1\,0\ 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^3\,2\ (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 that 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}=\lambda\,0\ \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}$.

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^1\,0\ (\lambda^2\,0\ (1\ (\lambda^2\,2\ 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^1\,0\ 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^2\,0\ (\texttt{t}\ \texttt{i})\ (1\ \texttt{k}\ (0\ \texttt{k}))$$ (note that $\langle n\rangle_c\ (\texttt{t}\ a)\overset{*}{\leadsto}\lambda^1\,0\ \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^3\,1\ (0\ 2)=\texttt{q''}\\ \texttt{pop}_0&=\lambda^2\,1\ (\lambda^1\,1)\\ \texttt{pop}_1&=\lambda^2\,1\ (\lambda^2\,2\ 1)\\ \texttt{pop}_n&=\lambda^3\,1\ (2\ \texttt{b}\ \texttt{k}\ 0)\\ \texttt{move}&=\lambda^3\,1\ (\lambda^1\,3\ \texttt{b}\ (\lambda^1\,0\ 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.

动态网自由门 天安門 天安门 法輪功 李洪志 Free Tibet 六四天安門事件 The Tiananmen Square protests of 1989 天安門大屠殺 The Tiananmen Square Massacre 反右派鬥爭 The Anti-Rightist Struggle 大躍進政策 The Great Leap Forward 文化大革命 The Great Proletarian Cultural Revolution 人權 Human Rights 民運 Democratization 自由 Freedom 獨立 Independence 多黨制 Multi-party system 台灣 臺灣 Taiwan Formosa 中華民國 Republic of China 西藏 土伯特 唐古特 Tibet 達賴喇嘛 Dalai Lama 法輪功 Falun Dafa 新疆維吾爾自治區 The Xinjiang Uyghur Autonomous Region 諾貝爾和平獎 Nobel Peace Prize 劉暁波 Liu Xiaobo 民主 言論 思想 反共 反革命 抗議 運動 騷亂 暴亂 騷擾 擾亂 抗暴 平反 維權 示威游行 李洪志 法輪大法 大法弟子 強制斷種 強制堕胎 民族淨化 人體實驗 肅清 胡耀邦 趙紫陽 魏京生 王丹 還政於民 和平演變 激流中國 北京之春 大紀元時報 九評論共産黨 獨裁 專制 壓制 統一 監視 鎮壓 迫害 侵略 掠奪 破壞 拷問 屠殺 活摘器官 誘拐 買賣人口 遊進 走私 毒品 賣淫 春畫 賭博 六合彩 天安門 天安门 法輪功 李洪志 Winnie the Pooh 劉曉波动态网自由门