# $\beta$ - conversion and $\alpha$-reduction problem in $\lambda$-calculus

Here is an expression that I am trying to reduce and my operations so far:

$$((\lambda x.(x (\lambda z.zy))) (\lambda z.\lambda y. zy) )= (x (\lambda z.zy))[x \to \lambda z.\lambda y. zy ] = ((\lambda z.\lambda y. zy) (\lambda z.zy)) = ((\lambda s.\lambda y. zy) (\lambda z.zy)) = \lambda y. zy$$

Is this procedure correct or am I making some small (or maybe big) mistake?

-

$(\lambda z. \lambda y. zy) (\lambda z.zy)$
Before doing the $\beta$-reduction, $y$ is free in the term $\lambda z.zy$, while the name $y$ is bound inside the abstraction on the left, so we change that name on the left.
$(\lambda z. \lambda s. zs) (\lambda z.zy)$
Now we can do the $\beta$-reduction
$\lambda s. (\lambda z.zy) s$
Another $\beta$-reduction
$\lambda s. sy$

-

My result is different:

(λx.(x(λz.zy)))(λz.λy.zy)
(x(λz.zy))[x:=(λz.λy.zy)]
(λz.λd.zd)(λz.zy) //rename z and y so capturing is avoided during substitution
(λz.λd.zd)(λv.vy)
(λd.zd)[z:=(λv.vy)]
(λd.(λv.vy)d)
(λd.dy)


I think you incorrectly renamed z to s.

-
I don't think you are allowed to rename the free occurrence of $y$. – mercio Oct 9 '13 at 10:47
@mercio You are right I renamed wrong variable. I have corrected it. Result is the same anyway. – Trismegistos Oct 9 '13 at 11:31