受控执行的代数语义：单色范畴、效应代数与共终止边界

我们提出了一种受控执行的代数语义框架，其中治理被形式化为公理化、可组合且与可表达性共终止的概念。该框架在 32 个 Rocq 模块中实现（约 12,000 行代码、454 个定理、0 个已接受引理），基于交互树和参数化共演化构建。一个包含三个公理（安全性、透明性、适当性）的 GovernanceAlgebra 记录可诱导一个对称单色范畴，经验证的五边形、三角形和六边形相干性均满足，其中每个张量组合都保持治理。一个代数效应系统约束处理器代数，使得只有可构造的治理保护处理器才能在安全片段中实现；能力集为空的程序必然仅发出可观测指令。能力索引的组合将程序与机器检验的能力边界捆绑在一起，一个二元保证定理确立了 within_caps 与 gov_safe 在所有组合运算符下同时成立。最高成果是共终止边界：在我们的形式模型中，通过四个原始态射构造器可表达的每个程序在解释下都受控，而每个受控程序都是此类程序的像。图灵完备性在治理内部得以保持；未经调节的 I/O 被排除在受控片段之外。治理否定建模为安全的共演化发散。该治理代数是参数化的：任何实例化这三个公理的系统都继承所有派生属性，包括收敛性、组合闭合性和目标保持。提取的 OCaml 代码可作为 BEAM 运行时的 NIF 运行，基于属性测试（70,000+ 随机输入、零差异）确认了规范与运行时解释器之间的行为等价性。