De Bruijn indexとは 意味・読み方・使い方

In mathematical logic, the De Bruijn index is a notation invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms in the λ calculus with the purpose of eliminating the names of the variable from the notation. Terms written using these indexes 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:

• The term λx. λy. x, sometimes called the K combinator, is written as λ λ 2 with De Bruijn indexes. The binder for the occurrence x is the second λ in scope.
• The term λx. λy. λz. x z (y z) (the S combinator), with De Bruijn indexes, is λ λ λ 3 1 (2 1).
• The term λz. (λy. y (λx. x)) (λx. z x) is λ (λ 1 (λ 1)) (λ 2 1). See the following illustration, where the binders are coloured and the references are shown with arrows.