lambda-calculusreduction

How to apply just one beta-reduction to `λy.(λx.λy.yx)yz`?


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.


Solution

  • 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)