How do I apply just one beta-reduction to λy.(λx.λy.yx)yz
?
The correct answer is λy.(λw.wy)z
.
Renaming is allowed only if necessary, and from the answer it is obvious that renaming was used.
Let's first add some parentheses do make the structure more apparent, because maybe that's the reason you got confused:
λy.(λx.λy.yx)yz = λy.(((λx.λy.(yx))y)z)
On the outermost level, there is nothing to be done. But we can do a beta-reduction inside the λy
, but first we need to an alpha renaming to avoid capturing the y
:
(λx.λy.(yx))y
--> (λx.λw.(wx))y (alpha renaming y to w)
--> λw.wy (beta)
Now putting this into the whole context:
λy.(λx.λy.yx)yz
--> λy.(λx.λw.(wx))yz (alpha renaming y to w)
--> λy.(λw.wy)z (beta)