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

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:

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

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

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

*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)

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)

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)

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