About
An agent is a compositional computational process. Fixed as an effectful Mealy coalgebra with typed termination, discrete ticks and a commutative effect monad, it composes under eight operators: sequencing (;), choice (⊕), parallel composition (⊗), guarded recursion (μ), delayed feedback (Tr), supervision (Sup), checkpointing (Persist) and human approval (Gate_H). Each operator is proved well-defined on agents, shown to respect bisimilarity or a stated coarser relation, and given the laws it satisfies at that relation. For sixteen historically separate fields, from actor systems and process calculi to durable execution and reinforcement learning, the series gives an explicit translation of one named mechanism into a term of this algebra together with an adequacy result for that translation. No field is claimed to reduce to the algebra.
The laws are not only stated in the papers: a deterministic TypeScript reference implementation checks them against generated and hand-built agent terms, and every appendix row in the papers cites the file, the identifier and the test that establishes it.
Operators, by owning Part
| Symbol | Meaning | Part |
|---|---|---|
| A : X ⇒ Y | an agent of sequential type X to Y over (I, Σ) | I |
| ~ | bisimilarity | I |
| ≃tr | finite-trace equivalence | I |
| ⊑ | stuttering-closed refinement | I |
| A ; B | sequential composition with silent handoff | II |
| A ⊕b B, A ⊕ B, A ⊕p B | guarded, nondeterministic, probabilistic choice | II |
| A ⊗ B, race(A, B) | synchronous product, first-halt product | II |
| A ▷ B | recovery: continue as B at A's failure reason | II |
| μX.F(X) | guarded recursion, with derived loop and delay | II |
| Trc(A) | delayed feedback on port c | III |
| Chk, linkc, A ∥ B | FIFO channel, linking, asynchronous interleaving | III |
| Act(A), BB, TS | actor, blackboard, tuple space | III |
| Gate_H(A) | human approval gate | III |
| Supσ, Persist_C, retry | supervisor, checkpointing, retry with backoff | IV |
| Wf(G), Replay | workflow over a Kahn network, deterministic replay | IV |
| πθ, V, A_π^Φ | parameterized policy, closed-loop value, shielded agent | V |
Background literature
- Milner, Communication and Concurrency (CCS), 1989.
- Hoare, Communicating Sequential Processes (CSP), 1985.
- Bergstra and Klop, Algebra of Communicating Processes (ACP), 1984.
- Hewitt, Bishop, Steiger, A universal modular ACTOR formalism, IJCAI 1973.
- Armstrong, Making reliable distributed systems in the presence of software errors, 2003.
- Burckhardt et al., Durable functions: semantics for stateful serverless, OOPSLA 2021.
- Rutten, Universal coalgebra: a theory of systems, TCS 249, 2000.
- Smolka, Foster, Hsu, Kappé, Kozen, Silva, Guarded Kleene algebra with tests, POPL 2020.
- Hoare, Möller, Struth, Wehrman, Concurrent Kleene algebra and its foundations, JLAP 80, 2011.
Author
Matthew Long
The YonedaAI Collaboration, YonedaAI Research Collective
Chicago, IL
matthew@yonedaai.com · yonedaai.com