Dec 14, 2010: Aleks Kissinger: Graph Rewriting and Monoidal Theories

December 14, 2010Graph Rewriting and Monoidal Theories
Room: Zi 5126Aleks Kissinger
12:30-13:30

Box-and-wire diagrams provide a powerful tool for reasoning about algebraic structures in monoidal categories. However, aside from the topological constructions of Joyal & Street, very little has been done to formalise these diagrams as concrete mathematical structures, subject to mechanised manipulation. We accomplish this by introducing a special kind of typed graph called an "open graph" and proving that the category of open graphs admits a well-behaved embedding into the "ambient" adhesive category of typed graphs. These results allow us to compose open graphs and do double-pushout graph rewriting much like in the standard categorical graph rewriting literature, but with the advantage that open graphs admit interpretation as morphisms in a traced symmetric monoidal category. We can formalise this connection by showing a certain construction on open graphs actually yields the *free* traced monoidal category over its collection of generators.