形式陈述
对任意总函数 ,Shoenfield 极限定理断言
右边正是极限可计算公理库极限可计算函数Limit-computable function · Computable in the limit · Limit recursive function允许可计算猜测有限次改口、只要求每个输入最终稳定到正确值的总函数。。对集合 ,把 取为特征函数可得
这里的 是Turing 归约公理库Turing 归约Turing reduction · Oracle reduction允许算法把目标语言作为预言机进行多次自适应查询的可计算性归约。, 是空集的第一次跳跃公理库Turing 跳跃Turing jump · Jump operator · 图灵跳跃把集合 A 送到相对于 A 的对角停机集 A′,从而统一产生严格更高 Turing degree 的运算。。相对版本同样精确: 当且仅当存在 -可计算的 逐点稳定到 。定理还可一致化:从一边的程序索引能有效得到另一边的索引;它并未提供可计算的稳定阶段。
直觉
能回答“某个搜索以后还会不会成功”这一类存在性问题。给定近似的当前值,询问未来是否还会变化,就是一个可识别事件:可以逐阶段寻找首个反例。停机预言机可以判定这个搜索最终有无结果,于是能够找到真正的最后版本。
反方向中, 的有限计算只查看有限多个 oracle 位。把 用“目前已经发现的停机程序”逐阶段逼近,某次计算可能因尚未发现的正例而暂时走错;但对固定输入,真实停机计算只涉及有限查询,这些位最终全部稳定。此后足够长的有界模拟便重复同一条正确轨迹。无限 oracle 被压缩成了每个输入上的有限、但事先不知道何时可靠的信息。
两边的关键都不是把 当作一个瞬间可见的无限表。正向证明用它逐次决定未来变化,反向证明只依赖实际计算的有限 use。若省略有限 use,就无法从 oracle 的逐位收敛推出整段计算稳定;若假设可计算地知道最后变化阶段,又会把结论错误加强成普通可计算性。
例子与边界
先从近似推出 -算法。给定总可计算 ,固定 后考察谓词
是 c.e.:逐个模拟 即可寻找一次变化,所以 能判定它。依次试 ,首个满足 的阶段一定存在,输出 即为极限。这个算法不靠猜测一个全局收敛速率。
反过来设 且对每个 停机。令 是在前 步发现进入 的有限集合,并定义 :用 作临时 oracle,模拟 至多 步;若停机则取其输出,否则输出 。真实计算对固定 只询问有限多个数。所有真实“是”答案最终进入 ,真实“否”答案永不进入;当这些位和运行时间都被阶段覆盖后, 永远等于 。
总性假设不可省略。若 在某些输入发散,上述默认输出 的近似仍可能收敛,却会把“无定义”误写成函数值;部分函数版本必须用带发散语义的另外表述。近似也无需单调,甚至可有限次往返;Shoenfield 定理保证最终稳定,不保证每项只改一次。最后, 结论针对集合的特征函数,不能把任意 集自动称为 limit computable。
推论与应用
定理把 的三种常用定义接在一起:双重算术定义、-可计算性与可计算稳定逼近。因此在有效阶段构造里,若阶段特征函数 是总可计算的,并且对每个 最终稳定到 ,就立刻得到上界 ;反过来,任何低于 的集合都有这样的统一可计算近似。仅证明某列猜测逐点稳定而不证明 可计算,并不足以应用本定理。
相对版本是有限伤害优先法的基础。以 为背景信息构造对象时,允许 -可计算的阶段策略;最终对象恰落在 以下。多次相对化得到 与 -可计算近似之间的对应,并和 Post 定理的 刻画吻合。
极限定理也提供错误检查:若有人声称一个 -可计算函数只有“越来越接近”却不最终恒定的整数近似,他尚未给出本定理要求的见证;若给出了可计算稳定模,则函数其实无需 。在算法学习与 trial-and-error computation 中,可以借用这种修订直觉,但只有输入、阶段、总性和逐点稳定量词完全一致时,结论才真的是 Shoenfield 极限定理。
参考资料
- Joseph R. Shoenfield, “On Degrees of Unsolvability,” Annals of Mathematics 69(3), 1959, pp. 644–653,极限定理及相对形式。
- Robert I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987,Chapter III,Limit Lemma 与 近似。
- Piergiorgio Odifreddi, Classical Recursion Theory, Vol. I, North-Holland, 1989,Chapter IV,limit computations and the arithmetical hierarchy。