# 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. – sepp2k Apr 3 '12 at 21:52
• Yes thanks I updated my question. Could you explain how you got λx.λy.y – prerm2686 Apr 3 '12 at 21:58

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$.
• @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$. – Gilles 'SO- stop being evil' Apr 3 '12 at 22:07