de Bruijn indices

de Bruijn indices are a technique for representing the terms of languages with binding without relying on named variables and \alpha-conversion. They are particularly useful for computing implementation

When using de Bruijn indices, a variable is replaced by a number denoting how much further up in its syntax tree the binding construct occurs, counting from the inside out.

For example, the untyped \lambda-term

\lambda x. x(\lambda y. yx)

is represented as

\lambda. 0(\lambda. 0\ 1)

In more detail:

The occurrence of y is replaced with 0 to signify that y is the variable bound by the most closely occuring \lambda binder. In much the same way, the first occurence of x is also replaced with 0.
The second occurrence of x is replaced with 1, to signify that this particular variable is bound two \lambda's up in the syntax tree.

Implementing de Bruijn indices

In dependent type theory

It is possible to encode terms with de Bruijn indices in a type-safe manner in a dependent type theory with indexed inductive types.

This was first noticed by Altenkirch and Reus 1999, using ideas by Bellegarde and Hook 1994 and Bird and Patterson 1999.

References

This technique originates with N. G. de Bruijn. It was first described in

Bruijn, N.G de. 1972. ‘Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem’. Indagationes Mathematicae (Proceedings) 75 (5): 381–92. https://doi.org/10.1016/1385-7258(72)90034-0.

@article{de_bruijn_1972,
	title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the {Church}-{Rosser} theorem},
	volume = {75},
	doi = {10.1016/1385-7258(72)90034-0},
	number = {5},
	journal = {Indagationes Mathematicae (Proceedings)},
	author = {de Bruijn, N.G},
	year = {1972},
	pages = {381--392}
}

The encoding of de Bruijn indices in languages with indexed inductive types was explicitly in the following references.

Bellegarde, Françoise, and James Hook. 1994. ‘Substitution: A Formal Methods Case Study Using Monads and Transformations’. Science of Computer Programming 23 (2–3): 287–311. https://doi.org/10.1016/0167-6423(94)00022-0. pdf

@article{bellegarde_substitution_1994,
	title = {Substitution: {A} formal methods case study using monads and transformations},
	volume = {23},
	doi = {10.1016/0167-6423(94)00022-0},
	number = {2-3},
	journal = {Science of Computer Programming},
	author = {Bellegarde, Françoise and Hook, James},
	year = {1994},
	pages = {287--311},
}

Bird, Richard S., and Ross Paterson. 1999. ‘De Bruijn Notation as a Nested Datatype’. Journal of Functional Programming 9 (1): 77–91. https://doi.org/10.1017/S0956796899003366. pdf

@article{bird_1999,
	title = {de {Bruijn} notation as a nested datatype},
	volume = {9},
	doi = {10.1017/S0956796899003366},
	number = {1},
	journal = {Journal of Functional Programming},
	author = {Bird, Richard S. and Paterson, Ross},
	year = {1999},
	pages = {77--91},
}

Altenkirch, Thorsten, and Bernhard Reus. 1999. ‘Monadic Presentations of Lambda Terms Using Generalized Inductive Types’. In Computer Science Logic, 1683:453–68. Lecture Notes in Computer Science. Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-48168-0_32. pdf

@inproceedings{altenkirch_1999,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Monadic {Presentations} of {Lambda} {Terms} {Using} {Generalized} {Inductive} {Types}},
	volume = {1683},
	doi = {10.1007/3-540-48168-0_32},
	booktitle = {Computer {Science} {Logic}},
	publisher = {Springer Berlin Heidelberg},
	author = {Altenkirch, Thorsten and Reus, Bernhard},
	year = {1999},
	pages = {453--468},
	file = {Altenkirch and Reus - 1999 - Monadic Presentations of Lambda Terms Using Genera.pdf:C\:\\Users\\tz20861\\Zotero\\storage\\V6Z79KYU\\Altenkirch and Reus - 1999 - Monadic Presentations of Lambda Terms Using Genera.pdf:application/pdf},
}

de Bruijn indices

Implementing de Bruijn indices

In dependent type theory

See also

References