paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Galois connection between Turing jumps and limits

图灵跳跃与极限之间的 Galois 连接
LMCS Volume 14, Issue 3(Computability and logic)2018匹配度 2/10 · 论文属于纯可计算性理论/可计算分析(图灵跳跃、极限可计算、表示空间上的 Galois 连接),与用户主攻的 PL↔AI(LLM/Agent 程序静态分析)、LLM 辅助形式化验证、浮点程序分析及贝叶斯程序分析均无直接交叉。仅“Galois 连接”与“极限可计算”在概念上与抽象解释的不动点语义/格论基础有微弱亲缘,但论文本身不涉及程序分析或 LLM,也无工程实现与工业落地。引用 8 inbox
Vasco Brattka
crossref: 2026-09-10

AI 速览

一句话:揭示图灵跳跃与极限可计算之间的伴随关系,并在表示空间上建立形式化 Galois 连接。

论文研究极限可计算函数与图灵跳跃、相对停机问题可计算性之间的关系。作者将输入侧图灵跳跃与输出侧取极限视为一对伴随操作,构造其单子,刻画 low 函数及相对停机问题可计算函数;这两类是能与极限可计算函数前后复合仍保持该类的最大函数类。作者在表示空间格上建立形式化 Galois 连接,并给出可计算度量空间版本。关键结果:点与序列上两类可计算性一致,但连续函数上极限可计算严格更大;在可计算度量空间上,相对停机可计算等价于极限可计算且连续模相对停机可计算。由此推出极限可计算的 Lipschitz 函数自动相对停机可计算;1-泛型点作为规范连续点,限制到这些点时两类一致,并应用于可计算分析。

问题
研究极限可计算、图灵跳跃与相对停机可计算性之间的精确关系,特别是函数情形下二者的分离与等价条件。
方法
用范畴论中的伴随与单子刻画输入侧图灵跳跃和输出侧极限操作,并把结论迁移到表示空间格和可计算度量空间,形成 Galois 连接。
评估
通过理论证明给出 low 函数与停机相对可计算函数的最大复合类、度量空间上的连续模刻画,以及 Lipschitz 和 1-泛型点等推论,展示于可计算分析。
原文摘要(Abstract)

Limit computable functions can be characterized by Turing jumps on the input side or limits on the output side. As a monad of this pair of adjoint operations we obtain a problem that characterizes the low functions and dually to this another problem that characterizes the functions that are computable relative to the halting problem. Correspondingly, these two classes are the largest classes of functions that can be pre or post composed to limit computable functions without leaving the class of limit computable functions. We transfer these observations to the lattice of represented spaces where it leads to a formal Galois connection. We also formulate a version of this result for computable metric spaces. Limit computability and computability relative to the halting problem are notions that coincide for points and sequences, but even restricted to continuous functions the former class is strictly larger than the latter. On computable metric spaces we can characterize the functions that are computable relative to the halting problem as those functions that are limit computable with a modulus of continuity that is computable relative to the halting problem. As a consequence of this result we obtain, for instance, that Lipschitz continuous functions that are limit computable are automatically computable relative to the halting problem. We also discuss 1-generic points as the canonical points of continuity of limit computable functions, and we prove that restricted to these points limit computable functions are computable relative to the halting problem. Finally, we demonstrate how these results can be applied in computable analysis.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot383,
  title = {A Galois connection between Turing jumps and limits},
  author = {Vasco Brattka},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 3},
  number = {Computability and logic},
  year = {2018},
  doi = {10.23638/lmcs-14(3:13)2018}
}