論文の概要: ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics

• arxiv url: http://arxiv.org/abs/2606.03063v1
• Date: Tue, 02 Jun 2026 02:51:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-03 22:00:04.70743
• Title: ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
• Title（参考訳）: ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
• Authors: Peng Chen,
• Abstract要約: 我々は Martin-Lof Dependent Type (MLTT) の保守的な拡張である ZX-Calculus (Knowledge Evolution Calculus) を提案する。 これは、トレースインデクシングされたタイプ、プレシーフ非モノトーン意味論、建設的なAGM信条修正を統合している。 Coq の機械化は論文に付随する(34の完全証明、0は2つの中心的な結果を認めている)。
• 参考スコア（独自算出の注目度）: 3.848983210046659
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We propose ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Lof Dependent Type Theory (MLTT) integrating trace-indexed types, presheaf non-monotone semantics, and constructive AGM belief revision. A Coq mechanisation accompanies the paper (34 complete proofs; zero admits for the two central results). (I) Trace types. FinTrace(s0,sn) is an inductive family of typed execution traces. FinTrace and Star(Step) are isomorphic as path types but not judgementally equal; TraceElim exposes the event label e:Event explicitly, giving a more ergonomic interface for event-driven induction. We prove the Trace-Reachability Correspondence, Deterministic Replay, and a canonicity framework via reducibility candidates with a Transport Lemma (RC-elim deferred; all other Core results are Coq-verified). (II) Sheaf semantics. Trace-indexed propositions are contravariant sheaves over the free trace partial-order category Tf. A Separation Theorem (explicit countermodel) distinguishes proof-theoretic monotonicity from semantic non-monotonicity. The term model is an initial CwF (syntactic universal property, not classical completeness). (III) AGM belief revision. We give an explicit constructive partial meet contraction algorithm verified against (C1)-(C4). All eight AGM postulates (R1)-(R8) are theorems. Proofs of R7 and R8 use the Disjunctive Entrenchment Lemma, given a self-contained constructive derivation. (IV) Integration. B^AGM fails the sheaf composition law BP-comp for sequential revision (explicit countermodel, Coq-verified). We introduce Single-Step Revision Systems (SSRS), prove B^AGM is a valid SSRS (Coq-verified), and show this suffices for trace morphisms, retraction characterisation, and revision witnesses. The BP-comp failure reveals a fundamental tension between path-dependent belief revision and functor consistency, not previously identified.
• Abstract（参考訳）: 本稿では, トレースインデックス型, 非単調なセマンティクス, 建設的 AGM 信念リビジョンを統合した Martin-Lof Dependent Type Theory (MLTT) の保守的拡張である ZX-Calculus (Knowledge Evolution Calculus) を提案する。 Coq の機械化は論文(34の完全証明、0は2つの中心的な結果を認めている)に付随する。 (I)トレース型。 FinTrace(s0,sn)は型付き実行トレースの帰納的ファミリである。 TraceElimはイベントラベルe:Eventを明示的に公開し、イベント駆動誘導のためのより人間工学的なインターフェースを提供します。 本稿では,Trace-Reachability Cor correspondingence, Deterministic Replay, and a canonicity framework via a reducibility candidate with a Transport Lemma (RC-elim deferred; all other core results are Coq-verified。 (II) 意味論。 トレースインデックス付き命題は、自由トレース部分順序圏 Tf 上の異変層である。 分離定理 (Explicit countermodel) は、証明理論の単調性と意味論的非単調性とを区別する。 項モデルは初期CwF(シンタクティック普遍性、古典的完全性ではない)である。 (III) AGM信条改正。 本稿では, (C1)-(C4) に対して明示的な構成的部分集合縮合アルゴリズムを提案する。 8つの AGM 仮定 (R1)-(R8) はすべて定理である。 R7 と R8 の証明は、自己完備な構成的導出を与える Disjunctive Entrenchment Lemma を用いている。 (4) 統合。 B^AGM はシーケンシャルリビジョンのための層組成法 BP-comp に失敗する(特殊対向モデル、Coq-verified)。 SSRS(Single-Step Revision Systems)を導入し,B^AGMが有効なSSRSであることを示す。 BP-compの故障は、経路依存的信念の修正と関手一貫性の基本的な緊張関係を明らかにする。

関連論文リスト

• LC-ERD: Mining Latent Logic for Self-Evolving Reasoning via Consistency-Regulated Reward Decomposition [55.572260012037084]
  本稿では, LC-ERD (Logic-Consistent Endogenous Reward Decomposition) を紹介する。 モデルの潜在論理エキスパートズ(Latent Logic Expertise)からのコンセンサスを集約することで、変分論理ポテンシャルを導出する。 LC-ERDは、論理の一貫性と正確性の間のトレードオフを明らかにする、堅牢な自己進化パスを提供する。
  論文  参考訳（メタデータ） (2026-05-19T07:27:50Z)
• NOETHER: A Constructive Framework for Metamorphic Pattern Discovery from Operator Algebras [6.691613382732758]
  メタモルフィックテストはIEEE/ISOソフトウェアテスト標準で認識され、AIシステムに対してますます推奨される。 既存のアプローチでは,3つの基本的疑問が残る帰納的根拠を共有している。 本稿では,演算子代数からメタパタン集合への下流ステップが機械的かつ証明可能なフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-05-17T11:18:35Z)
• Probing Structural Mathematical Reasoning in Language Models with Algebraic Trapdoors [0.0]
  言語モデルにおける構造的数学的推論を評価するためのベンチマークスイートを提案する。 各インスタンスは有限生成された部分群を整数行列のリストとして提示する。 本稿では,2つの最先端モデルから得られた5つの代表的な推論指標について実験結果について報告する。
  論文  参考訳（メタデータ） (2026-05-05T23:16:30Z)
• Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence [0.0]
  認知ワークフローシステムにおける構造ガバナンス理論の5つの結果を示す。 Coq 8.19の3つは、相互干渉木ライブラリーと機械化造幣を用いており、2つは明らかに還元された紙上で証明されている。 6番目のコントリビューションは、抽象モデルをデプロイされたランタイムに接続する。
  論文  参考訳（メタデータ） (2026-04-30T01:03:15Z)
• Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
  我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。 DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。 クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
  論文  参考訳（メタデータ） (2026-04-20T22:02:57Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• ARCHE: A Novel Task to Evaluate LLMs on Latent Reasoning Chain Extraction [70.53044880892196]
  本稿では、複雑な推論引数を標準推論パラダイムの組み合わせに分解し、Reasoning Logic Tree (RLT) という形で分解しなければならない、ARCHE(Latent Reasoning Chain extract)という新しいタスクを紹介する。 この作業を容易にするために,我々は,1,900以上の参照と38,000の視点を含む70のNature Communicationsの記事から得られた新しいベンチマークであるARCHE Benchをリリースする。 ARCHE Bench上での10のLLMの評価では、モデルがREAとECのトレードオフを示しており、完全な標準推論チェーンを抽出することはできません。
  論文  参考訳（メタデータ） (2025-11-16T07:37:09Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)

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

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