No need to rename a free variable in substitution?

I wonder if the following two substitutions are correct:
$$(x\,y)[x:=y] = (y\,y)$$

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

They are what I understand from http://en.wikipedia.org/wiki/Lambda_calculus#Substitution.

Although I can follow the rules there mechanically, I wonder why there is no renaming of $y$ to $z$ in the first substitution, while there is in the second?

Is it correct that in substitution $E[x:=M]$, if both $E$ and $M$ have some free variable with the same name, there is no need to rename the free variable in $E$, just as in the first substitution? Thanks.

Yes, it is all correct.

Lambda-calculus may be just taken as a formal system, with rules to be
followed. Period.

However, it may be useful to try to understand intuitively why the
rules are what they are.

So the following is very informal and should be taken as an attempt at
answering intuitively.

Consider whether the following expressions are equivalent:

-
$y$ and $z$ : they are not equivalent because a substitution on $y$ has
no effect on $z$, and conversely. The variables $y$ and $z$ are free
variables. They stand for themselves, or for
whatever value is associated to them in an environment where you
evaluate the expression, or by a substitution. Changing a free
variable for another (it is not renaming in such a case) will change
what you get in the environment, or by applying a substitution (which
amounts to the same).

-
$\lambda y. (x\,y)$ and $\lambda z.(x\,z)$ : they are equivalent
via alpha conversion. When applied to the same argument, and more
generally when used in the same context, they will always give the
same result. The variables $y$ and $z$ are bound variables. Renaming
a bound variable can be done at any time,
independently of the context, without ever changing the behavior of
the $\lambda$-abstraction.

The renaming in your example $ \lambda y. (x\,y) [x:=y] = \lambda
z.(y\,z)$ is needed because the $y$ in the substitution is a free
variable (possibly taking a value in whatever environment or
substitution may be provided). Without the renaming, it would be
undistinguisable from the bound variable of the $\lambda$-abstraction
once the substitution is performed. To avoid that, the bound variable
is renamed, since renaming it does not matter.

Contrarily, in the expression $(x\,y)[x:=y]$, both occurences of $y$
stand for the same free variable $y$ in the current environment. There
is no reason to try distinguishing them.

StackExchange Computer Science Q#28501, answer score: 3