Is it appropriate to do alpha reduction before substitution?

Question

In the lambda expression (λx. (λy. y z)(λw. w) z x)[z→y], I'm inclined to change y to another variable, then perform the substitution. Is this the correct way to approach this problem? Also, if that's the case, and you can just alpha-reduce back, couldn't (λx. (λy. y z)(λw. w) z x) be an appropriate answer (y => w, z => y, y => z, w => y, where they are all alpha-reductions)? Thanks!

Answer 1

I take it that you are writing $t[x {\rightarrow} s]$ for the result of substituting $s$ for $x$ in $t$. When you substitute $s$ for $x$ in a $\lambda$-expression $t$, you may use $\alpha$-conversion to rename bound variables in $t$ to avoid clashes, but you must not rename the free variables of $s$. In your example $s$ is $y$ and when you substitute $y$ for $z$ in $\lambda x.(\lambda y. y z) (\lambda w.w) z x$, you must get (something $\alpha$-equivalent to) $\lambda x. (\lambda y'. y' y) (\lambda w.w) y x$.