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

  • $\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, 2012 at 21:52
  • $\begingroup$ Yes thanks I updated my question. Could you explain how you got λx.λy.y $\endgroup$
    – prerm2686
    Apr 3, 2012 at 21:58

1 Answer 1


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

  • $\begingroup$ Oh ok so the y2 is not bound to y1. Thank you very much. $\endgroup$
    – prerm2686
    Apr 3, 2012 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$ Apr 3, 2012 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, 2012 at 10:29

Your Answer

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

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