Layered Monoidal Theories I: Diagrammatic Algebra and Applications

TL;DR

The mathematical foundations of layered monoidal theories are developed, as well as providing several instances of the approach, including digital and electrical circuits, quantum processes, chemical reactions, concurrent processes, and probability theory.

Abstract

We develop layered monoidal theories -- a generalisation of monoidal theories combining formal descriptions of a system at different levels of abstraction. Via their representation as string diagrams, monoidal theories provide a graphical formalism to reason algebraically about information flow in models across different fields of science. Layered monoidal theories allow mixing several monoidal theories (together with translations between them) within the same string diagram, while retaining mathematical precision and semantic interpretability. We develop the mathematical foundations of layered monoidal theories, as well as providing several instances of our approach, including digital and electrical circuits, quantum processes, chemical reactions, concurrent processes, and probability theory.

Figures (21)

• Figure 1: Left: an informal translation from a coarser language (English names) to a finer language (molecular graphs). Right: A formalisation of said translation as a term in a layered monoidal theory.
• Figure 2: Various features of layered monoidal theories.
• Figure 3: Rules for generating the basic terms of a layered signature
• Figure 4: 1-equations defining monoidal functors inside the fibres
• Figure 5: The structural 2-equations. Here $\mathsf{id}_T$ and $\mathsf{id}_S$ are the identity terms on the types $T$ and $S$, while $\mathsf{id}_{\varepsilon}$ is the identity term on $\varepsilon : \varepsilon$ obtained by the rule \ref{['term:ext-unit']}.

Theorems & Definitions (127)

• Definition 2.1: Monoidal signature
• Definition 2.2: Morphism of monoidal signatures
• Proposition 2.3
• proof
• Corollary 2.5
• proof
• Definition 2.6: Terms of a monoidal signature
• Definition 2.7: Monoidal theory
• Definition 2.8: Structural identities
• Definition 2.9: Term congruence