CentralNotice From Wikipedia, the free encyclopedia Jump to: navigation , search 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. [ 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: The term λ x . λ y . x , sometimes called the K combinator , is written as λ λ 2 with De Bruijn indices. The binder for the occurrence x is the second λ in scope. T...