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$
$\endgroup$
2
1 Answer
$\begingroup$
$\endgroup$
3
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$ Commented 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$ Commented 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$– RomualdCommented Apr 7, 2012 at 10:29
(λy.λx.λy.y) (λx.λy.y), it'd reduce toλx.λy.y. $\endgroup$