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

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

第4章 动态组合演算

本文档采用三段式结构：每节先给出英文原文，再给出中文翻译，最后给出详细解释说明。
本章把第3章的机制封装为"组件"，给出动态组合演算，并证明其元理论性质。

4.1 Components and Fibers / 组件与纤维

原文 (English)

This section fixes the objects the rules act on: the component; the fiber, an instantiation of a component carrying a lifecycle state of its own; and the registry, which holds the fibers a state carries and from which the coeffect context is read off.

Definition 43. A component over a context Γ carrying both effects and coeffects is defined as:
ℭΓ ≔ 𝔇Γ × 𝔓Γ × 𝔈∗Γ, representing a triple (𝑑, 𝑝, 𝑒), where:

• 𝑑 : 𝔇Γ is the coeffect specification, declaring the dependencies required from the environment;
• 𝑝 : 𝔓Γ ≔ 𝖲𝖾𝗍(𝐾) is the provision, declaring the coeffect keys the component may provide, and no key outside 𝑝 is one its effect function writes;
• 𝑒 : 𝔈∗Γ is the witnessed effect function, defining the effects contributed when the component is active together with the inverse that withdraws them.

The two declarations are the two directions of one interface, 𝑑 what the component reads from the environment and 𝑝 what the component writes to the environment, and Section 4.2 admits no two fibers of one registry whose provisions meet. Disjointness of provisions is where this chapter parts company with Section 3.2.3. The isolation of Definition 28 lets one key resolve through a realm table, so that two fibers may provide the same key in different realms; a calculus carrying realms would relax disjointness to disjointness within a realm. We read every key at one shared realm instead, which makes disjointness the right condition and each key’s provider unique. What it restricts is how often a component may be instantiated: one with a non-empty provision has one fiber at a time.

Definition 44. Fix a set 𝔑 of fiber names. A fiber instantiating the component (𝑑, 𝑝, 𝑒) is a tuple ⟨𝑑, 𝑝, 𝑒, 𝜋, 𝜎, 𝜏, 𝜃⟩, where:

• 𝑑, 𝑝, 𝑒 are the coeffect specification, provision, and effect function;
• 𝜋 : 𝔑 ∪ {𝗋𝗈𝗈𝗍} is the parent, the fiber this one was instantiated under, or the root marker;
• 𝜎 : Σ is the fiber’s own coeffect table, empty until it activates and written by its effects as they run;
• 𝜏 : {⊥, ⊤} is the retirement flag, ⊥ in a fresh fiber and ⊤ once the orchestrator has retired the fiber;
• 𝜃 : ΘΓ is the lifecycle state, which in the two-state model is ΘΓ ≔ 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 | 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔), where 𝑔 : Γ → Γ is the accumulator and 𝜔 : 𝑑 → 𝔑 the committed view.

The committed view 𝜔 sends each key the fiber declares to the name of the fiber that provided it when the transition committed.

Definition 45. Write 𝔉Γ for the set of fibers over Γ. A state 𝛾 ∈ Γ carries a registry 𝐹𝛾 : 𝔑 ⇀ 𝔉Γ, a finite partial function whose parent pointers form a tree rooted at 𝗋𝗈𝗈𝗍, together with whatever else in Γ no fiber’s 𝜎 names.

Each fiber owning a table means the coeffect context is derived rather than stored: it is what the active fibers jointly provide:
𝜎𝛾 ≔ ⋃{𝜎𝑚 | 𝑚 ∈ dom(𝐹𝛾), 𝜃𝑚 = 𝖠𝖼𝗍𝗂𝗏𝖾(−, −)}
The union is well defined because a fiber writes only the keys it declares and the provisions of distinct fibers are disjoint, so each key lies in the table of exactly one 𝖠𝖼𝗍𝗂𝗏𝖾 fiber, whose name we write provider𝑘(𝛾) and call the provider of 𝑘. Each key therefore has one possible provider, fixed by the provisions and not by the state.

中文翻译

本节固定了规则所作用的对象：组件（component）；纤维（fiber），即一个组件的实例化、自身带有一个生命周期状态；以及注册表（registry），它保存状态所携带的纤维，并且协同效应上下文（coeffect context）就是从中读出的。

定义 43。 在同时携带效应（effect）与协同效应（coeffect）的上下文 Γ 上，一个组件定义为 ℭΓ ≔ 𝔇Γ × 𝔓Γ × 𝔈∗Γ，表示三元组 (𝑑, 𝑝, 𝑒)，其中：

• 𝑑 : 𝔇Γ 是协同效应规约（coeffect specification），声明从环境所需的依赖；
• 𝑝 : 𝔓Γ ≔ 𝖲𝖾𝗍(𝐾) 是供给（provision），声明该组件可能提供的协同效应键，且其效应函数不会写出 𝑝 之外的键；
• 𝑒 : 𝔈∗Γ 是被见证的效应函数（witnessed effect function），定义组件激活时贡献的效应以及撤回它们的逆（inverse）。

这两个声明是同一接口的两个方向：𝑑 是组件从环境读取的部分，𝑝 是组件向环境写入的部分。第4.2节不允许同一注册表中两个纤维的供给相交。供给的不相交性（disjointness of provisions）正是本章与第3.2.3节分道扬镳之处：定义28的隔离性允许一个键通过域表（realm table）解析，使两个纤维可在不同域中提供同一键；而本章在单一共享域中读取每个键，从而使不相交性成为正确条件，且每个键的提供者唯一。这限制的是组件被实例化的频次：供给非空的组件一次只能有一个纤维。

定义 44。 固定纤维名集合 𝔑。实例化组件 (𝑑, 𝑝, 𝑒) 的一个纤维是元组 ⟨𝑑, 𝑝, 𝑒, 𝜋, 𝜎, 𝜏, 𝜃⟩，其中：

• 𝑑, 𝑝, 𝑒 是协同效应规约、供给与效应函数；
• 𝜋 : 𝔑 ∪ {𝗋𝗈𝗈𝗍} 是父纤维（parent），即本纤维在其下被实例化的纤维，或根标记；
• 𝜎 : Σ 是纤维自己的协同效应表，激活前为空，由其效应在运行时写入；
• 𝜏 : {⊥, ⊤} 是退役标志（retirement flag），新纤维为 ⊥，编排者退役后为 ⊤；
• 𝜃 : ΘΓ 是生命周期状态，两态模型下 ΘΓ ≔ 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 | 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔)，其中 𝑔 : Γ → Γ 是累加器（accumulator），𝜔 : 𝑑 → 𝔑 是已提交视图（committed view）。

已提交视图 𝜔 把纤维声明的每个键映射到转换提交时提供该键的纤维名。

定义 45。 记 𝔉Γ 为 Γ 上的纤维集合。状态 𝛾 ∈ Γ 携带注册表 𝐹𝛾 : 𝔑 ⇀ 𝔉Γ，这是一个有限偏函数，其父指针构成以 𝗋𝗈𝗈𝗍 为根的树，外加 Γ 中没有任何纤维的 𝜎 所命名的其余部分。

每个纤维拥有自己的表意味着协同效应上下文是派生的而非存储的：它就是所有激活纤维共同提供的：
𝜎𝛾 ≔ ⋃{𝜎𝑚 | 𝑚 ∈ dom(𝐹𝛾), 𝜃𝑚 = 𝖠𝖼𝗍𝗂𝗏𝖾(−, −)}
该并集是良定义的，因为纤维只写它声明的键，且不同纤维的供给不相交，所以每个键恰存在于一个激活纤维的表中，其名记为 provider𝑘(𝛾)，称为该键的提供者。因此每个键有唯一的可能提供者，由供给而非状态固定。

详细解释

本节确立了整个第4章的对象模型，核心是把第3章里"效应 + 协同效应"的机制封装成一个可命名、可实例化、带生命周期的"组件纤维"。理解这一节的关键是把握三件事的对应关系：

第一，组件 = effect + coeffect + 计算体的三元组。 一个组件 (𝑑, 𝑝, 𝑒) 是一个"接口的两面"：𝑑（coeffect specification，协同效应规约）声明它要从环境读什么依赖，𝑝（provision，供给）声明它可能向环境写哪些键，𝑒（witnessed effect function，被见证的效应函数）是真正执行副作用并产生一个逆函数的计算体。这非常像现实中的依赖注入（dependency injection）声明：𝑑 是"我需要什么"（比如需要一个数据库连接池、一个配置项），𝑝 是"我提供什么"（比如我提供一个 logger、一个 cache），𝑒 是"我激活时建立这些资源、退役时回收它们"的代码。𝑒 之所以是"被见证的"（witnessed），是因为它不仅要返回新的上下文，还要返回一个能精确还原的逆函数——这正是第3章恢复精确性（recovery exactness）在组件层的延续。

第二，纤维 = 组件的一次实例化 + 独立的生命周期。 同一个组件可以被多次实例化，每次实例化都是一个纤维，携带自己的协同效应表 𝜎、退役标志 𝜏、生命周期状态 𝜃，以及父指针 𝜋。这对应 Cordis/DSH 实践中"同一个插件类可以被装载多个实例"的能力：比如一个插件宿主可以同时运行多个配置不同的同一插件。父指针 𝜋 把所有纤维组织成一棵以 𝗋𝗈𝗈𝗍 为根的树，这正是"谁装载了谁"的因果链——对应 DSH 里一个 agent 会话启动子 agent、子 agent 再启动孙 agent 的层级关系。已提交视图 𝜔 是一个精巧设计：它记录的不是"键的值"，而是"提供该键的纤维名"，这样比较视图时不会被"值相等但提供者不同"的情况欺骗——这与实现中 fiber.committed 持有映射、fiber.target 持有其哈希（第5.1.3节）直接对应。

第三，注册表与派生的协同效应上下文。 状态 𝛾 的协同效应上下文 𝜎𝛾 不是单独存储的，而是对所有激活纤维的表取并集派生出来的。这有一个深刻后果：一个正在卸载（𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀）或正在重载（𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀）的纤维，即使它的表里还留着值，也不会被计入 𝜎𝛾——只有真正 𝖠𝖼𝗍𝗂𝗏𝖾 的纤维才对他人可见。这正是后续 4.3.1 撤回顺序得以成立的基础。供给不相交（disjointness of provisions）则对应"单一来源"（single-source）纪律：一个键在整个注册表里只有一个可能的提供者，编排者不能接纳第二个声明同一键的组件。这与第3.2.3节的域隔离（realm isolation）形成对比——域隔离允许同键多提供者，但本章为了演算的简洁选择了单一共享域。工程上，这意味着 Cordis 里同名服务的"最后注册者胜出"或"多实例共存"是被禁止的：要么用不同的键，要么显式分域。这正是组件生命周期、依赖解析得以静态推理的前提。

4.2 The Base Calculus / 基础演算

原文 (English)

This section gives the calculus of the two-state lifecycle of Figure 1 and nothing more: the target each fiber is compared against, and the five rules that move it.

Definition 46. The target view of 𝑛 at 𝛾 maps each declared key to its provider, so it is a total map 𝑑𝑛 → 𝔑, and is ⊥ when 𝑛 ought not to be running at all:
target𝑛(𝛾) ≔ { ⊥ if 𝜏𝑛 ∨ ¬(𝛾 ⊧ 𝑑𝑛); (𝑘 ∈ 𝑑𝑛) ↦ provider𝑘(𝛾) otherwise }
A state is quiescent when every fiber has reached its target view:
quiet(𝛾) ≔ ∀𝑛 ∈ dom(𝐹𝛾). { target𝑛(𝛾) = ⊥ if 𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾; target𝑛(𝛾) = 𝜔𝑛 if 𝜃𝑛 = 𝖠𝖼𝗍𝗂𝗏𝖾(−, 𝜔𝑛) }

Rules. The base calculus takes each transition to be atomic, immediate, and infallible. Five rules generate two relations. An orchestration rule, prefixed O- and written 𝛾 ⇒ 𝛿, is an action the orchestrator may perform. A lifecycle rule, prefixed L- and written 𝛾 ⟶ 𝛿, is a step the system takes unprompted whenever its premises hold.

𝑛 ∉ dom(𝐹𝛾) 𝜋 ∈ dom(𝐹𝛾) ∪ {𝗋𝗈𝗈𝗍} (𝑑,𝑝,𝑒) ∈ ℭΓ ∀𝑚 ∈ dom(𝐹𝛾). 𝑝 ∩ 𝑝𝑚 = ⌀
──────────────────────────────────────────────────────────────────── O-Insert
𝛾 ⇒ 𝛾[𝑛 ↦ ⟨𝑑,𝑝,𝑒,𝜋,⌀,⊥,𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾⟩]

𝑛 ∈ dom(𝐹𝛾)
──────────── O-Retire
𝛾 ⇒ 𝛾[𝜏𝑛 ↦ ⊤]

𝜏𝑛 = ⊤ 𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 ∀𝑚. 𝜋𝑚 ≠ 𝑛
──────────────────────────────── O-Remove
𝛾 ⇒ 𝛾 ∖ 𝑛

𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 𝜔 = target𝑛(𝛾) ≠ ⊥ 𝑒𝑛(𝛾) = (𝛿, 𝑔)
──────────────────────────────────────────────── L-Reload
𝛾 ⟶ 𝛿[𝜃𝑛 ↦ 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔)]

𝜃𝑛 = 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔) target𝑛(𝛾) ≠ 𝜔 𝑔(𝛾) = 𝛿
──────────────────────────────────────────── L-Unload
𝛾 ⟶ 𝛿[𝜃𝑛 ↦ 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾]

L-Reload installs the committed view alongside the inverse; L-Unload applies the inverse and discards the committed view. Both are driven by the same comparison: L-Reload fires when a fiber holds no committed view and its target view is not ⊥, L-Unload when the committed view it holds is not its target view. This is the reactive discipline of Section 3.2, read off a target that answers to retirement as well as to the coeffects: a transition is initiated whenever the target view changes, regardless of which of the two moved it.

Definition 47. An application of 𝑒𝑛, or one of its iterations where Section 4.3.2 applies, may register a component (𝑑, 𝑝, 𝑒) ∈ ℭΓ. In place of a state map it takes the O-Insert of that component with 𝜋 = 𝑛, and it yields as its inverse the O-Retire of the fiber so registered.

Definition 48 (Confinement). A map 𝑓 : Γ → Γ is confined to 𝑛 when: (1) Writes: dom(𝐹𝛿) = dom(𝐹𝛾), 𝛿(𝑚) = 𝛾(𝑚) for every 𝑚 ≠ 𝑛, and 𝛿(𝑛) and 𝛾(𝑛) differ in 𝜎 alone; (2) Reads: two states agreeing on 𝜎𝑛, on the restrictions 𝜎𝑚|𝑑𝑛 for every 𝑚, and on the part of the state that no fiber’s table names are carried by 𝑓 to states agreeing on the same three. An effect function 𝑒 is confined to 𝑛 when every application either registers a component or has both its state map and the inverse it yields confined to 𝑛. Every fiber’s effect function is required to be confined to that fiber.

中文翻译

本节给出图1两态生命周期的演算，仅此而已：每个纤维被比较的目标，以及移动它的五条规则。

定义 46。 纤维 𝑛 在状态 𝛾 的目标视图（target view）把每个声明的键映射到其提供者，因此是一个全映射 𝑑𝑛 → 𝔑；当 𝑛 根本不该运行时取 ⊥：
target𝑛(𝛾) ≔ { 若 𝜏𝑛 ∨ ¬(𝛾 ⊧ 𝑑𝑛) 则 ⊥；否则 (𝑘 ∈ 𝑑𝑛) ↦ provider𝑘(𝛾) }
当一个状态中每个纤维都已达到其目标视图时，该状态是静止的（quiescent）：
quiet(𝛾) ≔ ∀𝑛 ∈ dom(𝐹𝛾). { 若 𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 则 target𝑛(𝛾) = ⊥；若 𝜃𝑛 = 𝖠𝖼𝗍𝗂𝗏𝖾(−, 𝜔𝑛) 则 target𝑛(𝛾) = 𝜔𝑛 }

