lambda - 减少 Lambda 演算

Question

我最近一直在研究 lambda 计算，我对减少和替换有很多疑问。什么是 alpha 和 beta 减少？何时以及为什么使用它们？

如果有人能告诉任何关于减少和替代 lambda 演算的好的资源，那就太好了。

score 5 · Accepted Answer

Beta 缩减只是 lambda 演算中用于计算的主要应用规则。它通过替换应用，如下所示：

如果你有 lambda 项： (\xx) 和它右边的一些值： y

然后，您可以将所有绑定变量替换为 lambda 项中 (.) 右侧的所有变量。绑定变量是与 (.) 左边的变量匹配的变量，因此在本例中为 x。

The reduction would be of the form:
(\x.x)y    //y gets bound to all occurences of x to the right of the period
y

其中 y 绑定到 lambda 表达式中所有出现的 x。这就是身份功能。

阿尔法“减少”通常称为阿尔法等价或阿尔法重写规则。他们声明您可以更改任何 lambda 术语及其绑定变量的名称，而无需更改表达式的含义。

例如，使用上面的恒等函数，我们可以很容易地将 lambda 项写成 (\jj)。它不会改变我们应用程序的结果，如下所示：

(\j.j)y    //y gets bound to all occurrences of j to the right of the period
y

至于学习资源：维基百科页面非常详细，但符号很重，可能需要重读几次。

如果您只是想更好地了解 lambda 演算的工作原理，那么大多数计算机科学系都有幻灯片。

1 回答 1