【deepseek-harness】Cordis 时空可组合性编程范式 — 三段式精读笔记（二）

Cordis 时空可组合性编程范式 — 三段式精读笔记（二）

第3章 可逆效应与反应式协效应

本文档采用三段式结构：每节先给出英文原文，再给出中文翻译，最后给出详细解释说明。
本章是论文核心理论：将经典 effect/coeffect 提升为运行时机制，统一为"上下文范式"。

3. Revertible Effects and Reactive Coeffects / 可逆效应与反应式协效应

原文 (English)

This section lifts the concepts of effects and coeffects introduced in Section 2 to runtime mechanisms, constructing a theory of dynamic composition. The central idea is to turn the typing contexts carrying effects and coeffects into context types, i.e., runtime-operable types that reify the context as a first-class entity. For the effect type, we model it as a context transformation paired with an inverse, achieving local temporal composability. For the coeffect context, we model it as a type carrying dependency information, achieving local spatial composability. An observational equivalence on the coeffects then supplies the effects with independence. The unified context that carries both effects and coeffects constitutes a programming paradigm in its own right.

中文翻译

本节将第2章引入的效应（effects）与协效应（coeffects）概念提升为运行时机制，构建一套动态组合（dynamic composition）的理论。核心思想是把承载效应与协效应的类型上下文（typing contexts）转化为上下文类型（context types），即可运行时操作、把上下文物化为第一类实体（first-class entity）的类型。对于效应类型，我们将其建模为"一个上下文变换配以一个逆变换"，以此实现局部的时间可组合性（local temporal composability）。对于协效应上下文，我们将其建模为承载依赖信息的类型，以此实现局部的空间可组合性（local spatial composability）。随后，协效应上的一种观测等价（observational equivalence）为效应提供独立性（independence）。承载效应与协效应的统一上下文（unified context）本身就构成一种编程范式（programming paradigm）。

详细解释

这一段是整个第3章的纲领，值得逐句拆解。“提升为运行时机制"是关键：第2章把 effect/coeffect 当作类型层面的静态结构（编译期就能在类型里读出"这个函数有哪些效应、需要哪些上下文”），而本章要把它变成运行时能被操作、查询、回滚的对象。做法是把"上下文"从一个隐式的类型环境，提升为一个 first-class entity——即一个可以被传参、被读取、被修改、并且能记录"如何撤销这些修改"的运行时对象。

两条轴线分别对应论文标题"时空可组合性"的"时间"和"空间"：

• 时间可组合性靠"可逆效应"——每个效应都带一个逆变换，组件加载=施加效应，卸载=施加逆变换，环境因此能恢复到加载前。这是"时间"维度，因为它关乎"先做后做、能否撤销"。
• 空间可组合性靠"反应式协效应"——组件声明依赖，运行时在依赖满足时激活、在依赖撤回时停用。这是"空间"维度，因为它关乎"多个组件如何彼此引用、如何排布"。

最后一句预告了第3.3节：把两者合进一个统一上下文 Γ∞，并借协效应的观测等价来给效应独立性兜底，这套合体结构本身就是一种新范式。这为后续章节的"上下文范式"主张埋下伏笔。

3.1. Revertible Effects / 可逆效应

原文 (English)

Temporal composability is the ability to load and unload components at runtime such that, upon unloading, the shared environment is recovered to its pre-composition state. This requires that every modification a component makes to the environment be both trackable and recoverable. We therefore model an effect as a function of type Γ → Γ × (Γ → Γ): applied to the current context, it yields the modified context together with an explicit inverse. Supplying that inverse is what lets the effect be reverted, and returning it to the runtime is what makes the effect trackable. We call such effects revertible: by tracking and composing these inverses during execution, complete environment recovery becomes a structural guarantee.

中文翻译

时间可组合性（temporal composability）是指在运行时加载（load）与卸载（unload）组件的能力，使得卸载时共享环境能恢复到组合前的状态。这要求组件对环境的每一次修改都既是可追踪的（trackable）又是可恢复的（recoverable）。因此我们把一个效应建模为类型为 Γ → Γ × (Γ → Γ) 的函数：施加于当前上下文时，它返回修改后的上下文以及一个显式的逆函数（inverse）。提供这个逆函数正是让效应能被撤销（reverted）的依据，而把它交还给运行时则是让效应可被追踪的依据。我们把这样的效应称为可逆的（revertible）：通过在执行过程中追踪并组合这些逆函数，完整的环境恢复就成为一种结构性保证（structural guarantee）。

详细解释

这段定义了全章的动机和目标。核心模型是一个极简却关键的类型签名 Γ → Γ × (Γ → Γ)：

• 输入：当前上下文 γ : Γ；
• 输出：一对 (δ, g)，其中 δ 是施加效应后的新上下文，g : Γ → Γ 是一个能把任意上下文"撤回"的函数。

注意这里有两个层次的设计巧思：

工程对应：在 DSH/Cordis 实践里，这就是 ctx.effect() 注册清理函数的机制——你 ctx.effect(() => { setup(); return () => teardown(); })，setup 是前向 f，返回的 teardown 是逆 g，框架帮你把它们累积起来，组件卸载时自动按序调用 teardown。track/recover 就是这个累积与回放的形式化。所谓"结构性保证"是指：只要每个效应都守规矩（提供真逆），环境恢复不需要任何额外编程纪律，是数学上被保证的。

3.1.1. Effect Context / 效应上下文

原文 (English)

Given any impure function 𝑓impure : 𝑋 → 𝑌, we transform it into a pure form 𝑓 : Γ × 𝑋 → Γ × 𝑌, where Γ is the context and all possible side effects can be represented as transformations on Γ. For any fixed input 𝑥 : 𝑋, the induced map 𝛾 ↦ pr1(𝑓(𝛾, 𝑥)) captures the side effect of 𝑓 independently of the return value. Effects on Γ therefore live in the monoid of transformations Γ → Γ under composition ∘, where each monoid axiom has a direct reading as a property of effects:
• Closure: the sequential composition of two effects is again an effect;
• Associativity: a composite effect is independent of how it is bracketed;
• Identity: idΓ, the identity function on Γ, acts as the unit of composition.
To model effects that can be undone, we pair each transformation 𝑓 with another transformation 𝑔 that undoes 𝑓, and call 𝑔 a left inverse of 𝑓, abbreviated to inverse throughout the paper. Undoing is one-sided: what an inverse is held to is 𝑔 ∘ 𝑓 and never 𝑓 ∘ 𝑔. Pairs of transformations carry a multiplication of their own:

中文翻译

给定任何非纯函数 𝑓impure : 𝑋 → 𝑌，我们把它变换为纯形式 𝑓 : Γ × 𝑋 → Γ × 𝑌，其中 Γ 是上下文，所有可能的副作用都能表示为对 Γ 的变换。对于任意固定的输入 𝑥 : 𝑋，诱导出的映射 𝛾 ↦ pr1(𝑓(𝛾, 𝑥)) 独立于返回值地捕捉了 𝑓 的副作用。因此 Γ 上的效应存在于变换 Γ → Γ 在复合 ∘ 下构成的幺半群（monoid）中，其中每条幺半群公理都可直接读作效应的一条性质：
• 封闭性（Closure）：两个效应的顺序复合仍是一个效应；
• 结合律（Associativity）：复合效应与加括号的方式无关；
• 单位元（Identity）：Γ 上的恒等函数 idΓ 充当复合的单位。
为了给可撤销的效应建模，我们把每个变换 𝑓 配以另一个能撤销 𝑓 的变换 𝑔，并称 𝑔 为 𝑓 的左逆（left inverse），全文简称逆（inverse）。撤销是单边的：逆被约束的是 𝑔 ∘ 𝑓，而绝非 𝑓 ∘ 𝑔。变换对带有其自身的乘法：

详细解释

这段先把"副作用"标准化：任何非纯函数 f_impure : X → Y 都可以改写成纯函数 f : Γ × X → Γ × Y——把所有副作用都收进一个显式上下文参数 Γ。这正是 State monad 的思想。固定 x 后，"效应"就是纯粹看 γ 如何变成新 γ'，与返回值 Y 无关。所以效应自然落在 Γ → Γ 这个变换幺半群里，复合 ∘ 是群运算，idΓ 是单位。三条公理翻译过来就是效应组合的常识：连做两个效应还是一个效应；先做(A再B)再C 还是 先做A再(B再C) 结果一样；什么也不做的效应就是恒等。

接下来是为"可撤销"做准备的关键设计：把 f 和它的逆 g 配成对 (f, g)。注意论文特别强调"撤销是单边的"——只要求 g ∘ f（先做 f 再做 g 能还原），不要求 f ∘ g。这非常重要，因为真实世界绝大多数效应只有单向可逆：malloc/free 满足 free ∘ malloc 能（在抽象层面）释放内存，但 malloc ∘ free 毫无意义。要求双向可逆（即 f、g 互为双射逆）会过强，几乎排除所有实际效应。单边逆 g ∘ f = id 是恰好的强度。

Definition 1 (定义 1) — Twisted Composition / 扭曲复合

原文 (English)

Definition 1. Define the twisted composition of pairs of context transformations by
(𝑓1, 𝑔1) ∘ (𝑓2, 𝑔2) ≔ (𝑓1 ∘ 𝑓2, 𝑔2 ∘ 𝑔1) (4)
As for ∘ itself, the left operand acts after the right, and the inverses accumulate in the opposite order. It makes (Γ → Γ) × (Γ → Γ) a monoid with unit (idΓ, idΓ), the product of the monoid of transformations with its opposite, which we call the twisted composition monoid 𝔗Γ over Γ.

中文翻译

定义 1. 定义上下文变换对的扭曲复合（twisted composition）为：
(𝑓1, 𝑔1) ∘ (𝑓2, 𝑔2) ≔ (𝑓1 ∘ 𝑓2, 𝑔2 ∘ 𝑔1)　(4)
与 ∘ 本身一样，左操作数在右操作数之后作用，而逆函数按相反顺序累积。这使 (Γ → Γ) × (Γ → Γ) 成为一个以 (idΓ, idΓ) 为单位的幺半群，即变换幺半群与其相反幺半群的直积，我们称之为 Γ 上的扭曲复合幺半群 𝔗Γ。

详细解释

这个定义是全章代数的基石。考虑"先做效应 2，再做效应 1"的复合：前向变换自然是 f1 ∘ f2（先 f2 再 f1）。但逆变换必须反序：要撤销"先做 f2 再做 f1"，必须先撤销 f1、再撤销 f2，即 g2 ∘ g1（先 g1 再 g2）。这就是"扭曲"二字的含义——前向顺序复合，逆向反序复合。这恰好对应 LIFO（后进先出）的卸载语义：最后加载的组件最先被卸载。

这正是函数式编程里经典的"State + 反序"结构，类似线性逻辑里 !A 的对偶、或 free monoid 的反幺半群。𝔗Γ 作为"幺半群与其相反幺半群的直积"，是一个标准的代数构造。把效应抽象成 𝔗Γ 的元素，后续所有关于 track、effect、⋄ 的同态性质，本质上都是在说"我们的运行时操作忠实保持了 𝔗Γ 的代数结构"。这是把工程直觉（卸载要反序）形式化为代数定律的起点。

Definition 2 (定义 2) — Effect Context / 效应上下文

原文 (English)

Definition 2. Given a context Γ, define its effect context as:
𝜕Γ ≔ Γ × (Γ → Γ) (5)
It can be understood as a pair (𝛾, 𝜑), where:
• 𝛾 : Γ is the current context state;
• 𝜑 : Γ → Γ is the accumulator, the composite of the inverses of the effects performed so far, and the function that recovers the context to its initial state.
In particular, the initial effect context can be represented as (𝛾0, idΓ).
We also write 𝜕2Γ = 𝜕Γ × (𝜕Γ → 𝜕Γ), and so on up the tower.

中文翻译

定义 2. 给定上下文 Γ，定义其效应上下文（effect context）为：
𝜕Γ ≔ Γ × (Γ → Γ)　(5)
它可理解为一个对 (𝛾, 𝜑)，其中：
• 𝛾 : Γ 是当前上下文状态；
• 𝜑 : Γ → Γ 是累积器（accumulator），即迄今为止所执行效应之逆函数的复合，也是把上下文恢复到初始状态的函数。
特别地，初始效应上下文可表示为 (𝛾0, idΓ)。
我们还记 𝜕2Γ = 𝜕Γ × (𝜕Γ → 𝜕Γ)，并如此沿塔向上递推。

详细解释

这是论文里最重要的数据结构之一：∂Γ（读作"偏 Γ"或"effect context of Γ"）。它就是用户指南里反复强调的"状态 + 反函数累加器"的对。两个分量各有职责：

• γ : Γ 是"现在环境长什么样"——所有已施加效应的净结果；
• φ : Γ → Γ 是"把当前环境撤回初始环境"的复合逆函数——所有已施加效应之逆的累积。

初始时 φ = idΓ（什么效应都没做，撤回就是恒等）。每施加一个效应 (f, g)，γ 被 f 推进，φ 被 g 复合上去。最终要恢复时，只需对当前 γ 施加 φ，就回到 γ0。这样"恢复"成了一个纯函数应用，不需要遍历历史、不需要额外存储，O(1) 的语义代价（虽然 φ 本身可能很长）。

∂²Γ = ∂Γ × (∂Γ → ∂Γ) 的递推塔是关键伏笔：效应不仅可以作用在 Γ 上，还可以作用在 ∂Γ 上（即"对效应再施加效应"），这对应组件层级嵌套——父上下文管理子上下文的效应。第3.3节的统一上下文 Γ∞ 正是把这座塔折成一个自相似的不动点。工程上，∂Γ 对应框架为每个组件实例维护的"当前环境快照 + 清理函数链"。

Definition 3 (定义 3) — track / 追踪变换

原文 (English)

Definition 3. Define the transformation trackΓ on pairs of context functions:
trackΓ : (Γ → Γ) × (Γ → Γ) → 𝜕Γ → 𝜕Γ
trackΓ = (𝑓, 𝑔) ↦ (𝛾, 𝜑) ↦ (𝑓(𝛾), 𝜑 ∘ 𝑔) (6)
This transformation converts a forward function 𝑓 together with a candidate inverse 𝑔 into a transformation of the effect context 𝜕Γ. Applying trackΓ(𝑓, 𝑔) to a state (𝛾, 𝜑) transforms 𝛾 by 𝑓 and composes the inverse 𝑔 onto 𝜑, thereby tracking the effect of 𝑓 in the context.

中文翻译

定义 3. 定义上下文函数对上的变换 trackΓ：
trackΓ : (Γ → Γ) × (Γ → Γ) → 𝜕Γ → 𝜕Γ
trackΓ = (𝑓, 𝑔) ↦ (𝛾, 𝜑) ↦ (𝑓(𝛾), 𝜑 ∘ 𝑔)　(6)
该变换把一个前向函数 𝑓 连同一个候选逆 𝑔 转化为对效应上下文 𝜕Γ 的变换。把 trackΓ(𝑓, 𝑔) 施加于状态 (𝛾, 𝜑) 时，𝛾 被 𝑓 变换，逆 𝑔 被复合到 𝜑 上，从而在上下文中追踪 𝑓 的效应。

详细解释

track 是"施加一个可逆效应"的形式化。它做的两件事正是前述设计的落实：

注意复合方向 φ ∘ g（先 g 再 φ）——这与 Definition 1 的扭曲复合一致：新的逆加在累积器的"最内层"，意味着卸载时它会最先被执行（LIFO）。track 把 𝔗Γ 的元素 (f, g) 提升为 ∂Γ → ∂Γ 上的变换，是一个从"静态的效应对"到"动态的状态演化"的桥梁。工程上，每次组件调用一个带清理的 effect，框架就是做一次 track：更新环境状态，并把 cleanup 追加到清理链头部。

Theorem 4 (定理 4) — track 与前向投影交换

原文 (English)

Theorem 4. For every (𝑓, 𝑔) ∈ (Γ → Γ) × (Γ → Γ) the following diagram commutes, that is,
pr1 ∘ trackΓ(𝑓, 𝑔) = 𝑓 ∘ pr1 (7)
[交换图：上方 f : Γ → Γ，下方 trackΓ : ∂Γ → ∂Γ，两侧为 pr1 投影]
Proof. For all (𝛾, 𝜑) ∈ 𝜕Γ:
(pr1 ∘ trackΓ(𝑓, 𝑔))(𝛾, 𝜑) = pr1(𝑓(𝛾), 𝜑 ∘ 𝑔) = 𝑓(𝛾) = (𝑓 ∘ pr1)(𝛾, 𝜑) □

中文翻译

定理 4. 对每个 (𝑓, 𝑔) ∈ (Γ → Γ) × (Γ → Γ)，下图交换，即
pr1 ∘ trackΓ(𝑓, 𝑔) = 𝑓 ∘ pr1　(7)
证明. 对所有 (𝛾, 𝜑) ∈ 𝜕Γ：(pr1 ∘ trackΓ(𝑓, 𝑔))(𝛾, 𝜑) = pr1(𝑓(𝛾), 𝜑 ∘ 𝑔) = 𝑓(𝛾) = (𝑓 ∘ pr1)(𝛾, 𝜑) □

详细解释

（证明梗概：直接对任意 (γ, φ) 展开，track 后取第一分量 pr1 得 f(γ)，而 f ∘ pr1 作用于 (γ, φ) 也是 f(γ)，二者相等。）这个定理建立的性质是：track 在"状态分量"上的投影恰好就是前向函数 f。换句话说，如果我们只关心当前环境状态（忽略累积器 φ），那么"施加 track(f,g)"和"直接施加 f"没有区别。φ 只是额外记录了撤销信息，不影响状态演化的正确性。

这保证了 ∂Γ 是 Γ 的"忠实扩展"——它在 Γ 之上加了撤销追踪能力，但没有改变状态语义本身。这是一种"无副作用地增强语义"的设计原则：累积器 φ 是纯粹额外的、可被忽略的簿记信息。工程上，这等价于"清理函数链的存在不影响组件正常运行时看到的环境"。

Theorem 5 (定理 5) — track 是幺半群同态

原文 (English)

Theorem 5. trackΓ is a monoid homomorphism from 𝔗Γ into 𝜕Γ → 𝜕Γ. That is,

中文翻译

定理 5. trackΓ 是从 𝔗Γ 到 𝜕Γ → 𝜕Γ 的幺半群同态。即

trackΓ((𝑓1, 𝑔1) ∘ (𝑓2, 𝑔2)) = trackΓ(𝑓1, 𝑔1) ∘ trackΓ(𝑓2, 𝑔2)　(8)
证明.

详细解释

（证明梗概：单位情形 g=id 时 φ 不变；乘法情形按 track 定义展开，前向得 f1(f2(γ))，累积器得 φ ∘ g2 ∘ g1，正好等于 track 作用于扭曲复合 (f1∘f2, g2∘g1) 的结果。）这个定理建立的性质是：“先在代数层把效应对扭曲复合，再 track 提升"等价于"先分别 track 提升，再在 ∂Γ 上顺序复合”。即 track 忠实地把 𝔗Γ 的代数结构搬运到了运行时状态变换上。

这极其重要：它意味着我们可以在"静态的效应描述"层面做代数推理（结合律、单位律、扭曲复合的顺序），而 track 保证这些推理结论在"动态的状态演化"层面一一成立。工程上：组件 A、B、C 各自注册了一连串带清理的效应，无论你是"先把 A、B、C 的效应描述拼成一个大效应再一次性施加"，还是"依次施加 A、B、C 的效应"，最终环境状态和清理链完全相同。这就是"组合性"——整体行为由各部分行为合成，无额外意外。

Definition 6 (定义 6) — recover / 恢复变换

原文 (English)

Definition 6. Define the transformation recoverΓ on 𝜕Γ:
recoverΓ : 𝜕Γ → 𝜕Γ
recoverΓ = (𝛾, 𝜑) ↦ (𝜑(𝛾), idΓ) (9)
This transformation applies the recovery function 𝜑 to the current state 𝛾 and resets 𝜑 to the identity. The following diagram illustrates how recover recovers the context to its initial state after a sequence of effects track(𝑓1, 𝑔1), ⋯, track(𝑓𝑛, 𝑔𝑛) has been applied to 𝜕Γ.

中文翻译

定义 6. 定义 𝜕Γ 上的变换 recoverΓ：
recoverΓ : 𝜕Γ → 𝜕Γ
recoverΓ = (𝛾, 𝜑) ↦ (𝜑(𝛾), idΓ)　(9)
该变换把恢复函数 𝜑 施加于当前状态 𝛾，并把 𝜑 重置为恒等。下图展示了在一系列效应 track(𝑓1, 𝑔1), ⋯, track(𝑓𝑛, 𝑔𝑛) 施加于 𝜕Γ 之后，recover 如何把上下文恢复到初始状态。

详细解释

recover 是"卸载/回滚"的形式化：把累积器 φ 作用于当前状态 γ，得到恢复后的状态 φ(γ)，同时把累积器清空回 idΓ（因为已经恢复，无需再保留撤销信息）。这是 Definition 2 里"φ 是把上下文恢复到初始状态的函数"这一承诺的兑现。

关键点在于 φ 是所有逆的复合，所以一次 recover 就撤销了所有已追踪的效应——这是"all-or-nothing"（全有或全无）的恢复，3.1.2 节会专门解决"只撤销其中一个、保留其余"的需求。recover 对应工程上的"组件树整体卸载/页面卸载时，框架逆序调用所有已注册的 cleanup 函数，并清空清理链"。重置 φ = id 意味着卸载完毕后系统回到"无待清理"的干净态。

Theorem 7 (定理 7) — track 后 recover 等于 recover（稳健性不变式）

原文 (English)

Theorem 7. For every (𝛾, 𝜑) ∈ 𝜕Γ and every pair (𝑓, 𝑔) with 𝑔(𝑓(𝛾)) = 𝛾,
recoverΓ(trackΓ(𝑓, 𝑔)(𝛾, 𝜑)) = recoverΓ(𝛾, 𝜑) (10)
Proof.
recoverΓ(trackΓ(𝑓, 𝑔)(𝛾, 𝜑)) = recoverΓ(𝑓(𝛾), 𝜑 ∘ 𝑔) = (𝜑(𝑔(𝑓(𝛾))), idΓ) = (𝜑(𝛾), idΓ) = recoverΓ(𝛾, 𝜑) □
A sequence of pairs needs no separate argument. Let (𝑓1, 𝑔1), ⋯, (𝑓𝑛, 𝑔𝑛) be applied in order from (𝛾, 𝜑), and write 𝛿0 = 𝛾 and 𝛿𝑖 = 𝑓𝑖(𝛿𝑖−1). By Theorem 5 the composite trackΓ(𝑓𝑛, 𝑔𝑛) ∘ ⋯ ∘ trackΓ(𝑓1, 𝑔1) is trackΓ of the twisted composite (𝑓𝑛 ∘ ⋯ ∘ 𝑓1, 𝑔1 ∘ ⋯ ∘ 𝑔𝑛), and if 𝑔𝑖(𝛿𝑖) = 𝛿𝑖−1 for every 𝑖 then (𝑔1 ∘ ⋯ ∘ 𝑔𝑛)(𝛿𝑛) = 𝛿0 = 𝛾. That pair therefore meets the hypothesis of Theorem 7 at 𝛾, and one application of the theorem gives
recoverΓ((trackΓ(𝑓𝑛, 𝑔𝑛) ∘ ⋯ ∘ trackΓ(𝑓1, 𝑔1))(𝛾, 𝜑)) = recoverΓ(𝛾, 𝜑) (11)
Taking (𝛾, 𝜑) = (𝛾0, idΓ), recovery carries every state reached this way back to (𝛾0, idΓ). A pair with 𝑔 ∘ 𝑓 = idΓ meets the hypothesis at every state.
Recovery reads a state through the quantity 𝜑(𝛾), and we refer to 𝜑(𝛾) = 𝛾0 as the soundness invariant of a state in 𝜕Γ.

