# Why do we have to make variables unique when evaluating $\lambda$-calculus?

I'm studying $$\lambda$$-calculus and came across a problem that I'm not sure how to understand. More specifically, it's about evaluating $$\lambda$$-calculus expressions using $$\beta$$-reduction.

I was taught that the basic steps for performing $$\beta$$-reduction are to

1. Find reducible expressions in the form of ($$\lambda x.e_1$$) $$e_2$$.

2. Rewrite the expression by substituting every free occurrence of $$x$$ in $$e_1$$ with $$e_2$$.

I've solved some exercise problems which seemed fairly simple to understand, but came across one that I couldn't understand the answer.

The expression in question is ($$\lambda x.$$($$\lambda y.x$$)) $$y$$, and after following the rules above I ended up with the result of $$\lambda y.y$$ after replacing the free occurrence of $$x$$ with $$y$$ in $$\lambda y.x$$. However, the correct answer seems to be $$\lambda y.x$$.

The rationale that I've been able to find is that before applying $$\beta$$-reduction, we have to change variables to be "unique."

Could someone explain the reasoning behind this for me please?

When performing a $$\beta$$-reduction, there are cases in which an $$\alpha$$-conversion is needed first; otherwise, the $$\beta$$-reduction fails to preserve semantics. This is here the case: you are replacing the free variable $$x$$ with $$e_2$$ and $$e_2$$ contains free variables which are bound within $$e_1$$.

You can easily see why the semantics are not preserved: $$(\lambda y.y)$$ and $$(\lambda y.x)$$ are not equivalent expressions because $$(\lambda y.y)z = z$$ but $$(\lambda y.x)z = x$$. In order to preserve the semantics, you first need to perform an $$\alpha$$-conversion on $$(\lambda y.x)$$ so as to replace $$y$$ with something else which is not free in $$e_2$$ (thus achieving "uniqueness"—though IMO such a term should be frowned upon here).

• Thank you! I wasn't familiar with $\alpha$-conversion and didn't know it was needed in this sense. I'm also not in favor of the term "uniqueness" as well, but the resource I referred to seemed to use that term. – Seankala Dec 14 '18 at 9:06
• I just had one additional question. How do we choose which variables to perform $\alpha$-conversion on? If we take the equation I originally gave as an example - ($\lambda x.$($\lambda y.x$)) $y$ - then is it also equivalent to convert the first $x$ rather than the $y$, yielding $\lambda z.$($\lambda y.x$) $y$? – Seankala Dec 14 '18 at 9:24
• As I wrote in the answer, you need to replace every free variable $v$ in $e_2$ for which there is an occurence of $x$ in $e_1$ where the variable $v$ is bound. If you are allowed to use as much variables as you want to, then you can simply rename all free variables in $e_2$ which are bound somewhere in $e_1$ (although, of course, you do not have to do so). Also, in your expression (BTW it is not an equation!), if you replace $x$ with $z$, then you obtain $\lambda z. (\lambda y.z)y$, not $\lambda z. (\lambda y.x)y$. – dkaeae Dec 14 '18 at 13:39
• Additionally, in $\lambda z.(\lambda y.z) y$ you have the same problem in the reduction. Replacing $x$ with something else does not help; you must rename the bound $y$ so as to obtain, for instance, $(\lambda x.(\lambda z.x))y$ – dkaeae Dec 14 '18 at 13:44