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

• URL: http://arxiv.org/abs/2605.01032v2
• Date: Tue, 05 May 2026 10:30:32 GMT
• Title: Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
• Abstract summary: We present a framework for governed execution in which governance is axiomatized, compositional, and coterminous with expressibility.<n>A three-axiom GovernanceAlgebra record induces a symmetric monoidal category with verified pentagon, triangle, and hexagon coherence.<n>A dual guarantee theorem establishes that within_caps and gov_safe hold simultaneously under all composition operators.
• Score: 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.

Related papers

• A Compositional Theory of Causally Masked Transformers [50.88598486616582]
  We develop a formalization that derives expressivity directly from the model's implemented dynamics.<n>Each attention head updates its own state independently within a layer.<n>A modified form of soft attention supports irreversible, checklist-like state.
  arXiv  Detail & Related papers  (2026-07-29T14:47:19Z)
• Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization [25.540859911959885]
  Autoformalization (AF) asks a model to translate informal mathematical or logical reasoning into a formally checkable object.<n>We introduce a reference-free proxy-judge framework for AF that replaces gold-standard matching with a vector of per-axis property checks.<n>Across seven formalization backbones on miniF2F, ProofNet, e-SNLI, and ProntoQA, refinement consistently lifts Pass Rate over the single-shot ICL baseline.
  arXiv  Detail & Related papers  (2026-06-08T12:57:09Z)
• When Rule Violations Are Rare: Chimera Training for Logical Anomaly Detection [56.362776482614976]
  We study anomaly detection in a setting where constraints are given as logical rules over learned visual concepts.<n>We propose a neural rule evaluator that compiles each constraint into a directed acyclic graph and learns feature-aware subtree gates.<n>Across CLEVRER, OpenImages, and VidOR, the resulting evaluator improves rule-level anomaly AUROC over independent-events and same-image semantic-training baselines.
  arXiv  Detail & Related papers  (2026-05-25T02:52:36Z)
• NOETHER: A Constructive Framework for Metamorphic Pattern Discovery from Operator Algebras [6.691613382732758]
  Metamorphic Testing is recognised in IEEE/ISO software-testing standards and increasingly recommended for AI systems.<n>Existing approaches share an inductive grounding that leaves three foundational questions open.<n>We propose a framework whose downstream step from operator algebra to MetaPattern set is mechanical and provable.
  arXiv  Detail & Related papers  (2026-05-17T11:18:35Z)
• CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
  CktFormalizer is a framework that redirects hardware generation through a dependently-typed HDL embedded in Lean 4.<n>On VerilogEval (156 problems), RTLLM (50 problems), and ResBench (56 problems), CktFormalizer achieves simulation pass rates competitive with direct Verilog generation.
  arXiv  Detail & Related papers  (2026-05-08T14:20:06Z)
• Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries [0.0]
  We present a machine-checked formalization of structurally governed AI workflow architectures.<n>We prove that effect-level governance can be imposed without reducing internal computational expressivity.
  arXiv  Detail & Related papers  (2026-05-01T18:52:47Z)
• The Two Boundaries: Why Behavioral AI Governance Fails Structurally [0.0]
  We focus on the governance of effects, actions that AI systems perform in the world.<n>Rice's theorem proves the gap is undecidable in the general case for Turing-complete architecture.<n>We propose coterminous governance as the testable criterion for any AI governance system.
  arXiv  Detail & Related papers  (2026-04-30T01:12:32Z)
• Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence [0.0]
  We present five results in the theory of structural governance for cognitive workflow systems.<n>Three are in Coq 8.19 using the Interaction Trees library with mechanizedized coinduction; two are proved on paper with explicit reductions.<n>A sixth contribution connects the abstract model to the deployed runtime: the Verified Interpreter Specification.
  arXiv  Detail & Related papers  (2026-04-30T01:03:15Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T is a framework that evaluates the semantic correctness of formal theorems.<n>We construct a benchmark from 5 real-world Lean 4 repositories.<n>Experiments demonstrate that while state-of-the-art models achieve high compilation success, they perform significantly worse under our semantic metric.
  arXiv  Detail & Related papers  (2026-04-26T13:24:20Z)
• BLaDA: Bridging Language to Functional Dexterous Actions within 3DGS Fields [44.48260058069929]
  In unstructured environments, functional dexterous grasping calls for the tight integration of semantic understanding, precise 3D functional localization, and physically interpretable execution.<n>We propose BLaDA, an interpretable zero-shot framework that grounds open-vocabulary instructions as perceptual and control constraints for functional dexterous manipulation.<n>BLaDA significantly outperforms existing methods in both affordance grounding precision and the success rate of functional manipulation across diverse categories and tasks.
  arXiv  Detail & Related papers  (2026-04-09T16:10:20Z)
• A Monad-Based Clause Architecture for Artificial Age Score (AAS) in Large Language Models [0.0]
  This work develops an engineering-oriented, clause-based architecture that imposes law-like constraints on large language models.<n>Twenty selected monads from Leibniz's Monadology are grouped into six bundles.<n>Six minimal Python implementations are instantiated in numerical experiments acting on channel-level quantities.
  arXiv  Detail & Related papers  (2025-12-03T12:48:40Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• A Foundational Theory of Quantitative Abstraction: Adjunctions, Duality, and Logic for Probabilistic Systems [2.362412515574206]
  Large or continuous state spaces make exact analysis intractable and call for principled quantitative abstraction.<n>This work develops a unified theory of such abstraction by integrating category theory, coalgebra, quantitative logic, and optimal transport.
  arXiv  Detail & Related papers  (2025-10-22T10:16:24Z)
• Pure state entanglement and von Neumann algebras [41.94295877935867]
  We develop the theory of local operations and classical communication (LOCC) for bipartite quantum systems represented by commuting von Neumann algebras.<n>Our central result is the extension of Nielsen's Theorem, stating that the LOCC ordering of bipartite pure states is equivalent to the majorization of their restrictions.<n>In the appendix, we provide a self-contained treatment of majorization on semifinite von Neumann algebras and $sigma$-finite measure spaces.
  arXiv  Detail & Related papers  (2024-09-26T11:13:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.