规则。 基础演算把每次转换都视作原子的（atomic）、即时的（immediate）、不会失败的（infallible）。五条规则生成两个关系。编排规则（orchestration rule），前缀 O-，写作 𝛾 ⇒ 𝛿，是编排者可以执行的动作；其前提说明该动作何时合法，而非何时发生。生命周期规则（lifecycle rule），前缀 L-，写作 𝛾 ⟶ 𝛿，是只要前提成立系统便无需催促自行迈出的一步。

O-Insert（插入）： 在名 𝑛 不在注册表中、父 𝜋 存在（或为根）、组件合法、且其供给 𝑝 与注册表中所有现有纤维的供给不相交的前提下，插入一个初始为 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 的新纤维。这是编排者"让一个组件存在"的唯一入口。

O-Retire（退役）： 只要 𝑛 在注册表中，就将其退役标志 𝜏𝑛 置为 ⊤。退役是一个请求，与纤维当前状态无关——真正执行退役的是生命周期规则。

O-Remove（移除）： 当 𝑛 已退役（𝜏𝑛 = ⊤）、已静止（𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾）、且没有纤维以 𝑛 为父（∀𝑚. 𝜋𝑚 ≠ 𝑛）时，从注册表中删除 𝑛。退役与移除分离的原因是：一个已退役但仍激活的纤维必须先被去激活，提前移除会丢弃累加器并造成泄漏。

L-Reload（重载/激活）： 当纤维处于 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾、其目标视图 𝜔 ≠ ⊥、且执行效应函数 𝑒𝑛(𝛾) 得到新状态 𝛿 和逆 𝑔 时，把纤维置为 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔)。它一并安装已提交视图与逆函数。

L-Unload（卸载/去激活）： 当纤维处于 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔)、其目标视图已不再是 𝜔、且应用逆 𝑔(𝛾) = 𝛿 时，把纤维置为 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾。它应用逆函数并丢弃已提交视图。

两条规则都由同一个比较驱动：L-Reload 在纤维没有已提交视图且目标视图非 ⊥ 时触发，L-Unload 在纤维持有的已提交视图不再是其目标视图时触发。这就是第3.2节的反应式纪律（reactive discipline），从一个既响应退役又响应协同效应的目标视图中读出：每当目标视图变化，无论哪一方移动了它，都会发起一次转换。

定义 47。 𝑒𝑛 的一次应用（或其在4.3.2节的某次迭代）可以注册一个组件 (𝑑, 𝑝, 𝑒)。它以该组件的 O-Insert（取 𝜋 = 𝑛）替代状态映射，并以其逆产出该注册纤维的 O-Retire。

定义 48（约束性 confinement）。 映射 𝑓 : Γ → Γ 受约束于 𝑛 当且仅当：(1) 写：除 𝑛 外所有纤维不变，𝑛 自身只在 𝜎 上不同；(2) 读：在 𝜎𝑛、各 𝜎𝑚|𝑑𝑛、以及无纤维表命名的状态部分上达成一致的两个状态，经 𝑓 后仍在同样的三者上一致。效应函数 𝑒 受约束于 𝑛 当其每次应用要么注册一个组件，要么其状态映射与逆均受约束于 𝑛。每个纤维的效应函数都要求受约束于该纤维。

详细解释

本节是整个演算的"骨架版本"——只考虑两态生命周期（𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 / 𝖠𝖼𝗍𝗂𝗏𝖾），且把每次转换都假设为原子、即时、不会失败。理解本节的关键是抓住"目标视图驱动"这一反应式核心：

目标视图（target view）是整个系统的"指挥棒"。 每个纤维 𝑛 在任意状态 𝛾 下都有一个目标视图 target𝑛(𝛾)：如果它该运行，就是把它的依赖键 𝑑𝑛 解析到各自提供者的映射；如果它不该运行（被退役了，或依赖没满足），就是 ⊥。系统静止（quiescent）意味着每个纤维都已经"对齐"了自己的目标视图——该激活的激活了、该静止的静止了、且激活者的已提交视图恰好等于目标视图。这就像一个恒温器系统：每个房间的目标温度是给定的，系统不断调整直到所有房间都达标。这里的"目标"由两件事决定：退役标志 𝜏𝑛（编排者的意志）和依赖满足性 𝛾 ⊧ 𝑑𝑛（环境的状态）。注意目标视图记录的是提供者名而非值——这正是为了让"同一个值但不同提供者"也能触发转换，对应实现里用 fiber 名而非值比较。

五条规则分成两类。 三条编排规则（O-Insert / O-Retire / O-Remove）是外部输入：编排者只能"请求一个纤维存在或停止存在"，从不直接设置生命周期状态。这对应 Cordis/DSH 中宿主对插件的操作语义——宿主说"装载这个插件"或"卸载那个插件"，但插件具体何时真正激活、何时真正停止，是系统自己根据依赖状况决定的。两条生命周期规则（L-Reload / L-Unload）是系统自发的：只要前提满足就触发，无需调度器提及。规则的比较机制是统一的——比较"已提交视图 𝜔"与"目标视图 target"：相等则静止，不等则转换。这种"目标—已提交"双视图比较是反应式纪律的体现：无论是因为依赖消失了导致 target 变 ⊥，还是因为退役了导致 target 变 ⊥，纤维都会卸载；无论是因为新提供者上线导致 target 变了，纤维都会重载到新解析上。

O-Insert 的最后一个前提 ∀𝑚. 𝑝 ∩ 𝑝𝑚 = ⌀ 是单一来源纪律的执行点。 它禁止接纳第二个声明已有键的组件——这正是 4.1 节供给不相交性的落地。工程上，这相当于 DSH 插件系统拒绝注册一个与已存在插件冲突的服务名，避免"两个 logger 提供者"造成的歧义。O-Retire 与 O-Remove 分离是一个重要的工程细节：退役只是"打个标记"（设 𝜏=⊤），把目标视图变 ⊥，真正的去激活由 L-Unload 完成；只有当纤维已经静止且没有子纤维时才能 O-Remove。提前移除一个仍激活的纤维会丢掉它的累加器 𝑔（逆函数），导致副作用无法回收——这就是"资源泄漏"。∀𝑚. 𝜋𝑚 ≠ 𝑛 前提保证"先移除子再移除父"，维持注册表的树形良好性。

定义47的注册原语是"插件装载插件"的语义化。 一个组件在激活时可以注册别的组件，其逆函数是"退役所注册的纤维"而非"移除"。为什么用 O-Retire 而非 O-Remove 作为逆？因为逆函数必须"在任何到达它的地方都能执行"，而 O-Remove 有前提（纤维必须静止、无子）；如果子还激活着，父的逆就卡住了。O-Retire 唯一前提是 𝑛 在注册表中，永远能执行，退役后生命周期规则会自然把它带回 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾。这对应 DSH 里"agent 退出时，它启动的子 agent 会被级联回收"的语义——一个插件宿主加载的插件，在宿主卸载时也会被退役，逐层向下级联。

定义48的约束性（confinement）是故障隔离的边界。 它从写和读两个方向限制效应函数的能力：写上，一个纤维的效应只能改自己的 𝜎 表（加上注册原语新增的条目和退役标记），不能动别人的控制字段；读上，一个纤维只能读自己的表、各提供者表中它声明依赖的部分、以及环境状态，不能读别人的表或任何控制字段。这保证了一个组件不能"偷看"或"篡改"它没声明依赖的纤维的生命周期状态——这正是故障隔离与模块封装的形式化。读约束的第(2)条尤其重要：它解释了为什么组件能读到自己声明的协同效应值——这些值在提供者的表里，所以效应函数必须能读各 𝜎𝑚|𝑑𝑛。这对应 Cordis 里组件通过依赖注入拿到的"已解析的依赖实例"，而不是直接访问整个注册表。

最后，规则是非确定且纯反应式的：多条纤维可能同时需要转换，关系不规定顺序；也没有任何规则提及调度器。因此对"所有可能的步骤序列"成立的定理，对任何运行时采用的调度策略都成立——这是后续元理论能覆盖各种现实调度的关键。

4.3 Transitions in Progress / 进行中的转换

原文 (English)

This section extends the base calculus in four settings. The first supplies something Section 3.2 requires and Section 4.2 cannot express, a deactivation spread over an interval its dependents may occupy; the other three drop the idealization that a transition is atomic, immediate, and infallible, none of which a transition in a real runtime is. What is dropped is that a whole transition is one step, not that a step is one application of one rule, and the four share one structural consequence: a transition that is not a step needs a state to occupy while it is under way, one for each direction it may run in.

Definition 49. The lifecycle states of this section replace ΘΓ by
ΘΓ ≔ 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜁) | 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖, 𝑔, 𝜔) | 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔) | 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, 𝜁)
where 𝑖 is the remaining effect iterator, 𝑔 the accumulator built so far, 𝜔 the committed view, and 𝜁 : {⊥} ∪ Ξ the outcome, carried by 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 as the one its deactivation is headed for and by 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 as the one it reached, either ⊥ or an error from the set Ξ that Section 4.3.4 supplies.

A fiber is installed when it is in one of the three states carrying an accumulator and a committed view, and failed when it carries an error outcome:
installed𝑛(𝛾) ≔ 𝜃𝑛 ≠ 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(−), failed𝑛(𝛾) ≔ ∃𝜉 ∈ Ξ. 𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜉)
The quiescence is read on the wider state space, and 𝜎𝛾 still unions the tables of 𝖠𝖼𝗍𝗂𝗏𝖾 fibers alone, so a fiber whose transition is under way in either direction reads its coeffects through the 𝜔 it holds and provides none of its own; a key that its transition has already written is therefore not yet one a dependent may activate against.

中文翻译

本节在四种情境下扩展基础演算。第一种补足第3.2节要求而第4.2节无法表达的东西：一次去激活分散在一段时间内，供其依赖者占据；其余三种放弃"转换是原子的、即时的、不会失败的"这一理想化——而真实运行时里的转换三者皆非。被放弃的是"整次转换是一步"，而非"一步是一次规则应用"，四者共享一个结构后果：一次非一步的转换需要一个在它进行期间占据的状态，每个可能的方向各需一个。

定义 49。 本节的生命周期状态把 ΘΓ 替换为：
ΘΓ ≔ 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜁) | 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖, 𝑔, 𝜔) | 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔) | 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, 𝜁)
其中 𝑖 是剩余的效应迭代器（effect iterator），𝑔 是迄今构建的累加器，𝜔 是已提交视图，𝜁 : {⊥} ∪ Ξ 是结果（outcome），由 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 携带为其去激活所朝向的结果、由 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 携带为其已到达的结果，要么是 ⊥，要么是4.3.4节提供的错误集合 Ξ 中的某个错误。

一个纤维处于携带累加器与已提交视图的三种状态之一时是已安装的（installed），携带错误结果时是已失败的（failed）：
installed𝑛(𝛾) ≔ 𝜃𝑛 ≠ 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(−)，failed𝑛(𝛾) ≔ ∃𝜉 ∈ Ξ. 𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜉)
静止性在更宽的状态空间上读出，而 𝜎𝛾 仍然只对 𝖠𝖼𝗍𝗂𝗏𝖾 纤维的表取并集，所以一个转换正在进行（任一方向）的纤维通过它持有的 𝜔 读取自己的协同效应，且不提供自己的协同效应；因此其转换已经写下的键，尚未成为依赖者可以激活所依据的键。

详细解释

本节是整章的"分水岭"：它把基础演算那个过于理想的两态模型扩展为四态模型，逐步放弃"原子、即时、不会失败"三个理想化假设。核心结构洞见是：一次转换若不是单步完成的，就需要一个"进行中"的状态来栖身——每个方向（重载方向、卸载方向）各一个。

于是生命周期从两态扩展为四态：𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜁)（静止，携带结果 𝜁）、𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖, 𝑔, 𝜔)（重载中，携带剩余迭代器、已构建累加器、已提交视图）、𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔)（激活，携带累加器与已提交视图）、𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, 𝜁)（卸载中，携带累加器、已提交视图、朝向的结果）。这对应现实运行时里一次"热重载"或"卸载"不是瞬时的：它要执行一段代码、可能跨越多次迭代、可能等待异步操作、可能中途失败。

最关键的可见性规则：𝜎𝛾 仍然只对真正 𝖠𝖼𝗍𝗂𝗏𝖾 的纤维取并集。这意味着一个 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 或 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 的纤维，即使它的表里已经写了值，也不对他人可见——它通过自己持有的已提交视图 𝜔 来读依赖，但不向他人提供任何键。这有两个工程含义：一是"半装载的组件不对外可见"，避免依赖者看到一个还没准备好的服务；二是为 4.3.1 的撤回顺序奠定基础——一个开始卸载的纤维立即从 𝜎𝛾 中消失，于是依赖它的纤维会发现目标视图变化、也开始卸载，形成自然的级联。

后续四个子节分别处理：撤回（把卸载分成"标记离开"与"真正回收"两步）、迭代（把激活分成多次可中断的迭代）、异步（一次迭代在飞行期间环境会变）、失败（迭代可能抛错）。每个子节只往这个四态空间上加规则，不改变已有结果——这是本章"分层扩展"的设计哲学。

4.3.1 Withdrawal / 撤回

原文 (English)

Section 3.2 requires that dependents activate after their dependencies and that dependencies withdraw their provisions only after their dependents have deactivated. The second half must deliver that a consumer can still read 𝑘 throughout its own deactivation, and that the provider’s withdrawal of 𝑘 takes effect only afterwards. The base calculus cannot deliver it at all: its L-Unload removes the provisions and runs the inverse together, leaving no interval between them for a consumer’s teardown to occupy.

This layer splits that step in two, and guards the second half by the following condition.

Definition 50. The fiber 𝑛 is relied upon at 𝛾 when some other installed fiber resolves a key to it:
relied𝑛(𝛾) ≔ ∃𝑚 ∈ dom(𝐹𝛾), 𝑘 ∈ 𝑑𝑚. 𝑚 ≠ 𝑛 ∧ installed𝑚(𝛾) ∧ 𝜔𝑚(𝑘) = 𝑛

𝜃𝑛 = 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔, 𝜔) target𝑛(𝛾) ≠ 𝜔
──────────────────────────────────────── L-Leave
𝛾 ⟶ 𝛾[𝜃𝑛 ↦ 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, ⊥)]

𝜃𝑛 = 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, 𝜁) ¬ relied𝑛(𝛾) 𝑔(𝛾) = 𝛿
──────────────────────────────────────────────── L-Unload
𝛾 ⟶ 𝛿[𝜃𝑛 ↦ 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜁)]

L-Leave records the decision to deactivate without acting on it, which stops the fiber providing its coeffects while leaving its own committed view and everyone else’s intact. L-Unload applies the accumulator, discards the committed view, and leaves the fiber 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 on the outcome it carries. The two halves of the ordering are then carried by different parts of the form: the visibility half by the committed view, which L-Unload discards as its last act, and the ordering half by the premise ¬ relied𝑛(𝛾), which we call the guard and which holds the withdrawal of 𝑘 back until every consumer that resolves it to 𝑛 has gone.

The guard is imposed per binding rather than per fiber. A guard of this kind ordinarily deadlocks. What keeps it from doing so is 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 together with 𝜎𝛾 being the union over 𝖠𝖼𝗍𝗂𝗏𝖾 fibers alone: once L-Leave has marked 𝑛, its table leaves 𝜎𝛾, so no target view can name 𝑛 any longer, and every consumer that committed to 𝑛 is itself on its way out.

