Capture Avoidance

What goes wrong with naive substitution. Why $\alpha$-conversion is needed.

10 topics • ~1116 words

A type piece you want to insert contains a tag -- say y. But the composing stick already has an inner stick whose blanks are tagged y. If you insert the type piece as-is, the tag on the piece gets "captured" by the inner stick's instruction -- it fills the wrong blank. The piece's y was supposed to reference something outside, but now it is trapped inside.

Substitution is the engine of computation in lambda calculus. But the definition we have learned so far has a dangerous edge case. If we are not careful, substitution can silently change the meaning of a term. This concept explains what goes wrong and how to fix it.

The Capture Problem

Consider the substitution (λy.x)[x := y]. Naively, we replace the free x with y, giving λy.y. But this is wrong.

Before: λy.x is a function that ignores its argument and returns whatever x refers to externally.
After (naive): λy.y is the identity function -- it returns its argument.

The free variable y in the substituted term got captured by the binder λy. A variable that was supposed to stay free became bound. This changes the meaning of the term entirely.

Naive Substitution Fails

Here is a concrete example of capture in action.

Start with (λx.λy.x)[x := y]. The term λx.λy.x is a function that takes x and returns a constant function that always returns x.

Naive substitution replaces the free x in λy.x with y: λy.y -- but now the free y we inserted is bound by λy.

Before: λy.x ignores its argument and returns external x
After (naive): λy.y returns its argument -- the identity

The substitution changed the meaning of the inner function.

What Is Variable Capture?

Variable capture is the name for this specific error: a free variable in the substituted term accidentally becomes bound by a binder already present in the body.

In (λy.x)[x := y]:

y is free in the argument y
λy is a binder in the body λy.x
After naive substitution, the free y falls inside λy's scope
Result: λy.y -- the free y is now bound. Captured.

Capture happens when the argument contains a free variable whose name matches a binder in the body where the substitution lands.

Is This Capture?

To check whether a substitution M[x := N] risks capture, ask:

Does N contain any free variables?
Does any free variable in N share a name with a binder in M that is in scope where x appears?

If both answers are yes, naive substitution would cause capture.

(λy.x)[x := y] -- y is free in the argument, λy binds in the body where x appears. Capture risk.

(λy.x)[x := a] -- a is free in the argument, but no binder in the body uses a. No capture risk.

The Fix -- Alpha-Rename First

Before inserting a type piece tagged y into a stick whose inner stick uses y blanks, relabel the inner stick's blanks to a fresh tag -- say z. Now the piece's y passes through safely, and the inner stick's blanks still work with their new label.

The fix for variable capture is simple: $\alpha$-rename the conflicting binder before substituting.

(λy.x)[x := y] has a capture risk because the argument y matches the binder λy. So rename λy to a fresh name first:

$\alpha$-rename λy.x to λz.x (rename the binder from y to z)
Now substitute: (λz.x)[x := y] = λz.y

The result λz.y correctly keeps y free. The function still ignores its argument (now called z) and returns the external y. This is the right answer.

Safe Substitution

Capture-avoiding substitution follows two steps when there is a conflict:

$\alpha$-rename the conflicting binder to a fresh name
Substitute as usual

Example: (λx.λy.x)[x := y]

The free x appears inside λy's scope
The argument y matches the binder λy -- capture risk
Rename λy to λz: the body becomes λz.x
Substitute: (λz.x)[x := y] = λz.y

The result λz.y is correct: a function that ignores its argument z and returns the external y.

When Does Capture Happen?

Not every substitution risks capture. Capture requires a specific collision: a free variable in the argument must share a name with a binder in the body that is in scope where the replaced variable appears.

Capture risk:

(λy.x)[x := y] -- free y in argument, λy in body

No capture risk:

(λy.x)[x := a] -- free a in argument, but no λa in body
(λy.y)[y := a] -- y is bound, not being replaced
x[x := a] -- no binders at all

If the argument has no free variables, or its free variables do not collide with any binder in the body, substitution is safe.

No Capture Risk Here

Most substitutions do not require capture avoidance. When the argument's free variables do not collide with any binder in the body, you can substitute directly.

(λy.x)[x := a]

The argument is a (free variable)
The body's binder is λy -- which binds y, not a
No collision, so substitute directly: λy.a

(λy.x y)[x := a]

The argument a does not match the binder λy
Substitute directly: λy.a y

$\alpha$-renaming is only needed when there is a genuine name collision between the argument's free variables and the body's binders.

Result After Renaming

Putting it all together: when you see a substitution that risks capture, the procedure is:

Identify the conflict (which free variable matches which binder)
$\alpha$-rename the conflicting binder to a fresh name
Perform the substitution on the renamed term

Example: (λx.λy.x)[x := y]

Conflict: free y in argument, binder λy in body
Rename λy to λz: body becomes λz.x
Substitute: (λz.x)[x := y] = λz.y

The answer is a lambda expression -- but short enough to type.

Why Capture Avoidance Matters

Capture avoidance is not an optional safeguard or an edge-case workaround. It is part of the correct definition of substitution.

Without it, substitution can turn a constant function into the identity, or change which external value a term references. If substitution changes meaning, then $\beta$-reduction changes meaning, and computation itself becomes unreliable.

The full rule for substitution into an abstraction is:

(λy.M)[x := N] = λy.(M[x := N]) if y is not free in N (λy.M)[x := N] = λz.(M[y := z][x := N]) if y is free in N

where z is a fresh variable. The second case is capture avoidance: rename the binder, then substitute.

Ready to test your understanding?

Bitwit uses spaced repetition to help you truly master concepts like this—not just read about them. Each card generates with different values, so you can't just memorize answers.

Practice Capture Avoidance →