一条思维链就是一个 effect iterator

Spatiotemporal Composability（arXiv:2608.25512）为插件系统的动态组合做了形式化。它的核心类型 不是思维链的比喻 —— 它就是同一个类型。

𝔍_Γ := μ𝔍. Γ → Γ × (Γ → Γ) × Maybe(𝔍)

每次迭代吐出新状态、这一步自己的逆、以及还有没有下一步。论文称它是"一个被具体化的 delimited continuation，也就是主流语言用 yield 暴露的那个结构"。思维链就是一个 generator；而这是一个 自带 undo 的 generator。

三处精确转移

回跳拿到了可靠性保证。 conflict-learning-and-backjumping 拿 CDCL 的两根支柱做 agent 走进 死胡同后往回退的模型。Theorem 16 补上了 CDCL 默认成立的那一条：反序回退时，每一个逆拿到的正是 它自己那次施加所面对的状态，而且每一个中间状态都满足 soundness invariant。所以跳回一个中间 节点不是"大概回到那儿"，而是可证明地就是那个状态，搜索可以从那里继续，不必从根重放。

system boundary 说清了哪些步骤可以投机。 §6.1：一个位置在系统内，当系统能独占地修改它 并且能恢复原状；在外，当两者有一个做不到，此时操作表现为 id_Γ，既不被追踪也不被回退。 这就给了"对工具调用做树搜索为什么危险"一个可检查的判据：只碰内部状态的步骤可以随便试、随便丢； 已经发出邮件的那一步不行。今天的 agent 靠手写白名单回答这件事，这里它从"这个 effect 有没有逆"里 直接掉出来。

前置条件取代流水线。 一步声明它需要的 coeffect，拿不到就待命且不报错，直到它出现（Thm 70）。 没有人写顺序。这是把 gates-are-necessary-conditions 的 gate 翻了个面：不再是一张用边编码 "哪个阶段能接哪个阶段"的图，而是每个阶段声明自己要什么，链自己装配。

任务分解就是一次类型推导

往下压一层，整棵任务树就类型化了。一个目标是一个 key；达成它的那一步 provides 那个 key；这一步 先要什么，就是它的 coeffect 规格。任务完成于 σ ⊨ {goal}。子步骤照同样的方式往下分，一路到底。

同一批声明在两个方向上都跑。 正向，notify_d 把每次改动分类为激活或去激活，于是一步在它的 前提落地时激发。反向，要得到 goal，你去找谁提供它、递归进它的 requires —— 目标导向的证明搜索， 走的正是驱动正向执行的那同一个关系。这些声明不是一份计划，是一个关系，而计划只是对它的一次 遍历。"既精确又灵活"就是从这来的：每一步的前提和产物都是显式的，而没有人写顺序。

三个值得一起拿住的推论：

循环分解是静态可检的。 §6.5："一个依赖环只是让牵涉其中的组件永久处于非激活态……与并发系统 里的死锁不同——死锁取决于调度、必须在发生时才检出——这个条件单凭依赖声明就能预测。" 一个把任务分解成环的 agent，可以在加载时就被告知，而不是空转之后才发现。

一个裸 key 是主张，不是证明。 k ∈ dom(σ) 说的是有人绑了这个 key，不是他绑的东西满足消费者的 期望 —— 这是 §6.6 的 nominal linking，落在 agent 上正是"子 agent 说它做完了"。所以这个透镜需要 LCF 那个：certificate-is-the-subagent-boundary 与 promise ≠ proof 为每个 key 提供凭据。 时空可组合性给出结构；LCF 给出证据。 没有第二样，整棵推导树就搭在自述之上。

递归在一个 coeffect 变成脚本的地方终止。 它引出的那个开问题 —— agent 能不能把一个任务的类型 分解得足够细，细到一个脚本能接住每一块 —— 已经由语义本身回答了，不是外接上去的。§3.3.2 用测试 定义等价（Def 31）：一个测试是一串有可观察结果的有限操作词，σ ≃_S σ' 意思是 S 里没有任何测试 能区分它们。那就是一个带退出码的脚本。所以一个 coeffect 写不成测试的步骤，不是一个欠指定的类型 —— 在这篇论文自己的语义下它什么都不指称，因为没有任何状态它为真。

