DeepSeek Harness 论文《时空可组合性编程范式》中文白话

DeepSeek 开源的智能体产品 deepseek-harness 采用“一切皆插件”的架构，其中核心插件框架 Cordis 的思想来自同期论文《A Programming Paradigm for Spatiotemporal Composability》。论文试图用形式化方法回答一个工程问题：当系统运行时不断加载、卸载、替换和重新连接组件时，我们怎样保证系统不会被历史过程污染？

这篇文章的目的是绕开那些晦涩的公式定理，用大白话把论文的核心思想叙述成一条连贯的线索。文中保留 1 到 74 的定义、定理、引理和推论编号，主要是为了说明论文结构，可以用于导读；真正重要的是每个条目背后的工程含义。

论文讨论的是“动态组合”。它有两个方向：

时间方向：组件做过的事，之后能不能完整撤回。
空间方向：组件依赖什么、谁提供这些依赖、依赖变化时哪些组件应该响应。

论文用“效应”描述组件对环境的修改，用“余效应”描述组件对环境的需求，再把两者统一进一个运行时上下文。后半篇继续引入组件、纤程、注册表、生命周期规则和全局性质，说明这些局部机制怎样扩展成一个可推理的动态系统。

论文从哪里出发

论文不是从抽象数学兴趣出发，而是从运行时框架越来越常见的工程压力出发。

传统软件组合大多是静态的。函数调用、模块导入、类继承，通常在编译、启动或部署时就确定下来。系统运行以后，这些组合关系基本不变。可是现代软件越来越多地需要动态组合：插件可以运行时启用或禁用，服务可以热替换，配置可以增量生效，智能体运行时甚至可能生成、修改和部署自己的工具或组件。

这类系统的难点不在“能不能把代码加载进来”，而在“加载进来之后还能不能安全拿掉”。一个插件启用时可能注册命令、打开连接、启动定时任务、写入缓存、创建子组件；如果禁用时只是把插件标记为不可用，而没有完整撤销这些动作，系统就会留下幽灵状态。重启进程当然能清掉很多东西，但代价是所有组件都一起中断，进程内缓存、连接、会话和正在执行的任务也一起丢失。

运行时框架的核心矛盾

运行时框架的理想状态，是让组件像积木一样插拔：组件可以在系统继续服务的情况下进入、退出、替换，并且只影响真正依赖它的部分。

现实做法往往更粗糙。插件系统通常提供一个启动入口，再提供一个关闭回调，把清理责任交给插件作者。只要作者漏掉一个监听器、一个定时器或一条注册记录，卸载就不完整。很多平台因此退回到“禁用后重启宿主进程”这样的粗粒度方案。

容器编排也解决了一部分问题，但粒度通常是进程或服务。操作系统能回收进程资源，容器编排能重建服务依赖，可是进程内部的插件、工具、适配器、策略模块之间的依赖关系，仍然缺少同等粒度的生命周期语义。论文关心的正是这个粒度差：组件明明在同一个地址空间内动态组合，却只能借助进程级或容器级手段恢复。

插件架构为什么暴露这个问题

插件系统是动态组合的典型场景。论文用 VSCode 这类可扩展开发环境说明问题：很多扩展包含可执行代码，启用后会向宿主注册命令、视图、语言功能或事件监听。禁用或卸载扩展时，如果宿主不能单独卸载这个扩展的代码和副作用，就只能重启扩展宿主。

这暴露出两个限制。

第一是时间方向的限制：插件曾经做过的修改没有被结构化记录，关闭回调又和创建效应的位置分离，完整清理很难验证。

第二是空间方向的限制：插件之间即使能互相调用，也常常缺少类型化、结构化、可追踪的依赖声明。很多插件不是依赖彼此，而是都挂在宿主提供的固定扩展点上；一旦插件之间真的形成依赖，宿主也未必知道谁该先启用、谁该先退出。

自进化代理为什么让问题更尖锐

论文还把未来的自进化智能体运行时作为动机。一个长期运行的智能体系统可能包含工具库、权限系统、沙箱、记忆模块、上下文管理、子智能体编排、用户界面和自动化入口。更进一步，智能体可能自己生成新工具，替换旧工具，调整自己的组件拓扑。

在这种场景里，动态组合不再是偶尔发生的插件安装，而是系统持续运行的一部分。每次自我修改都重启整个进程，会打断正在执行的任务，丢失进程内状态；更危险的是，一个错误修改可能破坏恢复它所需要的运行时本身。

如果没有空间可组合性，每个模块都要自己发现依赖变化并临时适配。某个工具替换了接口，依赖它的规划器、权限检查器、任务恢复器可能都要各自写一套应对逻辑。依赖环、过期引用和半更新状态会在运行时才暴露。

所以论文的目标不是“让插件系统更方便一点”，而是为一种更细粒度、更连续的运行时演化提供基础语义。

粗粒度方案为什么不够

操作系统和容器编排已经提供了某种可组合性，但粒度太粗。

在时间方向上，操作系统可以回收整个进程。进程退出后，内存、文件描述符、线程等资源会被系统清理。这确实可靠，但它清理的是整个进程，不是某个组件。为了撤掉一个插件而重启所有插件，会丢掉缓存、连接和正在进行的计算。

在空间方向上，容器编排可以管理服务之间的依赖。服务坏了可以重启，副本可以滚动更新，网络端点可以重新绑定。但它管理的是服务级拓扑，无法表达同一进程内某个工具插件依赖某个存储插件、某个 UI 插件依赖某个权限插件这种细粒度关系。把所有内部组件都拆成独立服务，又会引入通信开销和部署复杂度。

论文因此提出：需要一种和组件同粒度的抽象。组件做出的修改，要在组件生命周期内被记录并可撤回；组件需要的依赖，要在组件生命周期内被声明、解析和响应。

两个正交维度

论文把动态组合拆成两个正交维度。

时间可组合性关心“组件离开时，它做过的事能不能被撤销”。这对应效应。每一次对环境的修改，都应当伴随一个撤销动作；运行时把这些撤销动作按正确顺序累积起来。组件卸载时，不靠作者临时想起应该清理什么，而是执行已经被上下文记录好的恢复器。

空间可组合性关心“组件运行时，它依赖什么、由谁提供、变化时谁该响应”。这对应余效应。组件声明自己需要哪些键；运行时根据当前依赖表判断它能否激活；依赖出现、消失或换了提供者时，运行时推动相关组件加载、卸载或重载。

这两个维度彼此独立，又必须合在一起。只有时间可组合性，系统知道怎么撤销组件，却不知道依赖变化该影响谁。只有空间可组合性，系统知道谁依赖谁，却不能保证卸载时资源完整释放。论文的核心贡献，就是把效应和余效应提升为运行时机制，再统一到同一个上下文中。

生命周期为什么成为中心

一旦组件可以运行时进入和退出，生命周期就不再只是“初始化和销毁”两个回调。

组件可能正在加载，依赖突然变化；可能异步加载已经发出，不能立即取消；可能加载一半失败，需要撤销已经完成的部分；也可能提供者准备卸载，但旧消费者还需要它完成自己的清理。论文第 4 章之所以引入纤程、目标视图、已提交视图、加载中、卸载中、被依赖守卫，正是为了把这些现实情况说清楚。

可以把整篇论文理解成一句话：动态组合不是“多几个生命周期钩子”，而是要让每个组件的效应、依赖和生命周期都进入同一个可推理的上下文模型。

基础效应

本章解释论文第 3 章开头和 3.1.1 节，覆盖编号 1 到 7。

这一章是整篇论文的地基。作者先不处理组件、依赖注入、异步加载和失败恢复，只问一个最朴素的问题：如果一个系统状态会被程序修改，怎样同时记住“做了什么”和“怎样撤销”？

论文把副作用看成对上下文状态的一次改动。最简单的形式是一对动作：一个动作把状态往前推进，另一个动作尝试把它撤回。这里的撤销动作还是预先给定的固定动作；下一章才会升级为“执行后根据实际结果生成撤销动作”的模型。

定义1：扭曲组合

这一条定义的是“正向动作 + 候选撤销动作”怎样组合。正向执行时，动作按发生顺序一个接一个叠加；撤销时，顺序必须反过来，后做的先撤，先做的后撤。

这里“扭曲”的意思不是正向计算被改变，而是同一个组合里同时保存了两种方向：正向顺序和恢复顺序。它形成了一个可以连续组合的结构：可以把很多小动作合成一个大动作，也有一个“什么也不做”的空动作，并且分组方式不会改变最终结果。

一个容易误读的点是：定义1只是在规定“撤销动作怎样堆叠”，还没有保证撤销动作一定正确。撤销正确性要等到定理7，在具体状态上要求“先做再撤能回到原状态”。也就是说，论文先搭出账本结构，再说明什么情况下账本里的撤销记录是可靠的。

工程直觉很接近嵌套资源清理：先打开数据库连接，再注册监听器，退出时先取消监听器，再关闭数据库连接。论文把这种栈式清理直觉抽象成代数结构，后面才能把组件卸载、热替换、依赖变更都纳入同一个推理框架。

定义2：效应上下文

效应上下文把两件事绑在一起：一件是当前状态，另一件是恢复器。恢复器可以理解成一条已经累积好的清理链，记录到目前为止应该怎样撤销。

如果系统从初始状态开始，那么一开始恢复器就是空的。每执行一个被跟踪的效应，当前状态会被推进一步，恢复器会追加一个新的清理动作。

这一条的关键意义是：恢复信息不再散落在组件自己的卸载函数里，而是成为运行时上下文的一部分。系统不仅知道“现在是什么”，还知道“如果现在要求恢复，应当怎样走回去”。

从程序设计角度看，这相当于把清理函数栈从组件内部挪到框架上下文里。组件只负责在每一步修改时交出对应撤销动作，框架负责累积和组合这些动作。

定义3：跟踪变换

跟踪变换说明怎样把“正向动作 + 撤销动作”接入效应上下文。它同时做两件事：

对当前状态执行正向动作。
把对应的撤销动作追加到恢复器里。

真正执行恢复时，新加入的撤销动作会先运行，旧的恢复器再运行。所以越晚发生的效应，越早被撤销。这正是后进先出的恢复顺序。

定义3把“做一件事”和“记录怎么撤销这件事”绑定成一个原子动作。后面实现里的 ctx.effect 就是这个思想的工程版本：组件执行一次上下文修改时，同时返回清理函数；框架负责把清理函数合成恢复器。

这里还没有讨论业务返回值。论文在这一节先只看状态怎样变化；组件执行时产生句柄、标识、查询结果等返回值的问题，会在后面的效应函数和迭代器模型里逐步补上。

定理4：当前状态一致

这条定理说明，跟踪机制不会改变正向动作本身的可见结果。白话说就是：带账本执行和不带账本执行，对“当前状态”这一项没有区别。多出来的只是第二项恢复器。

它的作用是消除一个基本疑问：为了记录撤销信息，系统会不会悄悄改变原操作的语义？定理回答说不会。跟踪只是在普通状态变换外面加了一层运行时记录机制，正向业务状态仍按原来的动作改变。

这也解释了为什么论文可以把副作用重写成上下文变换而不改变原本程序的正向含义。只要只观察当前上下文状态，跟踪版本和直接执行版本一致。

定理5：跟踪保持组合

这条定理说明，跟踪机制和组合机制彼此兼容。它同时保持两个性质：

空操作仍然是空操作。
组合后再跟踪，等于分别跟踪后再组合。

第二点是核心。假设组件加载时连续做两件事：先注册服务，再安装路由。你可以先把两件事合成一个大效应，再交给跟踪机制；也可以每做一步就让跟踪机制记录一次。最终得到的状态和恢复器一致。

