pith. sign in

arxiv: 2605.01032 · v2 · submitted 2026-05-01 · 💻 cs.AI · cs.LO· cs.PL

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

Alan L. McCann This is my paper

Pith reviewed 2026-05-09 19:19 UTC · model grok-4.3

classification 💻 cs.AI cs.LOcs.PL
keywords governed executionmonoidal categorieseffect algebrascoterminous boundariesalgebraic semanticsinteraction treescoinductioncapability systems
0
0 comments X

The pith

Governance is defined so that it exactly coincides with what programs can express using four basic constructors.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs an algebraic model for governed program execution using monoidal categories and effect algebras. It shows that a simple set of three axioms makes governance compositional and ensures it applies precisely to all programs built from the primitives and nothing else. This setup is fully mechanized with thousands of theorems proving coherence and safety properties. The result means that governance can be guaranteed by the way programs are constructed rather than checked after the fact. It keeps the full power of computation while ruling out direct unsafe operations.

Core claim

The central discovery is the coterminous boundary theorem establishing that, in the formal model, the programs expressible via the four primitive morphism constructors are exactly those that are governed under the interpretation. The GovernanceAlgebra with axioms for safety, transparency, and properness generates a symmetric monoidal category where governance is preserved under all compositions, and capability-indexed programs satisfy both bounds and safety simultaneously.

What carries the argument

The coterminous boundary, which equates the set of expressible programs with the set of governed programs, supported by the GovernanceAlgebra that induces a symmetric monoidal category with verified coherence.

If this is right

  • Programs in the empty capability set emit only observability directives.
  • Governance denial appears as safe coinductive divergence.
  • The algebra is parametric, so any system meeting the three axioms inherits convergence, closure, and preservation properties.
  • Turing completeness holds within the governed fragment while excluding unmediated input/output.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This suggests governance can be enforced at the level of program construction in verified systems.
  • Similar algebraic approaches might apply to other properties like security or resource bounds in programming languages.
  • Extracted code running in real environments confirms the model matches practical interpreters.

Load-bearing premise

That the three axioms of safety, transparency, and properness on the governance algebra are sufficient to create a symmetric monoidal category where every tensor and composition preserves governance.

What would settle it

Constructing a program from the four primitives that violates one of the governance properties when interpreted, or identifying a governed behavior that cannot be built from those primitives.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper presents an algebraic semantics for governed execution, axiomatizing governance via a GovernanceAlgebra record with three axioms (safety, transparency, properness) that induce a symmetric monoidal category with verified coherence (pentagon, triangle, hexagon) where tensor composition preserves governance. Built on interaction trees and parameterized coinduction, the development is mechanized in 32 Rocq modules (~12,000 lines, 454 theorems, 0 admits) and includes an algebraic effect system restricting handlers to governance-preserving ones, capability-indexed composition with dual guarantee theorems for within_caps and gov_safe, and the capstone coterminous boundary result equating programs from four primitive morphism constructors with governed programs under interpretation. Turing completeness is preserved, unmediated I/O is excluded, governance denial is modeled as safe coinductive divergence, and the framework is parametric with OCaml extraction and property-based testing on 70,000+ inputs confirming equivalence to the runtime.

Significance. If the mechanized results hold, the work provides a rigorous parametric foundation for governed execution that is compositional, preserves Turing completeness, and aligns expressibility exactly with governance via the coterminous boundary. The machine-checked proofs (454 theorems, zero admits), use of interaction trees with parameterized coinduction, extensive property-based testing, and OCaml extraction to BEAM runtime are notable strengths that lend substantial credibility. This could serve as a reusable algebraic basis for safe AI effect systems and runtimes, with any instantiation of the three axioms inheriting the derived properties including convergence and goal preservation.

minor comments (3)
  1. Abstract: The four primitive morphism constructors are referenced without being named or defined; an explicit enumeration or brief description early in the paper would improve readability for readers unfamiliar with the specific algebraic setup.
  2. Mechanization overview: While the 32 Rocq modules and 454 theorems are highlighted, a summary table or dependency diagram of the key modules (e.g., those establishing the monoidal category and the coterminous boundary) would aid navigation of the formal development.
  3. Coterminous boundary section: The capstone equivalence could be stated more prominently as a boxed theorem with an explicit 'if and only if' formulation to emphasize its central role.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive and detailed summary of our work, including recognition of the mechanized development in Rocq, the coterminous boundary result, preservation of Turing completeness, and the parametric nature of the governance algebra. The recommendation for minor revision is noted, and we will make any necessary adjustments in the revised version. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper derives its central coterminous boundary result directly from the three-axiom GovernanceAlgebra record (safety, transparency, properness) via mechanized proofs in Rocq. The induced symmetric monoidal category, coherence (pentagon/triangle/hexagon), tensor preservation of governance, and equivalence between programs built from the four primitive morphism constructors and governed programs are all established by 454 theorems with zero admits. The development is parametric on the axioms, uses interaction trees with parameterized coinduction, and includes dual guarantee theorems; no fitted parameters, self-definitional reductions, load-bearing self-citations, or ansatzes are present. Property-based testing on the extracted runtime serves only as external validation, not as part of the formal derivation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 1 invented entities

