Composition of substitutions

Composing two substitutions, say $\theta$ and $\lambda$, produces a new substitution, $\theta \circ \lambda$, which when applied to an expression, say $P$, results in the same expression as applying first $\theta$ and then $\lambda$ to $P$. That is,

$$(\theta \circ \lambda)(P) = \lambda(\theta(P)).$$

For example, if we think about first applying the $\theta$ substitution given above, then the substitution $\lambda = [ d/x, e/y, f/w]$, we can see that any instance of variable $x$ will first be replaced by $y$ when $\theta$ is applied. This becomes $e$ when $\lambda$ is applied, so the net result is that $x$ goes to $d$. The variable $y$ would becomes $f(x)$ which is changed to $f(d)$ by $\lambda$, and $z$ becomes $c$ which is unchanged by $\lambda$. Furthermore, the variable $w$ which is untouched by $\theta$, is replaced by $f$ when $\lambda$ is applied. So the resulting composition $\theta \circ \lambda = [ e/x, f(d)/y, c/z, f/w ]$.

Formally, we can define composition of substitutions by saying that if we have

$$\theta = [ t_1/x_1, t_2/x_2, \ldots, t_n/x_n ].$$

and

$$\lambda = [ s_1/y_1, s_2/y_2, \ldots, s_m/y_m ],$$

the composition is found by creating

$$\begin{eqnarray*} \theta \circ \lambda = && [ \lambda(t_1)/x_1, \lambda(t_2)/x_2... ...rm does \; not \; occur \; as \; a \; variable \; in} \; \theta] \end{eqnarray*}$$

and then removing any pairs of the form $x/x$.