Capture-Avoiding Substitution and the Substitution Lemma

Take the term λy. x y, in which x is free and y is bound. Replace the free x with x and nothing changes. Replace it with y instead, and a text editor produces λy. y y. The original function applies its argument to the outer x; the result applies its argument to itself. A textual replacement that a text editor would perform has changed the meaning of the program, and the mechanism responsible is variable capture: the substituted y fell inside the scope of a binder named y, and that binder took ownership of it.

Every serious implementation of the lambda calculus has to prevent this, and the ways of doing so are the subject here. The definition is short, the naive algorithm is wrong in exactly one case, and the repair introduces a lemma that underpins nearly every proof in the field.

The definition and the case that breaks it

Substitution is written M[x := N]: replace every free occurrence of x in M by N. The recursion follows the syntax.

• x[x := N] = N, and y[x := N] = y for a variable y distinct from x.
• (P Q)[x := N] = (P[x := N]) (Q[x := N]).
• (λy. P)[x := N] = λy. (P[x := N]), when y is not x and y does not occur free in N.
• (λx. P)[x := N] = λx. P, because the binder shadows the name.

The third clause carries the side condition, and the fourth exists because the recursion must stop at a shadowing binder. The condition y ∉ FV(N) is precisely what prevents capture: if the bound name y does not appear free in the argument, no free variable of the argument can be swallowed when the argument is placed under the λy.

When the condition fails, the fix is to rename the binder first. (λy. P)[x := N] becomes (λz. P[y := z])[x := N] for a fresh z, and the two steps commute because the renaming does not touch free variables. Freshness is relative to the union of the free variables of P and N plus the bound names in scope, and any name outside a finite set works, which is why the operation is total.

A worked example shows the order matters. Substituting y for x in λy. x y:

(λy. x y)[x := y]
  = λz. ((x z)[x := y])        rename y to fresh z
  = λz. (y z)                  substitute

The result is λz. y z, a function that applies the outer y to its argument. The uncorrected attempt gives λy. y y, which applies its argument to itself. The two terms are not alpha-equivalent and do not behave alike on any argument that distinguishes them.

Two algorithms, one invariant

The recursive definition translates directly into code with a renaming step, and the code is short enough that the invariant is visible.

subst :: String -> Term -> Term -> Term
subst x n (Var y)
  | x == y    = n
  | otherwise = Var y
subst x n (App f a) = App (subst x n f) (subst x n a)
subst x n (Lam y b)
  | y == x            = Lam y b                       -- shadowed, stop
  | y `elem` freeVars n =                   -- capture would occur
      let z = fresh (freeVars b ++ freeVars n ++ [x])
      in Lam z (subst x n (subst y (Var z) b))
  | otherwise         = Lam y (subst x n b)

Two properties are worth stating explicitly because they are the ones a test suite should assert.

Preservation of shape modulo alpha. The result is alpha-equivalent to the term obtained by any other correct substitution strategy. Different implementations pick different fresh names; the equivalence class is the same. This is what makes the operation well defined on equivalence classes rather than on trees, and it is the reason alpha-equivalence has to be settled before substitution can be specified.

No renaming for closed arguments. If N is closed, no capture is possible and no renaming is needed. The third clause of the definition can be applied unconditionally, and the algorithm degenerates to a plain structural walk. An implementation that substitutes only closed terms therefore never reaches the renaming branch.

The naive version, which skips the elem check, is wrong only when the argument has free variables and the binder name collides with one of them. That makes the bug easy to miss in testing: programs that only ever substitute literals and closed lambdas will pass every test. The failure appears when a partially applied function is substituted under a binder, which is exactly what happens during reduction of higher-order terms. The classic demonstration is the term (λx. λy. x) y, which reduces to λy. y by naive substitution, a constant function; correct substitution gives λz. y, a function that ignores its argument and returns the outer y. Those two terms are not equivalent, so the naive rule is not merely inefficient; it computes the wrong function.

Simultaneous substitution

Reduction substitutes one variable at a time, but many algorithms need to substitute several at once: instantiating a type scheme, unfolding a recursive definition with multiple parameters, or applying a list of arguments to a curried function. Simultaneous substitution M[x₁ := N₁, …, x_k := N_k] is not the same as sequential substitution, and the difference is a standard trap.

Consider the term x y under [x := y, y := x]. Done simultaneously, both free variables are replaced at once and the result is y x, the swap of the two. Done sequentially with x := y first, the term becomes y y, and then y := x turns both occurrences into x x. Done in the other order, y := x first gives x x, and then x := y gives y y. Simultaneous substitution alone produces the swap, and that is because each Nᵢ is substituted into the original term, never into the result of another substitution.

