de Bruijn index - Wikipedia

submited by

Style Pass

2024-10-28 18:00:02

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. Each de Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. The following are some examples:

De Bruijn indices are commonly used in higher-order reasoning systems such as automated theorem provers and logic programming systems.[ 2]

where n—natural numbers greater than 0—are the variables. A variable n is bound if it is in the scope of at least n binders (λ); otherwise it is free. The binding site for a variable n is the nth binder it is in the scope of, starting from the innermost binder.

The most primitive operation on λ-terms is substitution: replacing free variables in a term with other terms. In the β-reduction (λ M) N, for example, we must