8
$\begingroup$

I know this is a simple question but can someone show me how $(\lambda y. \lambda x. \lambda y.y) (\lambda x. \lambda y. y)$ reduces to $\lambda x. \lambda y. y$.

$\endgroup$
  • $\begingroup$ Are you sure you parenthesized this correctly? Because the way it's written, I don't see how it can be simplified at all. If it was (λy.λx.λy.y) (λx.λy.y), it'd reduce to λx.λy.y. $\endgroup$ – sepp2k Apr 3 '12 at 21:52
  • $\begingroup$ Yes thanks I updated my question. Could you explain how you got λx.λy.y $\endgroup$ – prerm2686 Apr 3 '12 at 21:58
10
$\begingroup$

The reason that $(\lambda y. \lambda x. \lambda y.y) (\lambda x. \lambda y. y)$ reduces to $\lambda x. \lambda y. y$ and not to $\lambda x. \lambda y.\lambda x.\lambda y.y$ is that the $y$ in the body of $\lambda y.\lambda x.\lambda y.y$ refers to the argument of the third lambda, not the first.

If you rename the arguments to have distinct names, $\lambda y.\lambda x.\lambda y.y$ would be written as $\lambda y_1.\lambda x.\lambda y_2.y_2$. So if you apply that function to the argument, that means that every occurrence of $y_1$ in $\lambda x.\lambda y_2.y_2$ should be replaced with the argument. However $y_1$ does not appear at all in that expression, so the argument is simply ignored and the result is just $\lambda x.\lambda y_2.y_2$.

$\endgroup$
  • $\begingroup$ Oh ok so the y2 is not bound to y1. Thank you very much. $\endgroup$ – prerm2686 Apr 3 '12 at 22:04
  • 7
    $\begingroup$ @prerm2686 A variable is always bound by the closest encompassing $\lambda$. The subterm $\lambda y.y$ is the identity function, no matter where you use it, even if you use it in a context that also uses the variable name $y$. $\endgroup$ – Gilles 'SO- stop being evil' Apr 3 '12 at 22:07
  • $\begingroup$ Reduction on wikipedia gives a more formal treatment of α-conversion and β-reduction. A reference I like is Chris Hankin's book $\endgroup$ – Romuald Apr 7 '12 at 10:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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