de Bruijn Numerals Marvin Borner
assumptions in this post understanding of pure lambda calculus
zero-based de Bruijn indices instead of named variables
n n n consecutive lambdas are written as λ n \lambda^n λ n
consecutive lambdas are written as ⟨ n ⟩ e \langle n\rangle_e ⟨ n ⟩ e encodes n ∈ N 0 n\in\mathbb{N}_0 n ∈ N 0 as a lambda calculus term of encoding e e e
encodes as a lambda calculus term of encoding 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 n n 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:
⟨ n ⟩ d = λ S ( n ) n \langle n\rangle_d=\lambda^{S(n)}n ⟨n⟩d=λS(n)n
For example, the decimal number 4 4 4 would be encoded as ⟨ 4 ⟩ d = λ 5 4 \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.
... continue reading