这件事非常重要，因为真实组件不会只做一个动作。组件加载可能注册服务、安装路由、打开连接、启动后台任务。定理5保证：只要每个小动作能提供自己的候选撤销动作，框架就能按组合规则自动得到整体恢复器，而不需要组件作者再手写一个总卸载函数。

从证明结构看，定理5是后续所有“局部正确可以组合成整体正确”的起点。后面关于带见证效应、效应提升、后进先出恢复和全局恢复精确性的结论，都是在更复杂模型里重复这个主题：组合不能破坏恢复语义。

定义6：恢复变换

恢复变换就是执行当前效应上下文里的恢复器。它先把累积好的清理链应用到当前状态，再把恢复器重置为空。它对应组件卸载时真正执行清理的动作。

这里有两个细节值得注意。

第一，恢复作用的是当前上下文层级中已经累积的效应，不是回滚整个进程，也不是重启系统。后面组件模型会让每个纤程持有自己的恢复器，因此恢复可以针对某个组件实例或某个上下文范围发生。

第二，恢复完成后仍然处在效应上下文里，只是恢复器已经清空。论文坚持把恢复也看成上下文变换，而不是跳出上下文模型的一段特殊代码。

这条定义把“卸载”从一段散乱的用户代码变成统一运行时操作。只要组件的修改都通过跟踪机制进入上下文，恢复操作就知道如何按正确顺序执行已累积的逆动作。

定理7：恢复不变量

这条定理是第一章的正确性核心。它说：如果在当前状态上，候选撤销动作确实能撤销刚刚发生的正向动作，那么跟踪这一步效应不会改变最终恢复目标。

白话说，加入一个可撤销的新动作后，“现在恢复会回到哪里”这个答案不变。正向动作会把状态往前推一步，但它的撤销动作也同时进入恢复器；恢复时先撤掉新动作，再继续执行旧恢复器，于是恢复终点保持不变。

论文把“恢复器应用到当前状态后得到什么”看成当前效应上下文的恢复读数。如果系统从初始状态开始，理想情况就是这个读数始终指向初始状态。这就是本章最后提到的“恢复正确性不变量”：中间状态可以变，但恢复器指向的原点不应变。

定理7的条件是局部的，只要求撤销动作能撤销自己这一次实际造成的修改，不要求它在所有可能状态上都是完美数学逆。论文特别保留这个弱条件，因为工程里的清理函数通常只保证能清理自己刚刚创建的东西。例如某次注册返回一个具体句柄，撤销函数只需要注销这个句柄，而不必对任意系统状态都成立。

这一章还没有解决多个组件交错执行、任意顺序卸载、依赖关系变化等问题。它只证明最底层账本是可靠的：当每一步都有可用的候选撤销动作时，跟踪不会改变正向语义，恢复器会按正确顺序累积，恢复目标保持不变。

可撤销效应

本章解释论文 3.1.2 和 3.1.3 节，覆盖编号 8 到 21。

第一章的模型有一个现实限制：撤销动作在执行前就固定好了，好像一个正向动作在所有状态下都用同一个清理函数。真实程序通常不是这样。注册监听器后拿到的句柄、打开文件后拿到的描述符、创建子组件后拿到的名字，都只有执行以后才知道。因此第二章把效应升级成“运行时返回撤销函数”的函数。

这一章还处理另一个问题：后进先出恢复适合单个效应序列，但动态系统常常要只撤销某一个组件，把别的组件保留下来。为此，论文先证明栈式撤销在单个序列内部成立，再引入“独立性”，说明在满足更强条件时，撤销可以不按原来的栈顺序执行。

定义8：带见证的效应

带见证的效应可以理解成一个运行时动作：输入当前上下文，输出新上下文和本次撤销函数。这个撤销函数不是提前写死的，而是根据本次执行结果生成的。

这比前面的固定逆动作更贴近编程实践。例如，注册事件监听器时，撤销动作要知道刚刚注册的是哪一个监听器；分配资源时，撤销动作要知道刚拿到的资源句柄。这些信息通常只有执行后才知道。

“带见证”的意思是：本次返回的撤销函数必须真的能撤销本次状态变化。这里的要求仍然是局部的。论文不要求撤销函数对所有状态都正确，只要求它能撤销自己这次实际造成的修改。

固定动作模型仍然可以嵌入进来：如果某个正向动作有一个在所有状态上都成立的撤销动作，那当然也可以把它看成“每次执行都返回同一个撤销函数”的带见证效应。后面的定理会说明这种嵌入和组合结构兼容。

定义9：效应组合

带见证效应返回的是“新状态 + 撤销函数”，所以不能再把它当成普通函数直接复合。定义9重新规定了效应组合的规则。

组合两个效应时，先执行前一个，拿到它的新状态和撤销函数；再在这个新状态上执行后一个，拿到第二个撤销函数。最终得到的总撤销函数必须按相反顺序执行：先撤销后一个效应，再撤销前一个效应。

这个定义把“组合效应也应当可撤销”变成明确规则。它对应编程中的常见模式：函数内部连续执行多个注册、打开、绑定等动作，每个动作返回一个清理函数，最终函数返回一个总清理函数。

需要注意，论文的符号顺序沿用了函数复合习惯，读起来可能和自然语言顺序相反。导读里只需抓住核心：正向按执行顺序，撤销按相反顺序。

定理10：效应形成组合结构

这条定理说明，带见证效应可以像普通动作一样被连续组合。空效应什么也不改，撤销函数也什么都不做；多个效应连续组合时，分组方式不会影响最终结果。

定理还说明，第一章的固定“正向 + 撤销”模型可以嵌入到这里。因此第二章不是推翻第一章，而是把“固定撤销动作”推广为“每次执行返回撤销动作”。

这使得效应可以模块化。小效应可以组成中效应，中效应再组成组件级效应，框架不用为每一层重新发明撤销逻辑。

定理11：见证可继承

这条定理说明，带见证效应在组合后仍然带见证。证明直觉很简单：如果第一步能撤回第一步，第二步能撤回第二步，那么组合撤销时先撤第二步、再撤第一步，就能回到组合执行前的状态。

定理还把第一章和第二章连起来：如果固定动作对本来就满足全局撤销条件，把它嵌入到带见证效应后，也一定满足带见证要求。

这正是论文想要的工程性质：开发者只需为每个原子效应提供清理方式，框架可以从这些原子清理方式自动构造复杂清理方式。

定义12：效应提升

效应提升把“作用在普通上下文上的效应”提升成“作用在效应上下文上的效应”。换句话说，原来的效应只知道怎样修改状态；提升后，它还会把本次撤销动作记录进恢复器。

这一步有两层含义。

第一层是正向执行：原效应修改当前状态，并返回本次撤销函数；提升后的上下文同时更新状态和恢复器。

第二层更微妙：提升后的效应本身也要返回一个高一层的撤销动作。撤销一个“已经被记录的效应”，不仅要撤销底层状态，还要在更高层说明“如果这次撤销也需要撤销，应该怎样重新执行”。这就是论文递归上下文思想的来源。

实际读论文时，这里公式会显得比较绕。抓住一点即可：效应提升让“执行、记录、撤销记录本身”都服从同一套上下文规则。

定理13：提升保持组合

这条定理说明，效应提升和效应组合相互兼容。先组合两个效应再提升，和先分别提升再组合，得到的行为一致。

从工程角度看，它保证框架可以把“执行并记录清理”写成统一机制，而不需要为不同组合层级写不同版本。无论组件内部有一个效应还是十个效应，最终都能通过同一套提升规则进入上下文。

定理14：层级投影

提升后的效应运行在“带恢复器的上下文”上，但如果只看底层当前状态，它仍然等同于原效应的正向行为。

这条定理解释了为什么递归提升不会改变底层业务语义。高层结构添加了恢复器和记录逻辑，但底层状态变化仍然是原操作本身。

它也帮助理解论文中的层级上下文：父上下文管理子上下文的效应，但子上下文里的实际业务状态仍按组件原本的效应变化。提升只是在旁边维护恢复信息，不是把业务状态改造成另一套语义。

定理15：提升后的恢复条件

这条定理指出一个很关键、也很容易漏掉的细节。提升后的高层撤销动作，可以把底层当前状态恢复回去；但它不一定能把恢复器本身也恢复成逐字相同的样子。

要让恢复器也完全相同，需要更强的“全局逆”条件。可是定义8只要求撤销函数能撤销本次实际变化。工程中的清理函数通常就是这种局部保证：它能清理自己这次创建的资源，但不保证对任意状态都是完美逆函数。

因此论文没有把“恢复器内部完全一样”作为基本要求，而是保留一个更现实的目标：恢复器最终指向的恢复结果不变。恢复器的内部写法可能不同，但从当前状态一路恢复回去，得到的可观察结果仍然正确。

这条定理让模型既严格又贴近真实代码。它承认局部撤销函数通常不是完美数学逆，同时保留足够强的恢复不变量，使组件卸载仍然可推理。

定理16：后进先出恢复

这条定理说明，一串带见证效应按执行顺序应用后，如果按相反顺序撤销，那么每一步都会遇到它自己当初产生的状态，因此能准确回到该效应执行前的上下文状态。

这就是常见的栈式资源管理原则。先申请的资源后释放，后申请的资源先释放。论文把它推广到任意上下文效应，而不只限于文件、锁或内存这类传统资源。

定理16不需要独立性假设，因为它只处理后进先出顺序。每个撤销函数都在最适合它的状态上执行，也就是它对应正向效应刚刚执行完的那个状态。

这个结论还没有处理“多个组件互相交错”的问题。它解决的是单条效应序列内部的恢复正确性。后面的独立性理论会处理跨组件交错，以及不按栈顺序卸载的问题。

定义17：变换幺半群

一个效应会产生一个正向状态变化，也可能在不同状态下产生不同撤销动作。论文把这些正向动作、撤销动作以及它们的各种组合收集起来，称为这个效应的变换幺半群。

这个结构用于描述某个效应“可能对上下文做出的所有相关动作”。后面判断两个效应是否独立时，不能只看正向动作，还要看它们可能返回的撤销动作，以及这些动作继续组合后的结果。

如果一个效应来自固定的正向动作和固定撤销动作，那么这个集合就比较简单；如果撤销函数依赖运行时状态，集合就可能包含更多候选撤销动作。

引理18：只看生成动作即可

这条引理说明两件事。

第一，如果两个效应的基本动作彼此可交换，那么由这些动作组合出来的所有复杂动作也彼此可交换。换句话说，检查全部组合太多，但只要基本动作之间都不冲突，闭包出来的组合也不冲突。

第二，组合效应不会凭空产生超出原有效应范围的新动作。它的所有相关动作都来自原来两个效应的相关动作。

这让独立性检查变得可操作。我们不必检查所有可能组合，只要检查基本动作之间是否冲突。后文关于依赖键可交换性的结论也依赖这个引理。

定义19：效应独立

两个效应独立，不只是说“先做 A 再做 B”和“先做 B 再做 A”最终状态一样。论文要求更强的条件。

第一，它们所有相关动作都能交换顺序。这不仅包括正向动作和正向动作，也包括正向动作和对方撤销动作、撤销动作和撤销动作。

第二，一个效应的动作不能改变另一个效应会返回哪个撤销函数。否则即使最终状态看似不冲突，恢复时也可能出错。例如 A 的存在让 B 注册到不同位置，B 返回的清理函数就可能变了；这时 A 和 B 不能算独立。

这个定义比普通“两个操作可交换”更强，因为动态卸载需要的是“一个组件的贡献可以从交错历史中单独拿掉”，而不是只比较两种执行顺序的最终状态。

如果一个效应要和自己独立，也要求它自己的相关动作彼此可交换。后面论文会把这个思想放到依赖键操作上：某个键内部的操作如果彼此独立，就称这个键是可交换的。

定理20：删除一个独立效应

