Lambda演算中的约简

Question

我最近一直在学习lambda演算，对于约化和代换有很多疑问。什么是α和β约化？它们何时以及为什么被使用？

如果有人能够推荐任何关于lambda演算中约化和代换的好资源，那将非常棒。

- user2714823

---

这是一个关于beta约简的很好的解释 beta reduction。 - wshcdr

Answer 1

Beta reduction是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 "reductions" 通常被称为alpha等价性或alpha重写规则。它们说明您可以更改任何lambda项和其绑定变量的名称而不更改表达式的含义。

例如，使用上面的身份函数，我们可以将lambda项简单地写成 (\j.j)。如下所示，这不会改变我们应用的结果：

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

关于学习资源：维基百科页面相当详细，但标注很多，可能需要仔细阅读几次。如果您只是希望更好地理解λ演算的工作原理，大多数计算机科学系都有讲义可供参考。您可能会发现以下链接有所帮助： http://www.classes.cs.uchicago.edu/archive/2002/winter/CS33600/slides/Lesson2.pdf https://www.utdallas.edu/~gupta/courses/apl/lambda.pdf。

- numberten