lambda - 减少 Lambda 微积分

Question

最近在研究lambda的计算，对reduction和substitution有很多疑惑。什么是 alpha 和 beta 缩减？何时以及为何使用它们？

如果有人能说出任何关于 lambda 微积分中减少和替代的好资源，那就太好了。

Answer 1

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

如果你有 lambda 项:(\x.x)和它右边的一些值:y

然后您将在 lambda 项中将所有绑定(bind)变量替换为 (.) 的右侧。绑定(bind)变量是匹配 (.) 左侧变量的变量，因此在本例中为 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 绑定(bind)到 lambda 表达式中所有出现的 x。这就是恒等函数。

Alpha“缩减”通常称为 alpha 等价或 alpha 重写规则。他们声明您可以更改任何 lambda 项及其绑定(bind)变量的名称，而不会更改表达式的含义。

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

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

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

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

您可能会发现这些有用:http://www.classes.cs.uchicago.edu/archive/2002/winter/CS33600/slides/Lesson2.pdf https://www.utdallas.edu/~gupta/courses/apl/lambda.pdf