> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/340-lambda-calculi/terms/de-bruijn-indexing.md).

# De Bruijn index

<https://en.wikipedia.org/wiki/De_Bruijn_index> <https://en.wikipedia.org/wiki/De_Bruijn_notation>

(*De Bruijn indexing* is a method for avoiding naming bound variables in lambda calculus, while an alternative syntax for lambda expressions is called *De Bruijn notation*)

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.

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.

Examples:

* λx. λy. x ≡ (λ λ 2)
* λx. λy. λz. x z (y z) ≡ λ λ λ 3 1 (2 1)
* λz. (λy. y (λx. x)) (λx. z x) ≡ λ (λ 1 (λ 1)) (λ 2 1)