Project: agent-algebra at /Users/mlong/Documents/Development/agent-algebra. Perspective: agent algebra. Date: 2026-09-03.
An agent is a compositional computational process. Central claim, quoted in every Part with a Part-specific qualification:
Part I fixes the object: discrete time, an effect monad T drawn from the list Id, P, D, Exc, and agents as effectful Mealy coalgebras with typed termination. Each later Part introduces its operators under additional assumptions stated in that Part and proves, for each operator, that it is well-defined on agents, which equivalence it respects, and which laws hold at that equivalence: Part II for ;, ⊕, ⊗ and μ; Part III for Tr, channels, ∥ and Gate_H; Part IV for Sup, Persist and Replay. For each of sixteen fields the series gives an explicit translation of one named mechanism into a term of the algebra together with a soundness or one-way simulation result for that translation; no field is claimed to reduce to the algebra.
| Part | slug | Title | arXiv | Scope |
|---|---|---|---|---|
| I | agent-object | Agents as Effectful Mealy Coalgebras | cs.LO | The agent as a coalgebra of (Y+1) × T(Σ×X)^I; bisimilarity, finite-trace equivalence, stuttering-closed refinement; invariants and greatest invariants; the (π, δ) factorization; environment co-agent; closed loop Run(A, E); quotient. No composition operators. |
| II | composition-laws | Laws of Agent Composition | cs.LO | ; skip 0, guarded, nondeterministic and probabilistic ⊕, ⊗, race, ▷, delay, guarded μ and while. Kleisli category up to ~, GKAT model, KAT modulo traces with the left-distributivity counterexample, monoidal ⊗ with the exchange-law failure, unique guarded solutions, congruence, recovery laws. |
| III | interaction-coordination | Channels, Actors, and Shared State | cs.DC | Delayed feedback Tr (delayed-trace axioms, yanking fails), FIFO channels, linking, scheduler agent, derived ∥ with shuffle traces and the CKA exchange law, actors and actor locality, blackboards (linearizable), tuple spaces (nondeterminate), session types as trace inclusion with binary deadlock freedom, Gate_H with gate refinement. |
| IV | execution-semantics | Failure, Supervision, and Durable Execution | cs.DC | Execution model γ = schedulers + fail-stop failure + fairness; retry, timeout, Sup_σ with OTP strategies and restart budgets, Persist, logs and Replay, workflows Wf(G) as Kahn networks. Replay determinism, Kahn determinism, supervision transparency (needs Persist), exactly-once under idempotent environments, series-parallel limit. |
| V | decision-control | Policies, Planning, and Feedback Control | cs.AI | Policy classes (deterministic, nondeterministic, stochastic, plan, control, LLM) instantiate (π, δ); ReAct as a μ-term; MDP value of closed loops; options as μ-terms with compositional value; belief agents for POMDPs; shields as guarded choice preserving controllable invariants (gate is a shield); weak/strong/strong-cyclic planning as trace properties; discrete linear feedback stability. |
| S | synthesis | An Algebra of Agents | cs.MA | Projection table of the sixteen fields, hierarchical composition diagram, five emergent properties, three objections answered, five open problems. |
Each paper: arXiv article, 11pt, 20 to 35 pages, Definitions, Theorems with proofs, Examples, Limitations, bibliography of verified entries. Central claim quoted verbatim in every introduction and limitations section. Shared notation in team/notation.md; ownership rulings in team/prospectus.md (lower-numbered Part owns a shared object).
code/agent-algebra: TypeScript (Node 24, vitest, fast-check with a fixed seed). One interpreter over a finite executable fragment of the term language (finite state spaces, finite-capacity channels, bounded recursion depth and tick budgets, rational-weight distributions); bisimulation by partition refinement (Id, P) and Baier, Engelen, Majster-Cederbaum (D). Tests are finite-model validation and exhaustive bounded checks, never theorem evidence: code/LAWS.md labels every row as finite-model check, exhaustive bounded check, or proof-only, and each Part's code-evidence appendix cites only the first two kinds. Theorems rest on their proofs.
multi-agent-team (contracts, board, integration gate), human-readable (humanizer grep), code-audit, bib-gate (every arXiv/DOI/URL resolved before compile), plan-critique. No Haskell, no Lean. Peer review: Gemini 3.1 Pro through the agy shim, review-fix loop until ACCEPT or MINOR REVISIONS, max 4 rounds per paper. Codex (gpt-5.6-sol, high): LaTeX formatting check per paper (max 2 fix passes), code-layer review, code-evidence audit, website review.
Research workers: Opus 5. Synthesis: Fable 5.1 (Opus if the Fable weekly window is at or above 85 percent). Utilities: Sonnet. Usage windows checked before every spawn wave; no spawn when the 5-hour window is at or above 85 percent.
0 pre-flight; 1 setup and sanity tests and this critique; 2 knowledge base (context transcript plus web research per Part); 3a code plan then code implementation (background); 3b five workers in parallel with contracts and board; post-worker review gate; integration reviewer gate; 4 synthesis; 4.5 bib gate, style, format, humanizer checks; 5 code verification; 6 website (LaTeX pre-pass, pandoc, HTML post-pass, KaTeX build-time rendering, post-build validator, 375px mobile check, OG validation, Codex website review, Vercel deploy); 7 social posts; 8 README, commit, GitHub repo YonedaAI/agent-algebra, final Slack summary.
- Scope: the user chose five Parts plus synthesis. Mitigation: every candidate result is proved, narrowed, or downgraded to a Proposition with countermodel, Conjecture, or Limitation (negative results are first-class); tests validate finite models only; the synthesis must contribute one cross-Part theorem (conservativity: Part III and IV operators do not change the equational theory of Part II terms up to ~).
- Thesis stated incrementally: the central claim now assigns each operator to the Part whose assumptions justify it (above).
- Signature fully typed: init : X → S, step : S × I → T(Σ × S) with outputs inside T, out : S → Y + 1 with termination outside T and silent; F(S) = (Y + 1) × (T(Σ × S))^I.
- Effects: T ranges over the fixed list Id, P, D, Exc; every law is stated per instance; T models only the leaf's choice effect; logs, shared state, scheduling and storage are agents and wiring, not effects in T.
- P and D never combined: nondeterministic ⊕ only for T = P, probabilistic ⊕_p only for T = D; no convex model.
- Kleene structure named precisely: KAT modulo trace-set equivalence (both distributive laws); left-handed Kleene algebra with tests modulo bisimilarity (left distributivity fails), citing Kozen and Silva 2012.
- Category defined first: Ag(I, Σ) with objects X, morphisms agents X ⇒ Y modulo ~, identity skip, composition ;, typing rules; the theorem is "sequential category", Kleisli is a remark.
- Delayed feedback: an explicit delay endofunctor; the delayed-trace axioms of Sprunger and Katsumata are listed (naturality in non-feedback ports, vanishing, superposing, delayed yanking Tr(swap) = delay_1); ordinary yanking fails with a witness; no traced-monoidal claim.
- Run is semantic closure, not an operator; Part I states the boundary; Part III proves Run coincides with the Tr form as a theorem about closed systems.
- Congruence proved operator by operator for Part II; Parts III and IV treat crash and schedule as inputs and state Sup, Persist and Replay results as refinements over marker erasure, not congruence claims.
- Session typing = fidelity + progress; deadlock defined operationally; binary deadlock freedom assumes both clauses, duality and a fair scheduler.
- Two parallel fragments: shuffle and CKA exchange only for the channel-only fragment; linearizability with tick order for the shared-object fragment; no CKA claim there.
- Kahn determinism only for the named fragment Wf_KPN (deterministic nodes, blocking reads, unbounded FIFOs, DAG topology, no race, retry or timeout); non-examples listed.
- Supervision transparency replaced by supervision refinement with explicit assumptions (deterministic children, Persist every tick, replay-idempotent environment with a deduplication key, marker erasure, stuttering closure).
- Exactly-once renamed effectively-once with crash points between ticks and a stated deduplication key.
- Planning modeled as a two-player game over an AND/OR transition system; plan terms are strategies; weak, strong and strong-cyclic defined over paths, strategies and fair paths.
- Decision and control theorems split with complete hypotheses: finite discounted MDP, semi-Markov options with bounded expected duration, finite POMDP, discrete linear system with Schur stability.
- Sixteen fields: adequacy criterion per field (soundness, one-way simulation, or proved limitation) with an explicit syntactic translation; "derived operator" replaced by "encoded mechanism with an adequacy result".
- Code implements a declared finite fragment; each claim row labeled tested, exhaustively checked, or proof-only.
- Property tests labeled finite-model validation; theorems rest on proofs.
- Verification circularity: review criteria are frozen in the reviewer prompts; unresolved reviewer objections are retained in reviews/ and summarized in each paper's Limitations; the author reads every final draft; an external named human review is outside this pipeline and is recorded as a limitation, not claimed.
- Bibliography gate extended: resolution plus title and first-author match against the resolved page; load-bearing citations name the specific result.
- Permission bypass is a platform setting the user selected for an unattended run; agents are confined to the project directory; accepted as an operational choice.
- Dependency gate added: Parts III to V draft only after the Part I and II contracts exist and an orchestrator contract-consistency check has posted CONTRACTS REVIEWED (bounded wait 25 minutes).
Non-blocking suggestions adopted: Part-specific qualification after the central claim; code claims selected by risk and coverage rather than count; unresolved major objections escalated into Limitations rather than exhausted by round caps; the synthesis contributes a cross-Part theorem; negative results kept; a toolchain manifest pinned in the README. Slack cadence and the automated humanizer pass stay as the user specified.
- Agent signature frozen and interface-polymorphic (team/CLAIMS.md section 1): X and Y are value types handed in at start and out at halt; I and Σ are per-tick alphabets; silence is τ; termination is halt : S → Y + 1, a state predicate outside T; identity and ; are derived from it.
- Monads defined exactly: Id; P = finite nonempty subsets (no empty choice); D = finite-support rational distributions summing to 1 (no subdistributions); Exc_E = X + E with E finite; admissible state spaces stated; laws per instance only.
- Claim ledger (team/CLAIMS.md section 2): every result carries one relation (~, ≃_tr, ⊑, trace-set equality, equality of values, reachability), its effect instances, hypotheses, kind, and code rows; "up to ~" is never used loosely.
- Part V is declared an interpretation layer with no operator of its own; the central claim says so.
- Conservativity restated as definitional conservativity over the marker-free Part II fragment under the lockstep scheduler with no crashes (thm:synthesis:conservativity), with the embedding reflecting bisimilarity.
- Staged contract gate: I and II, then III, then IV and V after a CONTRACTS REVIEWED line.
- Sixteen-field coverage matrix (team/CLAIMS.md section 3) with one accountable claim per field.
- Objection policy: a major correctness objection triggers repair, downgrade or removal with a confirming round, or a held paper; never a Limitation. Gate artifacts and the single-respawn rule are stated.
Non-blocking adopted: stable claim IDs are the labels; downgrade kinds are Theorem, Proposition, Counterexample, Conjecture, Limitation; the knowledge base validates load-bearing citations in Phase 2; bounded-channel tests are marked as not validating the unbounded-FIFO theorem; "nondeterminate" replaced by "nondeterministic"; the code agent received the frozen fragment before implementing the semantics.
- The exception monad is dropped: failure is a terminal outcome halt : S → Y + E + 1, so T ranges over Id, P, D only, all commutative; ▷ continues as the recovery agent started at the failure reason.
- Halted and failed states stutter by a required transition rule; outcomes are evaluated between ticks.
- Trace semantics frozen with its full type [[A]] : X × I* → T(Σ* × (Y + E + 1)), accepted traces, stuttering closure, and a complete relation vocabulary (~, ≃_tr, ≃_acc, ⊑, ~_erase, =_out, =_val, ⊆, reach, lin, |Out|, game solution).
- Value types versus per-tick interfaces separated; the types of ⊗, Tr, swap, link and Run are derived in CLAIMS.md section 1; Run is semantic closure.
- 0 is divergence; every law involving 0 is stated under accepted-trace equality, never under ~ (GKAT split into gkat-bisim and gkat-zero; KAT stated as kat-accepted).
- Every compound ledger row is split into atomic rows with one relation, one instance set, one hypothesis set and one kind (Counterexamples are their own rows, cex::).
- Superseded text is non-normative: CLAIMS.md governs over PLAN.md and prospectus sections 1 to 7; the central claim now says Parts II to IV introduce the operators and Part V interprets, and promises an adequacy result that may be a soundness theorem, a one-way simulation, or a proved limitation.
- closed-loop-is-trace carries dual interfaces, register initialisation, lockstep scheduling and hiding as hypotheses.
- effectively-once requires deterministic children or persisted state with recorded choices; persist-commutes and supervision-refinement are stated over marker erasure.
- Shield split into an adversarial theorem (P environment, deterministic policy) and a stochastic proposition (D policy, probability one); gate-is-shield restricted to Id and P with a deterministic oracle; LLM and POMDP results carry the rational finite-support (bounded-generation) abstraction.
- Coverage matrix completed with atomic simulation claims for actors, tuple spaces and OTP strategies, all IDs written in full.
- Audit outcomes now include BOUNDED_CHECK_ONLY and PROOF_ONLY; four Gemini rounds is a hard total cap and an open major objection at the cap holds the paper.
Non-blocking adopted: the branching counterexample carries rational weights 1/2, 1/2; the observation policy (fairness, erasure, hiding, stuttering) is defined once in CLAIMS.md section 1; a claim-dependency list follows the ledger; the series-parallel claim is split into a graph-shape proposition and a behavioral counterexample.
- Gemini review-fix loop on every paper and the synthesis (max 4 rounds, per-round files, mutex).
- Codex formatting check on every paper after the review loop (max 2 fix passes).
- Codex website review before deployment.
- Slack notification after each worker, the synthesis, code verification, deployment, and a final summary.
- Review-fix loops iterate; gates respawn on failure and abort on a second failure; no stubs, no self-review.
- Every agent spawn bypasses permission prompts.
- Every URL in every Slack message is a markdown link on its own bold-label line.
- Slack linter before every send and pipeline validator before the final send.