这条定理处理一串两两独立的带见证效应。假设一串效应已经执行，现在想把其中某一个单独撤掉。定理说明：只要它和后面的效应都独立，它的影响就可以一路穿过后面的效应，被单独分离出来。

直观地说，独立效应不会把彼此绑死。一个效应即使发生在中间，后面也可以把它单独撤掉，而不破坏其他效应的恢复逻辑。

这就是动态组件卸载真正需要的局部结论。组件 A 先加载，组件 B 后加载；现在要卸载 A，但 B 还留着。如果 A 和 B 的效应独立，A 的撤销函数可以穿过 B 的状态贡献，只撤回 A 自己。

推论21：任意顺序撤销

这条推论把前一定理用于整串效应：如果所有效应两两独立，那么它们的撤销函数可以按任意顺序执行，最终都能回到初始状态。

这比后进先出恢复更强。后进先出不需要独立性，因为它总是撤销最近发生的动作；任意顺序撤销需要独立性，因为撤销一个早发生的动作时，后面的动作可能仍然留在状态里。

动态组件系统正需要这个性质。组件可能按 A、B、C 顺序加载，却按 B、A、C 顺序卸载。独立性让这种非栈式卸载仍然可推理。

这一章最后给出局部时间可组合性的边界：单个组件内部可以依赖恢复器的后进先出顺序；多个组件之间若想任意交错和任意卸载，就必须另外证明独立性。论文后面会用观察等价和依赖键的可交换操作来支撑这种独立性，再在第 4 章把它提升为整个组件生命周期的恢复精确性。

依赖上下文

本章解释论文 3.2 节，覆盖编号 22 到 31。

前两章解决的是时间方向：一个组件做过的修改，之后怎样撤销。第三章转到空间方向：组件需要哪些依赖，谁提供这些依赖，依赖出现或消失时系统怎样发现。

论文把这种“从环境读取需求”的结构称为余效应。为了贴近工程语境，可以把它理解成一种更严格的依赖上下文：它像依赖注入容器一样从键找到值，但每个键有自己的类型和操作边界，提供依赖本身也必须可撤销，依赖变化还要能驱动组件生命周期。

定义22：依赖表

依赖表是一张有限表：每个依赖键都有自己的值类型，表里只保存当前已经提供出来的键和值。

它比普通键值表更严格。读取一个不存在的键是非法的；设置一个已经存在的键也是非法的；移除一个不存在的键同样非法。违反这些前置条件时，不产生合法状态转移，可以理解为运行时错误。

这条定义让“组件依赖环境”成为上下文中的一等结构。后面组件声明依赖时，实际上就是声明自己要求这张表中出现某些键。

“有限”也很重要。依赖满足性要能被运行时检查；如果依赖表不是有限可检查结构，响应式激活和失活就无法落地。

定义23：读取和设置

读取操作从依赖表中取出某个键的值，前提是这个键已经存在。设置操作把一个键和值放进依赖表，前提是这个键尚未存在。

关键在设置操作：它返回的不只是新依赖表，还返回一个撤销动作，用来删除刚设置的键。因此，提供依赖本身就是一个带见证的可撤销效应。

这把时间方向和空间方向连接起来：依赖的注册由效应系统跟踪，依赖的存在又由余效应系统用于组件激活。组件提供依赖时，系统自动知道怎样撤销这个提供。

换句话说，依赖操作不是另一套独立机制，而是可撤销效应作用在依赖表上的特例。这样注册依赖、撤销依赖、触发依赖变化通知，都可以复用前两章的恢复理论。

定义24：依赖项

一个依赖键不只是一个名字和一个值类型，还包含两层约束。

第一，这个键上的两个值怎样才算“观察上相同”。例如两个服务实例也许不是同一个对象，但它们暴露给组件的行为完全一样，就可以被某个等价关系视为相同。

第二，这个键允许组件执行哪些操作。每个操作可能读写该键的值，返回新的值、撤销动作和业务结果。业务结果可以是注册得到的句柄、查询得到的输出，或创建得到的标识。

论文要求这些操作尊重该键自己的等价关系：等价输入要么都能执行，要么都不能执行；执行后得到的结果也应该等价；返回给组件的业务结果也应一致。这是后面“观察等价”的基础。

依赖操作提升到整张依赖表时，只能读写自己的键，不能顺手改别的键。正是因为这个限制，论文后面才能证明不同键上的操作天然独立。

定义25：依赖声明

依赖声明就是一组依赖键。只要组件声明的所有键都已经出现在依赖表中，这个声明就被满足。

这是一种非常简化但有力的依赖模型。组件不需要自己轮询依赖是否存在，也不需要在每次读取时临时处理缺失依赖；运行时可以根据声明统一决定组件是否应当激活。

后面在实现中，这对应组件的注入声明。配置层只要知道组件声明哪些键，就能判断它什么时候可以加载，什么时候应该卸载或重载。

需要注意的是，定义25只声明“需要哪些键”，不指定“由哪个组件提供”。提供者解析是第 4 章目标视图负责的事情。

定义26：变化通知

变化通知比较依赖变化前后，某个组件的依赖声明是否被满足。

原来不满足、后来满足：组件有机会激活。
原来满足、后来不满足：组件应当失活。
满足性没有改变：这次变化对该组件是中性的。

这条定义把依赖变化转化成生命周期信号。提供者出现时，消费者可以被激活；提供者消失时，消费者必须进入卸载流程。

它也指出局部空间组合性的边界：通知能发现依赖变了，但还不能保证提供者会等消费者完成卸载再撤回资源。论文明确说，如果 A 提供某个键，B 依赖这个键，那么 B 的激活必须晚于 A 的提供；但 A 卸载时，单靠通知不能保证这个键在 B 清理完成前仍可读。这个更强的全局顺序要到第 4 章通过生命周期守卫和已提交视图来解决。

所以定义26提供的是“变化被发现”的机制，不是完整调度语义。真正的激活、失活、卸载等待会在生命周期演算里定义。

定义27：两种实现方式

效应可以有两种实现方式。第一种是原地修改：直接改当前上下文，并返回一个真正会撤销修改的函数。第二种是派生上下文：不改原上下文，而是创建一个带有不同访问规则的新上下文，恢复时只需丢弃它。

隔离和拦截更适合派生方式，因为它们改变的是“这个组件如何解析或使用依赖”，而不是共享依赖表中的实际值。

这条定义帮助区分两类上下文变化：有些变化是共享环境的可撤销修改，有些变化只是产生一个局部视角。两者都属于上下文范式，但恢复成本和跟踪方式不同。

在纯函数实现里，两种方式差别不大，都是返回一个新值；在命令式运行时里差别更明显：原地修改需要记录撤销动作，派生上下文只要让派生作用域结束即可。

定义28：隔离上下文

隔离上下文把逻辑依赖键和实际存储位置分开。组件仍然读同一个逻辑键，但这个键可以在不同上下文中解析到不同隔离域。

这允许同一个依赖键在不同组件或不同子上下文中对应不同值。例如测试组件可以使用模拟数据库，生产组件使用真实数据库，二者都读同一个逻辑键，但解析到不同绑定。

这种机制比普通依赖注入更细粒度，因为隔离可以在运行时按上下文调整，而不是全局替换某个服务。多个逻辑键也可以解析到同一个隔离域，从而共享同一个实际绑定；这给多租户、测试沙箱、局部覆盖提供了统一表达。

定义29：隔离操作

隔离版本的读取和设置都先经过隔离域解析。读取时，先看这个逻辑键在当前上下文里指向哪个隔离域，再去实际存储表里取值；设置时，也是在解析后的隔离域上写入。

隔离操作本身不写共享依赖表，只派生一个新上下文，在这个新上下文中某个逻辑键解析到指定隔离域。已有隔离可以被重新指定，因为派生上下文只改变视角，不需要像设置操作那样检查“是否已经提供”。

从实践看，这相当于给某个组件树换一套依赖命名空间。它让多个组件可以同时使用同名依赖，但互不影响。

需要区分设置和隔离：设置仍然是可撤销效应，因为它向某个隔离域写入提供值；隔离是派生上下文操作，因为它只改变当前作用域如何解析键。

定义30：拦截上下文

拦截上下文把依赖值的提供方式改为“根据元数据生成值”。依赖表里保存的不再只是一个现成值，而是一个提供函数；组件读取依赖时，会把自己的声明元数据和上下文携带的元数据合并，再交给这个提供函数。

这适合表达横切策略。例如文件系统服务可以根据元数据限制路径范围，数据库服务可以根据元数据决定权限级别，日志服务可以根据元数据附加标签。

重要的是，拦截改变的是如何使用依赖，而不是依赖是否存在。因此，改变拦截元数据通常不需要让依赖图整体重载。

定义31：拦截操作

拦截下有三类操作：读取、设置和拦截。读取会合并组件声明元数据和上下文元数据，再调用提供函数；设置注册的是提供函数；拦截则在派生上下文中追加或覆盖某个键的上下文元数据。

论文强调，元数据怎样合并由每个键自己定义。可以是覆盖，可以是集合合并，也可以是其他策略。上下文携带的元数据优先级更高，因此外层上下文可以约束内层组件。

这条定义把权限控制、沙箱策略、访问拦截等机制纳入余效应模型，同时保持组件代码不需要直接知道外层策略。

例如组件声明“我要访问某个目录”，外层上下文可以通过拦截元数据把访问限制到更小目录、附加审计标签或覆盖某些权限字段。组件仍然按同一个键读取依赖，但实际拿到的值已经被外层上下文策略加工过。

统一上下文

本章解释论文 3.3 节，覆盖编号 32 到 42。3.3.3 节没有新的编号条目，但它解释了为什么作者把前面的统一上下文称为一种编程范式。

前面两条线分别解决时间和空间：效应上下文负责“修改怎样撤销”，依赖上下文负责“依赖怎样声明和响应”。这一章把两者合成同一个递归上下文，并引入观察等价，让恢复和独立性不再要求物理状态逐字相等，而是要求组件能观察到的行为一致。

定义32：递归上下文

论文把效应上下文和依赖上下文统一成一个递归上下文。这个上下文包含三项：当前层状态、当前层恢复器、当前层依赖表。

这样一来，前面“状态 + 恢复器”的结构不再只是外面包一层，而是折叠进一个自相似的上下文里。上下文内部仍然可以包含上下文，组件创建子组件时也就自然对应到上下文的递归组合。

这条定义是论文所谓“上下文范式”的核心：所有组件和环境的交互都通过上下文发生，效应和依赖不再分散在全局变量、隐式注册表或手写生命周期回调中。

论文还强调，依赖表的键类型并不局限于传统“服务依赖”。任何需要跨组件共享的状态，都可以编码成某个依赖键上的值。这样，组件对共享环境的读写原则上都可以纳入依赖操作，再由效应系统跟踪恢复。

递归结构也对应层级组合。父上下文聚合子组件的效应，子组件可以继续创建子上下文。加载组件相当于执行其效应，卸载组件相当于执行恢复器；这种“插入/拔出”不再只是比喻，而是被上下文类型直接表达。

定义33：观察等价

真实系统很难恢复到物理上完全相同的状态。例如释放内存后，堆布局未必和分配前完全一样；动态生成的名称也不一定重复出现。因此论文用观察等价代替严格相等。

两个依赖上下文如果绑定同样的键，并且每个键上的值按该键自己的等价关系来看相同，就认为它们观察等价。两个完整状态是否观察等价，则只看组件能通过依赖上下文观察到的部分是否等价。

这样，系统恢复时不要求所有内部细节完全一致，只要求组件通过声明依赖能观察到的部分一致。这更符合工程上的“恢复正确”。

这个定义会“忘掉”没有绑定到任何依赖键的状态部分。论文不是说这些部分不存在，而是说如果它们没有通过依赖上下文暴露给观察者，就不应当影响恢复正确性的判断。

因为观察等价的状态有同样的依赖键集合，所以它们对依赖声明的满足性一致，对变化通知的分类也一致。这使得响应式依赖可以在观察等价意义下工作。

定义34：不可区分测试

为了说明某个键上的等价关系是否合理，论文定义了测试。测试由该键允许的操作组成，是一个有限操作序列；每一步把当前值继续交给下一个操作，并记录正向操作产生的业务结果。如果某一步前置条件失败，那么测试在这个值上未定义。

如果两个值对所有这种测试都表现一样，那么它们就是不可区分的。观察者只拥有这些操作，所以如果操作无法区分两个值，理论就不应强行把它们区分开。

这条定义把“等价”建立在可观察行为上，而不是底层表示上。它为后面判断操作是否可交换提供了更宽松也更实用的标准。

测试里不只考虑正向操作，也考虑可能的撤销动作。因此，撤销动作能造成的可观察差异也会被纳入比较。这样得到的不可区分性才足以支撑恢复和任意顺序撤销。

引理35：最粗观察关系

这条引理说明，不可区分关系是操作能够尊重的最宽松关系。所有允许操作都不会把不可区分的值变成可区分的表现。

反过来，如果某个等价关系能被所有操作尊重，那么它一定不会比不可区分关系更宽。也就是说，不可区分关系是这些操作视角下最大的合理等价。

这让论文后面可以安全地用观察等价替代严格相等：只要操作看不出区别，组件运行也不应依赖这些隐藏差异。

开发者可以为某个键选择更细的等价关系，但不能比“所有操作都无法区分”的关系更宽，否则某些操作会把等价输入变成可区分输出。最自然的选择就是直接采用这个不可区分关系。

定义36：尊重等价

一个映射尊重等价，意思是它不会把等价输入变成不等价输出。两个映射如果在每个输入上给出等价输出，就可视为观察上相同。

这条定义把观察等价从值扩展到函数、撤销函数和效应返回的成对结果。因为效应不只返回新状态，还返回撤销函数，所以撤销函数本身也要按观察等价比较。

后面所有“按等价恢复”的结论都依赖这个定义。否则，状态看似等价，但返回不同撤销函数，恢复行为仍可能分叉。

定义37：按等价恢复

这条定义把前面的带见证效应改写成观察等价版本。一个效应要被认为可恢复，需要满足三件事：效应本身尊重观察等价；本次返回的撤销函数能把新状态恢复到与旧状态观察等价；撤销函数本身也尊重观察等价。

如果把观察等价收紧成严格相等，就回到前面较强的定义。因此这不是另一个体系，而是前面体系的现实化版本。

它特别适合运行时组件系统，因为卸载后很多内部细节不可能完全回到原位，但只要组件可见的依赖和行为一致，就足够支持组合推理。

引理38：恢复结论可按等价重读

这条引理说明，第 3.1 节中关于恢复的所有“状态相等”结论，都可以改成“观察等价”结论。恢复器由多个撤销函数组合而成，只要每个撤销函数尊重等价，组合也尊重等价。

因此，前面建立的跟踪、恢复、后进先出撤销等结果，不会因为放宽成观察等价而失效。此时恢复正确性不变量也从“严格回到原状态”改写成“回到观察上等价的状态”。

这条引理承担承上启下的作用：前半部分用较直观的严格相等说明恢复，后半部分转向真实系统需要的可观察等价。

它还为后面的独立性放宽铺路。两个操作也许不能让底层表示完全相同，但只要它们留下的值按观察等价看不可区分，就可以算作可交换。

定义39：操作独立

两个依赖操作独立，首先要求它们作为效应彼此独立。也就是说，正向动作、撤销动作和撤销函数选择都要相容。

但依赖操作比普通效应多一个业务结果，所以定义39再加一条：一个操作的动作不能改变另一个操作产生的结果。

为什么还要管“结果”？因为很多操作不只修改状态，还返回值。例如分配资源会返回句柄，注册路由可能返回标识。如果执行顺序改变会导致返回结果不同，就不能视为独立。

如果同一个键上的任意两个操作都独立，论文称这个键可交换。这里还要求一个操作和自身也独立，所以“可交换键”是对该键暴露接口的一项强约束，不是自动成立的性质。

定理40：不同键天然独立

这条定理说明，作用在不同依赖键上的操作天然独立。因为每个操作只读写自己的键，一个键上的操作不会改变另一个键的值，也不会改变另一个键操作的结果。

这个结论让依赖表的分解有了组合意义。只要系统把共享位置拆成不同键，很多操作之间的独立性就能直接获得。

真正需要额外设计的是同一个键内部的操作。例如，向一个表里独立添加和删除条目，像注册路由或事件监听器，通常可以设计成可交换；但向有序中间件链里插入处理器通常不可交换，因为先后顺序会改变请求经过的处理链。

论文还用内存分配说明“是否可交换”取决于接口暴露了什么。如果句柄只在内部重命名、外部操作无法比较地址，那么两个分配顺序可能不可区分；如果地址作为可比较结果暴露出来，两个分配顺序返回不同地址，就不能算可交换。

定义41：由依赖操作构成的效应

组件的效应通常不是单个依赖操作，而是一串操作，并且后一步可能取决于前一步的结果。这条定义用递归方式描述这类由依赖操作构成的效应。

每一步先执行某个键上的操作，得到新状态、撤销函数和业务结果；然后根据结果选择下一段效应。这样可以表达真实组件加载逻辑中的分支、顺序和依赖结果。

论文把这种效应看成“由余效应介导的效应”。它说明组件对环境的修改，原则上都应通过它声明和获取到的依赖接口进行。

这里的“递归构造”还要求把所有可能分支都纳入考虑。因为一个操作结果不同，后续效应可能不同；证明独立性时不能只看某一次运行碰巧走到的路径。

定理42：可交换键带来独立效应

这条定理说明，如果两个效应共同操作的键都是可交换的，那么这两个效应整体独立。不同键上的操作天然独立，同一个键上的操作则由可交换性保证。

它把接口层面的设计要求转化成系统层面的并发和卸载性质。只要组件通过合适的依赖键操作环境，并且共享键的操作设计为可交换，不同组件的效应就能安全交错。

这也是论文从局部代数结构走向组件系统的关键桥梁。它说明独立性不是凭空假设，而可以由依赖接口的可交换性来支撑。

这条定理也有两个边界。第一，系统必须把所有跨组件共享的位置都绑定成依赖键，否则那些没有进入依赖表的共享状态不在证明范围内。第二，一个键是否可交换，是它提供的接口性质，责任在提供这个键的组件或框架设计者，而不是使用者临时补救。

本章补充：上下文范式的定位

论文 3.3.3 把这套机制放到编程范式谱系里比较。纯函数式写法倾向于显式传递状态，推理清晰，但调用链里到处都要接收和返回状态。命令式和面向对象写法倾向于隐式修改共享状态，写起来方便，但依赖和副作用常常藏在运行时容器、全局注册表或框架内部，分析和重构成本高。

上下文范式试图结合两者：组件通过显式上下文和环境交互，所以每个效应和依赖都能归属到某个上下文、某个组件；但开发者不必手动把完整状态穿过每一层函数，也不必为组合后的卸载和重连写全局流程。

在效应方向，开发者只为原子操作提供撤销函数，组合操作的撤销由上下文累积器自动得到。在依赖方向，开发者声明需要哪些余效应，运行时负责解析、通知、激活、失活和重连。论文称它为一种编程范式，是因为它不只是一个接口技巧，而是把副作用和依赖都强制收束到同一个上下文交互模型里。

组件模型

本章解释论文第 4 章开头、4.1 节和 4.2 节，覆盖编号 43 到 48。4.2 节还有五条基础演算规则，虽然没有单独编号为定义或定理，但它们是理解后续生命周期扩展的基础。

第 3 章只证明局部性质：一个效应序列怎样恢复，一个依赖声明怎样被满足或失效。第 4 章开始把这些局部机制放进一个动态系统：系统由组件组成，组件实例化成纤程，纤程被注册表管理，并通过生命周期规则加载、卸载、退休和删除。

论文先给出一个最小演算：所有转换都是原子、立即、不会失败的。下一章“生命周期”再逐步放开这三个假设，加入卸载等待、多步迭代、异步和失败。

定义43：组件

组件由三部分组成：依赖声明、提供声明和带见证的效应函数。

依赖声明说明组件运行前需要环境提供哪些键；提供声明说明组件激活后可能向环境提供哪些键；效应函数说明组件激活时要做什么，以及这些动作怎样撤销。

论文还要求：组件的效应函数不能写出提供声明之外的键。依赖声明是读边界，提供声明是写边界，效应函数是实际执行逻辑。

同一注册表中不同纤程的提供声明不能相交。这保证一个键最多有一个提供者，依赖解析不会出现歧义。隔离机制可以放宽这个限制，但第 4 章基础演算不引入隔离域，只采用单一共享域。

这个约束也意味着：如果某个组件有非空提供声明，它在同一个共享域里通常只能有一个实例；能大量实例化的是那些不提供键、只消费依赖或只注册子组件的组件。

这一条把前面的效应和余效应合成组件接口。组件不再只是代码模块，而是带有明确读写边界和恢复行为的运行时单元。

定义44：纤程

纤程是组件的一次运行实例。它记录组件定义中的依赖声明、提供声明和效应函数，也记录父纤程、自己的依赖表、退休标记和生命周期状态。

一个组件可以被实例化多次，每个实例有自己的生命周期和恢复器。因此论文不用“组件”直接表示运行实体，而引入“纤程”作为动态实例。

在基础模型里，生命周期状态只有两种：未激活，或已经活跃。活跃状态中保存两件事：组件激活时累积出来的恢复器，以及本次激活时提交的依赖解析结果。

后面 4.3 节会把这个两态模型扩展成加载中、活跃、卸载中、失败结果等更真实的状态；但定义44的基本字段在两套模型中保持一致。

定义45：注册表

运行状态携带一个纤程注册表。它把纤程名字映射到纤程实例。纤程的父指针形成一棵以根为起点的树，表示组件实例之间的嵌套关系。纤程名字是原子标识，只能比较是否相等，不能依赖名字内部结构。

当前依赖表不是单独维护的全局表，而是由所有活跃纤程自己的依赖表合并出来。因为不同纤程的提供声明不相交，而且每个纤程只能写自己声明会提供的键，这个合并结果是明确的。每个键如果存在，就有唯一提供者。

这条定义也区分了两种状态修改：依赖表中的修改会被其他组件通过依赖声明观察到；其他环境修改仍由恢复器跟踪，但不会进入依赖解析。

论文特别强调，没有规则直接写全局依赖表。全局依赖表只是活跃纤程的局部依赖表合并结果。一个纤程卸载或停止活跃后，它的提供就从全局依赖表中消失；但它自己的实际资源撤销可能稍后由恢复器完成。这个区分是后面解决“提供者要等消费者清理完再撤销”的基础。

定义46：目标视图

目标视图表示某个纤程现在应该处于什么依赖解析状态。

如果纤程已退休，或它声明的依赖当前不满足，目标视图就是空，表示它不该运行。否则目标视图是一张表，记录它的每个依赖键当前由哪个提供者纤程提供。

纤程的已提交视图表示它上次激活时接受的依赖解析结果。生命周期规则通过比较目标视图和已提交视图，决定是否加载、卸载或重载。

这里记录提供者名字，而不是直接记录依赖值，是为了检测提供者替换。两个提供者也许提供观察上等价的值，但它们是不同纤程；如果提供者变了，消费者应该重新经历生命周期，而不是因为值相等就悄悄沿用旧绑定。