中文翻译

第3.2节要求依赖者在依赖之后激活，且依赖只有在依赖者都已去激活之后才撤回其供给。后半段必须保证：一个消费者能在它自己整个去激活期间持续读到 𝑘，而提供者对 𝑘 的撤回只在之后才生效。基础演算根本做不到这一点：它的 L-Unload 把撤回供给与运行逆函数合在一起做，没有给消费者的拆卸留出任何时间间隔。

本层把这一步拆成两步，并用如下条件守护后半步。

定义 50。 当某个其他已安装纤维把一个键解析到 𝑛 时，纤维 𝑛 在 𝛾 处被依赖（relied upon）：
relied𝑛(𝛾) ≔ ∃𝑚 ∈ dom(𝐹𝛾), 𝑘 ∈ 𝑑𝑚. 𝑚 ≠ 𝑛 ∧ installed𝑚(𝛾) ∧ 𝜔𝑚(𝑘) = 𝑛

L-Leave（离开）： 当纤维 𝖠𝖼𝗍𝗂𝗏𝖾 且目标视图不再是 𝜔 时，记录去激活的决定但不立即执行——把纤维置为 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, ⊥)，这使它停止提供协同效应，同时保留自己的已提交视图与他人视图不变。

L-Unload（卸载）： 当纤维 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀、且不再被任何已安装纤维依赖（¬ relied𝑛(𝛾)）、且应用逆 𝑔(𝛾) = 𝛿 时，应用累加器、丢弃已提交视图、把纤维置为 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜁)。它是演算中唯一应用累加器的规则。

排序的两半于是由形式的不同部分承载：可见性的一半由已提交视图承载（L-Unload 在最后才丢弃它），排序的一半由前提 ¬ relied𝑛(𝛾) 承载——我们称之为守卫（guard），它把 𝑘 的撤回推迟到每个把 𝑘 解析到 𝑛 的消费者都离开之后。

守卫是按绑定（per binding）施加的，而非按纤维。这种守卫通常会导致死锁。使它不死锁的是 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 加上 𝜎𝛾 只对 𝖠𝖼𝗍𝗂𝗏𝖾 纤维取并集：一旦 L-Leave 标记了 𝑛，它的表就离开 𝜎𝛾，于是没有任何目标视图能再命名 𝑛，每个提交到 𝑛 的消费者自己也在退出的路上。

详细解释

这是整章最精妙的一节，它解决了一个非常实际的工程问题：当一个被依赖的组件要卸载时，依赖它的组件在执行自己的拆卸代码时，往往还需要用到那个正在被撤回的依赖。 论文举的例子非常贴切：关闭一个连接池通常意味着要把连接归还给"提供连接的那个东西"——也就是说，连接池消费者的拆卸代码恰恰需要那个正在被撤回的连接池本身。如果像基础演算那样把"撤回供给"和"运行逆函数"同时做掉，消费者的拆卸就会访问一个已经不存在的依赖，崩溃。

解决方法是把卸载拆成 L-Leave 和 L-Unload 两步。 L-Leave 只是"打个招呼说我要走了"——把纤维从 𝖠𝖼𝗍𝗂𝗏𝖾 移到 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀，但不立即运行逆函数，也不立即丢弃已提交视图。关键的可见性效果是：一旦进入 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀，该纤维的表就立即从 𝜎𝛾 中消失（因为 𝜎𝛾 只对 𝖠𝖼𝗍𝗂𝗏𝖾 取并集），于是所有依赖它的纤维会发现目标视图变了、也开始 L-Leave。但这个 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 的纤维自己仍然通过它持有的已提交视图 𝜔 读到它的依赖——所以它的拆卸代码（运行在逆函数 𝑔 里）仍能访问它需要的协同效应。

L-Unload 才是真正回收资源的那一步，它有守卫 ¬ relied𝑛(𝛾)：只有当没有任何已安装纤维再把键解析到 𝑛 时，才允许运行逆函数并真正撤回。这个守卫是"按绑定"的——只有那些确实声明了 𝑛 提供的键的纤维才算障碍，没声明的无关。这避免了"无关纤维挡住卸载"的问题。

为什么不会死锁？ 这是整个设计的精髓。一个普通的"等待依赖者离开"守卫极易死锁：如果依赖者永远不离开，提供者就永远卡在 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀。但这里有一个精巧的反馈环：L-Leave 让 𝑛 的表离开 𝜎𝛾 → 𝑛 不再是任何键的提供者 → 所有依赖 𝑛 的纤维的目标视图都变了（要么变 ⊥ 要么变别的提供者）→ 这些纤维也触发 L-Leave → 它们也进入 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 → 它们也不再被 𝜎𝛾 计入 → 依赖它们的纤维也开始离开……这是一个沿着协同效应依赖图的"自传播熄灭"过程。Theorem 66 把它证明为"守卫总会释放"。

与 Cordis/DSH 实践的对应。 这正是组件生命周期里"优雅停机"（graceful shutdown）的形式化：一个被依赖的服务收到卸载信号后，先停止接收新依赖者（L-Leave），等所有现有依赖者都完成拆卸后，才真正释放自己持有的资源（L-Unload）。它也对应热重载场景：替换一个 logger 实现时，先让所有使用旧 logger 的组件逐个切换/拆卸，最后才销毁旧 logger。守卫的存在保证了"先停消费者、再停提供者"的因果顺序——这就是空间可组合性（4.4.3）的来源。注意守卫只沿协同效应排序，不沿纤维树排序：父可以先于子运行逆函数，父子在环境状态上的交叉则由独立性假设（定义60）治理——这是一个比"严格树形拆卸"更弱、但更灵活的纪律。

4.3.2 Iteration / 迭代

原文 (English)

An activation may execute multiple effects in sequence, and the deactivation must recover them. We model such an activation with an effect iterator, each of whose iterations yields the modified context, an inverse, and a continuation.

Definition 51. Define the effect iterator 𝔈iterΓ and witnessed effect iterator 𝔈iter∗Γ as the recursive types:
𝔈iterΓ ≔ 𝜇ℑ. Γ → Γ × (Γ → Γ) × 𝖬𝖺𝗒𝖻𝖾(ℑ)
𝔈iter∗Γ ≔ 𝜇ℑ. (𝑒 : Γ → Γ × (Γ → Γ) × 𝖬𝖺𝗒𝖻𝖾(ℑ)) × ((𝛾 : Γ) → (𝐥𝐞𝐭 (𝛿, 𝑔, 𝑜) = 𝑒(𝛾) 𝐢𝐧 𝑔(𝛿) ≃ 𝛾))
where 𝑒(𝛾) yields a triple (𝛿, 𝑔, 𝑜): 𝛿 is the new context; 𝑔 is the inverse function of the current effect; 𝑜 indicates the continuation: 𝖭𝗈𝗍𝗁𝗂𝗇𝗀 signals termination; 𝖩𝗎𝗌𝗍(𝑖) provides the next iteration.

Definition 52. Define the effect iterator transformation effectiterΓ as:
effectiterΓ = 𝑖 ↦ (𝛾, 𝜑) ↦ 𝐥𝐞𝐭 (𝛿, 𝑔, 𝑜) = 𝑖(𝛾) 𝐢𝐧 𝐥𝐞𝐭 𝑡 = trackΓ(𝑔, pr1 ∘ 𝑖) 𝐢𝐧 𝐦𝐚𝐭𝐜𝐡 𝑜 | 𝖭𝗈𝗍𝗁𝗂𝗇𝗀 ⇒ ((𝛿, 𝜑 ∘ 𝑔), 𝑡) | 𝖩𝗎𝗌𝗍(𝑖′) ⇒ 𝐥𝐞𝐭 (𝑠, 𝑟) = effectiterΓ(𝑖′)(𝛿, 𝜑 ∘ 𝑔) 𝐢𝐧 (𝑠, 𝑡 ∘ 𝑟)
At each iteration, the inverse 𝑔 is composed onto 𝜑 in application order, so the accumulator 𝜑 ∘ 𝑔1 ∘ ⋯ ∘ 𝑔𝑘 naturally recovers effects in LIFO order when applied. The 𝖬𝖺𝗒𝖻𝖾(𝔈iter) continuation makes a boundary available between any two consecutive iterations. In this sense the effect iterator is a reified delimited continuation, the structure that mainstream languages expose through the yield operator, so the model maps directly onto the generators they already provide.

𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥) 𝜔 = target𝑛(𝛾) ≠ ⊥
────────────────────────────────────────── L-Begin
𝛾 ⟶ 𝛾[𝜃𝑛 ↦ 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑒𝑛, idΓ, 𝜔)]

𝜃𝑛 = 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖, 𝑔, 𝜔) target𝑛(𝛾) ≠ 𝜔 (𝛿, ℎ) = (𝛾, idΓ) ∨ 𝑖(𝛾) = (𝛿, ℎ, −)
────────────────────────────────────────────────────────── L-Divert
𝛾 ⟶ 𝛿[𝜃𝑛 ↦ 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔 ∘ ℎ, 𝜔, ⊥)]

𝜃𝑛 = 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖, 𝑔, 𝜔) target𝑛(𝛾) = 𝜔 𝑖(𝛾) = (𝛿, ℎ, 𝖩𝗘(𝑖′))
────────────────────────────────────────────────────────── L-Iter
𝛾 ⟶ 𝛿[𝜃𝑛 ↦ 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖′, 𝑔 ∘ ℎ, 𝜔)]

𝜃𝑛 = 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖, 𝑔, 𝜔) target𝑛(𝛾) = 𝜔 𝑖(𝛾) = (𝛿, ℎ, 𝖭𝗈𝗍𝗁𝗂𝗇𝗀)
────────────────────────────────────────────────────────── L-Finish
𝛾 ⟶ 𝛿[𝜃𝑛 ↦ 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔 ∘ ℎ, 𝜔)]

Each iteration composes the newly yielded inverse onto the accumulator as 𝑔 ∘ ℎ, so that the accumulator applies the inverses in last-in-first-out order. Between any two consecutive iterations the system may divert the transition if its target view has changed, applying the inverse accumulated so far to recover the context. L-Divert routes through 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 like every other deactivation rather than applying the accumulator where it stands.

中文翻译

一次激活可能依次执行多个效应，而去激活必须恢复它们。我们用效应迭代器（effect iterator）建模这样的激活，其每次迭代产出修改后的上下文、一个逆、和一个续延。

定义 51。 定义效应迭代器 𝔈iterΓ 与被见证的效应迭代器 𝔈iter∗Γ 为如下递归类型：
𝔈iterΓ ≔ 𝜇ℑ. Γ → Γ × (Γ → Γ) × 𝖬𝖺𝗒𝖻𝖾(ℑ)
𝔈iter∗Γ ≔ 𝜇ℑ. (𝑒 : Γ → Γ × (Γ → Γ) × 𝖬𝖺𝗒𝖻𝖾(ℑ)) × ((𝛾 : Γ) → (𝐥𝐞𝐭 (𝛿, 𝑔, 𝑜) = 𝑒(𝛾) 𝐢𝐧 𝑔(𝛿) ≃ 𝛾))
其中 𝑒(𝛾) 产出三元组 (𝛿, 𝑔, 𝑜)：𝛿 是新上下文；𝑔 是当前效应的逆函数；𝑜 指示续延：𝖭𝗈𝗍𝗁𝗂𝗇𝗀 表示迭代终止；𝖩𝗎𝗌𝗍(𝑖) 提供下一次迭代。见证条件 𝑔(𝛿) ≃ 𝛾 保证每次迭代可逆。

定义 52。 定义效应迭代器变换 effectiterΓ：每次迭代把逆 𝑔 以应用顺序组合到 𝜑 上，因此累加器 𝜑 ∘ 𝑔1 ∘ ⋯ ∘ 𝑔𝑘 在应用时自然以后进先出（LIFO）顺序恢复效应。𝖬𝖺𝗒𝖻𝖾(𝔈iter) 续延在任意两次连续迭代之间提供一个边界。在这个意义上，效应迭代器是一个具体化的限定续延（reified delimited continuation），即主流语言通过 yield 操作符暴露的结构，因此该模型可直接映射到它们已提供的生成器（generator）。

L-Begin（开始）： 当纤维 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥) 且目标视图 𝜔 ≠ ⊥ 时，进入 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀，携带整个效应函数 𝑒𝑛 作为迭代器、空累加器 idΓ、已提交视图 𝜔。

L-Iter（迭代）： 当纤维 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀、目标视图仍等于 𝜔、且本次迭代产出续延 𝖩𝗎𝗌𝗍(𝑖′) 时，应用本次迭代的状态映射，把新逆 ℎ 组合到累加器 𝑔 ∘ ℎ，带着下一次迭代器 𝑖′ 继续停留在 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀。

L-Finish（完成）： 当纤维 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀、目标视图仍等于 𝜔、且本次迭代产出 𝖭𝗈𝗍𝗁𝗂𝗇𝗀（终止）时，应用最后一次迭代的状态映射，组合最后逆，把纤维置为 𝖠𝖼𝗍𝗂𝗏𝖾(𝑔 ∘ ℎ, 𝜔)。

L-Divert（转向）： 当纤维 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 但目标视图已不再是 𝜔 时，要么放弃正在进行的迭代（取 (𝛾, idΓ)），要么让本次迭代落地（取 𝑖(𝛾) = (𝛿, ℎ, −)），然后转入 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔 ∘ ℎ, 𝜔, ⊥)。它像所有其他去激活一样经由 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 路由，而不是就地应用累加器。

每次迭代把新产出的逆以 𝑔 ∘ ℎ 组合到累加器上，使累加器以后进先出顺序应用各逆。在任意两次连续迭代之间，若目标视图已变，系统可以转向这次转换，应用迄今累积的逆来恢复上下文。

详细解释

本节把"激活是一个原子的、一次性执行全部效应的动作"这一假设拆碎：一次激活可以由多次迭代组成，每次迭代是一个可中断的边界。 这对应现实里一个组件的初始化往往不是一行代码，而是分阶段的——先打开文件、再建立连接、再启动后台线程——每个阶段都贡献一部分副作用，也都需要一个逆（关闭文件、断开连接、停止线程）。

效应迭代器是一个"具体化的限定续延"。 论文明确指出它映射到主流语言的 yield/生成器：每次调用 𝑖(𝛾) 产出 (𝛿, 𝑔, 𝑜)，𝛿 是当前阶段执行后的新上下文，𝑔 是这个阶段的逆，𝑜 是续延（要么 𝖭𝗈𝗍𝗁𝗂𝗇𝗀 表示"我执行完了"，要么 𝖩𝗎𝗌𝗍(𝑖′) 表示"还有下一阶段"）。这就像 Python 生成器 yield 出一个值后暂停，调用方可以继续 next 推进，也可以中途 close 提前终止。被见证版本 𝔈iter∗Γ 多了一个条件 𝑔(𝛿) ≃ 𝛾，保证每次迭代都是可逆的——这是恢复精确性的逐迭代版本。

累加器的 LIFO 组合是关键。 每次迭代把新逆 ℎ 组合到累加器 𝑔 ∘ ℎ 上（即新逆先应用）。这意味着如果激活顺序是"打开文件 → 建立连接 → 启动线程"，那么卸载顺序自然就是"停止线程 → 断开连接 → 关闭文件"——后启动的先回收，这正是资源管理的标准栈式纪律。这与 try/finally、RAII、defer 的语义完全一致，但这里它被形式化为累加器 𝑔 的代数组合。

