Basics of Substitution and Alpha-Equivalence

1Introduction

This lecture defines the operation that replaces only the free occurrences of a variable by a term. Naive textual replacement may accidentally bind a free variable, so bound variables must sometimes be renamed to avoid variable capture. Alpha-equivalence formalizes these harmless renamings.

2Substitution and capture

$M[x:=N]$M[x:=N] denotes the result of replacing the free occurrences of $x$x in $M$M by the term $N$N. Bound occurrences are not targets of substitution. For example,

By contrast, mechanically turning $(\lambda y.x)[x:=y]$(\lambda y.x)[x:=y] into $\lambda y.y$\lambda y.y makes the inserted occurrence of $y$y bound by $\lambda y$\lambda y, although it was free before insertion. This change is variable capture. The correct result first renames the binder and is $\lambda z.y$\lambda z.y.

3Fresh variables

For a finite set of terms $S$S, a variable $z$z is fresh for $S$S if its name occurs in none of the terms in $S$S. Because $\text{[PARSE ERROR: Undefined("Command("mathcal")")]}V$\mathcal V is infinite and finitely many terms contain only finitely many variable names, a fresh variable can always be chosen. Below, $z$z is chosen not to occur in either $M$M or $N$N, avoiding ambiguity during renaming.

4Capture-avoiding substitution

Capture-avoiding substitution is defined recursively on syntax:

There are three abstraction cases:

where $z$z in the last clause is fresh for both $M$M and $N$N. More precisely, if $x\notin \mathrm{F}\mathrm{V}\left(M\right)$x\notin\mathrm{FV}(M), the result is $M$M itself and no renaming is needed; the last clause need only be applied when $x\in \mathrm{F}\mathrm{V}\left(M\right)$x\in\mathrm{FV}(M).

For example, choosing $z$z fresh and distinct from $x,y$x,y gives

The inserted occurrence of $y$y remains free in the result.

5Alpha-conversion and alpha-equivalence

Alpha-conversion simultaneously renames a binder and the occurrences that it binds to a fresh variable. If $y\notin \mathrm{F}\mathrm{V}\left(M\right)$y\notin\mathrm{FV}(M), then

where the substitution on the right is capture-avoiding. Alpha-equivalence ${=}_{\alpha }$=_\alpha is the least congruence relation that permits this elementary renaming in any subterm and is reflexive, symmetric, and transitive. Consequently,

but free variables cannot be renamed, so $\lambda x.xy\text{[PARSE ERROR: Undefined("Command("not")")]}{=}_{\alpha }\lambda x.xz$\lambda x.x\;y\not=_\alpha\lambda x.x\;z. Moreover, $\lambda x.\lambda y.x\text{[PARSE ERROR: Undefined("Command("not")")]}{=}_{\alpha }\lambda x.\lambda y.y$\lambda x.\lambda y.x\not=_\alpha\lambda x.\lambda y.y: alpha-equivalence preserves binding structure.

6Connection to beta-reduction

Beta-reduction is defined by

using capture-avoiding substitution on the right. For example,

not $\lambda y.y$\lambda y.y. Different choices of a fresh variable may produce different spellings, but all resulting terms are alpha-equivalent.

7Related links