标题： Oracle 模态 显示英文标题

标题： Oracle modalities

摘要： 我们提出了一种新的图灵可约性的表述，基于更高模态，这一想法受到Hyland在有效拓扑中的子拓扑格中嵌入图灵度的发现所启发。在这个定义中，更高模态的作用类似于I/O单子或对话树，允许函数从外部预言机接收输入。然而，在同伦类型理论中，它们比单子具有更好的逻辑性质：它们与高类型兼容，并且每个模态对应一个反射子宇宙，在适当条件下它本身是同伦类型理论的一个模型。我们使用了马尔可夫归纳法和可计算选择的两个公理，在立方类型理论中给出了图灵可约性的一些基本结果的合成证明。这两个公理都是在有效拓扑中已经研究过的公理的变体。我们展示了它们在立方装配的某些反射子宇宙中成立，用模态在合成可计算性理论的一些简单证明中演示了它们的使用，并展示了它们对于预言机模态是向下绝对的。这些结果已使用Agda证明助手的立方模式进行形式化。我们探讨了图灵可约性与同伦理论之间的一些初步联系。这包括一个合成证明，即一旦两个图灵度在自然数上诱导出同构的置换群，它们就相等，该证明充分利用了马尔可夫归纳法以及在HoTT中将群表述为带基点、连通、1截断类型的表述。我们还基于这些思想给出了一些立方装配中模态的简单非拓扑例子，以说明我们预期的图灵度的高维类似物应该是什么样子。 显示英文摘要

摘要： We give a new formulation of Turing reducibility in terms of higher modalities, inspired by an embedding of the Turing degrees in the lattice of subtoposes of the effective topos discovered by Hyland. In this definition, higher modalities play a similar role to I/O monads or dialogue trees in allowing a function to receive input from an external oracle. However, in homotopy type theory they have better logical properties than monads: they are compatible with higher types, and each modality corresponds to a reflective subuniverse that under suitable conditions is itself a model of homotopy type theory. We give synthetic proofs of some basic results about Turing reducibility in cubical type theory making use of two axioms of Markov induction and computable choice. Both axioms are variants of axioms already studied in the effective topos. We show they hold in certain reflective subuniverses of cubical assemblies, demonstrate their use in some simple proofs in synthetic computability theory using modalities, and show they are downwards absolute for oracle modalities. These results have been formalised using cubical mode of the Agda proof assistant. We explore some first connections between Turing reducibility and homotopy theory. This includes a synthetic proof that two Turing degrees are equal as soon as they induce isomorphic permutation groups on the natural numbers, making essential use of both Markov induction and the formulation of groups in HoTT as pointed, connected, 1-truncated types. We also give some simple non-topological examples of modalities in cubical assemblies based on these ideas, to illustrate what we expect higher dimensional analogues of the Turing degrees to look like.