L-Begin / L-Iter / L-Finish 三条规则描述了一次成功激活的完整轨迹。 L-Begin 从 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 进入 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀，携带整个效应函数 𝑒𝑛 作为待执行的迭代器；L-Iter 反复推进，每次应用一个阶段、累积一个逆；L-Finish 在最后一次迭代产出 𝖭𝗈𝗍𝗁𝗂𝗇𝗀 时收尾，进入 𝖠𝖼𝗍𝗂𝗏𝖾。这三条规则都带前提 target𝑛(𝛾) = 𝜔——只有在目标视图没变的情况下才能继续推进。这是一个强约束：如果在多阶段激活的中途，环境变了（比如某个依赖消失了），不能继续安装更多效应。

L-Divert 处理"中途环境变了"的情况。 它有两种选择：第一种（取 (𝛾, idΓ)）放弃正在进行的迭代，相当于"还没开始这次迭代就发现目标变了，直接退出"；第二种让本次迭代落地后再退出。无论哪种，都转入 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 而非 𝖠𝖼𝗍𝗂𝗏𝖾——这一点至关重要：绝不让自己短暂地成为 𝖠𝖼𝗍𝗂𝗏𝖾 从而暴露给依赖者，因为一个正在退出的组件不该被别人当作稳定的提供者激活。L-Divert 在 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 遇到的守卫是空满足的（vacuous）——因为它从未 𝖠𝖼𝗍𝗂𝗏𝖾 过，没人把键解析到它。第一种选择（放弃迭代）只有在迭代边界才可能，所以"转向能发生的粒度就是迭代器的粒度"——这解释了为什么需要迭代器：它给出了中途可中断的点。第二种选择正是 4.3.3 异步所必需的。

退化情形： 普通的原子效应函数 𝔈Γ 就是"第一次迭代就产出 𝖭𝗈𝗍𝗁𝗂𝗇𝗀"的退化迭代器——它仍然经过 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀、L-Divert 仍适用，但累加器是 idΓ、没运行过迭代，所以要么全部安装、要么一个都不装。这保证了"全有或全无"的原子性在多阶段模型里仍然成立。

与 Cordis/DSH 实践的对应。 实现里每个变更点都允许一个迭代器（第5.1.1节），这对应一个组件的 install/uninstall 可以是分阶段的 generator。比如一个插件激活时可能 yield 多次（每次建立一种资源），卸载时按逆序回收。L-Divert 的第一种选择对应"热重载时发现依赖已变，立刻回滚尚未提交的阶段"——这正是热重载（hot reload）安全性的语义基础：你不会把半个状态留在系统里。

4.3.3 Asynchrony / 异步

原文 (English)

The layers so far let the environment move between one iteration and the next, and assume that each iteration itself completes instantaneously, its launch and its landing being one step. We model non-immediacy abstractly: an iteration yields a value of type 𝖥𝗎𝗍𝗎𝗋𝖾(𝐴), where 𝖥𝗎𝗍𝗎𝗋𝖾 is an opaque type constructor whose defining property is that between submission and resolution, external state may change.

Under this model an iteration is launched at one state and lands at another, and the fiber is 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 while it is in flight. What the layer adds is inertia: once launched, an iteration lands, and its landing cannot be declined. A target view that turns during the flight therefore cannot be answered by aborting the iteration, and only the alternative of L-Divert that lands one remains available: the iteration lands, and the fiber deactivates afterwards. This layer therefore adds no rule and no type that a rule matches on; at the granularity of Γ inertia is its whole content, and it takes the form of a restriction on which alternative of L-Divert a host may take.

That alternative is what the base calculus could not express. There, a transition whose target view had turned was undone in the same step that discovered it; here the iteration in flight must land first, so the fiber needs somewhere to be while its inverse runs, and the only sound place is 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 holding the inverse the iteration produced. Routing through 𝖠𝖼𝗍𝗂𝗏𝖾 instead would let the fiber provide its coeffects for the length of one step and oblige its dependents to activate against a component that is already leaving. This is the mutual chaining of reload and unload in the implementation.

A deactivation may also chain straight back into an activation, by a composite rather than a rule. L-Unload carries no premise on the target view, so whatever the target view has become while the fiber was deactivating, the accumulator runs and the fiber becomes 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾, from which L-Begin may immediately start a new transition.

中文翻译

到此为止的各层允许环境在一次迭代与下一次迭代之间移动，但假设每次迭代本身瞬时完成——其发起与落定是一步。我们抽象地建模非即时性（non-immediacy）：一次迭代产出一个类型为 𝖥𝗎𝗍𝗎𝗋𝖾(𝐴) 的值，其中 𝖥𝗎𝗍𝗎𝗋𝖾 是一个不透明类型构造子，其定义性质是：在提交与解析之间，外部状态可能改变。

在此模型下，一次迭代在一个状态发起、在另一个状态落定，纤维在飞行期间处于 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀。本层加入的是惯性（inertia）：一旦发起，一次迭代必然落定，其落定不可被拒绝。因此飞行期间发生转折的目标视图无法通过放弃迭代来回应，L-Divert 中"让迭代落地"的那一种选择才是唯一可用的：迭代落定，纤维随后去激活。本层因此不增加任何规则、也不增加任何规则可匹配的类型；在 Γ 的粒度上，惯性就是它的全部内容，其形式是对宿主可取 L-Divert 的哪一种选择的限制。

那一种选择正是基础演算无法表达的。在那里，目标视图已转折的转换在发现它的同一步里就被撤销；而这里飞行中的迭代必须先落定，于是纤维需要一个地方在它的逆运行期间栖身，唯一稳妥的地方是 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀，持有迭代产出的逆。若改经 𝖠𝖼𝗍𝗂𝗏𝖾 路由，会让纤维在一步的长度内提供其协同效应，迫使依赖者对一个正在离开的组件激活。这就是实现中重载与卸载的相互链式。

一次去激活也可能直接链式回到一次激活，由一个复合而非一条规则完成。L-Unload 不带关于目标视图的前提，所以无论纤维去激活期间目标视图变成了什么，累加器都会运行，纤维变成 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾，此后 L-Begin 可立即开启一次新转换。

详细解释

本节处理"即时性"假设的放弃：一次迭代的发起和落定不是同一瞬间——中间有一个异步的"飞行"窗口，期间外部世界可以变化。 这是任何真实运行时都逃不掉的现实：一个组件建立数据库连接、发起 HTTP 请求、等待锁，这些都是异步的，在 await 期间别的纤维完全可能改变系统状态。

核心概念是"惯性"（inertia）。 论文用一个不透明的 𝖥𝗎𝗍𝗎𝗋𝖾(𝐴) 类型抽象异步：迭代发起时返回一个 future，落定时才真正产出 (𝛿, 𝑔, 𝑜)。惯性的含义是"一旦发起，必然落定，不可撤回"——你不能在飞行中途把一个异步操作"取消掉"。这对应真实异步编程里：一个已经发出的网络请求，你通常不能真正"撤回"它，最多忽略它的结果。这是一个非常诚实、非常贴近现实的建模。

本节不增加任何新规则或新类型，只增加一个对 L-Divert 的限制。 这一点极其优雅：在 4.3.2 的 L-Divert 有两种选择——“放弃迭代"或"让迭代落地”。异步层只是禁止宿主使用"放弃迭代"那一种。为什么？因为飞行中的迭代无法被放弃（惯性），所以唯一选择是"让迭代落地"——也就是先把这次异步操作的结果应用上，然后再去激活。这把"异步"从一个全新的机制，简化成"对一个已有规则的一个分支的限制"——体现了本章"分层扩展不增加复杂度"的设计哲学。

为什么必须经 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 而非 𝖠𝖼𝗍𝗂𝗏𝖾 路由？ 这是一个微妙但关键的工程正确性论证。假设一个异步迭代在飞行期间，目标视图变了（比如它的某个依赖被退役了）。迭代必须落地（惯性），落地后它产出了一个逆函数。这时如果让纤维短暂地经过 𝖠𝖼𝗍𝗂𝗏𝖾，它就会在那一步里"暴露"给依赖者——别的纤维可能在这个瞬间看到它激活了、把键解析到它、激活起来。但这个纤维马上就要去激活！依赖者就会激活在一个"正在离开的提供者"上，造成使用后立即失效的灾难。所以必须直接进 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀——它不暴露给任何人，安静地完成回收。这对应实现里"重载与卸载相互链式"（mutual chaining of reload and unload）的语义。

去激活可以链式回到激活。 L-Unload 不看目标视图，所以无论卸载期间目标变成了什么，逆都会运行、纤维变 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾，然后 L-Begin 可以立刻开启新转换。这描述了一个常见模式：组件 A 被替换成组件 B——A 先卸载（目标变 ⊥ 或变 B），卸载完变 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾，然后 B 的 L-Begin 触发。这不是一条新规则，而是已有规则的组合——优雅地复用了 4.3.1/4.3.2 的机制。

与 Cordis/DSH 实践的对应。 这正是异步组件生命周期管理的语义：一个组件的 install 可能 await 一个远程配置加载，在 await 期间系统继续运转；加载完成后，无论中间发生了什么，都必须先把这次加载的副作用安装并准备好逆，然后才能去激活。它也对应"热替换不可中断已发出的异步操作"的现实约束——你不能因为要换掉一个组件就强行 cancel 它正在执行的 IO。进度定理（Theorem 66）明确声明它覆盖受惯性约束的宿主（不使用 L-Divert 的放弃分支），所以异步宿主也在进展性保证之内。

4.3.4 Failure / 失败

原文 (English)

Every rule so far assumes the effect it runs succeeds, and a runtime cannot. The effects a component installs reach outside the context that tracks them, and what they reach may refuse: a port already bound, a file that is not there, a peer that does not answer. A failing transition must still leave the fiber’s effects recovered rather than stranded.

Let Ξ be a set of errors and refine the effect iterator so that an iteration may raise in place of yielding a triple:
𝔈failΓ ≔ 𝜇ℑ. Γ → 𝖤𝗂𝗍𝗁𝖾𝗋(Ξ, Γ × (Γ → Γ) × 𝖬𝖺𝗒𝖻𝖾(ℑ))
The witness constrains the 𝖱𝗂𝗀𝗁𝗍 case alone, being vacuous where the pattern does not match, a raise having nothing to undo, and the 𝑖 that 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 carries is read at 𝔈fail∗Γ from here on. The layer adds one rule and puts the second outcome of Definition 49 to use.

𝜃𝑛 = 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖, 𝑔, 𝜔) 𝑖(𝛾) = 𝖫𝖾𝖿𝗍(𝜉)
──────────────────────────────────────── L-Raise
𝛾 ⟶ 𝛾[𝜃𝑛 ↦ 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, 𝜉)]

L-Raise recovers before it records. The fiber routes into 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 carrying the error as its outcome, the accumulator built up to the failing iteration is applied there, and the fiber arrives at 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜉) having installed nothing, at a state differing from the one an aborting L-Divert would have produced only in the outcome the fiber carries. Routing a failure like every other deactivation is what makes every outcome reachable only through L-Unload, which is the single fact Theorem 59 turns on. L-Begin has 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥) as a premise, so the lifecycle is not re-entered from an error outcome; this is the substance of the outcome, which withholds a fiber whose effect function has shown itself to be unsound in the state it ran against rather than retrying it against an unchanged environment. A failed fiber also obstructs nothing: it is 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾, so it carries no committed view and cannot make relied hold.

A failure is recorded on the fiber rather than propagated to its parent, so a component whose transition fails leaves its siblings running, which is the behavior a plugin host wants and the reason the outcome is per-fiber rather than a property of the whole state.

中文翻译

到此为止的每条规则都假设它运行的效应会成功，而运行时做不到。一个组件安装的效应会触达追踪它们的上下文之外的东西，而那些东西可能拒绝：一个已被绑定的端口、一个不存在的文件、一个不响应的对端。一次失败的转换仍必须让纤维的效应被恢复，而非搁浅。

令 Ξ 为错误集合，把效应迭代器精化为一次迭代可以抛出（raise）以替代产出三元组：
𝔈failΓ ≔ 𝜇ℑ. Γ → 𝖤𝗂𝗍𝗁𝖾𝗋(Ξ, Γ × (Γ → Γ) × 𝖬𝖺𝗒𝖻𝖾(ℑ))
见证只约束 𝖱𝗂𝗀𝗁𝗍 的情形，在模式不匹配处为空满足——一次抛出没什么可撤销的——此后 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 携带的 𝑖 在 𝔈fail∗Γ 上读出。本层增加一条规则，并启用定义49的第二个结果。

L-Raise（抛错）： 当纤维 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 且本次迭代抛出 𝖫𝖾𝖿𝗍(𝜉) 时，把纤维置为 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, 𝜉)，携带错误作为结果。

L-Raise 先恢复再记录。纤维携带错误作为结果路由进 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀，到失败迭代为止构建的累加器在那里被应用，纤维到达 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜉)，什么也没安装——与一个放弃式 L-Divert 所会产生的状态，只在纤维携带的结果上不同。把失败像所有其他去激活一样路由，使每个结果只能经由 L-Unload 到达，这正是定理59所依据的唯一事实。L-Begin 以 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥) 为前提，所以生命周期不会从错误结果重新进入；这就是结果的实质：它扣留一个其效应函数已在它运行所依据的状态下显示出不可靠的纤维，而不是在未改变的环境下重试它。一个失败的纤维也不阻碍任何东西：它是 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾，所以不携带已提交视图，也不能使 relied 成立。

失败记录在纤维上而非传播给其父，所以一个转换失败的组件让其兄弟继续运行——这是插件宿主想要的行为，也是结果是"每纤维"而非"整个状态的属性"的原因。

详细解释

本节放弃最后一个理想化假设——“不会失败”（infallible）。真实运行时里，效应会触达上下文之外的世界，而那个世界会拒绝：端口已被占用、文件不存在、对端不响应。 论文的关键要求是：一次失败的转换仍然必须把已安装的效应恢复掉，而不是让它们搁浅（stranded）在系统里。

L-Raise 的设计哲学是"先恢复，再记录"。 当一次迭代抛出 𝖫𝖾𝖿𝗍(𝜉)，纤维不是直接进入一个"错误"终态，而是先转入 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, 𝜉)——携带错误 𝜉 作为结果。在 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀，到失败迭代为止累积的累加器 𝑔 会被应用（这是 L-Unload 唯一应用累加器的特权），把失败前已经安装的所有效应逐个回收。最终纤维到达 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜉)——什么也没留下。这个状态和一个"放弃式 L-Divert"产生的状态几乎一样，只差纤维携带的结果字段：一个是 ⊥（正常放弃），一个是 𝜉（失败）。这种统一性是刻意的设计：失败被当成"一种特殊的去激活"来处理，与 L-Divert、L-Leave 走同一条 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 → L-Unload 通路。论文说"每个结果只能经由 L-Unload 到达，这正是定理59（保持性）所依据的唯一事实"——意思是，无论纤维以何种方式结束（成功卸载、被转向、失败），它都必然经过 L-Unload 应用累加器，所以"已提交视图不会指向已移除纤维"这一不变式对所有结果统一成立，无需对错误单独证一遍。

结果字段 𝜁 的实质是"扣留而非重试"。 L-Begin 的前提是 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥)——注意是 ⊥，不是 𝜉。所以一个失败的纤维（𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜉)）无法重新进入生命周期：L-Begin 不匹配它。这是有意的：一个效应函数已经在某个状态下表现出"不可靠"（比如在那个状态下绑端口失败），在环境没变的情况下重试它只会再次失败，毫无意义。所以系统选择"扣留"它——让它安静地待在 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜉)，既不重试也不阻碍别人。这对应工程里的"熔断"语义：一个反复失败的组件被标记为失败态，不再被调度，但其失败状态被显式记录，便于宿主诊断或显式重置。