静止状态表示每个纤程都已经追上自己的目标：不该运行的已经未激活，该运行的已经活跃并且已提交视图等于当前目标视图。这个概念后面用于定义系统最终稳定，并证明进展和汇合。

4.2 节的基础演算围绕目标视图给出五条规则：

插入：编排器插入一个新纤程，要求名字新鲜、父纤程存在或为根、组件合法、提供键不与现有纤程冲突。
退休：编排器把某个纤程标记为退休。这是请求停止，不直接改生命周期状态。
移除：只有退休、未激活、没有子纤程的条目才能从注册表删除。
重载：未激活且目标视图非空时，执行组件效应，得到新状态和恢复器，并把纤程置为活跃。
卸载：活跃但已提交视图与当前目标视图不一致时，执行恢复器，并把纤程置回未激活。

这些规则把第三章的响应式依赖落实成生命周期驱动：目标视图变了，就触发加载或卸载。

定义47：注册子组件

组件执行效应时，可以注册新的子组件。论文把这种注册看成父纤程的一个可撤销效应：正向动作是插入子纤程，撤销动作是退休这个子纤程。

为什么撤销动作不是直接删除？因为删除有前置条件：子纤程必须已经未激活且没有孩子。如果把删除作为撤销函数，父纤程运行恢复器时可能因为子纤程还活跃而失败。

所以论文让注册动作的撤销函数是“退休”。退休只有“纤程存在”这个前置条件，更适合放进恢复器。退休后，普通生命周期规则会把子纤程的目标视图变为空，触发它自己卸载；如果它还注册了孙子组件，孙子也会通过同样机制级联退休。

这条定义让组件树的动态扩展也纳入效应跟踪。父组件卸载时，它注册过的子组件会被退休，形成级联清理。

被退休但尚未删除的空条目后面称为残留条目。引理57会证明这种残留条目在观察上等价于不存在，因此“先退休、后按条件删除”不会污染系统语义。

定义48：限制作用域

限制作用域规定，纤程的效应函数必须只在自己的边界内工作。它包含写边界和读边界。

写边界：对已有注册表来说，效应不能增删其他纤程，不能改其他纤程字段；它只能改变自己纤程的依赖表。注册子组件是唯一受控例外，因为定义47已经规定了它只能通过插入和退休发生。

读边界：效应可以读自己的依赖表，可以读自己声明依赖对应提供者表上的相关值，也可以读不属于任何纤程表的普通环境部分；但不能随意读其他纤程的控制字段，不能读自己没有声明的依赖表内容。

这个约束是防止组件“偷看”或“偷改”系统调度状态。若组件能根据别的纤程生命周期分支，或者直接修改其他纤程的表，后面的独立性和恢复证明都会失效。

定义48对正向状态变换和返回的撤销函数都提出这个限制。也就是说，不只是加载动作要守边界，卸载时运行的恢复动作也要守边界。这样第 4.4 节才能把生命周期规则列成完整的字段变化清单，并证明良构、恢复精确和汇合。

生命周期

本章解释论文 4.3 节和 4.4.1 节，并把定义60作为后续全局时间可组合性的入口，覆盖编号 49 到 60。

上一章的基础演算把生命周期简化成原子、立即、不会失败的加载和卸载。论文随后放开这三个理想化假设：卸载可能需要等待依赖自己的消费者；加载可能由多个步骤组成；异步步骤发出后不能随便取消；某个步骤还可能失败。为了承载这些现实情况，生命周期必须有“进行中”的状态。

定义49：扩展状态

基础生命周期只有未激活和活跃两个状态，但真实系统加载和卸载可能分多步、异步、失败。因此论文把生命周期状态扩展为四类：

未激活：纤程没有安装，可能带有失败结果。
加载中：纤程正在执行组件效应，已经累积了一部分恢复器，并提交了本次依赖解析。
活跃：纤程成功加载，持有恢复器和已提交视图。
卸载中：纤程正在退出，等待安全时机运行恢复器，并保留最终结果。

这条定义使得生命周期可以表达真实运行时：组件可能正在加载，加载途中依赖变化，异步动作已发出，某步失败后需要先恢复已完成部分。

论文还定义了两个谓词：只要纤程不是未激活，就算已经安装；如果纤程处于带错误的未激活状态，就算失败。

扩展后的静止状态也要重读：加载中和卸载中永远不是静止；活跃状态静止当且仅当当前目标视图等于已提交视图；正常未激活静止当且仅当目标视图为空；失败后的未激活即使目标视图非空也可以静止，因为失败后不会自动重试。

还有一个关键规则延续自定义45：全局依赖表仍然只合并活跃纤程的表。加载中和卸载中的纤程虽然已经安装、持有已提交视图、可以通过旧视图读取依赖，但不向新消费者提供依赖。这一点后面支撑卸载顺序。

定义50：被依赖

如果某个已安装纤程的已提交视图中，有依赖键解析到另一个纤程，那么后者就是被依赖的。被依赖的提供者不能真正完成卸载。

生命周期规则因此把卸载拆成两段：先进入卸载中，使它不再对新消费者可见；然后等所有旧消费者离开后，才运行恢复器撤回实际资源。

这解决了第 3 章留下的问题：消费者失活时可能仍需要使用原来的依赖完成清理，所以提供者不能在通知消费者后立刻撤销依赖。

为什么不会死锁？因为提供者进入卸载中后，不再是活跃状态，它的依赖表不再进入全局依赖表，新消费者不会再把它选为提供者。旧消费者还通过已提交视图指向它，于是会被推动进入自己的卸载流程；等这些旧视图消失，被依赖守卫就会释放。

这个守卫是按依赖绑定关系判断的，不是按父子树判断的。父组件和子组件的生命周期不靠它强制排序；只有“某个已安装纤程的依赖解析到了某个提供者”才会阻止提供者完成卸载。

定义51：效应迭代器

效应迭代器把组件激活过程拆成多个步骤。每一步产生新状态、撤销函数和一个继续标记：要么迭代结束，要么还有下一步。

这种结构对应真实代码中的生成器或异步流程。组件加载可能注册多个资源，每个资源注册完成后才知道清理函数，并且每个步骤之间系统状态可能变化。

带见证的迭代器要求每一步返回的撤销函数都能把本步造成的改变恢复到观察等价的旧状态。同时，迭代器本身和返回的撤销函数都要尊重观察等价。

这让加载可以在步骤边界被中断。已经完成的步骤有恢复器；还没开始的步骤没有副作用；因此加载中途发现目标视图变化时，系统可以只撤销已完成部分。

定义52：迭代器提升

迭代器提升把多步效应变成一个可跟踪效应。每执行一步，就把该步返回的撤销函数组合进恢复器；如果还有后续步骤，就递归处理下一步。

核心顺序仍然是后进先出：本步返回的撤销函数会排在旧恢复器前面，因此恢复时先执行最新清理，再执行旧清理。

如果迭代器正常结束，组件完成加载；如果中途目标视图变化，系统可以在迭代边界停止继续加载，并用已累积的恢复器撤销已完成部分。

这条定义让“加载过程可被打断”成为形式化机制。现实中的热替换、依赖变化、异步取消，都需要这种分步边界，而不是把整个激活看成一个不可中断动作。

在生命周期规则里，基础的重载被拆成四类动作：开始加载、执行一步迭代、完成最后一步、加载中发现目标变化后转入卸载。最后一种情况覆盖了“已经加载了一部分，但依赖或配置已经不再匹配”的场景。

本章补充：异步和失败

论文 4.3.3 讨论异步，但没有新增编号条目。它的要点是：异步迭代一旦发出，就有惯性，不能因为目标视图变化而假装没有发生。若依赖在异步等待期间变化，当前迭代仍要落地，拿到它产生的撤销函数，然后纤程进入卸载中，由恢复器撤销已经落地的部分。

论文 4.3.4 讨论失败，也没有新增编号条目。失败版迭代器的一次迭代要么成功返回新状态、撤销函数和后续步骤，要么返回错误。见证条件只约束成功情况，因为失败本身没有成功安装的新效应需要撤销。

失败对应的生命周期路径是：如果加载中的迭代器返回错误，纤程转入卸载中，先用已经累积的恢复器清理，再到达带错误的未激活状态。失败结果保存在纤程上，不会让父组件或整个系统直接失败；失败纤程也不再提供依赖，不会阻塞别的纤程的卸载守卫。

定义53：步骤和片段

论文把执行历史编号。每一步都记录当前状态、使用了哪条规则、作用在哪个纤程上。初始状态的注册表为空，所以每个纤程都必须通过插入规则出现。

某个纤程从进入已安装状态到离开已安装状态之间的最大区间，称为它的运行片段。它从开始加载打开，到真正卸载关闭；最后一个运行片段也可能还没关闭。

每一步又被拆成两部分：一部分是真正作用在上下文业务状态上的动作，另一部分是控制字段编辑，例如改变生命周期状态、设置退休标记、插入或移除注册表条目。

通过这种编号和拆分，论文可以讨论“别的纤程在我的加载和卸载之间插入了哪些步骤”，从而证明全局时间可组合性。

这一区分还带出两个不同的等价关系。一个关系忽略控制字段，用于描述“恢复是否只撤销了业务贡献”；另一个关系保留注册表和生命周期信息，用于判断规则能否执行。二者服务于不同证明，不能混为一谈。

引理54：字段变化规律

这条引理系统总结生命周期规则能改哪些字段。它来自规则表和限制作用域约束，主要包括五个事实：

某个纤程自己的依赖表只会在作用于这个纤程自己的步骤中变化。
已提交视图只在开始加载时出现，只在真正卸载时消失，所以在一个运行片段内保持不变。
累积恢复器只在真正卸载时应用到状态上，其他规则最多携带或更新它。
已安装状态只会由开始加载打开，由真正卸载关闭。
父指针、依赖声明、提供声明和效应函数在纤程创建后不再改变；退休标记只会从未退休变成已退休，不会反向变化。

这些字段规律是后面所有证明的基础。没有它们，就无法确认某条规则是否会偷偷改变别的纤程，或破坏依赖图。

规则表还说明，失败和普通离开只是改变生命周期状态；真正运行恢复器的规则只有最终卸载。这使得失败、普通卸载、加载中转卸载最终都汇聚到同一个恢复出口。

引理55：等价不变

这条引理说明，如果两个状态按扩展后的观察关系等价，那么同一生命周期规则在一个状态可执行，当且仅当在另一个状态也可执行；执行后结果仍然等价。

规则只读取生命周期字段、注册表结构、依赖键是否存在、目标视图等可观察信息，不会依赖隐藏表示细节。因此隐藏细节不同不会导致规则行为分叉。

这个引理让整个生命周期演算可以在观察等价意义下工作。也就是说，系统证明关心的是组件能观察到的状态，而不是所有底层实现细节。

引理56：名称重命名

纤程名称是动态生成的原子标识，没有内部结构。只要把一个状态中的所有名称一致地替换成另一组名称，生命周期规则的行为不变。

这处理了动态注册带来的偶然差异。两个运行历史可能生成了不同具体名字，但只要父指针、依赖视图等关系结构相同，它们应被视为同一类运行。

后面的汇合定理需要这个结论，因为不同调度顺序可能在不同时间生成子纤程名称。论文用重命名把这些无关差异排除掉。

引理57：残留条目

残留条目指已经退休、正常未激活、自己的依赖表为空、也没有任何子纤程指向它的纤程。这样的条目虽然还在注册表里，但对其他规则几乎不可见。

它不提供依赖，不被任何父指针引用，也不参与已安装关系。因此其他纤程执行规则时，存在或不存在这个残留条目通常没有区别。

这个引理解释了为什么注册子组件的撤销动作可以只退休而不立即删除。退休后留下的空壳不会影响其他运行，后续再按条件移除即可。

