Hostname: page-component-74656f9884-c52kr Total loading time: 0 Render date: 2026-11-09T13:53:19.844Z Has data issue: false hasContentIssue false

Open-graphs and monoidal theories†

Published online by Cambridge University Press:  28 February 2013

LUCAS DIXON
Affiliation:
Google, New York, U.S.A. and University of Edinburgh, Edinburgh, United Kingdom Email: lucas.dixon@ed.ac.uk
ALEKS KISSINGER
Affiliation:
University of Oxford, Oxford, United Kingdom Email: aleks0@gmail.com
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

String diagrams are a powerful tool for reasoning about physical processes, logic circuits, tensor networks and many other compositional structures. The distinguishing feature of these diagrams is that edges need not be connected to vertices at both ends, and these unconnected ends can be interpreted as the inputs and outputs of a diagram. In this paper, we give a concrete construction for string diagrams using a special kind of typed graph called an open-graph. While the category of open-graphs is not itself adhesive, we introduce the notion of a selective adhesive functor, and show that such a functor embeds the category of open-graphs into the ambient adhesive category of typed graphs. Using this functor, the category of open-graphs inherits ‘enough adhesivity’ from the category of typed graphs to perform double-pushout (DPO) graph rewriting. A salient feature of our theory is that it ensures rewrite systems are ‘type safe’ in the sense that rewriting respects the inputs and outputs. This formalism lets us safely encode the interesting structure of a computational model, such as evaluation dynamics, with succinct, explicit rewrite rules, while the graphical representation absorbs many of the tedious details. Although topological formalisms exist for string diagrams, our construction is discrete and finitary, and enjoys decidable algorithms for composition and rewriting. We also show how open-graphs can be parameterised by graphical signatures, which are similar to the monoidal signatures of Joyal and Street, and define types for vertices in the diagrammatic language and constraints on how they can be connected. Using typed open-graphs, we can construct free symmetric monoidal categories, PROPs and more general monoidal theories. Thus, open-graphs give us a tool for mechanised reasoning in monoidal categories.

Information

Type
Paper
Copyright
Copyright © Cambridge University Press 2013