A Programming Paradigm for Spatiotemporal Composability

一、插件卸载只有重启一条路：撤销缺形式基础

1.1 一个具体场景

你维护一个聊天机器人框架：功能全是插件——平台适配器插件负责连接聊天平台，数据库插件负责连库，签到插件注册 /checkin 命令、每天早上定时推送。某天，用户在控制台里点了”禁用数据库插件”。你心里期望的图景很朴素：签到插件暂停，数据连接干净断开，其他插件不受影响；换成 postgres 后端再启用，签到插件自己恢复运行。

实际发生的事（以 VSCode 为实测对象，§1.2.1，p.4–5）出乎意料：大多数插件系统根本没有”卸载一个组件的效应”这个操作。VSCode 把所有扩展跑在共享的 extension host 进程里，扩展的 activate 一旦执行，禁用或卸载它就得重启整个宿主。按安装量前 100 的扩展统计，87 个含可执行代码，卸载即重启（数据取自 2026-06-09 的 VSCode Marketplace，脚注 1，p.5）。

deactivate 钩子只是宿主退出时的善后回调，不是活体卸载；而且它把效应的创建（activate）和清理（deactivate）拆在两处，清理对不对全靠作者自觉——论文引这一点为”局部性缺失”的证据（p.5）。依赖方面也好不到哪里去：extensionDependencies 几乎无人使用（前 100 里只有 7 个对非内置扩展声明），扩展间交互走 getExtension(...).exports，返回值默认无类型（p.5）。连 VSCode 都没做到的事，你手里的插件系统做到了吗？

那业界的现状是什么？不用这套方案，就把这两件事整个外包出去：把”卸载组件”外包给操作系统（杀进程 = 时间可组合，粒度是整个进程）、把”依赖管理”外包给容器编排（Kubernetes = 空间可组合，粒度是整个服务）（§1.2.3，p.5–6）。代价同样明摆着：每次重启丢光进程内积累的状态（缓存、连接、算到一半的计算），靠冗余副本保可用性；本可以是本地函数调用的交互被迫走网络。

第二个动机场景离本站更近（§1.2.2，p.5）：自进化 agent harness——agent 在持续服务请求的同时生成并部署对自己组件的修改。没有时间可组合，每次自我修改都得重启、丢光状态，而且一次坏的修改可能弄死赖以恢复的进程本身。没有空间可组合，每个模块只能各显神通地感知”我依赖的模块没了/换了”，naive 的代码热替换可能悄悄弄坏下游、或者在重载时才暴露循环依赖（p.5）。

1.2 论文对问题的重述

论文把”动态组合缺形式基础”拆成两个正交维度（§1.1，p.4）：

• 时间可组合性：组件卸载时，它对共享环境做过的所有修改（资源分配、事件注册、状态变更）被完整、安全地撤销。
• 空间可组合性：组件间依赖能以结构化、可验证的方式声明、发现、解析，依赖变化时生命周期被协调。

静态世界里这两个维度分别退化成词法作用域（RAII、bracket 模式）和模块导入解析；动态世界里组件在运行中来去，两个维度同时变难（p.4）。

然后是全文的题眼（§2.3，p.8–9）。效应系统形式化了”计算如何修改环境”，余效应系统形式化了”计算如何依赖环境”——两个维度各有一套现成的静态理论，但它们都是编译期仪器：效应在词法封闭作用域内跟踪、由编译期 handler 消账；余效应注解对着执行前就定死的上下文核对。

猜论文（先猜再往下读）：两台仪器都锁死在编译期——如果是你，第一步动作是什么：往类型系统里加更多注解，还是别的？（reveal 就在下面这段：p.9 原话——方向反过来，不再加注解，而是把效应/余效应的概念结构物化成运行时对象。）

论文的路线（p.9 原话转述）：不再给静态类型系统加更多注解，而是把效应/余效应的概念结构物化（reify），让运行时直接操作它们，动态地重建这些系统静态地提供的保证。注意这个转换的方向——不是把运行时问题抬进类型系统，而是把类型系统的概念搬下来。后文全部机制都是这一步的具体形态。

二、效应自带逆、依赖反应式解析、装卸历史无痕

一句话：把每个副作用做成”变换 + 自带逆”、把每个依赖做成”声明 + 反应式解析”、把两者统一进一个运行时可操作的上下文——装卸组件就从”重启”变成”跑一遍带账本的生成器 / 应用账本”，而且元理论保证：一个跑了任意装卸历史的系统，静息下来时和从头静态装配一次没区别。

这个论断往深一层想，分量落在”自带”和”自动”上。在此之前，撤销靠组件作者写清理回调、写对了无人担保；依赖协调靠各模块自己掂量”我的依赖没了怎么办”。这篇把两件事在使用处的自觉，挪成了定义处的结构：逆在效应被制造的那一刻就被记下，依赖在环境变化的那个瞬间就被分类处理——不靠记性，靠机制。拆开来数，这句话就是三件事：1) 每个副作用自带一份逆；2) 每个依赖进一张反应式解析的表；3) 两者统一进同一个运行时可操作的上下文。后面几段就按这三件事依次展开。

先打个比方。插件往系统里装东西，就像房客往公寓里搬家具。现在的做法是退房时靠房客”记得”把家具搬走（deactivate 回调），忘了就永久占用；更粗暴的公寓干脆规定退房必须整栋楼重建（进程重启）。这篇的方案是给每件搬进来的家具配一张”搬入回执”，公寓前台（运行时）把回执摞成一摞，退房时从顶往下逐张执行——搬了什么、怎么搬回去，结构上有保证，不靠记性。

再把比方译回工程语言。前台那摞回执，就是累积器 φ：一个把上下文还原到组件装载前状态的函数；每件家具的搬入就是一次效应：前向变换 f 加一个逆 g，g 在搬入那一刻被顺手记下。“哪些家具是这家房客的”不需要登记簿，φ 就是登记簿；“签到插件能不能开门营业”也不需要轮询，每次上下文变动都按它的依赖声明被分类为激活/停用/无关。

落到形式上：组件 = (d, p, e) 三元组——声明的依赖 d、可提供的键 p、带见证的效应迭代器 e（定义 48，p.31）；实例 fiber 带生命周期状态机；9 条规则的演算给出操作语义；元理论五组结果（保持、恢复精确性、排序、进展、合流）把单组件的保证抬到系统级（§4.3）。

所以它把问题重新形式化成了什么：把”动态组合”从工程惯例集合（生命周期回调、依赖注入容器、热重载）重构为一个有操作语义和元理论的演算——装卸的正确性是定理，不是纪律。同时它把 effect systems 这门”编译期学问”的适用域从程序文本扩展到了运行时。

三、从撤销需求反推出的五件数学工具

3.1 第一件：monoid 与同态——记账可靠，靠两条律

第一件工具是整台机器的地基，先说为什么需要它：要谈”撤销”，就得有地方记账，而记账最起码的要求是——把账逐条记和一把头汇总，结果必须一样，否则推理任何一段效应序列都得先问”这笔账是怎么分组的”。描述这类结构的语言就是 monoid：一个集合配上一个满足结合律（先加后加不分括号）的运算和一个单位元，也就是”能串联、有空白操作”的代数结构——列表拼接（空列表）、函数复合（恒等）、数字加法（0）。写成定义：monoid (M, ∘, e)：∘ 结合，e 单位。在这个骨架上再要一条”保结构的翻译”，就是同态：两个 monoid 之间的映射 h: M → N，满足 h(e)=e 且 h(x∘y)=h(x)∘h(y)——翻译完再复合 = 复合完再翻译。为什么本篇全篇都是它：track 是同态（Thm 5）意味着记账是可靠的——逐条记和汇总记一致；witness 在 ⋄ 下封闭（Thm 11）意味着链式撤销可靠；effect 提升保 ⋄（Thm 13）意味着层级间行为一致。三个”可靠性”全是同态律，§五和§六的回滚推理踩来踩去都是这块石头。先带一个问题往下走：为什么“逐条记”和“一把算”必须相等？

演绎一：结合律为什么是”记账”的硬前提（补充）。没有结合律，“逐条记”和”一把算”连陈述都写不出：三个效应 x、y、z，先记 x,y 再并 z 得 (x∘y)∘z，先并 y,z 再前置 x 得 x∘(y∘z)——两条路线要落在同一个终态，唯一的担保就是 (x∘y)∘z = x∘(y∘z)。所以不是”monoid 恰好结合”，而是”要批量推理就必须结合”，monoid 是这条需求的最小代数实现。

演绎二：同态律的逐点验证（补充，取最小的非平凡例子）。取 M = (ℕ, +, 0)（把”做了几步”当账），N = (Γ→Γ, ∘, id)（把”变换”当账），令 h(n) = fⁿ（f 自复合 n 次）。则 h(m+n) = f^(m+n) = f^m ∘ f^n = h(m)∘h(n)，且 h(0) = id：两条律逐点成立。“先走了 m+n 步”翻译过去就是”先做 f^m 再做 f^n”——翻译与复合可交换，这就是”账本对过程不敏感、只对总账敏感”的最小样本。本篇的 Thm 5 是同一件事的实装版：把”逐条压账”翻译成”∂Γ 上的变换”，同态律保证压账的分组方式不进结果。

3.2 第二件：扭积——“后做的先撤”是逼出来的，不是约定的

第二件工具回答一个具体问题：“做”和”撤”捆成一个对象之后，乘法怎么定义？答案其实藏在穿衣服的顺序里——你先穿袜子再穿鞋，脱的时候必须先脱鞋：撤销清单的顺序天然和操作顺序相反。到这里可以停下来猜一下：复合要保住“前向按执行顺序”，那第二个分量（逆）该怎么排？动手把乘法写出来，再往下看。论文的答案（定义 1，p.9）——扭积，把这条常识写进乘法：前向正序、逆反序，即 (f₁,g₁)∘(f₂,g₂) ≔ (f₁∘f₂, g₂∘g₁)。你写的和它一致吗？

结合律逐分量成立（两个分量各自结合，只是第二个分量”看起来反着”，反着结合还是结合）。它使对偶对成 monoid——数学上是”monoid 与其反 monoid 的直积”。边界要记：扭积里单位是 (id, id)，但单边逆不等于双边逆——g 撤得动 f（g∘f=id）不代表 f 撤得动 g；论文通篇只用单边（p.9 明示）。记住它：§五机制一开场的累积器，每一步记账都踩在这条乘法上。

核心演绎：反序不是约定，是被 witness 的应用点语义逼出来的（补充）。设效应按 e₁、e₂ 的次序施加，状态走 γ → δ₁ = f₁(γ) → δ₂ = f₂(δ₁)；要一个总逆 g 使 g(δ₂) = γ。手头的原料只有两条 witness：g₁(δ₁) = γ（e₁ 的应用点是 δ₁）、g₂(δ₂) = δ₁（e₂ 的应用点是 δ₂）。逐个试：若让 g₁ 先执行（正序思路），g₁ 遇到的是 δ₂——而它的 witness 只在 δ₁ 成立，担保为零；若让 g₂ 先执行，g₂ 遇到的恰是自己的应用点 δ₂，撤到 δ₁，紧接着 g₁ 遇到自己的应用点 δ₁，撤到 γ ✓。结论：每个逆恰好遇到自己应用时产生的状态——这条要求唯一的解就是”后做的先撤”。写进复合记号（右边的先执行）：总逆 = g₁∘g₂，书写顺序与应用顺序一致、执行顺序相反；新逆永远从右侧进入累积器——这正是 track 里 φ∘g 那个”∘g”的来历，也是扭积第二分量 g₂∘g₁ 的来历。

结合律的逐分量验证（两行，补充）：左结合 ((f₁,g₁)∘(f₂,g₂))∘(f₃,g₃) = (f₁∘f₂∘f₃, g₃∘g₂∘g₁)；右结合 (f₁,g₁)∘((f₂,g₂)∘(f₃,g₃)) = (f₁∘f₂∘f₃, g₃∘g₂∘g₁)。逐点相等——反序的复合”看起来反”，但复合本身仍按同一规则结合，所以不破坏 monoid 资格。

3.3 第三件：置换手算——检验“交换”最便宜的办法

第三件是件手艺而非理论：要验证”两个操作交换”，最便宜的办法是把状态空间缩小到几个点、把操作写成置换（重排标签的双射），手算两种顺序。两个置换交换 = 先做 A 再做 B 和先 B 再 A 给出同一个重排；写成定义：Γ 上双射 f 的复合构成对称群 Sₙ；f∘g = g∘f 即交换。这套手艺在 §6.3 要正经用一回：Γ={0,1,2} 上取 c: +1 循环与 s: swap(0,1)，两步即得反例。为什么本篇需要它：独立性（定义 42）就是”两个变换 monoid 的元素两两交换”——多组件交错时全部保证的基石——而数值法是检验交换直觉的最小工具。

练手（补充，为 §6.3 热身）：把 c、s 写成映射表，先自己算 c∘s 和 s∘c 各自作用在 0 上的结果——算完再看下表对拍。

c: 0→1, 1→2, 2→0        s: 0↔1, 2→2
c∘s 作用在 0（右先执行，s 先走）: s(0)=1，再 c(1)=2 → 终态 2
s∘c 作用在 0（c 先走）: c(0)=1，再 s(1)=0 → 终态 0
2 ≠ 0 ⇒ c∘s ≠ s∘c —— 两个单效应都可以各自完美撤销，
但互相不交换；§6.3 会看到：这个不交换在"出序撤销"时变成真实的破坏。

手艺要领两条：一是状态集越小越好（3 个点足够暴露一切非交换），二是每个操作必须写出完整的映射表（“+1 循环”“对换”这类口头描述在复合时最容易想错方向）。

3.4 第四件：观测等价——“恢复到位”承诺到哪，接口说了算

