如何仅对“λy.(λx.λy.yx)yz”应用一次 beta 约简？

Question

如何对

λy.(λx.λy.yx)yz

应用一项 beta 缩减？

正确答案是

λy.(λw.wy)z

。

仅在必要时才允许重命名，从答案中可以明显看出使用了重命名。

Answer 1

让我们首先添加一些括号，以使结构更加明显，因为也许这就是您感到困惑的原因：

λy.(λx.λy.yx)yz = λy.(((λx.λy.(yx))y)z)

在最外层，没有什么可做的。但是我们可以在

λy

内进行 beta 缩减，但首先我们需要进行 alpha 重命名以避免捕获

y

:

    (λx.λy.(yx))y
--> (λx.λw.(wx))y   (alpha renaming y to w)
--> λw.wy           (beta)

现在将其放入整个上下文中：

    λy.(λx.λy.yx)yz
--> λy.(λx.λw.(wx))yz   (alpha renaming y to w)
--> λy.(λw.wy)z         (beta)