Agent Algebra

An agent is a compositional computational process.

Description

The series fixes an agent as an object (S, init, step, halt) over an interface (I, Σ) with an effect monad T drawn from Id, P, D: init maps a start value into a state, step maps a state and an input to a T-weighted output and successor state, and halt reports halted, failed or running. Operators are added on top of this object: sequential composition (;), guarded, nondeterministic and probabilistic choice (⊕), the synchronous product (⊗), the first-halt product (race), recovery from failure (▷), guarded recursion (μ), delayed feedback (Tr), channels, asynchronous interleaving (∥), actors (Act), blackboards and tuple spaces, session types, the human approval gate (Gate_H), supervision (Sup), checkpointing (Persist), deterministic replay (Replay), and workflows.

The central claim of the series, quoted verbatim from team/notation.md:

Part I fixes the object: discrete time, an effect monad T drawn from the list Id, P, D, and agents as effectful Mealy coalgebras with typed termination and failure as a terminal outcome. Parts II to IV introduce the operators under additional assumptions stated in each Part and prove, for each operator, that it is well-defined on agents, which relation it respects, and which laws hold at that relation: Part II for ;, ⊕, ⊗, ▷ and μ; Part III for Tr, channels, ∥ and Gate_H; Part IV for Sup, Persist and Replay; Part V introduces no operator and interprets policies, plans, options, shields and controllers as terms of Parts I to IV, proving properties of their closed loops. For each of sixteen fields the series gives an explicit translation of one named mechanism into a term of the algebra together with an adequacy result for that translation, which is a soundness theorem, a one-way simulation, or a proved limitation; no field is claimed to reduce to the algebra.

The laws attributed to each operator are checked by a small deterministic reference layer rather than asserted: code/agent-algebra implements one interpreter with one rule per operator and tests it against the claim ledger.

Website: agent-algebra.vercel.app

Papers

Part	Title	Category	Pages	Web	PDF
Synthesis	An Algebra of Agents	cs.MA	28	web	pdf
Part I	Agents as Effectful Mealy Coalgebras	cs.LO	25	web	pdf
Part II	Laws of Agent Composition	cs.LO	28	web	pdf
Part III	Channels, Actors, and Shared State	cs.DC	29	web	pdf
Part IV	Failure, Supervision, and Durable Execution	cs.DC	28	web	pdf
Part V	Policies, Planning, and Feedback Control	cs.AI	25	web	pdf

How the Parts compose

Part I    the object: (S, init, step, halt) over (I, Σ) with T in {Id, P, D}
          equivalences ~, ≃_tr, ≃_acc, ⊑, and the closed loop Run(A, E)
            |
            v
Part II   operators on the object: ; ⊕ ⊗ race ▷ μ
          laws: which relation each operator respects, which equations hold at it
            |
            v
Part III  wiring: Tr, channels (Ch_k, link), ∥, Act, blackboards, tuple spaces,
          session types, Gate_H
            |
            v
Part IV   execution: Sup, Persist, retry, timeout, Wf, Replay
            |
            v
Part V    policies, plans, options, shields and controllers read as terms of
          Parts I to IV; no new operator, only closed-loop properties
            |
            v
Synthesis conservativity theorem (marker-free terms under lockstep, no crashes:
          Parts III and IV coincide with Part II) and the sixteen-field
          projection table (named mechanism -> term -> adequacy result)

Each Part fixes and cites the layer below it; nothing in Parts II to V changes the object of Part I, and Part V adds no operator to Parts I to IV.

What the code layer checks

The code layer is a finite model, not a proof assistant: it explores finite state spaces to a stated cap and tick budget, uses channels of finite capacity at least the tick budget, bounds recursion depth, and uses rational-weight distributions for D. Each row of code/LAWS.md is one of two kinds, or is marked proof-only:

Kind	Meaning
finite-model check	a fast-check property over generated finite terms or agents, seed 20260903, 100 runs
exhaustive bounded check	every input word, schedule, fault schedule or resolution up to a bound written in the test
proof-only	no code row; the result rests on its proof alone

