De Bruijn index

Remarks

Example: $\lambda x.\, \lambda y.\, \lambda z.\, x\, z\, (y\, z)$ becomes $\lambda\, \lambda\, \lambda\, 3\, 1\, (2\, 1)$. The occurrence of $x$ has the three abstractions $\lambda z$, $\lambda y$, $\lambda x$ around it, counting outward, and its binder is the third.

Non-example: $\lambda\, \lambda\, 1$ is not the de Bruijn form of $\lambda x.\, \lambda y.\, x$. Counting outward from $x$, the first enclosing abstraction is $\lambda y$, so the index of $x$ is $2$, and the form is $\lambda\, \lambda\, 2$. Counting from the outside instead gives de Bruijn levels, a different convention.

Two closed terms are $\alpha$-equivalent exactly when they have the same de Bruijn form. For terms with free variables, one fixes a list of the free variables and continues the count past the outermost abstraction. Beta reduction becomes $(\lambda\, M)\, N \to M[1 := N]$, where the substitution must shift the indices of free variables in $N$ and decrement those of $M$.