De Bruijn index

Mathematical notation in lambda calculus / From Wikipedia, the free encyclopedia

Dear Wikiwand AI, let's keep it short by simply answering these key questions:

Can you list the top facts and stats about De Bruijn index?

Summarize this article for a 10 year old


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:

  • 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.
  • The term λx. λy. λz. x z (y z) (the S combinator), with de Bruijn indices, is λ λ λ 3 1 (2 1).
  • The term λz. (λy. yx. x)) (λx. z x) is λ (λ 1 (λ 1)) (λ 2 1). See the following illustration, where the binders are colored and the references are shown with arrows.

Pictorial depiction of example

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

Oops something went wrong: