Agent Algebra
A 5-part series and a reference implementation give agents one algebra: sequencing, choice, parallel composition, recursion, supervision, checkpointing and human approval, each a well-defined operator with laws proved in the papers and checked against a deterministic code layer.
5 parts · 37 laws and counterexamples checked in code
Agent systems are assembled from a small vocabulary of loops, handoffs, retries, supervisors, approval steps and policies, and each item in that vocabulary has a mature theory in a different field. The five Parts of this series give all of them one mathematical object and prove, for each construc...
An agent, in the sense used by actor systems, workflow engines, control loops and language-model tool loops, is usually specified by a diagram and a runtime rather than by a mathematical object. This Part fixes the object. An agent is a coalgebra of the functor F(S) = (Y + E + 1) times (T(Sigma t...
We give an equational account of how agents compose. Fixing the agent object of Part I, an effectful Mealy coalgebra with typed termination and with failure as a terminal outcome, we define the composition signature: sequential composition with its unit and its diverging zero, immediate failure,...
Agents that interact do so through wires: feedback loops, message queues, shared stores, and the approval channel that connects a system to a person. This Part fixes the wiring layer of an algebra of agents whose object and operators are settled in Parts I and II. A single feedback operator with...
Agent runtimes crash, retry, checkpoint and replay, and their behaviour is usually described by an implementation rather than by an algebra. This Part supplies the execution layer for the agent algebra of the preceding Parts. An execution model is a class of scheduler agents together with a fail-...
Artificial intelligence and control present decision making in separate formalisms: Markov decision processes for reinforcement learning, AND/OR transition systems for planning under nondeterminism, belief states for partial observability, safety games for shields, and difference equations for fe...
Every operator in the running example is introduced by exactly one Part and composes with every operator introduced elsewhere.
Each row cites the paper's claim, the Part that proves it, the kind of check, and the test that runs it.
| Law | Part | Check | Test |
|---|---|---|---|
| thm:agent-object:quotient (decidability half) | Part I | finite-model check | partition refinement agrees with brute-force bisimulation on random Id, P and D agents |
| thm:agent-object:bisim-implies-trace | Part I | finite-model check | bisimilar random pairs are finite-trace equivalent |
| thm:agent-object:greatest-invariant | Part I | exhaustive bounded check | the gfp iteration returns an invariant containing every enumerated invariant inside Phi |
| thm:agent-object:quotient (minimality half) | Part I | finite-model check | A/~ is bisimilar to A and has no two bisimilar states |
| prop:agent-object:closed-loop-markov | Part I | exhaustive bounded check | Run(A,E) for T = D is row-stochastic and equals the product-kernel formula |
| thm:agent-object:final-mealy-id | Part I | finite-model check | for T = Id the bisimulation and trace-equivalence decisions agree on random Mealy machines |
| prop:agent-object:refinement-preorder | Part I | finite-model check | inserting random stutter ticks gives A refines A' and A' refines A |
| thm:composition-laws:sequential-category | Part II | finite-model check | seq is associative and skip is a two-sided unit up to bisimilarity |
| thm:composition-laws:gkat-bisim | Part II | finite-model check | every GKAT axiom holds up to bisimilarity on random deterministic agents |
| thm:composition-laws:kat-accepted | Part II | exhaustive bounded check (one designed witness) | left distributivity of seq over nondeterministic choice fails up to bisimilarity on the fixed witness |
| thm:composition-laws:monoidal | Part II | finite-model check | tensor is associative, commutative and unital up to bisimilarity |
| cex:composition-laws:exchange-fails | Part II | exhaustive bounded check | the one-tick versus two-tick exchange witness gives different traces |
| thm:composition-laws:unique-solutions | Part II | finite-model check | k-fold unrolling of a guarded recursion is bisimilar to the loop-state implementation |
| prop:composition-laws:recover-laws | Part II | finite-model check | recover is associative with skip and fail units, and race is associative and commutative up to bisimilarity |
| thm:interaction-coordination:delayed-trace | Part III | finite-model check | naturality, vanishing and superposing hold up to bisimilarity on random agents |
| prop:interaction-coordination:closed-loop-is-trace | Part III | finite-model check | Run(A,E) is bisimilar to Tr((A tensor E) ; swap) on random pairs |
| thm:interaction-coordination:shuffle | Part III | finite-model check (100 random component pairs and quadruples) plus one fixed strictness witness | the bounded trace set of asyncPar equals the shuffle of the component trace sets |
| thm:interaction-coordination:actor-locality | Part III | finite-model check | actor state is a function of init and the dequeued message sequence across 1000 schedules |
| prop:interaction-coordination:blackboard-linearizable | Part III | exhaustive bounded check | the linearizability checker accepts every blackboard history and rejects a replicated-blackboard history |
| prop:interaction-coordination:tuplespace-nondeterministic | Part III | exhaustive bounded check | tuple-space competition yields at least two outcomes while a FIFO link yields exactly one |
| thm:interaction-coordination:binary-deadlock-freedom | Part III | finite-model check | random dual-typed pairs never deadlock within the tick budget and an ill-typed pair does |
| thm:interaction-coordination:gate-refinement | Part III | exhaustive bounded check | Gate with an always-ok oracle equals A modulo stutters and a rejected action never appears |
| thm:execution-semantics:replay-determinism | Part IV | finite-model check (1000 seeds) | replay of a logged stochastic run reproduces the state trajectory and outputs on 1000 seeds |
| thm:execution-semantics:kahn-determinism | Part IV | finite-model check, bounded fragment only (finite-capacity channels with `k` ≥ the tick budget | random DAG workflows give identical outputs under 100 fair schedulers |
| thm:execution-semantics:supervision-refinement | Part IV | exhaustive bounded check | supervision with Persist every tick refines the crash-free run up to stuttering after erasing crash and restart markers |
| thm:execution-semantics:effectively-once | Part IV | exhaustive bounded check | retry against an environment idempotent on the dedup key ends in the crash-free environment state |
| prop:execution-semantics:timeout | Part IV | finite-model check | timeout_t(A) halts or fails by tick t+1 for every A |
| prop:execution-semantics:persist-commutes | Part IV | finite-model check | Persist commutes with seq up to bisimilarity on small agents |
| prop:execution-semantics:series-parallel-shape | Part IV | finite-model check | the recognizer accepts every tensor/seq term DAG and rejects the N-DAG |
| prop:execution-semantics:restart-budget | Part IV | finite-model check | dead-state entry coincides with budget exhaustion under random crash sequences |
| prop:decision-control:llm-is-agent | Part V | finite-model check (100 random kernels) | the seeded mock-LLM ReAct mu-term is bisimilar to a hand-written loop |
| thm:decision-control:closed-loop-value | Part V | finite-model check (Monte Carlo, stated tolerance) | Monte-Carlo value of A ; B matches the option-level Bellman computation within tolerance |
| thm:decision-control:belief-agent | Part V | exhaustive bounded check (Bayes) | belief update equals brute-force Bayes and DP value equals Monte-Carlo closed-loop value |
| thm:decision-control:shield-adversarial | Part V | finite-model check | shielded random policies produce 0 gridworld violations while unshielded produce more than 0 |
| prop:decision-control:planning-solution-notions | Part V | exhaustive bounded check | a strong-cyclic mu-plan reaches the goal under all fair schedulers and a weak plan fails on some |
| prop:decision-control:linear-stability | src/linear.ts spectralRadius | Part V | On over 300 random real triples (the borderline band where ` | ρ − 1 |
| prop:decision-control:gate-is-shield | Part V | exhaustive bounded check | Gate with a safety-oracle human and the shielded agent have the same marker-erased, stutter-collapsed traces |