减少 Lambda 演算答案

【问题标题】：Reduction in Lambda Calculus减少 Lambda 演算
【发布时间】：2013-08-28 10:24:05
【问题描述】：

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

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

【问题讨论】：

【解决方案1】：

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

如果你有 lambda 项：(\x.x) 以及它右侧的一些值：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。这就是恒等函数。

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

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

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

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

如果您只是想更直观地了解 lambda 演算的工作原理，大多数计算机科学系都会提供幻灯片。

【讨论】：