

















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.
| Comments: | 26 pages, 1 figure, 1 table. Companion proofs: this https URL. Project: this https URL. Updated license |
| Subjects: | Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Programming Languages (cs.PL) |
| MSC classes: | D.2.4, D.3.1, F.3.1, I.2.0 |
| Cite as: | arXiv:2605.01032 [cs.AI] |
| (or arXiv:2605.01032v3 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2605.01032 arXiv-issued DOI via DataCite |
From: Alan McCann [view email]
[v1]
Fri, 1 May 2026 18:59:01 UTC (24 KB)
[v2]
Tue, 5 May 2026 10:30:32 UTC (24 KB)
[v3]
Tue, 26 May 2026 12:41:10 UTC (24 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。