Throughout this blog we've been building Petri nets, analyzing them with ODEs, proving transitions in zero knowledge, composing them via typed links, and reading strategic values through lenses. Each technique works. But why do they all work together so cleanly?
The answer is a single mathematical structure: the symmetric monoidal category (SMC). Petri nets aren't just modeled by SMCs — they are SMCs. Every net we've built is a collection of morphisms in a category where parallel composition is the monoidal product and the wiring between components respects symmetry.
This post connects the structure we've been using to the theory that explains it.
A Petri net transition consumes tokens from input places and produces tokens into output places. In categorical terms, this is a morphism — a map from domain to codomain:
The transition t with inputs {p1, p2} and outputs {q1, q2, q3} is a morphism:
t : p1 ⊗ p2 → q1 ⊗ q2 ⊗ q3
The ⊗ is the monoidal product — it means "these things exist side by side." Two tokens in separate places aren't combined or merged; they coexist independently. The monoidal product is how Petri nets express concurrency: p1 ⊗ p2 means both places are marked, and both tokens are available simultaneously.
Places are the objects. Transitions are the morphisms. The multiset of tokens across all places — the marking — is an object in the free commutative monoid generated by the places.
Every category has composition of morphisms. A monoidal category adds a second operation: the monoidal product. These correspond exactly to the two ways we compose Petri nets.
Sequential composition (f ; g): the output places of transition f become the input places of transition g. Tokens flow through. This is ordinary morphism composition — the same operation that makes categories useful for modeling processes with stages.
Parallel composition (f ⊗ g): two transitions sit side by side with no shared places. They fire independently. This is the monoidal product — it expresses concurrency without interaction.
The symmetry is the swap map σ : A ⊗ B → B ⊗ A. It says we can reorder the components of a parallel composition without changing the behavior. In Petri net terms: the order we list the places doesn't matter. A net with places {stock, orders} is the same net as {orders, stock}. This is exactly the commutativity property we noted in Categorical Net Types — schema order doesn't matter because the composition is symmetric monoidal.
The formal result, due to Sassone (1995) and Meseguer-Montanari (1990), is:
A Petri net generates a free symmetric monoidal category whose objects are multisets of places and whose morphisms are equivalence classes of transition firings.
"Free" means nothing extra is imposed — the only equations are the ones forced by the SMC axioms (associativity, unitality, symmetry). The category captures exactly the net's behavior and nothing more.
What this gives us:
Associativity. Composing transitions is associative: (f ; g) ; h = f ; (g ; h). We can bracket firing sequences however we want. This is why event sourcing works — the fold over events doesn't depend on how we chunk the replay.
Unit. The identity morphism on a place is "do nothing — the token stays." Every place has an identity, and composing with it changes nothing. This is why idle places don't affect analysis.
Symmetry. The swap σ : A ⊗ B → B ⊗ A is natural. Reordering places is an isomorphism, not a transformation. This is why ODE signatures are invariant under reordering — shuffling places and transitions 100 times produces the same solution every time.
Bifunctoriality. Sequential and parallel composition interact correctly: (f₁ ⊗ f₂) ; (g₁ ⊗ g₂) = (f₁ ; g₁) ⊗ (f₂ ; g₂) when the wiring matches. In net terms: firing two independent transitions and then two more independent transitions is the same as firing each pair sequentially. This is why concurrent execution and sequential replay produce the same result.
The SMC structure has been present in every post. We just haven't named it.
The Token Language defines cell, func, arrow, guard — these are the generators of a free SMC. Cells are objects, funcs are morphisms, arrows define the domain and codomain of each morphism, and guards are predicates that constrain which morphisms are composable. The four-term DSL is a syntax for writing SMC generators.
Categorical Net Types defines five specializations. Each net type is a sub-SMC with additional structure — WorkflowNet restricts to single-token sequential paths (a free category, not just free SMC), ResourceNet adds conservation (P-invariants as kernel elements of the incidence matrix), GameNet combines both. The typed links (EventLink, DataLink, TokenLink, GuardLink) are functors between these sub-SMCs, preserving the structure each type demands.
Declarative Differential Models define the ODE system by reading the incidence matrix. The incidence matrix is the linear map between the free commutative monoids on transitions and places — it's the linearization of the SMC's morphism structure. Mass-action kinetics is a functor from the discrete SMC to continuous dynamics.
The Incidence Reduction works because the decoupled ODE system respects the monoidal product structure. Each accumulator's equation ẋᵢ = 1 - nᵢxᵢ is independent — the product decomposition of the lens mirrors the monoidal product of the SMC. No information leaks between components because the monoidal product means independence.
ZK Proofs verify transition firings — morphism validity — without revealing the marking. The Groth16 circuit encodes the incidence matrix (the SMC's morphism structure) as arithmetic constraints. The proof says "this morphism was applied to a valid object and produced a valid object" without disclosing which object. Privacy is a property of the morphism, not the objects.
ODE Signatures are invariant under isomorphism in the SMC. Two nets with different labels but the same wiring produce identical ODE solutions because they're isomorphic objects in the same category. The signature is a categorical invariant — it depends only on the isomorphism class, not the representation.
The lens structure we identified in the incidence reduction has a precise SMC interpretation.
A lens in a monoidal category is a pair of morphisms — Get and Put — satisfying coherence laws. For the analysis net:
The product decomposition Lens(A ⊗ B) ≅ Lens(A) ⊗ Lens(B) holds because the monoidal product distributes over lenses in an SMC. This is why dynamic evaluation works: updating one position's marking doesn't affect another's lens. The independence isn't accidental — it's a consequence of the monoidal structure.
The lens decomposition we found in the incidence reduction is not an isolated construction. Jules Hedges' Open Games framework (2018) arrives at the same structure from the game theory side — and the convergence is revealing.
In open games, a game is an optic (generalized lens) in a symmetric monoidal category. The forward pass carries players' strategies to outcomes. The backward pass propagates utilities back to decision points. Games compose sequentially (players move in order) and in parallel (players move independently) — the two SMC operations. Hedges' central result: Nash equilibrium is compositional. We can check equilibrium component-by-component because the optic decomposition respects the monoidal product.
Our construction does the same thing from the Petri net side. The Get morphism maps markings to strategic values via the incidence matrix. The Put morphism updates a marking and recomputes. The decomposition Lens(A ⊗ B) ≅ Lens(A) ⊗ Lens(B) means each place gets an independent lens — exactly as each player gets an independent game in Hedges' framework.
The correspondence is precise:
⊗; we show strategic evaluation decomposes along ⊗. Same theorem, different instances.The game models in this blog — tic-tac-toe, Hold'em — are literally open games composed from Petri net transitions. When we evaluate a position by reading the ODE's fixed point, we're computing the backward pass of an optic. When we update a marking and recompute, we're applying the Put of a lens. The Petri net formulation and the open game formulation agree because they're both optics in the same SMC.
Hedges started with games and discovered they form an SMC of optics. We started with Petri nets and discovered the analysis produces optics. The convergence isn't coincidence — it's the monoidal structure asserting itself. Any system where independent components evaluate independently will produce this pattern, because that's what the monoidal product means.
Step back and look at what we've built across this blog. The layers compose:
Theory (objects): DDM, Token Language, Net Types, JSON-LD — these are the generating objects of the ecosystem's SMC.
Models (morphisms): Tic-tac-toe, coffee shop, Hold'em, enzyme kinetics, sudoku — each is a morphism built from the theory generators.
Analysis (functors): Incidence reduction, ODE signatures, P-invariants — these are functors that map nets to their properties, preserving the monoidal structure.
Proofs (natural transformations): ZK proofs, lenses, sealed invariants — these are transformations between functors, proving that properties hold uniformly across all models.
Each layer composes with the ones above and below it. Models compose via typed links. Analysis composes via functor composition. Proofs compose via vertical composition of natural transformations. The whole stack is an SMC of SMCs — a 2-category, if we want to be precise.
This isn't imposed structure. We didn't design the blog to be a 2-category. The posts accumulated one at a time, each solving a specific problem. But Petri nets carry symmetric monoidal structure inherently, and everything built on them inherits it. The coherence shows up as: techniques from one post transfer cleanly to another. The ODE analysis that works on tic-tac-toe works on poker. The ZK circuit that proves tic-tac-toe transitions proves any Petri net transition. The composition rules that wire order processing to inventory wire any two schemas together.
Category theory has a reputation for being abstract machinery disconnected from practice. But in this ecosystem, the SMC structure is the reason practical things work:
Models compose without surprises because the monoidal product guarantees independence. Adding a new schema to a CompositeNet can't break existing schemas — monotonicity follows from the SMC axioms.
Analysis transfers across domains because functors preserve structure. The same incidence reduction works on games, resources, and biochemistry because it's a functor — it maps any net to its strategic values, regardless of what the tokens represent.
Proofs are generic because the ZK circuit encodes the incidence matrix, not the application. Swapping topology constants gives proofs for a different game, a different workflow, a different token standard. The circuit is a natural transformation — it works uniformly across all objects in the category.
The ODE is well-behaved because mass-action kinetics is a monoidal functor from discrete nets to continuous dynamics. It preserves the product structure: independent components stay independent. The decoupling lemma is a theorem about monoidal functors, not a lucky coincidence about ODEs.
Lenses decompose cleanly because the monoidal product distributes over the lens construction. Each place gets its own lens, composed in parallel. Dynamic evaluation updates one lens without touching the others — not because we designed it that way, but because the SMC forces it.
The category theory isn't a framework we adopted. It's the structure we discovered by building things that work.
For the net type taxonomy: Categorical Net Types
For the lens interpretation: The Net as a Lens
For the incidence matrix as linear map: The Incidence Reduction
For the ZK circuit encoding: Zero-Knowledge Proofs for Petri Nets
See also Petri Nets as a Universal Abstraction for the full treatment of these ideas.