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

【问题标题】：Knights of the Lambda Calculus infinity written as lisp code用 lisp 代码编写的 Lambda 微积分无穷大骑士
【发布时间】：2013-10-19 11:10:47
【问题描述】：

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

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

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

【问题讨论】：

在您的代码中，您显示 Y 已使用但未定义。它的定义是什么？
@WillNess 它是 Y Combinator。
请问它的定义是什么？你的意思是和Y F = F (Y F)一样吗？因为 that 不是 lambda 表达式，而您在 lambda 表达式中使用它。 Lambda 演算没有定义，这就是为什么他们使用大写字母 Y 表示它应该用 lambda 表达式 for Y 替换。这也意味着你不应该在那里使用大写 F，而是使用常规f.
在@dsm 答案中查看 Rosetta Code 中的方案实现。而且我的代码不是 lambda 演算，它的 lisp 代码 λ 可以写成 lambda。
@WillNess 我没有定义Y，因为众所周知，就像我写(! 10) 并且没有定义阶乘函数一样。

标签： lambda lisp lambda-calculus infinity y-combinator

【解决方案1】：

通过 eta 收缩，您的表达式 Y (λ f. Y f) 是 Y Y。由于Y f 减少到f (Y f)，我们得到 p>

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

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

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

【讨论】：

【解决方案2】：

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

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

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

【讨论】：

【解决方案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 组合子，要么仅代表这个规范组合子。

这张图片是在麻省理工学院通过实现一种嵌入式编程语言在方案中绘制的，该方案将图片作为原子对象和组合图片的简单方法，see here。

而at this link是计算机科学家Peter Henderson的函数几何语言的详细描述，他试图创建一种编程语言来生成埃舍尔的图片，也被用来生成MIT-SCHEME的标志：

【讨论】：