Substitution, Capture, and Alpha-Equivalence

Free variables and substitution

$\Pi$ and $\lambda$ bind their variable: in $\tLam{x}{A}{t}$, occurrences of $x$ inside $t$ refer to the argument. The binder's scope is the body only; $x$ is not bound in the annotation $A$. A variable occurrence that is not bound by an enclosing $\Pi$ or $\lambda$ is free.

For example, $\FV(\tLam{x}{P}{f\;x\;y}) = \{P, f, y\}$, and $\FV(\tPi{P}{\Sort{0}}{P \to P}) = \emptyset$, so the latter is a closed term. Constants are never bound, so they contribute nothing.

The explorer colours each bound variable like its binder and underlines free ones; hover a variable to see its binder. Try a term with shadowing, such as fun (x : A) => fun (x : A) => x.

We write $\subst{t}{x}{s}$ for the result of replacing the free occurrences of $x$ in $t$ with $s$. Binders make this subtle: in $\subst{(\tLam{y}{A}{x})}{x}{y}$, the body means "ignore the argument and return the outer $x$". Replacing $x$ with $y$ naively gives $\tLam{y}{A}{y}$, the identity function, because the binder has captured the formerly free $y$. To preserve the meaning, substitution must rename the binder first.

The following examples exercise each binder case.

In the last example, the free $y$ of the replacement still refers to the outer $y$, and the bound variable, now $z$, still refers to the argument. Without the renaming, the result would be $\tLam{y}{A}{f\;y\;y}$, which passes its argument twice. The explorer performs both substitutions side by side; the colours show whether the $y$ in the result is the free one from the replacement or the one the binder captured.

Variable capture in contexts

It is tempting to drop the side condition $x \notin \dom(\Gamma)$ of C-Ext and let a new assumption simply shadow an old one, as most programming languages do. Doing so makes the kernel unsound. Consider

The variable $y$ has the outer $x$ as its type, and the innermost $\lambda$ ignores its argument. So the correct type of $t$ is

A checker without $\Freshen$ looks up $y$ in the context $x : \Sort{0},\; y : x,\; x : \Sort{0}$ and returns its type, the bare name $x$. At that point $x$ refers to the inner binder, and the checker returns

which says "from any element of any type, produce an element of every type". Given $A : \Sort{0}$ and $a : A$, the term $t\;A\;a$ then has type $\tPi{B}{\Sort{0}}{B}$, a proof of False. Such $A$ and $a$ exist even in the empty context: $A = \tPi{P}{\Sort{0}}{P \to P}$ is itself a proposition, and the identity function $a = \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}}$ proves it.

With $\Freshen$, the innermost binder is renamed to $x'$ before it enters the context, so the context becomes $x : \Sort{0},\; y : x,\; x' : \Sort{0}$, the lookup of $y$ returns $x$, which still refers to the outer binder, and $\Infer$ returns the correct type above. The derivation explorer shows the renaming happen: the note on the innermost T-Lam node reports it, and the context of the leaf contains $x'$.

