Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries

受控执行的代数语义：幺半范畴、效应代数与共界边界

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.

摘要： 我们提出了一种受控执行的代数语义，其中治理（governance）被公理化、具有组合性，并与表达能力共界（coterminous）。该框架在 32 个 Rocq 模块中实现（约 12,000 行代码，454 条定理，0 条公理假设），构建于交互树（interaction trees）和参数化共归纳（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.

一个包含三条公理的 GovernanceAlgebra 记录（安全性、透明性、规范性）导出了一个对称幺半范畴，并验证了五边形、三角形和六边形相干性，其中每个张量组合都保持了治理属性。代数效应系统限制了处理器代数，使得在安全片段中只能构建保持治理的处理器；空能力集中的程序可证明仅发出可观测性指令。

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.

能力索引组合将程序与机器检查的能力边界捆绑在一起，且双重保证定理确立了在所有组合算子下，within_caps（能力范围内）和 gov_safe（治理安全）同时成立。核心成果是共界边界：在我们的形式模型中，每个可通过四个原始态射构造子表达的程序在解释下都是受控的，且每个受控程序都是此类程序的映射。

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.

图灵完备性在治理内部得以保留；未经中介的 I/O 被排除在受控片段之外。治理拒绝被建模为安全的共归纳发散。治理代数是参数化的：任何实例化这三条公理的系统都将继承所有派生属性，包括收敛性、组合闭包和目标保持性。

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.

提取出的 OCaml 代码作为 NIF（原生实现函数）在 BEAM 运行时中运行，通过基于属性的测试（70,000 多次随机输入，零冲突）证实了规范与运行时解释器之间的行为等价性。