# String Diagram Rewriting Protocol > Kernel protocol for compositional string diagram rewriting across all skills - Skill: `plurigrid/string-diagram-rewriting-protocol` (Agent Skill, multi-file: 2 files) - Install (CLI): `npx skillmds@latest add plurigrid/string-diagram-rewriting-protocol` - Raw SKILL.md: https://api.skillmd.com/api/skills/plurigrid/string-diagram-rewriting-protocol/raw - Safety review: pending - Works with: Claude Code, Claude.ai, OpenAI Codex - Category: Coding & Dev Tools - License: UNLICENSED - Author: plurigrid (https://skillmd.com/u/plurigrid) - Updated: 2026-09-17 - Page: https://skillmd.com/skills/plurigrid/string-diagram-rewriting-protocol --- # SKILL: String Diagram Rewriting Protocol **Trit**: 0 (ERGODIC) **Domain**: category-theory, rewriting-systems, string-diagrams, meta-protocol **Role**: Kernel skill connecting 20 rewriting-capable skills into a unified pipeline ## 1. Purpose This skill defines the **universal rewriting protocol** by which all information streams and decisions are represented as string diagrams and transformed via categorical rewriting. It is the missing meta-layer: every other skill in the 5-layer architecture plugs into this protocol through a standard interface. ## 2. String Diagrams: Syntax A **string diagram** in a monoidal category (C, ⊗, I) is a planar graph where: - **Wires** = objects (types) in C - **Boxes** = morphisms f : A → B - **Vertical composition** = sequential application (;) read top-to-bottom - **Horizontal composition** = tensor product (⊗) read left-to-right - **Cups/caps** = units/counits of duality (when C is compact closed) - **Crossings** = symmetry σ_{A,B} : A ⊗ B → B ⊗ A (when C is symmetric) ``` A B A B │ │ │ │ ├───┤ │ │ │ f │ : A ⊗ B → C │ │ ├───┤ ├───┤ │ │ │ g │ : A ⊗ B → C ⊗ D │ C │ ├───┤ │ │ │ │ C D Sequential: Tensor: A A C │ │ │ ┌─┴─┐ ┌─┴─┐ │ │ f │ │ f │ │ └─┬─┘ └─┬─┘ │ B B │ │ │ ┌─┴─┐ ┌─┴─┐ │ │ g │ │ g │ │ └─┬─┘ └─┬─┘ B D C g ∘ f f ⊗ g ``` ### 2.1 Formal Grammar ``` Diagram ::= Wire | Box | Seq | Tensor | Id | Swap | Trace Wire ::= object in Ob(C) Box ::= morphism f : A₁ ⊗ ... ⊗ Aₙ → B₁ ⊗ ... ⊗ Bₘ Seq ::= Diagram ; Diagram (vertical composition) Tensor ::= Diagram ⊗ Diagram (horizontal juxtaposition) Id ::= id_A : A → A (straight wire) Swap ::= σ_{A,B} : A ⊗ B → B ⊗ A (crossing) Trace ::= Tr^U(f) : A → B (feedback loop, f : A ⊗ U → B ⊗ U) ``` ### 2.2 Axioms (Coherence Conditions) Every valid string diagram manipulation must preserve these: **Monoidal axioms:** ``` (f ⊗ g) ⊗ h = f ⊗ (g ⊗ h) associativity (α) I ⊗ f = f = f ⊗ I unitality (λ, ρ) (f ; g) ⊗ (h ; k) = (f ⊗ h) ; (g ⊗ k) interchange law ``` **Symmetric monoidal axioms:** ``` σ_{A,B} ; σ_{B,A} = id_{A⊗B} involution σ_{A⊗B,C} = (σ_{A,C} ⊗ id_B) ; (id_C ⊗ σ_{A,B}) hexagon ``` **Traced monoidal axioms** (when applicable): ``` Tr^U(f ⊗ id_U) = f vanishing Tr^U(σ_{A,U}) = id_A superposing Tr^{U⊗V}(f) = Tr^U(Tr^V(f)) composition (Joyal-Street-Verity) ``` **Mac Lane coherence theorem**: Every diagram of canonical isomorphisms (built from α, λ, ρ, σ) commutes. This means string diagram equality = ambient isotopy of the plane. ## 3. Rewrite Rules: The DPO Framework A **rewrite rule** is a span in the category of string diagrams: ``` L ←──l── K ──r──→ R │ │ m (match) m* (comatch) │ │ ▼ ▼ G ←────── D ──────→ H ``` Where: - **L** = left-hand side (pattern to match) - **K** = interface (what is preserved) - **R** = right-hand side (replacement) - **G** = host diagram (before rewrite) - **H** = result diagram (after rewrite) - **D** = context (G with L removed = H with R removed) ### 3.1 DPO Conditions The bottom squares must be **pushouts** in the ambient adhesive category: 1. **Matching**: Find m : L → G (a mono/regular mono) 2. **Gluing condition**: The pushout complement D exists iff: - **Dangling condition**: No edge in G\m(L) is incident to a node in m(L)\m(K) - **Identification condition**: m is injective on L\K 3. **Pushout construction**: H = D +_K R ### 3.2 Rule Interface Every skill that provides rewrite rules must implement: ``` RewriteRule = { name : String, L : Diagram, -- left-hand side K : Diagram, -- interface R : Diagram, -- right-hand side l : Morphism(K, L), -- left leg r : Morphism(K, R), -- right leg NAC : [Diagram], -- negative application conditions PAC : [Diagram], -- positive application conditions priority: ℤ, -- scheduling priority trit : GF3, -- which phase: -1 verify, 0 transport, +1 generate } ``` ### 3.3 SPO and SqPO Extensions | Approach | Pushout type | Cloning | Deletion | Use case | |----------|-------------|---------|----------|----------| | DPO | Double | No | Safe | Default: well-behaved rewriting | | SPO | Single | No | Greedy | When dangling edges should vanish | | SqPO | Sesqui | Yes | Safe | Duplicating subdiagrams | **Selection heuristic**: Use DPO unless the rule requires cloning (→ SqPO) or greedy deletion (→ SPO). The `trit` field guides this: - `+1` generation rules often need SqPO (create copies) - `0` transport rules use DPO (structure-preserving) - `-1` verification rules use DPO with NACs (reject bad patterns) ## 4. Confluence and Termination ### 4.1 Critical Pairs Two rules r₁, r₂ form a **critical pair** when their left-hand sides overlap: ``` L₁ / \ / \ G₁ G ← overlap \ / \ / L₂ ``` The overlap is computed as the **pushout** of L₁ ← K → L₂ over their common sub-diagram K. **Procedure** (Plump 1993, Ehrig et al. 2006): 1. Enumerate all pairs of rules (rᵢ, rⱼ) 2. For each pair, compute all overlaps via joint surjections 3. Apply rᵢ and rⱼ to each overlap, yielding (H₁, H₂) 4. Check if H₁ and H₂ are **joinable** (rewrite to a common form) ### 4.2 Local Confluence (Newman's Lemma) **Theorem** (Newman 1942): If a rewriting system is: - **Terminating** (no infinite reduction sequences), AND - **Locally confluent** (all critical pairs are joinable) Then it is **confluent** (all divergences can be resolved). ### 4.3 Termination Orderings For string diagram rewriting, use a **weighted size measure**: ``` w(d) = Σ_{box b in d} weight(b) + |wires(d)| ``` A rule L → R is **size-decreasing** if w(L) > w(R) for all matches. Rules that increase size must be controlled by strategies or priorities. ### 4.4 Normal Forms A diagram d is in **normal form** w.r.t. rule set R if no rule in R applies to d. The rewriting protocol seeks normal forms in three phases: ``` Phase 1 (+1): GENERATE — expand abbreviations, unfold definitions Phase 2 (0): TRANSPORT — apply equational rewrites until fixpoint Phase 3 (-1): VERIFY — check invariants, flag contradictions ``` ## 5. The Five-Layer Architecture Each layer provides rules to the protocol: ``` Layer 5: WORLDING ← decision + feedback worlding, glass-bead-game, active-interleave, cybernetic-open-game Layer 4: DATA & CONCURRENCY ← state + synchronization acsets-algebraic-databases, crdt, propagators Layer 3: SEMANTICS ← meaning + equivalence open-games, bisimulation-game, linear-logic Layer 2: REWRITING ENGINES ← rule application algebraic-rewriting, homoiconic-rewriting, categorical-rewriting-triad4 interaction-nets, graph-grafting Layer 1: FORMALISM ← syntax + types recursive-string-diagrams, discopy-operads, zx-calculus topos-adhesive-rewriting, operadic-composition ``` ### 5.1 Inter-Layer Protocol Information flows **bidirectionally** between layers: ``` Layer N+1 Layer N │ │ │ ──── rule request ────→ │ "apply this rewrite" │ │ │ ←── result diagram ─── │ "here is the rewritten diagram" │ │ │ ←── critical pair ──── │ "these rules conflict" │ │ │ ──── strategy hint ───→ │ "prefer this rule ordering" ``` ### 5.2 Skill Binding Interface Each skill binds to the protocol by exporting: ``` SkillBinding = { skill_name : String, layer : 1..5, trit : GF3, rules : [RewriteRule], category : CategorySpec, -- what ambient category the rules live in objects : [ObjectSpec], -- wire types this skill introduces functors : [FunctorSpec], -- translations to/from other skills' categories } ``` **CategorySpec**: ``` CategorySpec = { name : String, -- e.g. "FinGraph", "Petri", "ZX" monoidal : Bool, -- has ⊗? symmetric : Bool, -- has σ? compact : Bool, -- has cups/caps? traced : Bool, -- has Tr? adhesive : Bool, -- safe DPO? enrichment : Option(String), -- e.g. "CMon" for linear logic } ``` ## 6. GF(3) Conservation in Rewriting Every rewrite step must conserve the GF(3) trit sum: ``` trit(L) ≡ trit(R) (mod 3) ``` This is enforced by assigning trits to generators: | Generator type | Trit | Role | |---------------|------|------| | Introduction | +1 | Create new structure | | Transportation| 0 | Move/reshape without creating or destroying | | Elimination | -1 | Remove/verify/simplify | **Conservation theorem**: If every rewrite rule has trit(L) ≡ trit(R) mod 3, then trit is an invariant of the rewriting system. Proof: by induction on rewrite steps, each step preserves the sum. ### 6.1 Balanced Triads Three skills form a **balanced triad** when their trits sum to 0: ``` skill_a (+1) + skill_b (0) + skill_c (-1) ≡ 0 (mod 3) ``` The protocol ensures every rewriting pipeline passes through a balanced triad: 1. **Generate** (+1): Produce candidate diagrams 2. **Transport** (0): Apply equational rewrites 3. **Verify** (-1): Check invariants, reject ill-formed results ### 6.2 Layer Trit Assignments ``` Layer 1 (Formalism): recursive-string-diagrams 0 operadic-composition 0 discopy-operads 0 topos-adhesive-rewriting +1 zx-calculus -1 Layer 2 (Rewriting): algebraic-rewriting +1 graph-grafting -1 homoiconic-rewriting 0 categorical-rewriting 0 interaction-nets -1 Layer 3 (Semantics): open-games +1 linear-logic 0 bisimulation-game -1 Layer 4 (Data): acsets-algebraic-databases 0 propagators +1 crdt 0 Layer 5 (Worlding): worlding +1 glass-bead-game 0 active-interleave 0 cybernetic-open-game 0 ``` Each layer sums to 0 (mod 3): the protocol is **globally balanced**. ## 7. The Rewriting Pipeline ### 7.1 Full Pipeline ``` Input Stream ──→ PARSE ──→ DIAGRAM ──→ REWRITE ──→ NORMAL FORM ──→ DECIDE │ │ │ │ │ L1 L1 L2+L1 L3+L4 L5 │ │ │ │ │ tokenize build AST apply rules evaluate commit to boxes to diagram to fixpoint semantics action ``` ### 7.2 Rewrite Loop ```python def rewrite(diagram, rules, strategy="innermost"): """Core rewriting loop.""" while True: matches = find_all_matches(diagram, rules) if not matches: return diagram # normal form reached match = strategy.select(matches) # DPO step assert gluing_condition(match) context = pushout_complement(match) diagram = pushout(context, match.rule.R) # GF(3) conservation check assert trit(diagram) == trit(original) % 3 ``` ### 7.3 Strategies | Strategy | Description | When to use | |----------|-------------|-------------| | Innermost | Reduce innermost redexes first | Default; mimics call-by-value | | Outermost | Reduce outermost redexes first | Lazy evaluation; may find NF faster | | Priority | Follow rule priorities | When rules have explicit ordering | | Parallel | Apply non-overlapping rules simultaneously | Interaction nets; maximum parallelism | | Adaptive | Use propagator network to select | When semantic feedback matters | ## 8. Adhesive Categories for String Diagrams The protocol requires the ambient category to be **adhesive** (or at least quasi-adhesive) to guarantee well-behaved DPO rewriting. ### 8.1 Adhesive Category Axioms A category C is **adhesive** if: 1. C has pushouts along monomorphisms 2. C has pullbacks 3. Pushouts along monos are **van Kampen squares**: ``` A van Kampen square is a pushout square: A ──→ B │ │ ▼ ▼ C ──→ D such that for any commutative cube with this square as bottom face, if the back faces are pullbacks, then: top face is pushout ⟺ front faces are pullbacks ``` ### 8.2 Examples of Adhesive Categories | Category | Adhesive? | String diagrams? | Used by | |----------|-----------|-------------------|---------| | **Set** | Yes | No (discrete) | acsets base | | **Graph** | Yes | Yes (typed) | graph-grafting | | **C-Set** (presheaves on C) | Yes | Yes | algebraic-rewriting | | **Petri** | Quasi | Yes (nets) | open-games | | **Hypergraph** | Yes | Yes (hyper-wires) | operadic-composition | | **Cospan(FinSet)** | No* | Yes (open systems) | crdt, propagators | *Cospans are not adhesive but can use AGREE framework (Corradini et al. 2020). ## 9. Connections to Each Skill ### Layer 1: Formalism **recursive-string-diagrams**: Provides the base `Diagram` type — white trapezoid as atomic morphism. This skill supplies recursive nesting: diagrams inside boxes. **discopy-operads**: Python implementation of monoidal categories via DisCoPy. Supplies `Diagram`, `Box`, `Ty` (type = wire), and free monoidal category construction. **zx-calculus**: Specialized string diagrams for quantum circuits. Z-spiders (green), X-spiders (red), Hadamard boxes. The ZX rewrite rules are a complete equational theory for qubit quantum mechanics (Coecke-Duncan 2011, Backens 2014). **topos-adhesive-rewriting**: Provides the adhesive category infrastructure. Van Kampen conditions, incremental query updating, pushout computation. **operadic-composition**: Colored operads for multi-input composition. Supplies the `compose_operad` operation for wiring diagrams with multiple ports. ### Layer 2: Rewriting Engines **algebraic-rewriting**: AlgebraicRewriting.jl — DPO/SPO/SqPO over C-Sets. Primary computational engine for applying rules. Supplies `rewrite`, `homomorphisms`. **interaction-nets**: Lafont's optimal reduction. Rules are local (one active pair), deterministic, and maximally parallel. Three combinators: γ (constructor), δ (duplicator), ε (eraser). **homoiconic-rewriting**: Self-modifying rules. Rules can rewrite other rules. Five-layer architecture for reflective rewriting (cf. Clavel-Meseguer rewriting logic). **categorical-rewriting-triad4**: Design-phase system using DisCoPy + graph grafting for world transformation. **graph-grafting**: Tree/graph operations with GF(3) coloring. Supplies `graft!`, `prune!`, `transplant!` for structural modification. ### Layer 3: Semantics **open-games**: Hedges-Ghani compositional game theory. Games as string diagrams in Para(Optic(C)). Players are boxes, strategies flow through wires. Supplies Nash equilibrium checking as a semantic invariant. **bisimulation-game**: Attacker/Defender games for observational equivalence. Two diagrams are equivalent iff Defender has a winning strategy. Supplies behavioral equivalence as a semantic relation. **linear-logic**: Girard's resource-sensitive logic. Provides the type system for wires: ⊗ (tensor), ⅋ (par), ! (of course), ? (why not), ⊸ (lollipop). Star-autonomous categories as semantics. ### Layer 4: Data & Concurrency **acsets-algebraic-databases**: Attributed C-Sets as the data model for diagrams. Functors C → Set give typed, attributed graphs. Supplies Δ (restriction), Σ (left Kan), Π (right Kan) data migrations. **crdt**: Conflict-free replicated data types. Join-semilattice merge for concurrent diagram edits. Supplies `merge : D × D → D` with commutativity, associativity, idempotence. **propagators**: Radul-Sussman constraint propagation. Cells accumulate partial information about diagrams; propagators enforce constraints bidirectionally. Supplies the adaptive strategy engine. ### Layer 5: Worlding **worlding**: Meta-skill for composable world construction. Each "world" is a rewriting context with its own rule set. Supplies `world-hop` for switching between rewriting contexts. **glass-bead-game**: Interdisciplinary synthesis via analogy. Connections between domains as rewrite rules. Supplies cross-domain translation. **active-interleave**: Context sampling from multiple information streams. Supplies the input pipeline: which diagrams to rewrite next. **cybernetic-open-game**: Agent ↔ Environment feedback loop as open game. Supplies the decision-making layer: which rewrite to commit. ## 10. Soundness and Completeness ### 10.1 Soundness A rewriting system R is **sound** w.r.t. an equational theory E if: ``` d₁ →_R d₂ implies d₁ =_E d₂ ``` Every rewrite rule must be derivable from the axioms of the ambient monoidal category. ### 10.2 Completeness A rewriting system R is **complete** (= convergent) if it is: 1. **Confluent**: d₁ ←* d *→ d₂ implies ∃d₃: d₁ *→ d₃ ←* d₂ 2. **Terminating**: No infinite rewrite sequences **Knuth-Bendix completion**: Given an equational theory E, attempt to generate a complete rewriting system R by: 1. Orient equations into rules (using a termination ordering) 2. Compute critical pairs 3. Add new rules to resolve non-joinable critical pairs 4. Repeat until no new critical pairs arise (or fail) ### 10.3 Decidability String diagram equality is decidable for: - Free symmetric monoidal categories (Joyal-Street 1991) - ZX-calculus for Clifford circuits (Backens 2014) - Interaction nets with the 3 combinators (Lafont 1997) It is undecidable in general (reduces to Post correspondence problem). ## 11. Implementation Sketch ### 11.1 Julia (via AlgebraicRewriting.jl + Catlab.jl) ```julia using Catlab, AlgebraicRewriting # Define the wire types @present WireTheory(FreeSymmetricMonoidalCategory) begin A::Ob; B::Ob; C::Ob f::Hom(A, B) g::Hom(B, C) end # Define a rewrite rule: f;g ↦ h (where h = g∘f) L = @acset Graph begin V=3; E=2; src=[1,2]; tgt=[2,3] end K = @acset Graph begin V=3; E=0 end R = @acset Graph begin V=3; E=1; src=[1]; tgt=[3] end rule = Rule(homomorphism(K, L), homomorphism(K, R)) # Apply to a host graph G = @acset Graph begin V=5; E=4; src=[1,2,3,4]; tgt=[2,3,4,5] end H = rewrite(rule, G) ``` ### 11.2 Python (via DisCoPy) ```python from discopy import Ty, Box, Diagram, Functor # Wire types A, B, C = Ty('A'), Ty('B'), Ty('C') # Morphisms (boxes) f = Box('f', A, B) g = Box('g', B, C) # String diagram: sequential composition d = f >> g # g ∘ f : A → C # Rewrite rule: replace f >> g with h h = Box('h', A, C) rewritten = d.replace(f >> g, h) ``` ### 11.3 Zig (via interaction tensor) ```zig const Diagram = struct { boxes: []Box, wires: []Wire, pub fn compose(self: Diagram, other: Diagram) Diagram { ... } pub fn tensor(self: Diagram, other: Diagram) Diagram { ... } pub fn rewrite(self: Diagram, rule: Rule) ?Diagram { ... } pub fn trit(self: Diagram) i2 { var sum: i32 = 0; for (self.boxes) |b| sum += b.trit; return @intCast(i2, @mod(sum, 3)); } }; const Rule = struct { L: Diagram, K: Diagram, R: Diagram, l: Morphism, // K → L r: Morphism, // K → R }; ``` ## 12. Verification Checklist For any skill binding to this protocol, verify: - [ ] **Monoidal**: Does your category have ⊗ and I? - [ ] **String diagrams**: Can morphisms be drawn as boxes-and-wires? - [ ] **Adhesive**: Do pushouts along monos exist and are van Kampen? - [ ] **Rules well-formed**: Is each rule a valid L ← K → R span? - [ ] **NACs specified**: Are negative application conditions defined? - [ ] **Confluence**: Are critical pairs joinable? - [ ] **Termination**: Is there a decreasing measure? - [ ] **GF(3) conserved**: Does trit(L) ≡ trit(R) mod 3? - [ ] **Soundness**: Is each rule derivable from equational axioms? - [ ] **Functors declared**: Are translations to other skills' categories given? ## 13. References ### Foundational - Joyal, A. & Street, R. (1991). *The geometry of tensor calculus, I.* Advances in Mathematics. - Selinger, P. (2010). *A survey of graphical languages for monoidal categories.* New Structures for Physics. - Mac Lane, S. (1963). *Natural associativity and commutativity.* Rice University Studies. ### Rewriting Theory - Lack, S. & Sobocinski, P. (2004). *Adhesive categories.* FOSSACS. - Ehrig, H. et al. (2006). *Fundamentals of Algebraic Graph Transformation.* Springer. - Plump, D. (1993). *Evaluation of functional expressions by hypergraph rewriting.* PhD thesis. - Corradini, A. et al. (2020). *On the essence of parallel independence for the double-pushout approach.* LNCS. ### String Diagrams - Coecke, B. & Duncan, R. (2011). *Interacting quantum observables: categorical algebra and diagrammatics.* NJP. - Backens, M. (2014). *The ZX-calculus is complete for stabilizer quantum mechanics.* NJP. - Bonchi, F., Sobocinski, P. & Zanasi, F. (2017). *Interacting Hopf algebras.* JPAL. ### Computation - Lafont, Y. (1990). *Interaction nets.* POPL. - Radul, A. & Sussman, G.J. (2009). *The art of the propagator.* MIT CSAIL TR. - Patterson, E. et al. (2022). *Categorical data structures for technical computing.* Compositionality. ### Game Theory - Hedges, J. (2016). *Towards compositional game theory.* PhD thesis, Oxford. - Ghani, N. et al. (2018). *Compositional game theory.* LICS. ## SDF Interleaving ### Primary Chapter: 7. Propagators String diagram rewriting = propagator network where cells are diagrams and propagators are rewrite rules. The merge operation is confluence. ### GF(3) Balanced Triad ``` sdf (+1) + string-diagram-rewriting-protocol (0) + zx-calculus (-1) = 0 mod 3 ``` **Skill Trit**: 0 (ERGODIC — transport/coordination) ### Secondary Chapters - Ch1: Flexibility through Abstraction — combinators as string diagram generators - Ch3: Variations on Arithmetic — generic dispatch as rule selection - Ch4: Pattern Matching — match finding in DPO - Ch9: Generic Procedures — multi-method = multi-sorted rewriting --- *"String diagrams are to monoidal categories what commutative diagrams are to categories."* — Peter Selinger