Hypergraph rewriting and symmetric monoidal structure
String diagrams give a powerful graphical syntax for morphisms in
symmetric monoidal categories (SMCs). In addition to forming the
foundation of categorical quantum mechanics, they have recently found
applications in electrical circuits, parallelism, programming language
semantics, and control theory.
An important role in many such approaches is played by equational
theories, which can be oriented and treated as diagram rewrite rules.
In this talk, I'll give a new foundation for this form of rewriting by
interpreting diagrams combinatorially as typed hypergraphs and
establish the precise correspondence between diagram rewriting modulo
the laws of SMCs on the one hand and convex double pushout (DPO)
rewriting of hypergraphs, on the other. Furthermore, this SMC
rewriting arises as a restriction of a richer notion of rewriting
modulo the structure of a "hypergraph category", i.e. a category where
each object has a chosen special commutative Frobenius algebra. Hence,
by removing this restriction, we obtain a rewriting paradigm where
Frobenius laws come for free.
After giving the core framework, I'll also discuss some of the results
we have in developing the meta-theory of hypergraph rewriting for
SMCs, namely the construction of termination proofs via graph metrics
and strongly convex critical pair analysis.