Good day . I need to reduce the following expression of lambda calculus:
$(\lambda z. zy)(\lambda z. zy)$
Now, since I am having the variable $y$ in both the left and right pair of parentheses, I think that I should rename one of them to another variable, namely $u$.
$(\lambda z. zu)(\lambda z. zy)$. Now, by reducing I get: $(\lambda z. zy)u$ , which yields $uy$
However: in the solution of the exercise I found online they did not rename the variable $y$! I am not sure why. Since the variable $y$ appears in both pairs of parentheses we'd need to rename one of them. They simply got $(\lambda z. zy)y$ which evaluates to $yy$.
The reason I'm asking is because in one other example, they did rename one of the variables. It's this example:
$$(\lambda x. \lambda y. xy)(\lambda x. \lambda y. xy)$$
What they did is they renamed one of the variables $y$ to $z$ so they got
$$(\lambda x. \lambda \color{red}z. x \color{red}z)(\lambda x. \lambda y. xy)$$
Can anyone explain why we don't rename the variable in the first example, but we need to do it in the second example?
You cannot rename free variables! You can only rename bound variables (so you can rename $\lambda x. xy$ to $\lambda z. zy$ but you cannot rename $\lambda x.xy$ to $\lambda x. xz$ since the result becomes different).
Think of this: $\lambda x.x$ is the identity function, and it is $\alpha$-equivalent to $\lambda y.y$ or to $\lambda z.z$ or any other identity function. So here you can rename. While instead, $x$ is the variable $x$, and if you try renaming it to $y$ you are changing the semantics of the term: $x$ is not $\alpha$-equivalent to $y$.
Hence, in $(\lambda z. zy)(\lambda z. zy)$ you cannot rename $y$, if you really wanted you could rename $z$ and get $(\lambda z. zy)(\lambda u. uy)$ and get $yy$ as you would get without renaming, clearly.
I think in your second example they did rename the variable because the variable $y$ wasn't free in the term $t$ they were substituting for $x$. So if they didn't rename it they would get $\lambda y. (\lambda x. \lambda y. xy)y$ that is different from the true result that is $\lambda z. (\lambda x. \lambda y. xy)z$ or any equivalent form like $\lambda u. (\lambda x. \lambda y. xy)u$ or $\lambda y. (\lambda x. \lambda z. xz)y$.