用代数方法构建可验证的程序治理模型，确保安全与表达能力同步。
Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
- 基于交互树和共归纳的代数框架，通过三公理定义治理机制
- 证明所有组合操作均保持治理性，且表达力与治理范围完全匹配
- 适用于需要强安全保障的系统开发，如高可信运行时
本文提出一种代数语义框架，对受控执行进行形式化建模。该框架基于交互树与参数化共归纳，以三个公理（安全性、透明性、正确性）定义治理代数，构造出满足五边形、三角形与六边形一致性条件的对称单幕范畴，所有张量组合均保持治理性。一个代数效应系统限制处理器代数，仅允许构造保持治理性的处理器；在空权限集下的程序仅输出可观测指令。权限索引的组合机制为程序绑定机器可验证的权限边界，双重保证定理表明 within_caps 与 gov_safe 在所有组合算子下同时成立。核心成果为‘共终止边界’：在本模型中，所有由四种基本态射构造器表达的程序，在解释下均为受控的，且每个受控程序都是此类程序的像。图灵完备性在治理范围内得以保留，未受控输入输出被排除于受控片段之外。治理拒绝建模为安全的共归纳发散。治理代数是参数化的，任何满足三公理的系统自动继承全部推导性质，包括收敛性、组合封闭性与目标保持性。提取的 OCaml 代码作为 BEAM 运行时的 NIF 模块运行，基于属性的测试（70,000+ 随机输入，零分歧）确认了规范与运行时解释器的行为等价。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。