| Summary: | <p>String diagrams are graphical representations of morphisms in various sorts of categories. The mathematical results which establish their soundness and completeness provide an elegant bridge between algebra and topology, equating a certain class of topological deformations to the equational theory of an algebraic structure. Beyond this conceptual appeal they also are practical tools to reason in the corresponding categories, making it easy to build intuition about the combinatorics of morphisms and efficiently communicate proofs to peers. Finally, they provide data structures to encode morphisms and manipulate them with computer programs such as proof assistants. Our contributions to the field explore three main directions.</p>
<p>First, we define a new class of string diagrams that we call sheet diagrams and prove their soundness and completeness for morphisms in free bimonoidal categories. This makes it possible to use string diagrams in situations involving two monoidal structures, one distributing over the other.</p>
<p>Second, the bulk of our work consists in studying how string diagram isotopy can be checked computationally. This is done by providing algorithms or hardness results for a particular class of decision problems, called word problems. Those word problems consist in determining whether two given diagrams can be related via a sequence of isotopy moves, whose nature depends on the algebraic structure at hand. We provide algorithms for the word problems for monoidal categories (or equivalently 2-categories or bicategories) and double categories. We also provide a hardness result for the word problem for braided monoidal categories, showing that this word problem is at least as hard as the unknotting problem, for which no polynomial-time solution is known to date.</p>
<p>Finally, we give a taste of how those techniques can be applied to real-world systems. We show how bimonoidal categories model the data transformation workflows offered by OpenRefine, an open source data wrangler focused on tabular data. This model has guided a refactoring of the architecture of the tool and suggests user interfaces to manipulate those workflows.</p>
|
|---|