中文翻译

定理 7. 对每个 (𝛾, 𝜑) ∈ 𝜕Γ 和每个满足 𝑔(𝑓(𝛾)) = 𝛾 的对 (𝑓, 𝑔)，

recoverΓ(trackΓ(𝑓, 𝑔)(𝛾, 𝜑)) = recoverΓ(𝛾, 𝜑)　(10)
证明. recoverΓ(trackΓ(𝑓, 𝑔)(𝛾, 𝜑)) = recoverΓ(𝑓(𝛾), 𝜑 ∘ 𝑔) = (𝜑(𝑔(𝑓(𝛾))), idΓ) = (𝜑(𝛾), idΓ) = recoverΓ(𝛾, 𝜑) □
效应对序列无需单独论证。设 (𝑓1, 𝑔1), ⋯, (𝑓𝑛, 𝑔𝑛) 从 (𝛾, 𝜑) 起按序施加，记 𝛿0 = 𝛾、𝛿𝑖 = 𝑓𝑖(𝛿𝑖−1)。由定理 5，复合 trackΓ(𝑓𝑛, 𝑔𝑛) ∘ ⋯ ∘ trackΓ(𝑓1, 𝑔1) 就是扭曲复合 (𝑓𝑛 ∘ ⋯ ∘ 𝑓1, 𝑔1 ∘ ⋯ ∘ 𝑔𝑛) 的 trackΓ，而若每个 𝑖 满足 𝑔𝑖(𝛿𝑖) = 𝛿𝑖−1，则 (𝑔1 ∘ ⋯ ∘ 𝑔𝑛)(𝛿𝑛) = 𝛿0 = 𝛾。该对因此在 𝛾 处满足定理 7 的前提，一次应用定理便得
recoverΓ((trackΓ(𝑓𝑛, 𝑔𝑛) ∘ ⋯ ∘ trackΓ(𝑓1, 𝑔1))(𝛾, 𝜑)) = recoverΓ(𝛾, 𝜑)　(11)
取 (𝛾, 𝜑) = (𝛾0, idΓ)，恢复把以这种方式到达的每个状态都带回到 (𝛾0, idΓ)。满足 𝑔 ∘ 𝑓 = idΓ 的对在每个状态处都满足前提。
恢复通过量 𝜑(𝛾) 读取一个状态，我们把 𝜑(𝛾) = 𝛾0 称为 𝜕Γ 中某状态的稳健性不变式（soundness invariant）。

详细解释

（证明梗概：track 后状态为 (f(γ), φ∘g)，对其 recover 得 (φ(g(f(γ))), id)；由前提 g(f(γ))=γ 得 (φ(γ), id)，恰等于对原状态 recover。序列情形由定理 5 归约为单个扭曲复合对，再套用单步结论。）这个定理建立的性质是恢复目标的稳定性：在施加任何"满足逆关系 g(f(γ))=γ"的效应前后，"recover 之后到达的状态"完全不变。换言之，每个可逆效应都不改变 recover 的终点——无论你做了多少合法的可逆操作，最终 recover 都能回到同一个初始态 (γ0, idΓ)。

这是时间可组合性的核心数学保证。φ(γ) = γ0 被命名为稳健性不变式（soundness invariant）：任何时刻，把当前累积器作用于当前状态，都应回到初始状态。只要每个效应都守规矩（在其作用点提供真逆），这个不变式就永远成立。工程含义：只要每个 effect 注册的 cleanup 真能撤销该 effect 的副作用，那么"组件树整体卸载后环境必然回到加载前的样子"——这不是测试出来的，而是数学保证的。

注意前提 g(f(γ))=γ 是"在作用点 γ 处成立"，这正是单边逆的精确含义：只要求在 f 实际作用的那个状态处 g 能还原，对其他状态 g 的行为不受约束。这给了实际效应实现很大自由度。

3.1.2. Revertible Effect Functions / 可逆效应函数

原文 (English)

The track/recover model of the previous section takes inverses as given a priori: trackΓ(𝑓, 𝑔) fixes 𝑔 before any context state is seen, so one 𝑔 has to serve every state the effect is applied at. In practice, however, the inverse of each effect is not known a priori: it must be supplied by the caller at the point of effect application. Moreover, recover is all-or-nothing: it cannot selectively undo one effect while retaining others. To address both issues, we enhance the model at both the input and output sides:

中文翻译

上一节的 track/recover 模型把逆视为先验给定的：trackΓ(𝑓, 𝑔) 在看到任何上下文状态之前就固定了 𝑔，因此一个 𝑔 必须服务于该效应被施加的每个状态。然而在实践中，每个效应的逆并非先验已知：它必须由调用者在效应施加点提供。此外，recover 是全有或全无的：它无法有选择地撤销一个效应而保留其余。为解决这两个问题，我们在输入侧和输出侧都增强模型：

详细解释

3.1.1 的 track(f, g) 模型有两个实际缺陷：

论文用对称的"输入侧 + 输出侧"增强来解决：

• 输入侧 Γ → Γ × (Γ → Γ)：效应函数接收当前 Γ，返回新 Γ + 针对此次调用的逆。逆是在调用点、看到具体状态后生成的，因此可以因状态而异。
• 输出侧 ∂Γ → ∂Γ × (∂Γ → ∂Γ)：在 ∂Γ 层面同样返回一个逆，使得"撤销这一个效应"本身也是一个可施加的 ∂Γ 上的操作，从而实现选择性撤销。

这种"输入输出结构一致"的对称设计，让两层都能复用同一套 track/diamond/同态理论。这正是接下来定义 𝔈Γ 与 𝔈*Γ 的动机。工程上，输入侧增强对应"cleanup 闭包捕获了 setup 时的具体资源句柄"（如 ctx.effect(() => { const id = setInterval(…); return () => clearInterval(id); })，返回的 cleanup 绑定了具体的 id），输出侧增强对应"卸载单个组件时只跑它自己的 cleanup 链、不动其他组件"。

Definition 8 (定义 8) — Effect Function / Witnessed Effect Function

原文 (English)

Definition 8. Define the effect function 𝔈Γ and witnessed effect function 𝔈∗Γ as:
𝔈Γ ≔ Γ → Γ × (Γ → Γ)
𝔈∗Γ ≔ (𝑒 : Γ → Γ × (Γ → Γ))
× ((𝛾 : Γ) → ((𝛿 : Γ) × (𝑔 : Γ → Γ) × ((𝛿, 𝑔) = 𝑒(𝛾) → 𝑔(𝛿) = 𝛾)))
(12)
where 𝑒(𝛾) yields a pair (𝛿, 𝑔) representing:
• 𝛿 : Γ is the new context;
• 𝑔 : Γ → Γ is the inverse function of the current effect.
An element of 𝔈∗Γ chooses its inverse per state, and the constraint 𝑔(𝛿) = 𝛾 holds that choice to reverting the effect where it was applied, leaving 𝑔 unconstrained everywhere else. A single 𝑔 with 𝑔 ∘ 𝑓 = idΓ meets the constraint at every state at once, and induces an element of 𝔈∗Γ by (𝑓, 𝑔) ↦ 𝛾 ↦ (𝑓(𝛾), 𝑔), which Theorem 11 shows to be a homomorphism. The constraint can be visualized as the following commutative diagram, ensuring that the inverse 𝑒 returns indeed reverses the transformation at the state where 𝑒 was applied.

中文翻译

定义 8. 定义效应函数 𝔈Γ 与带见证的效应函数 𝔈∗Γ 为：

𝔈Γ ≔ Γ → Γ × (Γ → Γ)
𝔈∗Γ ≔ (𝑒 : Γ → Γ × (Γ → Γ)) × ((𝛾 : Γ) → ((𝛿 : Γ) × (𝑔 : Γ → Γ) × ((𝛿, 𝑔) = 𝑒(𝛾) → 𝑔(𝛿) = 𝛾)))　(12)
其中 𝑒(𝛾) 给出一对 (𝛿, 𝑔) 表示：
• 𝛿 : Γ 是新上下文；
• 𝑔 : Γ → Γ 是当前效应的逆函数。
𝔈∗Γ 的元素按状态选择其逆，约束 𝑔(𝛿) = 𝛾 把这一选择限定为"在效应施加处撤销该效应"，而对其他地方的 𝑔 不加约束。一个满足 𝑔 ∘ 𝑓 = idΓ 的单一 𝑔 在每个状态处同时满足约束，并通过 (𝑓, 𝑔) ↦ 𝛾 ↦ (𝑓(𝛾), 𝑔) 诱导出 𝔈∗Γ 的一个元素，定理 11 证明这是一个同态。该约束可视化为如下交换图，确保 𝑒 返回的逆确实在 𝑒 施加的状态处撤销了变换。

详细解释

这个定义区分两个层次：

• 𝔈Γ（效应函数）：纯类型 Γ → Γ × (Γ → Γ)，只要求"接收 Γ，返回新 Γ 和某个逆函数"。这是纯粹的语法层类型，不保证返回的 g 真能撤销 f。
• 𝔈*Γ（带见证的效应函数）：在 𝔈Γ 之上附加一个证明分量——对每个状态 γ，要求 e(γ) = (δ, g) 满足 g(δ) = γ。即"逆 g 在作用点 δ 处确实能把状态还原回 γ"。这个附加的依赖类型分量就是"见证（witness）"，证明该效应在此状态处确实可逆。

关键设计在于见证约束 g(δ) = γ 的局部性：只要求 g 在 f 实际作用的那个状态 δ 处能还原到 γ，对其他状态 g 的行为完全自由。这比"全局逆 g ∘ f = idΓ"弱得多，也更贴合现实——一个 cleanup 函数只需要能撤销它自己那次 setup 做的事，不需要对任意历史状态都成立。

论文指出：若存在一个全局逆 g 满足 g ∘ f = idΓ，则它自动满足每个状态处的见证约束，从而 (f,g) ↦ γ ↦ (f(γ), g) 把 𝔗Γ 的元素嵌入 𝔈Γ。这说明 𝔈Γ 是 𝔗Γ 的推广——𝔗Γ 要求"一个逆适用所有状态"，𝔈Γ 允许"每个状态各自的逆"。工程上，𝔈Γ 对应"cleanup 闭包"模式：每个 effect 调用返回的 cleanup 捕获了该次调用的具体资源，只对该资源有效。

Definition 9 (定义 9) — Effect Composition ⋄ / 效应复合

原文 (English)

Definition 9. Given functions 𝑓, 𝑔 ∈ 𝔈Γ, define their effect composition 𝑓 ⋄ 𝑔 as:
𝑓 ⋄ 𝑔 : Γ → 𝜕Γ
𝑓 ⋄ 𝑔 = 𝛾 ↦ let (𝛿, 𝑠) = 𝑔(𝛾) in let (𝜀, 𝑡) = 𝑓(𝛿) in (𝜀, 𝑠 ∘ 𝑡) (13)

中文翻译

定义 9. 给定函数 𝑓, 𝑔 ∈ 𝔈Γ，定义它们的效应复合 𝑓 ⋄ 𝑔 为：

𝑓 ⋄ 𝑔 : Γ → 𝜕Γ
𝑓 ⋄ 𝑔 = 𝛾 ↦ 令 (𝛿, 𝑠) = 𝑔(𝛾) ；令 (𝜀, 𝑡) = 𝑓(𝛿) ；得 (𝜀, 𝑠 ∘ 𝑡)　(13)

详细解释

为什么需要新运算符 ⋄？因为 𝔈Γ 的元素类型是 Γ → Γ × (Γ → Γ)，不再是 Γ 上的自同态（输出多了一个逆函数分量），所以不能直接用函数复合 ∘ 来组合——∘ 要求前后件的输出输入类型对齐。⋄ 专门处理这个"输出带逆函数"的结构。

语义：先施加 g（得新状态 δ 和逆 s），再在 δ 上施加 f（得更新状态 ε 和逆 t），最终复合逆为 s ∘ t（先撤销 f 用 t，再撤销 g 用 s，即反序）。这与 Definition 1 的扭曲复合完全同构：前向 f ∘ g（先 g 后 f），逆向 s ∘ t（先 t 后 s）。⋄ 就是把扭曲复合从"固定的变换对"推广到"逐状态生成逆的效应函数"。

工程含义：组件做了一连串 effect 调用 e1, e2, …, en，框架用 ⋄ 把它们复合成"一个等效的大效应函数"，其前向是所有 effect 的顺序叠加，其逆是所有 cleanup 的反序叠加。这样无论组件内部有多少 effect，对外都表现为一个可整体施加、整体撤销的单元。

Theorem 10 (定理 10) — ⋄ 的幺半群结构

原文 (English)

Theorem 10. Effect composition carries the monoid structure of 𝔗Γ over to 𝔈Γ. That is,

中文翻译

定理 10. 效应复合把 𝔗Γ 的幺半群结构搬运到 𝔈Γ。即

详细解释

（证明梗概：单位 ηΓ 返回 (γ, id)，对 ⋄ 是左右单位；结合律由 ∘ 的结合律按"状态分量"和"逆分量"分别成立；同态性直接展开 ⋄ 的定义可见复合结果恰为扭曲复合的像。）这个定理建立的性质是：𝔈Γ 在 ⋄ 下也是幺半群，且 𝔗Γ 通过"固定逆"嵌入是同态。即"逐状态生成逆"的效应函数空间，保持了"固定逆"的变换对空间的全部代数结构。

意义：我们在 3.1.1 里为 𝔗Γ 建立的所有代数性质（结合律让复合与加括号无关、单位律让"空效应"有表示），通过 ⋄ 和这个同态，原封不动地迁移到了更贴近实践的 𝔈Γ 上。开发者写"逐次 effect 调用"的代码，享受的是和"静态变换对"一样的代数组合性保证。ηΓ = γ ↦ (γ, id) 是"什么也不做的效应"——它对应一个注册了空 cleanup 的 effect，是组件效应序列的自然起点。

Theorem 11 (定理 11) — 见证在复合下保持

原文 (English)

Theorem 11. Witnessing survives effect composition, and a uniform inverse witnesses at every state. That is,

中文翻译

定理 11. 见证在效应复合下得以保持，且统一逆在每个状态处都是见证。即

详细解释

（证明梗概：单位 id 显然自逆；封闭性利用 ⋄ 的复合逆 s ∘ t，由 s(δ)=γ 和 t(ε)=δ 得 (s∘t)(ε)=γ，即复合后仍满足见证约束。第2部分由 g∘f=id 直接得每个状态处 g(f(γ))=γ。）这个定理建立的性质是："每个 effect 都守规矩（带见证）"这一性质，在用 ⋄ 组合多个 effect 后依然成立。即组件把若干个可逆 effect 复合成一个，得到的整体效应函数仍是可逆的、带见证的。

这是"组合不破坏正确性"的形式化保证。如果没有这个定理，开发者可能担心"单个 effect 的 cleanup 写对了，但组合起来会不会出问题？" 定理 11 回答：不会——只要每个组成部分带见证，复合就带见证。而且 𝔈Γ 是 𝔈Γ 的子幺半群，说明"带见证"是一个在复合下封闭的良好性质。第2部分进一步说明：传统"全局可逆对 (f, g) 满足 g∘f=id"被同态嵌入后自动落入 𝔈Γ，新旧模型兼容。

工程含义：组件内部无论嵌套多深的 effect 注册（ctx.effect 里再 ctx.effect），只要每一层都正确返回了 cleanup，整个组件卸载时就能正确回滚——这是定理 11 保证的，不需要开发者额外操心组合的正确性。

Definition 12 (定义 12) — effect 变换（把 𝔈Γ 提升到 𝔈𝜕Γ）

原文 (English)

Definition 12. Define the effect function transformation effectΓ as:
effectΓ : 𝔈Γ → 𝜕Γ → 𝜕2Γ
effectΓ = 𝑒 ↦ (𝛾, 𝜑) ↦ let (𝛿, 𝑔) = 𝑒(𝛾) in ((𝛿, 𝜑 ∘ 𝑔), trackΓ(𝑔, pr1 ∘ 𝑒)) (14)
Since effectΓ(𝑒) is itself 𝔈𝜕Γ, what it returns is an inverse in the sense of Definition 8 read one level up. That inverse is itself a track of the pair obtained by swapping the two directions of the effect. The ordinary tracking rule applies once more: undoing the effect is an effect in its own right, transforming the state by 𝑔, and the way to undo that is to perform the effect again, which is what pr1 ∘ 𝑒 does. The inverse therefore composes onto the accumulator it is handed, exactly as track prescribes.

中文翻译

定义 12. 定义效应函数变换 effectΓ 为：

effectΓ : 𝔈Γ → 𝜕Γ → 𝜕2Γ
effectΓ = 𝑒 ↦ (𝛾, 𝜑) ↦ 令 (𝛿, 𝑔) = 𝑒(𝛾) ；得 ((𝛿, 𝜑 ∘ 𝑔), trackΓ(𝑔, pr1 ∘ 𝑒))　(14)
由于 effectΓ(𝑒) 本身属于 𝔈𝜕Γ，它所返回的就是把定义 8 上读一层意义上的逆。该逆本身是把效应两个方向互换后所得对的 track。普通的追踪规则再次适用：撤销一个效应本身也是一个效应，它用 𝑔 变换状态，而撤销它的办法是再次执行该效应，这正是 pr1 ∘ 𝑒 所做的。因此该逆就按 track 的规定复合到它所接收的累积器上。

详细解释

这是全章最精巧的定义之一。effect 把一个作用在 Γ 上的效应函数 e ∈ 𝔈Γ，提升为作用在 ∂Γ 上的效应函数 effect(e) ∈ 𝔈∂Γ。提升后 effect(e) 接收 ∂Γ 的状态 (γ, φ)，返回 ∂Γ 的新状态 (δ, φ ∘ g) 以及一个 ∂Γ 上的逆函数——后者实现了 3.1.2 开头说的"输出侧增强"，让"撤销这一个 effect"本身成为 ∂Γ 上可施加的操作。

新状态 (δ, φ ∘ g) 就是 track 做的事（前推 γ、累积 g）。精妙之处在返回的逆函数 trackΓ(g, pr1 ∘ e)：

• 它的前向是 g（把状态 δ 撤回 γ）——即"撤销该 effect"；
• 它的逆（即"撤销这个撤销"）是 pr1 ∘ e——即"再做一次原 effect"。

这构成一个优美的对偶："撤销一个效应"本身也是一个效应，而撤销"撤销"就是再做原效应。这呼应了线性逻辑里的对偶性，也实现了"选择性撤销"——你可以施加 effect(e) 的逆来只撤掉 e 这一个效应，而不动其他效应，因为撤销 e 是 ∂Γ 上独立的可施加操作。pr1 ∘ e 是 e 的前向部分（忽略逆函数），作为"撤销撤销"的逆，逻辑自洽。

工程对应：这就是"卸载单个组件"——只跑该组件的 cleanup 链（g），不碰其他组件；而若之后又重新加载该组件，相当于施加 pr1 ∘ e，把环境重新推回去。这是 hot-reload、组件按需挂卸的理论基础。

Theorem 13 (定理 13) — effect 保持 ⋄

原文 (English)

Theorem 13. effect preserves the ⋄ operation. That is, ∀𝑓, 𝑔 ∈ 𝔈Γ:
effectΓ(𝑓) ⋄ effectΓ(𝑔) = effectΓ(𝑓 ⋄ 𝑔) (15)
Proof. Take any (𝛾, 𝜑) ∈ 𝜕Γ, and let (𝛿, 𝑠) = 𝑔(𝛾) and (𝜀, 𝑡) = 𝑓(𝛿), so that (𝑓 ⋄ 𝑔)(𝛾) = (𝜀, 𝑠 ∘ 𝑡) and pr1 ∘ (𝑓 ⋄ 𝑔) = (pr1 ∘ 𝑓) ∘ (pr1 ∘ 𝑔). Then
(effectΓ(𝑓) ⋄ effectΓ(𝑔))(𝛾, 𝜑) = ((𝜀, 𝜑 ∘ 𝑠 ∘ 𝑡), trackΓ(𝑠, pr1 ∘ 𝑔) ∘ trackΓ(𝑡, pr1 ∘ 𝑓)) = ((𝜀, 𝜑 ∘ 𝑠 ∘ 𝑡), trackΓ(𝑠 ∘ 𝑡, (pr1 ∘ 𝑓) ∘ (pr1 ∘ 𝑔))) = effectΓ(𝑓 ⋄ 𝑔)(𝛾, 𝜑)
where the first step unfolds Definition 12 at (𝛾, 𝜑) and at (𝛿, 𝜑 ∘ 𝑠), the second is Theorem 5, and the third folds Definition 12. □

中文翻译

定理 13. effect 保持 ⋄ 运算。即 ∀𝑓, 𝑔 ∈ 𝔈Γ：

effectΓ(𝑓) ⋄ effectΓ(𝑔) = effectΓ(𝑓 ⋄ 𝑔)　(15)
证明. 取任意 (𝛾, 𝜑) ∈ 𝜕Γ，令 (𝛿, 𝑠) = 𝑔(𝛾)、(𝜀, 𝑡) = 𝑓(𝛿)，于是 (𝑓 ⋄ 𝑔)(𝛾) = (𝜀, 𝑠 ∘ 𝑡) 且 pr1 ∘ (𝑓 ⋄ 𝑔) = (pr1 ∘ 𝑓) ∘ (pr1 ∘ 𝑔)。则
(effectΓ(𝑓) ⋄ effectΓ(𝑔))(𝛾, 𝜑) = ((𝜀, 𝜑 ∘ 𝑠 ∘ 𝑡), trackΓ(𝑠, pr1 ∘ 𝑔) ∘ trackΓ(𝑡, pr1 ∘ 𝑓)) = ((𝜀, 𝜑 ∘ 𝑠 ∘ 𝑡), trackΓ(𝑠 ∘ 𝑡, (pr1 ∘ 𝑓) ∘ (pr1 ∘ 𝑔))) = effectΓ(𝑓 ⋄ 𝑔)(𝛾, 𝜑)
其中第一步在 (𝛾, 𝜑) 与 (𝛿, 𝜑 ∘ 𝑠) 处展开定义 12，第二步用定理 5，第三步折回定义 12。 □

