patternMinor
Why do we have to make variables unique when evaluating $\lambda$-calculus?
Viewed 0 times
uniquewhycalculusmakelambdavariableswhenhaveevaluating
Problem
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
-
Find reducible expressions in the form of ($\lambda x.$$e_1$) $e_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?
I was taught that the basic steps for performing $\beta$-reduction are to
-
Find reducible expressions in the form of ($\lambda x.$$e_1$) $e_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?
Solution
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).
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).
Context
StackExchange Computer Science Q#101524, answer score: 2
Revisions (0)
No revisions yet.