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

Question

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?

• Will Ness: no, the correct answer is $λz.y$. the problem is known as "variable capture": without renaming the binder variable $λy$ to something unique (aka "fresh") like e.g. $λz,ドル the originally free $y$ in the application would become bound.

Answer 1

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).

• Sean: 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.
• Sean: 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$?
• dkaeae: 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: 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$