Alpha-Equivalence and de Bruijn Indices in the Lambda Calculus

The lambda calculus has three syntactic forms and no primitive data. A term is a variable, an application of one term to another, or an abstraction over a variable. Everything else, including numbers, pairs, and recursion, is built from those three. That economy is the point of the system, and it is also why the first implementation problem appears immediately: the only operation that does real work, substitution, is defined on terms whose variable names are supposed to be irrelevant.

An editor, a type checker, or a compiler pass that compares two terms must decide whether they are the same term. Character-by-character comparison answers the wrong question, because λx. x and λy. y are the same function written twice. A correct comparison has to see through the names, and the standard way to make that cheap is to stop storing them.

Binders, scope, and free variables

The grammar is usually written with two conventions that remove most parentheses. Application associates to the left, so M N P means (M N) P. Abstraction extends as far to the right as possible, so λx. λy. x y means λx. (λy. (x y)) and not (λx. λy. x) y. Under those conventions the term λx. λy. x y x is unambiguous.

A variable occurrence is bound if it sits inside the body of an abstraction that names it, and free otherwise. The body of λx. M is everything after the dot, and an occurrence of x there is bound by that lambda unless an inner binder re-binds the same name. So in λx. x (λx. x), both occurrences of x are bound, but by different binders: the outer one for the left occurrence, the inner one for the right.

The set of free variables is defined by recursion:

• FV(x) = {x}
• FV(M N) = FV(M) ∪ FV(N)
• FV(λx. M) = FV(M) \ {x}

A term with no free variables is closed, and closed terms are also called combinators. Openness matters because substitution only ever concerns free occurrences: replacing x inside λx. M is a no-op, since the inner binder shadows the name. Every implementation bug in this area is some version of failing to respect that shadowing.

The equivalence that names hide

Two terms are alpha-equivalent when they differ only in the names chosen for bound variables. The relation is the least congruence containing the axiom

λx. M  ≡α  λy. M[x := y]      provided y is not free in M

and it is an equivalence relation compatible with application and abstraction. The side condition is not decoration. Without it, λx. λy. x would be identified with λy. λy. y: renaming the outer binder to y captures the inner binder y, which was a different variable, and the two terms no longer compute the same function. With the condition, the renaming has to pick a name that does not already occur free, which is always possible because a finite term mentions finitely many names.

The practical consequence is that a term denotes an equivalence class, not a syntax tree. λx. λy. x and λa. λb. a are the same class, and both are the standard encoding of the constant-true function. λx. λy. y is a different class, the constant-false function, even though it has the same binder shape. Deciding the relation is straightforward: walk both terms at once, keep a map from each bound name to a binder identity, and compare identities at the leaves. The traversal is O(n) in the size of the terms and needs no renaming at all; the map costs O(d) space in the nesting depth, and a scope-ordered stack gives the same bound.

What it costs is memory and sharing. If the representation stores names as strings, every binder carries a pointer plus characters, and two alpha-equivalent terms produce two distinct trees that cannot be hash-consed together. A compiler that interns terms to share common subexpressions will find that λx. x and λy. y hash differently and are stored twice.

Counting binders instead of naming them

de Bruijn’s alternative, published in 1972, removes names from bound occurrences entirely. Each bound variable becomes a natural number: the number of binders between the occurrence and the binder that introduces it. The innermost enclosing binder is 0, the next one out is 1, and so on.

Named term	Nameless term
λx. x	λ. 0
λx. λy. x	λ. λ. 1
λx. λy. y	λ. λ. 0
λx. x x	λ. 0 0
λx. λy. x y	λ. λ. 1 0

Read the last row from the inside out. In λ. λ. 1 0, the 0 sits under two binders and refers to the nearest one, so it is the y; the 1 skips one binder and refers to the outer x. The fourth row is the one to check against the first: λx. x x becomes λ. 0 0, both occurrences pointing at the same binder, and its alpha-variant λz. z z produces exactly the same tree. Free variables are where the encoding needs a convention, since a free occurrence has no binder to count to. Implementations either require terms to be closed, or add a separate constructor for free variables that carries a name, or treat an index that runs past the enclosing binders as a free variable numbered from the top. The locally nameless style takes the second option, and it is the one that keeps opening and closing binders total.