详细解释

（证明梗概：在 (γ, φ) 处展开 effect(f) ⋄ effect(g)，状态分量得 (ε, φ∘s∘t)；逆分量是两个 track 的复合，由定理 5（track 是同态）合并为单个 track (s∘t, (pr1∘f)∘(pr1∘g))。这恰好等于 effect(f⋄g) 在该处的展开。）这个定理建立的性质是：“先在 Γ 层用 ⋄ 复合两个效应，再用 effect 提升"等价于"先分别用 effect 提升，再在 ∂Γ 层用 ⋄ 复合”。即 effect 是 ⋄ 的同态。

这与定理 5（track 是同态）一脉相承，但升了一层：track 把 𝔗Γ 的结构搬到 ∂Γ → ∂Γ，effect 把 𝔈Γ 的 ⋄ 结构搬到 𝔈∂Γ。意义在于"分层的代数一致性"——无论你在哪一层（Γ、∂Γ、∂²Γ…）做组合，代数行为都一致。这是 ∂-塔能折叠成自相似 Γ∞（3.3.1）的数学前提。工程上：父组件管理多个子组件的效应，"先复合子组件效应再提升到父层"和"先各自提升再在父层复合"等价，这让嵌套组件树的卸载语义无歧义。

Theorem 14 (定理 14) — 提升映射与前向投影的关系

原文 (English)

Theorem 14. Let 𝑒 ∈ 𝔈Γ, write 𝑓 ≔ pr1 ∘ 𝑒, and let 𝑒′ ≔ effectΓ(𝑒) with forward map 𝑓′ ≔ pr1 ∘ 𝑒′. Then

中文翻译

定理 14. 设 𝑒 ∈ 𝔈Γ，记 𝑓 ≔ pr1 ∘ 𝑒，并令 𝑒′ ≔ effectΓ(𝑒)，其前向映射为 𝑓′ ≔ pr1 ∘ 𝑒′。则

详细解释

（证明梗概：第1部分直接由定义 12 展开，提升后的状态分量就是 f(γ)，与"先投影再施加 f"一致；第2部分复用定理 4，因为提升后的逆 g' = track(g, f)，而 track 与投影交换。）这个定理建立的性质是：effect 提升在"状态投影"上与原效应一致——提升后的前向映射 f' 投影到状态层等于原 f，提升后的逆 g' 投影到状态层等于原 g。

这是定理 4（track 与投影交换）在 effect 层面的对应。它说明 ∂Γ 这一层是 Γ 的"忠实扩展"：添加累积器 φ 和"可选择性撤销"能力，没有改变状态层面的语义。意义在于分层抽象的健全性——开发者可以只在 Γ 层面推理"状态怎么变"，而 ∂Γ 层的累积器、可撤销逆等机制是透明的增强，不引入额外状态行为。工程上：组件看到的环境状态，无论框架内部用 ∂Γ 还是 Γ 表示，对组件逻辑而言等价。

Theorem 15 (定理 15) — 提升逆的计算与稳健性保持

原文 (English)

Theorem 15. Let 𝑒 ∈ 𝔈∗Γ and write 𝑓 ≔ pr1 ∘ 𝑒. Fix (𝛾, 𝜑) ∈ 𝜕Γ, let (𝛿, 𝑔) = 𝑒(𝛾), and write (Δ, 𝑔′) for the value of effectΓ(𝑒) at (𝛾, 𝜑). Then
𝑔′(Δ) = (𝛾, 𝜑 ∘ 𝑔 ∘ 𝑓) (16)
The state is recovered exactly. The accumulator is restored as well, equivalently effectΓ(𝑒) ∈ 𝔈∗𝜕Γ, if and only if 𝑔 ∘ 𝑓 = idΓ; and in every case (𝜑 ∘ 𝑔 ∘ 𝑓)(𝛾) = 𝜑(𝛾), so the soundness invariant is preserved.
Proof. By Definition 12, Δ = (𝛿, 𝜑 ∘ 𝑔) and 𝑔′ = trackΓ(𝑔, 𝑓), so
𝑔′(Δ) = (𝑔(𝛿), 𝜑 ∘ 𝑔 ∘ 𝑓) = (𝛾, 𝜑 ∘ 𝑔 ∘ 𝑓)
using 𝑔(𝛿) = 𝛾. Membership in 𝔈∗𝜕Γ requires this to equal (𝛾, 𝜑) at every input; taking 𝜑 = idΓ turns the equality of accumulators into 𝑔 ∘ 𝑓 = idΓ, and that condition conversely gives the equality of accumulators for every 𝜑. Finally (𝜑 ∘ 𝑔 ∘ 𝑓)(𝛾) = 𝜑(𝑔(𝛿)) = 𝜑(𝛾). □
The lower triangle therefore closes only when the inverse witnessed at 𝛾 reverts 𝑓 at every state, so effectΓ does not carry 𝔈∗Γ into 𝔈∗𝜕Γ. What holds in every case is agreement at 𝛾: recoverΓ(𝑔′(Δ)) = recoverΓ(𝛾, 𝜑), which is the whole of what Theorem 7 assumes of an accumulator, so reverting leaves the recovery target untouched.

中文翻译

定理 15. 设 𝑒 ∈ 𝔈∗Γ，记 𝑓 ≔ pr1 ∘ 𝑒。固定 (𝛾, 𝜑) ∈ 𝜕Γ，令 (𝛿, 𝑔) = 𝑒(𝛾)，并记 (Δ, 𝑔′) 为 effectΓ(𝑒) 在 (𝛾, 𝜑) 处的值。则

𝑔′(Δ) = (𝛾, 𝜑 ∘ 𝑔 ∘ 𝑓)　(16)
状态被精确恢复。累积器也一并恢复（等价于 effectΓ(𝑒) ∈ 𝔈∗𝜕Γ）当且仅当 𝑔 ∘ 𝑓 = idΓ；而在任何情况下 (𝜑 ∘ 𝑔 ∘ 𝑓)(𝛾) = 𝜑(𝛾)，故稳健性不变式得以保持。
证明. 由定义 12，Δ = (𝛿, 𝜑 ∘ 𝑔) 且 𝑔′ = trackΓ(𝑔, 𝑓)，故 𝑔′(Δ) = (𝑔(𝛿), 𝜑 ∘ 𝑔 ∘ 𝑓) = (𝛾, 𝜑 ∘ 𝑔 ∘ 𝑓)，用到 𝑔(𝛿) = 𝛾。属于 𝔈∗𝜕Γ 要求此式在每个输入处等于 (𝛾, 𝜑)；取 𝜑 = idΓ 把累积器相等化为 𝑔 ∘ 𝑓 = idΓ，而该条件反过来也对每个 𝜑 给出累积器相等。最后 (𝜑 ∘ 𝑔 ∘ 𝑓)(𝛾) = 𝜑(𝑔(𝛿)) = 𝜑(𝛾)。 □
因此下三角只在"𝛾 处见证的逆在每个状态处都还原 𝑓"时才闭合，故 effectΓ 并不把 𝔈∗Γ 映入 𝔈∗𝜕Γ。任何情况下都成立的是在 𝛾 处的一致：recoverΓ(𝑔′(Δ)) = recoverΓ(𝛾, 𝜑)，这正是定理 7 对一个累积器的全部假设，故撤销使恢复目标保持不变。

详细解释

（证明梗概：提升后的状态 Δ = (δ, φ∘g)，提升后的逆 g' = track(g, f)，所以 g'(Δ) = (g(δ), φ∘g∘f) = (γ, φ∘g∘f)，用到见证 g(δ)=γ。要让它完全等于原 (γ, φ) 需 φ∘g∘f = φ 对所有 φ 成立，等价于 g∘f=id。但稳健性不变式 φ(γ) 始终保持，因为 (φ∘g∘f)(γ) = φ(g(δ)) = φ(γ)。）这个定理揭示了一个微妙的不对称：

• 状态被精确恢复：g'(Δ) 的状态分量是 γ，撤销后状态回到施加 effect 前。✓
• 累积器只在 g∘f=id（全局可逆）时才完全恢复：否则累积器变成 φ∘g∘f，多了 g∘f 的"残留"。这意味着 effect 不把 𝔈Γ（局部见证）映入 𝔈∂Γ（∂Γ 层的局部见证）——这是一个刻意的"不完美"。

