[Solved]: No need to rename a free variable in substitution?

Problem Detail: 

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.

Asked By : Tim

Answered By : babou

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/28501

 Ask a Question

 Download Related Notes/Documents