lambda-calculus - Lambda 演算的 Beta 化简

Question

我知道这可能真的很简单，但我在弄清楚如何减少这种情况时遇到了问题。以下是我的等式。

(λx λy . y x) z

我只需要知道从哪里开始，因为我完全迷失了。

Answer 1

那个 lambda 表达式在语法上不正确，我认为你的意思是这样写：

(λx.λy.y x) z 

或者

(λxy.y x) z

这很重要，因为有效的 lambda 表达式是 λx.M 而不是 λx M 的形式，或者使用语法糖你可以写 λxy.M 但不能写 λxλy.M 并且这个 (λx.λy.yx) 令人困惑，因为它看起来像一个应用程序。

我会同时减少(λx.λy.y x) z和(λx.λy.yx) z

1) (λx.λy.y x) z
2)(λx.λy.y x)通过将 x 应用到 来减少λx.λy.y，因此(λx.λy.y x) z减少到λy.y z 3)λy.y z通过将 z 应用到 来减少λy.y z，结果将是 z。

如果你的意思是(λx.λy.yx)z

1) (λx.λy.yx) z 2) λx.(λy.yx) z 3) 将 z 应用于第一个抽象：λy.yz 4) 减少结果的其他方法是：λy.yz

我建议您查看 lambda-calculus 定义并了解应用程序、抽象和变量之间的区别。

另外在早期最好使用 () 并且总是以扩展的方式编写 lambda 表达式，这样你就会少犯错误。

Answer 2

您的 lambda 表达式可以采用两个输入参数，但只有一个输入 z。因此，这导致部分应用。

在您的情况下，这意味着参数 x 的值是 z。因此，该表达式中所有出现的 x 都将替换为 z。但是，参数 y 没有被赋予任何值，因为没有任何输入，所以参数 y 保持绑定。

正如 fsvieira 所说，λy.yz 是正确的答案。