de Bruijn indices are a technique for representing the terms of languages with binding without relying on named variables and -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 -term
is represented as
In more detail:
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].
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}
}
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},
}