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.
No need to rename a free variable in substitution?
lambda calculus
Yes, it is all correct.Lambda-calculus may be just taken as a formal system, with rules to befollowed. Period.However, it may be useful to try to understand intuitively why therules are what they are.So the following is very informal and should be taken as an attempt atanswering intuitively.Consider whether the following expressions are equivalent:$y$ and $z$ : they are not equivalent because a substitution on $y$ hasno effect on $z$, and conversely. The variables $y$ and $z$ are freevariables. They stand for themselves, or forwhatever value is associated to them in an environment where youevaluate the expression, or by a substitution. Changing a freevariable for another (it is not renaming in such a case) will changewhat you get in the environment, or by applying a substitution (whichamounts to the same).$\lambda y. (x\,y)$ and $\lambda z.(x\,z)$ : they are equivalentvia alpha conversion. When applied to the same argument, and moregenerally when used in the same context, they will always give thesame result. The variables $y$ and $z$ are bound variables. Renaminga bound variable can be done at any time,independently of the context, without ever changing the behavior ofthe $\lambda$-abstraction.The renaming in your example $ \lambda y. (x\,y) [x:=y] = \lambdaz.(y\,z)$ is needed because the $y$ in the substitution is a freevariable (possibly taking a value in whatever environment orsubstitution may be provided). Without the renaming, it would beundistinguisable from the bound variable of the $\lambda$-abstractiononce the substitution is performed. To avoid that, the bound variableis 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. Thereis no reason to try distinguishing them.