Substitution

Definition

Substitution is the operation of replacing all free occurrences of a variable in an Expression with another expression. In Type Theory, substitution is written $e[t/x]$, meaning “replace all free occurrences of $x$ in $e$ with $t$“.

Substitution is fundamental to the operational semantics of type theory, particularly in β-reduction where $(\lambda x.e)(a)$ reduces to $e[a/x]$.

Notation

For expression $e$, term $t$, and variable $x$:

• $e[t/x]$: Substitute $t$ for $x$ in $e$
• Multiple substitutions: $e[t_1/x_1,t_2/x_2,\dots ,t_n/x_n]$
• Simultaneous substitution: All replacements happen at once

Formal Definition

Substitution is defined inductively on the structure of expressions:

x[t/x] &= t \\ y[t/x] &= y \quad \text{if } x \neq y \\ (e_1 \, e_2)[t/x] &= (e_1[t/x]) \, (e_2[t/x]) \\ (\lambda x. e)[t/x] &= \lambda x. e \quad \text{(bound variable blocks substitution)} \\ (\lambda y. e)[t/x] &= \lambda y. (e[t/x]) \quad \text{if } x \neq y \text{ and } y \notin \text{FV}(t) \end{aligned}$$ ## Variable Capture A critical issue in substitution is *variable capture*. Consider: $$(\lambda y. x)[y/x] = \lambda y. y$$ This is incorrect because the free variable $y$ being substituted has been captured by the lambda binding. The correct approach requires renaming the bound variable first (α-conversion): $$(\lambda y. x)[y/x] = (\lambda z. x)[y/x] = \lambda z. y$$ ## Capture-Avoiding Substitution To avoid variable capture, substitution must: - Rename [[Bound Variable|bound variables]] when they would capture free variables in the substituted term - Use fresh variable names that don't appear in either expression - Preserve the meaning of the expression through α-equivalence The formal rule for lambda abstraction: $$(\lambda y. e)[t/x] = \lambda z. (e[z/y][t/x])$$ where $z$ is fresh (not in $\text{FV}(e) \cup \text{FV}(t)$). ## Properties - Substitution preserves types: If $\Gamma, x : A \vdash e : B$ and $\Gamma \vdash t : A$, then $\Gamma \vdash e[t/x] : B$ - Substitution is not commutative in general: $e[t_1/x_1][t_2/x_2] \neq e[t_2/x_2][t_1/x_1]$ in general - Simultaneous substitution avoids ordering issues - Substitution interacts with reduction via the substitution lemma ## In Type Theory Substitution appears in several key places: - [[Computation Rule|β-reduction]]: $(\lambda x. e)(a) = e[a/x]$ - [[Dependent Product|Dependent functions]]: Applying $f : \Pi_{x:A} B(x)$ to $a : A$ gives $f(a) : B[a/x]$ - [[Dependent Sum|Dependent pairs]]: The second projection has type $B[\pi_1(p)/x]$ - Type families: Substituting values into type expressions ## Related Concepts - [[Free Variable]]: Variables that can be substituted - [[Bound Variable]]: Variables that block substitution within their [[Scope]] - [[Scope]]: The region where a variable binding is active - [[Computation Rule]]: Uses substitution for β-reduction - [[Lambda Calculus]]: The foundational system for substitution - [[Alpha Equivalence]]: Renaming bound variables to avoid capture