A chain of thought is an effect iterator

Spatiotemporal Composability (arXiv:2608.25512) formalizes dynamic composition for plugin systems. Its central type is not a metaphor for a reasoning chain — it is the same type.

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

Each iteration yields the new context, the inverse of that step, and whether another follows. The paper calls it "a reified delimited continuation, the structure that mainstream languages expose through the yield operator". A chain of thought is a generator; this is a generator that carries its own undo.

Three things that transfer exactly

Backjumping gets a soundness guarantee. conflict-learning-and-backjumping takes CDCL's two pillars as the model for an agent tracing back out of a dead end. Theorem 16 supplies what CDCL assumes: reverting in reverse order hands each inverse the state its own application ran against, and every intermediate state satisfies the soundness invariant. So a jump to an intermediate node is not "roughly where we were" — it is that state, provably, and the search may resume from it rather than replaying from the root.

The system boundary says which steps may be speculated on. §6.1: a location is inside when the system can modify it exclusively and restore what was there; outside when either fails, and an operation on it "acts as id_Γ and is therefore neither tracked nor reverted". That is a checkable rule for the question that makes tree search over tool use dangerous: a step touching only inside-state may be tried and discarded freely; a step that sent an email may not. Today agents answer this with a hand-written allowlist. Here it falls out of whether the effect has an inverse.

Preconditions replace the pipeline. A step declares the coeffects it needs and waits, inactive and not erroring, until they exist (Thm 70). Nobody writes the order. This is gates-are-necessary-conditions with the gate turned inside-out: instead of a graph whose edges encode which stage may follow which, each stage names what it requires and the chain assembles itself.

Task decomposition is a typing derivation

Push it down one level and the whole task tree types. A goal is a key; a step that achieves it provides that key; what the step needs first is its coeffect specification. The task is complete when σ ⊨ {goal}. Sub-steps decompose the same way, all the way down.

The same declarations run in both directions. Forward, notify_d classifies each change as activating or deactivating, so a step fires when its premises land. Backward, to obtain goal you find who provides it and recurse into their requires — goal-directed proof search over exactly the relation that drives forward execution. The declarations are not a plan; they are a relation, and a plan is one traversal of it. That is where "precise and flexible at once" comes from: every step's premises and product are explicit, and nobody writes the order.

Three consequences worth holding together:

A circular decomposition is statically detectable. §6.5: "a dependency cycle simply leaves the involved components permanently inactive… Unlike deadlock in concurrent systems, which depends on the schedule and must be detected as it happens, this condition is predictable from the dependency declarations alone." An agent that decomposes a task into a cycle can be told so at load, not after it spins.

A bare key is a claim, not a proof. k ∈ dom(σ) says someone bound the key, not that what they bound meets the consumer's expectation — §6.6's nominal linking, which on an agent is exactly "the subagent said it was done". This lens therefore needs the LCF one: certificate-is-the-subagent-boundary and promise ≠ proof supply the warrant for each key. Spatiotemporal composability gives the structure; LCF gives the evidence. Without the second, the derivation tree is built on self-report.

The recursion terminates where a coeffect becomes a script. The open question this raises — can an agent decompose a task's typing far enough that a script can accept each piece — is already answered by the semantics rather than bolted onto them. §3.3.2 defines equivalence by tests (Def 31): a test is a finite word of operations with observable outcomes, and σ ≃_S σ' means no test in S distinguishes them. That is a script with an exit code. So a step whose coeffect cannot be written as a test is not an under-specified type — under the paper's own semantics it denotes nothing, because there is no state it is true of.

Which gives the stopping rule: split until every leaf's coeffect is a test. That is exactly when the recursion is well founded (pc-well-founded-recursion), and it relocates the whole intelligence budget into choosing the decomposition, since verification is then $?. The agent does not have to be right; it has to keep splitting until being right is checkable.

Alternative plans are isolation realms, and abandoning one is free. A key admits one provider (k ∉ dom(σ)), so two strategies for one subgoal cannot be two competing bindings — each explores in its own realm (Σ^iso). And isolation is a derived realization (Def 23): it writes nothing to the shared table, "with the identity as its inverse; recovery discards the derived context". So exploring three decompositions in parallel and dropping two costs no reverting at all — the dropped branches never entered the table anyone else reads.

What it adds to the Petri-net lens

tokens-petri-nets-capabilities already reaches half of this, and reaches it correctly: a transition fires when its input places are marked, which is exactly σ ⊨ d. Token minting living with the verifier is exactly set's precondition k ∉ dom(σ) — a violation "is signalled as an error and produces no transition", so unforgeability is constructive rather than a discipline.

What Petri nets do not have is the inverse. Undoing a transition means authoring the reverse transition by hand, and returning to the original marking is not guaranteed. The accumulator φ supplies it structurally. So: Petri nets + inverse = this paper, and the thing vibe-linter currently has no answer for — after a check fails, which state does it return to? — is precisely the half that was missing.

Why it beats the state-machine framing

A state machine over N gates has up to 2^N states, and adding a gate redraws every edge that touches it. The coeffect formulation has N declarations and computes the state. But the real defect of the FSM lens is over-specification of order. §3.4 closing:

"What the decomposition divides is a computation's commuting part from its order-sensitive part. The commuting part is carried by the effects — a component performs them in whatever order its task calls for, and Theorem 43 reverts them in whatever order the system finds convenient, no two components constraining each other. The order-sensitive part is carried by the coeffects, since a key whose operations do not commute is one whose order has to be imposed from outside."

A state machine's edges are an order, so it commits to one everywhere. This language makes you declare order only where the key genuinely fails to commute (Def 44: a table where each registration takes an entry of its own commutes; a single slot does not). Everything else is free to interleave. That is an eighth lens for vibe-linter, and it explains why the token/Petri-net and ramadge-wonham-supervisory-control lenses — both of the state-machine genus — felt like they were saying more than they meant.

The shape already exists in offices

An OA approval workflow is this system, built by people who were not thinking in these terms.

And the classic OA bugs are the paper's named failures: a recall that voids the approval but never releases the budget hold is an effect without its inverse; a workflow stuck because an approver left is a coeffect whose provider vanished, erroring instead of waiting; needing a redeploy to change a flow is no hot replacement. van der Aalst's workflow nets are the received theory here, which is the same Petri-net lens — and the same missing half.

Where it does not fit

LLM steps are not deterministic, so Confluence (§4.3.5) fails. The honest cut: which step the model chooses is stochastic; what effects that step performs need not be. The theory governs the effects, not the sampling.

The inverse of "the model concluded X" is not clean — deleting the token does not restore the conditioning. This is survivable only because of §3.3.2: equalities are read up to observational equivalence, and "the part of a state that no key binds is forgotten". Bind conclusions at keys and reverting the key suffices; leave them implicit in the transcript and nothing is recoverable. That is a design constraint on the harness, not a property it gets for free.

Up: vibe-linter · recursive-harness Near: 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