De Bruijn indices

(1) let x = 2 in x + 3 end

and

(2) let y = 2 in y + 3 end

(Both of these programs are written in Standard ML, a beautiful programming language based on work done at Edinburgh University. Each takes the value of the variable as set in the let statement and plugs it in for every occurrence of that variable up until the matching end statement. Thus, each program goes next to "2+3" and then to "5" and is done.)

Obviously, these are the same programs, with the only difference being the names of the variables involved. However, proving this can be somewhat difficult, especially in more complicated programs. The simplest solution to this problem is to, each time you see a new variable, give it a number, instead of a name. After this is done, the programs would both look like this (I make the variable names in bold so as not to confuse them with the literal numbers in the program):

let 1 = 2 in 1 + 3 end

A more complex example would be

let x = 2 in let y = 3 in x+y end end

which would become

let 1 = 2 in let 2 = 3 in 1+2 end end

De Bruijn indices are a variation on this. However, instead of giving each variable a unique number, when variables are referenced, they are replaced with a number indicating how far back they were bound. So if a variable is referenced immediately after being bound, it is one. If another variable is bound in between the first variable's binding and reference, in that specific reference, the first variable is numbered two. One slightly odd thing about this is that, when bound, no name is given to the variable, as none is needed. Only the value to be referenced is given. Thus, our more complex example from above,

let x = 2 in let y = 3 in x+y end end

becomes

let 2 in let 3 in 2+1 end end

In this, the two let statements merely give the value the variable will refer to, rather than the number of the variable itself. The actual body of the program here is "2+1". In this, the 2 refers to the variable bound two variable bindings back, which has a value of 2, and the 1 refers to the variable bound one binding back, which has the value of 3, so we get 2+3, which gives us 5.

De Bruijn indices have several advantages over the simpler numbering of variables. One of these is that it can be implemented using a stack of variable values where, to find the value of a variable, you simply pop the stack as many times as is the variable's number. When a variable goes out of scope, its value is removed from the stack. This keeps the numbers managable, and, more importantly, there will always be exactly as many values stored as variables in scope. This keeps memory usage low. On the other hand, de Bruijn indices are a much more complicated concept than simple numbering. However, once understood, they are easier to implement and manipulate.