De Bruijn indexing
De Bruijn indexing is a technique used to remove names from lambda calculus terms, replacing them with De Bruijn indices. The resulting terms have trivial wikipedia:alpha equivalence, making them simpler to manipulate at the cost of increased cognitive overhead. De Bruijn indexing was introduced by wikipedia:Nicolaas Govert de Bruijn in 1972.
M’colleague Bob Atkey once memorably described the capacity to put up with de Bruijn indices as a Cylon detector, the kind of reverse Turing Test that the humans in Battlestar Galactica invent, the better to recognize one another by their common inadequacies. ~ Conor McBride
Idea
Recall that lambda calculus only has three constructors: abstraction, application, and variable lookup; and consider closed terms for now. Due to lexical scoping, every variable lookup is always scoped: there is a lambda-binder somewhere above the variable which introduces its scope. For example, here's the identity function:
λx.x
But also, here's the identity function:
λy.y
These are quite similar in the sense that they are alpha-equivalent: we can transform one term into another by renaming variables in a scope-respecting manner. It turns out that any scope-respecting renaming must preserve the number of lambda-binders above the variable. The De Bruijn index is merely that number.
Notation
The following notation is common throughout the community and wiki.
Closed terms consist of lambda, parentheses, and numeric indices. Traditionally, as long as there are fewer than ten layers of lambda, application is denoted by parentheses and juxtaposition. For example, the following lambda calculus term:
λx.λy.(xy)
Is notated as the following term with De Bruijn indices:
λλ(21)
Sometimes it can be nice to add whitespace for readability:
λλ(2 1)
And some authors will remove outermost parentheses:
λλ21
Conventions
Should De Bruijn indices start at 0 or 1? De Bruijn used 1-indexing, but many computer scientists working today use 0-indexing. In general, authors will note their convention and often justify it as well, as is the case in De Bruijn 1972.
Examples
The identity function:
λ1
The K combinator:
λλ2
The S combinator:
λλλ((31)(21))
See Also
- wikipedia:De Bruijn index
- De Bruijn 1972, which introduced the concept