lambda - 用 lisp 代码编写的 Lambda 微积分无穷大骑士

Question

Knights of the Lambda Calculus 徽标的无穷大写为(Y F) = (F (Y F))

这个lisp代码是一样的吗？它也代表无穷大吗？

(Y (λ (F) (YF)))

Answer 1

通过 eta 收缩你的表达Y (λ f. Y f)是Y Y。由于Y f归约为f (Y f)，我们得到

Y Y --> Y (Y Y) --> Y Y (Y (Y Y)) --> Y (Y Y) (Y (Y Y)) --> ...

所以它是一个发散的 lambda 项。

Y f本身并不是一个发散的术语。它减少到f (Y f)，f现在接管。如果f曾经使用它的参数，并且被它的调用者强迫这样做，那么只有这样链才会继续。

Answer 2

Y这里是一个定点组合器。给定一个函数f ，它返回一个x = f(x)的值。当我们写Y(f)而不是写x时，我们有Y(f) = f(Y(f))。在传统的 lambda 演算符号中，这是(F (YF)) = (YF)，这就是您在图像中看到的。

一些数值函数有一个或多个不动点。例如，（正）平方根函数以及平方函数的不动点是 1 和 0。一些数值函数，例如f(x) → x+1没有不动点。在某些形式中，包括无类型的 lambda 演算，每个函数都有一个固定点。

这个特定的定点运算符是 Y 组合子，在各个地方都有更详细的描述，包括上面链接的 Wikipedia 文章。定点运算符很重要，因为除其他外，它们允许以诸如无类型 lambda 演算之类的形式定义递归函数。

Answer 3

这个方程y-combinator实际上可以通过从这个方程开始的 4-5 次归约推导出来，也称为canonical combinator,

((lambda (self) (self self)) (lambda (self) (self self)))

要查看这种无限递归的具体结果，需要为递归插入一个最终标准，例如在这种原始递归方程中：

((lambda(s) (s s 100))
 (lambda(s n)
   (if (zero? n)
     0
     (+ n (s s (- n 1))))))

;Value: 5050

图片实际上代表 y 组合子或仅代表此规范组合子。

这张图片是在麻省理工学院通过在方案中实现嵌入式编程语言绘制的，该方案将图片作为原子对象以及组合图片的简单方法，请参见此处。

在这个链接上详细描述了计算机科学家的功能几何语言，Peter Henderson他试图创建一种编程语言来生成 Escher 的图片，并且还被用来生成 MIT-SCHEME 的标志：