論文の概要: Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions

• arxiv url: http://arxiv.org/abs/2307.15543v1
• Date: Fri, 28 Jul 2023 13:16:46 GMT
• ステータス: 処理完了
• システム内更新日: 2023-07-31 12:36:13.225794
• Title: Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
• Title（参考訳）: インダクティブ・コンストラクションの計算におけるOracleの計算可能性とチューリング低減性
• Authors: Yannick Forster, Dominik Kirst, Niklas M\"uck
• Abstract要約: インダクティブ・コンストラクションの計算におけるオラクル計算可能性とチューリング再現性の概念を総合的に展開する。 通常、合成手法では、メタレベル関数に基づいたオラクル計算の定義を用いる。 チューリングの再現性は上半格子を形成し、決定可能性を持ち、真理値の再現性よりも厳密に表現可能であることを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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$.
• Abstract（参考訳）: 我々は,coq 証明アシスタントの基礎となる構成型理論である inductive constructions (cic) において,oracle の計算可能性とチューリングの還元可能性に関する合成概念を開発する。 通常の合成手法では、CICのような構成系では、すべての定義可能な関数が構成によって計算可能であるという事実に依拠し、オブジェクトレベルの計算モデルではなくメタレベルの関数に基づくオラクル計算の定義を用いる。 このようなアプローチは、coqで実行するマシンチェックされた証明に適しています。 オラクル計算可能性という高次概念の優れた合成レンダリングを見つけるには緊張がある。 一方で、すべての概念が忠実に捉えられるように、中心的な結果を証明するのに十分な情報が必要である。 一方、合成計算可能性のための公理の恩恵を受けるには十分な制限が必要であり、これは通常一階のオブジェクトに関係している。 効果的な topos における連続関数に基づく andrej bauer の定義から着想を得て,oracle の有効な計算を特徴付けるシーケンシャル連続性の概念を用いた。 主な技術的結果として、チューリングの再現性は上半ラッチを形成し、決定性を持ち、真理値よりも厳密に表現され、述語$p$とその補語の両方がオラクル$q$に対して半決定可能であれば、$p$チューリングの還元は$q$となることを示す。

関連論文リスト

• On Computational Indistinguishability and Logical Relations [1.024113475677323]
  この研究は、疑似乱数関数によって誘導される暗号化スキームが、純粋に方程式的なスタイルでアクティブな敵に対して安全であることが証明されたセキュリティ証明の例で締めくくられる。
  論文  参考訳（メタデータ） (2024-08-30T15:08:51Z)
• On the Representational Capacity of Neural Language Models with Chain-of-Thought Reasoning [87.73401758641089]
  CoT推論による現代言語モデル(LM)の性能向上 LMは弦上の分布の族を確率的チューリングマシンと同一に表現できることを示す。
  論文  参考訳（メタデータ） (2024-06-20T10:59:02Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
  本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。 具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。 コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
  論文  参考訳（メタデータ） (2023-08-29T17:22:39Z)
• Efficient Computation of Counterfactual Bounds [44.4263314637532]
  我々は,構造因果モデルのサブクラスにおけるクレダルネットのアルゴリズムを用いて,正確な反ファクト境界を計算する。 近似の精度を信頼性のある間隔で評価する。
  論文  参考訳（メタデータ） (2023-07-17T07:59:47Z)
• The vacuum provides quantum advantage to otherwise simulatable architectures [49.1574468325115]
  理想のゴッテマン・キタエフ・プレスキル安定化状態からなる計算モデルを考える。 測定結果の確率密度関数を計算するアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-05-19T18:03:17Z)
• Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
  マッチングやアリティ向上の活性化関数を用いて,任意の論理を単一層で学習できることが示される。 我々は,非ゼロパラメータの数を信念関数の有効アリティに直接関連付ける基礎を用いて,信念表を表現する。 これにより、パラメータの間隔を誘導することで論理的複雑性を低減する最適化アプローチが開かれる。
  論文  参考訳（メタデータ） (2022-03-16T22:47:53Z)
• Resource Optimisation of Coherently Controlled Quantum Computations with the PBS-calculus [55.2480439325792]
  量子計算のコヒーレント制御は、いくつかの量子プロトコルやアルゴリズムを改善するために使用できる。 我々は、量子光学にインスパイアされたコヒーレント制御のためのグラフィカル言語PBS計算を洗練する。
  論文  参考訳（メタデータ） (2022-02-10T18:59:52Z)
• Statistically Meaningful Approximation: a Case Study on Approximating Turing Machines with Transformers [50.85524803885483]
  本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。 回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
  論文  参考訳（メタデータ） (2021-07-28T04:28:55Z)
• Programming by Rewards [20.626369097817715]
  我々は、性能、資源利用、あるいはベンチマーク上の正確性などの量的指標を最適化するための新しいアプローチである「報酬によるプログラミング」 (PBR) を定式化し、研究する。 PBR仕様は、(1)入力機能$x$と(2)報酬関数$r$で構成され、ブラックボックスコンポーネントとしてモデル化されている(実行しかできない)。 フレームワークは理論的に確立された -- 報酬が優れた特性を満たす場合において、合成されたコードは正確な意味で最適であることを示す。
  論文  参考訳（メタデータ） (2020-07-14T05:49:14Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。