论文也说明了少数例外：如果删除残留条目后，这个名字重新变得可用，或它的提供声明不再阻止新插入，那么某些插入行为可能受影响。除了这种“名字新鲜性”和“提供冲突检查”层面的差异，残留条目可以被视为不存在。

定义58：良构注册表

良构注册表要求四件事：

父指针必须指向已有纤程或根。
不同纤程的提供声明不能相交。
已安装纤程的已提交视图必须覆盖它声明的全部依赖，并且指向注册表中的纤程。
如果已安装纤程的已提交视图把某个依赖解析到提供者，那么这个提供者也必须是已安装状态。

这一定义把注册表应满足的结构性约束集中列出。它保证组件树、依赖提供者和生命周期状态之间没有明显矛盾。

后面所有全局性质都默认从良构状态出发。若注册表本身已经损坏，再讨论恢复、顺序和汇合就没有意义。

父子树无环没有在定义58单独列成一条，因为定义45已经要求父指针形成树，而且纤程只能在父纤程已存在时创建。

定理59：良构保持

这条定理说明，只要某步之前注册表良构，执行任意一条生命周期或编排规则后，注册表仍然良构。

证明依赖前面的字段变化规律。例如插入纤程时会检查父指针和提供键冲突；移除纤程时要求没有子纤程；开始加载时写入的已提交视图来自当前活跃提供者；真正卸载只有在没有旧消费者依赖它时才会发生。

它说明规则设计不会把系统带进坏状态。特别是卸载守卫不仅服务于依赖顺序，也保证不会留下已提交视图指向已经卸载的提供者。

失败也通过“卸载中再到失败未激活”的路径收束，所以良构保持不需要为失败结果另开一套证明路径。

定义60：迭代器独立

这一条把独立性推广到效应迭代器。因为迭代器可能根据业务结果选择不同后续步骤，所以不仅要考虑当前步骤的正向动作和撤销动作，还要考虑所有可能继续执行到的迭代器。

两个迭代器独立，要求两类条件：

两者所有可能步骤产生的相关动作都可交换，按观察等价理解。
一个迭代器在被另一个迭代器的动作移动过的状态上执行时，仍返回等价的撤销函数和等价的后续步骤；如果步骤注册了子组件，注册出的组件也要一致。

这比普通效应独立更强，但也是必要的。否则，两个纤程的步骤虽然当前看似能交换，交换后却可能选择不同的下一步，最终运行历史就会分叉。

一个步骤序列被称为两两独立，是指这个序列中曾经出现过的每个纤程的效应迭代器两两独立。论文强调这是“族”而不是“集合”：同一个组件被实例化两次时，也要求它的迭代器和自身独立，也就是它自己的相关动作可交换。

定义60是下一章全局时间可组合性的前提。恢复精确定理主要使用动作可交换条件，汇合定理还需要“返回同样撤销函数和后续步骤”的条件来交换步骤顺序。

全局性质

本章解释论文 4.4.2 到 4.4.5 节，覆盖编号 61 到 73。

这一章把前面的局部机制提升为全局系统性质。这里所有结论都有明确前提，主要包括：步骤序列两两独立、注册表良构、依赖优先关系无环、每个迭代器长度有界、纤程名字集合有限、组件完整提供、最终状态无失败。不要把这些结论读成任意动态系统都天然成立；论文证明的是满足这些纪律的动态组件系统具备可组合性。

定理61：恢复精确

这条定理给出全局时间可组合性的核心结论。它说：在两两独立的前提下，把某个纤程当前累积的恢复器应用到当前状态上，效果等价于从它本次运行片段打开时开始，只保留其他纤程插进来的那些动作。

更直观地说，如果纤程 A 加载期间系统中还有 B、C 在活动，A 卸载时运行自己的恢复器后，B、C 的影响应该仍然保留，只有 A 的影响消失。

定理使用“忽略控制字段”的等价关系，因为恢复精确关注的是业务状态、依赖表和环境修改，而不是生命周期记录本身是否逐字段相同。

论文还提醒：如果 A 在运行片段中注册了子纤程，并且这些子纤程也执行了步骤，那么结论不能简单读成“A 从未发生过”。因为在没有 A 的历史里，这些子纤程也不会存在。这个问题要到引理72删除片段时一起处理。

推论62：结束恢复

这条推论把恢复精确定理用到运行片段真正关闭的时刻。纤程关闭时必然会执行自己的恢复器，因此关闭后的状态等价于：这个纤程自己的贡献被删除，只留下其他纤程在同一区间内做过的事。

它覆盖普通卸载、加载中转向卸载、失败后恢复等不同路径。因为所有这些路径最终都通过同一个卸载恢复规则运行累积恢复器。

这就是“组件卸载不留业务痕迹”的形式化版本。只要效应都经过上下文并满足独立性，卸载可以把组件贡献从历史中删除。

这里的等价关系不关心失败结果字段，所以普通加载中断和加载失败在“业务状态是否恢复”这个问题上走同一个证明。

定理63：依赖顺序

这条定理给出全局空间可组合性的核心顺序。它包含三层结论。

第一，一个纤程只有在依赖已经被提供时才能开始加载。

第二，如果消费者在自己的已提交视图中把某个依赖键解析到某个提供者，那么在消费者的整个运行片段中，这个解析保持不变。

第三，消费者的运行片段嵌在提供者的运行片段里面：提供者先开始，消费者后开始；如果提供者要结束，消费者必须先结束。

这意味着提供者先于消费者可用，消费者先于提供者完成退出。更强的是，消费者卸载过程中仍能通过已提交视图读到原来的提供者绑定。

这正是响应式依赖管理需要的顺序：依赖变化会让消费者停用，但提供者不会在消费者清理完成前撤回资源。

定理64：解析一致

这条定理说明，一个纤程在一次加载过程中使用的是同一个依赖解析结果。加载开始时，系统会提交当时的目标视图；在这一轮加载继续执行期间，目标视图必须保持一致。

如果依赖解析在加载中途变化，纤程不能继续假装没变。它要么已经完成并进入活跃状态，要么转入卸载，撤销已完成的部分。

异步步骤会带来一个现实细节：已经发出的异步动作可能必须落地，不能强行取消。因此论文允许它先落地，再立即进入卸载恢复。这保证加载过程不会横跨两个不一致的依赖解析。

定理的分支覆盖“正常完成”“异步落地但目标已过期”和“加载失败”。后两种都会进入卸载路径，再由结束恢复推论保证已完成贡献被撤销。

定义65：优先关系

如果一个纤程可能提供另一个纤程声明的某个依赖键，论文就认为前者在优先关系上先于后者。

这个关系只读取依赖声明和提供声明，而这些字段在纤程创建后不再改变。

优先关系描述激活依赖，而不是父子生命周期。A 先于 B，表示 B 需要等 A 提供依赖后才能激活；而 A 是否必须活得比 B 久，是前面依赖顺序定理保证的。

论文后面的进展和汇合都假设优先关系无环。如果组件声明自己依赖自己提供的键，或形成互相依赖环，系统可能永远无法激活它们。

定理66：进展

这条定理回答“系统会不会一直卡在半加载、半卸载状态”。在一组有限性和无环性前提下，如果系统不是静止状态，就总能找到下一条生命周期规则可以执行；并且每个纤程的生命周期步骤数有界，最终会到达静止状态。

它的前提很重要：

依赖优先关系必须无环。
每个效应迭代器长度有界。
本次历史中出现过的纤程名字集合有限。
注册表保持良构。

证明直觉是：优先关系无环，所以总能找到某个没有未满足前置依赖的纤程推进；迭代器长度有界，所以加载不会无限执行内部步骤；名字集合有限，所以不会靠无限注册新纤程逃避结束。

纤程名字集合有限是一个假设，不是定理自动推出的。论文解释说，这排除了组件无限制注册自身实例这类情况；如果组件注册树深度和分支都有界，就能满足这个条件。

定义67：支持集合

支持集合描述在某个状态中哪些纤程“应该被保留”。一个纤程被支持，需要满足两类条件：

如果它不是根插入的，则创建它的父纤程也被支持。
它声明的每个依赖键，都由某个被支持的纤程可能提供。

支持关系把父子树和依赖优先关系合在一起。父组件支持子组件，提供者支持消费者。最终静止状态应该只留下被最终配置和依赖关系支持的纤程。

注意支持集合使用的是“可能提供”的声明，而不是当前实际依赖表。因此如果组件声明“可能提供”但成功激活后没有全部提供，支持集合会高估实际可运行纤程。定义69会补上这个缺口。

引理68：支持有根基

这条引理说明，在优先关系无环时，支持集合是良好定义的，并且存在唯一的最小支持集合。

直观地说，如果没有依赖环，就可以从根插入的纤程开始，一层层加入父子关系支持的纤程和依赖关系支持的纤程。这个过程不会陷入“必须先有自己才能支持自己”的循环。

结论还说明，支持集合只由退休标记、父指针、依赖声明和提供声明决定。它不依赖调度过程，也不依赖纤程当前正在加载还是卸载。

定义69：完整提供

完整提供是对组件提供声明的加强。组件声明自己可能提供哪些键，定义43只要求它不要写出这个范围；定义69进一步要求：凡是这个组件实例成功活跃，它就必须把自己声明会提供的键全部提供出来。

为什么需要这个条件？因为支持集合只看提供声明。如果组件声明会提供某个键，但实际活跃后没有提供，消费者可能在支持集合里看似被支持，运行时却无法真正激活。

因此，完整提供把“声明上可能提供”收紧成“成功后一定提供”。它是后面静止支持和汇合结论的关键前提。

引理70：静止时的支持

这条引理说明，如果系统到达静止状态，没有失败纤程，并且所有组件都完整提供，那么活跃纤程集合正好等于支持集合。

这很重要，因为它把运行时状态和声明式配置对齐了。静止时哪些纤程活着，不再取决于调度历史，而是由父子关系、依赖声明和提供声明决定。

没有“无失败”这个前提，结论会不成立：失败纤程可能已经静止，但它并没有成为活跃纤程。没有“完整提供”这个前提，支持集合也可能包含声明上被支持、实际却因提供者未安装某个键而无法活跃的纤程。

引理71：步骤交换

这条引理说明，在步骤独立和注册表良构条件下，两个作用于不同纤程的相邻步骤，在一定条件下可以交换顺序，而且最终状态相同。

它是汇合证明的基本换位工具。只要两个步骤没有同一个控制目标，也不涉及会改变对方可执行性的生命周期关系，就可以把它们换个顺序。

由于独立效应的状态动作可交换，且控制字段写在不同纤程上，交换不会改变结果。迭代器独立还保证，交换后返回的撤销函数和后续步骤不会变。

它没有说任意两步都能交换。例如卸载相关步骤涉及已提交视图、被依赖守卫和恢复器，通常要借助恢复精确、结束恢复和删除片段来处理，而不是直接交换。

引理72：删除片段

这条引理说明，在满足独立、完整提供、最终静止且无失败等条件时，某个已经关闭的纤程运行片段可以从执行历史中删除；如果这个片段里注册了临时子纤程，也要把这些临时子纤程的相关步骤一起删除。

它依赖前面的结束恢复推论：关闭片段的恢复器已经撤销了该纤程自己的状态贡献。剩下的残留条目也对其他规则不可见，可以被忽略。

这条引理形式化了“加载又卸载的组件等于没来过”。它是证明动态历史不污染最终状态的关键。

删除后的最终状态与原最终状态观察等价；差异只可能出现在那些本来就应该消失或成为残留的临时纤程名字上。

定理73：汇合

这是论文最重要的全局结论之一。前提是：序列到达静止状态、没有失败纤程、步骤两两独立、每个组件都完整提供，并以支持集合为最终应保留的纤程集合。

定理有两个结论。