The framework rests on three domain-specific axioms for governance plus standard background formalisms (interaction trees, parameterized coinduction); no numerical free parameters are introduced.

axioms (3)
  • domain assumption safety
    One of the three axioms in the GovernanceAlgebra record that the monoidal category and all derived properties depend on.
  • domain assumption transparency
    One of the three axioms in the GovernanceAlgebra record that the monoidal category and all derived properties depend on.
  • domain assumption properness
    One of the three axioms in the GovernanceAlgebra record that the monoidal category and all derived properties depend on.
invented entities (1)
  • GovernanceAlgebra record no independent evidence
    purpose: To axiomatize governance so that it is compositional and induces a monoidal category.
    The core structure introduced to define the semantics; no independent evidence outside the formalization is provided.

pith-pipeline@v0.9.0 · 5586 in / 1592 out tokens · 87806 ms · 2026-05-09T19:19:21.711160+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages · 1 internal anchor

  1. [1]

    Constitutional AI: Harmlessness from AI Feedback

    Yuntao Bai, Saurav Kadavath, Sandipan Kundu, Amanda Askell, Jackson Kernion, Andy Jones, Anna Chen, Anna Goldie, Azalia Mirhoseini, Cameron McKinnon, et al. Constitutional AI: Harmlessness from AI feedback.arXiv preprint arXiv:2212.08073,

    work page internal anchor Pith review Pith/arXiv arXiv

  2. [2]

    doi: 10.1145/2500365.2500581. Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacC´ arthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook. Continuous formal verification of Amazon s2n. InInternational Conference on Computer Aided Verification (CAV), pages 430–446,

    work page doi:10.1145/2500365.2500581

  3. [3]

    doi: 10.1007/978-3-319-96142-2

    work page doi:10.1007/978-3-319-96142-2

  4. [4]

    Towards guaranteed safe ai: A framework for ensuring robust and reliable ai systems

    David Dalrymple, Joar Skalse, Yoshua Bengio, Stuart Russell, Max Tegmark, Sanjit Seshia, Steve Omohundro, Christian Szegedy, Ben Goldhaber, Nora Ammann, et al. Towards guaranteed safe AI: A framework for ensuring robust and reliable AI systems.arXiv preprint arXiv:2405.06624,

    work page arXiv

  5. [5]

    and Van Horn, Earl C

    doi: 10.1145/365230.365252. 18 Brendan Fong and David I. Spivak.An Invitation to Applied Category Theory: Seven Sketches in Compositionality. Cambridge University Press,

    work page doi:10.1145/365230.365252

  6. [6]

    doi: 10.1017/9781108668804. David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. InACM Conference on LISP and Functional Programming, pages 28–38,

    work page doi:10.1017/9781108668804

  7. [7]

    Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj¨ oberg, and David Costanzo

    doi: 10.1145/319838.319848. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj¨ oberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 653–669,

    work page doi:10.1145/319838.319848

  8. [8]

    The power of parameterization in coinductive proof

    doi: 10.1145/2429069.2429093. Hans H¨ uttel, Ivan Lanese, Vasco T. Vasconcelos, Lu´ ıs Caires, Marco Carbone, Pierre-Malo Deni´ elou, Dimitris Mostrous, Luca Padovani, Ant´ onio Ravara, Emilio Tuosto, et al. Foundations of session types and behavioural contracts.ACM Computing Surveys, 49(1):1–36,

    work page doi:10.1145/2429069.2429093

  9. [9]

    ACM Comput

    doi: 10.1145/2873052. Andr´ e Joyal and Ross Street. Braided tensor categories. InAdvances in Mathematics, volume 102, pages 20–78,

    work page doi:10.1145/2873052

  10. [10]

    B., et al

    doi: 10.1006/aima.1993.1055. Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. InACM SIGPLAN Haskell Symposium, pages 94–105,

    work page doi:10.1006/aima.1993.1055 1993

  11. [11]

    doi: 10.1145/2804302.2804319. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. InACM Symposium on Operating Systems Principles (SOSP), pages 207–220,

    work page doi:10.1145/2804302.2804319

  12. [12]

    seL4: formal verification of an OS kernel,

    doi: 10.1145/1629575.1629596. Daan Leijen. Type directed compilation of row-typed algebraic effects.Proceedings of the ACM on Programming Languages, 1(POPL):1–28,

    work page doi:10.1145/1629575.1629596

  13. [13]

    In: Proceedings of the 44th ACM SIGPLAN Sympo- sium on Principles of Programming Languages (POPL)

    doi: 10.1145/3009837.3009872. Xavier Leroy. Formal verification of a realistic compiler.Communications of the ACM, 52(7): 107–115,

    work page doi:10.1145/3009837.3009872

  14. [14]

    Communications of the ACM 52(7), pp

    doi: 10.1145/1538788.1538814. Pierre Letouzey. A new extraction for Coq. InTypes for Proofs and Programs (TYPES), pages 200–219,

    work page doi:10.1145/1538788.1538814

  15. [15]

    doi: 10.1007/3-540-39185-1

    work page doi:10.1007/3-540-39185-1

  16. [16]

    doi: 10.1007/978-3-540-69407-6

    work page doi:10.1007/978-3-540-69407-6

  17. [17]

    doi: 10.1016/j.jlap.2008.08.004. John M. Lucassen and David K. Gifford. Polymorphic effect systems. InACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL), pages 47–57,

    work page doi:10.1016/j.jlap.2008.08.004 2008

  18. [18]

    Lucassen and David K

    doi: 10.1145/73560.73564. Saunders Mac Lane.Categories for the Working Mathematician, volume 5 ofGraduate Texts in Mathematics. Springer-Verlag,

    work page doi:10.1145/73560.73564

  19. [19]

    19 Alan Lawrence McCann

    doi: 10.1007/978-1-4612-9839-7. 19 Alan Lawrence McCann. Effect-transparent governance for AI workflow architectures: Semantic preservation, expressive minimality, and decidability boundaries, 2026a. Alan Lawrence McCann. Mechanized foundations of structural governance: Machine-checked proofs for governed intelligence, 2026b. Alan Lawrence McCann. Cryptog...

    work page doi:10.1007/978-1-4612-9839-7

  20. [20]

    doi: 10.1007/978-3-642-00590-9

    work page doi:10.1007/978-3-642-00590-9

  21. [21]

    Gordon D

    doi: 10.1023/A:1023064908962. Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects.Logical Methods in Computer Science, 9(4):1–36,

    work page doi:10.1023/a:1023064908962

  22. [22]

    Traian Rebedea, Razvan Dinu, Makesh Narsimhan Sreedhar, Christopher Parisien, and Jonathan Cohen

    doi: 10.2168/LMCS-9(4:23)2013. Traian Rebedea, Razvan Dinu, Makesh Narsimhan Sreedhar, Christopher Parisien, and Jonathan Cohen. NeMo guardrails: A toolkit for controllable and safe LLM applications with programmable rails. InConference on Empirical Methods in Natural Language Processing (EMNLP), System Demonstrations,

    work page doi:10.2168/lmcs-9(4:23)2013 2013

  23. [23]

    Kasper Svendsen Vistrup, Simon Spies, Amin Timany, and Derek Dreyer

    doi: 10.1145/3674633. Kasper Svendsen Vistrup, Simon Spies, Amin Timany, and Derek Dreyer. Program logics a la carte. InProceedings of the ACM on Programming Languages (POPL), volume 9,

    work page doi:10.1145/3674633

  24. [24]

    Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C

    doi: 10.1145/3704860. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: Representing recursive and impure programs in Coq. Proceedings of the ACM on Programming Languages, 4(POPL):1–32,

    work page doi:10.1145/3704860

  25. [25]

    Pierce, and Steve Zdancewic

    doi: 10.1145/3371119. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. Modular, compositional, and executable formal semantics for LLVM IR.Proceedings of the ACM on Programming Languages, 5(ICFP):1–30,

    work page doi:10.1145/3371119

  26. [26]

    Modular, compositional, and executable formal semantics for LLVM IR

    doi: 10.1145/3473572. 20 A Rocq Module Index Table 2 lists all 36 modules with their primary theorems. All theorem names are valid Rocq identifiers that can be checked in the mechanization. 21 Table 2: Complete Rocq module index with primary theorems. Module Lines Primary Theorems Prelude 31 (base definitions) Directives 245 DirectiveE (14 constructors), ...

    work page doi:10.1145/3473572