# The kernel renames the inner x to x' and infers the correct type.
# A kernel that let the inner x shadow the outer one would accept this
# as a proof of the second statement, which is false.
goal forall (x : Sort 0), forall (y : x), forall (x' : Sort 0), x
exact fun (x : Sort 0) => fun (y : x) => fun (x : Sort 0) => y
qed
goal forall (x : Sort 0), forall (y : x), forall (x' : Sort 0), x'
exact fun (x : Sort 0) => fun (y : x) => fun (x : Sort 0) => y
qed

The problem is the same as in substitution: a name is moved into a scope where it means something else. It affects any representation that identifies variables by name, whether the context is a list or a hash map. There are three common remedies.

1. Reject shadowing outright. This is the simplest option, but the reserved name _ used by $A \to B$ must be exempt and never added to the context.
2. Rename on entry, as $\Freshen$ does. This is our choice.
3. Represent bound variables by position (de Bruijn indices [de Bruijn 1972]) or use the locally nameless style, in which bound variables are indices and free variables carry unique identifiers. Lean 4 takes the latter approach.

A test suite should include $t$ above and check that the kernel either rejects it or assigns it the correct type.

Alpha-equivalence

The names of bound variables carry no meaning. $\tLam{x}{A}{x}$ and $\tLam{y}{A}{y}$ are the same function, and $\tPi{P}{\Sort{0}}{P \to P}$ and $\tPi{Q}{\Sort{0}}{Q \to Q}$ are the same proposition. Terms that differ only in the names of bound variables are called alpha-equivalent. A kernel cannot compare types with plain syntactic equality, which would reject the second pair.

(A congruence is an equivalence relation that is preserved by every term constructor: if the parts are related, so are the wholes.) This definition is easy to state but not directly executable, since it does not say which names to choose. An implementation instead walks both terms in lockstep and remembers, for each side, the list of binders passed so far. A bound variable is then identified by which binder it refers to, not by its name.

To describe this walk, we use a judgment of the form $E_1; E_2 \vdash s \alphaeq t$, where $E_1$ and $E_2$ are lists of names. The list $E_1$ records the binders that enclose $s$, from the outermost to the innermost, and $E_2$ records those that enclose $t$. The judgment reads: "$s$, placed inside the binders $E_1$, and $t$, placed inside the binders $E_2$, are the same term up to the names of bound variables". Two lists are needed because the two terms may use different names for corresponding binders. For example, comparing $\tLam{x}{A}{\tLam{y}{B}{x}}$ with $\tLam{a}{A}{\tLam{b}{B}{a}}$ passes two binders on each side and arrives at

which holds because $x$ and $a$ both refer to the outer of the two binders. Comparing two whole terms starts from empty lists, $\cdot\,;\cdot \vdash s \alphaeq t$.

To say "the same binder" precisely, let $\mathrm{idx}(E, x)$ be the position of the last occurrence of $x$ in $E$, counted from the right starting at $0$, or undefined if $x \notin E$. In the example, $\mathrm{idx}((x, y), x) = \mathrm{idx}((a, b), a) = 1$. Taking the last occurrence handles shadowing: in $\tLam{x}{A}{\tLam{x}{B}{x}}$ the body refers to the inner $x$.

Free variables are compared by name ($\alpha$-Free), bound variables by position ($\alpha$-Bound), and constants by name ($\alpha$-Const). A variable that is bound on one side and free on the other is never equal to anything, which is why there is no rule for that case. Because both sides descend through binders together, $E_1$ and $E_2$ always have the same length. So comparing positions counted from the right is the same as comparing positions counted from the left, and an implementation may store each list as a map from names to binding depths, provided it restores the previous entry when it leaves a binder. Using positions instead of names everywhere gives the de Bruijn representation, in which alpha-equivalent terms are syntactically identical.

Examples

The first example of Chapter 6 ended by comparing the inferred type with the stated one, where $P \to P$ abbreviates $\tPi{\_}{P}{P}$:

• $\cdot\,;\cdot \vdash \tPi{P}{\Sort{0}}{\tPi{h}{P}{P}} \alphaeq \tPi{P}{\Sort{0}}{\tPi{\_}{P}{P}}$ $\alpha$-Pi
  • $\cdot\,;\cdot \vdash \Sort{0} \alphaeq \Sort{0}$: holds $\alpha$-Sort
  • $P;\, P \vdash \tPi{h}{P}{P} \alphaeq \tPi{\_}{P}{P}$ $\alpha$-Pi
    • $P;\, P \vdash P \alphaeq P$: holds, both have index $0$ $\alpha$-Bound
    • $P, h;\; P, \_ \vdash P \alphaeq P$: holds, both have index $1$ $\alpha$-Bound

The names $h$ and $\_$ differ, but neither is ever looked up, so they do not matter. The wrong proof of Chapter 6 fails at the last step instead:

• $\cdot\,;\cdot \vdash \tPi{P}{\Sort{0}}{\tPi{h}{P}{\Sort{0}}} \alphaeq \tPi{P}{\Sort{0}}{\tPi{\_}{P}{P}}$ $\alpha$-Pi
  • $\cdot\,;\cdot \vdash \Sort{0} \alphaeq \Sort{0}$: holds $\alpha$-Sort
  • $P;\, P \vdash \tPi{h}{P}{\Sort{0}} \alphaeq \tPi{\_}{P}{P}$ $\alpha$-Pi
    • $P;\, P \vdash P \alphaeq P$: holds $\alpha$-Bound
    • $P, h;\; P, \_ \vdash \Sort{0} \alphaeq P$: no rule applies

Positions also tell apart terms that a careless comparison of names would confuse. $\tLam{x}{A}{\tLam{y}{A}{x}}$ and $\tLam{a}{A}{\tLam{b}{A}{b}}$ are not alpha-equivalent: the bodies reach $x, y;\, a, b \vdash x \alphaeq b$, and $\mathrm{idx}$ gives $1$ for $x$ but $0$ for $b$. Conversely, $\tLam{x}{A}{\tLam{x}{A}{x}}$ and $\tLam{a}{A}{\tLam{b}{A}{b}}$ are alpha-equivalent, because the last occurrence of $x$ in $(x, x)$ has index $0$, the same as $b$ in $(a, b)$.

The rules of Figure 11.1 are a different definition from Definition 11.3, so we must check that they agree.

The idea of the proof is that both sides say the same thing: $s$ and $t$ have the same de Bruijn representation. For the algorithm this is almost immediate, since its rules compare positions exactly as de Bruijn indices do. For Definition 11.3, the key fact is that renaming a bound variable does not change the de Bruijn representation. Appendix B gives the full proof.

Exercises