Exercise 1.5
Give the results of the following substitutions:
(a) (λx. y(λy. xy))[y := λz. zx],
(b) ((xyz)[x := y])[y := z],
(c) ((λx. xyz)[x := y])[y := z],
(d) (λy. yyx)[x := yz].
(a) Because $x$ and $y$ are bound variables in the term, we should α-rename them before substitution happens.
$$\begin{align} (\lambda x. y(\lambda y. xy)) \; [y := \lambda z. zx] & =_{\alpha} (\lambda a. y(\lambda b. a b))\; [y := \lambda z. zx] \\ \\ & = (\lambda a. (\lambda z. z x)(\lambda b. a b)) \\ \\ & =_{\alpha} (\lambda a. (\lambda z. z x)(\lambda y. a y)) \end{align}$$
The last line re-introduces $y$ but is not necessary.
(b) The variables $x$, $y$ and $z$ in the term are free, unbound so we can proceed with the substation in the given order.
$$\begin{align} ((x y z)[x := y])[y := z] & = (y y z)[y := z] \\ \\ & = (z z z) \end{align} $$
(c) Here $x$ is a bound variable so we should α-rename the term before attempting substitution.
$$\begin{align}((λx. xyz)[x := y])[y := z] & =_{\alpha} ((λa. ayz)[x := y])[y := z] \\ \\ & = (λa. ayz)[y := z] \\ \\ &= (λa. a z z) \\ \\ & =_{\alpha} (λx. x z z) \end{align}$$
Note that the first substitution $[x := y]$ has no effect.
(d) Here $y$ is bound variable so we should α-rename the term before proceeding with substitution.
$$\begin{align} (λy. yyx)[x := yz] & =_{\alpha} (λa. aax)[x := y z] \\ \\ & = (λa. a a (y z)) \\ \\ & =_{\alpha} (λx. x x (y z)) \end{align}$$
Exercise 1.6
Show that the following proposition is not always true:
$$M[x := N,y := L] ≡ M[x := N][y := L]$$
where the expression on the left-hand side means a simultaneous substitution; so, $M[x := N,y := L]$ is the result of replacing all free $x$’s and $y$’s in $M$ at the same time(‘together’) by $N$ and $L$, respectively. (The expression on the right-hand side is concerned with sequential substitution.)
Let's take $M := xy$, $N:=y$ and $L:=x$, and perform the simultaneous substitution.
$$\begin{align} (x y) [x:= y, y:=x] = (y x) \end{align}$$
Now let's consider the sequential substitution.
$$\begin{align} (x y) [x:= y][y:=x] & = (y y) [y:=x] \\ \\ & = (x x) \end{align}$$
This counter-example shows the proposition is not always true.
