Lambda微积分的还原

Question

最近我一直在研究λ的计算，我对减缩和替换有很多疑问。什么是α和β减少？它们何时被使用，为什么被使用？

如果有人能告诉我们在兰达仙人掌的还原和替代方面有什么好的资源，那就太好了。

Answer 1

β约简只是在lambda演算中用于计算的主要应用规则。它是通过替代实施的，如下所示：

如果您有lambda项：(\x.x)和它右边的值:y

然后将所有绑定变量替换到(.)的右侧。)用你的兰博达术语。绑定变量是与(.)的左边变量相匹配的变量，因此在本例中是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项及其绑定变量的名称，而无需更改表达式的含义。

例如，使用上面的标识函数，我们可以像(\j.j)一样轻松地编写lambda术语。它不会改变我们应用程序的结果，如下所示：

(\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