Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions

要約

私たちは、Coq 証明アシスタントの基礎となる構成型理論である帰納法計算 (CIC) におけるオラクルの計算可能性とチューリング還元可能性の総合的な概念を開発します。
合成アプローチでは通常のように、CIC などの構築的なシステムではすべての定義可能な関数が構築によって計算可能であるという事実に基づいて、オブジェクト レベルの計算モデルではなくメタレベルの関数に基づいたオラクル計算の定義を採用します。
このようなアプローチは、Coq で実行されている機械チェックによる証明に適しています。
オラクルの計算可能性の高次の概念を適切に合成して表現するものを見つけるには緊張が伴います。
一方で、すべての概念が忠実に把握されていることを確認しながら、中心的な結果を証明するのに十分な情報を提供する必要があります。
一方で、通常は 1 次オブジェクトに関係する合成計算可能性の公理から利益を得るには、十分に制限する必要があります。
効果的なトポスの連続関数に基づいた Andrej Bauer の定義からインスピレーションを得て、有効なオラクル計算を特徴付けるために逐次的連続性の概念を使用します。
主な技術的結果として、チューリング還元可能性が上部半格子を形成し、決定可能性を伝達し、真理値表還元可能性よりも厳密に表現力が高いことを示し、述語 $p$ とその補数の両方がオラクルに対して半決定可能であることを証明します。
$q$、次に $p$ チューリング還元により $q$ になります。

要約(オリジナル)

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$.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google