Part	Claim rows	Kind
I, agent-object	7	finite-model and exhaustive bounded checks
II, composition-laws	7	finite-model and exhaustive bounded checks
III, interaction-coordination	8	finite-model and exhaustive bounded checks
IV, execution-semantics	8	finite-model and exhaustive bounded checks
V, decision-control	7	finite-model and exhaustive bounded checks
Counterexamples C1 to C4	4	exhaustive bounded checks, one designed witness each

That is 41 table rows (37 ledger claims plus 4 counterexamples), run by 62 tests in code/agent-algebra, plus 9 further results in code/LAWS.md that are marked proof-only because no finite model establishes them (for example the final-coalgebra half of the Mealy-coalgebra theorem, and the whole-equational-theory conservativity theorem of the synthesis).

The four counterexamples, one line each:

ID	Witness
C1	⊗ is symmetric in execution, but ∥ under leftBiased is not: commutativity is a property of the semantics, not of the execution model
C2	A ; (B ⊕_b C) evaluates the choice test on A's halting value; (A;B) ⊕_b (A;C) evaluates it on the start value, one tick earlier
C3	A ; (B ⊗ C) and (A;B) ⊗ (A;C) differ, so fan-out needs a channel or Tr, never a duplicated prefix
C4	(A ▷ B) ⊕ (A ▷ B) is idempotent under both relations tried, but (A ▷ B) ⊕ (A ▷ C) is not under trace equivalence: which law holds depends on the equivalence, not on the operators

Every paper's Appendix A cites, for each claim, a code ID, the file and identifier in code/agent-algebra/src, and the test as test file › describe › it, taken verbatim from code/LAWS.md. Appendix prose says "finite-model check" or "exhaustive bounded check", never "verifies": the tests are finite-model checks, not proofs, and the theorems rest on their proofs alone.

Building a paper

Each paper is a single .tex file in papers/latex. From that directory:

pdflatex <slug>.tex
pdflatex <slug>.tex

or, with latexmk installed:

latexmk -pdf <slug>.tex

Running pdflatex twice resolves cross references and the table of contents. Output PDFs are collected in papers/pdf.

Building the HTML and the site

scripts/tex2html/build.sh <slug>
cd website
npm ci
NEXT_PUBLIC_SITE_URL=https://agent-algebra.vercel.app npm run build
npm run test:mobile

build.sh runs the tex2html stages (figures, prepass, pandoc, postpass) for one paper slug and writes docs/papers/<slug>.html. The website build reads papers/series.json and the HTML in docs/papers and renders paper pages with KaTeX.

Running the tests

cd code/agent-algebra
npm ci
npm test
npm run demo

npm test runs the vitest suite (62 tests) with the fast-check seed fixed at 20260903. npm run demo prints one seeded trace per derived pattern.

Repository layout

• papers/latex: the LaTeX source of each paper, one file per slug
• papers/pdf: the compiled PDFs
• docs/papers: the HTML rendering used by the website
• images: cover images and figures
• code/: the executable reference layer (code/agent-algebra) and its law ledger (code/LAWS.md) and description (code/README.md)
• reviews/: external review rounds and audits for every paper
• team/: the interface contracts, the claim ledger (team/CLAIMS.md), the shared notation (team/notation.md), and the coordination board (team/board.md)
• posts/: platform-specific announcement drafts
• website/: the Next.js site
• scripts/: the tex2html build chain
• context/: the seed conversation, kept for provenance
• sources/: links to the primary literature

Toolchain

Tool	Version
Node.js	24.18
npm	12
TeX Live (pdflatex)	2026
pandoc	3.11
KaTeX (website)	0.18
Next.js	14.2
Playwright	1.x
ImageMagick	7
rsvg-convert	as installed
poppler (pdfinfo, pdftocairo)	as installed
Python	3.12

Author

Matthew Long The YonedaAI Collaboration, YonedaAI Research Collective Chicago, IL matthew@yonedaai.com https://yonedaai.com

Licence and provenance

Papers are licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). Code is licensed under the MIT License. See LICENSE for the full text and the exact scope of each licence.

The transcript under context/ is the author's own exported conversation (share id 6a99d54d-cf50-83e8-9f0a-be2482b369cc), kept for provenance. The prompt is the author's; the reply is model output; no authorship is claimed over the reply.