但论文随即指出：即便累积器不精确恢复，稳健性不变式 φ(γ) = γ0 依然保持（因为残留 g∘f 作用在 γ 上由见证得 γ，故 φ(g(f(γ))) = φ(γ)）。而且 recover(g'(Δ)) = recover(γ, φ)——撤销后，"recover 的终点"不变。这正是定理 7 所需的全部。

工程直觉：选择性撤销（只撤一个组件）后，累积器可能不再是完美的"全局恒等复合"，留下了被撤组件的"幻影"残留；但这不影响"若现在整体 recover，仍能回到初始态"这一关键保证。状态是对的，整体回滚能力是对的，只是累积器的内部表示多了无害的残留。这在实践中完全可接受——你撤掉一个组件后，环境状态正确，且若需要彻底回滚仍能回滚。这就是论文所说的"撤销使恢复目标保持不变"。

Theorem 16 (定理 16) — 反序撤销恢复各自应用点状态

原文 (English)

Theorem 16. Let 𝑒1, ⋯, 𝑒𝑛 ∈ 𝔈∗Γ be applied in order from (𝛾0, idΓ) and reverted in the reverse order. Then

中文翻译

定理 16. 设 𝑒1, ⋯, 𝑒𝑛 ∈ 𝔈∗Γ 从 (𝛾0, idΓ) 起按序施加，并按反序撤销。则

详细解释

（证明梗概：施加步骤由见证 g(δ)=γ 满足定理 7 前提，故保稳健性不变式；反序撤销时，第 i 个逆收到的是"第 i 次应用产生的状态"（因为后续应用已被更后的逆先撤销了），由定理 15 精确恢复并保稳健性。）这个定理建立的性质是：反序（LIFO）撤销能让每个逆恰好作用于它自己当初应用时产生的状态，从而精确恢复。

关键洞察：“反序"之所以不需要任何额外假设（不像独立性那样需要交换性条件），是因为 LIFO 天然保证"撤销 e_i 时，e_{i+1}…e_n 已经被撤销了，环境正好是 e_i 应用后的状态 δ_i”，于是 e_i 的逆 g_i 收到的正是它见证所对应的状态 δ_i，由见证 g_i(δ_i)=δ_{i-1} 精确恢复。这是累积器 φ 的自然语义——它就是按 LIFO 反序复合的。

工程含义：框架卸载组件树时按"后注册先卸载"的 LIFO 顺序调用 cleanup，每个 cleanup 收到的环境正好是它注册时的环境，因此能正确撤销。这是 React useEffect 清理、Vue unmounted hook、DSH 组件卸载等机制的共同理论基础——LIFO 不是随意选择，而是数学上保证"每个清理函数作用于它熟悉的上下文"的唯一顺序。定理 16 是 3.1 节"局部时间可组合性"判据的一半（另一半是定理 7 的整体恢复）。

3.1.3. Independence of Effects / 效应的独立性

原文 (English)

Reverting an effect at the state its own application produced is what Theorem 16 covers; reverting one at any other state is what this subsection covers. Two situations call for the latter. An inverse may be run while later effects are still in place, which is what withdrawing one component from a running system amounts to; and one sequence may interleave the effects of several components, each keeping the inverses of its own, so that the inverses of one component are separated by the applications of another. In both an inverse meets a state that foreign effects have moved, and whether it still reverts what it was built to revert is a question of commutation: what has to commute is every transformation one effect can perform with every transformation the other can perform, forward map and yielded inverse alike. A single accumulator settles neither situation, 𝜑 being a composite that runs every inverse it holds in one order and all at once.

中文翻译

在一个效应自身应用所产生的状态处撤销它，是定理 16 所覆盖的情形；在任意其他状态处撤销一个效应，则是本小节所覆盖的情形。两种情况需要后者。一个逆可能在后续效应仍在位时运行，这正是"从运行系统中撤下一个组件"所意味的；而一个序列也可能交织多个组件的效应，各自保留自己的逆，使得一个组件的逆被另一个组件的应用所分隔。两种情况下，一个逆都会遇到被外来效应搬动过的状态，而它是否仍能撤销它当初被构造来撤销的东西，是一个交换性问题：必须交换的是某个效应能执行的每个变换与另一个效应能执行的每个变换，前向映射与所产逆函数一视同仁。单个累积器无法解决这两种情形，因为 𝜑 是一个复合，按一个顺序一次性运行它持有的所有逆。

详细解释

这一段定义了"撤回（withdrawal）"与"反序撤销"的本质区别，是全章工程直觉最关键的一处：

• 定理 16（反序撤销）：先撤最后施加的，环境逐步还原，每个逆总作用于"自己产生的状态"。这要求"先做后撤"的严格 LIFO 配对。
• 撤回（withdrawal）：从运行系统中单独撤下某一个组件，而其他组件的效应仍在位。此时被撤组件的逆遇到的状态，已经被"它之后施加的其他组件的效应"搬动过了——逆不再作用于它熟悉的 δ_i，而作用于一个被外来效应改变过的状态。

为什么这很难？因为单个累积器 φ 是"所有逆的复合，按一个固定顺序一次性施加"，它无法表达"只撤 e_j、保留 e_{j+1}…e_n"。要做选择性撤回，就必须让 e_j 的逆 g_j 作用于"被 e_{j+1}…e_n 改变后的状态"，而 g_j 是否还能正确撤销，取决于 g_j 与那些外来变换是否交换——即"先做外来效应再做 g_j"和"先做 g_j 再做外来效应"是否等价。这就是"交换性"成为独立性核心的原因。

论文点出两个需要撤回的真实场景：(1) 热卸载某个组件（其他组件继续运行）；(2) 多组件效应交织（A 的效应、B 的效应、A 的效应、B 的效应…交替）。两者都要求"逆能对付被外来效应搬动的状态"。后续定义 17-19、定理 20、推论 21 正是为此建立交换性条件。工程上，这是"插件式架构""动态启停模块"的理论门槛——没有独立性保证，撤一个插件可能破坏其他插件的状态。

Definition 17 (定义 17) — Transformation Monoid 𝔐(𝑒) / 变换幺半群

原文 (English)

Definition 17. For an effect function 𝑒 ∈ 𝔈Γ, the transformation monoid 𝔐(𝑒) is the submonoid of Γ → Γ generated by the forward map of 𝑒 together with every inverse 𝑒 yields, and the generators of 𝔐(𝑒) are the elements of that generating set:
𝔐(𝑒) ≔ ⟨{pr1 ∘ 𝑒} ∪ {pr2(𝑒(𝛾)) | 𝛾 ∈ Γ}⟩ (17)
An effect induced by a pair (𝑓, 𝑔) ∈ 𝔗Γ has 𝑓 and 𝑔 for its generators, the inverse it yields being 𝑔 at every state.

中文翻译

定义 17. 对一个效应函数 𝑒 ∈ 𝔈Γ，变换幺半群 𝔐(𝑒) 是 Γ → Γ 中由 𝑒 的前向映射连同 𝑒 所产每个逆共同生成的子幺半群，𝔐(𝑒) 的生成元就是该生成集中的元素：

𝔐(𝑒) ≔ ⟨{pr1 ∘ 𝑒} ∪ {pr2(𝑒(𝛾)) | 𝛾 ∈ Γ}⟩　(17)
由对 (𝑓, 𝑔) ∈ 𝔗Γ 诱导的效应以 𝑓 和 𝑔 为生成元，它在每个状态处所产的逆都是 𝑔。

详细解释

𝔐(e) 收集了"效应 e 可能执行的所有变换"——包括它的前向映射 pr1 ∘ e，以及它在每个可能状态 γ 处可能产出的逆 pr2(e(γ))。这些变换在复合下生成一个幺半群（因为 𝔈Γ 的逆是逐状态的，e 在不同状态可能产出不同的逆，所以要把"所有可能状态的逆"都纳入生成元）。

为什么要收集"前向 + 所有逆"而不只是前向？因为独立性要求"两个效应的所有变换两两交换"——不仅前向之间交换，前向与逆、逆与逆都要交换。原因是：撤回 e_1 时，e_1 的逆 g_1 要与"e_2 的前向 f_2"（把状态搬动）交换；而若 e_2 也在被撤回，e_2 的逆 g_2 也要与 g_1 交换。所以必须把每个效应的"全部变换能力"纳入考量，𝔐(e) 正是为此定义。

由固定对 (f, g) 诱导的效应最简单：前向恒为 f、逆恒为 g，所以 𝔐(e) = ⟨f, g⟩ 只有两个生成元。这把 𝔗Γ 的情形纳入了 𝔐(e) 框架。工程上，𝔐(e) 可理解为"组件 e 可能对环境做的所有动作的集合"——包括它的正向操作和它的所有可能的清理动作。

Lemma 18 (引理 18) — 交换性由生成元判定，⋄ 不扩大变换幺半群

原文 (English)

Lemma 18. Commutation is settled on the generators, and ⋄ enlarges no transformation monoid. That is,

中文翻译

引理 18. 交换性在生成元上即可判定，且 ⋄ 不扩大任何变换幺半群。即

详细解释

（证明梗概：第1部分用"与某集交换的映射构成子幺半群"两次——先证 𝔐(e1) 全在"与 𝔐(e2) 生成元交换"的子幺半群里，再固定 e1 的元素证 𝔐(e2) 全在"与它交换"的子幺半群里；第2部分由 ⋄ 的定义，复合效应的生成元都是成分生成元的复合。）这个引理是实用性的关键：判定两个效应是否全部变换两两交换，只需检查生成元层面的交换性即可——幺半群的封闭性会把交换性自动传播到所有复合元素。

这极大降低了独立性判定的负担：不用枚举 𝔐(e1)、𝔐(e2) 的所有元素（可能无穷多），只要检查"e1 的前向 + e1 的所有逆"与"e2 的前向 + e2 的所有逆"这有限几对生成元是否交换。第2部分说明 ⋄ 复合不引入新的变换能力——复合效应的变换幺半群被成分的并集所界定，所以"复合后的独立性"可由"成分间的独立性"推出。这为定理 42（多操作组件的独立性）铺路。工程上：判断"两个组件能否独立撤回"，只需看它们各自的核心操作（前向+清理）是否交换，不必分析它们组合后的所有可能行为。

Definition 19 (定义 19) — Independence / 独立性

原文 (English)

Definition 19. Effect functions 𝑒1, 𝑒2 ∈ 𝔈Γ are independent when

中文翻译

定义 19. 效应函数 𝑒1, 𝑒2 ∈ 𝔈Γ 是独立的（independent），当

∀𝑓 ∈ 𝔐(𝑒1), 𝑔 ∈ 𝔐(𝑒2). 𝑓 ∘ 𝑔 = 𝑔 ∘ 𝑓　(18)

∀𝑔 ∈ 𝔐(𝑒2), 𝛾 ∈ Γ. pr2(𝑒1(𝑔(𝛾))) = pr2(𝑒1(𝛾))　(19)
并对 𝑒1、𝑒2 互换同样要求。
族 (𝑒𝑙)𝑙∈𝐿 是成对独立的（pairwise independent），当每对 𝑙 ≠ 𝑙′ 的 𝑒𝑙、𝑒𝑙′ 都独立。族中可重复一个效应函数，而把一个效应视为与自身独立，即是要求 𝔐(𝑒) 交换。
对于由对 (𝑓1, 𝑔1) 与 (𝑓2, 𝑔2) 诱导的效应，条款 (1) 由引理 18(1) 即四对 𝑓1, 𝑓2；𝑔1, 𝑔2；𝑓1, 𝑔2；𝑔1, 𝑓2 的交换，而条款 (2) 直接成立，因为诱导效应在每个状态处只产一个逆。⋄ 下的交换是不同的性质。𝑒1 ⋄ 𝑒2 = 𝑒2 ⋄ 𝑒1 所等同的，是两种顺序的复合前向映射彼此相等、两种顺序的复合逆彼此相等，每个逆在复合中进入的是其自身应用所产生的状态；而独立性则把一个效应的每个变换与另一个的每个变换关联起来，包括前向映射与外来逆的配对。

详细解释

独立性定义有两条要求：

论文特别区分了"独立"与"⋄ 交换"：e1 ⋄ e2 = e2 ⋄ e1 只说"两种施加顺序的复合结果相等"，其中每个逆作用于"自己应用产生的状态"；而独立性是更强的"每个变换与每个变换（含外来逆）交换"。前者是"整体顺序无关"，后者是"局部可任意穿插撤回"。独立性蕴含 ⋄ 交换，但反之不然。一族效应成对独立，且"一个效应与自己独立"即其 𝔐(e) 是交换幺半群——这要求同一效应的多次施加之间也交换（如多次注册同类资源）。

由固定对诱导的效应，条款2自动成立（逆恒为 g，不随状态变），只需检查条款1的四对生成元交换。工程上，独立性对应"两个组件操作互不干涉的资源"——例如 A 注册路由、B 注册事件监听，两者改的是不同的表，天然交换；而 A、B 都往同一个有序链表插入中间件则不独立（顺序敏感）。

Theorem 20 (定理 20) — 独立性下省略一个效应的状态定位

原文 (English)

Theorem 20. Let 𝑒1, ⋯, 𝑒𝑛 ∈ 𝔈∗Γ be pairwise independent and applied in order from 𝛾0. Write 𝑓𝑖 ≔ pr1 ∘ 𝑒𝑖, let 𝛿𝑖 ≔ 𝑓𝑖(𝛿𝑖−1) with 𝛿0 ≔ 𝛾0, and let 𝑔𝑖 ≔ pr2(𝑒𝑖(𝛿𝑖−1)) be the inverse 𝑒𝑖 yields where it is applied. Fix 𝑗 and write 𝛿′𝑖 ≔ (𝑓𝑖 ∘ ⋯ ∘ 𝑓𝑗+1)(𝛿𝑗−1) for the states of the sequence with 𝑒𝑗 omitted, so that 𝛿′𝑗 = 𝛿𝑗−1. Then for every 𝑢 with 𝑗 ≤ 𝑢 ≤ 𝑛,

中文翻译

定理 20. 设 𝑒1, ⋯, 𝑒𝑛 ∈ 𝔈∗Γ 成对独立并从 𝛾0 起按序施加。记 𝑓𝑖 ≔ pr1 ∘ 𝑒𝑖，令 𝛿𝑖 ≔ 𝑓𝑖(𝛿𝑖−1) 且 𝛿0 ≔ 𝛾0，并令 𝑔𝑖 ≔ pr2(𝑒𝑖(𝛿𝑖−1)) 为 𝑒𝑖 在其施加处所产的逆。固定 𝑗，记 𝛿′𝑖 ≔ (𝑓𝑖 ∘ ⋯ ∘ 𝑓𝑗+1)(𝛿𝑗−1) 为省略 𝑒𝑗 的序列的状态，故 𝛿′𝑗 = 𝛿𝑗−1。则对每个满足 𝑗 ≤ 𝑢 ≤ 𝑛 的 𝑢，

𝑔𝑗(𝛿𝑢) = (𝑔𝑗 ∘ 𝑓𝑢 ∘ ⋯ ∘ 𝑓𝑗+1)(𝛿𝑗) = (𝑓𝑢 ∘ ⋯ ∘ 𝑓𝑗+1)(𝑔𝑗(𝑓𝑗(𝛿𝑗−1))) = 𝛿′𝑢
最后等式依赖 𝑔𝑗(𝑓𝑗(𝛿𝑗−1)) = 𝛿𝑗−1，即定义 8 对 𝑒𝑗 在 𝛿𝑗−1 处所要求的见证。

详细解释

（证明梗概：第1部分第一式用交换性把 f_j 穿过后续 f_{j+1}…f_u，归纳得 δ_u = f_j(δ’u)——即"含 e_j 的状态"等于"省略 e_j 的状态"再做 f_j；第二式用交换性把 g_j 穿过后续前向，再用见证 g_j(f_j(δ{j-1}))=δ_{j-1} 得 g_j(δ_u)=δ’_u——即撤掉 e_j 后到达省略序列的状态。第2部分由条款2，e_j 的变换不扰动 e_i 产的逆，故 e_i 在被 e_j 搬动的状态处仍产相同的 g_i。）这个定理是独立性的核心回报，它精确刻画了"撤回一个效应"会到达哪里：

• 条款1：在"含 e_j 的完整序列"到达的状态 δ_u 处施加 e_j 的逆 g_j，会到达"省略 e_j 的序列"所到达的状态 δ’_u。换句话说，撤回 e_j 等价于"e_j 从未发生过"——这正是"干净撤回"的语义：撤下一个组件后，环境就是"这个组件从没加载过"的样子，无论它之后还有多少其他组件的效应在位。
• 条款2：撤回 e_j 后，其他组件 e_i (i>j) 在新状态处仍产出与原来相同的逆 g_i。这意味着"撤回 e_j 不影响其他组件的撤销能力"——可以继续撤回任何其他组件，它们的逆仍然有效。

两条合起来，使得"撤回 e_j"后，剩下的系统就像"从未加载过 e_j"一样，可以继续按任何顺序撤回剩余组件。这就是推论 21（任意顺序撤回都回到初始态）的基础。工程上，这保证了"从运行系统热卸载任意一个插件，其余插件状态正确、且各自仍能被正确卸载"——动态插件架构、微前端卸载、运行时模块替换的理论根基。

Corollary 21 (推论 21) — 任意置换顺序撤回都回到初始态

原文 (English)

Corollary 21. Let 𝑒1, ⋯, 𝑒𝑛 ∈ 𝔈∗Γ be pairwise independent and applied in order from 𝛾0, and let 𝑔1, ⋯, 𝑔𝑛 be as above. Applying the 𝑛 inverses at 𝛿𝑛 in the order of any permutation of {1, ⋯, 𝑛} reaches 𝛾0.
Proof. By downward induction on 𝑛. Let the permutation begin with 𝑗. By Theorem 20(1) applying 𝑔𝑗 at 𝛿𝑛 reaches 𝛿′𝑛, the state the sequence with 𝑒𝑗 omitted reaches, and by Theorem 20(2) the inverses the remaining effects yielded there are the 𝑔𝑖 in hand. That sequence is pairwise independent, being a subfamily, so the induction hypothesis applies to it and to the rest of the permutation; the empty sequence reaches 𝛾0. □
LIFO order is one such permutation, and Theorem 16 reverts in it with no hypothesis at all. What independence buys is every other order, and with it the sequence that interleaves several components, which Section 4.4.2 carries to a whole system’s trace.

中文翻译

推论 21. 设 𝑒1, ⋯, 𝑒𝑛 ∈ 𝔈∗Γ 成对独立并从 𝛾0 起按序施加，𝑔1, ⋯, 𝑔𝑛 如上。在 𝛿𝑛 处按 {1, ⋯, 𝑛} 的任意置换顺序施加这 𝑛 个逆，都到达 𝛾0。
证明. 对 𝑛 向下归纳。设置换以 𝑗 开头。由定理 20(1) 在 𝛿𝑛 处施加 𝑔𝑗 到达 𝛿′𝑛，即省略 𝑒𝑗 的序列所到达的状态，而由定理 20(2) 其余效应在那处所产的逆正是手上的 𝑔𝑖。该序列作为子族仍成对独立，故归纳假设适用于它及置换的剩余部分；空序列到达 𝛾0。 □
LIFO 顺序是这样一个置换，而定理 16 在其中撤销且无需任何假设。独立性所买到的是所有其他顺序，以及随之而来的多个组件效应交织的序列，第 4.4.2 节将其推广到整个系统的轨迹。

详细解释

（证明梗概：对置换长度向下归纳。置换第一个撤的是 g_j，由定理 20(1) 到达"省略 e_j 的状态"，由定理 20(2) 剩余效应在那里仍产手中的 g_i；剩余是成对独立的子族，归纳假设适用，递归到底即回到 γ0。）这个推论是独立性章节的高潮结论：在成对独立的前提下，撤回 n 个效应的顺序可以是 {1,…,n} 的任意置换，最终都回到初始状态 γ0。

对比定理 16（LIFO 撤销无需任何假设）和推论 21（任意顺序需独立性）：

• LIFO 是"免费"的——天然配对，每个逆作用于自己产生的状态，不需要任何额外条件。
• 任意顺序 是独立性"买到"的——允许先撤中间某个、再撤后面的、再撤前面的，任意穿插。这覆盖了"多组件效应交织"的真实场景：A 的效应、B 的效应、A 的效应交替出现，卸载时可能按任意顺序撤回各自的效应。

工程意义极其重要：在动态组合的系统里，组件的加载/卸载顺序往往不可预测（用户可能先关 A 再关 B，或先关 B 再关 A，或热替换某个）。只要各组件效应成对独立，无论以什么顺序卸载，系统都能正确回到干净状态。这是"时空可组合性"中"时间"维度的完整保证——不仅是"能撤销"，更是"以任意顺序撤销都正确"。第 4.4.2 节把这条推论推广到整个系统轨迹的全局时间可组合性。

3.1.3 小节收尾 — 可逆效应的总结与判据

原文 (English)

Together, these constructions constitute revertible effects: each effect function in 𝔈∗Γ explicitly provides its own inverse, effect tracks these inverses on the effect context 𝜕Γ, and the ⋄ operation composes them while preserving revertibility. What they deliver is local temporal composability, local in that the guarantee is read of one component’s effects taken by themselves. We take that to be the following criterion: for every sequence of effect functions a component applies, the accumulator recovers the context it began at (Theorem 7), and reverting the sequence hands each inverse the state its own application ran against (Theorem 16). Loading a component is applying such a sequence and accumulating its inverses in 𝜑; unloading it is applying 𝜑.
Two things the criterion leaves out, and both arrive once several components are in play: reverting out of the order the accumulator imposes, and a sequence that interleaves the effects of others. Independence delivers them (Corollary 21), and it is a condition on the effects rather than a property of the construction, Section 3.3.2 being where the discipline that meets it is identified and Section 4.4.2 where the guarantee is read of a whole system’s trace. Where independence fails, the order has to be carried elsewhere: within one component by the accumulator, which reverts in LIFO order whatever the effects (Section 4.3.2), and across components by a declared coeffect, which orders one activation against another (Section 4.3.1).

中文翻译

合起来，这些构造构成可逆效应：𝔈∗Γ 中每个效应函数显式提供自己的逆，effect 在效应上下文 𝜕Γ 上追踪这些逆，而 ⋄ 运算在保持可逆性的前提下复合它们。它们所交付的是局部时间可组合性，"局部"在于该保证是就一个组件自身的效应而言的。我们把它作为如下判据：对一个组件施加的每条效应函数序列，累积器恢复它起步时的上下文（定理 7），而撤销该序列时把每个逆交给其自身应用时所针对的状态（定理 16）。加载一个组件就是施加这样一条序列并把其逆累积进 𝜑；卸载它就是施加 𝜑。
判据漏掉两件事，而两者都在多个组件同场时才出现：按累积器所施顺序之外的顺序撤销，以及与其他组件效应交织的序列。独立性交付这两者（推论 21），且它是施加于效应之上的条件而非构造本身的性质，第 3.3.2 节确定满足它的纪律，第 4.4.2 节把保证读自整个系统的轨迹。当独立性失败时，顺序须由别处承载：组件内由累积器承载，无论效应如何都按 LIFO 顺序撤销（第 4.3.2 节）；组件间由声明的协效应承载，把一个激活与另一个激活排序（第 4.3.1 节）。

详细解释

这段是 3.1 节的总结陈词，明确划定了"局部时间可组合性"的判据边界：

• 判据（已达成）：单组件视角下，(1) 累积器能恢复初始上下文（定理 7）；(2) 反序撤销让每个逆作用于自己应用时的状态（定理 16）。加载=施加效应序列并累积逆，卸载=施加累积器 φ。
• 判据之外（需多组件才出现）：(1) 非累积器顺序（非 LIFO）的撤销；(2) 多组件效应交织的序列。这两者靠"独立性"解决（推论 21），但独立性是对效应的条件（开发者/接口设计者的责任），不是构造自动给的。

论文诚实地指出：当独立性不成立时（即两个效应操作顺序敏感的同一资源，如共享有序链表），顺序不能由效应机制自动处理，必须由"别处"承载——组件内靠累积器强制 LIFO，组件间靠协效应声明来排序。这把"时间可组合性"的局限和补救都说清楚了：效应机制保证局部可逆；全局顺序敏感的部分交给协效应（3.2 节）。

这是一种分层负责的清晰设计哲学：效应管"可逆"（能撤），协效应管"顺序"（该先谁后谁），两者分工。第 3.3.2 节会给出"什么接口设计能满足独立性"的纪律（交换键、可交换操作），第 4 章给出全局语义。工程上，这提示开发者：把可交换的资源（路由表、监听器集合）设计为独立效应可任意穿插撤回；把顺序敏感的资源（中间件链）设计为协效应，由依赖声明强制顺序。

3.2. Reactive Coeffects / 反应式协效应

原文 (English)

Spatial composability is the ability for components to declare dependencies on one another and for the system to resolve, provide, and withdraw those dependencies at runtime. This requires that dependency satisfaction be re-evaluated whenever the shared context changes, so that a component activates when its dependencies become available and deactivates when they are withdrawn. We therefore model dependencies of a component as a specification and classify each change to the context, against that specification, as activating, deactivating, or neutral. Classifying against the specification is what detects a change in satisfaction; responding to that classification is what drives activation and deactivation. We call such coeffects reactive: by classifying context changes and driving activation and deactivation from them, correct coeffect ordering becomes a structural guarantee.

中文翻译

空间可组合性（spatial composability）是指组件能够彼此声明依赖、并由系统在运行时解析、提供和撤回这些依赖的能力。这要求每当共享上下文变化时都重新评估依赖的满足性，使得组件在其依赖可用时激活、在依赖被撤回时停用。因此我们把组件的依赖建模为一个规约（specification），并针对该规约把对上下文的每次变化分类为激活（activating）、停用（deactivating）或中性（neutral）。针对规约分类正是检测满足性的变化；对该分类做出响应正是驱动激活与停用。我们把这样的协效应称为反应式的（reactive）：通过分类上下文变化并据此驱动激活与停用，正确的协效应排序成为一种结构性保证。

详细解释

3.2 节转向"空间"维度。核心思想：组件不直接引用彼此，而是声明依赖（“我需要 key k 的某个值”），由系统在运行时解析依赖、提供值、并在依赖撤回时停用组件。这本质是依赖注入（DI/IoC）的形式化，但加了"反应式"——依赖满足性随上下文变化而动态重评估。

机制是"分类驱动"：每次上下文变化（一次效应），系统针对某组件的依赖规约分类这次变化——是"让依赖从不满足变满足"（激活）、“从满足变不满足”（停用）、还是"不影响满足性"（中性）。激活时执行组件效应（带完整追踪），停用时施加累积器恢复。这样"组件何时启停"由数据流自动决定，而非由开发者手动编排顺序。

“反应式"是关键修饰词：传统 DI 是"启动时一次性注入”，而 Cordis 的协效应是"运行时持续监听依赖变化并动态启停"。这对应 React 的依赖数组、Vue 的响应式、Spring 的 @Autowired 但更强——依赖可动态增删，组件随之自动激活停用。所谓"结构性保证"指：组件启停顺序由依赖满足性自动决定，不需要开发者手动排"先启 A 再启 B"——只要 B 依赖 A 提供的 key，系统自然先让 A 激活、提供 key、再让 B 激活。

3.2.1. Coeffect Context / 协效应上下文

原文 (English)

Traditional inversion-of-control (IoC) containers [38] typically model dependencies as simple key-value mappings. This section formalizes IoC as a coeffect context that synergizes with revertible effects to provide a mathematical foundation for dynamic composition.

中文翻译

传统控制反转（IoC）容器 [38] 通常把依赖建模为简单的键值映射。本节把 IoC 形式化为一个协效应上下文（coeffect context），它与可逆效应协同，为动态组合提供数学基础。

详细解释

开宗明义：协效应上下文就是 IoC 容器的形式化。传统 IoC（Spring、Angular DI 等）把依赖存成"key → value"的字典，组件按 key 取依赖。Cordis 把这个字典形式化为类型 Σ，并让它与可逆效应机制协同——关键协同点在于：注册/撤回一个依赖本身就是一个效应（带逆），所以依赖的增删自动可逆，组件卸载时其注册的依赖自动被撤回。这是 3.1（效应可逆）与 3.2（协效应依赖）的接合点，论文称之为"synergy（协同）"。

Definition 22 (定义 22) — Coeffect Context Σ / 协效应上下文

原文 (English)

Definition 22. Given a type family 𝒱︀ : 𝐾 → Type, define the coeffect context as the dependent partial function type:
Σ ≔ (𝑘 : 𝐾) ⇀ 𝒱︀𝑘 (20)
where 𝜎 : Σ is a finite partial function assigning to each 𝑘 ∈ dom(𝜎) ⊆ 𝐾 a value of type 𝒱︀𝑘. We write:
• 𝜎(𝑘) for application (defined when 𝑘 ∈ dom(𝜎));
• 𝜎[𝑘 ↦ 𝑣] for the table binding 𝑣 at 𝑘 and agreeing with 𝜎 elsewhere;
• 𝜎 ∖ 𝑘 for restriction (defined when 𝑘 ∈ dom(𝜎));
• 𝑘 ∈ dom(𝜎) for membership.
The use of a type family 𝒱︀ ensures that each dependency key 𝑘 is associated with a specific value type 𝒱︀𝑘, providing static type safety for dependency access. Extension and restriction carry preconditions, imposed by the operations below: a dependency cannot be provided twice (𝑘 ∉ dom(𝜎) for extension) nor revoked if absent (𝑘 ∈ dom(𝜎) for restriction). A violated precondition is signalled as an error and produces no transition, so the effect algebra, which describes the transitions that do occur, applies to these operations unchanged. A reader preferring to internalize the failure may read every Σ ⇀ Σ below as Σ → 𝖬𝖺𝗒𝖻𝖾(Σ) and compose in the 𝖬𝖺𝗒𝖻𝖾 monad (Section 2.1), at the cost of replacing each identity by the partial identity on the operation’s domain.

中文翻译

定义 22. 给定类型族 𝒱︀ : 𝐾 → Type，定义协效应上下文为依赖偏函数类型：

Σ ≔ (𝑘 : 𝐾) ⇀ 𝒱︀𝑘　(20)
其中 𝜎 : Σ 是一个有限偏函数，给每个 𝑘 ∈ dom(𝜎) ⊆ 𝐾 赋一个类型为 𝒱︀𝑘 的值。我们记：
• 𝜎(𝑘) 为应用（在 𝑘 ∈ dom(𝜎) 时有定义）；
• 𝜎[𝑘 ↦ 𝑣] 为在 𝑘 处绑定 𝑣、其余与 𝜎 一致的表；
• 𝜎 ∖ 𝑘 为限制（在 𝑘 ∈ dom(𝜎) 时有定义）；
• 𝑘 ∈ dom(𝜎) 为成员关系。
使用类型族 𝒱︀ 确保每个依赖键 𝑘 关联一个特定的值类型 𝒱︀𝑘，为依赖访问提供静态类型安全。扩展与限制带有前置条件，由下文的运算施加：依赖不能被提供两次（扩展要求 𝑘 ∉ dom(𝜎)），也不可在缺失时撤销（限制要求 𝑘 ∈ dom(𝜎)）。被违反的前置条件报为错误且不产生任何迁移，故描述确实发生的迁移的效应代数对这些运算不变地适用。偏好把失败内化的读者，可把下文每个 Σ ⇀ Σ 读作 Σ → 𝖬𝖺𝗒𝖻𝖾(Σ) 并在 𝖬𝖺𝗒𝖻𝖾 幺半群中复合（第 2.1 节），代价是把每个恒等换成该运算定义域上的偏恒等。

详细解释

Σ 是一个依赖类型的有限偏映射：键集 K，每个键 k 对应一个特定类型 𝒱_k 的值。这比普通键值字典更强——它是 dependent type，键决定了值的类型，所以 σ(k) 的类型在编译期就确定，访问依赖有静态类型安全（不会取到类型不符的值）。这正是 IoC 容器理想的形式：注册 Logger 接口，取出来就是 Logger 类型，无需运行时转型。

两个核心操作带前置条件：

• 扩展 σ[k ↦ v]：要求 k ∉ dom(σ)——同一 key 不能被注册两次。这防止两个组件同时提供同一个依赖造成的歧义。
• 限制 σ ∖ k：要求 k ∈ dom(σ)——不能撤销不存在的依赖。

违反前置条件时报错且不产生状态迁移。论文特别说明：因为"确实发生的迁移"都满足前置条件，所以 3.1 的效应代数（track/recover/⋄）对这些操作原封不动适用——错误路径不进入效应代数。偏好严格形式的读者可把所有 Σ ⇀ Σ 读成 Σ → Maybe(Σ)（用 Maybe 幺半群复合），把"前置条件不满足"内化为返回 Nothing。这给了两种等价视角：乐观的（只看成功路径，用偏函数）和严格的（用 Maybe 显式处理失败）。工程上，这对应 IoC 容器的"重复注册报错""注销不存在的报错"行为，以及 TypeScript/Scala 中 DI 的类型安全取值。

Definition 23 (定义 23) — get / set 运算

原文 (English)

Definition 23. The get and set operations on Σ are:
get : (𝑘 : 𝐾) → Σ ⇀ 𝒱︀𝑘
get = 𝑘 ↦ 𝜎 ↦ 𝜎(𝑘)
set : (𝑘 : 𝐾) × 𝒱︀𝑘 → Σ ⇀ Σ × (Σ ⇀ Σ)
set = (𝑘, 𝑣) ↦ 𝜎 ↦ (𝜎[𝑘 ↦ 𝑣], 𝜆𝜎′.𝜎′ ∖ 𝑘) (21)
where get(𝑘) requires 𝑘 ∈ dom(𝜎) and set(𝑘, 𝑣) requires 𝑘 ∉ dom(𝜎) as preconditions.
Notably, set(𝑘, 𝑣) has type 𝔈∗Σ, precisely an effect function on the coeffect context. We can therefore directly apply the effect machinery from Section 3.1: effectΣ provides automatic tracking and recovery of dependency registrations. This is the synergy between reactive coeffects and revertible effects: coeffect operations are effects, and effects are revertible.

中文翻译

定义 23. Σ 上的 get 与 set 运算为：

get : (𝑘 : 𝐾) → Σ ⇀ 𝒱︀𝑘
get = 𝑘 ↦ 𝜎 ↦ 𝜎(𝑘)
set : (𝑘 : 𝐾) × 𝒱︀𝑘 → Σ ⇀ Σ × (Σ ⇀ Σ)
set = (𝑘, 𝑣) ↦ 𝜎 ↦ (𝜎[𝑘 ↦ 𝑣], 𝜆𝜎′.𝜎′ ∖ 𝑘)　(21)
其中 get(𝑘) 要求 𝑘 ∈ dom(𝜎)、set(𝑘, 𝑣) 要求 𝑘 ∉ dom(𝜎) 作为前置条件。
值得注意的是，set(𝑘, 𝑣) 的类型是 𝔈∗Σ，正是协效应上下文上的一个效应函数。因此我们可直接套用第 3.1 节的效应机制：effectΣ 提供依赖注册的自动追踪与恢复。这就是反应式协效应与可逆效应之间的协同：协效应运算是效应，而效应是可逆的。

详细解释

两个基本运算：

• get(k)：读 key k 的值（纯读，无副作用），要求 k 已注册。
• set(k, v)：注册 key k 为值 v，返回新表 σ[k↦v] 以及一个逆函数 λσ'.σ'∖k（把任意表的 k 删掉）。注意 set 的类型 Σ ⇀ Σ × (Σ ⇀ Σ) 正是 𝔈*Σ（效应函数）——它返回新状态 + 逆。

这是全章关键的协同点：set（注册依赖）是一个效应函数，于是它自动获得 3.1 的全部可逆机制——effectΣ 会追踪它的逆，组件卸载时逆（删 k）自动施加，依赖被自动撤回。论文用一句话点睛：“协效应运算是效应，而效应是可逆的”。这意味着依赖的注册和撤回不需要单独写清理代码——注册即追踪，卸载即撤回，由效应机制统一处理。

这是 Cordis 设计的优美之处：把 DI 的"注册/注销"纳入效应系统，于是 DI 容器的"组件卸载时自动注销其提供的依赖"成了数学保证，而非框架的额外约定。工程上，ctx.provide(k, v) 注册依赖、组件卸载时框架自动撤回 k，无需开发者在 cleanup 里手写"删除我注册的依赖"——这正是 set 作为 𝔈*Σ 带来的自动性。

Definition 24 (定义 24) — Coeffect at a Key / 键上的协效应（三元组）

原文 (English)

Definition 24. A coeffect at a key 𝑘 is a triple (𝒱︀𝑘, ≃𝑘 , 𝒜︀𝑘), where 𝒱︀𝑘 is the value type of Definition 22, ≃𝑘 is an equivalence relation on 𝒱︀𝑘 up to which values at 𝑘 are compared (Section 3.3.2), and 𝒜︀𝑘 is a set of coeffect operations, the operations the value bound at 𝑘 provides to a component holding it. An operation 𝑎 ∈ 𝒜︀𝑘 carries an argument type 𝑋𝑎 and an outcome type 𝐵𝑎, and acts on the value alone:
𝑎 : 𝑋𝑎 → 𝒱︀𝑘 ⇀ 𝒱︀𝑘 × (𝒱︀𝑘 ⇀ 𝒱︀𝑘) × 𝐵𝑎 (22)
its first two constituents forming an effect function on 𝒱︀𝑘 witnessed as Definition 8 requires, and its third an outcome. Each operation is required to respect ≃𝑘: at ≃𝑘-related values it is defined at both or at neither, and where defined it yields ≃𝑘-related successors, inverses that again carry ≃𝑘-related values to ≃𝑘-related values, and equal outcomes. An operation acts on the coeffect context through its lift
𝑎Σ(𝑥)(𝜎) ≔ let (𝑣, 𝑔, 𝑏) = 𝑎(𝑥)(𝜎(𝑘)) in (𝜎[𝑘 ↦ 𝑣], 𝜆𝜎′.𝜎′[𝑘 ↦ 𝑔(𝜎′(𝑘))], 𝑏) (23)
defined when 𝑘 ∈ dom(𝜎), whose first two constituents are an effect function on Σ.

中文翻译

定义 24. 键 𝑘 处的协效应是一个三元组 (𝒱︀𝑘, ≃𝑘 , 𝒜︀𝑘)，其中 𝒱︀𝑘 是定义 22 的值类型，≃𝑘 是 𝒱︀𝑘 上的等价关系，键 𝑘 处的值按它比较（第 3.3.2 节），𝒜︀𝑘 是一组协效应运算，即绑定在 𝑘 处的值提供给持有它的组件的运算。一个运算 𝑎 ∈ 𝒜︀𝑘 带有参数类型 𝑋𝑎 和结果类型 𝐵𝑎，并只作用于该值：

𝑎 : 𝑋𝑎 → 𝒱︀𝑘 ⇀ 𝒱︀𝑘 × (𝒱︀𝑘 ⇀ 𝒱︀𝑘) × 𝐵𝑎　(22)
其前两个分量构成 𝒱︀𝑘 上如定义 8 所要求的带见证效应函数，第三个是结果。每个运算要求尊重 ≃𝑘：在 ≃𝑘 相关的值处它要么都有定义要么都无定义，且在有定义处产出 ≃𝑘 相关的后继、把 ≃𝑘 相关的值映到 ≃𝑘 相关值的逆、以及相等的结果。一个运算通过其提升作用于协效应上下文：
𝑎Σ(𝑥)(𝜎) ≔ 令 (𝑣, 𝑔, 𝑏) = 𝑎(𝑥)(𝜎(𝑘)) ；得 (𝜎[𝑘 ↦ 𝑣], 𝜆𝜎′.𝜎′[𝑘 ↦ 𝑔(𝜎′(𝑘))], 𝑏)　(23)
在 𝑘 ∈ dom(𝜎) 时有定义，其前两个分量是 Σ 上的效应函数。

中文翻译（续说明）

一个键不止承载一个值类型，还承载：(1) 一个用于比较该值的等价关系 ≃_k（3.3.2 节用于观测等价）；(2) 一组运算 𝒜_k——绑定在该键的值"提供给持有者"能做什么。每个运算接收参数、作用于值、返回"新值 + 值上的逆 + 一个结果"。前两者是值层面的小效应函数（带见证），第三个是运算的结果（如查询返回的数据）。运算必须尊重等价关系 ≃_k。提升 aΣ 把"值层面"的运算抬到"上下文层面"——读取 σ(k)、运算、写回新值、并生成上下文层面的逆。

详细解释

这个定义把"一个依赖"从"一个值"升级为"一个带接口的对象"：键 k 不仅存一个值，还声明了 (1) 这个值怎么比较相等（≃_k，为 3.3.2 的观测等价铺路）；(2) 这个值提供哪些操作（𝒜_k，类似对象的方法集）。每个操作 a 的签名 X_a → 𝒱_k ⇀ 𝒱_k × (𝒱_k ⇀ 𝒱_k) × B_a 揭示了三层结构：

• 接收参数 x : X_a；
• 作用于值 v : 𝒱_k，返回新值 + 值上的逆 + 结果 b : B_a——前两个是值层面的可逆效应函数，第三个是操作的"返回值"（如读操作返回的数据）。

关键：操作本身也是可逆的——它返回值上的逆，所以操作可被追踪和撤销。这把"可逆性"从"上下文层"下沉到"值层"——不仅注册/注销依赖可逆，连对依赖值的操作也可逆。提升 aΣ 把值层操作抬到上下文层：读 σ(k)、操作得新值、写回 σ[k↦v]、生成上下文逆（“把任意 σ’ 的 k 处值用 g 变换”）。这样值层操作的逆也进入效应累积器，组件卸载时自动撤销。

“尊重 ≃_k"的要求是 3.3.2 的伏笔：操作的语义必须在等价类上良定义——相等的值操作后仍相等、产出相等的逆和结果。这保证后续用 ≃ 商化时操作语义不塌陷。工程上，这对应"依赖注入的对象不仅有值，还有方法 API，且方法调用是可逆的”——比如注入一个 Database 依赖，它的 query/update 操作都带逆（update 的逆是反向 update），整个调用链可回滚。

3.2.2. Specification and Notification / 规约与通知

原文 (English)

The preceding definitions describe how individual dependencies are registered and accessed. Accessing an absent dependency, however, is a runtime failure. A component should therefore activate only once all the dependencies it declares are present, rather than accessing them optimistically and failing when one is missing. This raises two questions: whether a component’s declared dependencies are jointly satisfied, and how the system should respond when that status changes. The coeffect context Σ carries a natural observational structure that makes both questions tractable: for any coeffect specification 𝑑 ⊆ 𝐾, define the satisfaction predicate:
𝜎 ⊧ 𝑑 ≔ ∀𝑘 ∈ 𝑑. 𝑘 ∈ dom(𝜎) (24)
This predicate is decidable (since dom(𝜎) is finite). Since all mutations to 𝜎 pass through effect functions (whose inverses recover the previous domain), changes to satisfaction are detectable at each effect boundary. This is the algebraic basis of reactivity: the effect system guarantees that every coeffect change is observed.

中文翻译

前面的定义描述了单个依赖如何被注册与访问。然而访问一个缺失的依赖是运行时失败。因此组件应只在其声明的所有依赖都存在时才激活，而不是乐观地访问、在缺失时才失败。这引出两个问题：组件声明的依赖是否被联合满足？当该状态变化时系统应如何响应？协效应上下文 Σ 带有一个自然的观测结构，使两个问题都可处理：对任何协效应规约 𝑑 ⊆ 𝐾，定义满足谓词：

𝜎 ⊧ 𝑑 ≔ ∀𝑘 ∈ 𝑑. 𝑘 ∈ dom(𝜎)　(24)
该谓词可判定（因 dom(𝜎) 有限）。由于对 𝜎 的所有修改都经过效应函数（其逆恢复先前定义域），满足性的变化在每个效应边界都可被检测。这就是反应性的代数基础：效应系统保证每个协效应变化都被观测。

详细解释

这段解决"何时激活组件"的问题。直觉：组件声明"我需要依赖 {k1, k2, k3}“，只有当这些 key 全部存在于 Σ 时，组件才能安全激活（否则访问缺失依赖会运行时报错）。满足谓词 σ ⊧ d 就是"声明集 d 的所有 key 都在 σ 的定义域里”——一个简单的子集检查，因 dom(σ) 有限而可判定。

反应性的代数基础在这句：“所有对 σ 的修改都经过效应函数，所以满足性的变化在每个效应边界可被检测”。因为 set（注册 k）和其逆（删 k）都是效应，每次效应施加后，系统都能重新计算 σ ⊧ d 是否成立，从而发现"依赖从缺失变满足"（激活）或"从满足变缺失"（停用）。效应系统的"可追踪性"（每个变化都被记录）直接转化为协效应的"可观测性"（每个依赖变化都被察觉）——这是 3.1 与 3.2 协同的第二层：效应的可追踪性支撑了协效应的反应性。

工程上：框架在每次依赖注册/注销（效应边界）后，重新评估所有组件的依赖满足性，自动激活新满足的、停用不再满足的。这是 React useEffect 依赖数组、Vue watch 响应式、Spring 上下文刷新的统一形式化——依赖变化触发组件生命周期，且因效应可逆，停用的组件能被干净回滚。

Definition 25 (定义 25) — Coeffect Specification 𝔇Σ / 协效应规约

原文 (English)

Definition 25. A coeffect specification is:
𝔇Σ ≔ 𝖲𝖾𝗍(𝐾) (25)
representing the set of dependencies a component declares from the environment.

中文翻译

定义 25. 协效应规约为：

𝔇Σ ≔ 𝖲𝖾𝗍(𝐾)　(25)
表示一个组件从环境声明的依赖集合。

详细解释

协效应规约就是一个 key 的集合——组件声明"我需要 d 里的所有 key"。形式上就是 K 的子集。这极其简洁：依赖声明就是"一个 key 集合"，满足性就是"这个集合 ⊆ dom(σ)"。没有复杂的规约语言，最小化但够用。后续（定义 30）拦截会扩展规约为带元数据的依赖映射，但基本形式就是集合。工程上对应 React 的依赖数组 [k1, k2, k3]、Angular 的构造函数参数类型列表——都是"我需要这些"的集合表示。

Definition 26 (定义 26) — notify 分类 / 通知分类

原文 (English)

Definition 26. Given a coeffect specification 𝑑 ⊆ 𝐾 and states 𝜎, 𝜎′ ∈ Σ, define:
notify𝑑(𝜎, 𝜎′) ≔
{ activating if 𝜎 ⊭ 𝑑 ∧ 𝜎′ ⊧ 𝑑
deactivating if 𝜎 ⊧ 𝑑 ∧ 𝜎′ ⊭ 𝑑
neutral otherwise (26)
This is well-defined because 𝜎 ⊧ 𝑑 is decidable and all state transitions are mediated by effect functions. The reactive invariant is: an activating transition triggers execution of the component’s effects (with full effect tracking), whereas a deactivating transition triggers recovery by applying the accumulator. The precise operational semantics of these transitions depend on their interaction with control flows, and are developed in Section 4.

中文翻译

定义 26. 给定协效应规约 𝑑 ⊆ 𝐾 和状态 𝜎, 𝜎′ ∈ Σ，定义：

notify𝑑(𝜎, 𝜎′) ≔
{ 激活（activating）　若 𝜎 ⊭ 𝑑 ∧ 𝜎′ ⊧ 𝑑
　停用（deactivating）　若 𝜎 ⊧ 𝑑 ∧ 𝜎′ ⊭ 𝑑
　中性（neutral）　　　其他　(26)
这是良定义的，因为 𝜎 ⊧ 𝑑 可判定且所有状态迁移都由效应函数中介。反应式不变式为：一次激活迁移触发组件效应的执行（带完整效应追踪），而一次停用迁移通过施加累积器触发恢复。这些迁移的精确操作语义取决于它们与控制流的交互，在第 4 章展开。

详细解释

notify_d(σ, σ') 把一次状态迁移（σ → σ’）针对规约 d 分类为三态：

• 激活：迁移前不满足（缺依赖）、迁移后满足——组件该启动；
• 停用：迁移前满足、迁移后不满足——组件该停止；
• 中性：满足性未变——不动作。

这把"依赖变化 → 组件启停"的形式化落到了一个三值分类函数上。反应式不变式规定了系统对每类的响应：激活→执行组件效应（带追踪，所以之后能回滚）；停用→施加累积器（撤销该组件所有效应）。中性→无操作。这是 3.2 节"反应式"的核心机制：分类驱动响应。

良定义性依赖两点：(1) 满足谓词可判定（dom 有限）；(2) 所有迁移经效应函数中介（所以每次迁移都有明确的 σ、σ’ 可比较）。第4章会给出这些迁移与控制流（异步、错误、并发）交互的精确操作语义。工程上，notify 对应框架的"依赖变化检测 → 触发 mount/unmount 生命周期"——检测到依赖变满足就 mount 组件（跑 setup effect），变不满足就 unmount（跑 cleanup）。

3.2.2 收尾 — 局部空间可组合性判据及其局限

原文 (English)

What set and notify deliver together is local spatial composability, local in the same sense as before, the guarantee being read of one component’s coeffects taken by themselves. We take that to be the following criterion: a component activates only at a state satisfying its specification, so it never reads a binding that is absent, and every change to the context is classified against that specification, so a loss of satisfaction is detected where it happens and drives a deactivation. Both halves are immediate from the definitions above, satisfaction being a precondition checked where the component would activate and notify𝑑 being defined at every transition.
The criterion covers one direction of the coeffect ordering and not the other. If component 𝐴 provides a key 𝑘 and component 𝐵 declares 𝑘 ∈ 𝑑𝐵, then 𝐵 can activate only after 𝐴 has activated and provided 𝑘, since 𝜎 ⊧ 𝑑𝐵 requires 𝑘 ∈ dom(𝜎). The converse fails: unloading 𝐴 removes 𝑘 from dom(𝜎) and so breaks 𝐵’s satisfaction, but a notification cannot by itself keep 𝑘 readable for as long as 𝐵’s own teardown needs it, nor hold 𝐴’s recovery back until 𝐵 has finished. Ordering a withdrawal after the deactivations it causes is a condition on other components rather than on the one acting, so it belongs to the global form of the guarantee, and Section 4.3.1 supplies the machinery it takes.

中文翻译

set 与 notify 合在一起交付的是局部空间可组合性，"局部"的含义同前，保证是就一个组件自身的协效应而言的。我们把它作为如下判据：组件只在一个满足其规约的状态处激活，故它从不读取缺失的绑定；且对上下文的每次变化都针对该规约分类，故满足性的丧失在发生处被检测并驱动停用。两半都直接来自上述定义——满足性是在组件将激活处检查的前置条件，而 notify𝑑 在每次迁移处有定义。
该判据覆盖协效应排序的一个方向，而非另一个。若组件 𝐴 提供键 𝑘 而组件 𝐵 声明 𝑘 ∈ 𝑑𝐵，则 𝐵 只能在 𝐴 激活并提供 𝑘 之后激活，因为 𝜎 ⊧ 𝑑𝐵 要求 𝑘 ∈ dom(𝜎)。反向不成立：卸载 𝐴 把 𝑘 从 dom(𝜎) 移除从而破坏 𝐵 的满足性，但通知本身无法在 𝐵 自身拆解所需的整个期间保持 𝑘 可读，也无法把 𝐴 的恢复推迟到 𝐵 完成之后。把一次撤回排在它所致的停用之后，是对其他组件的条件而非对正在行动的组件的条件，故它属于保证的全局形式，第 4.3.1 节提供所需的机制。

详细解释

这段划定了"局部空间可组合性"的判据和局限：

• 判据（已达成）：(1) 组件只在依赖满足时激活——永不访问缺失依赖（避免运行时错误）；(2) 每次上下文变化都分类——满足性丧失即被检测并触发停用。两者都直接由定义 25/26 得出。
• 覆盖的方向：依赖满足性强制了"提供者先于消费者激活"的顺序——B 依赖 A 提供的 k，所以 A 必须先激活（注册 k），B 才能满足。这是"激活顺序"的一个方向，是免费的。
• 未覆盖的方向：反向——“撤回 A 时，B 应先停用，A 的资源 k 在 B 停用前不能被撤”。通知能检测到"B 的满足性因 A 卸载而丧失"并触发 B 停用，但无法保证"A 的恢复（删 k）等到 B 停用完成之后"——这涉及跨组件的时序协调，是"对其他组件的条件"，属于全局保证，由第 4.3.1 节的机制处理。

这是诚实的能力边界声明：局部协效应机制保证"依赖满足才激活、丧失就停用"，但"卸载顺序的正确编排"（先停用依赖者、再撤回被依赖者）需要全局机制。工程上对应：DI 容器能自动按依赖图激活组件，但"优雅停机时按依赖逆序卸载"通常需要容器额外的事务/排序逻辑。第 4 章的 calculus 补全这部分。

3.2.3. Isolation and Interception / 隔离与拦截

原文 (English)

The basic coeffect context Σ models a flat dependency table. In practice, however, the system may need to bind distinct values to the same logical dependency for different components. This section extends the coeffect context with two mechanisms: coeffect isolation (the same key resolves differently in different contexts) and coeffect interception (cross-cutting behavior on dependency access).
Realization. The two mechanisms differ from get and set in what they act on. A provision writes the shared table every component reads, so it is an effect on that table and carries an inverse to withdraw it. Isolation and interception instead adjust how a key is resolved for the components under one context, leaving the table itself as it stands. Typing an operation as an effect fixes its denotation, a successor state paired with an inverse, but not its realization, which determines how that inverse is carried out.

中文翻译

基本协效应上下文 Σ 建模一个扁平的依赖表。然而在实践中，系统可能需要为不同组件把不同的值绑定到同一个逻辑依赖上。本节用两个机制扩展协效应上下文：协效应隔离（同一个键在不同上下文中解析不同）与协效应拦截（对依赖访问的横切行为）。
实现（Realization）。这两个机制与 get 和 set 在作用对象上不同。一次提供（provision）写入每个组件都读的共享表，所以它是该表上的一个效应，带一个逆以撤回它。隔离与拦截则调整"一个键对某上下文下的组件如何解析"，而让表本身保持原样。把一个运算类型化为效应，固定的是它的指称——一个后继状态配一个逆——而非它的实现，实现决定那个逆如何被执行。

详细解释

3.2.3 引入两个高级机制，应对扁平依赖表的局限。首先区分两类操作的作用对象：

• 提供（provision，即 set）：写共享表——所有组件都读的同一张表。它是效应，带逆（删 key），所以可逆、可追踪。
• 隔离/拦截：不写共享表，而是调整"键如何被解析"——为某个上下文下的组件派生出一个不同的解析视图，表本身不变。

论文引入"实现（realization）“概念区分效应的两种执行方式（见定义 27）。隔离和拦截被归为"派生实现”——它们产生一个派生上下文（fresh context deriving from the inherited one），而非修改共享表。因此它们不需要逆（没改共享表，没什么可撤回的），卸载时派生上下文被丢弃即可。这是它们与 set 的本质区别：set 是"真修改"（带逆、进累积器），隔离/拦截是"派生视图"（无逆、随上下文生命周期丢弃）。工程上，隔离类似"子作用域/子容器"，拦截类似"中间件/装饰器"——都不改原始注册表，只在特定作用域内改变解析行为。

Definition 27 (定义 27) — Two Realizations / 两种实现

原文 (English)

Definition 27. An effect function on a context admits two realizations:
• In-place realization mutates the context and returns a nontrivial inverse; the successor aliases the input, and recovery runs the inverse to undo the mutation.
• Derived realization leaves the input intact and returns a fresh context deriving from it, with the identity as its inverse; recovery discards the derived context. A context derived from another is what the recursive structure of Definition 32 carries.
In a purely functional setting the two coincide, and an imperative host may choose either per operation; Section 5.1.2 implements both. Isolation and interception are given derived realization outright: each produces a fresh context whose own table differs from the inherited one, so each is typed below as a map from context to context rather than as an effect function. Nothing in the shared table changes, so there is no inverse to track and nothing for Definition 12 to lift, and recovery discards the derived context along with the adjustment it carried. Assignment on a derived table overrides whatever the inherited table held at the key, which is why neither operation carries a precondition.

中文翻译

定义 27. 上下文上的一个效应函数容许两种实现：
• 原地实现（in-place realization）变异上下文并返回一个非平凡的逆；后继别名输入，恢复通过运行该逆撤销变异。
• 派生实现（derived realization）保持输入不变，返回一个从它派生的新鲜上下文，以恒等为逆；恢复丢弃该派生上下文。从一个上下文派生出的上下文正是定义 32 的递归结构所承载的。
在纯函数式环境下两者重合，命令式宿主可按运算选择其一；第 5.1.2 节实现两者。隔离与拦截径直采用派生实现：各自产出一个自有表与所继承表不同的新鲜上下文，故下文各自被类型化为从上下文到上下文的映射而非效应函数。共享表无任何改变，故无逆可追踪、无物可供定义 12 提升，且恢复随其所承载的调整一并丢弃派生上下文。派生表上的赋值覆盖继承表在该键处所持有的任何东西，这就是两个运算都不带前置条件的原因。

详细解释

两种"实现"区分效应如何被执行：

• 原地实现：真改上下文（如 set 注册依赖），返回非平凡逆，恢复时跑逆撤销。这是"可逆修改"的标准模式，进效应累积器。
• 派生实现：不改输入，返回一个"派生的新上下文"（继承父上下文但有自己的局部表），逆是恒等（因为没改父表，没什么可撤销的），恢复时直接丢弃派生上下文。这是"作用域视图"模式。

纯函数式下两者等价（不可变，所谓"修改"本来就是返回新值）；命令式宿主可按需选。隔离和拦截强制用派生实现——它们被类型化为 Σ → Σ（普通映射）而非效应函数，因为它们不改共享表，只是"在某个上下文下改变键的解析"，产出的是局部派生视图。卸载时派生视图被丢弃，共享表从未被动过。

"派生表上的赋值覆盖继承表"且无前置条件——因为派生表是局部的，覆盖不影响共享表，不存在"重复注册"的冲突。这给了隔离/拦截很大的灵活性：可以随时在派生作用域里重定义任何键。工程上，原地实现=全局单例容器的注册/注销；派生实现=创建子容器/子作用域，在子作用域里覆盖某些依赖，父容器不受影响，子作用域销毁时覆盖自动消失。

Definition 28 (定义 28) — Coeffect Context with Isolation Σiso / 带隔离的协效应上下文

原文 (English)

Definition 28. Define the coeffect context with isolation as:
Σiso ≔ (𝐾 ⇀ 𝑅) × ((𝑟 : 𝑅) ⇀ 𝒱︀𝑟) (27)
It can be represented as a pair (𝜌, 𝜎), where:
• 𝜌 : 𝐾 ⇀ 𝑅 is the isolation realm table, assigning a realm identifier to each isolated key; a key outside dom(𝜌) resolves to its own realm, so we write 𝜌(𝑘) = 𝑘 there (𝑅 ⊇ 𝐾);
• 𝜎 : (𝑟 : 𝑅) ⇀ 𝒱︀𝑟 is the dependency table, a partial dependent function from realm identifiers to typed values.
The two-layer mapping structure decouples the logical layer from the storage layer, making dependency access context-aware. When accessing a key 𝑘, the system first resolves 𝜌(𝑘) to obtain a realm identifier 𝑟, then accesses 𝜎(𝑟) for the actual value.

中文翻译

定义 28. 定义带隔离的协效应上下文为：

Σiso ≔ (𝐾 ⇀ 𝑅) × ((𝑟 : 𝑅) ⇀ 𝒱︀𝑟)　(27)
它可表示为一对 (𝜌, 𝜎)，其中：
• 𝜌 : 𝐾 ⇀ 𝑅 是隔离域表（isolation realm table），给每个被隔离的键赋一个域标识符；dom(𝜌) 之外的键解析到它自身的域，故在那里记 𝜌(𝑘) = 𝑘（𝑅 ⊇ 𝐾）；
• 𝜎 : (𝑟 : 𝑅) ⇀ 𝒱︀𝑟 是依赖表，一个从域标识符到类型化值的偏依赖函数。
两层映射结构把逻辑层与存储层解耦，使依赖访问具有上下文感知能力。访问键 𝑘 时，系统先解析 𝜌(𝑘) 得到域标识符 𝑟，再访问 𝜎(𝑟) 取实际值。

详细解释

隔离机制用两层映射实现"同一逻辑键在不同上下文解析到不同值"：

• 第一层 ρ : K ⇀ R（域表）：把逻辑键 k 映射到一个"域标识符 r"——即"k 在当前上下文里属于哪个域"。
• 第二层 σ : R ⇀ 𝒱_r（依赖表）：从域标识符 r 取实际值。

访问 k 时两步走：先 ρ(k) 得域 r，再 σ(r) 得值。这样同一个逻辑键 k，在不同上下文（不同 ρ 映射）下解析到不同域 r，从而取到不同的值。未在 ρ 中显式隔离的键 ρ(k)=k（解析到自身域），保持默认行为。

这本质是"键的重定向"——逻辑键不变，但通过域表重定向到不同的存储槽。论文称之为"运行时 ad-hoc 多态"：同一个键名在不同上下文有不同实现，且可运行时动态调整。应用场景：多租户系统（不同租户的 “UserService” 是不同实例）、测试环境（mock 替换真实依赖）、组件沙箱（隔离的依赖副本）。工程上类似 NestJS 的模块作用域、Angular 的分层注入器、Node.js 的模块隔离——同一 token 在不同作用域解析到不同 provider。

Definition 29 (定义 29) — get/set/isolate on Σiso / 隔离上下文上的运算

原文 (English)

Definition 29. The get, set, and isolate operations on Σiso are:
get : (𝑘 : 𝐾) → Σiso ⇀ 𝒱︀𝜌(𝑘)
get = 𝑘 ↦ (𝜌, 𝜎) ↦ 𝜎(𝜌(𝑘))
set : (𝑘 : 𝐾) × 𝒱︀𝜌(𝑘) → Σiso ⇀ Σiso × (Σiso ⇀ Σiso)
set = (𝑘, 𝑣) ↦ (𝜌, 𝜎) ↦ ((𝜌, 𝜎[𝜌(𝑘) ↦ 𝑣]), 𝜆(𝜌′, 𝜎′).(𝜌′, 𝜎′ ∖ 𝜌′(𝑘)))
isolate : 𝐾 × 𝑅 → Σiso → Σiso
isolate = (𝑘, 𝑟) ↦ (𝜌, 𝜎) ↦ (𝜌[𝑘 ↦ 𝑟], 𝜎) (28)
where get and set carry the preconditions of Definition 23 transported along 𝜌, namely 𝜌(𝑘) ∈ dom(𝜎) and 𝜌(𝑘) ∉ dom(𝜎). The context that isolate(𝑘, 𝑟) derives assigns the realm 𝑟 to 𝑘 and inherits the dependency table unchanged, so a key already isolated is reassigned rather than refused.
The coeffect isolation mechanism essentially implements a runtime ad-hoc polymorphism system. Through isolation realm identifiers, the same dependency key can resolve to entirely different values in different contexts, and this polymorphism can be dynamically adjusted at runtime. Compared to traditional dependency injection, coeffect isolation provides finer-grained control, enabling customized isolation for specific components; set remains an effect function (𝔈∗Σiso) and thus inherits revertibility, whereas isolate needs none, deriving a context instead of writing the shared table.

中文翻译

定义 29. Σiso 上的 get、set、isolate 运算为：

get : (𝑘 : 𝐾) → Σiso ⇀ 𝒱︀𝜌(𝑘)
get = 𝑘 ↦ (𝜌, 𝜎) ↦ 𝜎(𝜌(𝑘))
set : (𝑘 : 𝐾) × 𝒱︀𝜌(𝑘) → Σiso ⇀ Σiso × (Σiso ⇀ Σiso)
set = (𝑘, 𝑣) ↦ (𝜌, 𝜎) ↦ ((𝜌, 𝜎[𝜌(𝑘) ↦ 𝑣]), 𝜆(𝜌′, 𝜎′).(𝜌′, 𝜎′ ∖ 𝜌′(𝑘)))
isolate : 𝐾 × 𝑅 → Σiso → Σiso
isolate = (𝑘, 𝑟) ↦ (𝜌, 𝜎) ↦ (𝜌[𝑘 ↦ 𝑟], 𝜎)　(28)
其中 get 与 set 带有沿 𝜌 搬运的定义 23 的前置条件，即 𝜌(𝑘) ∈ dom(𝜎) 与 𝜌(𝑘) ∉ dom(𝜎)。isolate(𝑘, 𝑟) 所派生的上下文把域 𝑟 赋给 𝑘 并原样继承依赖表，故已被隔离的键是被重新赋值而非被拒绝。
协效应隔离机制本质上实现了一个运行时 ad-hoc 多态系统。通过隔离域标识符，同一个依赖键可在不同上下文中解析到完全不同的值，且此多态可在运行时动态调整。相比传统依赖注入，协效应隔离提供更细粒度的控制，能为特定组件定制隔离；set 仍是效应函数（𝔈∗Σiso）从而继承可逆性，而 isolate 无需逆，它派生上下文而非写共享表。

详细解释

三个运算：get/set 沿域表 ρ 搬运——所有访问都先经 ρ(k) 重定向到域 r，再操作 σ®。所以 set 注册的是"域 r 处的值"，逆是"删域 r"。isolate(k, r) 只改域表 ρ[k↦r]，不动依赖表 σ——它是派生实现（按定义 27），产出新上下文 （ρ[k↦r], σ），无逆（σ 没变），是 Σiso → Σiso 的普通映射而非效应函数。

关键对比：set 仍是效应函数 𝔈*Σiso，所以注册依赖可逆（进累积器，卸载自动撤回）；isolate 不是效应函数，它派生上下文，卸载时派生上下文被丢弃，域表调整随之消失。这种分工让"隔离"成为轻量、无副作用的视图操作，而"提供值"仍是可逆的真修改。已被隔离的键可被重新赋域（覆盖而非报错），因为 isolate 改的是派生上下文的域表，不影响共享表。

论文点明这是"运行时 ad-hoc 多态"——同一名字在不同上下文有不同实现，类比函数重载但运行时动态分派。相比传统 DI（一个 token 全局一个实现），隔离允许"按上下文定制实现"。工程上，这就是"为某个子树/某个测试用例注入 mock""为某个租户注入租户专属服务"的能力——通过 isolate 把键重定向到隔离域，再在该域 set 专属值。

Definition 30 (定义 30) — Coeffect Context with Interception Σinter / 带拦截的协效应上下文

原文 (English)

Definition 30. Define the coeffect context and specification with interception as:
Σinter ≔ ((𝑘 : 𝐾) → ℳ︀𝑘) × ((𝑘 : 𝐾) ⇀ (ℳ︀𝑘 → 𝒱︀𝑘))
𝔇inter ≔ (𝑘 : 𝐾) ⇀ ℳ︀𝑘 (29)
The context Σinter is a pair (𝜄, 𝜎): 𝜄 is the context-carried metadata installed on the context itself, empty (𝜖𝑘) by default; and 𝜎 maps each key 𝑘 to a provider function from metadata ℳ︀𝑘 to value 𝒱︀𝑘. A specification 𝑑 ∈ 𝔇inter carries the component-declared metadata, assigning each key its metadata 𝑑(𝑘), with dom(𝑑) serving as the dependency set. Each key equips its metadata with a monoid (ℳ︀𝑘, ⊕𝑘, 𝜖𝑘): the merge ⊕𝑘 is associative with identity 𝜖𝑘 (the empty metadata).

中文翻译

定义 30. 定义带拦截的协效应上下文与规约为：

Σinter ≔ ((𝑘 : 𝐾) → ℳ︀𝑘) × ((𝑘 : 𝐾) ⇀ (ℳ︀𝑘 → 𝒱︀𝑘))
𝔇inter ≔ (𝑘 : 𝐾) ⇀ ℳ︀𝑘　(29)
上下文 Σinter 是一对 (𝜄, 𝜎)：𝜄 是安装在上下文自身上的上下文携带元数据（context-carried metadata），默认为空（𝜖𝑘）；𝜎 把每个键 𝑘 映射到一个从元数据 ℳ︀𝑘 到值 𝒱︀𝑘 的提供者函数。规约 𝑑 ∈ 𝔇inter 承载组件声明的元数据，给每个键赋其元数据 𝑑(𝑘)，dom(𝑑) 充当依赖集。每个键为其元数据配备一个幺半群 (ℳ︀𝑘, ⊕𝑘, 𝜖𝑘)：合并 ⊕𝑘 结合且以 𝜖𝑘（空元数据）为单位。

详细解释

拦截机制给依赖访问附加"横切元数据"，不改变依赖值本身。上下文 Σinter = (ι, σ) 两部分：

• ι : K → ℳ_k：上下文携带的元数据——安装在上下文上的、对所有组件可见的"拦截配置"，默认空。比如全局的"日志级别"“权限上下文”“追踪 trace id”。
• σ : K ⇀ (ℳ_k → 𝒱_k)：提供者函数表——每个 key 不再直接存值，而是存一个"接收元数据、返回值"的函数。即提供者可以根据元数据动态决定返回什么值。

规约 𝔇inter 也升级：从"key 集合"变成"key → 组件声明元数据"的映射。组件声明"我需要 key k，并且我以元数据 d(k) 的方式使用它"。dom(d) 仍是依赖集。

每个 key 的元数据 ℳ_k 配备一个幺半群 (ℳ_k, ⊕_k, ϵ_k)——元数据可合并，合并结合、有空单位。这允许"上下文元数据"与"组件声明元数据"通过 ⊕_k 合并。工程上，拦截对应"依赖访问的中间件/装饰器"——比如给所有数据库访问附加"事务上下文"“读写权限”“审计标签”，这些是横切关注点，不改变数据库本身，但影响访问行为。元数据幺半群让多个拦截器可叠加（如多个权限标签取并集、多个日志级别取最高）。

Definition 31 (定义 31) — get/set/intercept on Σinter / 拦截上下文上的运算

原文 (English)

Definition 31. The get, set, and intercept operations on Σinter are:
get : (𝑘 : 𝐾) × ℳ︀𝑘 → Σinter ⇀ 𝒱︀𝑘
get = (𝑘, 𝜇) ↦ (𝜄, 𝜎) ↦ 𝜎(𝑘)(𝜇 ⊕𝑘 𝜄(𝑘))
set : (𝑘 : 𝐾) × (ℳ︀𝑘 → 𝒱︀𝑘) → Σinter ⇀ Σinter × (Σinter ⇀ Σinter)
set = (𝑘, 𝜓) ↦ (𝜄, 𝜎) ↦ ((𝜄, 𝜎[𝑘 ↦ 𝜓]), 𝜆(𝜄′, 𝜎′).(𝜄′, 𝜎′ ∖ 𝑘))
intercept : (𝑘 : 𝐾) × ℳ︀𝑘 → Σinter → Σinter
intercept = (𝑘, 𝜈) ↦ (𝜄, 𝜎) ↦ (𝜄[𝑘 ↦ 𝜄(𝑘) ⊕𝑘 𝜈], 𝜎) (30)
where get and set carry the preconditions of Definition 23 on the provider table, namely 𝑘 ∈ dom(𝜎) and 𝑘 ∉ dom(𝜎). The context that intercept(𝑘, 𝜈) derives merges 𝜈 onto the metadata inherited at 𝑘 and inherits the provider table unchanged.
When a component with specification 𝑑 accesses key 𝑘, the system evaluates 𝜎(𝑘)(𝑑(𝑘) ⊕𝑘 𝜄(𝑘)): the component-declared metadata is merged with the context-carried metadata 𝜄, and the provider function is applied to the result. This merge follows each key’s own semantics (e.g. scalar fields are overwritten, set-valued fields unioned) and is right-biased, so 𝜄(𝑘) takes priority and can override the component’s declaration, letting an enclosing context constrain how a component uses a coeffect without modifying that component (e.g. Section 6.3).

中文翻译

定义 31. Σinter 上的 get、set、intercept 运算为：

get : (𝑘 : 𝐾) × ℳ︀𝑘 → Σinter ⇀ 𝒱︀𝑘
get = (𝑘, 𝜇) ↦ (𝜄, 𝜎) ↦ 𝜎(𝑘)(𝜇 ⊕𝑘 𝜄(𝑘))
set : (𝑘 : 𝐾) × (ℳ︀𝑘 → 𝒱︀𝑘) → Σinter ⇀ Σinter × (Σinter ⇀ Σinter)
set = (𝑘, 𝜓) ↦ (𝜄, 𝜎) ↦ ((𝜄, 𝜎[𝑘 ↦ 𝜓]), 𝜆(𝜄′, 𝜎′).(𝜄′, 𝜎′ ∖ 𝑘))
intercept : (𝑘 : 𝐾) × ℳ︀𝑘 → Σinter → Σinter
intercept = (𝑘, 𝜈) ↦ (𝜄, 𝜎) ↦ (𝜄[𝑘 ↦ 𝜄(𝑘) ⊕𝑘 𝜈], 𝜎)　(30)
其中 get 与 set 带有定义 23 在提供者表上的前置条件，即 𝑘 ∈ dom(𝜎) 与 𝑘 ∉ dom(𝜎)。intercept(𝑘, 𝜈) 所派生的上下文把 𝜈 合并到 𝑘 处继承的元数据上，并原样继承提供者表。
当一个带规约 𝑑 的组件访问键 𝑘 时，系统求值 𝜎(𝑘)(𝑑(𝑘) ⊕𝑘 𝜄(𝑘))：组件声明的元数据与上下文携带的元数据 𝜄 合并，再把提供者函数作用于结果。该合并遵循每个键自身的语义（如标量字段被覆盖、集合值字段取并），且右偏，故 𝜄(𝑘) 优先，可覆盖组件的声明，让外层上下文在无需修改组件的前提下约束组件如何使用一个协效应（如第 6.3 节）。

详细解释

三个运算的关键在 get 的语义：访问 key k 时，不是直接取值，而是 σ(k)(d(k) ⊕_k ι(k))——把"组件声明的元数据 d(k)“与"上下文携带的元数据 ι(k)“用 ⊕_k 合并，再交给提供者函数 σ(k) 求值。所以最终取到的值取决于元数据的合并结果——元数据充当"访问参数”，提供者按参数返回不同值。这是拦截的核心：不改值，改"值如何被访问”。

合并 d(k) ⊕_k ι(k) 右偏——ι(k)（上下文元数据）优先，能覆盖 d(k)（组件声明）。这意味外层上下文可以"在不修改组件代码的前提下，约束组件如何使用依赖"——比如组件声明"我要以读写模式访问数据库"，但外层上下文通过拦截把元数据覆盖为"只读"，组件就被强制只读访问。这是强大的"横切控制"——不需要改组件，外层就能施加策略（权限降级、审计注入、性能限制）。

intercept(k, ν) 是派生实现（按定义 27），只改上下文元数据 ι[k↦ι(k)⊕_k ν]，不动提供者表 σ——合并新元数据 ν 到继承的 ι(k) 上。无逆（σ 没变），是 Σinter → Σinter 的普通映射。set 仍是效应函数（注册提供者函数，带逆删 k，可逆）。工程上，intercept 对应"为某子树注入拦截中间件"——如给某子树的所有数据库访问附加"事务边界"“权限标签”，外层上下文通过 intercept 覆盖组件的访问元数据，实现 AOP（面向切面编程）式的横切控制。

3.3. The Context Paradigm / 上下文范式

原文 (English)

Section 3.1 and Section 3.2 each act on a context, the first as the carrier of effects and the second as the carrier of coeffects, leaving open what a single context carrying both looks like. This section gives that unification a concrete construction, assembles from the coeffects an observational equivalence that supplies the effect independence Section 3.1.3 leaves open, and argues that the resulting context type constitutes a programming paradigm in its own right.

中文翻译

第 3.1 节与第 3.2 节各自作用于一个上下文，前者作为效应的载体、后者作为协效应的载体，留下"一个同时承载两者的单一上下文长什么样"未决。本节给该统一一个具体构造，从协效应组装出一个观测等价以提供第 3.1.3 节留下的效应独立性，并论证所得上下文类型本身就构成一种编程范式。

详细解释

3.3 节是全章也是全论文的范式主张所在。三件事：(1) 把效应上下文 ∂Γ 与协效应上下文 Σ 统一成单一类型 Γ∞；(2) 用协效应的观测等价 ≃ 来补全 3.1.3 留下的独立性条件（独立性是"对效应的条件"，谁来保证它成立？答案：用协效应的等价关系商化后，独立性变得可达）；(3) 论证这套统一上下文构成一种新编程范式。

这是从"两个机制"到"一个范式"的升维：3.1 给了可逆效应（时间），3.2 给了反应式协效应（空间），但它们若各自为政只是两个工具；3.3 把它们合为一个统一上下文，并证明这个合体能解决单独时无法解决的问题（独立性保证），于是"上下文"成为编程的一等范式——所有副作用、所有依赖都经此单一实体。这呼应论文标题"时空可组合性"——时间（效应）和空间（协效应）在统一上下文里合体。

3.3.1. Unified Context / 统一上下文

原文 (English)

For a context Γ, the effect context 𝜕Γ (Section 3.1) provides a higher-level abstraction, carrying the previous-level context and that level’s accumulator (Definition 2). Making this structure recursive and combining it with the coeffect context Σ yields the following type:
Definition 32. The context type Γ∞ is defined as:
Γ∞ ≔ 𝜇Γ. Γ × (Γ → Γ) × Σ (31)
where the three projections are:
• Γ: the current context state (recursive);
• Γ → Γ: the accumulator, which recovers this level’s effects;
• Σ: the coeffect context carrying dependency information.
Under this definition, effect maps 𝔈Γ∞ to itself, unifying the 𝜕-tower into a single self-similar type. The coeffect context Σ is structurally integrated: dependency operations (set, get) act on Σ, and the accumulator tracks their reversal. Since the type family 𝒱︀ underlying Σ is unconstrained, any state the system needs to share across components can be encoded as a dependency with an appropriate value type— Σ subsumes all shared mutable states, not just inter-component dependencies. Every interaction between a component and its environment passes through this single entity.
Hierarchical composition. The recursive structure of Γ∞ supports hierarchical control: a parent context aggregates multiple child-level effects, forming a tree-shaped control structure that maintains modularity while enabling unified cross-level management. The effect transformation realizes a literal “plug-in” metaphor:
• Loading a component corresponds to executing its effects (plugging in);
• Unloading a component corresponds to recovering its effects (unplugging, without affecting other running components);
• Components at different levels of the hierarchy are independently loadable and unloadable; a parent context aggregates and manages the effects of all its children, enabling arbitrarily nested composition.

中文翻译

对一个上下文 Γ，效应上下文 𝜕Γ（第 3.1 节）提供一个更高层抽象，承载上一层上下文及该层的累积器（定义 2）。使该结构递归并与协效应上下文 Σ 结合，得到如下类型：
定义 32. 上下文类型 Γ∞ 定义为：

Γ∞ ≔ 𝜇Γ. Γ × (Γ → Γ) × Σ　(31)
其三个投影为：
• Γ：当前上下文状态（递归）；
• Γ → Γ：累积器，恢复本层效应；
• Σ：承载依赖信息的协效应上下文。
在此定义下，effect 把 𝔈Γ∞ 映到自身，把 𝜕-塔统一为一个自相似类型。协效应上下文 Σ 被结构性地整合：依赖运算（set、get）作用于 Σ，累积器追踪其逆。由于 Σ 之下的类型族 𝒱︀ 不受约束，系统需要在组件间共享的任何状态都可编码为一个带适当值类型的依赖——Σ 囊括了所有共享可变状态，而不仅是组件间依赖。组件与其环境之间的每次交互都经此单一实体。
层级组合。Γ∞ 的递归结构支持层级控制：父上下文聚合多个子层效应，形成一个树状控制结构，在保持模块性的同时支持统一的跨层管理。效应变换实现了一个字面的"插拔"比喻：
• 加载一个组件对应执行其效应（插入）；
• 卸载一个组件对应恢复其效应（拔出，不影响其他运行中的组件）；
• 层级中不同层的组件可独立加载与卸载；父上下文聚合并管理其所有子级的效应，支持任意嵌套组合。

详细解释

定义 32 是全章构造的高潮：Γ∞ = μΓ. Γ × (Γ → Γ) × Σ 是一个递归不动点类型（μ 是最小不动点算子）。它把 ∂-塔（∂Γ、∂²Γ、…无穷堆叠）折成一个自相似的单一类型——每个 Γ∞ 节点包含三部分：

因为 Γ 递归地是 Γ∞ 自身，effect : 𝔈Γ∞ → 𝔈∂Γ∞ 实际上把 𝔈Γ∞ 映到自身（∂Γ∞ = Γ∞ × (Γ∞→Γ∞)，而 Γ∞ 又含 Γ×(Γ→Γ)×Σ…自相似）。这样所有层级的效应操作都统一在同一个类型上，无需为每层定义新类型。这是"统一上下文"的字面含义——一个类型管所有层。

关键论断：“Σ 囊括所有共享可变状态，而非仅组件间依赖”。因为 𝒱（值类型族）不受约束，任何需要在组件间共享的状态（配置、缓存、连接池、UI 状态…）都能编码为某个 key 的依赖。于是 Γ∞ 成为"组件与环境之间所有交互的唯一通道"——效应通过累积器、依赖通过 Σ，全经此实体。这是范式的核心主张：不再有"隐式全局状态"，一切共享都经上下文。

"插拔比喻"把抽象落实为直觉：加载组件=插入（施加效应、注册依赖），卸载=拔出（施加逆、撤回依赖），且不影响其他组件。层级结构支持树状嵌套——父管子的效应，可任意深度。工程上，Γ∞ 对应框架的"组件树 + 依赖容器 + 清理链"的统一运行时对象：每个组件实例有自己的 Γ∞ 视图，父组件的上下文包含子组件的，set/get 操作依赖、effect 注册清理，全在一个自相似结构里。这正是 DSH/Cordis 实践中 ctx 对象的形式化——它是效应入口（ctx.effect）也是依赖入口（ctx.inject/provide），二者统一于一个递归上下文。

3.3.2. Observational Equivalence / 观测等价

原文 (English)

The recovery guarantee of Section 3.1 asserts an equality of states (Theorem 7), which is an idealization, because the physical state cannot be recovered as it stood. For example, free releases a block to the allocator without restoring the layout the heap had before malloc; and a generative name is not restored by the inverse that discards it, since the next creation draws a fresh one [39]. The equalities of Section 3 are therefore to be read up to an equivalence ≃, and we take ≃ to be an observational equivalence: two states are related when no observer can distinguish them. Comparing behaviour rather than representation is the established route to program equivalence [40], and the relation such a comparison yields depends on what the observer is given to work with [41]. What an observer of a context is given is the coeffects it carries, each of which arrives with an equivalence of its own (Definition 24), so the relation on a context is assembled from theirs. Assembling it is the business of this subsection, and quotienting by it is what buys the independence Section 3.1.3 asks for.

中文翻译

第 3.1 节的恢复保证断言一个状态的相等（定理 7），这是一个理想化，因为物理状态无法恢复成它原来的样子。例如，free 把一块内存归还给分配器，却不能恢复 malloc 之前堆的布局；而一个生成性名字不会被丢弃它的逆恢复，因为下一次创建会取一个全新的 [39]。故第 3 章的相等应读作"模等价 ≃"，而我们取 ≃ 为一个观测等价：当没有观测者能区分两个状态时，它们相关。比较行为而非表示是程序等价的既定路径 [40]，而这样的比较所产生的关系取决于观测者被给予了什么来操作 [41]。一个上下文的观测者被给予的是它所携带的协效应，每个协效应都自带一个等价（定义 24），所以上下文上的关系由它们组装而成。组装它是本小节的事务，而按它商化正是买到第 3.1.3 节所要求的独立性。

详细解释

这段是 3.3.2 的动机，揭示了一个深刻问题：定理 7 断言"recover 后状态 = 初始状态"是字面相等，但物理上不可能——free 不能恢复 malloc 前的堆布局（碎片化、地址可能不同），生成性名字（gensym、Symbol()、UUID）丢弃后重建会得到新名字。所以"相等"必须弱化为"模等价 ≃"。

论文取 ≃ 为观测等价："没有观测者能区分的两个状态"视为等价。这是程序等价的经典思路（比较行为而非表示，引用 [40][41]）。关键洞察：观测者能观测什么，取决于它被给予了什么"操作接口"——而上下文的观测者被给予的正是协效应（定义 24 里每个 key 带 𝒜_k 操作集）。所以上下文上的等价关系，由各 key 的协效应等价 ≃_k 组装而成。

最关键的一句：“按 ≃ 商化正是买到 3.1.3 所要求的独立性”。回忆 3.1.3：独立性是"对效应的条件"（开发者责任），论文当时留下"3.3.2 确定满足它的纪律"。答案在此——通过观测等价商化，两个"表示不同但观测不可区分"的状态被视为相同，于是"两个操作留下 ≃_k 等价的值"也算"交换"（因为结果不可区分）。这极大放宽了独立性的可达性：不要求字面交换，只要求"观测上交换"。这就是"用协效应的等价为效应独立性兜底"的机制——观测等价让独立性从"严格条件"变成"工程上可达的条件"。

Definition 33 (定义 33) — Observational Equivalence ≃ / 观测等价

原文 (English)

Definition 33. Two coeffect contexts are related when they bind the same keys to related values, and two states of a context when their coeffect projections are:
𝜎 ≃ 𝜎′ ≔ dom(𝜎) = dom(𝜎′) ∧ ∀𝑘 ∈ dom(𝜎). 𝜎(𝑘) ≃𝑘 𝜎′(𝑘)
𝛾 ≃ 𝛾′ ≔ 𝜎𝛾 ≃ 𝜎𝛾′ (32)
writing 𝜎𝛾 for the coeffect projection of 𝛾 (Definition 32).
The part of a state that no key binds is thereby forgotten, and forgetting it is what lets Theorem 7 be read up to ≃ at all: the heap layout and the generative name of the examples above lie outside the relation unless some key binds them. What Section 3.2.2 needs of ≃ follows rather than being assumed. Related states have the same domain, so they agree on the satisfaction predicate 𝜎 ⊧ 𝑑 and on the classification notify𝑑 of Definition 26, and reactivity is a property of Σ/ ≃.

中文翻译

定义 33. 两个协效应上下文在它们把相同的键绑定到相关的值时相关，两个上下文状态在它们的协效应投影相关时相关：

𝜎 ≃ 𝜎′ ≔ dom(𝜎) = dom(𝜎′) ∧ ∀𝑘 ∈ dom(𝜎). 𝜎(𝑘) ≃𝑘 𝜎′(𝑘)
𝛾 ≃ 𝛾′ ≔ 𝜎𝛾 ≃ 𝜎𝛾′　(32)
其中 𝜎𝛾 记 𝛾 的协效应投影（定义 32）。
状态中没有任何键绑定的部分由此被遗忘，而遗忘它正是让定理 7 能模 ≃ 来读的前提：上面例子中的堆布局和生成性名字除非被某键绑定，否则处于关系之外。第 3.2.2 节对 ≃ 所需的并非假设而是推论。相关状态有相同的定义域，故它们在满足谓词 𝜎 ⊧ 𝑑 及定义 26 的分类 notify𝑑 上一致，反应性是 Σ/ ≃ 的性质。

详细解释

定义 33 把"观测等价"具体化：

• σ ≃ σ'：两个协效应上下文等价，当它们定义域相同（绑定的 key 集一样）且每个 key 的值按该 key 的等价 ≃_k 相关。
• γ ≃ γ'：两个状态等价，当它们的协效应投影 σ_γ 等价——即只比较协效应部分，状态中"没有被任何 key 绑定的部分"被遗忘。

“遗忘未被绑定的部分"是关键——堆布局、生成性名字、内存地址等"物理表示细节”，除非某个 key 显式绑定它们，否则不在等价关系里，自动被忽略。这正是让定理 7"模 ≃ 成立"的前提：recover 后堆布局可能不同、生成的名字可能不同，但只要这些差异没有被任何协效应 key 绑定（即没有观测者能通过协效应操作看到差异），两个状态就 ≃ 等价，定理 7 的"相等"读作"模 ≃ 相等"就成立。

论文强调"3.2.2 对 ≃ 的需求是推论而非假设"：因为 ≃ 的状态定义域相同，所以满足谓词 σ ⊧ d 一致（依赖满足性不变），notify_d 分类一致（激活/停用判定不变）——反应性在商集 Σ/≃ 上良定义。这意味着用观测等价商化不破坏反应式协效应的语义，两个等价状态在反应性上行为一致。工程上，这允许框架"recover 后物理状态略有不同（如内存地址变了），但只要语义观测一致，就视为正确恢复"——给真实运行时（带 GC、带地址随机化）留出实现空间。

Definition 34 (定义 34) — Tests and Indistinguishability ≈_𝒜 / 测试与不可区分性

原文 (English)

Definition 34. Let 𝑉 carry a set 𝒜 of operations in the sense of Definition 24, and write 𝔐(𝑎) for the transformation monoid (Definition 17) of the effect functions 𝑎(𝑥) over every argument 𝑥 : 𝑋𝑎. A test over 𝒜 is a finite word over the generators of the monoids 𝔐(𝑎), 𝑎 ∈ 𝒜, each letter applied to the value the letters before it left; its outcomes are those the letters that are forward maps of operations yield along the way, and it is undefined where a precondition fails. Values 𝑣, 𝑣′ : 𝑉 are indistinguishable, written 𝑣 ≈𝒜 𝑣′, when every test over 𝒜 is defined at both or at neither and yields the same outcomes at both.

中文翻译

定义 34. 设 𝑉 按定义 24 的意义承载一组运算 𝒜，并记 𝔐(𝑎) 为效应函数 𝑎(𝑥) 在每个参数 𝑥 : 𝑋𝑎 上的变换幺半群（定义 17）。𝒜 上的一个测试是诸幺半群 𝔐(𝑎)（𝑎 ∈ 𝒜）的生成元上的一个有限字，每个字母施加于前面字母所留下的值；其结果是那些作为运算前向映射的字母沿途所产出的，且在前置条件失败处无定义。值 𝑣, 𝑣′ : 𝑉 不可区分（记 𝑣 ≈𝒜 𝑣′），当 𝒜 上的每个测试在两者处都有定义或都无定义，且在两者处产出相同的结果。

详细解释

这个定义把"观测等价"精确化为"通过操作测试不可区分"。一个"测试"是一串操作的有限序列（字）：从某值出发，依次施加一系列操作（前向映射或逆），每步把上一步的结果作为输入。测试的"结果"是沿途前向映射所产出的 outcomes 序列。若某个操作的前置条件在某步失败，整个测试在该值处"无定义"。

两个值 v ≈_𝒜 v'（不可区分）当且仅当：所有可能的测试在 v 和 v’ 上行为一致——要么都有定义且产出相同结果序列，要么都无定义。即"无论观测者怎么用 𝒜 里的操作去探测，都无法区分 v 和 v’"。这是"观测等价"的严格形式化：等价 = 所有可能的观测实验都给不出差异。

这里用"变换幺半群 𝔐(a) 的生成元"作为测试的字母，是因为操作可能产逆（定义 24 的操作返回值上的逆），所以测试可包含"施加逆"的步骤——观测者不仅能调用操作，还能撤销操作来探测。这覆盖了"通过反复操作-撤销-再操作来区分值"的所有可能观测手段。≈_𝒜 是最粗的、操作能尊重的等价（见引理 35），所以取 ≃_k = ≈_{𝒜_k} 是最宽松的合理选择——只把"操作真的无法区分"的值视为等价。工程上，这定义了"两个依赖值何时算一样"——只要通过其 API 怎么测都测不出差别，就视为等价，允许底层表示不同。

Lemma 35 (引理 35) — 不可区分性是最粗的可尊重等价

原文 (English)

Lemma 35. Indistinguishability is the coarsest relation the operations respect. That is,

中文翻译

引理 35. 不可区分性是运算所尊重的最粗关系。即

详细解释

（证明梗概：第1部分，在测试前加一个操作字母仍是合法测试，由 v≈v’ 知所有测试一致，故加字母后到达的值仍不可区分、结果仍相等——操作尊重 ≈。第2部分，若等价 R 被所有操作尊重，则 R 相关的值经测试每步（前向或逆）都保持相关、结果相等，故所有测试一致，即 R ⊆ ≈。）这个引理确立 ≈_𝒜 的** extremal（极值）性质**：它是"所有操作都尊重的等价"中最粗的（最大的）——任何被操作尊重的等价 R 都被 ≈_𝒜 包含。

意义：开发者选择 ≃_k 时有两个约束——(a) 必须被操作尊重（否则操作语义在商集上不良定义）；(b) 越粗越好（商掉越多，独立性越易满足）。引理 35 说 ≈_{𝒜_k} 是满足 (a) 的最粗等价，所以它是"最佳选择"——取 ≃_k = ≈_{𝒜_k} 既合法又最宽松。任何更细的 ≃_k（如字面相等）也合法但过于严格，不利于独立性。这给了 ≃_k 选择的明确指导：用操作能区分的最小粒度。工程上，这意味"只要依赖值的 API 行为相同就视为等价"，不必要求内部表示完全一致——例如两个数据库连接对象，只要查询返回相同结果、事务行为一致，就 ≃ 等价，即便底层连接 ID 不同。

Definition 36 (定义 36) — Map Respecting ≃ / 映射尊重等价

原文 (English)

Definition 36. A map 𝑓 : Γ → Γ respects ≃ when
∀𝛾, 𝛾′ ∈ Γ. 𝛾 ≃ 𝛾′ ⇒ 𝑓(𝛾) ≃ 𝑓(𝛾′) (33)
Two maps are related when they agree at every state, and two pairs in 𝜕Γ when both components are:
𝑓 ≃ 𝑔 ≔ ∀𝛾 ∈ Γ. 𝑓(𝛾) ≃ 𝑔(𝛾)
(𝛿, 𝑔) ≃ (𝛿′, 𝑔′) ≔ 𝛿 ≃ 𝛿′ ∧ 𝑔 ≃ 𝑔′ (34)
A map respecting ≃ is one that descends to Γ/ ≃, and two maps related by ≃ are two that descend to the same map there. An effect function needs both: the first so that the state it computes is determined on the quotient, the second so that the inverse it returns is.

中文翻译

定义 36. 一个映射 𝑓 : Γ → Γ 尊重 ≃，当

∀𝛾, 𝛾′ ∈ Γ. 𝛾 ≃ 𝛾′ ⇒ 𝑓(𝛾) ≃ 𝑓(𝛾′)　(33)
两个映射在每个状态处一致时相关，𝜕Γ 中的两个对在两个分量都相关时相关：
𝑓 ≃ 𝑔 ≔ ∀𝛾 ∈ Γ. 𝑓(𝛾) ≃ 𝑔(𝛾)
(𝛿, 𝑔) ≃ (𝛿′, 𝑔′) ≔ 𝛿 ≃ 𝛿′ ∧ 𝑔 ≃ 𝑔′　(34)
尊重 ≃ 的映射是能下降到 Γ/ ≃ 的映射，由 ≃ 相关的两个映射是下降到那里同一映射的两个。一个效应函数两者都需要：前者使它计算的状态在商集上确定，后者使它返回的逆在商集上确定。

详细解释

这个定义把"尊重等价"从值层扩展到映射层，为"在商集 Γ/≃ 上做效应推理"做准备：

• 映射尊重 ≃（式33）：f 把等价的状态映到等价的状态——即 f 在等价类上良定义，能"下降"到商集 Γ/≃ 成为一个函数。若不尊重，f 在等价的两个状态上给出不等价的结果，那 f 在商集上就没意义。
• 两个映射 ≃ 相关（式34上半）：f ≃ g 当它们在每个状态处给出等价的结果——即 f、g 下降到商集上是同一个函数。这是"映射层面的观测等价"。
• ∂Γ 中对的 ≃ 相关（式34下半）：(δ, g) ≃ (δ', g') 当状态等价 δ ≃ δ' 且逆等价 g ≃ g'。

论文点明效应函数两者都需要：(1) 尊重 ≃（状态在商集上确定）；(2) 返回的逆也 ≃ 相关（逆在商集上确定）。因为效应函数不仅返回状态还返回逆，若只状态尊重而逆不尊重，"撤销"在商集上就无意义。这为定义 37（把 𝔈*Γ 读作模 ≃）铺路：带见证的效应函数在商集上也要良定义。工程上，这保证"用观测等价推理效应"时，状态和清理函数都在等价类层面确定，不会出现"等价状态却要不同清理"的歧义。

Definition 37 (定义 37) — 𝔈*Γ Read up to ≃ / 模等价读带见证效应函数

原文 (English)

Definition 37. Read Definition 8 up to ≃: an 𝑒 ∈ 𝔈Γ lies in 𝔈∗Γ when 𝑒 respects ≃ as a map Γ → 𝜕Γ and, writing (𝛿, 𝑔) = 𝑒(𝛾), for every 𝛾 ∈ Γ

中文翻译

定义 37. 把定义 8 模 ≃ 来读：一个 𝑒 ∈ 𝔈Γ 属于 𝔈∗Γ，当 𝑒 作为映射 Γ → 𝜕Γ 尊重 ≃，且记 (𝛿, 𝑔) = 𝑒(𝛾)，对每个 𝛾 ∈ Γ

详细解释

定义 37 把定义 8（带见证效应函数）的"字面相等"全部替换为"模 ≃ 等价"：

• e 作为 Γ → ∂Γ 尊重 ≃（状态和逆都在商集上良定义）；
• 见证条件从 g(δ) = γ 弱化为 g(δ) ≃ γ——逆只需把状态撤回到等价的初始状态，而非字面相同；
• g 尊重 ≃（逆在商集上良定义）。

取 ≃ 为字面相等就恢复定义 8，所以定义 37 是定义 8 的严格推广。这个推广的意义：效应的"可逆性"现在只需"观测可逆"——recover 后状态不必字面回到原样，只需回到一个观测等价的状态。这解决了开篇 free/堆布局/生成性名字的问题：recover 后堆布局不同、生成的名字不同，但只要观测等价（通过协效应操作测不出差别），就算"正确恢复"。

这是让 3.1 的全部理论"落地到真实物理状态"的关键一招——把理想化的字面相等换成工程可达的观测等价。引理 38 会证明 3.1 的所有等式在替换后仍成立。工程上，这允许框架的 recover 实现"尽力而为"——恢复语义观测一致的状态即可，不必强求物理表示完全一致，这给 GC、内存复用、地址随机化等真实运行时机制留出空间。

Lemma 38 (引理 38) — 3.1 的等式模 ≃ 成立，累积器尊重 ≃

原文 (English)

Lemma 38. With 𝔈∗Γ read as in Definition 37, every equality of states asserted in Section 3.1 holds with = replaced by ≃, and the accumulator of every state reachable from (𝛾0, idΓ) respects ≃.
Proof. An accumulator is a composition of inverses, each respecting ≃ by Definition 37(2), and a composition of maps respecting ≃ respects ≃, the base case being idΓ. The proofs of Section 3.1 then go through unchanged, respect being what carries a relation through an inverse: from 𝑔2(𝛿2) ≃ 𝛿1 and 𝑔1(𝛿1) ≃ 𝛾 respect gives (𝑔1 ∘ 𝑔2)(𝛿2) ≃ 𝛾, which is the step each composition of inverses takes, and the soundness invariant of Theorem 7 reads 𝜑(𝛾) ≃ 𝛾0 by that step. □
The commutation Definition 19 asks for is read up to ≃ by the same lemma, and reading it that way is what makes it attainable at all: two operations may leave values that ≃𝑘 identifies and still count as commuting. Of two operations it asks one thing more than of the effect functions their lifts induce, an operation yielding an outcome as well.

中文翻译

引理 38. 把 𝔈∗Γ 按定义 37 来读，第 3.1 节所断言的每个状态等式在把 = 换成 ≃ 后仍成立，且从 (𝛾0, idΓ) 可达的每个状态的累积器都尊重 ≃。
证明. 累积器是诸逆的复合，每个逆由定义 37(2) 尊重 ≃，而尊重 ≃ 的映射的复合仍尊重 ≃，基础情形是 idΓ。第 3.1 节的证明随后不变地通过，尊重正是把一个关系穿过一个逆携带的东西：由 𝑔2(𝛿2) ≃ 𝛿1 与 𝑔1(𝛿1) ≃ 𝛾，尊重给出 (𝑔1 ∘ 𝑔2)(𝛿2) ≃ 𝛾，这正是每次逆复合所取的步骤，而定理 7 的稳健性不变式按该步骤读作 𝜑(𝛾) ≃ 𝛾0。 □
定义 19 所要求的交换由同一引理模 ≃ 来读，而这样读正是让它可达的原因：两个运算可留下 ≃𝑘 等同的值而仍算作交换。对两个运算，它比其提升所诱导的效应函数多要求一件事——运算还产出一个结果。

详细解释

（证明梗概：累积器是逆的复合，每个逆尊重 ≃（定义37条款2），尊重 ≃ 的映射复合仍尊重 ≃（基础 id 尊重）。3.1 的证明中，每步"逆复合"用"尊重穿过逆"传递 ≃：g2(δ2) ≃ δ1 和 g1(δ1) ≃ γ 得 (g1∘g2)(δ2) ≃ γ，故稳健性不变式读作 φ(γ) ≃ γ0。）这个引理是"模 ≃ 化"的核心验证：3.1 节所有定理（7、11、13、15、16 等）在把字面相等 = 换成 ≃ 后全部仍成立。证明几乎不变——“尊重 ≃"这个性质承担了原来”="承担的"穿过逆传递"职责。

意义：3.1 的整个可逆效应理论，从"字面相等"版本平滑迁移到"观测等价"版本，无需重做。稳健性不变式从 φ(γ) = γ0 变成 φ(γ) ≃ γ0——recover 到达的是观测等价的初始态，而非字面相同。这让理论从理想化（物理不可能）变为工程可达（观测一致即可）。

更关键的是后半段：定义 19 的交换性也模 ≃ 来读，而这正是让独立性"可达"的原因。原来交换性要求 f∘g = g∘f（字面相等），两个操作必须留下完全相同的值才算交换——这对大多数真实操作过强。模 ≃ 后，f∘g ≃ g∘f 即可——两个操作留下观测等价的值就算交换。这极大放宽了独立性的门槛：只要两个操作的结果"测不出差别"，就视为交换，就独立。这是"用观测等价为独立性兜底"的精确机制——独立性从"严格字面条件"变为"宽松观测条件"，在工程上变得切实可达。

Definition 39 (定义 39) — Independence of Operations / 运算的独立性

原文 (English)

Definition 39. Operations 𝑎 and 𝑎′ are independent when their lifts are independent as effect functions (Definition 19) at every pair of arguments, and neither one’s transformations disturb the outcome the other yields:
∀𝑥 : 𝑋𝑎, 𝑔 ∈ 𝔐(𝑎′Σ), 𝜎 ∈ Σ. pr3(𝑎Σ(𝑥)(𝑔(𝜎))) = pr3(𝑎Σ(𝑥)(𝜎)) (35)
and the same with 𝑎 and 𝑎′ exchanged, writing 𝔐(𝑎Σ) for the transformation monoid of the lifts 𝑎Σ(𝑥) over every argument as Definition 34 writes 𝔐(𝑎) for that of the operation itself. A key 𝑘 is commutative when any two operations of 𝒜︀𝑘 are independent, an operation being held independent of itself as well.
Across distinct keys the condition holds outright.

中文翻译

定义 39. 运算 𝑎 与 𝑎′ 独立，当它们的提升作为效应函数在每对参数处独立（定义 19），且任一个的变换不扰动另一个所产的结果：

∀𝑥 : 𝑋𝑎, 𝑔 ∈ 𝔐(𝑎′Σ), 𝜎 ∈ Σ. pr3(𝑎Σ(𝑥)(𝑔(𝜎))) = pr3(𝑎Σ(𝑥)(𝜎))　(35)
并对 𝑎、𝑎′ 互换同样要求，其中 𝔐(𝑎Σ) 记提升 𝑎Σ(𝑥) 在每个参数上的变换幺半群，正如定义 34 对运算本身记 𝔐(𝑎)。一个键 𝑘 是交换的（commutative），当 𝒜︀𝑘 的任意两个运算独立，一个运算也与自身独立。
跨不同键该条件径直成立。

详细解释

定义 39 把"效应函数的独立性"（定义 19）抬到"运算的独立性"：两个运算独立，当 (1) 它们的提升 aΣ、a'Σ 作为效应函数独立（按定义 19，模 ≃）；(2) 任一个的变换不扰动另一个的结果（式35）——比效应函数多一条，因为运算还产出 outcome b（定义 24 的第三分量），要求 outcome 也不被扰动。

"键 k 是交换的"当 𝒜_k 里任意两个运算独立（含自己与自己）。这是关于"一个依赖值提供的操作集是否彼此可任意穿插"的性质。论文随即给出重要结论：“跨不同键该条件径直成立”——定理 40 会证明。

这个定义是"什么接口设计满足独立性"的具体化：一个 key 是交换的，当它的所有操作两两独立。这是 3.1.3 留下的问题"独立性是开发者责任，什么设计能满足它"的答案——把共享资源设计为交换键（操作两两独立的接口）。工程上，“交换键"对应"可任意顺序操作的资源”——如一个集合的 add/remove（任意顺序结果相同）、一个路由表的注册/注销（顺序无关）；而"非交换键"对应"顺序敏感资源"——如有序链表的插入、有状态机的事件序列。

Theorem 40 (定理 40) — 不同键的运算独立

原文 (English)

Theorem 40. Operations at distinct keys are independent.
Proof. Let 𝑎 lie in 𝒜︀𝑘 and 𝑎′ in 𝒜︀𝑘′ with 𝑘 ≠ 𝑘′. By Definition 24 every generator of 𝔐(𝑎Σ) is of the form 𝜎 ↦ 𝜎[𝑘 ↦ 𝑢(𝜎(𝑘))] for a map 𝑢 on 𝒱︀𝑘, being either the lift of a forward map or the lift of a yielded inverse, and likewise for 𝑎′ at 𝑘′. Two such maps commute, each reading and writing one key alone and the two keys differing, and Lemma 18(1) extends the commutation from the generators to the two monoids. For the second condition, what 𝑎Σ yields at 𝜎, inverse and outcome alike, is determined by 𝜎(𝑘), which every generator of 𝔐(𝑎′Σ) leaves as it stands.□

中文翻译

定理 40. 不同键上的运算独立。
证明. 设 𝑎 属 𝒜︀𝑘、𝑎′ 属 𝒜︀𝑘′ 且 𝑘 ≠ 𝑘′。由定义 24，𝔐(𝑎Σ) 的每个生成元形如 𝜎 ↦ 𝜎[𝑘 ↦ 𝑢(𝜎(𝑘))]（𝑢 是 𝒱︀𝑘 上的映射），或是前向映射的提升或是产出逆的提升，𝑎′ 在 𝑘′ 处亦然。两个这样的映射交换——各自只读写一个键而两键不同——引理 18(1) 把交换从生成元扩展到两个幺半群。对第二个条件，𝑎Σ 在 𝜎 处所产的（逆与结果 alike）由 𝜎(𝑘) 决定，而 𝔐(𝑎′Σ) 的每个生成元让 𝜎(𝑘) 原样不动。□

详细解释

（证明梗概：不同键 k≠k’ 的操作，各自的变换只读写自己的键，互不干涉——σ[k↦u(σ(k))] 不动 k’，反之亦然，故两映射交换；由引理 18(1) 生成元交换扩展到整个幺半群交换。第二个条件：aΣ 的产出由 σ(k) 决定，而 a’ 的变换不动 σ(k)，故 a’ 不扰动 a 的产出。）这个定理建立的性质是：操作不同键的运算天然独立——无需任何额外条件。

直觉很直接：两个操作改的是依赖表里不同的键，就像两个函数改不同的全局变量，天然不冲突。每个操作的变换只读写自己的键 σ[k↦…]，对其他键的值"原样不动"，所以两个不同键的操作变换交换，且互不扰动对方的产出（因为产出只依赖自己的键值，而对方不动自己的键值）。

这个定理是独立性"可达性"的基石：只要把不同组件的共享状态编码为不同的键，这些组件的操作就自动独立。这是 3.3.1 “Σ 囊括所有共享状态，每个共享位置绑自己的键"设计的回报——通过"每共享位置一键"的纪律，跨组件的独立性被结构性地保证。组件 A 操作 key kA、组件 B 操作 key kB，kA≠kB，则 A、B 独立，可任意穿插撤回。工程上，这指导"把共享状态分区到不同依赖键”——如 A 用 “featureFlags.A”、B 用 “featureFlags.B”，各自操作自己的键，天然独立可热插拔。

Definition 41 (定义 41) — Coeffect-Mediated Effect Functions / 协效应中介的效应函数

原文 (English)

Definition 41. The coeffect-mediated effect functions form the least set 𝔈𝒜Σ ⊆ 𝔈Σ that contains the unit 𝜂Σ and is closed under the following: for a key 𝑘, an operation 𝑎 ∈ 𝒜︀𝑘, an argument 𝑥 : 𝑋𝑎, and a family (𝑒𝑏)𝑏∈𝐵𝑎 of members,
𝜎 ↦ let (𝛿, 𝑠, 𝑏) = 𝑎Σ(𝑥)(𝜎) in let (𝜀, 𝑡) = 𝑒𝑏(𝛿) in (𝜀, 𝑠 ∘ 𝑡) (36)
is again a member. Each stage performs one operation and chooses what follows it by the outcome, so an argument may depend on the outcomes already obtained. The operations occurring in a member are the ones its stages perform, over every choice of outcome.

中文翻译

定义 41. 协效应中介的效应函数构成最小集 𝔈𝒜Σ ⊆ 𝔈Σ，它包含单位 𝜂Σ 并在如下规则下封闭：对一个键 𝑘、一个运算 𝑎 ∈ 𝒜︀𝑘、一个参数 𝑥 : 𝑋𝑎 和一个成员族 (𝑒𝑏)𝑏∈𝐵𝑎，

𝜎 ↦ 令 (𝛿, 𝑠, 𝑏) = 𝑎Σ(𝑥)(𝜎) ；令 (𝜀, 𝑡) = 𝑒𝑏(𝛿) ；得 (𝜀, 𝑠 ∘ 𝑡)　(36)
仍是一个成员。每个阶段执行一个运算并按结果选择后续，故一个参数可依赖于已获得的结果。一个成员中出现的运算即其各阶段所执行的，遍历结果的每种选择。

详细解释

定义 41 刻画"通过协效应操作组合而成的效应函数"——这是真实组件效应函数的形状。它归纳定义：

• 基础：单位 ηΣ（空效应）；
• 归纳步：执行一个操作 aΣ(x) 得 (δ, s, b)（新状态、逆、结果 b），然后根据结果 b 选择后续效应函数 e_b，在 δ 上执行 e_b 得 (ε, t)，复合逆为 s ∘ t。

关键在"按结果选择后续"——操作返回 outcome b，后续行为可依赖 b（e_b 是按 b 索引的效应函数族）。这建模了"组件根据运行时获取的依赖值动态决定下一步"的真实逻辑：先 get 一个配置，根据配置值决定执行哪条分支的效应。每阶段的参数 x 也可依赖之前阶段获得的 outcomes。所以这是"数据依赖的控制流"——效应序列的形状由协效应操作的返回值动态决定。

"出现的运算"是该成员所有阶段执行的操作，遍历所有可能的 outcome 选择（因为分支依赖 b，不同 b 走不同后续，所以要取所有可能路径上的操作并集）。这为定理 42 的归纳证明做准备——要证两个 𝔈^𝒜_Σ 成员独立，需考虑它们所有可能执行的操作。工程上，𝔈^𝒜_Σ 对应"组件体内用 ctx.inject 取依赖、根据依赖值做条件分支、再施加效应"的完整模式——效应不是静态固定的序列，而是随依赖值动态展开的树。

Theorem 42 (定理 42) — 交换键下协效应中介效应函数独立

原文 (English)

Theorem 42. Let 𝑒1, 𝑒2 ∈ 𝔈𝒜Σ and let every key at which operations of both occur be commutative (Definition 39). Then 𝑒1 and 𝑒2 are independent (Definition 19).
Proof. By induction on the construction of Definition 41, 𝔐(𝑒𝑖) lies in the submonoid generated by the generators of the operations occurring in 𝑒𝑖: the unit generates the trivial monoid, and a stage is a ⋄-composite of 𝑎Σ(𝑥) with a member, to which Lemma 18(2) applies.
For clause (1) of Definition 19 it is therefore enough, by Lemma 18(1), that a generator of an operation occurring in 𝑒1 commute with a generator of one occurring in 𝑒2. Where the two operations lie at distinct keys this is Theorem 40, and where they lie at one key that key carries operations of both and is commutative by hypothesis.
For clause (2), take 𝑔 ∈ 𝔐(𝑒2), a composite of generators of the operations occurring in 𝑒2, and induct on the construction of 𝑒1. The unit yields idΣ at every state. At a stage, let (𝛿, 𝑠, 𝑏) = 𝑎Σ(𝑥)(𝜎) and (𝜀, 𝑡) = 𝑒𝑏(𝛿), so that the stage yields 𝑠 ∘ 𝑡 at 𝜎. Independence of the operations, applied to one generator of 𝑔 at a time, yields 𝑠 and 𝑏 again at 𝑔(𝜎), so the same continuation 𝑒𝑏 is chosen, and clause (1) puts the state it runs from at 𝑔(𝛿), where the induction hypothesis yields 𝑡 again. The stage therefore yields 𝑠 ∘ 𝑡 at 𝑔(𝜎). □

中文翻译

定理 42. 设 𝑒1, 𝑒2 ∈ 𝔈𝒜Σ，并设两者都有运算出现的每个键都是交换的（定义 39）。则 𝑒1 与 𝑒2 独立（定义 19）。
证明. 对定义 41 的构造归纳，𝔐(𝑒𝑖) 落在 𝑒𝑖 中出现运算的生成元所生成的子幺半群里：单位生成平凡幺半群，一个阶段是 𝑎Σ(𝑥) 与一个成员的 ⋄-复合，引理 18(2) 适用。
故对定义 19 的条款 (1)，由引理 18(1)，只需 𝑒1 中某运算的生成元与 𝑒2 中某运算的生成元交换。两运算在不同键处由定理 40 给出，在同一键处则该键承载两者的运算且由假设交换。
对条款 (2)，取 𝑔 ∈ 𝔐(𝑒2)（𝑒2 中出现运算的生成元的复合），对 𝑒1 的构造归纳。单位在每个状态处给 idΣ。在一个阶段处，令 (𝛿, 𝑠, 𝑏) = 𝑎Σ(𝑥)(𝜎)、(𝜀, 𝑡) = 𝑒𝑏(𝛿)，故该阶段在 𝜎 处产 𝑠 ∘ 𝑡。运算的独立性，逐个施加 𝑔 的一个生成元，在 𝑔(𝜎) 处再次给出 𝑠 和 𝑏，故选择相同的后续 𝑒𝑏，且条款 (1) 把它运行的状态放在 𝑔(𝛿) 处，归纳假设在该处再次给出 𝑡。故该阶段在 𝑔(𝜎) 处产 𝑠 ∘ 𝑡。 □

详细解释

（证明梗概：先由构造归纳 + 引理 18(2) 得 𝔐(e_i) 落在"e_i 中操作生成元"生成的子幺半群。条款1：由引理 18(1) 只需生成元交换——不同键由定理 40、同键由"该键交换"假设。条款2：对 e_1 构造归纳，每阶段操作 a 在 g(σ) 处仍产出相同的 s 和 b（因为操作独立，g 不扰动 a 的产出），故选相同后续 e_b；状态由条款1搬到 g(δ)，归纳给相同的 t；故阶段在 g(σ) 产出相同的 s∘t。）这个定理是 3.3 节的核心成果，补全了 3.1.3 留下的"独立性由谁保证"的问题：

结论：如果两个协效应中介的效应函数 e1、e2，在它们共享的每个键（即两者都有操作出现的键）上，该键都是交换的（操作两两独立），那么 e1、e2 整体独立。

这意味着：独立性不再是"开发者手动验证每个效应交换"的负担，而是由"接口设计纪律"结构性保证——只要把共享资源设计为交换键（操作两两独立的接口），任何使用这些键的组件效应函数都自动独立。结合定理 40（不同键天然独立），独立性条件被分解为两种可工程化的情形：(1) 不同组件用不同的键——自动独立；(2) 多组件共享同一键——只要该键的接口是交换的（如集合的 add/remove），就独立。

证明的精妙在条款2的归纳：操作独立性保证"外来变换 g 不扰动 a 的产出 s 和 b"——所以即使状态被搬动到 g(σ)，操作 a 在那里仍产出相同的逆 s 和相同的 outcome b，于是选择相同的后续分支 e_b。这保证"动态分支"的独立性——不只是静态操作交换，连"根据 outcome 选择后续"的控制流也保持独立。这是把独立性从"静态操作"扩展到"动态数据依赖控制流"的关键。工程上，这是"只要共享资源的 API 是交换的（无序集合操作），组件就能任意穿插加载/卸载"的全局保证——动态插件、微前端、热重载的理论根基。

3.3.2 收尾 — 交换部分与顺序敏感部分的分解

原文 (English)

Every interaction between a component and its environment passes through the context, and the type family 𝒱︀ is unconstrained, so a system may bind every location it shares across components at a key of its own (Section 3.3.1). A component’s effect function is then the lift of a coeffect-mediated one along the coeffect projection, and independence transfers to that lift, whose transformations move the projection alone. The assumption Section 3.1.3 leaves open is met that way, and with it the temporal composability of a whole system of components.
What the decomposition divides is a computation’s commuting part from its order-sensitive part. The commuting part is carried by the effects: a component performs them in whatever order its task calls for, and Corollary 21 reverts them in whatever order the system finds convenient, no two components constraining each other. The order-sensitive part is carried by the coeffects, since a key whose operations do not commute is one whose order has to be imposed from outside the effects, and two places are available for imposing it. Within one component the accumulator imposes it, reverting in LIFO order whatever the effects (Theorem 16). Across components a declared coeffect imposes it, one component providing what another declares and the provision preceding the declaration’s satisfaction (Section 3.2.2). Composability is thereby had at the grain of components rather than of single effects, which is the scale Section 4 works at.
Two limits of the theorem are worth naming. Binding every shared location at a key is the paradigm’s discipline and not a property of the construction, so a location the system cannot reify as a coeffect lies outside the boundary of Section 6.1 and outside the theorem with it. And commutativity of a key is a property of the interface that key publishes, so meeting it is an obligation on the component providing the key rather than on the components consuming it.

中文翻译

组件与其环境之间的每次交互都经上下文，且类型族 𝒱︀ 不受约束，故系统可把它跨组件共享的每个位置绑定到各自的键上（第 3.3.1 节）。一个组件的效应函数即是协效应中介者沿协效应投影的提升，独立性传递到该提升，其变换只搬动投影。第 3.1.3 节留下的假设由此满足，随之整个组件系统的时间可组合性也满足。
该分解所划分的，是一个计算的交换部分与顺序敏感部分。交换部分由效应承载：组件按其任务所需的任何顺序执行它们，推论 21 按系统方便的任何顺序撤销它们，无两个组件相互约束。顺序敏感部分由协效应承载，因为一个操作不交换的键是其顺序须从效应之外施加的键，而施加它有两处可用。组件内由累积器施加，无论效应如何都按 LIFO 顺序撤销（定理 16）。组件间由声明的协效应施加，一个组件提供另一个所声明的，且提供先于声明的满足（第 3.2.2 节）。可组合性因此在组件粒度而非单效应粒度上获得，这是第 4 章工作的尺度。
该定理的两个局限值得点名。把每个共享位置绑到一个键是范式的纪律而非构造的性质，故系统无法物化为协效应的位置处于第 6.1 节边界之外，也随之处于定理之外。而一个键的交换性是该键所发布接口的性质，故满足它是对提供该键的组件的义务，而非对消费它的组件的义务。

详细解释

这段是 3.3.2 的总结，把整套理论收束为一个优美的计算分解：

• 交换部分由效应承载：可任意顺序执行、任意顺序撤销（推论 21），组件互不约束——这是"无序可逆"的部分。
• 顺序敏感部分由协效应承载：操作不交换的键（顺序敏感资源），其顺序从效应之外施加，两处可用：(1) 组件内由累积器强制 LIFO（定理 16）；(2) 组件间由协效应声明强制"提供先于消费"（3.2.2）。

这是一个清晰的分工哲学：效应管"可逆"（能撤、任意顺序撤），协效应管"顺序"（顺序敏感的部分由依赖关系排序）。可组合性在"组件粒度"而非"单效应粒度"上获得——这是第 4 章 calculus 的工作尺度。整套机制把"一个计算的哪些部分需要严格顺序、哪些部分可任意穿插"明确分离，前者交给协效应的依赖图，后者交给效应的可逆累积器。

论文诚实地点名两个局限：

工程上，这指导框架设计：把所有跨组件共享收进依赖容器（遵守纪律），且内置的共享资源（路由表、事件总线、缓存）应设计为交换接口（add/remove 无序安全），这样基于它们的组件就自动获得时空可组合性。这是 Cordis 范式对"如何设计可组合系统"的具体方法论。

3.3.3. Situating the Context Paradigm / 上下文范式的定位

原文 (English)

Programming paradigms differ fundamentally in how they handle side effects. Two established poles define the spectrum:
Explicit state threading (functional). To preserve referential transparency, purely functional languages model side effects as explicit transformations on state. The State monad 𝑆 → (𝐴, 𝑆) [23] threads an environment through every computation. This approach yields strong compositional guarantees: effects are visible in types and amenable to equational reasoning. However, it imposes significant ergonomic costs: every function in the call chain must accept and return the state parameter, even when it merely passes the state through unchanged. As the number of effect dimensions grows (logging, configuration, I/O), monadic stacking or effect-handler boilerplate proliferates.
Implicit mutation (imperative/OOP). Mainstream imperative languages permit components to modify shared state and access dependencies without explicit declaration at the call site. On the effect side, a representative example is React’s useEffect hook: it registers a persistent side effect on the component’s internal fiber, yet neither the effect target nor the registration mechanism appears as an explicit parameter—identification relies on call-order position within hidden runtime state. On the coeffect side, Java’s service locator pattern (e.g., Spring’s ApplicationContext.getBean(…)) retrieves dependencies from a process-wide registry at runtime, requiring null checks and type casts at each call site; dependency relationships are implicit and scattered across the codebase. More generally, understanding how f() modifies or depends on the system requires reading its implementation transitively. Refactoring becomes fragile because moving or removing a call may silently break distant invariants.

中文翻译

编程范式在如何处理副作用上有根本差异。两个既定极点定义了谱系：
显式状态穿梭（函数式）。为保持引用透明性，纯函数式语言把副作用建模为对状态的显式变换。State 幺半群 𝑆 → (𝐴, 𝑆) [23] 把一个环境穿梭过每个计算。该路径给出强组合保证：效应在类型中可见、可做等式推理。然而它施加显著的工效成本：调用链中的每个函数都必须接受并返回状态参数，即便它只是把状态原样穿过。随着效应维度增多（日志、配置、I/O），幺半群叠加或效应处理器样板代码激增。
隐式变异（命令式/OOP）。主流命令式语言允许组件修改共享状态、在调用点无需显式声明就访问依赖。在效应侧，一个代表性例子是 React 的 useEffect hook：它在组件内部 fiber 上注册一个持久副作用，但效应目标与注册机制都不作为显式参数出现——识别依赖隐藏运行时状态中的调用顺序位置。在协效应侧，Java 的服务定位器模式（如 Spring 的 ApplicationContext.getBean(…)）在运行时从进程级注册表取依赖，每个调用点需要 null 检查与类型转换；依赖关系是隐式的、散布在代码库中。更一般地，理解 f() 如何修改或依赖系统需要传递性地读其实现。重构变得脆弱，因为移动或移除一个调用可能悄然破坏远端不变式。

详细解释

3.3.3 是论文的范式定位论证，把"上下文范式"放在已有范式的谱系中凸显其独特价值。论文先描绘两个极端：

• 函数式（显式状态穿梭）：以 State monad S → (A, S) 为代表。优点——引用透明、效应在类型可见、可等式推理、组合保证强。缺点——工效成本高：每个函数都要显式传状态参数，即便只是穿透；效应维度一多（日志+配置+IO），monad 叠加（monad transformers）或 effect handler 样板代码爆炸。即"正确但繁琐"。
• 命令式/OOP（隐式变异）：以 React useEffect（效应侧）和 Spring getBean（协效应侧）为代表。优点——工效好，调用点不用显式声明。缺点——隐式、不可追踪：useEffect 的副作用目标和注册机制不在签名里，靠"调用顺序+隐藏运行时状态"识别；getBean 的依赖关系散布代码库，要 null 检查、类型转换；理解 f() 的影响要传递性读实现；重构脆弱（移动调用可能悄悄破坏远端不变式）。即"方便但失控"。

这两个极端呈现经典的"正确性 vs 工效"权衡：函数式牺牲工效换正确性，命令式牺牲可追踪性换工效。论文接下来要论证"上下文范式"同时获得两者的优点——既有函数式的可追踪性，又有命令式的工效。这段铺垫是范式主张的对照基线。工程上，每个有经验的开发者都感受过这种张力：纯函数式代码安全但啰嗦，React/Spring 代码好写但调试时难追踪副作用来源——Cordis 的上下文范式声称能两全。

3.3.3 续 — 上下文范式的综合

原文 (English)

The context paradigm combines the traceability of the functional approach with the ergonomics of the imperative approach. Effects and coeffects are both mediated through an explicit context parameter. Each operation is therefore attributable to the specific context on which it was invoked, and hence to the component that context belongs to.
Beyond combining the strengths of both poles, the context paradigm lets the developer handle each effect and dependency individually and composes them into the system’s behavior automatically. For revertible effects, the developer supplies the inverse of each atomic operation, and the inverse of any composite follows by composition (Section 3.1), so a component’s teardown is derived from its loading rather than written alongside it. For reactive coeffects, a component declares only the dependencies it needs, and the runtime resolves and re-wires them automatically (Section 3.2), keeping them consistently wired as providers are added, removed, or replaced. In both directions, correctness that would otherwise rest on developer discipline becomes a structural property of the paradigm.

中文翻译

上下文范式把函数式路径的可追踪性与命令式路径的工效结合起来。效应与协效应都通过一个显式上下文参数中介。故每个操作都可归因到它被调用的那个特定上下文，从而归因到该上下文所属的组件。
在结合两极优点之外，上下文范式让开发者逐个处理每个效应与依赖，并自动把它们组合成系统行为。对可逆效应，开发者提供每个原子操作的逆，任何复合的逆由复合得出（第 3.1 节），故一个组件的拆解由其加载派生而来，而非与加载并列编写。对反应式协效应，一个组件只声明它所需的依赖，运行时自动解析并重新接线（第 3.2 节），在提供者被添加、移除或替换时保持它们一致接线。在两个方向上，原本依赖于开发者纪律的正确性成为范式的结构性属性。

详细解释

这是范式主张的正面论述，三层递进：

这回应了开篇的权衡：函数式用"显式"换正确性但牺牲工效，命令式用"隐式"换工效但牺牲正确性。上下文范式用"单一显式上下文参数"同时获得"显式（可追踪）“和"隐式于上下文内部（工效）”，并通过"逐个声明 + 自动组合"把正确性从开发者负担转为结构保证。工程上，这就是 DSH/Cordis 的 ctx 对象哲学：ctx.effect() 注册可逆效应、ctx.inject() 声明依赖，框架自动管理回滚与响应——开发者写的是"我要做什么"（声明式），框架保证"卸载时正确撤销、依赖变化时正确启停"（结构性）。这是论文标题"时空可组合性编程范式"的最终落点：一种让动态组合的正确性成为结构保证，而非开发者负担的编程范式。