α-conversion

Overview

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

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

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

• $v\notin FV(M)\Rightarrow [P/v][v/x]M{\equiv }_{\alpha }[P/x]M$
• $v\notin FV(M)\Rightarrow [x/v][v/x]M{\equiv }_{\alpha }M$
• $y\notin FV(P)\Rightarrow [P/x][Q/y]M{\equiv }_{\alpha }[([P/x]Q)/y][P/x]M$
• $x\notin FV(Q)\wedge y\notin FV(P)\Rightarrow [P/x][Q/y]M{\equiv }_{\alpha }[Q/y][P/x]M$
• $[P/x][Q/x]M{\equiv }_{\alpha }[([P/x]Q)/x]M$

Substitution is well-defined with respect to $\alpha$-conversion. That is, if $M{\equiv }_{\alpha }{M}^{\prime }$ and $N\equiv N^{\prime }$, then $[N/x]M{\equiv }_{\alpha }[N^{\prime }/x]M^{\prime }$

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\ge 2$. As in equivalence-transformation, simultaneous substitution is different from sequential substitution.

Bibliography

• Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.