paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Instance reducibility and Weihrauch degrees

实例可归约性与 Weihrauch 度
LMCS vol.Volume 18, Issue 32022匹配度 2/10 · 该论文属于可计算性理论、构造数学与 Weihrauch 度理论,讨论实例可归约性与格结构,未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析。虽与形式化验证的逻辑基础有间接关联,但不在用户当前核心研究问题范围内。引用 6 inbox
Andrej Bauer
crossref: 2026-09-10

AI 速览

一句话:提出实例可归约性,证明实例度构成 frame,并推广为结构更丰富的扩展 Weihrauch 度。

逆向构造数学中若干原理需要统一的可归约性来比较和分类。作者提出谓词间的实例可归约性,并研究其实例度。证明实例度构成一个 frame,等价于真值上集合按反向 Smyth 偏序构成的 frame;子对象分类子以单调和反单调两种方式嵌入,¬¬-稠密的度恰可归约到排中律度。在相对 realizability topos 中给出实例度的显式表述,称为扩展 Weihrauch 度;在 Kleene-Vesley realizability 中,¬¬-稠密 modest 实例度恰对应 Weihrauch 度。扩展度通过可计算的下确界与上确界、蕴含、参数访问和结果计算控制,改进了 Weihrauch 度的结构并拓宽其范围。

问题
如何为逆向构造数学中的多种原理(形式 Church 论题、Brouwer 连续性原理与扇定理、排中律、有限原理、函数选择、Markov 原理等)提供统一的可归约性框架,以便比较和分类。
方法
引入谓词间的实例可归约性,研究实例度的格论与范畴语义结构,并在相对 realizability topos 中构造扩展 Weihrauch 度。
评估
通过数学证明与范畴/realizability 构造进行论证,而非实验评估;关键验证包括实例度构成 frame、与真值上集合 frame 等价,以及在 Kleene-Vesley realizability 下与 Weihrauch 度的对应。
原文摘要(Abstract)

We identify a notion of reducibility between predicates, called instance reducibility, which commonly appears in reverse constructive mathematics. The notion can be generally used to compare and classify various principles studied in reverse constructive mathematics (formal Church's thesis, Brouwer's Continuity principle and Fan theorem, Excluded middle, Limited principle, Function choice, Markov's principle, etc.). We show that the instance degrees form a frame, i.e., a complete lattice in which finite infima distribute over set-indexed suprema. They turn out to be equivalent to the frame of upper sets of truth values, ordered by the reverse Smyth partial order. We study the overall structure of the lattice: the subobject classifier embeds into the lattice in two different ways, one monotone and the other antimonotone, and the $\lnot\lnot$-dense degrees coincide with those that are reducible to the degree of Excluded middle. We give an explicit formulation of instance degrees in a relative realizability topos, and call these extended Weihrauch degrees, because in Kleene-Vesley realizability the $\lnot\lnot$-dense modest instance degrees correspond precisely to Weihrauch degrees. The extended degrees improve the structure of Weihrauch degrees by equipping them with computable infima and suprema, an implication, the ability to control access to parameters and computation of results, and by generally widening the scope of Weihrauch reducibility.

链接与引用

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

BibTeX
@article{paperbot1669,
  title = {Instance reducibility and Weihrauch degrees},
  author = {Andrej Bauer},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 3},
  year = {2022},
  doi = {10.46298/lmcs-18(3:20)2022}
}