失败是"每纤维"而非"全状态"的。 失败记录在纤维自己身上，不传播给父纤维。所以一个组件转换失败，它的兄弟组件继续运行。论文明确说"这是插件宿主想要的行为"——一个插件装载失败不应该拖垮整个宿主和其他插件。这与传统的异常传播（exception propagation）形成鲜明对比：传统模型里子失败会沿调用栈向上抛、可能让父也失败；而这里的故障隔离（fault isolation）是显式的——每个纤维独立结算，失败不传染。这与 DSH 的故障隔离实践完全对应：一个 agent 子任务失败，不会让父 agent 和兄弟任务都崩溃，而是被隔离在那个任务里。

失败纤维不阻碍任何人。 因为它是 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾，不携带已提交视图，所以 relied 谓词不会因为它而成立——它不会卡住别人的 L-Unload 守卫。这是一个重要的"不添麻烦"性质：失败的组件既不重试、也不挡道，干净地退出舞台。O-Remove 也不需要为错误结果拓宽前提——𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(−) 的通配已经覆盖 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(𝜉)，所以失败的纤维可以像正常静止纤维一样被移除。

与 Cordis/DSH 实践的对应。 这正是"组件装载失败的优雅处理"的形式化：一个插件在初始化时抛异常（比如端口冲突），系统会把它之前已经成功的初始化步骤全部回滚（关掉已打开的文件、已建立的连接），然后把它标记为失败态，不影响其他插件。宿主可以查询哪些插件失败了、为什么失败，决定是否重试或上报。它也是故障隔离的形式化基石：单个组件的失败被限制在该组件的生命周期内，不会级联。

4.4 Metatheory / 元理论

原文 (English)

Section 4.3 supplies ten rules: the three orchestration rules of Section 4.2; L-Begin, L-Iter, and L-Finish for an activation; L-Divert and L-Raise for the two ways an activation may end early; and L-Leave and L-Unload for a deactivation. This section reads the two dimensions of composability off those rules in their global form, one fiber’s guarantee holding whatever the other fibers do in between, and adds what only a whole system can be asked for: that it always reaches the configuration its targets call for, and that the configuration is the one a static assembly would have produced.

Definition 53. Index the steps by 𝑡, so that 𝛾𝑡 is the state the first 𝑡 of them reach, and write step𝑡 ≔ 𝑟(𝑛) for the step taken at 𝛾𝑡: the rule 𝑟 it applies and the name 𝑛 it applies that rule at. The sequence starts at a 𝛾0 with dom(𝐹0) = ⌀. An episode of 𝑛 is a maximal interval [𝑏, 𝑢] of indices throughout which installed𝑛 holds.

Every rule concludes in the shape 𝛾 ⟶ 𝛿[⋯]. The state map of a step taken at 𝛾𝑡 by a rule acting on 𝑛 is
Ψ𝑡 ≔ { pr1 ∘ 𝑖 at L-Iter, L-Finish, and a landing L-Divert; 𝑔 at L-Unload; idΓ at every other rule }
and the edit edit𝑡 : Γ → Γ is the bracket read as a function. Each step factors as 𝛾𝑡+1 = edit𝑡(Ψ𝑡(𝛾𝑡)).

Lemma 54. Reading Table 1 together with Definition 48, for every step 𝑡 and all fibers 𝑚, 𝑛 present at 𝛾𝑡:

Lemma 55 (≃-invariance). Let 𝛾 ≃ 𝛾′. Then a rule of Section 4.3 applies at 𝛾 acting on 𝑛 if and only if it applies at 𝛾′ acting on 𝑛, and the states the two applications reach are again related by ≃.

Lemma 56 (Equivariance). Let 𝜒 : 𝔑 → 𝔑 be a bijection. Then 𝜒 ⋅ 𝛾 is a state, well formed where 𝛾 is, and step𝑡 = 𝑟(𝑛) carries 𝛾𝑡 to 𝛾𝑡+1 if and only if 𝑟(𝜒(𝑛)) carries 𝜒 ⋅ 𝛾𝑡 to 𝜒 ⋅ 𝛾𝑡+1.

Lemma 57 (Vestigial entries). Call 𝑛 vestigial at 𝛾 when 𝜏𝑛 = ⊤, 𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥), 𝜎𝑛 = ⌀, and no 𝑚 has 𝜋𝑚 = 𝑛; a vestigial entry satisfies 𝛾 ≈ 𝛾 ∖ 𝑛. If 𝑛 is vestigial at 𝛾 then for every rule and every 𝑚 ≠ 𝑛: a rule applying at 𝛾 acting on 𝑚 applies at 𝛾 ∖ 𝑛, and conversely, unless it is an O-Insert drawing the name 𝑛 or claiming a key of 𝑝𝑛.

中文翻译

第4.3节给出十条规则：第4.2节的三条编排规则；激活用的 L-Begin、L-Iter、L-Finish；激活可能提前结束的两种方式的 L-Divert 和 L-Raise；以及去激活的 L-Leave 和 L-Unload。本节从这些规则的全局形式中读出可组合性的两个维度——一个纤维的保证无论其他纤维在中间做什么都成立——并加上只有整个系统才能被要求的东西：它总能达到其目标所要求的配置，且该配置是静态装配本会产生的那个。

定义 53。 用 𝑡 给步骤编号，𝛾𝑡 是前 𝑡 步达到的状态，记 step𝑡 ≔ 𝑟(𝑛) 为在 𝛾𝑡 迈出的步骤：它应用的规则 𝑟 与它应用该规则的名 𝑛。序列从 dom(𝐹0) = ⌀ 的 𝛾0 开始。纤维 𝑛 的一幕（episode）是 installed𝑛 持续成立的指标极大区间 [𝑏, 𝑢]。

每条规则结论形如 𝛾 ⟶ 𝛿[⋯]。在 𝛾𝑡 由作用于 𝑛 的规则迈出的一步，其状态映射为
Ψ𝑡 ≔ { L-Iter、L-Finish、落地式 L-Divert 处取 pr1 ∘ 𝑖；L-Unload 处取 𝑔；其他每条规则取 idΓ }
编辑 edit𝑡 是把方括号读作函数。每一步分解为 𝛾𝑡+1 = edit𝑡(Ψ𝑡(𝛾𝑡))。

引理 54。 结合表1与定义48，对每一步 𝑡 与 𝛾𝑡 处所有纤维 𝑚, 𝑛：

引理 55（≃-不变性）。 令 𝛾 ≃ 𝛾′。则第4.3节的一条规则在 𝛾 作用于 𝑛 可应用，当且仅当它在 𝛾′ 作用于 𝑛 可应用，且两次应用达到的状态仍由 ≃ 关联。

引理 56（等变性）。 令 𝜒 : 𝔑 → 𝔑 为双射。则 𝜒 ⋅ 𝛾 是状态，在 𝛾 良构处良构，且 step𝑡 = 𝑟(𝑛) 把 𝛾𝑡 带到 𝛾𝑡+1 当且仅当 𝑟(𝜒(𝑛)) 把 𝜒 ⋅ 𝛾𝑡 带到 𝜒 ⋅ 𝛾𝑡+1。

引理 57（残留条目）。 称 𝑛 在 𝛾 处残留（vestigial），若 𝜏𝑛 = ⊤、𝜃𝑛 = 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥)、𝜎𝑛 = ⌀、且无 𝑚 使 𝜋𝑚 = 𝑛；残留条目满足 𝛾 ≈ 𝛾 ∖ 𝑛。若 𝑛 在 𝛾 残留，则对每条规则与每个 𝑚 ≠ 𝑛：在 𝛾 作用于 𝑚 的规则也在 𝛾 ∖ 𝑛 作用于 𝑚，反之亦然，除非它是抽取名 𝑛 或申领 𝑝𝑛 之键的 O-Insert。

详细解释

本节是整章元理论的"基础设施层"，为后续五个性质定理建立一套统一的证明语言和若干引理。理解本节的关键是把握"把规则读作对状态的写"这一统一切入视角。

核心思路：把每条规则分解为"状态映射 Ψ𝑡"加"编辑 edit𝑡"两部分。 Ψ𝑡 是真正改写上下文内容的函数（在迭代落地时是迭代器的前向投影 pr1 ∘ 𝑖，在 L-Unload 时是累加器 𝑔，其他时候是恒等 idΓ），edit𝑡 是只改控制字段（生命周期状态、退役标志等）的赋值。于是每一步都是 𝛾𝑡+1 = edit𝑡(Ψ𝑡(𝛾𝑡))。这种分解把"内容变更"和"控制字段变更"清晰地分开——这是后续所有证明的基础设施。表1正是把十条规则读成这种"写"的完整清单，使每个证明都变成"查表"。

引理54是"事实清单"引理，它从表1 + 定义48（约束性）中读出五条贯穿全章的事实：(1) 一个纤维的表只在自己被作用时变，且变更在 Ψ𝑡 内——这是约束性的直接后果；(2) 已提交视图 𝜔 只在 L-Begin 产生、只在 L-Unload 消失，所以在一个 episode（纤维从激活到卸载的整个区间）内 𝜔 保持不变——这是空间可组合性（4.4.3）的核心不变式；(3) 累加器只在 L-Unload 应用——这是恢复精确性的关键；(4) 纤维安装/卸载的边界恰是 L-Begin/L-Unload；(5) 𝜋/𝑑/𝑝/𝑒 一旦随条目产生就不再被写，𝜏 单调——这保证依赖图与供给在运行中是稳定的。这五条事实在后续每个定理证明里反复引用，相当于把"查表"的结果固化。

引理55（≃-不变性）保证整个演算下降到观察等价商 Γ/≃。 它说的是：如果两个状态在观察等价 ≃ 下相等（即对所有可观察的东西一致），那么规则在两者上的可应用性相同、结果仍 ≃ 相等。这意味着规则的判断只依赖可观察量，不会因为"不可观察的内部表示差异"而分歧。这是把第3章的观察等价性贯穿到组件层的桥梁——证明中它逐一检查每条规则的前提只读 ≃ 保持的成分（控制字段、𝑑/𝑝/𝑒、目标视图、dom(𝐹𝛾)），结论里的写也都尊重 ≃。

引理56（等变性）处理纤维名的匿名性。 纤维名是"动态创建的局部名"（引用[39]），规则只用相等比较、不计算、不检查结构。所以对纤维名的任何双射重命名，规则序列保持相同结构。这让证明可以"忽略具体用了哪些名"，只关心结构——这是 4.1 节"名是原子"纪律的兑现。后续汇合性定理在匹配两棵注册树时正是用一个双射对齐它们的名字。

引理57（残留条目）是一个"看不见的条目"引理。 一个"残留"纤维是：已退役、已静止、空表、没人以它为父——它只剩一个名字壳。引理说这样的条目对任何作用于其他纤维的规则都不可见（𝛾 ≈ 𝛾 ∖ 𝑛）。这非常重要：定义47的注册原语在父卸载时退役子纤维、留下一个残留条目（Lemma 57 提到的"退化条目"），它和"纤维不存在"在控制字段以外无法区分。这个引理让证明可以"假装残留条目不存在"，是汇合性证明里删除被退役注册（Lemma 72）的工具。

两个等价关系 ≃ 与 ≈ 的分工。 ≃ 是观察等价（含注册表域和控制字段），用于"规则是否区分两个状态"；≈ 是"除控制字段外一致"，用于恢复精确性——它精确比较表与环境状态，只忘掉"哪个纤维安装的"。论文明确说 ≃ 和 ≈ 互不精化，各自忘掉对方必须保留的东西：≃ 必须保留控制字段（规则靠它判断），≈ 必须保留表与环境（恢复精确性是关于效应的断言）。后续定理对两半各用其一。

总之，本节建立了一套"把规则当写、把状态当索引序列、用 ≃/≈ 两个等价分别读两半"的统一证明框架，五个性质定理都在其上展开。

4.4.1 Preservation / 保持性

原文 (English)

Definition 45 fixes the shape of a registry, and the rules have to be checked against it before the results below can add to it. This subsection identifies the invariant the rules preserve, of which the first clause is that shape and the rest what those results assume.

Definition 58. A registry 𝐹𝛾 is well formed when, for all 𝑚, 𝑛 ∈ dom(𝐹𝛾) and all 𝑘 ∈ 𝐾:

Clause (1) is the tree of Definition 45 read one edge at a time. The acyclicity needs no clause, since the fiber a pointer names is registered before the fiber naming it.

Theorem 59 (Preservation). If 𝐹𝑡 is well formed then so is 𝐹𝑡+1, whichever rule step 𝑡 applies. Each clause is established at 𝛾𝑡+1 from all four at 𝛾𝑡.

The guard on L-Unload is what carries clauses (3) and (4). The premise ∀𝑚. 𝜋𝑚 ≠ 𝑛 of O-Remove speaks only of parent pointers; what keeps a committed view from naming a removed fiber is the guard, imposed several steps earlier and for a different reason. Because a failure is routed through 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 as well, the argument does not have to be repeated for an error outcome. Two things follow that the base calculus does not enjoy. A name freed by O-Remove may be reissued by O-Insert, since no stale committed view can name it; and a fiber may be removed as soon as it is 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾, without a separate check that nobody depends on it.

中文翻译

定义45固定了注册表的形状，规则必须先对照它检查，后续结果才能在其上添加。本小节识别规则所保持的不变式，其第一条是该形状，其余是那些结果所假定的。

定义 58。 注册表 𝐹𝛾 良构（well formed），当对所有 𝑚, 𝑛 ∈ dom(𝐹𝛾) 与所有 𝑘 ∈ 𝐾：

第(1)条是定义45的树按一条边读出。无环性无需条款，因为指针所命名的纤维先于命名它的纤维注册。

定理 59（保持性）。 若 𝐹𝑡 良构，则无论第 𝑡 步应用哪条规则，𝐹𝑡+1 也良构。每条条款在 𝛾𝑡+1 处由 𝛾𝑡 处全部四条建立。

L-Unload 上的守卫承载了条款(3)与(4)。O-Remove 的前提 ∀𝑚. 𝜋𝑚 ≠ 𝑛 只涉及父指针；使已提交视图不命名已移除纤维的，是守卫——它在几步之前为另一个理由施加。因为失败也经 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 路由，该论证不必为错误结果重复。随之而来的是基础演算所不享有的两件事：O-Remove 释放的名可由 O-Insert 重新签发，因为没有陈旧的已提交视图能命名它；且一个纤维一旦 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 就可被移除，无需单独检查无人依赖它。

详细解释

保持性（preservation）是类型论/操作语义里最经典的不变式：“如果系统现在处于良好状态，迈一步后仍处于良好状态。” 本节定义了注册表的良构性（Definition 58，四条），并证明十条规则都保持它（Theorem 59）。

四条良构条款的含义。 (1) 父指针落在注册表或根里——注册表始终是一棵良形的树；(2) 不同纤维的供给不相交——单一来源纪律，每个键至多一个提供者；(3) 一个已安装纤维的已提交视图是它声明的依赖键到注册表内纤维名的全映射——即它声明的每个依赖都解析到了某个存在的纤维；(4) 如果已安装纤维 𝑛 把键 𝑘 解析到 𝑚，那么 𝑚 也是已安装的——即已提交视图只指向同样已安装的提供者。第(3)(4)条合起来就是"激活的纤维依赖的提供者也都激活着"，这是空间可组合性的形状保证。

