Graph Rewrite Systems for Classical Structures in Dagger−Symmetric Monoidal Categories
Aleks Kissinger · 2008
This paper introduces several related graph rewrite systems derived from known identities on classical structures within a †-symmetric monoidal category. First, we develop a rewrite system based on a single classical structure, and use it to develop a proof of the so-called “spider-theorem, ” where a connected graph containing a single classical structure can be uniquely determined by the number of inputs and outputs (i.e. it can be rewritten as a graph resembling an n-legged spider). These spiders are shown to be the normal forms of graphs containing a single classical structure. Next, complementary classical structures are introduced, as well as a new rewrite system on graphs of red and green spiders. A proof of convergence is given for a limited two-colour rewrite system, as well as insights into ways to approach normalisation in a more powerful rewrite system. Acknowledgements I would first like to thank my supervisor Ross Duncan. It has been a privilege working with him for the past six months, as his knowledge and energy have been inspirational to me and pivotal in the creation of this work. To him I give my deepest thanks for the