We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions (CIC), the constructive type theory underlying the Coq proof assistant. As usual in synthetic approaches, we employ a definition of oracle computations based on meta-level functions rather than object-level models of computation, relying on the fact that in constructive systems such as CIC all definable functions are computable by construction. Such an approach lends itself well to machine-checked proofs, which we carry out in Coq. There is a tension in finding a good synthetic rendering of the higher-order notion of oracle computability. On the one hand, it has to be informative enough to prove central results, ensuring that all notions are faithfully captured. On the other hand, it has to be restricted enough to benefit from axioms for synthetic computability, which usually concern first-order objects. Drawing inspiration from a definition by Andrej Bauer based on continuous functions in the effective topos, we use a notion of sequential continuity to characterise valid oracle computations. As main technical results, we show that Turing reducibility forms an upper semilattice, transports decidability, and is strictly more expressive than truth-table reducibility, and prove that whenever both a predicate $p$ and its complement are semi-decidable relative to an oracle $q$, then $p$ Turing-reduces to $q$.

翻译：我们在归纳构造演算（CIC）中发展了合成式的预言机可计算性与图灵归约性概念，CIC是Coq证明助手所依赖的构造类型论。遵循合成方法的惯例，我们采用基于元层次函数而非对象层次计算模型的预言机计算定义，这一做法依赖于在CIC这类构造系统中所有可定义函数均可通过构造方式实现可计算性的事实。该方法天然适用于机器验证证明，我们已在Coq中完成了相关验证。在寻找高阶预言机可计算性的合适合成表述时存在一种张力：一方面，它需要具备足够的信息量以证明核心结论，确保所有概念都被准确刻画；另一方面，它又必须受到充分限制以利用合成可计算性公理——这些公理通常涉及一阶对象。受基于有效拓扑斯中连续函数的Andrej Bauer定义的启发，我们使用序列连续性概念来刻画有效的预言机计算。作为主要技术成果，我们证明了图灵归约性构成上半格结构、传递可判定性，且其表达能力严格强于真值表归约性；并证明了当谓词$p$及其补集均相对于预言机$q$半可判定时，$p$可图灵归约至$q$。