证明梗概： Theorem 59 对四条分别归约。第(1)条由 O-Insert（前提保证新纤维的父存在）与 O-Remove（前提 ∀𝑚.𝜋𝑚≠𝑛 保证无幸存者以被删者为父）维护。第(2)条由 O-Insert 的最后一前提维护，且无其他规则写 𝑝 或扩大 dom(𝐹𝛾)。第(3)条：唯一写 𝜔 的是 L-Begin，其前提 𝜔 = target ≠ ⊥ 保证它是全的、取值于提供者；唯一缩小 dom(𝐹𝛾) 的 O-Remove 删除的是非安装纤维。第(4)条是关键且最微妙的一步——它可能被"某安装纤维掉落"“某 𝜔 被写”"某被 𝜔 命名的纤维离开"破坏。核心在于 L-Unload 的守卫 ¬ relied𝑛(𝛾)：当一个提供者要卸载时，守卫要求没有任何已安装纤维还把键解析到它，于是被它提供的消费者要么也已不在安装状态、要么已提交视图不再指向它——所以删掉它不会让任何已安装纤维的 𝜔 指向虚空。论文特别强调：O-Remove 的前提 ∀𝑚.𝜋𝑚≠𝑛 只管父指针，真正阻止"已提交视图指向已删纤维"的是 L-Unload 守卫——它在好几步之前、为"撤回顺序"这个完全不同的理由被施加，却顺带保护了第(4)条。这种"一个机制服务多个不变式"的复用是本章设计的优雅之处。

失败也走 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 通路的好处。 因为 L-Raise 把失败也路由进 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀，4.3.4 的论证与正常卸载同构，所以第(3)(4)条对错误结果自动成立，无需单独再证一遍——这是 4.3.4 "失败当作特殊去激活"设计的回报。

保持性带来的两个工程红利。 第一，O-Remove 释放的纤维名可以被 O-Insert 重新签发——因为没有陈旧的已提交视图能指向已删名（守卫保证任何指向它的视图都已随依赖者卸载而消失）。这对应"插件名可被复用"：卸载一个叫 “logger” 的插件后，可以再装载一个同名插件，不会因为旧引用而混乱。第二，一个纤维一旦 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾 就可立即 O-Remove，无需额外检查"没人依赖我"——因为守卫已经在它离开 𝖠𝖼𝗍𝗂𝗏𝖾 时（L-Leave→L-Unload）保证了这一点。这简化了实现：退役一个静止纤维是安全的，不用再做依赖扫描。这与 Cordis/DSH 的依赖解析、组件生命周期管理直接对应——卸载一个插件不需要全系统扫描谁还在用它，守卫已经替你扫过了。

4.4.2 Temporal Composability / 时间可组合性

原文 (English)

Local temporal composability recovers one sequence of effects with one accumulator (Section 3.1.3). The registry holds one accumulator per fiber and the fibers interleave: between the moment 𝑛 composes an inverse onto 𝑔𝑛 and the moment 𝑔𝑛 runs, other fibers have moved the state. Whether 𝑔𝑛 still undoes what it was built to undo there is what the global form of the guarantee asserts, and the condition it turns on is that the intervening steps commute with 𝑔𝑛.

Definition 60. For 𝑖 ∈ 𝔈iter∗Γ let reach(𝑖) be the least set of iterators containing 𝑖 and closed under continuation, and read the transformation monoid 𝔐 at an iterator by taking for its generators the forward maps and the yielded inverses of every iterator in reach(𝑖). Two iterators 𝑖, 𝑗 are independent when:
∀𝑓 ∈ 𝔐(𝑖), 𝑔 ∈ 𝔐(𝑗). 𝑓 ∘ 𝑔 ≃ 𝑔 ∘ 𝑓
∀𝑖′ ∈ reach(𝑖), 𝑔 ∈ 𝔐(𝑗), 𝛾 ∈ Γ. pr2,3(𝑖′(𝑔(𝛾))) ≃ pr2,3(𝑖′(𝛾))
and symmetrically in 𝑗. A family (𝑖𝑙) is pairwise independent when 𝑖𝑙 and 𝑖𝑙′ are independent for every 𝑙 ≠ 𝑙′, and a sequence of steps is pairwise independent when (𝑒𝑛) is, where 𝑁 is the set of names the sequence ever holds.

Theorem 61 (Recovery exactness). Let the sequence of steps be pairwise independent, let an episode of 𝑛 open at 𝑏, let 𝑢 ≥ 𝑏 lie in it, and let 𝑡1 < ⋯ < 𝑡𝑙 be the indices in [𝑏, 𝑢) at which the acting fiber is not 𝑛. Then
𝑔𝑢𝑛(𝛾𝑢) ≈ (Ψ𝑡𝑙 ∘ ⋯ ∘ Ψ𝑡1)(𝛾𝑏)
That is, applying 𝑛’s accumulator at 𝛾𝑢 yields, up to the control fields, the state those same steps would have produced from 𝛾𝑏.

Corollary 62 (Terminal recovery). Let the sequence of steps be pairwise independent and let an episode of 𝑛 open at 𝑏 and close at 𝑢, whatever outcome 𝑛 arrives at. Then, with 𝑡1 < ⋯ < 𝑡𝑙 as in Theorem 61,
𝛾𝑢+1 ≈ (Ψ𝑡𝑙 ∘ ⋯ ∘ Ψ𝑡1)(𝛾𝑏)
A fiber removed by O-Remove leaves nothing behind either.

Pairwise independence is assumed of the components by the results above, and Section 3.3.2 is what discharges it: where every effect a component performs is an operation of a key and every key is commutative, any two effect functions built from those operations are independent (Theorem 42). The coeffect operations of Section 3.2 are the case that needs no hypothesis at all: the maps a component contributes there are composites of set operations and of the corresponding restrictions, two such commute whenever they touch disjoint keys, and clause (2) of Definition 58 makes the provisions of distinct fibers disjoint.

中文翻译

局部时间可组合性用一个累加器恢复一串效应（第3.1.3节）。注册表每个纤维持有一个累加器，而纤维交错运行：在 𝑛 把一个逆组合到 𝑔𝑛 上、与 𝑔𝑛 实际运行之间，其他纤维已移动了状态。𝑔𝑛 是否仍撤销它被构建来撤销的东西，正是该保证的全局形式所断言的，而它所依赖的条件是：中间这些步骤与 𝑔𝑛 交换。

定义 60。 对 𝑖 ∈ 𝔈iter∗Γ，令 reach(𝑖) 为含 𝑖 且对续延封闭的最小迭代器集合，把变换幺半群 𝔐 在迭代器上读作以 reach(𝑖) 中每个迭代器的前向映射与所产逆为生成元。两个迭代器 𝑖, 𝑗 独立（independent）当：
∀𝑓 ∈ 𝔐(𝑖), 𝑔 ∈ 𝔐(𝑗). 𝑓 ∘ 𝑔 ≃ 𝑔 ∘ 𝑓
∀𝑖′ ∈ reach(𝑖), 𝑔 ∈ 𝔐(𝑗), 𝛾 ∈ Γ. pr2,3(𝑖′(𝑔(𝛾))) ≃ pr2,3(𝑖′(𝛾))
且在 𝑗 中对称。一个族群两两独立当每对 𝑙 ≠ 𝑙′ 的 𝑖𝑙, 𝑖𝑙′ 独立；一个步骤序列两两独立当序列所持名集合 𝑁 上的 (𝑒𝑛) 两两独立。

定理 61（恢复精确性）。 令步骤序列两两独立，令 𝑛 的一幕在 𝑏 开启，𝑢 ≥ 𝑏 在其中，令 𝑡1 < ⋯ < 𝑡𝑙 为 [𝑏, 𝑢) 中作用纤维非 𝑛 的指标。则
𝑔𝑢𝑛(𝛾𝑢) ≈ (Ψ𝑡𝑙 ∘ ⋯ ∘ Ψ𝑡1)(𝛾𝑏)
即在 𝛾𝑢 处应用 𝑛 的累加器，得到（控制字段以外）那些相同步骤本会从 𝛾𝑏 产生的状态。

推论 62（终态恢复）。 令步骤序列两两独立，令 𝑛 的一幕在 𝑏 开启、在 𝑢 关闭，无论 𝑛 到达何种结果。则
𝛾𝑢+1 ≈ (Ψ𝑡𝑙 ∘ ⋯ � Ψ𝑡1)(𝛾𝑏)
被 O-Remove 移除的纤维也不留下任何东西。

上述结果把两两独立性假设于组件，而第3.3.2节正是消解它之处：当组件执行的每个效应都是某个键的操作、且每个键都交换时，由这些操作构建的任意两个效应函数都独立（定理42）。第3.2节的协同效应操作是完全无需假设的情形：组件在那里贡献的映射是集合操作与相应限制的复合，两个这样的映射只要触及不相交的键就交换，而定义58的条款(2)使不同纤维的供给不相交。

详细解释

时间可组合性（temporal composability）回答的是这个全局问题：当一个纤维 𝑛 在某状态 𝛾𝑏 下构建了累加器 𝑔𝑛（一串逆函数），然后其他纤维在中间插队执行了一堆步骤，把状态推进到 𝛾𝑢——这时再运行 𝑔𝑛，它还能精确撤销 𝑛 当初安装的东西吗？还是已经被中间的步骤"污染"了？ 这是把第3章的局部恢复精确性（单个组件、单线程）推广到多纤维交错的全局场景。

核心条件是"两两独立性"（pairwise independence）。 定义60把第3章的独立性（Definition 19）扩展到迭代器：两个纤维的效应迭代器独立，意味着它们产生的所有前向映射和逆函数两两交换（𝑓 ∘ 𝑔 ≃ 𝑔 ∘ 𝑓），且一个迭代器在另一个映射作用过的状态上产出的逆与续延不变。第一条件是"映射可交换"（trace 理论里重排相邻独立动作保持终点的基础，引用[44]）；第二条件更强，Theorem 73 还需要它——因为重排两个纤维的步骤意味着在一个被另一纤维移动过的状态上求值迭代器，光映射可交换还不够，还要保证迭代器在那里产出同样的逆和续延。

Theorem 61（恢复精确性）的含义。 它说：在 𝑛 的整个 episode（从 L-Begin 到 L-Unload）内，𝑛 的累加器 𝑔𝑢𝑛 在最终状态 𝛾𝑢 上运行，得到的状态（控制字段以外）恰好等于"那些非 𝑛 的中间步骤单独从 𝛾𝑏 跑出来的状态"。换句话说，𝑛 的安装与卸载在整体效果上是"净零"的——它装了什么、卸了什么，对环境的净影响就是零，仿佛 𝑛 从未存在过。这是局部时间可组合性"一个累加器恢复一串效应"的全局版本：即使中间被别的纤维插了一脚，𝑔𝑛 仍然精确撤销 𝑛 自己的贡献，不多不少。右式读作"假如 𝑛 从未开始"还要额外假设 𝑛 注册的子纤维也没在区间内行动。

证明梗概： 对 𝑢 归纳。𝑛 自己的步骤分两类——迭代落地类（L-Iter/L-Finish/落地 L-Divert）使 𝑔𝑛+1 = 𝑔𝑛 ∘ ℎ，结合见证条件 ℎ(Ψ𝑢(𝛾𝑢)) ≃ 𝛾𝑢 得 𝑔𝑛+1(𝛾𝑢+1) ≈ 𝑔𝑛(𝛾𝑢)，归纳假设不变传递；非落地类（L-Leave/L-Raise/放弃 L-Divert/O-Retire）使 𝑔𝑛 不变。𝑚 ≠ 𝑛 的步骤使 𝑔𝑛 不变但 Ψ𝑢 ∈ 𝔐(𝑒𝑚)，由独立性 𝑔𝑛(𝛾𝑢+1) ≈ Ψ𝑢(𝑔𝑛(𝛾𝑢))，归纳假设把 Ψ𝑢 追加进去。整个证明就是 Theorem 7 的计算一步一步搬过来，独立性在每个非 𝑛 步骤处把 𝑔𝑛 与 Ψ𝑢 交换。

Corollary 62（终态恢复）的含义。 当 episode 关闭（𝑛 的 L-Unload 执行了），由引理54(4) 该步是 L-Unload，由引理54(3) Ψ𝑢 = 𝑔𝑛，所以 𝛾𝑢+1 ≈ 𝑔𝑛(𝛾𝑢)，直接套 Theorem 61。这说无论 𝑛 以何种结果结束（正常、被转向、失败），它关闭后留下的状态等于"𝑛 从未开始"的状态——失败纤维的贡献为零。O-Remove 移除的纤维也什么都不留。这是汇合性（4.4.5）的基石：任何动态历史都不留痕迹。

独立性如何消解？ 论文指出第3.3.2节正是消解点：如果组件的每个效应都是某个键的操作、且每个键都交换（commutative），那么任意两个由这些操作构建的效应函数都独立（Theorem 42）。协同效应操作是完全无需假设的情形：组件贡献的映射是集合操作（增删键值）与相应限制的复合，两个这样的映射只要触及不相交的键就交换，而定义58的条款(2)（供给不相交）恰好保证了不同纤维触及不相交的键。这是一个美妙的闭环：4.1 的供给不相交性 → 协同效应操作自动独立 → 时间可组合性自动成立。工程上，这意味着只要组件遵守"只写自己声明的键、键操作可交换"的纪律，多组件并发交错就保证恢复精确，无需额外的锁或协调。

与 Cordis/DSH 实践的对应。 这正是"热重载/动态装卸载不留脏状态"的理论保证：一个插件被装载、运行一段时间、又被卸载，期间其他插件也在并发运行、改状态——但卸载后系统状态（除控制字段外）等同于这个插件从未被装载过。这让"反复装载-卸载-重装载"是安全的，不会累积残留。它也是故障隔离的时间维度：一个失败组件的副作用被精确回滚，不会因为别的组件在中间动了状态而回滚不干净。

4.4.3 Spatial Composability / 空间可组合性

原文 (English)

Local spatial composability holds a component to its own specification, activating it only where its dependencies are provided and classifying every context change against them (Section 3.2.2). The global form adds what quantifies over other fibers: a provider withdraws a binding only after every dependent that resolved it has deactivated, and the resolution a transition installs its effects against does not shift under it. Two properties of the coeffect side deliver the two, proved together as two halves of one invariant, namely the fixity of 𝜔𝑛 over an episode that Lemma 54(2) establishes. The ordering theorem is what that fixity buys over the part of the episode in which 𝑛 is 𝖠𝖼𝗍𝗂𝗏𝖾 and then 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀, and the coherence theorem what it buys over the part in which 𝑛 is installing its effects.

Theorem 63 (Ordering). A fiber begins a transition only where its dependencies are provided:
step𝑡 = L-Begin(𝑚) ⇒ 𝛾𝑡 ⊧ 𝑑𝑚
Let further [𝑏′, 𝑢′] be an episode of 𝑚 with 𝜔𝑏′𝑚(𝑘) = 𝑛 for some 𝑚 ≠ 𝑛 and 𝑘 ∈ 𝑑𝑚, let [𝑏, 𝑢] be the episode of 𝑛 containing 𝑏′, and let 𝑡 range over [𝑏′, 𝑢′]. Then:

Theorem 64 (Resolution coherence). Let an episode [𝑏, 𝑢] of 𝑛 open at 𝑏 with 𝜔𝑏𝑛 = 𝜔. Then 𝜃𝑛 is 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(−, −, −) on an initial interval [𝑏, 𝑟] of the episode, and every iteration of the transition runs against the one resolution 𝜔:
∀𝑡 ∈ [𝑏, 𝑟]. step𝑡 ∈ {L-Iter(𝑛), L-Finish(𝑛)} ⇒ target𝑡𝑛 = 𝜔
Where the fiber leaves that interval, so that 𝑟 < 𝑢, exactly one of the following holds:

中文翻译

局部空间可组合性把组件约束在自己的规约上：只在依赖被提供处激活它，并把每次上下文变更对照依赖分类（第3.2.2节）。全局形式加上量化于其他纤维的内容：一个提供者只有在其每个解析到它的依赖者都已去激活后才撤回一个绑定，且一次转换安装效应所依据的解析不在它底下移动。协同效应侧的两个性质给出这两点，作为同一不变式——引理54(2)确立的 𝜔𝑛 在一幕中的固定性——的两半一起证明。排序定理是这一固定性在 𝑛 为 𝖠𝖼𝗍𝗂𝗏𝖾 然后 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 的那部分幕上换来的，而相干定理是它在 𝑛 安装效应的那部分幕上换来的。

