de Bruijn indices are a technique for representing terms of the -calculus (and other type theories with binders) without relying on named variables. They are particularly useful for representing the -calculus in memory.
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 term is represented as . In more detail:
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}
}