Free & Bound Variables and Substitution
The one rule that makes the lambda calculus run is β-reduction, and its whole content is a
single act: substitute the argument for the parameter in the function body. It sounds like
find-and-replace. It is not. Get substitution subtly wrong — as every implementer has at least once —
and your interpreter will silently compute the wrong answer, changing the meaning of a program without
raising a single error. This lesson defines substitution correctly, which first requires us to
say precisely which variables a term uses and which it merely mentions.
The distinction is exactly the one logic draws between the x in
\forall x.\, P(x) — bound by the quantifier — and a stray
x that refers to something outside. In the lambda calculus the
\lambda is the binder, and everything about scope, α-equivalence and
capture flows from getting free versus bound right.
Free variables, defined by recursion on the term
A variable occurrence is bound if it lies within the body of a
\lambda that names it, and free otherwise. The set
\mathrm{FV}(M) of free variables of a term is defined by structural
recursion over the three constructors:
\mathrm{FV}(x) = \{x\}, \qquad
\mathrm{FV}(M\ N) = \mathrm{FV}(M) \cup \mathrm{FV}(N), \qquad
\mathrm{FV}(\lambda x.\, M) = \mathrm{FV}(M) \setminus \{x\}.
The abstraction case is the interesting one: wrapping a term in \lambda x
removes x from the free set, because that
\lambda now binds every x beneath it. A term with
no free variables — \mathrm{FV}(M) = \varnothing — is called
closed, or a combinator; closed terms are the self-contained programs
of the calculus. In \lambda x.\, x\ y the occurrence of
x is bound while y is free, so
\mathrm{FV}(\lambda x.\, x\ y) = \{y\}.
Binding, drawn on the tree
On the AST, a variable's status is a question about its ancestors: an occurrence of
x is bound by the nearest enclosing \lambda x on
the path to the root, and free if there is none. Here is
\lambda x.\, (x\ (\lambda y.\, x\ y))\ z; step through to see each leaf
classified and each binding arrow drawn.
The two x leaves both resolve to the outer
\lambda x (dashed arrows); the y leaf resolves to
the inner \lambda y; and z has no binder above it,
so it is free. Hence \mathrm{FV} = \{z\}. Reading binding off the tree like
this is exactly what a correct substitution algorithm must do — it may only touch the
free occurrences of the variable it is replacing.
α-conversion: names are irrelevant
The name of a bound variable carries no meaning — it is a local placeholder. Renaming it
consistently throughout its scope is α-conversion, and two terms that differ only by
such renamings are α-equivalent, written M =_\alpha N. Thus
\lambda x.\, x \;=_\alpha\; \lambda y.\, y \;=_\alpha\; \lambda z.\, z ,
all three being "the identity function". α-conversion is legal only when the new name is
fresh for the body — renaming \lambda x.\, \lambda y.\, x to
\lambda y.\, \lambda y.\, y is illegal, because the outer
x would be captured by the inner binder and change meaning. From here on we
follow Barendregt's variable convention: we always assume the bound variables of the
terms in a discussion are chosen distinct from the free variables (and from each other), silently
α-renaming when needed. This convention is what lets us pretend substitution is simple even though its
honest definition is not.
Capture-avoiding substitution, case by case
We write M[x := N] for "the term M with every
free occurrence of x replaced by
N." Its full definition, by recursion on M, has
five cases — and the last is where all the subtlety lives:
\begin{aligned}
x[x := N] &= N \\
y[x := N] &= y && (y \neq x) \\
(M_1\, M_2)[x := N] &= (M_1[x := N])\,(M_2[x := N]) \\
(\lambda x.\, M)[x := N] &= \lambda x.\, M && \text{(x is re-bound: stop)} \\
(\lambda y.\, M)[x := N] &= \lambda y.\, (M[x := N]) && (y \neq x,\ y \notin \mathrm{FV}(N))
\end{aligned}
Walk the cases. A variable equal to x becomes N;
any other variable is untouched; application distributes into both subterms. For abstraction, if the
bound variable is x, we stop — the inner
\lambda x shadows the substitution, so no free
x remains below. And if the bound variable is some other
y, we may descend into the body only when
y \notin \mathrm{FV}(N). That side condition is the crux.
The capture problem
Why the side condition? Suppose we ignore it and compute
(\lambda y.\, x)[x := y] by blind replacement. We would get
\lambda y.\, y — the identity function. But the original term was the
constant function returning the free x, and after substituting the
argument y we should still have a constant function returning that
y. The free y we substituted in got
captured by the inner binder \lambda y and silently changed
from "the outside value" to "the bound parameter". Meaning was destroyed with no error raised.
The repair is to α-rename before descending. When the fifth clause's side condition
fails (y \in \mathrm{FV}(N)), first rename the bound
y to a fresh y' not occurring in
M or N, then proceed:
(\lambda y.\, x)[x := y] \;=_\alpha\; (\lambda y'.\, x)[x := y] \;=\; \lambda y'.\, y .
Now the result is a genuine constant function returning the outer y —
correct. This is capture-avoiding substitution: substitution that renames bound variables just
enough to keep every free variable of N free after the copy.
If x \neq y and x \notin \mathrm{FV}(L), then
for all terms M,
M[x := N][y := L] \;=\; M[y := L]\,[\,x := N[y := L]\,].
This equation — that substitutions may be reordered provided their variables do not interfere — is
the workhorse behind proofs of confluence and type soundness. Its proof is a routine but instructive
structural induction on M.
Substitution in code
Here is capture-avoiding substitution implemented faithfully in TypeScript: freeVars
computes \mathrm{FV}, fresh mints a name avoiding a given set,
and subst follows the five clauses, α-renaming exactly when a bound variable would capture
a free variable of the replacement. Press Run and watch the capture case rename
y to y'.
type Term =
| { tag: "var"; name: string }
| { tag: "abs"; param: string; body: Term }
| { tag: "app"; fn: Term; arg: Term };
const v = (name: string): Term => ({ tag: "var", name });
const lam = (param: string, body: Term): Term => ({ tag: "abs", param, body });
const app = (fn: Term, arg: Term): Term => ({ tag: "app", fn, arg });
function freeVars(t: Term): Set<string> {
switch (t.tag) {
case "var": return new Set([t.name]);
case "app": return new Set([...freeVars(t.fn), ...freeVars(t.arg)]);
case "abs": { const s = freeVars(t.body); s.delete(t.param); return s; }
}
}
// A name not in `avoid`: y, y', y'', ...
function fresh(base: string, avoid: Set<string>): string {
let name = base;
while (avoid.has(name)) name += "'";
return name;
}
// M[x := N], capture-avoiding.
function subst(M: Term, x: string, N: Term): Term {
switch (M.tag) {
case "var":
return M.name === x ? N : M;
case "app":
return app(subst(M.fn, x, N), subst(M.arg, x, N));
case "abs": {
if (M.param === x) return M; // x re-bound: stop
if (!freeVars(N).has(M.param)) // safe: descend directly
return lam(M.param, subst(M.body, x, N));
// capture would occur: α-rename the bound variable first
const y2 = fresh(M.param, new Set([...freeVars(N), ...freeVars(M.body), x]));
const renamed = subst(M.body, M.param, v(y2));
return lam(y2, subst(renamed, x, N));
}
}
}
function show(t: Term): string {
switch (t.tag) {
case "var": return t.name;
case "abs": return `λ${t.param}. ${show(t.body)}`;
case "app": {
const f = t.fn.tag === "abs" ? `(${show(t.fn)})` : show(t.fn);
const a = t.arg.tag === "var" ? show(t.arg) : `(${show(t.arg)})`;
return `${f} ${a}`;
}
}
}
// Safe case: (λz. x z)[x := (a b)] — z does not occur free in the replacement.
const safe = lam("z", app(v("x"), v("z")));
console.log("safe :", show(subst(safe, "x", app(v("a"), v("b")))));
// λz. (a b) z
// Capture case: (λy. x)[x := y] — naive replace would capture y.
const risky = lam("y", v("x"));
console.log("capture:", show(subst(risky, "x", v("y"))));
// λy'. y (bound y renamed to y', outer y stays free)
The fresh/α-rename branch fires precisely when the replacement's free variables would
collide with a binder — turning the treacherous λy. y into the correct
λy'. y. Every real interpreter, compiler and proof assistant contains a version of this
function; getting it right is a rite of passage.
α-renaming is a persistent nuisance: equal functions look different, and substitution has to
manufacture fresh names. In 1972 Nicolaas de Bruijn proposed erasing names altogether.
Replace each variable occurrence by a number — how many \lambdas you
must cross, outward, to reach the one that binds it. The identity \lambda x.\, x
becomes \lambda.\, 0; the constant \lambda x.\, \lambda y.\, x
becomes \lambda.\, \lambda.\, 1; and
\lambda x.\, \lambda y.\, y becomes \lambda.\, \lambda.\, 0.
The payoff is enormous: α-equivalent terms become literally identical, so equality is
just syntactic comparison and capture cannot happen — there are no names left to capture. The cost is
that substitution must shift indices as it crosses binders, which is fiddly in its own way.
Nearly every serious implementation (Coq's kernel, GHC Core in places, most textbook interpreters)
uses de Bruijn indices or a "locally nameless" hybrid precisely to sidestep the capture problem this
lesson is about.
The classic error is to replace every occurrence of the variable, ignoring shadowing.
Consider (\lambda x.\, x)[x := N]. The x inside is
bound by the local \lambda x — it is not the same
x we are substituting for. The correct result is
\lambda x.\, x, unchanged (clause four: "x re-bound, stop"), not
\lambda x.\, N.
The mirror-image error is to forget the capture check and let a free variable of
N slip under a binder that names it, as in the
(\lambda y.\, x)[x := y] = \lambda y.\, y disaster above. Both mistakes come
from treating substitution as textual replacement. It is not textual — it is defined relative to
binding structure. When you compute by hand, first mark which occurrences are free; substitute
only those; and α-rename any binder that would otherwise capture.