定理 63（排序）。 一个纤维只在依赖被提供处开始转换：
step𝑡 = L-Begin(𝑚) ⇒ 𝛾𝑡 ⊧ 𝑑𝑚
进一步令 [𝑏′, 𝑢′] 为 𝑚 的一幕，其中 𝜔𝑏′𝑚(𝑘) = 𝑛 对某 𝑚 ≠ 𝑛 与 𝑘 ∈ 𝑑𝑚 成立，令 [𝑏, 𝑢] 为含 𝑏′ 的 𝑛 的一幕，𝑡 遍历 [𝑏′, 𝑢′]。则：

定理 64（解析相干性）。 令 𝑛 的一幕 [𝑏, 𝑢] 在 𝑏 开启且 𝜔𝑏𝑛 = 𝜔。则 𝜃𝑛 在该幕的初始区间 [𝑏, 𝑟] 上为 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(−, −, −)，且转换的每次迭代都依据同一个解析 𝜔 运行：
∀𝑡 ∈ [𝑏, 𝑟]. step𝑡 ∈ {L-Iter(𝑛), L-Finish(𝑛)} ⇒ target𝑡𝑛 = 𝜔
当纤维离开该区间，即 𝑟 < 𝑢 时，恰有其一成立：

详细解释

空间可组合性（spatial composability）回答的是这个全局问题：多个纤维并发存在时，"谁该先激活、谁该后卸载、依赖解析会不会在转换中途被换掉"这些跨纤维的因果约束是否成立？ 它由两个定理共同保证，二者都建立在引理54(2)的同一不变式上：已提交视图 𝜔𝑛 在 𝑛 的整个 episode 内保持不变。

Theorem 63（排序）有三层含义。 第一层是"激活有前提"：L-Begin 只在 𝛾𝑡 ⊧ 𝑑𝑚 时发生——即依赖都满足才激活，这是 L-Begin 前提 target ≠ ⊥ 的直接读出。第二层是核心的"提供者活过消费者"：如果一个消费者 𝑚 在其 episode 中把键 𝑘 解析到提供者 𝑛，那么(1)整个 𝑚 的 episode 期间 𝜔𝑚(𝑘) 始终是 𝑛（已提交视图不变）；(2) 𝑛 的 episode 严格包含 𝑚 的——𝑛 先开始（𝑏 < 𝑏′）、后结束（𝑢′ < 𝑢）。即提供者一定先于消费者激活、后于消费者卸载——这正是 4.3.1 撤回守卫要交付的"依赖只有在依赖者都去激活后才撤回"。第三层是"值稳定"：在 𝑚 的 episode 期间，𝑘 在 𝑛 表里的值不变（𝜎𝑡𝑛(𝑘) = 𝜎𝑏′𝑛(𝑘)），因为 𝑛 在此期间只能是 𝖠𝖼𝗍𝗂𝗏𝖾 或 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀，L-Leave 是唯一可能作用于它的规则且 Ψ=idΓ 不改表。

证明梗概： (1) 直接是引理54(2)。(2) 𝑚 的 L-Begin 在 𝑏′−1 写 𝜔𝑏′𝑚 = target，target 的值是提供者，故 𝑛 在 𝑏′ 已 𝖠𝖼𝗍𝗂𝗏𝖾；而 𝑛 的 L-Begin 在 𝑏−1 留下 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀，故 𝑏 ≠ 𝑏′，即 𝑏 < 𝑏′。若 𝑛 的 episode 在 𝑢 关闭且 𝑢 ≤ 𝑢′，则 𝑢 ∈ [𝑏′,𝑢′]，由(1) 𝜔𝑢𝑚(𝑘)=𝑛 即 relied𝑢𝑛，但 𝑢 处的 L-Unload 否认 relied——矛盾，故 𝑢′ < 𝑢。(3) 由(2) 𝑛 的 L-Unload 在 [𝑏′,𝑢′] 之外，且 𝑛 在 [𝑏′,𝑢′] 起点已是 𝖠𝖼𝗍𝗂𝗏𝖾，故只有 L-Leave 可能作用于 𝑛，其 Ψ=idΓ，表不变。整个证明的力量来自 L-Unload 守卫 ¬ relied：它正是阻止"提供者在消费者还活着时卸载"的机制，排序性是守卫的回报。

Theorem 64（解析相干性）解决"多阶段激活中途依赖被换"的问题。 它说：𝑛 的 episode 开头有一段 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 区间 [𝑏, 𝑟]，在这段里每次迭代都依据同一个解析 𝜔 运行（target𝑡𝑛 = 𝜔）。离开这段只有两种情况：要么 L-Finish 成功进入 𝖠𝖼𝗍𝗂𝗏𝖾(−, 𝜔)（带着原解析激活）；要么 L-Divert/L-Raise 退出，episode 关闭且按推论62净零恢复。关键在于：一个多阶段转换绝不会"装了一半发现解析变了还继续装"——L-Iter/L-Finish 带 target=𝜔 前提，一旦 target 偏离 𝜔 就走 L-Divert 退出。L-Raise 不看 target（抛错是迭代自己的事，不是环境要求的），任何情况下都退出转换。两个变化方向不分彼此：依赖消失（target 变 ⊥）和依赖被替换（target 变别的纤维）都同样使 target ≠ 𝜔，走同一条退出路径。

惯性的边界。 论文诚实指出：如果一次迭代正在异步飞行时 target 转了，惯性使它必须落地（4.3.3），落地的迭代装了一个依据"已不再成立"的解析算出的效应。所以规则交付的是一个析取：要么 target 没变、装的是一致的；要么 target 变了、走 L-Divert 净零退出。第二个分支正是让第一个分支安全的原因——没有"装了一半"的中间态留存。

与 Cordis/DSH 实践的对应。 排序定理对应"依赖解析的稳定性"：一旦一个组件激活时把它的依赖解析到具体实例，整个生命周期里这些解析不会偷偷换掉——它用的始终是同一个 logger、同一个数据库连接池。这避免了"组件 A 用着 logger v1，中途系统把 logger 换成 v2，A 还以为自己在用 v1"的混乱。解析相干性对应"多阶段初始化的一致性"：一个组件分阶段激活时，所有阶段都基于同一份依赖快照，不会"第一阶段用 v1、第二阶段用 v2"。这二者合起来就是空间可组合性——组件在空间上（相对于其他组件）的行为是可预测、不随他人动作而漂移的。这与 DSH 的依赖注入、热重载中"替换一个服务要先卸载所有使用者、再装载新版本"的纪律完全对应。

4.4.4 Progress / 进展性

原文 (English)

A guard that defers a provider’s withdrawal until its dependents are gone delivers Theorem 63 only if it eventually releases. One relation on the fibers of a registry carries the argument.

Definition 65. The precedence relation on the names of a registry is
𝑛 ≺ 𝑚 ≔ 𝑝𝑛 ∩ 𝑑𝑚 ≠ ⌀
so that 𝑛 may provide a key 𝑚 declares. It reads 𝑑 and 𝑝 alone, which by Lemma 54(5) come into existence with a fiber’s entry and are never written again.

Theorem 66 and Theorem 73 are established on the hypothesis that ≺ is acyclic, which is an assumption and not something the definition delivers, 𝑛 ≺ 𝑛 holding of a component that declares a key it provides itself. What ≺ orders is the two fibers’ activations and not their lifetimes: 𝑛 ≺ 𝑚 says that 𝑛 has to become 𝖠𝖼𝗍𝗂𝗏𝖾 before 𝑚 can, whereas that a provider outlives its consumer is Theorem 63(2).

Theorem 66 (Progress). Assume ≺ acyclic, len(𝑒𝑛) ≤ 𝐾 for every 𝑛, and the set 𝑁 of names finite; and let every step apply a lifecycle rule. Write 𝑆(𝑛) for the number of steps acting on 𝑛 and 𝑉(𝑛) ≔ |{𝑡 : target𝑡𝑛 ≠ target𝑡+1𝑛}| for the number of times its target view turns. Then:

Finiteness of 𝑁 is assumed rather than derived, and one condition on the components delivers it. The components a host holds are finitely many programs given before anything runs, so if no component can register, however indirectly, a fiber of a component that registers one of its own, the registrations form a tree of bounded depth, and len(𝑒𝑛) ≤ 𝐾 bounds its branching. What the assumption rules out is a component that registers instances of itself without bound.

中文翻译

一个把提供者撤回推迟到其依赖者都离开的守卫，只有在它最终释放时才交付定理63。注册表纤维上的一个关系承载该论证。

定义 65。 注册表名上的先序关系（precedence relation）为
𝑛 ≺ 𝑚 ≔ 𝑝𝑛 ∩ 𝑑𝑚 ≠ ⌀
即 𝑛 可能提供 𝑚 声明的键。它只读 𝑑 与 𝑝，而由引理54(5) 二者随纤维条目产生且不再被写。

定理66与定理73建立在 ≺ 无环的假设上，这是一个假设而非定义所交付的——声明一个自己提供的键的组件满足 𝑛 ≺ 𝑛。≺ 排序的是两个纤维的激活而非其寿命：𝑛 ≺ 𝑚 说的是 𝑛 必须先于 𝑚 成为 𝖠𝖼𝗍𝗂𝗏𝖾，而提供者比消费者长寿则是定理63(2)。

定理 66（进展性）。 假设 ≺ 无环、每个 𝑛 的 len(𝑒𝑛) ≤ 𝐾、名集合 𝑁 有限；且每步应用一条生命周期规则。记 𝑆(𝑛) 为作用于 𝑛 的步数，𝑉(𝑛) ≔ |{𝑡 : target𝑡𝑛 ≠ target𝑡+1𝑛}| 为其目标视图转折次数。则：
1.（无死锁）¬ quiet𝑡 蕴含某条生命周期规则在 𝛾𝑡 可应用；
2.（终止性）𝑆(𝑛) ≤ (𝐾 + 4)(𝑉(𝑛) + 1)，且 𝑉(𝑛) 与 ∑𝑛 𝑆(𝑛) 均有限。
由此每条极大的生命周期步骤序列终止于一个静止状态。

𝑁 的有限性是假设而非导出，组件上的一个条件交付它。宿主持有的组件是运行前给定的有限多个程序，所以若没有组件能（无论多间接地）注册一个会注册自身的组件的纤维，则注册形成一棵有界深度的树，len(𝑒𝑛) ≤ 𝐾 约束其分支度。该假设排除的是无界地注册自身实例的组件。

详细解释

进展性（progress）回答两个关键问题：系统会不会卡死（deadlock）？系统会不会无限运行不停下来（nontermination）？ 这是 4.3.1 撤回守卫能成立的前提——守卫"等依赖者离开"如果永远不释放，就死锁了。Theorem 66 证明：在合理假设下，既不死锁也必终止，且每条极大步骤序列都收敛到静止状态。

先序关系 ≺ 是论证的工具。 𝑛 ≺ 𝑚 定义为"𝑛 的供给与 𝑚 的依赖有交集"——即 𝑛 可能是 𝑚 的提供者。它只读 𝑑 和 𝑝，而这两个字段随纤维诞生就不再变（引理54(5)），所以 ≺ 在运行中是稳定的。论文诚实地指出 ≺ 无环是一个假设而非定义保证的：一个声明了自己提供的键的组件满足 𝑛 ≺ 𝑛（自环）。≺ 排序的是"激活顺序"（𝑛 要先 𝖠𝖼𝗍𝗂𝗏𝖾 才能轮到 𝑚），不是"寿命"（提供者比消费者长寿是 Theorem 63(2) 的结论，是守卫换来的，不是 ≺ 给的）。这个区分很重要：进展性假设的是激活无环，而"提供者后死"是定理证明的。

无死锁的证明梗概。 设 ¬ quiet𝑡，则有某纤维没对齐目标。按 𝜃𝑛 的四种可能逐一查表：𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥) 且 target≠⊥ → L-Begin 可用；𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 且 target=𝜔 → L-Iter/L-Finish/L-Raise 之一可用；𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀 且 target≠𝜔 → L-Raise（若抛错）或 L-Divert（落地式，惯性宿主也可用）；𝖠𝖼𝗍𝗂𝗏𝖾 且 target≠𝜔 → L-Leave 可用。若没有任何纤维处于这四种，则必有某 𝑚0 处于 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀。关键的反死锁论证从这里开始：若 ¬ relied𝑚0，则 L-Unload 可用，停。否则存在 𝑚1 ≠ 𝑚0 把某键解析到 𝑚0，由 Theorem 63(3) 该键 ∈ 𝑝𝑚0 ∩ 𝑑𝑚1，即 𝑚0 ≺ 𝑚1；且 𝑚0 是 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀（不在 𝜎𝛾 中），故 𝑚1 的 target 已不指向 𝑚0，𝑚1 也必处于 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀。于是构造一条 𝑚0 ≺ 𝑚1 ≺ 𝑚2 ≺ … 的链，每步严格 ≺ 递增。由 ≺ 无环，链中所有名互不相同；由 dom(𝐹𝑡) 有限，链必终止——终止处即 ¬ relied，L-Unload 可用。这就是 4.3.1 所说的"守卫总会释放"的形式化：沿着依赖图往上找，无环 + 有限保证能找到一个无人依赖的 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀 纤维，解锁整条链。

终止性的证明梗概。 两个断言界住 𝑆(𝑛)。(A) 在 target𝑛 恒为 𝜔∗ 的极大区间内，作用于 𝑛 的步数至多 𝐾+4：从 𝖠𝖼𝗍𝗂𝗏𝖾(−,𝜔≠𝜔∗) 走 L-Leave+L-Unload，若 𝜔∗≠⊥ 再 L-Begin+至多 𝐾 次落地+可能一次额外 L-Unload（若末次落地是 L-Raise）；其他状态是其后缀。(B) 若 target𝑛 在第 𝑡 步转折且该步作用于 𝑚，则要么 𝑚 ≺ 𝑛（𝑚 是 𝑛 某依赖的提供者），要么该步写 𝜏𝑛——因为 target 只依赖 𝜏𝑛 与各提供者的表，表只在自身纤维被作用时变。由无环 𝑚≠𝑛（第一种），由 𝜏 单调第二种每纤维至多一次。综合 (A)(B)：𝑆(𝑛) ≤ (𝐾+4)(𝑉(𝑛)+1)，且 𝑉(𝑛) ≤ 1 + ∑𝑚≺𝑛 𝑆(𝑚)。这是一个沿无环 ≺ 的良基递归，定义 𝐵(𝑛) = (𝐾+4)(2 + ∑𝑚≺𝑛 𝐵(𝑚)) 界住 𝑆(𝑛)，故 𝑉(𝑛) 与 ∑𝑛 𝑆(𝑛) 都有限。结合无死锁，每条不可扩展的序列必静止。

进展性的工程含义。 这是整个动态组合系统的"活性"（liveness）保证：系统不会因为复杂的依赖关系而卡死，也不会因为反复重载而无限震荡。𝑉(𝑛) 有限意味着每个纤维的目标视图只会转折有限次——这背后是 𝜏 单调（每个纤维至多被退役一次）和 ≺ 无环（依赖提供者的转折次数被提供者的步数界住）。终止性说系统最终会"安静下来"达到静止状态。这与 Cordis/DSH 的实践对应：装载/卸载一堆相互依赖的组件后，系统一定会稳定到一个一致状态，不会永远在"装载-卸载"震荡或死锁等待。无环假设排除"循环依赖"（A 依赖 B、B 又依赖 A）——这是依赖注入系统的标准要求；有限性假设排除"组件无限自我繁殖"——一个会无限制注册自身实例的组件会让 𝑁 无限增长。

