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:
- Matching: Find m : L → G (a mono/regular mono)
- 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
- 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:
+1generation rules often need SqPO (create copies)0transport rules use DPO (structure-preserving)-1verification 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):
- Enumerate all pairs of rules (rᵢ, rⱼ)
- For each pair, compute all overlaps via joint surjections
- Apply rᵢ and rⱼ to each overlap, yielding (H₁, H₂)
- 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:
- Generate (+1): Produce candidate diagrams
- Transport (0): Apply equational rewrites
- 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
| 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:
- C has pushouts along monomorphisms
- C has pullbacks
- 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:
- Confluent: d₁ ←* d *→ d₂ implies ∃d₃: d₁ → d₃ ← d₂
- Terminating: No infinite rewrite sequences
Knuth-Bendix completion: Given an equational theory E, attempt to generate a complete rewriting system R by:
- Orient equations into rules (using a termination ordering)
- Compute critical pairs
- Add new rules to resolve non-joinable critical pairs
- 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