# Lambda Calculus Evaluation

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

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

## 1 Answer

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

• Oh ok so the y2 is not bound to y1. Thank you very much. Commented Apr 3, 2012 at 22:04
• @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$. Commented Apr 3, 2012 at 22:07
• Reduction on wikipedia gives a more formal treatment of α-conversion and β-reduction. A reference I like is Chris Hankin's book Commented Apr 7, 2012 at 10:29