α-conversion

Overview

Let $λ$ -term $P$ contain an occurrence of $λ x . M$ , and let $y \notin F V (M)$ . The act of replacing this occurrence of $λ x . M$ with $λ y . [y / x] M$ is called a change of bound variable or an $α$ -conversion in $P$ .

If $P$ can be changed to $λ$ -term $Q$ by a finite series of changes of bound variables, we shall say $P$ is congruent to $Q$ , or $P$ $α$ -converts to $Q$ , or $P \equiv_{α} Q$ .

Let $x$ , $y$ , and $v$ be distinct variables. Then

$v \notin F V (M) ⟹ [P / v] [v / x] M \equiv_{α} [P / x] M$
$v \notin F V (M) ⟹ [x / v] [v / x] M \equiv_{α} M$
$y \notin F V (P) ⟹ [P / x] [Q / y] M \equiv_{α} [([P / x] Q) / y] [P / x] M$
$x \notin F V (Q) \land y \notin F V (P) ⟹ [P / x] [Q / y] M \equiv_{α} [Q / y] [P / x] M$
$[P / x] [Q / x] M \equiv_{α} [([P / x] Q) / x] M$

Substitution is well-defined with respect to $α$ -conversion. That is, if $M \equiv_{α} M^{'}$ and $N \equiv N^{'}$ , then

[N / x] M \equiv_{α} [N^{'} / x] M^{'} .

Simultaneous Substitution

Substitution can be generalized in the natural way to define simultaneous substitution

[N_{1} / x_{1}, N_{2} / x_{2}, \dots, N_{n} / x_{n}] M

for $n \geq 2$ . As in equivalence-transformation, simultaneous substitution is different from sequential substitution.