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.