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 . However, this involves the use of bound variables, which are hard to deal with when formalizing substitution of variables; in addition, the statements and refer to the same thing. De Bruijn indices involve the use natural numbers instead of bound variables; both and would be written as when using De Bruijn indices, and would be written as . A statement like where is both a bound variable and a free variable would be written as using de Bruijn indices.
de Bruijn indices are discussed in section 9.1 of:
The notion is due to:
See also:
Last revised on July 21, 2023 at 22:15:44. See the history of this page for a list of all contributions to it.