第一，任何这样的历史都可以规约成一种标准历史：保留同样的编排输入，然后按某个符合依赖关系的顺序，让最终被支持的纤程各自完成一次运行片段。那些加载后又卸载的临时片段可以被删除，独立相邻步骤可以交换。

第二，任意两条从同一初始状态出发、具有相同编排输入的合法序列，只要都满足前提并到达静止无失败状态，它们的最终状态在适当重命名纤程名字后观察等价。

这给动态组合提供了核心保证：系统经历过加载、卸载、重载、替换的历史并不重要；只要最后配置相同，并满足前提，静止后的状态就等价。

定理73和进展定理合在一起，可以读成：满足纪律的生命周期系统有一个唯一的稳定结果。调度可以不同，但最终等价于按最终支持集合从头静态装配。

论文也明确排除失败，因为失败是真实分歧来源。同一个步骤是否失败可能取决于当时状态，不同调度可能让一个纤程失败或成功。结束恢复只能保证失败纤程对业务状态不留下贡献，不能把失败状态本身抹掉。

最后还要注意，汇合说的是状态，不是运行过程中对外发出的所有事件。论文第 6 章会区分边界内可撤销的获取动作和越过边界的发送动作；后者不在这个汇合保证里。

实现入口

本章解释论文第 5 章。编号条目只有定义74，但第 5 章还包含大量实现映射、算法和案例说明，是把前面形式化模型落到 Cordis 的关键部分。

论文把 Cordis 定位为“时空可组合性的元框架”：它本身不规定网页、数据库、界面、聊天机器人等具体领域语义，只提供动态组合的通用运行时语义。实现分三层：

核心库：直接实现效应、余效应、上下文和生命周期。
组件加载器：在核心库之上实现声明式配置、增量协调和热模块替换。
应用框架：例如 Koishi，在 Cordis 上提供领域词汇和插件生态。

理论到实现的对应关系可以这样理解：统一上下文对应运行时的 ctx；效应迭代器对应返回或产生清理函数的回调；效应提升对应 ctx.effect(callback)；依赖存储、隔离和拦截对应上下文内部的存储表、隔离映射和拦截元数据；纤程对应组件实例；恢复器对应 fiber.dispose；已提交视图和目标视图分别对应 fiber.committed 和 fiber.target。

实现1：效应跟踪

Cordis 的核心入口是 ctx.effect(callback)。所有会修改上下文的操作都要通过它，包括提供依赖、注册组件以及其他上下文变更。回调可以是单步效应，也可以是多步迭代器；每一步产生一个清理函数，运行时把这些清理函数合成为一个总恢复器。

实现的关键点有三个：

执行器驱动迭代器，每一步把新的清理函数放进恢复器，形成后进先出的清理顺序。
守卫在每个迭代边界检查是否还应继续执行，对应“加载可在边界中断”。
清理函数最多运行一次。重复运行清理函数会让它遇到自己没有见证过的状态，理论上不再保证正确。

论文也明确说：运行时不会自动证明回调返回的清理函数真的正确。这仍然是组件作者的义务。形式化理论说明的是“如果每个清理函数正确，那么组合和恢复正确”；实现层无法自动验证任意用户代码。

实现2：余效应操作

Cordis 用三类内部槽实现余效应：实际值存储、键到隔离域的映射、键到元数据的映射。

ctx.get(key) 先经过隔离映射，再从实际存储中取值。ctx.set(key, value) 是一个 ctx.effect：正向写入存储，清理函数删除该绑定；安装和删除都会触发通知。

通知机制会遍历存活纤程，检查变化的键是否出现在该纤程的注入声明中，并且是否解析到同一个隔离域；若受影响，就重新计算目标视图。真正是否加载、卸载或保持不变，由目标视图和生命周期状态机决定。

隔离和拦截则是派生上下文操作。ctx.isolate(key, realm) 改变键解析到哪个隔离域；ctx.intercept(key, metadata) 合并访问元数据。它们不直接改共享存储，所以不需要显式清理函数，派生上下文结束时这些视角调整自然消失。

实现3：组件生命周期

ctx.use(component, config) 实例化一个组件，创建纤程。论文把它解释为注册子组件原语：父上下文运行一个被跟踪的效应，正向效果是插入子纤程并触发刷新，撤销效果是把子纤程标记为退休并触发卸载。

工程实现中的几个字段直接对应形式化概念：

fiber.target：当前目标视图的摘要，按提供者标识记录。
fiber.committed：加载开始时提交的依赖解析视图。
fiber.dispose：累积恢复器。
fiber.inertia：正在进行的异步转换句柄。

刷新流程会重新计算目标视图。如果目标变了，并且当前没有转换在进行，就启动重载或卸载。重载先记录已提交视图，再执行组件逻辑；完成后如果目标没变，就进入活跃状态并通知依赖它的纤程；如果目标已变，就链到卸载。卸载会先等待受影响的消费者完成清理，再执行 fiber.dispose，最后根据当前目标决定保持未激活还是重新加载。

这里对应了前面几个关键结论：记录已提交视图，保证清理期间仍能读旧依赖；先把提供者标记为卸载中，使它停止服务新消费者；等待消费者清理完成，落实被依赖守卫；重载和卸载互相链式调用，表达异步步骤的惯性。

实现4：上下文访问

Cordis 还用 TypeScript Proxy 提供 ctx[key] 式访问。它和裸 ctx.get(key) 不同：普通读取只是查存储；代理访问会沿纤程链查找当前纤程的已提交视图，确认这个键是组件声明并已经提交的依赖。

如果访问未声明键，会报未声明访问错误；如果声明了但当前纤程尚未加载提交，会报未激活访问错误。这把依赖声明从“只在加载前检查”推进到“访问点也检查”，形成一种运行时能力约束。

定义74：配置条目

配置条目是组件加载器中的声明式单位。一个配置条目声明一个纤程，记录稳定标识、组件模块地址、隔离设置、拦截设置、组件配置以及是否禁用。

稳定标识用于协调子列表变化，组件地址决定实例化哪个组件，隔离和拦截决定上下文视角，配置数据绑定到组件的效应函数，禁用状态对应纤程是否应退休。

论文用它把前面的形式化生命周期落到工程配置层。配置树成为系统应该加载什么的权威记录；加载器根据配置条目字段变化增量地插入、退休、重载纤程，并依靠前面的进展和汇合定理保证最终状态等价于从最终配置重新装配。

配置条目能作为忠实规格，是因为最终应保留哪些纤程只依赖退休标记、父子关系、依赖声明和提供声明。运行时状态、恢复器、已提交视图等不属于“最终应该存在什么”的声明性输入。

实现5：声明式协调和隔离迁移

当配置条目字段变化时，加载器不总是整棵树重建，而是按字段做最小扰动：

稳定标识或模块地址变化：重建该条目。
隔离设置变化：重分配隔离域。
拦截设置变化：原地更新，因为拦截元数据在读取时生效，不改变依赖满足性。
配置变化：交给组件自己比较，必要时才重载。
禁用状态变化：设置或取消退休。

隔离迁移比普通隔离更复杂，因为配置条目可能在配置树中移动。论文引入分隔标签判断某个绑定是否属于当前条目自己的隔离作用域：如果提供者和条目的标签一致，说明这个绑定应随条目迁移到新隔离域；如果不一致，就只是外部共享绑定，不应被搬走。

实现6：热模块替换

热模块替换把“可撤销效应”模式提升到模块级。因为一个组件的所有上下文效应都被纤程包住，所以替换模块时可以清理旧纤程，再从新模块实例化新纤程，而不需要像传统前端热替换那样让开发者手写接受边界。

论文的热替换分三步：

模块分类：从变化模块和不能热替换的外部模块出发，计算哪些模块可以接受替换，哪些必须拒绝。
过期配置条目检测：找出依赖树触达可替换模块的配置条目。
事务化重载：先备份并清理模块缓存，再重新导入过期条目；若导入失败，则恢复缓存，并用旧模块重建纤程。

这保证系统不会停在半重载状态。失败时可以回滚到旧模块对应的纤程，成功时旧纤程的效应被撤销，新纤程的效应重新安装。

实现7：Koishi 案例

论文用 Koishi 作为生产案例。Koishi 是基于 Cordis 的聊天机器人框架，拥有大量社区插件，覆盖即时通讯适配器、数据库驱动、管理控制台和用户功能。论文强调两个观察。

第一，Cordis 作为元框架足够通用。Koishi 服务端插件组合的是聊天机器人运行时资源；Koishi Web 控制台也是一个独立 Cordis 应用，组合的是浏览器和 UI 资源。这说明上下文范式不绑定某个领域。

第二，时空可组合性降低插件作者负担。插件通过上下文执行效应，清理顺序由 Cordis 自动组合；插件声明注入依赖，依赖出现、消失、替换时，运行时只重载受影响的消费者。不同作者写的插件只需要在依赖键上达成接口约定，不必互相知道生命周期细节。

论文也很谨慎：Koishi 案例只能说明“这个模型在一个真实生态中可实现、可采用”，不是严格的对照实验。它没有量化性能开销，也没有证明开发效率相对其他架构更高。

贯穿理解

六层主线

这 74 个编号条目可以按六层理解。

第一层是可撤销效应：每个环境修改都返回撤销动作，系统把撤销动作按正确顺序累积。这一层回答“组件做过的事怎样收回来”。

第二层是响应式依赖：组件声明自己需要哪些键，依赖表变化时系统判断组件应激活、失活还是不受影响。这一层回答“组件和组件之间怎样连接”。

第三层是统一上下文：效应恢复器和依赖表被放进同一个上下文，组件所有环境交互都通过它发生。这一层回答“修改环境”和“依赖环境”为什么可以放进同一个范式。

第四层是生命周期演算：组件实例化为纤程，纤程通过目标视图、已提交视图和规则在未激活、加载中、活跃、卸载中之间转换。这一层回答“依赖变化怎样变成加载和卸载动作”。

第五层是全局性质：在独立性、无环依赖、完整提供等前提下，组件可以交错运行和卸载，系统最终仍会收敛到由最终配置决定的状态。这一层回答“动态历史会不会污染最终结果”。

第六层是工程实现：Cordis 用 ctx.effect、ctx.set/get、ctx.use、fiber.dispose、fiber.committed、fiber.target、配置条目和热模块替换，把论文的形式化结构落到运行时框架。

不能误读的前提

这篇论文最容易误读的地方，是把有条件定理读成无条件承诺。它的保证依赖几个纪律：

每个效应提供的撤销函数必须真的能撤销本次效应。
跨组件共享状态应通过依赖键暴露，否则不在理论边界内。
需要任意顺序卸载或交错执行时，相关效应或键操作必须独立。
依赖优先关系要无环，否则组件可能永久无法激活。
组件若声明提供某些键，成功活跃后应完整提供这些键，否则汇合定理的支持集合会失准。
失败是被显式排除在汇合结论之外的真实分歧来源。

这些前提并不是论文的缺陷，反而是它的价值所在。它没有把复杂系统说成“天然可靠”，而是明确列出哪些约束足以换来可恢复、可协调、可收敛的动态组合。

讨论边界

第 6 章讨论部分说明，论文的理论边界同样重要。

系统边界

系统边界决定什么能恢复。打开文件、分配内存、注册服务这类获取动作可以在边界内被记录并撤销；已经写到外部文件、发到网络、收款成功这类发送动作通常越过边界，不能靠撤销函数消失，只能延迟提交或做补偿动作。

这一区分很关键。论文并不是承诺“所有外部世界的变化都能撤销”。它承诺的是：只要某个位置被系统纳入上下文，并且访问它的操作能提供撤销语义，它就可以进入恢复理论。越过边界的输出，只能靠业务层设计来处理，例如等状态确定后再提交，或用退款、删除、反向事件等补偿动作达到应用认可的等价状态。

服务复用和滚动替换