惯性的兼容性。 论文特别指出进展性只要求宿主提供 L-Begin/L-Leave/L-Unload/L-Iter/L-Finish/L-Raise/L-Divert，从不要求 L-Divert 的放弃分支——所以受 4.3.3 惯性约束（不能放弃飞行中迭代）的异步宿主也完全在进展性保证之内。这是一个精心设计的覆盖：异步现实运行时也能得到活性保证。

4.4.5 Confluence / 汇合性

原文 (English)

The results so far are about individual fibers. The property that characterizes the system as a whole is that its dynamic history leaves no trace: whatever sequence of activations and deactivations a running system has been through, the state it quiesces at is the one the same insertions and retirements would have produced had each component that ends up active been loaded once, in dependency order, and none ever unloaded. The lifecycle relation is confluent, and the normal form it converges on is the statically assembled one. This is the analogue, for dynamic composition, of the consistency with a from-scratch evaluation that change propagation establishes for incremental computation [45].

Definition 67. A fiber is supported at 𝛾 when it is not retired, the fiber registering it is supported, and every key it declares is provided by a supported fiber. The support relation is the union 𝑚 ⊲ 𝑛 ≔ 𝑚 ≺ 𝑛 ∨ 𝜋𝑛 = 𝑚, and where well founded we write 𝐴 for the support set: 𝑛 ∈ 𝐴 ≔ ¬𝜏𝑛 ∧ (𝜋𝑛 = 𝗋𝗈𝗈𝗍 ∨ 𝜋𝑛 ∈ 𝐴) ∧ ∀𝑘 ∈ 𝑑𝑛. ∃𝑚 ∈ 𝐴. 𝑘 ∈ 𝑝𝑚.

Lemma 68 (Support is well founded). Let ≺ be acyclic and let 𝛾 be reached by a sequence of steps. Then ⊲ is well founded, and 𝐴 is the one solution of Definition 67, a function of 𝜏, 𝜋, 𝑑, and 𝑝 alone.

Definition 69. A component (𝑑, 𝑝, 𝑒) is total on its provision when an activation of it that finishes has installed every key of 𝑝, so that dom(𝜎𝑛) = 𝑝𝑛 at every 𝖠𝖼𝗍𝗂𝗏𝖾 fiber instantiating it.

Lemma 70 (Support at quiescence). Let ≺ be acyclic, let quiet(𝛾), let no fiber of 𝛾 be failed, and let every component be total on its provision. Then the support set is the set of 𝖠𝖼𝗍𝗂𝗏𝖾 fibers: 𝐴 = {𝑛 : 𝜃𝑛 = 𝖠𝖼𝗍𝗂𝗏𝖾(−, −)}.

Lemma 71 (Transposition). Let the steps be pairwise independent and 𝐹𝑡 well formed, and let steps 𝑡 and 𝑡+1 act on distinct fibers 𝑚 and 𝑛. (1) If both apply an activation rule (L-Begin, L-Iter, or L-Finish), and step 𝑡+1 is applicable at 𝛾𝑡, then step 𝑡 is applicable at the state step 𝑡+1 produces, and the two orders reach the same 𝛾𝑡+2. (2) If step 𝑡 applies an activation rule at 𝑚, step 𝑡+1 an orchestration rule at 𝑛, and step 𝑡 does not register 𝑛, then the same holds.

Lemma 72 (Deletion). Let the sequence be pairwise independent, every component total on its provision, let it reach a quiescent 𝛾𝑇 at which no fiber is failed, let [𝑏, 𝑢] be a closing episode of 𝑛, let no episode of any 𝑚 with 𝑛 ≺ 𝑚 close, and let no fiber 𝑛 registers during [𝑏, 𝑢] have an episode. Write 𝑅 for those registration names. Then deleting the steps acting on 𝑛 in [𝑏, 𝑢], together with every step acting on a name of 𝑅, leaves a sequence reaching a state ≈-equal to 𝛾𝑇 and ≃-equal to it outside 𝑅.

Theorem 73 (Confluence). Let a sequence reach a quiescent 𝛾𝑇 at which no fiber is failed, let the steps be pairwise independent and every component total on its provision, and let 𝐴 be as in Definition 67. Then:

Failure is excluded from the statement because it is a genuine source of divergence, and the calculus should not be read as denying it. They do not differ in anything else, by Corollary 62, which puts a failed fiber’s contribution to the state at nothing.

The theorem is what licenses reasoning about a Cordis application as though it were statically assembled. An orchestrator that adds a component, removes it, replaces a provider, and reverts the replacement is guaranteed to arrive at the state it would have obtained by writing the final composition down at the outset.

中文翻译

到此为止的结果都是关于单个纤维的。刻画整个系统的性质是：其动态历史不留痕迹——无论一个运行中的系统经历过怎样的激活与去激活序列，它静止于的状态，都是"相同的插入与退役、按依赖顺序各装载一次最终激活的组件、且从不卸载任何一个"本会产生的那一个。生命周期关系是汇合的（confluent），它收敛到的正规形式是静态装配的那个。这是动态组合类比于增量计算中变更传播所建立的"与从头求值一致"的性质[45]。

定义 67。 一个纤维在 𝛾 处受支持（supported），当它未被退役、注册它的纤维受支持、且它声明的每个键都由某受支持纤维提供。支持关系是 𝑚 ⊲ 𝑛 ≔ 𝑚 ≺ 𝑛 ∨ 𝜋𝑛 = 𝑚 的并，在良基处记 𝐴 为支持集：𝑛 ∈ 𝐴 ≔ ¬𝜏𝑛 ∧ (𝜋𝑛 = 𝗋𝗈𝗈𝗍 ∨ 𝜋𝑛 ∈ 𝐴) ∧ ∀𝑘 ∈ 𝑑𝑛. ∃𝑚 ∈ 𝐴. 𝑘 ∈ 𝑝𝑚。

引理 68（支持良基）。 令 ≺ 无环且 𝛾 由步骤序列达到。则 ⊲ 良基，且 𝐴 是定义67的唯一解，仅是 𝜏, 𝜋, 𝑑, 𝑝 的函数。

定义 69。 一个组件 (𝑑, 𝑝, 𝑒) 在其供给上完全（total on its provision），当它的一次完成的激活已安装 𝑝 的每个键，故每个实例化它的 𝖠𝖼𝗍𝗂𝗏𝖾 纤维处 dom(𝜎𝑛) = 𝑝𝑛。

引理 70（静止处的支持）。 令 ≺ 无环、quiet(𝛾)、无失败纤维、每个组件在其供给上完全。则支持集就是 𝖠𝖼𝗍𝗂𝗏𝖾 纤维集：𝐴 = {𝑛 : 𝜃𝑛 = 𝖠𝖼𝗍𝗂𝗏𝖾(−, −)}。

引理 71（换位）。 令步骤两两独立且 𝐹𝑡 良构，步骤 𝑡 与 𝑡+1 作用于不同纤维 𝑚 与 𝑛。(1) 若两者都应用激活规则，且步骤 𝑡+1 在 𝛾𝑡 可应用，则步骤 𝑡 在步骤 𝑡+1 产生的状态上可应用，两种顺序达到同一 𝛾𝑡+2。(2) 若步骤 𝑡 在 𝑚 应用激活规则、步骤 𝑡+1 在 𝑛 应用编排规则、且步骤 𝑡 不注册 𝑛，则同理。

引理 72（删除）。 令序列两两独立、每组件在其供给上完全、达到无失败纤维的静止 𝛾𝑇，令 [𝑏, 𝑢] 为 𝑛 的关闭幕、无 𝑛 ≺ 𝑚 的 𝑚 的幕关闭、且 𝑛 在 [𝑏, 𝑢] 期间注册的纤维无幕。记这些注册名为 𝑅。则删除 [𝑏, 𝑢] 中作用于 𝑛 的步骤及每个作用于 𝑅 中名的步骤，留下一个达到与 𝛾𝑇 ≈ 相等、且在 𝑅 之外 ≃ 相等的状态的序列。

定理 73（汇合性）。 令某序列达到无失败纤维的静止 𝛾𝑇，步骤两两独立、每组件在其供给上完全，𝐴 如定义67。则：
1.（正规形式）𝛾𝑇 可（在被归约撤回的名以外）由 𝛾0 经一个序列达到：该序列以原序取相同的编排步骤（编排者插入的纤维处的步骤先于每个生命周期步骤，其余各跟随注册它所作用纤维的那步），并按 ⊲ 的一个线性化枚举 𝑛1,…,𝑛𝑘，依次各取 𝑛𝑖 的一幕。
2.（汇合）从 𝛾0 取相同编排步骤的任意两个这样的序列，达到的状态经引理56的重命名后由 ≃ 与 ≈ 关联。

失败被排除在陈述之外，因为它是真正的发散之源，演算不应被读作否认它。由推论62它们在其余任何方面都不异，失败纤维对状态的贡献为零。

该定理正是允许把 Cordis 应用当作静态装配来推理的依据。一个添加组件、移除它、替换提供者、再回退替换的编排者，保证到达"一开始就把最终组合写下来"本会得到的状态。

详细解释

汇合性（confluence）是整章、也是整篇论文最宏大的结论：无论系统经历过怎样曲折的动态装卸载历史，它最终静止的状态，都等同于"把最终该激活的组件按依赖顺序一次性装载、从不卸载"的静态装配结果。 论文把它类比为增量计算里变更传播建立的"与从头求值一致"性质[45]——动态组合与静态组合在结果上不可区分。这是"时空可组合性"中"空间"维度的终极保证：动态历史不留痕迹。

支持集 𝐴 是"哪些纤维最终该激活"的纯输入函数。 定义67递归地定义"受支持"：未被退役、注册者受支持（或根插入）、每个声明的键都由某受支持纤维提供。这个定义只读 𝜏/𝜋/𝑑/𝑝 四个字段——全是运行中不变的字段（引理54(5)），所以 𝐴 完全由输入（编排者的插入与退役、组件的声明）决定，与调度顺序无关。Lemma 68 证明这个递归良基且有唯一解：按注册顺序给纤维编号，父指针总是指向更早注册的纤维（O-Insert 前提），所以 ⊲ 的父半部天然下降；若成环必混用 ≺ 半部，而无环 ≺ 迫使环需经"某纤维声明其自己子树提供的键"，但该键在 𝑚 的 L-Begin 前就已被 𝖠𝖼𝗍𝗂𝗏𝖾 纤维提供（L-Begin 前提 𝛾⊧𝑑𝑚），单一来源禁止第二个提供者，故该纤维永不被注册——环不存在。

完全性（totality，定义69）补上"声明 𝑝"与"实际安装 dom(𝜎)"的缝。 支持集读 𝑝（组件可能提供的键），而 target 读 dom(𝜎𝛾)（实际安装的键），二者只由 dom(𝜎𝑛) ⊆ 𝑝𝑛 联系。完全性要求"完成的激活必安装 𝑝 的全部键"，于是 dom(𝜎𝑛) = 𝑝𝑛，缝被补上。Lemma 70 证明在静止、无失败、完全性下，支持集恰等于 𝖠𝖼𝗍𝗂𝗏𝖾 纤维集——即"该激活的都激活了"。完全性虽是假设，但独立性已界住它能失败的程度：若一组件只在别的组件效应到达的状态才装某键，其前向映射就不与那组件交换，违反独立性——所以"装哪些键"由组件本身而非调度决定，完全性只是要求这个固定集合是全部 𝑝。

三个引理是汇合性证明的"重排工具"。 Lemma 71（换位）是 trace 理论的重排引理：作用于不同纤维的两个相邻步骤，在独立性下可交换且达到同态。它分激活-激活、激活-编排两种情形，关键都用定义60的两条件（映射交换 + 迭代器在被移动状态上产出不变）和供给不相交（定义58(2)，使一纤维的表写入不触及另一纤维的依赖键）。Lemma 72（删除）是"动态历史不留痕迹"的核心：一个关闭的 episode（连同它注册的子纤维）可以从序列中整段删掉，终态不变——这正是 Corollary 62（终态恢复，𝑛 的净贡献为零）加上 Lemma 57（残留条目不可见）的应用：删掉的步骤把状态留在原处，残留的注册条目对后续规则不可见。残留引理正是删除被退役注册的工具。

Theorem 73 的证明梗概（两步归约到正规形式）。 (1) 正规形式分三阶段构造。关闭幕先走：归纳地挑一个 ⊲-极大的关闭幕 𝑛，Lemma 72 的三前提满足（无 𝑛≺𝑚 的关闭幕、𝑛 注册的纤维无幕），删掉它，归纳数减一。非 𝐴 纤维无生命周期步骤：由 Lemma 70 + quiet，它们全程 𝖨𝗇𝖺𝖼𝗍𝗂𝗏𝖾(⊥)，L-Begin 是唯一可用规则但会开幕——矛盾。编排步骤归前：编排者插入的纤维的编排步骤用 Lemma 71(2) 一路前移到最前；注册产生的编排步骤留在注册处。幕排序连续化：按 ⊲ 线性化 𝑛1,…,𝑛𝑘，归纳地把 𝑛1 的所有步骤前移成连续初始块（𝑛1 是 ⊲ 极小故 𝑑=∅、𝜋=root，其 target 不读他人、恒定，每步只读自己的 𝜃/𝑖，故处处可应用，Lemma 71 逐步前移），再在余下后缀上对 𝐴∖{𝑛1} 重复。(2) 汇合：两个序列都归约到正规形式，二者跑过相同的 𝐴（仅注册树的名字不同，用 Lemma 56 的双射对齐），⊗ 的两个线性化只差不可比幕的换位，Lemma 71 保证终点不变，故两正规序列一致。结合 Theorem 66 的终止性，生命周期关系有唯一正规形式。

失败被诚实排除。 论文明确说失败是"真正的发散之源，演算不应否认"：是否抛错取决于运行所依据的状态，一种调度可能失败一个纤维而另一种完成它，两静止态在该纤维的生命周期状态上不同。但由 Corollary 62，失败纤维对状态的贡献为零，所以两态在其余任何方面都不异——失败只影响"那个纤维是否激活"，不影响环境状态。这是一个诚实的边界：汇合性保证的是"状态"汇合，不是"哪些组件成功"汇合。

与 Cordis/DSH 实践的对应——这是论文的"杀手级应用"。 Theorem 73 是允许"把 Cordis 应用当作静态装配来推理"的执照。具体场景：一个编排者"添加组件 A、移除 A、替换提供者 P 为 Q、再回退替换（Q 换回 P）“——这串复杂动态操作最终到达的状态，保证等于一开始就把最终组合（含 P、不含 A）写下来的静态装配结果。这意味着组件作者在推理"哪些协同效应在作用域内"时，只需推理静止状态，无需追踪动态历史。它也划定了保证的边界：定理说的是"状态”，不是"沿路产生的发射（emissions）"——这是第6.1节区分"获取（acquisition，边界内追踪）"与"发射（emission，跨边界）"的伏笔。动态组合因此获得了静态组合的可推理性：你写下一个 Cordis 应用并反复热重载它，最终状态与"一次性写定"不可区分——这就是"时空可组合性"的最终承诺。

本笔记覆盖论文第4章（动态组合演算）全部小节：4.1 组件与纤维、4.2 基础演算、4.3 进行中的转换（撤回/迭代/异步/失败）、4.4 元理论（保持性/时间可组合性/空间可组合性/进展性/汇合性）。所有操作语义规则名与关键形式、所有引理与定理陈述均按原文保留，证明以梗概形式概括并点明其所建立的性质。