于是有了停止规则：一直拆，拆到每个叶子的 coeffect 都是一个测试。 那正好是递归良基的时候 （pc-well-founded-recursion），而且它把整份智力预算挪到选择怎么分解上，因为验证这时就是 $?。agent 不必是对的；它只要一直拆，拆到"对不对"可检为止。

候选计划各是一个隔离 realm，丢弃一个是免费的。 一个 key 只容一个提供者（k ∉ dom(σ)），所以 一个子目标的两种策略不可能是两个互相竞争的绑定 —— 每一个在自己的 realm（Σ^iso）里探索。而隔离是 一种派生实现（Def 23）：它什么都不写进共享表，"以恒等为其逆；恢复时把派生出的上下文丢掉"。 所以并行探索三种分解、丢掉两种，完全不需要回退 —— 被丢掉的分支从没进过任何别人读的表。

它给 Petri 网那个透镜补了什么

tokens-petri-nets-capabilities 已经摸到了一半，而且摸对了：变迁在输入库所被标记时激发，这正是 σ ⊨ d。"铸造权归 verifier"正是 set 的前置条件 k ∉ dom(σ) —— 违反它"被报为错误，且不产生 转移"，所以不可伪造是构造性的，不是靠纪律。

Petri 网没有的是逆。 撤销一次变迁要手写反向变迁，而且回到原 marking 并不保证。accumulator φ 结构性地把它补上。所以：Petri 网 + 逆 = 这篇论文，而 vibe-linter 现在答不上来的那个问题 ——一次检查失败之后，它退回到哪个状态？—— 正是缺的那一半。

为什么它比状态机那个框架好

N 个 gate 的状态机最多 2^N 个状态，加一个 gate 就要重画所有碰到它的边；coeffect 这边是 N 条声明， 状态是算出来的。但 FSM 透镜真正的毛病是过度指定顺序。§3.4 结尾：

"这个分解切开的，是一次计算中可交换的部分和对顺序敏感的部分。可交换的部分由 effect 承载 —— 组件按任务需要的任何顺序执行它们，而 Theorem 43 允许系统按任何方便的顺序回退它们， 两个组件互不约束。对顺序敏感的部分由 coeffect 承载，因为一个操作不可交换的 key，它的顺序 必须从 effect 之外强加。"

状态机的边本身就是顺序，所以它处处承诺顺序。这套语言只让你在 key 真的不可交换的地方声明顺序 （Def 44：每次注册各占一个条目的表可交换；单槽不可交换）。其余全部自由交错。这是 vibe-linter 的第八个透镜，而且解释了为什么 token/Petri 网 和 ramadge-wonham-supervisory-control 这两个 ——都属状态机一族——总让人觉得它们说的比想说的多。

这个形状早就在办公室里了

OA 审批流就是这套系统，只是搭它的人没这么想过。

而 OA 的经典 bug 正是论文点名的那几种失败：撤回了、审批作废了、预算冻结没解 —— 这是 有 effect 没有逆；审批人离职流程卡死 —— 这是 coeffect 的提供者消失了，系统选择报错而不是 等待；改流程要停机重发 —— 没有热替换。这一行的成熟理论是 van der Aalst 的 workflow net， 也就是同一个 Petri 网透镜 —— 也缺同一半。

不合身的地方

LLM 的步骤不确定，所以 Confluence（§4.3.5）不成立。 老实的切法：模型选哪一步是随机的， 那一步施加了什么 effect 不必是。理论管 effect，不管采样。

"模型得出了结论 X"的逆不干净 —— 删掉 token 并不能恢复条件分布。这件事能活下来只因为 §3.3.2： 等式读到观察等价为止，而且"没有任何 key 绑定的那部分状态就此被遗忘"。把结论绑在 key 上，撤销 那个 key 就够了；让它们隐在 transcript 里，就什么都收不回来。这是对 harness 的一条设计约束， 不是白送的性质。

上级：vibe-linter · recursive-harness 邻近：tokens-petri-nets-capabilities · conflict-learning-and-backjumping · dynamics-to-a-fixed-point · convergence-needs-an-observable-target · cordis-fiber · everything-is-a-plugin · seam-three-roles