第四件工具回答”恢复”这个词到底承诺到哪。直觉是餐馆：两个东西”等不等”不看出入库房怎么摆，看顾客能不能点出差别——把所有可能的点单都试一遍，单子完全一样就算等价。点什么单的权利由接口给：接口不发某道菜，顾客就点不到，两个在这道菜上不同的状态就成了等价。写成定义（定义 31，p.23）：操作集 𝒜 上的测试 = 有限长的操作字母（前向或逆）序列，逐字应用于值，outcome 沿途收集；v ≈𝒜 v′ ⟺ 每条测试在两边同时有定义且 outcome 相同。≃ₖ ≔ ≈{𝒜ₖ}，且是”所有操作都尊重的等价中最粗的”（Lemma 32，证明是标准的前缀归纳）。为什么需要它：物理状态回不去（堆布局、生成性名字），一切恢复断言只能读到”接口看不出的差别被抹平”为止（§3.3.2，p.23）——机制篇里”恢复到位”、数学展开里的恢复精确性，量的都是这把尺子。这是程序等价的标准路线（转引论文 [41][42]，Plotkin 式上下文等价的近亲，我未核对原始文献）。

演绎一：≈_𝒜 是等价关系（补充，三行）。自反：同一条测试在 v 与 v 自己身上 outcome 当然相同。对称：等价条件对两边对称。传递：若 v≈v′ 且 v′≈v″，任何测试 τ 在 v 与 v″ 上的定义性与 outcome 都经由 v′ 中转——定义性逐测试传递，outcome 相等链式传递。所以 ≈_𝒜 良定义，才能充当定理里的”等号”。

演绎二：接口宽度决定等价粗细（补充，最小样本）。状态集 {0,1}，两个接口：(a) 𝒜 = ∅（什么都不让测）：测试只剩空序列，任何两状态都 ≈——等价最粗；(b) 𝒜 = {a}，a 为 0↔︎1 对换：测试 [a] 在 0 与 1 上的 outcome 分别是 1 与 0，不同 ⇒ 0 与 1 可分辨——等价变细。同一个”物理世界”，接口发不发 a，直接决定”恢复到位”承诺几个状态。这正是 §5.5 那句”接口发布哪些结果决定 ≃ 有多粗”（p.29–30）的玩具版：分配器不把句柄值当 outcome 发布，句柄重命名后的两个堆就不可区分。

3.5 第五件：良基与合流——守卫为什么必然释放，历史为什么可以无痕

最后两件武器一并备下，因为它们后面要在同一批定理里并肩出场。第一件是良基：直觉就是”没有无限下降链”（naturals 上 < 良基，整数上 < 不是——可以一直往下）；良基序的价值在于保证归纳法和递归有解——只要每一步都在往下走，过程就必然停。第二件是合流：直觉是”怎么走殊途同归”——从一个状态出发按不同顺序做重写，终点（正规形）相同。落到本篇的定义：≺ 先决序（定义 72，p.49）无环即可良基化；合流在论文里以”唯一正规形”陈述（Thm 80(2)：任意两条取同样编排步的序列，终点经改名后 ≃）。为什么本篇需要：守卫（relied）是典型的”看起来会死锁”的前提，无死锁证明 = 沿 ≺ 构造下降链（Thm 73）——良基在那里兜底；合流 = 演算的招牌定理（Thm 80）——动态历史能不能无痕，全看它。这两件武器都来自重写理论的标准库（转引论文 [46] trace theory、[47] change propagation）。

演绎一：为什么”没有无限下降链”就能归纳（最小反例论证，补充）。要证命题 P 对所有元素成立，反设不然：取”使 P 失败”的元素里 ≺-最小的一个 x（良基保证取得到——若取不到最小元，就能从任一失败元一路往下挑，挑出无限下降链，矛盾）。x 的所有 ≺-前驱都满足 P，而 P 的归纳步恰好是”前驱成立 ⇒ 本元成立”，于是 x 满足 P——与”x 失败”矛盾。Thm 73 的无死锁证明就是这条论证的实装：沿”谁的提交视图指向我”一步步上溯（≺ 严格增大），良基 + 名字有限逼出”上溯必停”。

演绎二：合流的菱形（补充，玩具图）。合流的标准形状是菱形——从同一状态出发的两条不同次序的路径在中点汇合：

          γ
         / \
     a 后 b   b 后 a        （同样的两步，先后不同）
         \ /
          γ*                 （终点相同——菱形闭合）

本篇的版本有两处加强：终点不要求相等、只要求 ≃（接口测不出即可，§3.4 的让步在这里回收）；而且”步”不是单操作、是整个 episode（一进一出的完整生命周期）。Lemma 78 就是”菱形左半边”的证明（两个激活步可对换），Lemma 79 是”删掉一段历史不改变终点”，Thm 80 把两者叠起来：任意调度都能洗成规范形。

四、Γ、φ、fiber、ω：全篇记号一张表

五、八个机制：从可逆效应到组件演算

承上启下：§一 的麻烦是插件系统的”卸载即重启”——时间不可组合（状态丢光）与空间不可组合（依赖各显神通），§二 的路线是把效应/余效应从编译期仪器物化为运行时可操作的机制：效应自带逆、依赖反应式解析、统一上下文。上节备好的五件数学工具就是这套机制的骨架：monoid 与同态（§3.1）解释累积器为何能记账，扭积（§3.2）解释逆为何在应用点交付，置换与观测等价（§3.3–3.4）支撑”静息态 = 静态装配”的合流性，偏序与良基（§3.5）给恢复的终止性背书。本节八个机制小节逐个落到 track/recover 与组件演算上。

5.0 贯穿示例的数据结构——三个插件的家当

贯穿示例的三个组件（形式按论文 Table 2 与算法 1/4 的模型，TypeScript 风格示意；apply 是生成器，每步 yield 一个逆——对应效应迭代器 ℑΓ）：

adapter_discord = {
  provide: ['platform'],
  inject: [],
  apply: function* (ctx) {
    const conn = connectDiscord(token)     // 副作用：开连接
    yield () => conn.close()               // 第 1 步的逆
    const gate = ctx.store.register(conn)  // 副作用：把连接登记进表
    yield () => ctx.store.unregister(gate) // 第 2 步的逆
  }
}
database_mysql = { provide: ['storage'], inject: [], apply: ...（同构） }
checkin = {
  provide: [],
  inject: ['platform', 'storage'],        // d：声明依赖
  apply: function* (ctx) {
    yield () => ctx.platform.on('checkin', handler)
    yield () => ctx.storage.ready(pushDaily)
  }
}

运行时为每个实例（fiber）维护：父指针 π、自己的绑定表 σ、退役标志 τ、生命周期 θ（Inactive / Reloading(i,g,ω) / Active(g,ω) / Unloading(g,ω)，定义 49，p.31–32），其中 g 是累积器、ω 是提交视图。下面八个机制都长在这个数据结构上。

5.1 机制一：可逆效应——逆在制造时入账，卸载就是念账本（§3.1.1，p.9–12）

【类比 · 购物小票】 退换货不靠你记住买过什么，靠收银台顺手打的购物小票：小票按时间摞好，退货从最近一张退起。累积器就是这本小票——效应发生的那一刻，它的逆就被自动记下。 【跨域锚点】 数据库事务的 undo log：每条修改附带反向操作，回滚就是按逆序重放。（类比与通识锚点，非论文内容）

先看病。插件卸载时，它开过的连接、注册过的事件、改过的状态谁来收尾？现行做法是清理回调——作者”记得”写清理、写对了没人担保，忘一步就是永久残留（§一里 VSCode 的 deactivate 钩子就是这种形态）。病根出在：产生效应的代码和清理效应的代码拆在两处，效应发生的那一刻，系统并不知道”该怎么撤它”。

药方从最一般的设定起步。原文表述：任何杂质函数 f : X ⇝ Y 都可以纯化成 f : Γ × X → Γ × Y，其副作用独立于返回值、表现为上下文变换 Γ → Γ；这些变换在复合 ∘ 下成 monoid（封闭/结合/单位三律各有效应解读，p.9）。要可撤销，就给每个变换 f 配一个左逆 g（论文通称”逆”，明确只是单边的：只承诺 g∘f = id，从不承诺 f∘g，p.9）。

“做”和”撤”怎么捆在一起复合？对偶对 (f, g) 的乘法是扭积（定义 1，式 4，p.9）：

(f_1, g_1) \circ (f_2, g_2) \coloneqq (f_1 \circ f_2,\ g_2 \circ g_1)

逐符号：前向按执行顺序复合，逆反着复合——后做的东西先撤。它使 (Γ→Γ)×(Γ→Γ) 成 monoid（单位 (id, id)），即”变换 monoid 与其反 monoid 的积”，记 𝔗Γ。然后把账本做进上下文本身（定义 2，式 5，p.9）：

\partial\Gamma \coloneqq \Gamma \times (\Gamma\to\Gamma)

∂Γ 就是一个二元组 (γ, φ)——γ 是当前状态，φ 是累积器，“迄今所有效应之逆按反序的复合”，一调用就把上下文送回组件装载前的样子。初始为 (γ₀, id)。track 把一对 (f, g) 提升到 ∂Γ 上（定义 3，式 6，p.10）：

\mathrm{track}_\Gamma(f,g) \;=\; (\gamma, \varphi) \mapsto (f(\gamma),\ \varphi \circ g)

这套记账为什么可靠？p.10 的两个定理给出白话版：Theorem 4 说 track 不碰前向行为（第一投影上就是 f）；Theorem 5 说 track 是 monoid 同态——一步步记账和一把头记账结果相同，所以任意长的效应序列可以当成一个效应推理。卸载那一刻的收尾只有一行，recover（定义 6，式 9，p.11）：(γ, φ) ↦ (φ(γ), id)。Theorem 7（式 10，p.11）补上最后一块基石：只要 g 撤得动 f（g(f(γ))=γ），任何 track 步骤都保持 φ(γ) 不动——这个量叫可靠性不变量 φ(γ)=γ₀，是全部恢复保证的载体。

全篇就看这张：图 22——∂Γ 的 track/recover 与 LIFO 累积器，后面七个机制全部站在这台机器上。

数值例：Γ = {0,1,2,3}，f₁: γ ↦ γ+1 (mod 4)（g₁: −1），f₂: γ ↦ γ+2 (mod 4)（对合，g₂ = f₂）。从 (1, id) 出发：track(f₁,g₁) 得 (2, g₁)；track(f₂,g₂) 得 (0, g₁∘g₂)。recover：(g₁(g₂(0)), id) = (g₁(2), id) = (1, id)——精确回到起点，而裸上下文走到 0 之后 f₁ 做了什么已经无处可查（图 22 上排）。

意义：撤销从”作者的记忆义务”变成了”效应的结构属性”——逆在应用点随手交付、账本随效应生长；§五后面七个机制，全部长在这台机器上。

流程（补充，自绘；状态对 (γ, φ) 随每步走一遍，数值例同上）：

装载期：每个效应一步，逆从右侧压进累积器（φ∘g，后进先出）

 (γ, φ)              动作                (γ, φ)'
 (1, id)   ── track(f₁,g₁) ──▶   (2, g₁)         逆 g₁ 入账
 (2, g₁)   ── track(f₂,g₂) ──▶   (0, g₁∘g₂)      逆 g₂ 压到最右（最先执行）
                                  ▲ 账本 φ 只增不减，γ 随便走

卸载期：一行，recover 应用整个累积器，然后清账

 (0, g₁∘g₂) ── recover ──▶ (g₁(g₂(0)), id) = (1, id)   ✓ 回到起点

读图要点：γ 列走到哪里都无法回退（裸上下文是有去无回的），真正的”回家路”全部寄存在 φ 里；φ 的复合方向保证最后进的逆最先执行——这就是”购物小票从最近一张退起”的数学形态。Thm 7 说的”每步之后 recover 的结果不动”，在图上就是：任何一行直接执行 recover，落点都是 (1, id)。

GIF 循环播放，点击可放大。

5.2 机制二：效应函数与效应迭代器——逆不承诺全局，只承诺应用点（§3.1.2–3.1.3，p.12–16）

【类比 · 万能钥匙换房卡】 要求一把钥匙开得了酒店所有房间的门（uniform 逆），钥匙就得越造越复杂、还未必造得出来；改成房卡——住哪间发哪张、住多久管多久——每张卡的义务立刻变小，兑现反而有保证。per-state 逆就是房卡。 【跨域锚点】 租车还车：把你借车期间用掉的油加回去就算交割清楚，没人要求你把里程表倒回去——义务按”这一次使用”算，不按”全世界复原”算。（类比与通识锚点，非论文内容）

先看病。上一节的 track/recover 已经能把”卸载”变成”应用账本”，但这个模型有两个先天缺陷（p.12 原文列出）：一是 g 在应用前就固定，一个 uniform g 必须在所有状态都撤得动，而撤销其实只需要”在应用它的那个状态”撤得动——malloc/free 就是反例：free 撤销的是这一次分配，不是”所有 malloc”；二是 recover 全有或全无，不能选择性撤销一个效应留下别的。

病根出在类型签名上：变换 Γ→Γ 只返回新状态，逆没有被一并交付，于是只能事后去配一个处处成立的 g。这里再停一下：要让逆在应用点交付，你会改哪一头——输入的类型、输出的类型，还是两个都得动？想好了再往下看。修法是输入输出两端各补一个逆（p.12）：输入端从 Γ→Γ 升为 Γ → Γ×(Γ→Γ)（变换加逆一起返回），输出端从 ∂Γ→∂Γ 升为 ∂Γ → ∂²Γ（∂²Γ = ∂(∂Γ)，递归塔）。于是有核心类型（定义 8，式 12，p.12）：

\mathcal{E}_\Gamma \coloneqq \Gamma \to \Gamma \times (\Gamma\to\Gamma), \qquad \mathcal{E}_\Gamma^* \coloneqq (e : \mathcal{E}_\Gamma) \times \big((\gamma,\delta,g).\ ((\delta,g)=e(\gamma)) \to g(\delta)=\gamma\big)