论文讨论了服务多路复用：同一个服务键可以有多个实现。它可以表现为互斥绑定，也可以表现为聚合绑定。前者像“当前使用哪个数据库驱动”，后者像“有多个消息适配器同时提供能力”。

互斥绑定的优点是简单：消费者看到的就是某一个具体提供者。缺点是切换提供者会扰动所有消费者，因为它们的目标视图会从旧提供者变成新提供者，于是触发卸载和重载。数据库驱动、模型供应商、默认存储后端这类“同一时刻只选一个”的服务，通常适合这种模式。

服务代理则把一个稳定的中间服务放在前面。消费者依赖代理，多个后端提供者依赖或注册到代理。这样后端变化时，消费者看到的依赖键和提供者身份不变，不一定需要重载。代理内部可以做负载均衡、故障切换、滚动更新，也可以把本地调用扩展成跨进程调用。

这个设计解释了论文为什么不把“多个提供者”简单当作冲突。对于某些键，多个提供者确实意味着歧义；对于另一些键，应该引入一个代理，把多提供者问题变成代理内部的调度问题。前者强调依赖解析的一致性，后者强调减少消费者生命周期扰动。

服务替换时，关键不是立刻拔掉旧提供者，而是先停止让新消费者绑定到旧提供者，再等待已经绑定的旧消费者完成卸载。这和前面的被依赖守卫一致。它使滚动更新成为可能：新提供者先上线，新消费者逐步转过去，旧消费者清完后旧提供者再撤销自己的效应。

访问控制和沙箱

访问控制可以由依赖声明和拦截机制支撑：组件只能访问声明过的依赖，外层上下文可以通过元数据限制路径、权限或标签。

但这不是完整安全沙箱。不可信代码仍需要语言外机制，例如独立进程、容器或 WebAssembly 边界。论文的上下文模型能让“组件应该访问什么”变得可声明、可检查、可拦截，但它不能单独阻止恶意代码绕开宿主语言的普通能力。

语言和操作系统协同

语言实现这套范式，需要能捕获撤销函数的闭包或等价机制，需要能动态加载和卸载模块，还需要依赖声明、类型扩展和访问拦截能力。TypeScript 可以用 Proxy 和模块扩展实现；其他语言可能用类型类、特征、装饰器、宏、描述符或反射实现。

论文第 6.4 更具体地把语言要求拆成两个方向。

时间方向至少需要两种能力。第一，语言要能把撤销动作保存成值，因为组件卸载时要在未来某个时刻执行它。第二，语言或运行时要能把组件代码引入进来，也能在不再引用时撤掉它。托管运行时通常依赖模块缓存和垃圾回收，原生代码则更接近动态链接和卸载，WebAssembly 要看宿主环境怎样管理模块实例。

空间方向至少需要表达依赖声明和上下文访问边界。组件要能说清楚自己需要哪些依赖，运行时要能在访问点检查“这个组件有没有声明过这个键”。如果语言支持类型扩展或结构化接口检查，还可以把一部分依赖兼容问题提前到类型层；如果只靠普通对象和字符串键，运行时就要承担更多检查责任。

论文也设想了更深的协同。如果语言原生支持上下文，开发者不必把上下文作为普通参数传来传去，编译器也能更早发现依赖环或未声明访问。如果操作系统把文件描述符、内存区域、权限能力等资源作为依赖提供出来，它就能在更细粒度上帮助组件恢复，而不只是回收整个进程。

依赖环和接口兼容

互相依赖在这个模型中不会自动解决，而是会让组件无法激活。论文建议通过更细粒度组件拆分，把双向交互拆成核心组件和单向集成组件。这样理论上保持无环，但会增加配置和命名负担。

依赖版本和接口兼容也是开放问题。形式模型按依赖键身份连接提供者和消费者，但真实生态会遇到两类故障：接口漂移和键冲突。

接口漂移是指提供者仍然使用同一个依赖键，但新版本改变了方法签名、字段结构或行为约定。消费者看起来依赖满足了，真正调用时却可能报错或产生沉默的行为差异。键冲突则更糟：两个独立作者碰巧用了同一个键名，却表示完全不同的接口，运行时会把错误的提供者交给消费者。

论文讨论了三种缓解方向。键命名空间可以减少冲突，让键带上包名、组织名或生态域。版本化或同伴依赖可以让消费者声明自己兼容哪个提供者版本。结构兼容则不只看键名，而是比较接口结构是否满足消费者需要。三者都很实用，但都会把模型从“键身份连接”推进到更复杂的生态治理和类型兼容问题，所以论文没有把它们纳入核心定理。

思想实验：一个智能体运行时的组件演化

下面构造一个简化的智能体运行时，用一个完整生命周期串起前面概念。它不是论文中的案例，而是帮助理解论文概念怎样落到实际系统。

设想一个长期运行的智能体宿主，里面有这些组件：

ModelProvider：提供大模型调用能力。
MemoryStore：提供会话记忆和向量检索能力。
ToolRegistry：提供工具注册表。
PlannerAgent：依赖模型、记忆和工具注册表，负责规划任务。
FileTool：依赖权限服务，向工具注册表注册文件读写工具。
BrowserTool：依赖权限服务，向工具注册表注册网页访问工具。
PolicyGuard：提供权限服务，并通过拦截元数据限制不同工具能访问的路径、域名或操作类型。

初始装配

系统启动时，根配置插入 ModelProvider、MemoryStore、ToolRegistry 和 PolicyGuard 四个提供者纤程。它们没有复杂依赖，目标视图很快变为非空，于是进入加载中。

ToolRegistry 加载时创建一张工具表，并把“工具注册表”这个依赖键写入自己的依赖表。这个写入是一个可撤销效应：正向动作是提供注册表，撤销动作是删除这个提供。

PolicyGuard 加载时提供权限服务。它的拦截机制可以让不同工具拿到不同权限视角。例如 FileTool 只能访问工作区目录，BrowserTool 只能访问允许的域名集合。

当这些提供者活跃后，FileTool 和 BrowserTool 的依赖声明被满足。它们开始加载：读取权限服务，读取工具注册表，向注册表注册自己的工具入口。每次注册都返回清理函数，卸载时可以注销对应工具。

最后，PlannerAgent 的依赖也满足。它读取模型、记忆和工具注册表，注册自己的任务循环和事件监听。此时系统静止：所有应该运行的纤程都活跃，已提交视图等于目标视图。

这一阶段对应论文的空间方向：谁依赖谁，不是散落在代码里的临时读取，而是由依赖声明和目标视图决定。也对应时间方向：每个组件加载时对上下文做的修改，都已经进入恢复器。

分叉一：替换记忆组件

现在智能体决定把 MemoryStore 从本地向量库切换到远程记忆服务。配置层插入新的 RemoteMemoryStore，并退休旧的 MemoryStore。

旧记忆组件一旦退休，它的目标视图变为空。但它不能立刻真正撤销，因为 PlannerAgent 的已提交视图仍然指向它。生命周期规则会先让旧记忆组件进入卸载中，停止服务新消费者；同时，PlannerAgent 的目标视图发现记忆提供者变了，于是进入卸载中。

PlannerAgent 卸载时仍然可以通过已提交视图读取旧记忆服务，完成自己的清理。例如它可能需要把未完成任务状态写回旧记忆，注销旧监听器，取消旧检索会话。等它卸载完成，旧记忆组件不再被依赖，才真正执行自己的恢复器，撤销连接、注销提供、释放本地资源。

随后 PlannerAgent 的目标视图指向新记忆组件，重新加载。最终系统再次静止。这条分叉演示了已提交视图和被依赖守卫：提供者不会在消费者清理完成前撤回旧依赖。

分叉二：工具热替换成功

开发者修改了 BrowserTool，加入新的截图能力。热模块替换发现这个配置条目受影响，于是准备替换该工具纤程。

旧 BrowserTool 先卸载：它从工具注册表注销旧工具入口，撤销事件监听，释放浏览器会话。由于这些动作都通过上下文效应注册，恢复器按后进先出顺序执行。

新模块导入成功后，系统实例化新的 BrowserTool。它读取同一个权限服务和工具注册表，注册新工具入口。PlannerAgent 依赖的是工具注册表这个键，而不是某个具体工具模块；如果注册表的可观察接口设计得足够可交换，工具条目的增删不会破坏其他工具条目，规划器可以只看到工具集合变化，而不需要整个系统重启。

这条分叉演示了可撤销效应、可交换键和热模块替换：替换不是把进程推倒重来，而是撤销旧组件贡献，再安装新组件贡献。

分叉三：工具热替换失败

如果新 BrowserTool 模块导入失败，生命周期会走另一条路径。

系统先备份旧模块和旧配置状态，再尝试导入新模块。失败发生后，不能停在“旧工具已撤、新工具未装”的半状态。加载器恢复模块缓存，用旧模块重新实例化 BrowserTool。

这时旧纤程的效应已经撤销，新纤程重新安装旧版本效应。对其他组件来说，最终系统回到一个可用状态。失败本身会被记录，但它不会让已经撤销的半成品效应留在注册表里。

这条分叉演示了论文对失败的态度：失败是真实分歧，不能被汇合定理抹掉；但已经完成的上下文效应必须通过恢复器清掉，避免系统停在半安装状态。

分叉四：自进化代理添加新组件

运行一段时间后，智能体根据任务需求生成一个 CodeSearchTool，用于搜索代码库。它把新工具作为子组件注册到当前配置树中。

注册子组件本身也是父纤程的可撤销效应。正向动作是插入 CodeSearchTool 纤程，撤销动作不是直接删除，而是退休它。这样即使新工具已经加载、甚至又注册了自己的子组件，父组件卸载时也只需要发出退休请求，后续卸载会沿生命周期规则级联完成。

CodeSearchTool 依赖权限服务和工具注册表。权限服务通过拦截元数据限制它只能读工作区源码目录，不能访问用户主目录。工具加载后向工具注册表注册搜索入口，返回注销函数。

如果这个工具后来被智能体判定无用，配置层退休它。工具先进入卸载中，注销搜索入口，释放索引句柄，最后变成未激活。若它留下一个已退休、未激活、无子组件、无提供的残留条目，引理57说明这个条目基本可视为不存在，后续可安全移除。

这条分叉演示了注册子组件、限制作用域、拦截和残留条目。

分叉五：外部输出越过边界

假设 PlannerAgent 调用 BrowserTool 抓取网页，然后向用户发送一条总结消息。抓取会话、工具注册、临时缓存都在系统边界内，可以通过恢复器撤销。

但已经发给用户的消息越过了系统边界。即使随后组件卸载，恢复器也不能让用户“没看见”那条消息。系统能做的只是设计补偿：例如再发送一条更正消息，或在发送前等任务状态稳定后再提交。

这条分叉演示了第 6 章的系统边界：可撤销效应不是时间机器。它能恢复系统掌控内的上下文状态，不能自动抹掉外部世界已经接收的输出。

这个思想实验对应的整体图景

在这个智能体运行时里，时间可组合性保证每个组件卸载时可以撤销自己通过上下文安装的贡献；空间可组合性保证依赖提供者变化时，只有真正受影响的消费者重载；生命周期演算保证加载中、卸载中、失败和异步落地都有明确路径；全局性质则说明，在独立性、无环依赖和完整提供等前提下，不同演化历史最终会收敛到由最终配置决定的状态。

如果只用一句话概括这篇论文：它把动态插件系统里最难控制的两类问题，也就是“做过的事怎么撤销”和“依赖变化怎么传播”，都收束到上下文里；再通过恢复器、观察等价、独立性、目标视图、已提交视图、进展和汇合，证明满足约束的动态系统最终可以像静态装配一样被理解。

标签： 人工智障

作者： 宁嘉 | 参小智

日期：2026年08月15日