De Bruijn Numerals

Summary

assumptions in this post understanding of pure lambda calculus zero-based de Bruijn indices instead of named variables nnn consecutive lambdas are written as λn\lambda^nλn ⟨n⟩e\langle n\rangle_e⟨n⟩e​ encodes n∈N0n\in\mathbb{N}_0n∈N0​ as a lambda calculus term of encoding eee S(n)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 nnn-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⟨n⟩d​=λS(n)n For example, the decimal number 444 would be encoded as ⟨4⟩d=λ54\langle4\rangle_d=\lambda^54⟨4⟩d​=λ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,⟨n⟩e​=λkn​En​, with EnE_nEn​ being a normal form and knk_nkn​ increasing indefinitely with nnn. And, to be fair, it makes sense: An increasing nnn will require an increasing number of applications s...