逐符号：e 应用在 γ 上产出 (δ, g)——新状态 δ 加这次的逆 g；见证（witness）要求 g(δ)=γ 只在应用点成立。这是全文最重要的一个”定义即纪律”的设计：逆不需要全局成立，只需要”在哪应用的就在哪撤干净”，per-state 逆由此合法。效应复合 ⋄（定义 9，式 13）在 𝔈Γ 上造出 monoid，且 witness 在 ⋄ 下封闭（Theorem 11，p.13）：两个见证过的效应复合起来还是见证过的——s(δ)=γ、t(ε)=δ 蕴含 (s∘t)(ε)=γ，链式撤销自动成立。提升算子 effect 把 𝔈Γ 映到 𝔈∂Γ（定义 12，p.13）：撤销本身也是一个效应，撤销的撤销就是再做一遍原效应——论文用这个自相似把所有层级统一进同一种类型（p.13–15，Theorem 13–15）。其中 Theorem 15 值得记：提升后的逆精确恢复状态（永远），但累积器也复原 iff g∘f = idΓ——per-state 逆足以恢复上下文状态，不足以让撤销这步本身像没发生过。

组件装载不是单个效应而是一整个序列，所以药方的后半截是把序列本身也物化为效应迭代器（定义 17，式 17，p.15）：

\mathcal{I}_\Gamma \coloneqq \mu\mathcal{I}.\ \Gamma \to \Gamma \times (\Gamma\to\Gamma) \times \mathsf{Maybe}(\mathcal{I})

这就是 generator——每次 next() 产出（新状态，逆，续体），续体是 Nothing（完事）或 Just(下一个迭代)。论文明说：效应迭代器是”物化的 delimited continuation”，主流语言通过 yield 暴露这个结构，所以模型直接映射到现成的 generator（p.16）。装载 = 跑一遍迭代器、逆逐个压进 φ；卸载 = 应用 φ，LIFO 撤销（Theorem 16，p.15–16：逆序撤销时每个逆恰好拿到自己应用时产生的那个状态）。

意义：逆的交付从”全局承诺”降到”应用点承诺”——义务变小了，保证反而变硬了；组件的装载与卸载从此有了一个能直接落进现有语言的原语。

流程（补充，自绘；effect iterator 的驱动循环，对应实现里 generator 的 next()）：

                    ┌─────────────────────────────────┐
                    │        L-Iter：跑一次迭代          │
                    ▼                                 │
     e(γ) ──▶ (δ, g, o)                              │
               │      │      │                       │
               │      │      └─ o = Just(i) ─────────┘  还有续体，继续迭代
               │      └─ o = Nothing：装载完成
               │            fiber 落 Active(g总, ω)
               │
               └─ 逆 g 逐个压进累积器（右侧进入）
                     装载完成后 g总 = g₁∘g₂∘…∘gₖ

停用（全演算唯一的应用点 L-Unload）：
     Active(g总, ω) ── L-Unload ──▶ 应用 g总（LIFO 一轮）──▶ Inactive

对应到 5.0 贯穿示例：adapter_discord 的 apply 是 generator，两个 yield 就是两次 L-Iter；第一个 yield 交出 conn.close、第二个交出 unregister，装载完 g总 = conn.close ∘ unregister（书写序），执行时 unregister 先走——登记先进后出，正好和 setup 顺序镜像。

5.3 机制三：反应式余效应——漏报被代数堵死，反应因此免费（§3.2.1–3.2.2，p.16–19）

【类比 · 拔插头】 插线板上一排电器，谁插在哪个插座上一目了然：拔掉某个插头，插在它上面的电器自然停机，插回去自然复活——没有任何电器需要”感知”插座的存在，全靠物理连接自己说话。依赖声明就是这排插座。 【跨域锚点】 电子表格：改一个单元格，引用它的公式自动重算——重算的触发是结构给的，不是每个公式自己轮询出来的。（类比与通识锚点，非论文内容）

先看病。时间可组合有了着落，空间可组合还悬着：一个模块怎么知道”我依赖的东西没了/换了”？§一里批评过的现状是各显神通——轮询、回调、约定俗成的事件，谁都可能漏报。病根出在依赖没有被当成一等公民：它只是代码里隐式的调用关系，系统对它无从下手。

药方是把依赖显式做成一张类型化的表——把 IoC 容器（key-value 依赖注入）形式化为余效应上下文（定义 19，式 20，p.17）：

\Sigma \coloneqq (k:K) \rightharpoonup \mathcal{V}_k

逐符号：K 是依赖键的集合，𝒱 是类型族（键 k 只能绑 𝒱ₖ 类型的值——静态类型安全），Σ 是有限偏函数表。两个原语：get(k) 要求 k 已在表中；set(k, v) 要求 k 不在表中，产出新表加逆（撤 = 从表中删掉 k）。本机制的枢纽是这句话（p.17）：set 的类型恰好是 𝔈*Σ——余效应操作本身就是效应函数，于是 3.1 的全部机器（跟踪、回滚、复合）原封不动地接管依赖的注册与注销。“coeffect 操作是效应，而效应是可逆的”，这是全文最优雅的一步。

反应性来自一个可判定的满足谓词（式 22，p.18）：σ ⊨ d ⟺ d 里每个键都在 dom(σ) 里。组件声明规格 d ⊆ K（定义 21）；每次上下文变更按规格分类（定义 22，式 24，p.18）：