The representation also has a second, easily confused coordinate. An index counts upward from an occurrence to its binder, which is what the table above shows. A level counts downward from the root to a binder, so each binder has a fixed level for its whole scope. Levels are useful in evaluators, where the environment is an array and a binder at level k is stored at slot k, giving O(1) lookup. Indices are useful in terms, because they are stable under substitution deeper in the term. Confusing the two produces an off-by-one error at every binder boundary, and the resulting terms usually still look plausible.

The storage difference is modest but real. An index is a machine word, and small indices fit in a tagged immediate with no allocation at all. A name is a pointer plus a string, typically interned to avoid duplicating the characters, so at minimum 8 bytes per occurrence plus the intern table entry. For a term with a million nodes, the difference between 8 bytes and 0 bytes per node is 8 MB of live data, which is the difference between fitting in a cache-friendly arena and not.

Shift, and why substitution needs it

Removing names creates one obligation. When a term is moved under a binder, every free index in it must increase by the number of binders crossed, or it will point at the wrong binder. The operation that performs this adjustment is called shift, written ↑ with a cutoff and a delta.

data Term = Var Int | Lam Term | App Term Term

-- shift every index >= cutoff by delta
shift :: Int -> Int -> Term -> Term
shift c d (Var i) | i >= c    = Var (i + d)
                  | otherwise = Var i
shift c d (Lam t) = Lam (shift (c + 1) d t)
shift c d (App f a) = App (shift c d f) (shift c d a)

The cutoff is what makes the operation compositional. Without it, shifting a term would also renumber indices that refer to binders outside the term, which is wrong: those binders did not move. Entering a lambda raises the cutoff by one, because everything below that point is now one binder deeper.

Substitution is written in terms of shift. The parameter j is the index being replaced, counted at the current depth, and s is the replacement term:

subst :: Term -> Int -> Term -> Term
subst s j (Var i) | i == j    = s                           -- replaced
                  | otherwise = Var i
subst s j (Lam t) = Lam (subst (shift 0 1 s) (j + 1) t)     -- s lifted under the binder
subst s j (App f a) = App (subst s j f) (subst s j a)

-- beta: substitute the argument for the binder, then drop the binder
beta :: Term -> Term -> Term
beta (Lam body) arg = shift 0 (-1) (subst (shift 0 1 arg) 0 body)

The argument is shifted up by one before the traversal begins, because the traversal descends under the binder while the argument does not: without the shift, its free indices would point one binder too shallow. Inside the traversal, entering a Lam shifts the substituted term again for the same reason, and raises the target index. Finally the binder is removed, so every remaining index above it must come down by one, which is the negative shift applied outside. Getting any of these wrong produces a term that is well formed and refers to the wrong binder, and the error surfaces far from its cause.

What the nameless representation gives up

Nothing about the calculus changes, but the human interface does. Error messages and debuggers need names, and a nameless term has none. Two workarounds are common. The first keeps a name hint on each binder, used only when printing and ignored by equality and substitution; hints may be stale after reduction, which is acceptable because they are not part of the term. The second is the locally nameless representation, which stores bound variables as indices and free variables as names. Opening a binder with a fresh name is then a total operation, substitution of a closed term needs no shift at all, and free variables remain printable. The cost is a more complicated invariant: a term is only well formed if every index is in scope, and every operation must preserve that.

The failure modes are worth naming because they are easy to hit. Substituting an open term into a context with fewer binders can leave a free index that collides with a binder, producing a term that looks fine and means something else. Printing a term after substitution without renumbering the hints produces misleading output. And any traversal that treats Lam as a node without adjusting the cutoff will shift indices that should have been left alone. These are not deep errors; they are the reason the shift function is written once, carefully, and reused everywhere.

Deciding equality in practice

For a compiler pass that compares terms, the nameless representation reduces equality to a structural walk with no environment, no allocation, and no hash collisions between distinct names. It also makes hashing meaningful: the hash of a term is the hash of its structure, so alpha-equivalent subterms always share a bucket and can be merged. With names, the same merge requires normalising names first, which is the traversal the indices were meant to avoid.

The price is paid at the boundaries: parsing produces names, printing consumes them, and every interface to a human has to reconstruct them. Inside those boundaries, the term is a tree of integers and applications, and the equivalence that the theory takes for granted is the same equality the runtime already knows how to compute. The next operation to build on this representation is capture-avoiding substitution, which is where the side conditions of alpha-renaming turn into an algorithm, and then beta reduction, which is the only rewrite rule the system has.