8

关于 Y 组合器的Wikipedia 文章提供了 Y 组合器的以下 JavaScript 实现：

function Y(f) {
    return (
        (function (x) {
            return f(function (v) { return x(x)(v); }); })
        (function (x) {
            return f(function (v) { return x(x)(v); }); })
    );
}

JavaScript 中 Y 组合子的存在应该意味着每个 JavaScript 函数都有一个固定点（因为对于每个函数g，Y(g)并且g(Y(g))应该相等）。

然而，想出没有固定点的函数并不难Y(g) = g(Y(g))（见这里）。甚至某些泛函也没有固定点（参见此处）。

每个函数都有一个不动点的证明如何与给定的反例相一致？Y(g) = g(Y(g))JavaScript 不是适用于证明的无类型 lambda 演算吗？

4

3 回答 3

4

据我了解 Wikipedia 文章，它并不暗示“每个 JavaScript 函数都有一个固定点”，这个例子只是展示了如何为具有它的函数实现 Y 组合器的规范。

不，根据那篇文章和关于定点的文章中的定义，JavaScript 不能是无类型的 lambda 演算，因为它可以制定明显未能通过“有定点”检查的函数，比如function f(x){ return x + 1 }或者x ^ 1如果你想包含非-numbers ，因此也无法通过“每个函数至少有一个固定点”检查。

于 2012-06-14T14:50:48.460 回答
3

不动点理论有多种形式。那些编程语言在指称语义的标题下进行研究。它们依赖于形成具有特殊属性的结构化可数集的值。 格和完全偏序是两个例子。所有这些集合都有一个“底部”元素，它原来是一个固定点，意思是“没有有用的结果”。事实上，你对计算机程序感兴趣的唯一定点算子是最少的定点运算符：那些找到在结构化值集中最低的唯一最小定点的运算符。（注意，在这些结构化集合中，所有整数都处于同一“级别”。只有底部元素位于下方。其余层由更复杂的类型组成，如函数和元组类型，即结构。）如果你有一些离散数学，这很好地展示了它。Tarsky 的不动点定理实际上是说每个单调（或交替连续）的函数都有一个不动点。有关定义，请参见上面的参考。在可操作的计算机程序中，底部元素对应于非终止计算：无限递归。

所有这一切的重点是，如果你有一个严格的计算数学模型，你就可以开始证明关于类型系统和程序正确性的有趣事情。因此，这不仅仅是一项学术活动。

于 2012-06-22T04:09:08.670 回答
3

lambda 表达式的问题在于它们不能被解释为数学意义上的函数，即从一个集合到另一个集合的映射。

原因是函数集A自身的基数总是大于 的基数A，所以不是所有的函数 fromA到A都可以是 的元素A。也就是说，存在f: A -> A表达式f(f)没有意义的功能。

这就像“不包含自身的所有集合的集合”，在逻辑上没有意义。

JavaScript 不是 lambda 演算的模型。

你的例子的问题是

(lambda x.g(x x)) (lambda x.g(x x))

应该相当于

g((lambda x.g(x x)) (lambda x.g(x x)))

但它不在您的 JavaScript 程序中g的指示函数在哪里0。

x x总是undefined。因此，第一行的计算结果为g (undefined) = 0。第二行计算为g (g (undefined)) = g (0) = 1。这意味着您的 lambda 演算 JavaScript 模型实际上并不是真正的模型。

由于对于每个非空集D都有一个从D到D没有固定点的函数，显然不可能有 lambda 演算的模型。我认为甚至应该有可能证明在任何图灵完备的语言中都不存在 Y 组合器的实现。

于 2012-06-22T15:40:52.710 回答