論文の概要: Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
- arxiv url: http://arxiv.org/abs/2605.01032v1
- Date: Fri, 01 May 2026 18:59:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-05 20:33:49.545502
- Title: Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
- Title（参考訳）: 強制執行の代数的意味論:モノイドカテゴリー、エフェクト代数、および境界境界
- Authors: Alan L. McCann,
- Abstract要約: 本稿では, 統治が公理化され, 構成され, 合理化され, 表現力に富む支配実行のための枠組みを提案する。
三軸ガバナンス アルゲブラレコードは、検証された五角形、三角形、六角形のコヒーレンスを持つ対称なモノイダル圏を誘導する。
双対保証定理は、in within_caps と gov_safe が全ての合成演算子の下で同時に保持されることを確立する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: We present an algebraic semantics for governed execution in which governance is axiomatized, compositional, and coterminous with expressibility. The framework, mechanized in 32 Rocq modules (~12,000 lines, 454 theorems, 0 admitted), is built on interaction trees and parameterized coinduction. A three-axiom GovernanceAlgebra record (safety, transparency, properness) induces a symmetric monoidal category with verified pentagon, triangle, and hexagon coherence, where every tensor composition preserves governance. An algebraic effect system constrains the handler algebra so that only governance-preserving handlers can be constructed in the safe fragment; programs in the empty capability set provably emit only observability directives. Capability-indexed composition bundles programs with machine-checked capability bounds, and a dual guarantee theorem establishes that within_caps and gov_safe hold simultaneously under all composition operators. The capstone result is the coterminous boundary: within our formal model, every program expressible via the four primitive morphism constructors is governed under interpretation, and every governed program is the image of such a program. Turing completeness is preserved inside governance; unmediated I/O is excluded from the governed fragment. Governance denial is modeled as safe coinductive divergence. The governance algebra is parametric: any system instantiating the three axioms inherits all derived properties, including convergence, compositional closure, and goal preservation. Extracted OCaml runs as a NIF in the BEAM runtime, with property-based testing (70,000+ random inputs, zero disagreements) confirming behavioral equivalence between the specification and the runtime interpreter.
- Abstract（参考訳）: 本稿では, 統治が公理化され, 構成的で, 表現性に富む, 支配的実行のための代数的意味論を提案する。
このフレームワークは32のRocq加群(約12,000行、454の定理、0が認められている)で機械化され、相互作用木とパラメタライズド・コインダクションの上に構築されている。
三軸ガバナンス アルゲブラ記録(安全、透明性、適正性)は、検証された五角形、三角形、六角形のコヒーレンスを持つ対称なモノイダル圏を誘導し、すべてのテンソル構成がガバナンスを保存する。
代数効果系はハンドラ代数を制約し、ガバナンス保存ハンドラのみを安全なフラグメント内に構築することができる。
キャパビリティインデックス付き合成は、マシンチェックされた機能境界を持つプログラムをバンドルし、二重保証定理は、in within_caps と gov_safe が全てのコンポジション演算子の下で同時に保持されることを保証する。
私たちの形式モデルでは、4つの原始射影コンストラクタを通して表現可能な全てのプログラムは解釈の下で制御され、全ての支配されたプログラムはそのようなプログラムのイメージである。
チューリング完全性はガバナンス内で保持され、非仲介I/Oは管理されたフラグメントから除外される。
ガバナンスの否定は、安全なコインダクティブな分散としてモデル化されている。
ガバナンス代数はパラメトリックであり、3つの公理をインスタンス化する任意の系は、収束、構成的閉包、ゴール保存を含むすべての派生した性質を継承する。
抽出されたOCamlはBEAMランタイムでNIFとして動作し、プロパティベースのテスト(70,000以上のランダムな入力、ゼロの不一致)により仕様と実行時インタプリタ間の振る舞いの等価性を確認する。
関連論文リスト
- Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries [0.0]
構造的に管理されたAIワークフローアーキテクチャのマシンチェック形式化を提案する。
我々は、内部の計算表現性を低下させることなく、効果レベルのガバナンスを課すことを証明した。
論文 参考訳（メタデータ） (2026-05-01T18:52:47Z) - The Two Boundaries: Why Behavioral AI Governance Fails Structurally [0.0]
私たちは、AIシステムが世界で果たす効果のガバナンス、アクションに重点を置いています。
ライスの定理は、このギャップがチューリング完全アーキテクチャの一般的な場合では決定できないことを証明している。
我々は,任意のAIガバナンスシステムの検証可能な基準として,コーディネートガバナンスを提案する。
論文 参考訳（メタデータ） (2026-04-30T01:12:32Z) - 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) - Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
T は形式定理の意味的正しさを評価する枠組みである。
5つの実世界のLean 4リポジトリからベンチマークを構築します。
実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
論文 参考訳（メタデータ） (2026-04-26T13:24:20Z) - BLaDA: Bridging Language to Functional Dexterous Actions within 3DGS Fields [44.48260058069929]
構造化されていない環境では、機能的デクスタラスな把握は意味理解の緊密な統合、正確な3D機能局在化、物理的に解釈可能な実行を要求する。
BLaDAは,開語彙命令を知覚的および制御的制約として根拠として,機能的デキスタス操作のための解釈可能なゼロショットフレームワークである。
BLaDAは、様々なカテゴリやタスクにおける機能的操作の成功率と精度の両方において、既存の手法を著しく上回っている。
論文 参考訳（メタデータ） (2026-04-09T16:10:20Z) - A Monad-Based Clause Architecture for Artificial Age Score (AAS) in Large Language Models [0.0]
この研究は、大規模言語モデルに法則的な制約を課すエンジニアリング指向の節ベースのアーキテクチャを開発する。
ライプニッツのモナドロジーから選ばれた20のモナドは6つのバンドルに分けられる。
6つの最小限のPython実装は、チャネルレベルの量に作用する数値実験でインスタンス化される。
論文 参考訳（メタデータ） (2025-12-03T12:48:40Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - A Foundational Theory of Quantitative Abstraction: Adjunctions, Duality, and Logic for Probabilistic Systems [2.362412515574206]
大規模あるいは連続的な状態空間は、正確に解析しやすくし、原理化された量的抽象を要求する。
この研究は、圏論、コレージュブラ、量論理、最適輸送を統合することで、そのような抽象の統一理論を発展させる。
論文 参考訳（メタデータ） (2025-10-22T10:16:24Z) - Pure state entanglement and von Neumann algebras [41.94295877935867]
我々は、フォン・ノイマン代数の交換で表される二部量子系に対する局所演算の理論と古典的通信(LOCC)を開発する。
我々の中心的な成果はニールセンの定理の拡張であり、二分極純状態のLOCC順序はそれらの制限のメジャー化と等価である、と述べている。
付録では、半有限フォン・ノイマン代数と$sigma$-finite測度空間上の偏化の自己完備な処理を提供する。
論文 参考訳（メタデータ） (2024-09-26T11:13:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。