The implementation rule follows: substitute all bindings into the argument terms first, then walk the target term once, replacing any free occurrence of a bound name by its corresponding pre-substituted argument, and renaming binders as needed. Each replacement term is put in final form, with the other bindings already applied, before it enters the target. In de Bruijn form, simultaneous substitution is a single traversal with a list of terms and a shift applied at each binder, which is one of the reasons that representation is preferred for implementations.

The substitution lemma

The lemma that ties substitution to reduction is stated as follows. If M, N, and L are terms, x ≠ y, and x is not free in L, then

M[x := N][y := L]  =  M[y := L][x := N[y := L]]

The equation says that substituting N for x and then L for y is the same as substituting L for y first and then substituting, for x, the term N with L already put in place of its free y. Both conditions matter: x ≠ y keeps the two variables distinct, and x ∉ FV(L) stops the first substitution from handing the variable x a term that contains free occurrences of the very name the second substitution is about to replace. In the induction the equation is used up to alpha-equivalence, because binders met on the way down are renamed.

Its importance is disproportionate to its simplicity. It is the step that lets a proof about reduction proceed past a binder: when a reduction happens inside the body of a lambda and the result is later instantiated, the lemma converts the two orders of operation into each other, so the induction hypothesis applies. Preservation of typing, confluence, and the correctness of every abstract machine are proved with it, usually without comment.

There is a second form, often called the substitution lemma for typing: if Γ, x : A ⊢ M : B and Γ ⊢ N : A, then Γ ⊢ M[x := N] : B. Its proof requires the first lemma plus weakening, and its failure would mean that beta reduction breaks type soundness. Systems that get substitution wrong fail this lemma, which is why it is the standard first theorem in any mechanised development.

Substitution as an operation on environments

Textual substitution rewrites the term. An alternative, used by every practical evaluator, is to never rewrite at all: pair the term with an environment mapping names to values or closures, and look up a variable at the moment it is needed. Substitution is then deferred, possibly forever.

The trade is real and quantifiable. Textual substitution costs time proportional to the size of the term each time it is applied, and a naive evaluator can perform it repeatedly on the same subterm. The classic example is Church numeral addition, where substitution copies the function body for each application, giving a cost that grows with the number of applications. Environment-based evaluation costs a lookup per variable access, typically a small constant or a short linked-list walk, and never copies the body. For a term of size n evaluated with m reductions, the difference is between O(n·m) and O(m) work, ignoring the cost of allocating closures.

The price is that terms and environments become mutually recursive data, and the resulting structure is a closure, not a term. Reduction no longer produces a term; it produces a value, which may be a closure holding a pointer to an unevaluated body and an environment. That is fine for an interpreter and awkward for anything that needs to inspect the result, which is why normalisation and printing require an extra step that forces closures back into syntax. The details belong with the machines that implement this strategy, covered in the abstract machines for reduction.

There is a middle path used in proof assistants: explicit substitutions. The term language is extended with a constructor for a suspended substitution, and the calculus gains rules for pushing substitutions under binders and applying them to variables. This makes the step from one term to another small and local, at the cost of adding reduction rules and losing the clean statement that terms are the only objects. Implementations that need to record every intermediate state of a proof find the trade worthwhile; interpreters generally do not.

Where implementations go wrong

Four failure modes recur, and all are visible in the definitions above.

The first is treating the shadowing case as an optimisation rather than a rule. (λx. P)[x := N] must return the lambda unchanged; an implementation that recurses into P will replace occurrences that belong to the inner binder, silently changing the meaning of every term with nested same-name binders.

The second is choosing a fresh name that is not actually fresh. Freshness must be checked against the free variables of both the body and the argument, and against names already introduced by outer renamings during the same traversal. A generator that increments a counter per traversal without consulting the term can collide with a name that appears in the argument.

The third is applying the renaming after the substitution instead of before. Renaming λy. P to λz. P[y := z] and then substituting for x works; substituting first and renaming afterwards may already have captured the variable, and the later renaming cannot undo it.

The fourth is forgetting that substitution into an application is not commutative with reduction. Substitution is defined on terms, not on values; substituting into a term that has a redex does not reduce that redex, and implementations that interleave the two must be explicit about which order they guarantee. Beta reduction and evaluation order takes up that order directly, since beta reduction is the rule that consumes the results of substitution and the choice of where to apply it first determines whether a program terminates at all.