**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

De Bruijn indices are used to represent terms in lambda calculus and type theory without naming bound variables.

Usually in informal mathematical language, an expression involving a lambda is written out as $\lambda x.\phi(x)$. However, this involves the use of bound variables, which are hard to deal with when formalizing substitution of variables; in addition, the statements $\lambda x.\phi(x)$ and $\lambda y.\phi(y)$ refer to the same thing. De Bruijn indices involve the use natural numbers instead of bound variables; both $\lambda x.\phi(x)$ and $\lambda y.\phi(y)$ would be written as $\lambda \phi(\underline{0})$ when using De Bruijn indices, and $\lambda x.\lambda y.\phi(x, y)$ would be written as $\lambda \lambda \phi(\underline{1}, \underline{0})$. A statement like $x \lambda x.\phi(x)$ where $x$ is both a bound variable and a free variable would be written as $\underline{1} \lambda \phi(\underline{0})$ using de Bruijn indices.

de Bruijn indices are discussed in section 9.1 of:

- Théo Winterhalter,
*Formalisation and Meta-Theory of Type Theory*, Nantes (2020) [pdf, github]

The notion is due to:

- Nicolaas de Bruijn,
*Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem*, Indagationes Mathematicae (Proceedings)**75**5 (1972) 381-392 [doi:10.1016/1385-7258(72)90034-0, pdf]

See also:

- Wikipedia, De Bruijn index

Last revised on July 21, 2023 at 22:15:44. See the history of this page for a list of all contributions to it.