3
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

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

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – Sean
    Dec 14, 2018 at 9:06
  • $\begingroup$ 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$? $\endgroup$
    – Sean
    Dec 14, 2018 at 9:24
  • $\begingroup$ 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$. $\endgroup$
    – dkaeae
    Dec 14, 2018 at 13:39
  • $\begingroup$ 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$ $\endgroup$
    – dkaeae
    Dec 14, 2018 at 13:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.