Substitution of variable with term including unbound but used variable - refactor?

Question

λx.y[x:=y] == λx.y since x is bound, no substitution happens. But what about λx.y[y:=x]? y is not bound, but if we perform the substitution then we get λx.x, but λx.x is not alpha-equivalent to the original λx.y. What do we do in this case? Can we refactor λx.y[y:=x] to λx.y[y:=z] and get λx.z, which is alpha equivalent to λx.y? Or is this a problem?

Answer 1

The substitution, $(\lambda \color{blue}x.y)[y:=\color{green}x] = \lambda \color{blue}x.\color{green}x$ , is not capture-avoiding , because the variable $\color{blue}x$ is not fresh for the substituted term $\color{green}x$.   Thus it changes the meaning of the function.

So to preserve the meaning of the function, we do need to first alpha-replace with a fresh variable.

$(\lambda x.y)[y:=x] = (\lambda z.y)[y:=x] = \lambda z.x$

---

PS: "$t$ is fresh for $s$" means $t$ is not in the free variables of $s$.