De Bruijn index

Summary

De Bruijn indices write terms of the lambda calculus without names for bound variables. Each bound occurrence of a variable is replaced by a natural number that counts the abstractions between the occurrence and its binder. Two terms that differ only by renaming of bound variables then become literally the same. Nicolaas Govert de Bruijn introduced them in 1972, and they are widely used in proof assistants and compilers.