\mathrm{notify}_d(\sigma, \sigma') \coloneqq \begin{cases} \text{activating} & \sigma \nvDash d \wedge \sigma' \vDash d \\ \text{deactivating} & \sigma \vDash d \wedge \sigma' \nvDash d \\ \text{neutral} & \text{otherwise} \end{cases}

激活触发效应执行（按 3.1 跟踪），停用触发累积器回滚。为什么反应性是免费的（p.18）：所有对 σ 的变更都走效应函数（逆会恢复 domain），所以满足性的每次变化都在效应边界可观测—— algebra 保证没有漏报。拆一个部件给你看：把“所有变更都必须走效应函数”这条纪律拿掉，允许某处绕开它原地改表——满足性的变化就发生在这条野路径上，效应边界什么都看不到，activating/deactivating 全部哑火，读悬空绑定的组件无人通知。“免费”的成本，预付的正是这条纪律。贯穿示例里：database_mysql 激活 → storage 出现 → checkin 的规格从 ⊭ 变 ⊨（activating，自动激活）；卸掉 database → storage 消失 → deactivating，checkin 自动停用，不会读到悬空绑定。

意义：依赖协调从”每个模块自带的求生技能”变成”表上的一次分类”——组件作者只写声明，激活与停用由结构推动，漏报被代数堵死。

流程（补充，自绘；每次表变更 σ→σ′ 后，按组件声明 d 走这棵判定树）：

        σ ⊨ d ？（变更前依赖满足吗）
        ├─ 否 ──▶ σ′ ⊨ d ？
        │         ├─ 是 ──▶ activating   ──▶ 激活：跑效应迭代器，逆入账
        │         └─ 否 ──▶ neutral      （一直缺着，不动）
        └─ 是 ──▶ σ′ ⊨ d ？
                  ├─ 否 ──▶ deactivating ──▶ 停用：应用累积器回滚
                  └─ 是 ──▶ neutral      （键在但值可能变了 → 不重装，
                                          见 §6.7"原地覆写不触发"的坑）

贯穿示例走一遍：卸掉 database_mysql ⇒ storage 从 dom(σ) 消失 ⇒ checkin 判定 deactivating ⇒ 自动回滚，全程无人写一行”监听代码”。反方向：database 重新激活 ⇒ storage 回到表上 ⇒ activating ⇒ checkin 复活。两跳都只是判定树上的两次谓词求值——“反应式”三个字的实现成本低得惊人，成本全部预付在了”每个变更都必须走效应函数”这条纪律上。

5.4 机制四：隔离与拦截——调整走派生实现，恢复就是丢弃（§3.2.3，p.19–21）

【类比 · 同店分厨】 同一间厨房（键），对不同桌（realm）出不同的菜——点菜先报桌号再报菜名，解析走两跳；出餐口还可以统一加一道工序（metadata 拦截），不必改任何一道菜的配方。 【跨域锚点】 软件测试里给被测对象垫一个假数据库：业务代码一行不改，替换发生在”依赖出口”处，而不是业务本身。（类比与通识锚点，非论文内容）

先看病。依赖表成了运行时的一等公民，新需求立刻冒出来：同一个键，不同组件要解析出不同的值（多租户、测试、沙箱）；访问依赖时还要附加横切行为（策略、日志）。惯例做法是改代码——每个用到处各改一遍。病根：解析和访问被焊死在”一张全局表、一次直读”上，没有任何可调的中间层。

药方是两个扩展。隔离（定义 24–25，p.19–20）：加一层 realm 表 ρ : K ⇀ R，解析变两跳 k → ρ(k) → σ(ρ(k))；isolate(k, r) 把 k 的 realm 改到 r。拦截（定义 26–27，p.20–21）：每个键带一个 metadata monoid (ℳₖ, ⊕ₖ, εₖ)，提供者存的是”从 metadata 到值”的函数 σ(k): ℳₖ → 𝒱ₖ，读取时把组件声明的 metadata 与上下文携带的 metadata 合并后喂进去；合并是右偏的——外围上下文的 ι(k) 优先，可以覆盖组件自己的声明。论文给的用例（p.21 + §6.3 p.72–73）：编排器给社区组件的数据库依赖注入”只读”元数据，不用改任何一方代码。

这两个操作的实现选择单独成定义（定义 23，p.19）：效应有两种实现方式（realization）——原地（in-place，改共享表、逆非平凡）与派生（derived，不动原表、派生一个新上下文、逆是恒等、恢复 = 丢弃派生上下文）。隔离和拦截被直接规定为派生实现：不写共享表就没有效应可跟踪，恢复时连调整一起丢弃。纯函数环境里两者重合，命令式宿主可逐操作选择（p.19；§5.1.2 实现了两种）。

意义：多租户与横切需求从”改每一处用点”变成”改一张解析表、配一份元数据”——而且两种调整都是派生实现，恢复时整个丢弃，不进账本。

流程（补充，自绘；隔离把一次解析拆成两跳，拦截在出口处垫一道工序）：

隔离（两跳解析）                    拦截（出口工序）
组件要读键 k                        组件要读键 k
     │                                  │
     ▼                                  ▼
ρ: k ↦ r（先查桌号）                ι(k) ⊕ 组件声明的 metadata
     │                              （上下文的优先，右偏合并）
     ▼                                  │
σ: r ↦ 值（再查本桌的菜）                 ▼
     │                              σ(k) 合成后的 metadata ↦ 值
     ▼                                  │
恢复 = 丢弃派生上下文 ◀────────────────┘
（两者都是派生实现：不动共享表 ⇒ 无效应可跟踪 ⇒ 逆 = id，账本干净）

对照记忆：原地实现（in-place）改共享表、逆非平凡、要进账本；派生实现（derived）复制一份上下文在上面改、恢复就是”扔掉复印件”。隔离与拦截被直接规定为派生——调整是”视图”不是”事实”，撤销视图当然不需要记账。

5.5 机制五：统一上下文与观测等价——恢复的口径由接口定（§3.3，p.21–26）

【类比 · 黑箱验收】 验收一台机器，不看内部零件怎么摆，只按说明书上的按钮挨个按、比对输出——说明书没暴露的差别，验收上一律不算差别。观测等价就是这台验收规程。 【跨域锚点】 图灵测试的思路同款：问不出可分辨的回答，就当作不可分辨。（类比与通识锚点，非论文内容）

先看病。到这里效应有一套机器、依赖有一张表，可两者还是两本账；更要命的是”恢复”这个词还欠着一层诚实：说”恢复到位”，到底承诺到哪？病根：共享状态散落在系统各处，而物理状态本来就不可能原样复原。

药方分两步。第一步，把两本账合成一本。统一上下文（定义 28，式 29，p.21）：

\Gamma_\infty \coloneqq \mu\Gamma.\ \Gamma \times (\Gamma\to\Gamma) \times \Sigma

效应上下文（状态+累积器）与余效应上下文（依赖表）合体成一个递归类型——每一层都长这样，父层聚合子层的效应，所以层级组合天然支持（“加载 = 插入，卸载 = 拔出而不影响其他在跑的组件”，p.22–23）。𝒱 类型族不受限意味着任何要跨组件共享的状态都可以编码成一个依赖——Σ 吞下全部共享可变状态，组件与环境的每次交互都过这一个实体（p.21）。这就是”上下文范式”：一条纪律，不是一堆 API。

第二步，把承诺校准到可实现的高度——然后是诚实的一步（§3.3.2，p.23）：Theorem 7 断言的是状态相等，但物理状态不可能原样恢复——free 不会复原 malloc 之前的堆布局，生成性名字（generative name）用掉就是用掉了（p.23，引 [40]）。

所以第 3 节所有等式改读为观测等价 ≃：两个值不可区分，当且仅当”该键操作集生成的每条有限测试（有限长的前向/逆序列，读沿途 outcome）在两边要么都无定义、要么结果相同”（定义 31，p.23）；≃ₖ 是使所有操作都尊重的最粗等价（Lemma 32）；上下文级的 ≃_S 按 key 组装（定义 33，式 34，p.24），S 之外的键被遗忘。

这个选择给出一个工程自由度（p.29–30）：接口发布哪些结果决定 ≃ 有多粗——分配器不把句柄值暴露为可比较的 outcome，句柄重命名后的两个堆就不可区分、分配就可交换（论文点名为 CompCert 内存模型的同款手法，转引 [44]）；POSIX 的 open 强制返回最小可用描述符，仅此一条就让两次描述符分配不可交换（转引 [45]，Scalable Commutativity Rule 的同款读法）。判定一个 key 可不可交换，从”内在属性”变成了”接口设计选择”。

意义：恢复的语义从”物理复原”落到”接口不可区分”——这是全篇最诚实也最实用的一次让步，后面所有定理的等号都按这个口径读。

流程（补充，自绘；Γ∞ 的自相似分层——“父层的三个槽位，每个都装着一个同构的小 Γ∞”）：

Γ∞ = (γ, φ, Σ)                    ← 每一层都长这样
       │
       ├─ γ  ──▶ 又是一个 Γ∞ = (γ, φ, Σ)   ← 递归塔
       │            └─ ……
       ├─ φ  ──▶ 本层效应的累积器（子层效应汇拢于此）
       └─ Σ  ──▶ 本层可见的依赖表

装载 = 在父层 Σ 注册 + 子层开跑（插入一个新 Γ∞）
卸载 = 应用该子层自己的 φ，然后整体拔出——兄弟层毫发无损

这就是”层级组合天然支持”（p.22–23）的形状根据：每个组件实例是一层，层的进出只碰自己的三个槽位；父层通过 φ 收拢子层的全部效应（子效应的逆是父层的效应——∂²Γ 的递归在结构上自动成立，对应 §5 实现里 dispose 插进父上下文的那一行）。

5.6 机制六：独立性——家当分得清，回滚就不挑次序（§3.4，p.26–30）

【类比 · 合租室友】 各住各屋、各用各桌的室友，谁先谁后打扫互不影响；共用一口锅的就算”纠缠”——得排依赖序。独立性证明的正是前者：只要家当分得清，回滚就不必讲究次序。 【跨域锚点】 停车场里互不遮挡的独立车位：任何顺序停取都行，共用车道的才需要排队协调。（类比与通识锚点，非论文内容）

先看病。单组件的保证（一个累积器、LIFO）到多组件就不够：卸载一个组件时，它的逆要在一个被别人的效应移动过的状态上运行——别人的操作会不会弄脏我的退房？条件是什么？

药方是把”互不干扰”写成可检验的数学条件。独立性（定义 42，式 39–40，p.27）：两个迭代器独立，当 (1) 一方的一切变换（前向+逆）与另一方的一切变换交换；(2) 一方的变换不扰动另一方 yield 出的逆与续体。两个支撑引理：交换性在生成元上判定即可（Lemma 41）；然后两级归约——不同键的操作天然独立（Theorem 45，p.29：各读各写一个键，键局部映射必交换）；同键的交换性被做成 coeffect 的第三个成分——见证（定义 46，p.29）：提供该键的组件在定义处附上”我的操作两两交换”的证明，消费者不承担任何义务。与效应的 witness 完全平行：“每个逆都撤得动”与”每个操作都交换”都是定义处一次性供给、使用处免检的条件。

结论（Theorem 43，p.28）：独立效应族按任意顺序应用后，按任意排列撤销全部逆，都回到起点——不只 LIFO。再经 Theorem 47（p.30）：只要两组件的 provide 与对方的 (inject∪provide) 不相交、共享操作键都交换，两组件的上下文中介迭代器独立——交换性由 witness 供给后，唯一要查的只剩”声明不相交”，而这从组件声明直接读出。论文对分解的总结（p.30）值得整段记：可组合性把一个计算切成”可交换部分”与”次序敏感部分”——前者交给效应（随便什么顺序执行、随便什么顺序撤），后者交给余效应（组件内的累积器强加 LIFO；跨组件的声明式依赖强加”先提供后消费”）。可交换性于是以组件为粒度成立，这正是第 4 章工作的尺度。

意义：交错世界的检查项从”任意交错的全部可能”缩到”读一遍组件声明”——把全局正确性压成局部义务，正是这一步使多组件系统还可推理。

流程（补充，自绘；判定两组件能否任意交错，工程上只剩两问）：

两组件 i、j 想交错执行，按序回答：
  ① 声明不相交吗？   Pᵢ∩Sⱼ = ∅ 且 Pⱼ∩Sᵢ = ∅
     （读组件声明的 provide/inject —— O-Insert 前提已强制 provision 不相交）
        │ 否 ──▶ 有纠缠：走守卫 + 依赖序（§5.7 / Lemma 67），不许任意交错
        ▼ 是
  ② 共享键的操作交换吗？
     （共享键的 coeffect 第三成分自带 witness：提供者在定义处一次性供给）
        │ 否 ──▶ 键的 witness 缺席：键不可交换（接口设计的责任，§5.5）
        ▼ 是
  ①② 成立 ⇒ Thm 47：两组件独立 ⇒ Thm 43：装载任意序、卸载任意排列，都回得去

注意①的巧妙处：它根本不需要跑系统——组件声明是静态文本，“读一遍”就是全部成本。②则在提供者写组件的那天一次性结清。运行时真正要动态判定的，一个都没有。

5.7 机制七：组件演算——消费者先走完，提供者才回滚（§4.1–4.2，p.31–38）

【类比 · 退房查房】 客人退房要先走完自己的收尾（teardown），房间才能翻新（提供者回滚）；查房没完成，家具一件不许动。守卫就是那个查房环节：还有人的行李寄存在这间房，就不许翻新。 【跨域锚点】 危楼定向爆破：先疏散全部住户，再动承重结构——次序错了会出人命，所以次序被写进规程而不是靠现场发挥。（类比与通识锚点，非论文内容）

先看病。前六个机制备齐了零件——效应有逆、依赖有表、上下文统一——但零件不等于装配图：组件什么时候算激活、提供者撤离时消费者怎么走、卸载会不会卡死在半路，全都没有说法。病根：生命周期是隐式的，散落在各实现的自定义回调里。

药方是一台显式的状态机加一套写死前提与动作的规则。组件 = (d, p, e)（定义 48，p.31）；fiber（定义 49，p.31–32）= ⟨d, p, e, π, σ, τ, θ⟩，生命周期 θ ∈ ΘΓ = Inactive | Reloading(i, g, ω) | Active(g, ω) | Unloading(g, ω)。

注册表（定义 50，p.32）以名字为索引、父指针成树；coeffect 上下文不是存储而是派生的（式 46，p.33）：σ_γ = 所有 Active fiber 的表之并——联合良定义靠 O-Insert 的前提”新 fiber 的 provision 与所有在册 provision 不相交”（单源纪律：一个键至多一个可能提供者）。提交视图 ω：每个声明键在激活那一刻解析到的提供者名字（不是值！）。目标视图 targetₙ(γ)（定义 53，式 48，p.35）： retired 或不满足时为 ⊥，否则把每个声明键映到当前提供者；fiber 的每个生命周期规则都在”ω 与 target 一致/背离”上触发。

9 条规则（Figure 1，p.34；规则全文 p.34–37）：

• 编排规则（外部请求）：O-Insert（名字新鲜、父在册、provision 全局不相交 → 落册为 Inactive）；O-Retire（唯一前提”在册”——打 τ=⊤，只是请求）；O-Remove（τ=⊤、Inactive、表空、无子 → 摘除）。
• 生命周期规则（系统自发）：激活三步 L-Begin（target≠⊥ 才许）→ L-Iter（跑一次迭代，逆压进 g）→ L-Finish（落 Active(g∘h, ω)）；停用三步 L-Leave（Active 且 target≠ω → 进 Unloading，只停供、不行动）；L-Divert（Reloading 中 target 变了 → 携已积累的逆改道 Unloading；可在任意两次迭代之间落入）；L-Unload（全演算唯一应用累积器的地方，前提是守卫 ¬reliedₙ：没有任何在册 fiber 的提交视图指向 n）。
• 实例化即效应（定义 52，p.35）：效应迭代器的一步可以实例化组件（插件装插件），原语 = “对该组件做 O-Insert(π=n)”，其逆 = O-Retire。逆为什么是 retire 不是 remove（p.35）：逆必须在任何状态都适用，O-Remove 带前提（无子、表空），做成逆就可能卡死；O-Retire 只有一个前提。父组件卸载时子组件被级联 retire——贯穿示例里卸掉 adapter_discord，它实例化的子 fiber 全部跟着走。

在读两阶段设计之前，可以先拆一次部件：把守卫 ¬relied 拿掉，L-Unload 来了直接应用累积器——你推一步，看会先坏在哪。此刻消费者 checkin 还在 Unloading 里跑自己的 teardown，而 teardown 往往还要读正被撤离的依赖（关连接池得把连接还给提供者）；提供者先回滚，teardown 读到的就是悬空绑定。守卫干的就是把“提供者回滚”压到“消费者走完”之后——这个等待必然结束的证明在 §6.5（Thm 73）。

两个设计的理由要单独记（p.36–37）：停用为什么拆成两步——组件因提供者撤离而被拆时，正在跑自己的 teardown 代码，而 teardown 往往还要读那个正在撤离的依赖（关连接池要把连接还给提供者）。一步到位的停用（先撤提供、再跑逆）会让 teardown 读到悬空绑定。所以 L-Leave 先把 fiber 移出 σ_γ（依赖立刻重算、改道），提供者的 L-Unload 被守卫 ¬reliedₙ 压住——消费者先走完，提供者才回滚。这个守卫平时会死锁，靠两点解活：Unloading 的表不在 σ_γ 里（没人再提交给它），以及 σ_γ 只对 Active 取并（§4.1 p.33）。Theorem 73 把它变成”守卫必然释放”。

限制效应函数可以碰什么（定义 55–56，p.38）：confinement——一个效应函数写，只许写自己的表和声明键上的值（值住在提供者的表里）；读，只许读同样的两处。控制字段（别人的生命周期状态）既不许读也不许写。配合”上下文范式固定效应函数的形状（操作步/提供步/实例化步的序列）“，confinement 是形状的推论（Lemma 57）——这使 Table 1（p.40，九条规则作为写入的完整清单）成为完备清单，后面的元理论全部靠它。

意义：装卸的正确性从”约定俗成的回调时序”变成”九条规则的状态机”——每条规则的前提与动作都被写死，无死锁与合流这些系统级性质（下一节）才有处下脚。

流程（补充，自绘；把贯穿示例从头到尾走一个完整 episode，每步标规则名与关键前提——9 条规则怎么协作，看这一张表）：

阶段一：装 adapter_discord（提供 platform）
 t0  O-Insert(adapter)   前提: 名字新鲜/父在册/provision 不交 → 落册 Inactive
 t1  L-Begin(adapter)    前提: target≠⊥ → Reloading(i, id, ω={platform→adapter})
 t2  L-Iter              开连接；逆 conn.close 压进 g
 t3  L-Iter              登记进表；逆 unregister 压进 g
 t4  L-Finish            → Active(g, ω)；platform 进入 σ_γ

阶段二：装 checkin（声明 platform+storage；database 已装好 storage）
 t5  O-Insert(checkin) → Inactive
 t6  L-Begin(checkin)    前提: σ⊨d（两个键都有 Active 提供者）→ ω 记下两个 uid
 t7  L-Iter…L-Finish     → Active；订阅生效

阶段三：卸 adapter（重头戏：两阶段停用 + 守卫放行）
 t8  O-Retire(adapter)   前提: 仅"在册" → τ=⊤（只是请求，状态未变）
 t9  L-Leave(adapter)    前提: Active 且 target≠ω（retire 使 target=⊥）
                          → Unloading；只把自己移出 σ_γ，不行动
                          ⇒ platform 离开 σ_γ ⇒ checkin 判 deactivating
 t10 L-Leave(checkin)    同理进 Unloading（自己走完 teardown）
 t11 L-Unload(checkin)   前提: ¬relied（没人提交视图指向 checkin）✓
                          → 应用累积器 → Inactive；其提交视图随之消失
 t12 L-Unload(adapter)   前提: ¬relied——t11 之后 checkin 不再指向 adapter ✓ 放行
                          → unregister、conn.close 按 LIFO 执行 → Inactive
 t13 O-Remove(adapter)   前提: τ=⊤/Inactive/表空/无子 → 摘除名字

盯住 t9–t12 四行：消费者 checkin 在 t11 走完自己的收尾（此刻它 teardown 里读的 storage——本例中是 platform——绑定仍在，因为提供者被守卫压住没动），提供者 adapter 在 t12 才回滚。守卫”平时死锁、此处解活”的机关（Unloading 不在 σ_γ、σ_γ 只对 Active 取并）保证 t12 的前提必然在有限步内变真——这正是 Thm 73 要证的事。

GIF 循环推进：两个 fiber 的状态徽章、共享表 σ 的键、守卫的锁与放行随拍实时变化。

5.8 机制八：五组元理论——装卸的正确性从此是定理（§4.3，p.39–55；§5，p.57–69）

【类比 · 竣工验收】 机制讲完只算主体封顶，交付前还要逐项验收：结构不走形、退货不多不少、工序不乱、工期有底、殊途同归；实现映射则是施工图到工地的对照表。 【跨域锚点】 桥梁通车的荷载试验：设计书上的每条承诺都要当场复验，合格才许放行。（类比与通识锚点，非论文内容）

先看病。零件和装配图都有了，但”机制写对了”不等于”系统级保证成立”：单组件的账本可靠，并不自动推出交错系统也可靠。病根：从局部到全局的每一步归纳都可能漏条件。药方是五组元理论，一组一组把保证抬上去；最后落到实现映射，验证抽象与工程对得上号。

• 保持（Theorem 64，p.43）：注册表四个良构条件（父指针成树、provision 两两不交、ω 全函数且指向在册 fiber、提交视图只指向 Active 提供者）被每条规则保持。后两条全靠守卫：一个被 remove 的名字不可能还活在谁的提交视图里。
• 恢复精确性（Theorem 68，式 55，p.46）：fiber n 的 episode 从 b 开到 u，中间别人插了任意步（t₁…t_l 时刻作用在别人身上），则 gₙᵘ(γᵘ) ≃K (Ψ{t_l}∘⋯∘Ψ_{t₁})(γᵇ)——跑 n 的累积器，等于那些外来步骤根本没发生过（对照读法 p.46：前提是 n 实例化的 fiber 没在中间动过，否则那些 fiber 本不会存在）。这是”运行逆只撤回自己的贡献、不多不少”的定理化。推论 69：episode 关闭时 γ^{u+1} ≃_K 外来步骤的复合，且 n 的表回到空——O-Remove 的”表空”前提自动满足。证明骨架（p.46–47）：n 自己的步对 φ(γ) 逐次不变（Theorem 7 一路走）；别人的步要么与 n 独立（交换过去，Lemma 66/Thm 47），要么与 n 纠缠（pₘ∩dₙ≠∅ 的提供者被守卫挡住动不了，Lemma 67 分三种情况处理）。纠缠对是独立性原则上管不了的：消费者的操作就作用在提供者安装的值上，两个顺序在每个绑定缺席的状态上都不同——替身是规则本身从不按那个坏顺序交错两张映射（p.44–45）。
• 排序（Theorem 70，p.47–48）：episode 内 ω 不变（Lemma 59(2)），于是消费者 b′ 严格落在提供者 episode 内部（b < b′），提供者关闭晚于消费者（u′ < u），且绑定值在期间只被”声明了该键的 fiber”的操作移动。解析一致性（Theorem 71，p.48）：transition 只跑在单一解析 ω 上；target 一变，要么 transition 还没落地（被 L-Divert 改道），要么恰好落地（落进的迭代本来就是 n 自己的、会被累积器撤掉）——一个 transition 绝不横跨两个依赖解析。
• 进展（Theorem 73，p.49–50）：≺（pₙ∩dₘ≠∅ 即 n ≺ m）无环 + 迭代长度 ≤ K + 名字集有限 ⇒ 无死锁且终止，界 S(n) ≤ (K+3)(V(n)+1)（V(n) 是 target 翻转次数）。无死锁的证明构造很干净：从任一卡住的 Unloading fiber 沿”谁提交视图指向我”上溯，≺ 严格递增，无环 + 有限名 ⇒ 链终止。
• 合流性（Theorem 80，p.54–55）：设每个组件”装满其 provision”（定义 76：激活完成时装上了 provision 的每个键）、≺ 无环，则任意调度到达的静息态，≃ 于规范形——同样的编排步 + 按支持序 ⊲ 一次性各装载一个 episode。动态历史不留痕迹。证明三件套（p.51–55）：支持集 A 只读 τ/π/d/p 四个字段、是编排输入的函数（定义 74/Lemma 75）；对换引理（Lemma 78：两个激活步在独立时交换次序端点不变）；删除引理（Lemma 79：闭合并被 A 排除的 episode 连同其实例化产物可整体删除，状态 ≃_K 不变——vestigial entry 引理 62 保证退役空壳对规则不可见）。
• 实现映射（§5，Table 2，p.58）：Γ∞ ↔︎ ctx（一等上下文），track/effect ↔︎ ctx.effect，Σ/隔离/拦截 ↔︎ ctx[@@store]/ctx.isolate/ctx.intercept，fiber 各字段 ↔︎ fiber.uid/inject/apply/state/dispose/committed/target。核心循环 execute（算法 1，p.59）：generator 驱动 + guard 查询，guard 翻转即停在迭代边界、只留已积累的逆（这就是 L-Divert 的迭代边界语义）；dispose 前插进父上下文的 ctx.dispose——子效应的逆本身是父层的效应，∂²Γ 的递归落地。生命周期（算法 5，p.62–63）：refresh 比对 target（用提供者 uid 的摘要——uid 新鲜不复用，提供者被替换不会被误判为同一个）；reload 在 Line 14 提交视图、unload 在 Line 25 先 drain 所有已通知的依赖再跑 dispose——Theorem 70 的三行对应。论文明确点出一个语义陷阱（p.63）：提供者原地覆写自己的绑定不会被观察到（target 记的是提供者不是值）；想传播就撤了重装。HMR（§5.2.2，p.67–69）：模块分类不动点（有一个 import 被接受则接受、全 declined 则 declined、循环中的默认 declined）→ stale entry 检测 → 事务性重载（失败恢复缓存、用备份模块重建，p.69）——对比 Webpack/Vite 的 HMR 不需要开发者手工标注 accept 边界，因为 fiber 已经圈住了组件的全部效应。

意义：有了这五组，“装卸正确性是定理”才真正成立——动态历史无痕不再是设计愿望，而是带条件、带证明的结论；实现映射则证明这套演算不是纸上谈兵。

流程（补充，自绘；五组元理论的抬升结构——每组定理站在哪几块石头上）：

Thm 7  单步不变量：witness 在手，recover 结果不被单步移动
  │ Thm 5（同态：序列当一步）           → Thm 16  单组件 LIFO 回滚
  │ Def 42 独立 + Lemma 41（生成元判定） → Thm 43   多组件任意排列回滚
  │ Lemma 66（不纠缠=独立）
  │ Lemma 67（纠缠三情况：守卫挡/交换吸收/Reloading 无扰）
  │ Table 1（九规则=写入的完备清单，Lemma 57 confinement）
  │                                    → Thm 68   交错下的恢复精确性（+Cor 69 终态恢复）
  │ Def 72 ≺ + Lemma 59（字段只写一次）  → Thm 73   无死锁 + 步数界 (K+3)(V+1)
  │ Lemma 75（支持集良基）+ Lemma 78（对换）+ Lemma 79（删除）
  │                                    → Thm 80   合流：动态历史无痕
  └── §5 Table 2 + 算法 1/5：抽象 ↔ TypeScript 实现的逐项对照

读法提示：这张图同时是 §六 的路线图——6.1 对应第一行，6.3 第二行，6.4 中间三行，6.5 倒数第二行，6.6 最后一行。每往上一行，“保证”的适用范围就从一个 fiber 扩到任意调度的整个系统。

六、七个定理逐行展开：从扭积同态到合流性

本章七节的分工：主干是 6.4 恢复精确性（Thm 68）与 6.6 合流性（Thm 80）——一分钟卡点名的两个关键判断；6.5 进展性的界（Thm 73）是守卫必然释放的前置，随主干读。支线四节是单机件精查：6.1 扭积同态、6.2 witness 边界、6.3 出序反例、6.7 提交视图，时间紧可后读。

6.1 扭积同态与 LIFO 回滚——每步都有人接住是构造保证（Thm 5 + Thm 16）

先看这笔账的记法：只有一条——前向照做、逆压栈。要紧的是”逐条压”和”一把算”结果相同，否则推理时就得关心记账的分组方式。

下面这笔推导是我的补充（论文证明在 p.10，我逐行重抄验证过）：对任意 (γ, φ) ∈ ∂Γ，

\mathrm{track}(f_1,g_1)\circ\mathrm{track}(f_2,g_2)\,(\gamma,\varphi) = \mathrm{track}(f_1,g_1)\,(f_2(\gamma), \varphi\circ g_2) = (f_1(f_2(\gamma)),\ \varphi\circ g_2\circ g_1)

而扭积的像：\mathrm{track}((f_1,g_1)\circ(f_2,g_2))(\gamma,\varphi) = \mathrm{track}(f_1\circ f_2,\ g_2\circ g_1)(\gamma,\varphi) = (f_1(f_2(\gamma)),\ \varphi\circ g_2\circ g_1)。两式逐点相等，单位显然。白话回译：账本对”过程”不敏感，只对”总账”敏感——这是后面一切”把序列当一个效应”的推理基础。

边界要把 Theorem 7 的假设读清：φ(γ) 不变只在 g(f(γ))=γ 时成立——逆真的撤得动。这个前提运行时不查（§5.1.1，p.59 自认：witness 是组件作者的义务，不是运行时验证的属性），是 §九.1 的入口。序列版（p.12）：n 步的复合逆 (g₁∘⋯∘gₙ)(δₙ)=γ₀，一次应用 Theorem 7 得式 (11)——LIFO 不是约定而是扭积的定义后果。

Thm 7 的证明只有三行，值得原样铺开（p.11，重抄）：

\mathrm{recover}(\mathrm{track}(f,g)(\gamma,\varphi)) = \mathrm{recover}(f(\gamma), \varphi\circ g) = (\varphi(g(f(\gamma))), \mathrm{id}) = (\varphi(\gamma), \mathrm{id}) = \mathrm{recover}(\gamma, \varphi)

中间那步 (\varphi\circ g)(f(\gamma)) = \varphi(g(f(\gamma))) 是复合的定义，而 g(f(\gamma))=\gamma 恰是假设——整个定理就”住”在这一步上：账本 φ 外层套着新逆 g，套对了位置（g 先执行），新效应就等于没发生。序列版把这”一步”换成”整个扭积复合”，靠的正是 Thm 5 把序列压成一步。

Thm 16（LIFO 逐个撤，p.15–16）展开成状态账（补充，按论文证明逐行加注）。设 e_1,\dots,e_n 依次施加于 (\gamma_0,\mathrm{id})：第 i 步把状态推到 \delta_i = f_i(\delta_{i-1})、账本推到 \varphi_i = g_1\circ\cdots\circ g_i。两个方向的断言分别核：

• 应用步（正向走）：每步 g_i(\delta_i)=\delta_{i-1} 由 \mathcal{E}^* 的 witness 直接给出，正是 Thm 7 的假设——所以每走一步，\varphi_i(\delta_i) = \gamma_0 都保持着（可靠性不变量随行）。
• 撤销步（反向走）：第 n 个逆 g_n 第一个执行，它遇到的状态是 \delta_n——恰好是它自己应用时产生的状态，witness 在此有效：撤到 \delta_{n-1}；接着 g_{n-1} 遇到 \delta_{n-1}，又是自己的应用点……一路到 g_1(\delta_1)=\gamma_0。每个逆都”踩点”成功，不是运气，是”后做的先撤”这条执行次序的构造性保证。

这就是”逆序撤销时每个逆恰好拿到自己应用时产生的那个状态”（Theorem 16 原话的直译）的全部内容。它与 §6.3 的反例互为表里：一旦出序，某个逆就会撞上”别人后续效应改过的状态”，witness 不覆盖那里，破坏随即发生。

6.2 witness 的两副面孔——状态永远恢复，账本未必（Thm 11 + Thm 15）

先看直觉。uniform 逆（一个 g 撤所有状态上的 f）像”万能钥匙”，要求太强；per-state 逆（在哪个状态应用就给哪把钥匙）像房卡。witness 的定义精确锁在后者：((\delta,g)=e(\gamma)) \to g(\delta)=\gamma。

推导是我的补充：closure 一行——e₁, e₂ ∈ 𝔈*Γ 复合，(s∘t)(ε) = s(t(ε)) = s(δ) = γ：每个逆恰好在它被制造的那个状态上用，链条自动闭合。这是”组合大效应不需要重新写逆”的形式根据（§7.3 对 React useEffect 的批评正在此：hook 不可组合，所以复合逆无从导出，p.80）。

Theorem 15（p.14–15）的不对称值得单独写：提升后的逆 g′ 满足 g′(Δ) = (γ, φ∘g∘f)。第一分量永远恢复（用 g(δ)=γ）；第二分量（累积器复原）当且仅当 g∘f = idΓ。白话回译：撤销总是把世界弄回原样，但”撤销”这个动作本身不留痕，要求逆是全 state 空间的逆，不只是应用点上的。malloc/free 的例子：free 恢复”这块内存可用”（状态恢复），但不恢复堆的布局（累积器不复原）——下一块 malloc 的地址暴露了发生过 malloc 这件事。观测等价（本篇 §3.4）就是把这个暴露定义成”不算数”。

把 Thm 15 的计算逐行铺开（p.14–15，按论文证明重抄加注）。输入 (\gamma,\varphi)\in\partial\Gamma，e(\gamma)=(\delta,g)，提升 \mathrm{effect}(e)(\gamma,\varphi)=(\Delta,g')，其中按定义 12：\Delta=(\delta, \varphi\circ g)（状态走一步、账本收下 g），g'=\mathrm{track}(g, f)（“撤销本身也是个效应”：前向 g、它的逆是重做 f）。于是

g'(\Delta) = \mathrm{track}(g,f)(\delta, \varphi\circ g) = (g(\delta),\ (\varphi\circ g)\circ f) = (\gamma,\ \varphi\circ g\circ f)

三段各管一件事：g(\delta)=\gamma 是 witness（状态永远恢复）；(\varphi\circ g\circ f) 里多出来的 g\circ f 是”撤销动作”自己留的痕（账本未必恢复）。恢复当且仅当 g\circ f=\mathrm{id}_\Gamma：若成立，\varphi\circ g\circ f=\varphi，提升效应属于 \mathcal{E}^*_{\partial\Gamma}；反之取 \varphi=\mathrm{id}，账本复原迫使 g\circ f=\mathrm{id}——论文正是用这个特例把”当且仅当”钉死（p.15）。最后一行 (\varphi\circ g\circ f)(\gamma)=\varphi(g(\delta))=\varphi(\gamma) 说明：不管留不留痕，可靠性不变量都不动——撤销这步永远不弄脏”回家路”，只是可能在账本上留个自己来过的戳。

6.3 任意排列回滚与出序破坏——§3.3 的练手在这里兑现（Thm 43 + 反例）

连一回前面：§3.3 让你手算的那对 c、s 在这里回来了——你在那里已经算出 c∘s ≠ s∘c，本节只补最后一里路：这个不交换怎样变成一次真实的撤销破坏。

先看直觉。独立 = 我做的事和你的事互不引用，那么撤的时候不用管谁先谁后，甚至可以隔着别人的未撤操作撤自己的。

数值例是我的补充（手算验证过）：Γ = {0,1}²（四态，写成 (x,y)）。A 的效应 = 翻转 x（自逆），B 的效应 = 翻转 y（自逆）——作用于不同”键”，交换。从 (0,0)：A → (1,0)，B → (1,1)。现在先撤 A（模拟”A 组件先被卸载”）：翻转 x 得 (0,1)——B 的贡献完好；再撤 B：(0,0) ✓。

反例：Γ = {0,1,2}，c: γ ↦ γ+1 (mod 3)（逆 c⁻¹: γ ↦ γ−1），s = swap(0,1)（自逆）。从 0：c → 1，s → 0。LIFO 撤销：s(0)=1，c⁻¹(1)=0 ✓。出序撤销（先撤 c，模拟 c 的组件先卸）：c⁻¹(0)=2，s(2)=2——终态 2 ≠ 0，破坏。这两个例子的形状就是 Lemma 67 说的纠缠/非纠缠之分：非纠缠对（不同键）可交换，纠缠对（我操作你提供的值）要么被守卫挡住（提供者走不掉），要么必须等依赖序。

定理在 p.28 的陈述：独立效应族 e₁…eₙ 依次应用后，以 {1,…,n} 的任意排列为序应用各自在应用点 yield 的逆，都到达 γ₀。证明骨架（p.28–29）：固定排列首元素 j，两条引理——(1) gⱼ 在被后续前向映射平移过的任何状态上仍然撤回”删去 eⱼ 的序列”所到达的状态（交换性 + witness 在原应用点）；(2) 后续效应在被 gⱼ 平移过的状态上 yield 同一个逆（定义 42 条款 2）。然后对 n 下归纳。白话回译：交错世界里”卸载单个组件”合法，靠的就是这两条。

两条引理的完整推演（p.28–29，逐行重抄加注）。记 \delta_i = f_i(\delta_{i-1})（完整序列的状态），\delta_i' = (f_i\circ\cdots\circ f_{j+1})(\delta_{j-1})（删去 e_j 的序列的状态），注意 \delta_j'=\delta_{j-1}。

• 断言 (1)：对一切 u\ge j，\delta_u = f_j(\delta_u') 且 g_j(\delta_u) = \delta_u'。第一式对 u 归纳：u=j 时就是 \delta_j=f_j(\delta_{j-1}) 的定义；归纳步是本证明的心脏——

\delta_{u+1} = f_{u+1}(\delta_u) = f_{u+1}(f_j(\delta_u')) = f_j(f_{u+1}(\delta_u')) = f_j(\delta_{u+1}')

中间那步相等就是定义 42 条款 1（f_{u+1} 与 f_j 交换；u+1>j 保证二者是不同成员）。第二式把 g_j 沿后续前向映射一路”搬过去”：

g_j(\delta_u) = (g_j\circ f_u\circ\cdots\circ f_{j+1})(\delta_j) = (f_u\circ\cdots\circ f_{j+1})(g_j(f_j(\delta_{j-1}))) = \delta_u'

每搬一次用一次交换性，最后落点 g_j(f_j(\delta_{j-1}))=\delta_{j-1} 是 e_j 在自己应用点的 witness。合起来：不管隔了多少别人的操作，g_j 总能精确撤回”没装过 e_j“的世界。 - 断言 (2)：i>j 的每个 e_i 在 \delta_{i-1}' 处 yield 的逆与在 \delta_{i-1} 处相同。因为 \delta_{i-1}' = g_j(\delta_{i-1})（断言 1），而 f_j\in\mathcal{M}(e_j)，定义 42 条款 2（一方的变换不扰动另一方 yield 的逆）直接给出 \mathrm{pr}_2(e_i(\delta_{i-1}')) = \mathrm{pr}_2(e_i(\delta_{i-1}))。

有了两条断言，定理就是对 n 的下降归纳：排列首元素 j 执行后（断言 1），局面恰好是”删去 e_j 的独立族 + 剩余排列”（断言 2 保证手里的逆没变），归纳假设接管；空序列到达 \gamma_0。归纳能滚动，全靠删掉一个效应后剩下的族仍两两独立——这是”族”这个设置（而非单对）真正的用途。

6.4 恢复精确性——跑谁的账本，别人的步进就等于没发生（Thm 68）

先看直觉。n 的账本记的是 n 自己的逆。等 n 退房时，公寓已经被别的房客改过了。定理说：n 的累积器作用在”被改过的现在”上，效果等同于作用在”n 刚搬进来的那一刻”上然后跳过 n 住店期间别人的一切动作——n 的退房对别人零扰动，别人的逗留对 n 的退房零干扰。

式 55（p.46）的陈述：episode [b,u] 内作用于非 n 的步 t₁<⋯<t_l，则 g_n^u(\gamma^u) \simeq_K (\Psi_{t_l}\circ\cdots\circ\Psi_{t_1})(\gamma^b)。读法三则（p.46 原文明示的边界）：(1) 等价读在 ≃_K（所有表的绑定层面），控制字段在比较之外；(2) “右侧 = n 从未开始的样子”假设 n 实例化的 fiber 未在 [b,u) 内动过（那些 fiber 本不会存在）；(3) 每个绑定只恢复到其键的 ≃ₖ 为止——单调分配器不复位、堆布局不还原、已发的消息还是已发。

证明引擎拆成三种步、各有一台机器（p.46–47；对 episode 内每个 u 归纳，补充解读）：

步 u 作用在谁身上？            用哪台机器                     效果
────────────────────────────────────────────────────────────────
n 自己（L-Iter/Finish 等）     Thm 7 + witness               φ(γ) 逐次保持
别人 m，与 n 不纠缠            Lemma 66 ⇒ Def 42 条款1        gn 与 Ψᵤ 交换
别人 m，与 n 纠缠              Lemma 67 三情况                也能交换（见下）

Lemma 67（纠缠步，p.45）是全文最密的一页，三情况各用一句话立住：

1. m 是 n 的提供者方向（p_m\cap(d_n\cup p_n)\ne\emptyset）：n 的提交视图 ω 在整个 episode 里钉着 m（Lemma 59(2)），m 天天在 relied 之下——守卫把 m 的一切 L-Unload 压死，m 永远到不了能被”动真格”的状态；而 L-Leave/O-Retire 的状态映射是恒等（Table 1）。所以 \Psi_t = \mathrm{id}：纠缠者根本没出手。
2. m 是消费者方向（k\in p_n\cap d_m）：把 \Psi_t 和 g_n 都拆成原子映射，一对一对地交换过去——不同键的对是键局部映射直接交换；实例化/退役只写空表和控制字段没人读；同键操作对由该键的 witness 供给交换性。最后剩一对硬骨头：m 在键 k 上的操作映射对上 n 在 k 上的 restriction（卸载 = 把键从表里摘掉）。吸收论证：“对 k 的值写一次、随后把 k 整个移除” = “只是移除”——写被移除吸收；反方向则撞上一个 k 已被移除的空表，操作无定义。两边复合在 \gamma^t 上相等。
3. n 正在 Reloading：此时 n 不可能是任何人的提供者（它的键不在 σ_γ，别人的 target 解析到 ⊥）——消费者方向直接不出现；提供者方向归情况 1。

归并回主归纳：n 自己的步逐次保持 φ(γ)（Thm 7 一次一步），别人的步被三种机器逐一”搬过” g_n，归纳假设带着新 Append 的 \Psi_u 滚动——最后 g_n^u(\gamma^u) 与”外来步骤的复合作用在 \gamma^b“相差在 ≃_K 之内。补充：这一段是全文读起来最密的地方，Table 1（p.40）作为”九条规则 = 写入清单”的索引反复被查，读前先把那张表抄在手边。

6.5 进展性的界——守卫的等待为什么必然结束（Thm 73）

先看这个界是怎么数出来的。一个 target 变来变去的系统会不会永远在路上？答案：不会，而且步数可数。每次 target 翻转要么消耗一个严格更下层 fiber 的一步（≺ 下降），要么消耗本 fiber 唯一的一次 τ 写入。

p.49–50 的陈述：≺ 无环、len(eₙ) ≤ K、名字集有限 ⇒ (1) 不静息则某条生命周期规则可走（无死锁）；(2) S(n) ≤ (K+3)(V(n)+1)，且一切极大序列终于静息。数值例（我的补充）：K=2（每组件至多 2 次迭代）、某 fiber 的 target 翻转 3 次，则作用于它的步 ≤ 3×(2+3)=15：每次翻转至多 Leave+Unload+Begin+2 次迭代 = 5 步。论文自认两个假设的分量（p.50）：名字有限要靠”组件不能无界自实例化”来给；≺ 无环是假设不是定理——自环（组件声明自己提供的键）就破环，运行时可以直接报告（§6.5，p.74：依赖环的组件永久 inactive，可从声明静态预测，对比并发死锁必须运行时检测）。

证明的两根支柱各铺开一层（p.49–50，逐行重抄加注）：

支柱 (A)：target 不变的最长区段里，作用在 n 上的步至多 K+3 步。 盯住 Table 1 的 θₙ 列：从 Active(−,ω)（ω≠ω*）出发只有一条命令链——L-Leave、L-Unload，然后若 ω*≠⊥ 再来一个 L-Begin 和至多 len(eₙ)≤K 次 landing（L-Iter/L-Finish）；从 Reloading 出发把 L-Leave 换成 L-Divert，其余同。3 个固定步 + K 次迭代 = K+3。为什么链不会在区段内重复：L-Begin 写下的 ω 就是当时的 target（=ω*），此后落定 Active(−,ω*)，而 target 恒为 ω* 的区段里没有任何规则再适用——链条自己关门。

支柱 (B)：target 的每次翻转，要么消耗一个严格 ≺-更下层 fiber 的一步，要么消耗 n 自己唯一的一次 τ 写入。 targetₙ(γ) 是 τₙ、各 fiber 生命周期状态、提供者表 domain 的函数（定义 53），从来不是绑定值的函数；表 domain 只在”作用于表主自己”的步里变（Lemma 59(1)）；于是每次翻转要么由”作用于提供者 m（k∈dom(σ_m)∩dₙ ⇒ m≺n）“的步造成，要么由 O-Retire 写 τₙ 造成——τ 单调（Lemma 59(5)），每个 fiber 一辈子只有一次。无环性保证 m≠n 且”严格更下层”有底。

两根支柱合起来是一台递归计数器：S(n)\le(K+3)(V(n)+1)，V(n)\le 1+\sum_{m\prec n}S(m)，代入得 B(n)=(K+3)(2+\sum_{m\prec n}B(m))——≺ 无环 ⇒ 这个递归沿良基序展开必有穷（§3.5 演绎一的实装），一切 S(n) 有限、总和有限。无死锁的构造（(1) 的证明）另有一步巧劲：四种”不安静”的 fiber 各有规则可走，唯一可能卡住的是 Unloading 且 relied 的——从它沿”谁提交视图指向我”上溯，每次上溯 ≺ 严格增大且对方也必须是 Unloading（否则就属于四种可走者），无环 + 名字有限逼出”上溯必停于 ¬relied”，L-Unload 放行。

6.6 合流性——任意折腾过的系统，静息时等于从头装一遍（Thm 80）

先看这笔账的来历（图 25）。一个系统被编排器折腾了一天——装了卸、卸了换、换了又回滚。定理说：它停下来的时候，和”把最终配置一次性写下来、按依赖序装一遍”没区别（表逐 key 不可区分，fiber 名字可差）。这正是声明式 loader 增量 reconciliation 的正确性依据（§5.2.1，p.65 明引 Thm 80/73/Cor 69）。

条件盘点（p.54，全部要念）：≺ 无环；名字集有限；每个组件装满其 provision（定义 76——声明提供 k 就必须装 k，不许”有些配置下装”）；排除 failed fiber（§4.4 p.56 自认：一个调度下某迭代可能 raise 而另一个完成，两个静息态就会差那个 fiber 的生命周期状态——所以合流性排除失败者，且”必须排除”）。对照物（p.51 原文点名）：这是增量计算的 change propagation “与从头求值一致”定理在动态组合上的类似物（转引 [47]）。白话回译：动态性的全部自由度（时序、调度、中途状态）都被压缩掉了，只有最终配置算数——这是比”能卸载”强得多的主张：它保证可推理性（组件作者可以只对着静息态推理 coeffect 的 scope，p.55）。

证明展开成一台”洗牌机”（p.51–55，五步；补充解读，引理内容按原文重述）：

任意调度（终态静息 γᵀ）
  │
  │ ① 圈定支持集 A（Lemma 75）：读 τ/π/d/p 四个字段递归定义，
  │    ⊲ = ≺ ∪ 父指针，无环 ⇒ 良基 ⇒ A 有唯一解且是"编排输入的函数"
  ▼
  │ ② 静息时 A = Active 全体（Lemma 77）：quiet + 装满 provision（Def 76）
  │    把支持集与 Active 集合的缺口闭合；A 之外的 fiber 全程 Inactive、没动过
  ▼
  │ ③ 删 episode（Lemma 79）：取 ⊲-最大、其 episode 会闭合的 n
  │    （最大性恰好凑齐引理三前提），Cor 69 说"跑完累积器 = 外来步照旧"，
  │    于是整段 episode 连同它实例化的产物可整体删除，γᵀ 不变（≃ᴷ）
  │    ⇒ 重复此步直到"会闭合的 episode"清零
  ▼
  │ ④ 编排步前置（Lemma 78(2)）：O-Insert/Retire/Remove 与别人的生命周期步
  │    可交换（前者 Ψ=id、只写自己的控制字段），逐个搬到最前，相对次序不变
  ▼
  │ ⑤ episode 排序（Lemma 78(1) + 按 ⊲ 归纳）：独立的激活步两两可对换，
  │    把各 episode 洗成"⊲-最小者先装"的规范次序，逐段排连续
  ▼
规范形：同样的编排步 + 沿 ⊲ 一次性各装一个 episode —— 与任意调度终点 ≃

三处值得停下来看的地方。其一，Lemma 78(1) 的前提保持论证与 §6.3 断言 (1) 同血统：交换两步之前要证明”对方的规则前提不被搬乱”——targetₘ 读的字段里，激活步 m 只移动 dom(σ_m)，而单源纪律（Def 63 条款 2）保证没人声明的键不会被第二个提供者搬动。其二，Lemma 79 删得干净靠两件小事：vestigial entry（Lemma 62：退役空壳对规则不可见）让”被删 fiber 的遗骸”不挡幸存者的路；“声明不相交”让 targetₘ 与 reliedₘ 里对 n 的引用要么随删除放松（守卫只松不紧）、要么把 m 归进被删集合。其三，②的”装满 provision”是把合流从”几乎成立”推到”成立”的那一钉子：没有它，某个组件”在别的组件效应到达的状态下才装某键”就会让静息态依赖调度——独立性（Lemma 66）已经禁止了”依赖别的组件的状态”，totality 再禁掉”依赖没到达的状态”。

6.7 提交视图记 uid 不记值——原地覆写为什么不触发任何人（§5.1.3，p.63）

补充（论文只给一句、值得展开）：target/ω 记录的是提供者的 fiber uid，不是绑定值。好处：uid 新鲜且不复用，提供者被替换不会被误判为”同一个提供者给了同样的值”——替换必然触发重载。代价：提供者原地覆写自己的绑定不触发任何人的重载（dom 和 provider 都没变）。要把变更传播给依赖方，唯一正路是”撤了重装”（withdraw + reinstall，让 key 暂时离开 dom(σ_γ)，制造一次 deactivating + activating）。这把一个接口设计纪律摆在了提供者组件作者面前：可变状态要么自己内部消化（依赖方通过操作读，每次操作天然过 ≃ₖ 的测试），要么走撤装传播——没有第三种”悄悄改”。

七、牵出的前置概念与失效条件

“待补”节点会在此后的分支笔记里逐个补齐；最顺位的两片：Scalable Commutativity Rule（“接口决定交换性”是本篇的核心设计杠杆）与 Nooks（运行时记账回滚的系统级前驱）。

八、发散：从撤销粒度到 harness 自进化

8.1 “撤销”的三个粒度：从 Invalidated 到 accumulator

发散：把簇内碰过的撤销机制排成谱系。StructAgent 的 Invalidated 是状态级撤销——探针判定某个状态不可信后，打上无效标签、下游全部失效重做；撤销的对象是”一个状态节点”，粒度粗、方向是向前重算。本篇的 accumulator 是效应级撤销——每个副作用带逆，卸载时逆序执行；对象是”一次环境修改”，粒度细、方向是向后回滚。LH 的 fresh-context 是回避撤销——不撤销任何东西，每次从零上下文重跑，用隔离代替回收。

三者的适用条件不同：状态级撤销要求”状态可以被重新计算”（重算代价可承受）；效应级撤销要求”每个效应都写得出逆”（作者义务，本篇 witness 的位置）；fresh-context 要求”重跑幂等且外部副作用可容忍”（读多的任务行，写多的不行）。本篇 §6.1 的系统边界理论（p.70–71）给第三个条件补了精确表述：边界内的 location（可独占修改、可还原）走 acquisition（open/malloc/fork 的记录，可逆）；边界外是 emission（write/send 推出去的数据，不可逆），只有”扣留到确定”与”补偿”两条路（p.71）。这解释了 fresh-context 在 agent 任务里为什么常用：agent 的执行记录大多在边界内（文件、进程、内存），emission（对外发消息）少。

回到这篇：它给簇内”检测到污染 → 切断”的原则补上了”切断之后怎么恢复”的下半句——StructAgent 只回答了”标记并重做”（往前），本篇回答了”精确撤销”（往后），两者其实可以叠加：Invalidated 判定 + accumulator 回滚到判定点，比”回滚到 episode 开头”更省。

8.2 与训练侧三处方的对照：回滚是第四种处理

发散：SimpleTIR §8.1 把训练侧处理不稳定的方案排成”删除（SimpleTIR）/ 重采样（MT-GRPO）/ 记账（TARA）“。本篇给执行侧带来第四种：回滚（rollback）。四种方案在同一个二维平面上：信息保留度 × 对判分/逆的要求。删除丢信息、对判分零要求；记账保信息、要求判分质量；重采样保信息、要求采样算力（G^{K−1});回滚保信息（卸载后重装，状态精确复位）、要求逆的质量（每个效应写对逆）。有趣的是”对啥有要求”的迁移：训练侧三方案的要求都压在”评分”上（judge/黄金轨迹/奖励设计），回滚的要求压在”撤销”上（逆的正确性）——后者是工程义务不是统计问题，可以逐效应审计，而 judge 误差率难审计。这也许解释了为什么系统侧（本篇、Nooks 谱系）宁可承担”写逆”的成本：义务明确、可本地验证。

回到这篇：论文 §7.3（p.80–81）把 React useEffect 点名为”结构上最接近效应-清理配对”的现有实践，又指出它的不可组合性正是痛点；§5.1 的实现（generator yield 逆 + 自动复合）就是”让写逆的成本只在原子效应处支付一次”。对簇的含义：如果后续做 agent harness 工程化，“组件注册进 harness 时必须 yield 自己的逆”应该是 harness 的准入契约——这把 SimpleTIR 的”格式契约决定检测上限”翻译成了 harness 版：“逆契约决定回滚上限”。

8.3 fresh-context vs 回滚：状态不污染的两个解，合流性是充分统计量的运行时版

连一连（先连再往下看）：前簇里”历史不污染现在”已有两个解——StructAgent 的 Invalidated、LH 的 fresh-context。它们各自接上本篇的哪件东西？（答案就在下两段：Invalidated 接 track/recover——但 SA 是”标记并重做”，本篇是”精确反演”；fresh-context 接合流性 Thm 80——都要”静息态只看当前配置”，一个靠遗忘，一个靠账本可坍缩。）

发散：LH 的 fresh-context 执行器和本篇的回滚在目标上同一（历史不应污染现在），机制上相反。fresh-context 是遗忘式：丢弃全部历史，重跑；正确性不依赖历史被正确保存，代价是重算。回滚是记忆式：历史被压缩成一摞逆，精确反演；代价是每个效应都要写逆、且恢复只到 ≃。

二者的适用分界恰好是”状态的可重建性”：能从输入重建的状态（缓存、中间结果）用 fresh-context 划算；重建不了或重建代价高的状态（连接、句柄、用户可见的注册）必须用回滚。更有意思的是 Thm 80 与簇内”充分统计量”线索（依赖图：状态 = 充分统计量，LH/StructAgent 线）的同构：合流性说”静息态是编排输入的函数，与路径无关”——终态对历史的条件分布退化为对最终配置的分布，这就是”充分统计量”的确定性版本：最终配置是全部历史的充分统计量。训练侧 TARA/MT-GRPO 争论”中间步骤要不要记账”，本篇从运行时侧给了第三种答案：记账可以，但记完要能坍缩——能坍缩的账本（合流）才不负担路径复杂性。

回到这篇：这也许是本篇对 agent harness 最重要的输出。自进化 harness 的每次自我修改都是一次”编排事件”，如果 harness 的组件层满足本篇的条件，则”harness 现在长什么样”只需要看当前配置，不需要回放修改史——自我修改的历史复杂度被结构性地消掉了，审计也只需要对着配置而不是对着日志。

8.4 观测等价 ≃ₖ：接口即判分器（判分器质量问题簇第四例）

发散：簇内已有三条”检测上限 = 判分器契约”的证据（ToolVerse 黄金轨迹、StructAgent 探针、SimpleTIR void 契约），本篇给出第四例、也是最形式化的一例：≃ₖ 由键的操作集生成——接口发布哪些 outcome，决定哪些差别”存在”。分配器不暴露句柄值 → 句柄重命名不可见 → 分配可交换（p.29–30）；POSIX open 暴露最小描述符 → 分配不可交换。同一个数学结构，两边是”能不能并发扩展”（scalability），中间是”能不能无序撤销”（composability）。设计杠杆因此清晰：想让一个资源可回滚、可交错，就收缩它的接口——少发布一个 outcome，多一类交换。这与 §3.4.2 的 CRDT 论证（每次注册带唯一 tag，转引 [43]）完全同构：CRDT 是”为了交换性而设计数据类型”，≃ₖ 是”为了交换性而设计接口”。

回到这篇：论文把这条写成 Theorem 45/47 的假设结构（witness 在定义处供给），但没有把它当作一个”设计方法论”来正面陈述——散在 §3.4.2 的例子里。对做 agent 工具生态的人，这是可操作的：工具 API 的每个返回值都是未来的回滚障碍，能不返回的标识符就不要返回。

8.5 agent harness 自进化：论文动机与本站主线的交汇点

发散：本篇 §1.2.2（p.5）与 §8（p.82）把 self-evolving agent harness 列为动机与未来验证，给出的论证值得抄录进簇：自进化 harness 要在持续服务中修改自己的组件；没有时间可组合，每次修改 = 重启 = 丢光过程内积累（“in-flight tasks are disrupted repeatedly”，坏修改还会弄死恢复进程本身）；没有空间可组合，模块间的适应只能 ad hoc（naive 热替换静默破坏下游、循环依赖重载时才爆）。论文引用 OpenAI/Anthropic 的 harness engineering 博文（转引 [8][9]，未核对原文内容）说明这已是工业实践话题。对照本站：SimpleTIR §8.4 说”配方即 harness”（训练配方塑造行为分布），LH 说”能力 = 模型 × harness”；本篇补的是 harness 自身的可演化性从哪来——答案是结构性的：组件粒度 + 可逆效应 + 反应式依赖，让”harness 改自己”从高危操作降级为日常操作。验证缺口也明摆着：论文没有 agent 实验（§5.3 案例是聊天机器人），“高频自修改下恢复保证 + 开销”是开放命题（§8 自认）。

回到这篇：对本站的研究问题清单，这直接生成一个候选方向——给一个最小 agent harness（工具注册 + 会话状态 + 子代理）加上 Cordis 式组件语义，测自修改序列下的恢复率与停机时间。这是七篇里第一篇能直接长出工程实验的种子。

8.6 常见误读（破）

这篇的定理容易被读过头，立两个靶子打掉。

误读一：“运行时兜底”论——把 Thm 68/80 读成“运行时会担保我恢复”。破：担保的前提是 witness（逆真的撤得动）与交换性（操作真的互不干扰），两者都是组件作者在定义处的证明义务，运行时一个都不检查（§5.1.1，p.59 自认两处）。定理是有条件的，条件押在作者的承诺上——所以 §九.1 说它“仍是纪律问题，只是从使用处移到了定义处”。

误读二：“恢复 = 复原”论——把“恢复到位”读成“一切回到没发生过”。破：恢复的口径是 ≃ₖ——接口测试测不出的差别才算抹平（Def 31，p.23；Thm 68 的读法三则，p.47：单调分配器不复位、堆布局不还原、已发的消息还是已发）；边界外的 emission 干脆不在担保里，只有扣留与补偿两条路（§6.1，p.71）。回滚撤的是效应，不是时间。

8.7 写作之维：这篇论文自己是怎么说服人的

• 标题先立纲领：“A Programming Paradigm for Spatiotemporal Composability”——不是“一个框架”，是“一个范式”，贡献的量级在标题就报出来了。
• 说服从统计起手（§1.2.1）：VSCode 安装量前 100 里 87 个含可执行代码、卸载即重启——痛点不是讲故事，是数出来的。
• 定义先于算法：Def 1–81 编号密集推进，双条件与带见证的迭代器是主菜，搜索/编排算法反而靠后——“定义即贡献”的排布让证明有处落脚。
• 可信度靠三件套收口：Table 1 把“九条规则 = 全部写入点”钉成完备清单（p.40），Table 2 做抽象到 TypeScript 的逐项映射（p.58），Koishi 4000+ 插件当存在性证明（§5.3 自认 “existence-and-adoption result”，p.70）。

8.8 发散收拢

把五条支线拽回来：8.1 把本篇定位为簇内撤销谱系的”效应级”一格，与 Invalidated（状态级）、fresh-context（回避）互补且可叠加；8.2 把训练侧”删除/重采样/记账”扩展出第四种处理”回滚”，并指出义务从”评分”迁移到”逆”；8.3 论证合流性 = 终态对路径无关 = 充分统计量的运行时版，是本篇对”自进化 harness 可推理”的核心输出；8.4 把”接口决定交换性”收进判分器质量簇，给出收缩接口的设计杠杆；8.5 落到本站主线的交汇与一个可做的实验。合起来，本篇给簇补上的格子是：当组件要在运行中来去时，“撤销”与”依赖”如何从纪律变成定理。

带走一句话：逆在制造的那一刻入账，装卸从此不靠记性；但撤得动靠作者作证，撤得净只到接口为止。

这句话的失效条件（每条都锚在正文）：witness 与交换性是承诺不是检查（p.59）；恢复只到 ≃ₖ（p.47）；emission 出了边界就没有逆（p.71）；≺ 有环、或组件不装满 provision，合流性作废（p.54、Def 76）。

九、承诺制的逆与不可逆边界：本篇的局限

1. witness 承诺制，运行时不验证：逆真的撤得动、操作真的交换，都是定义处附带的证明义务，运行时不检查（§5.1.1，p.59 自认两处）。Theorem 68/80 的全部保证以此为前提——大厦的可靠性锚在组件作者的义务上，工程上仍是纪律问题，只是从”每次使用处”移到了”定义处”。
2. 恢复只到 ≃ₖ，emission 不管：绑定只恢复到其键的等价为止（p.47）；边界外的 emission（写文件、发消息）不可逆，只有扣留与补偿两条路，且补偿的更粗等价下交换性要重新证明（§6.1，p.71）。对 agent 场景，真正的不可逆动作（对外调用）仍在系统外。
3. 单源纪律的简化：一个键至多一个提供者（O-Insert 前提，p.34）；有非空 provision 的组件同时只能有一个 fiber（p.33 自认”简化了形式化而非系统”）。多提供者要走 realm（§4.4，p.56）或 broker（§6.2，p.71–72）两条绕路。
4. 合流性的条件堆：≺ 无环 + 名字有限 + 每组件装满 provision（Def 76）+ 排除 failed fiber（p.56）。任一不满足，招牌定理就缩水——尤其是”声明了却只在某些配置下安装”的组件会破坏静息态 = 配置的函数这一性质（p.65 loader 段明说）。
5. 案例证据是观察性的：单一生态（Koishi）、单一语言（TypeScript），无对照架构、无定量开销（p.70 自认 “existence-and-adoption result rather than a quantitative one”）。
6. 依赖链接是名义的：只有 key 名字相等，无版本/结构兼容——interface drift 与 key collision 两个问题论文自认未解，三个候选方案（包命名空间 / peer dependencies / 结构谓词）各有缺陷，列为开放问题（§6.6，p.75–76）。
7. 开销零数据：Proxy 拦截每次属性访问、get 两跳解析（isolate 表 + store）、notify 全 fiber 扫描（算法 3，p.61，O(fibers×keys)）。Koishi 场景（单实例几十个插件）无碍，但论文用它论证 agent harness 高频自修改场景（§8）时恰恰缺这个数字——正因为把高频自修改摆成了核心动机，开销零数据才从“未尽的测量”升级成“主张与证据之间的缺口”。
8. 原地覆写不观察（§5.1.3，p.63）：提供者改自己的绑定不触发依赖重载——语义上自洽（target 记 uid），但这是个静默陷阱，错误用法不报错、只是不传播。
9. 失败不自愈：迭代 raise 后 fiber 落 FAILED、不许自动重试（防无限循环），重试 = 编排层 revision（§4.4，p.56）——恢复保证因此排除失败者（见 4），但”谁来 revision、何时”留给编排器。
10. 异步宿主降级：异步下迭代不可拒收，L-Divert 只剩 landing 分支（inertial，p.55）——target 中途变化的响应延迟到迭代结束；论文证明结果覆盖惯性宿主（Thm 73 不用 abort 分支），但”停用响应延迟”是真实的运行时代价。

十、最小复现：五个可证伪预测 5/5 通过

10.1 范围声明

本篇的实证主张（Koishi 4000 插件的生产可用性、VSCode 87/100 统计）不可最小复现，论文数字只作引用。以下五个可证伪预测是核心数学的最小演绎，全部纯 CPU 精确算术/离散模拟；脚本 repro/repro_cordis.py（纯 Python 标准库），真实输出 repro/repro_cordis_output.txt，最终 5/5 PASS（首轮 4/5，P1–P3/P5 直接通过，P4 FAIL 已定位为我的测试字母表设计错误，非论文数学问题，见 10.3）。

10.2 可证伪预测与判据（运行前写下）

• P1（扭积-track 同态）：Γ 取 8 元素集上的随机函数对（含非双射），验证 \mathrm{track}((f_1,g_1)\circ(f_2,g_2)) = \mathrm{track}(f_1,g_1)\circ\mathrm{track}(f_2,g_2) 逐点成立，且 Theorem 7 在 g(f(γ))=γ 的状态保持 φ(γ)。判据：10⁶ 次随机组合零反例；并验证假设边界为实（假设失效处 φ 能区分）。
• P2（任意排列回滚 vs 出序破坏）：交换效应族（{0,1}⁴ 上 4 个位翻转）从随机初态应用后，24 种撤销排列全部回初态；非交换族（+1 循环 × swap(0,1)）作对照——LIFO 恒成功、出序撤销到达 ≠ 初态。判据：交换族 24/24 × 100 初态、对照 LIFO 3/3、出序至少 1 处失败。
• P3（守卫时序）：按 9 规则实现最小解释器（效应 = 表-注册式 provide/op/inst 步），12 步编排脚本（含提供者换血 mysql→pg、子组件级联、net 撤了重装）在 200 个随机调度种子下验证 Theorem 70(2)（消费者 episode 严格嵌套提供者 episode）、Thm 73（无死锁、一切序列终于静息）、Thm 64 保全四条款。判据：三类违反全零。
• P4（交换性的接口判据）：表-注册类键（每注册占一条目、逆删该条目、接口只发布内容谓词不发布内部 tag/顺序）与链-插入类键（顺序敏感、dispatch 可观察），枚举长度 ≤3 的全部测试词（字母 = 前向操作 + 已 yield 的逆，Def 31）。判据：表键零区分词（≃）、链键存在区分词（≄）。
• P5（合流性）：同一编排脚本 500 次随机调度到达的静息 σ_γ（domain + 值）与活动组件多重集，与规范形（按 ⊲ 序一次性装配）逐一相等。判据：500/500 全部相等。

10.3 运行结果

脚本真实运行（P1 用时 14.0s，总计约 14s）：

• P1 过：10⁶ 次随机组合 × 8 状态 = 8,000,000 次逐点检验，同态反例 0；Theorem 7 在假设成立处检验 999,255 个状态、反例 0；假设失效被排除的 7,000,745 个状态中 φ 确实区分 6,126,373 个（87.5%）——假设边界是实的，Theorem 7 不是同义反复。
• P2 过：交换族 2400/2400（100 初态 × 24 排列）全部回初态；非交换族 LIFO 3/3 成功、出序撤销 3/3 失败（三个初态全部被破坏，比”至少一处”更强）。
• P3 过：200 个随机调度全部 drain 到静息（步数 43–75），提交视图边 1,894 条逐一检验嵌套（提供者先开、后关），Theorem 70(2) 违反 0；保全违反 0；死锁 0。12 步编排里的硬片段全部走过：提供者换血（mysql 退役 → pg 顶上 → checkin/logger 自动迁移）、group 组件实例化子组件、net 撤了重装（依赖二次重激活）。
• P4 首轮 FAIL，定位为测试设计错误：首轮字母表含 pop（撤销栈顶），它区分出了表键的两个插入序。诊断：pop 在两个运行里不指称同一个映射（A 态栈顶是 b 的逆、B 态是 a 的逆），违反 Def 31 “字母 = 前向映射或已 yield 的特定逆”的语义——表注册 yield 的逆是按条目的闭包（undo_a/undo_b），不是栈顶弹出。修正字母表（去掉 pop、补 has_a/has_b/count 三个可观察字母增强检验力）后重跑。
• P4 过（修正后）：表键 399 个测试词（长度 ≤3 全枚举）零区分；链键首个区分词就是单字母 (disp0,)——插入序不同，一次 dispatch 就暴露。两族判定与理论预测一致。
• P5 过：500 个随机调度的静息态（σ_γ：db → {checkin, logger, pg}，net → {checkin, socket}；活动组件多重集：3×checkin、2×logger、db_pg、group_g、net）与规范形装配逐一相等，无一例外——Theorem 80 的”动态历史无痕”在其条件成立的最小系统上行为成立。

10.4 预测对照

边界重申：本复现支持的是命题的数学行为（同态、排列回滚、守卫排序、接口决定交换性、合流）在其条件成立的最小模型上成立；论文的生产主张（Koishi 案例、VSCode 统计、开销）仍只有论文自报证据。复现里键的值语义取了论文 §3.4.2 的表-注册代表例（并集操作可交换）——若换非交换键（链式覆写），P3/P5 的断言前提即失效，这正是论文把交换性做成 per-key witness 的原因。

五条全对，按门禁自检一次”这预测可能错吗”：可能，而且真错过一次——P4 首轮用 pop 当字母，它”区分”了表键的两个插入序，但 pop 在两个运行里不指称同一个映射（Def 31 的字母语义被我的测试设计违反），FAIL 是测试错、不是数学错；这条留痕恰是可证伪性在工作的实证。再看判据形状：P1/P2/P4/P5 都带”必失败”对照（边界处须被 φ 区分、出序撤销须失败、链键须有区分词），不是”怎么跑都对”的软预测；P3 是纯”无违反”判据，形状最弱，硬度来自 Thm 73 的正断言（200 调度全部静息）。自检结论：可证伪性成立，最弱一环（P3）如实登记。

十一、三张方法卡：守卫演算、接口先行、效果逆同封装

11.1 守卫式生命周期演算（guarded lifecycle calculus）

• 层级：L1 领域具体（多组件系统形式化）。底层原理：归因靠对照（L2 卡已立：notes/method_attribution_by_control.md）。
• 操作定义：把系统状态迁移写成”规则 + 守卫”的演算（9 规则），想要的安全性（消费者 episode 严格嵌套提供者 episode、无死锁、保全条款）作为定理证明而非口头承诺；验证用最小解释器跑 200 个随机调度种子，三类违反程序化断言全零（复现 P3，Thm 70/73/64）。
• 迁移去向：①任何多组件系统（插件、工作流、微服务编排）的安全性论证模板：规则 → 守卫 → 定理 → 随机调度断言；②协议设计的”先写死守卫再写功能”纪律。
• 失效边界：定理覆盖的是演算模型——实现与模型之间的缝隙（解析器、并发原语、外部 IO）不在保证内；随机调度断言依赖种子分布，是定理的抽查不是证明。
• 方法卡：notes/method_guarded_lifecycle.md（L1）

11.2 接口性质先行（interface-first verifiability）

• 层级：L1 领域具体（API/接口设计）。底层原理：立场之争重构为可测量（MCONTR）的近亲——把”这两个实现能不能互换”变成可判定的测量。
• 操作定义：接口只发布内容谓词、不发布内部表示（tag、顺序），使”实现可交换”从口号变成区分词判定：枚举长度 ≤3 的全部测试词，表-注册类键零区分词（可互换 ≃），链-插入类键存在区分词（不可互换 ≄）——复现 P4 的判据本身就是设计审查工具。
• 迁移去向：①API 评审清单：接口暴露的是内容还是表示？②可替换性验收：用区分词枚举代替”应该兼容”的口头保证。
• 失效边界：区分词枚举只在有限深度（≤3）内完备；接口谓词本身写错时判定器给出假安心。
• 方法卡：notes/method_interface_first_verifiability.md（L1）

11.3 效果-逆同封装（effect–inverse packing）

• 层级：L1 领域具体（可撤销系统设计）。
• 操作定义：每个效果封装时携带自己的逆（扭积 f\otimes g + track/recover 同态），撤销正确性化为代数性质：组合的追踪 = 追踪的组合（复现 P1：10^6 随机函数对组合零反例）；并显式给出适用边界——交换效果族任意排列撤销全部回初态，非交换族 LIFO 恒成功、出序撤销必失败（复现 P2 对照组）。
• 迁移去向：①事务/迁移系统的撤销设计（先判效果族是否交换，再选撤销策略）；②编辑器/工作流的 undo 语义规范。
• 失效边界：非交换效果族的出序撤销不可修复，只能限制撤销顺序（LIFO）或改设计；逆不完整（有不可逆 IO）时同态保证失效。
• 方法卡：notes/method_effect_inverse_packing.md（L1）

11.4 方法依赖

本篇产出 L1 三张（守卫式生命周期演算 / 接口性质先行 / 效果-逆同封装）；“接口决定可判定面”的立场在此前已被引为 L2 卡”立场之争重构为可测量”（MCONTR）的第二实例——本篇 §11.2 是它的操作化落地。

十二、还没吃透的六处（未攻克登记）

1. Thm 80 的证明细节：Lemma 79（删除引理）的 vestigial-entry 归纳与 Thm 80(1) 的”闭 episode 逐个摘除”读了两遍才顺；“一个编排步 instantiated 的 fiber 不能前移”（p.55）这段的边界没完全吃透。部分消化：P5 复现在行为层验证了定理的结论（500 调度全等于规范形）与其条件的作用，但行为验证不替代证明阅读——逐行重构仍欠。补齐时机：读 Cordis v4 loader 源码对照 reconciliation 分支。
2. 拦截与 ≃ 的相容性：拦截改变 get 的返回值（metadata 进了提供函数），但 §4.4（p.56）说拦截”no premise reads it、无需扩展演算”。拦截后的 get 是否还是 Def 29 意义上的”该键的操作”、是否自动继承该键的交换性 witness——论文没写，我没推出来。补齐时机：读 Cordis v4 源码里 intercept 的实现。
3. realm 动态 reassign 的两处表述：§4.4 说运行时改 realm = 接口变更、要走 revision 重装（p.56），§5.2.1 的 Algorithm 7 又有”realm moved without reloading its provider”（p.67）的短路径——两者的适用边界没理顺。补齐时机：同上，源码。
4. Koishi 生产规模下的开销：无任何数字。补齐时机：cordiverse/cordis 的 issues/博客，或自测。
5. agent harness 场景的实证：论文动机与结论都指向它但零实验——恢复率、停机时间、高频修改下的守护开销全是空白。这是本站候选研究问题（§8.5）。
6. Thm 73 的 V(n) 界的紧性：界是 (K+3)(V(n)+1)，论文没讨论紧不紧；复现解释器观测到编排+静息总步数 43–75（200 调度），但未仪表化 V(n) 与 S(n) 的分项——界的实际松紧仍未测。补齐时机：解释器加 V/S 计数器重跑。

十三、可信度：A 级原文转录与核对状态

• A 级（论文原文转录，逐页核对）：全部页码引用、定义 1–81 的陈述、Theorem 4/5/7/11/15/16/43/45/47/64/68/70/71/73/80 的陈述、Table 1/2、算法 1–10、§1.2.1 的 VSCode 统计（87/100、7/100——论文自报的 marketplace 统计，脚注 1）。
• B 级（论文自报、无法独立验证）：Koishi 4000+ 插件与四年在产（p.69–70）、VSCode 生态观察、“Cordis v3 在生产运行”（脚注 4）。
• C 级（我的推导 + 已由复现程序化验证）：§6.1 同态逐行重抄（复现 P1：8×10⁶ 逐点零反例）、§6.3 数值例（复现 P2：2400/2400 与 3/3 对照）、§5.7 守卫时序与 §6.6 合流（复现 P3/P5：200 调度 + 500 调度零违反）、§5.5/§8.4 接口判据（复现 P4）、§5.0 的组件示意代码（按论文算法 1/4 模型写的形式化示意，非 Cordis 真实 API）。
• D 级（我的推断，标注于正文）：§八全部发散（撤销谱系、第四种处理、合流=充分统计量、接口即判分器、harness 实验方向）、§九.7–8 的工程批评。
• 横向核实初核（2026-09-03）：版本 v1-only 已核（abs 页直查；2026-08-26 提交，无 v2）。工件存在且活跃：cordiverse/cordis（GitHub API：8037 stars、pushed 2026-09-03、描述与论文副标题一致）、koishijs/koishi（6165 stars、pushed 2026-08-28）；均未验代码与论文一致性（论文 = Cordis v4，Koishi 生产 = v3）。第三方未查（v1 仅一周，查无讨论的概率高——留档待查）；统计审查不适用（无可重算的结果表；论文仅 1 图 2 表且均为映射/规则表）；发表信息：预印本无会议标注。