In mathematical logic, the de Bruijn index is a tool invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms of lambda calculus without naming the bound variables.
[1] Terms written using these indices are invariant with respect to α-conversion, so the check for α-equivalence is the same as that for syntactic equality.
[2] Formally, λ-terms (M, N, ...) written using de Bruijn indices have the following syntax (parentheses allowed freely): where n—natural numbers greater than 0—are the variables.
Formally, a substitution is an unbounded list of terms, written M1.M2..., where Mi is the replacement for the ith free variable.
The increasing operation in step 3 is sometimes called shift and written ↑k where k is a natural number indicating the amount to increase the variables, and is defined by For example, ↑0 is the identity substitution, leaving a term unchanged.
The steps outlined for the β-reduction above are thus more concisely expressed as: When using the standard "named" representation of λ-terms, where variables are treated as labels or strings, one must explicitly handle α-conversion when defining any operation on the terms.
Thus, even if a system uses de Bruijn indices internally, it will present a user interface with names.
This eliminates the need to reindex free variables, for example when weakening the context, whereas de Bruijn indices eliminate the need to reindex bound variables, for example when substituting a closed expression in another context.
[3] De Bruijn indices are not the only representation of λ-terms that obviates the problem of α-conversion.
[5] Another common alternative is an appeal to higher-order representations where the λ-binder is treated as a true function.
When reasoning about the meta-theoretic properties of a deductive system in a proof assistant, it is sometimes desirable to limit oneself to first-order representations and to have the ability to name or rename assumptions.
The locally nameless approach uses a mixed representation of variables—de Bruijn indices for bound variables and names for free variables—that is able to benefit from the α-canonical form of de Bruijn indexed terms when appropriate.