Evaluación del cálculo lambda

Sé que esta es una pregunta simple, pero ¿alguien puede mostrarme cómo $(\lambda y. \lambda x. \lambda y.y) (\lambda x. \lambda y. y)$ reduce a $\lambda x. \lambda y. y$.

La razón que $(\lambda y. \lambda x. \lambda y.y) (\lambda x. \lambda y. y)$ reduce a $\lambda x. \lambda y. y$ y no a $\lambda x. \lambda y.\lambda x.\lambda y.y$ es que el $y$ en el cuerpo de $\lambda y.\lambda x.\lambda y.y$ se refiere al argumento de la tercera lambda, no a la primera.

Si cambia el nombre de los argumentos para que tengan nombres distintos, $\lambda y.\lambda x.\lambda y.y$ se escribiría como $\lambda y_1.\lambda x.\lambda y_2.y_2$. Entonces, si aplica esa función al argumento, eso significa que cada aparición de$y_1$ en $\lambda x.\lambda y_2.y_2$debe ser reemplazado con el argumento sin embargo$y_1$ no aparece en absoluto en esa expresión, por lo que el argumento simplemente se ignora y el resultado es simplemente $\lambda x.\lambda y_2.y_2$.