Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Layered Monoidal Theories

Leo Lobski

TL;DR

Layered Monoidal Theories develops a general graphical framework for describing systems across multiple levels of abstraction, unifying monoidal theories with translations between layers. It introduces three interrelated layered forms—opfibrational, fibrational, and deflational theories—and proves free-model constructions and adjunctions tying syntax to semantics via opfibrations, fibrations, and deflations. The approach is instantiated across diverse domains (digital/electrical circuits, ZX-calculus, CCS, chemistry retrosynthesis), demonstrating how functor boundaries and cobox/window concepts enable modular, cross-level reasoning and derivations. The work offers a modular, diagrammatic methodology to reason about layered descriptions of complex systems, enabling inter-layer translations, enriched 2-categorical reasoning, and formalization of domain-specific formalisms within a single cohesive theory.

Abstract

In the first part, we develop layered monoidal theories - a generalisation of monoidal theories combining descriptions of a system at several levels. Via their representation as string diagrams, monoidal theories provide a graphical syntax with a visually intuitive notions of information flow and composition. 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 define three flavours of layered monoidal theories, provide a recursively generated syntax for each, and construct a free-forgetful adjunction with respect to three closely related semantics: opfibrations, fibrations and deflations. We motivate the general theory by providing several examples from existing literature. In the second part, we develop a formal approach to retrosynthesis - the process of backwards reaction search in synthetic chemistry. Chemical processes are treated at three levels of abstraction: (1) (formal) reactions encode all chemically feasible combinatorial rearrangements of molecules, (2) reaction schemes encode transformations applicable to 'patches' of molecules (including the functional groups), and (3) disconnection rules encode local chemical rewrite rules applicable to a single bond or atom at a time. We show that the three levels are tightly linked: the reactions are generated by the reaction schemes, while there is a functorial translation from the disconnection rules to the reactions. Moreover, the translation from the disconnection rules to the reactions is shown to be sound, complete and universal - allowing one to treat the disconnection rules as a formal syntax with the semantics provided by the reactions. We tie together the two parts by providing a formalisation of retrosynthesis within a certain layered monoidal theory.

Layered Monoidal Theories

TL;DR

Layered Monoidal Theories develops a general graphical framework for describing systems across multiple levels of abstraction, unifying monoidal theories with translations between layers. It introduces three interrelated layered forms—opfibrational, fibrational, and deflational theories—and proves free-model constructions and adjunctions tying syntax to semantics via opfibrations, fibrations, and deflations. The approach is instantiated across diverse domains (digital/electrical circuits, ZX-calculus, CCS, chemistry retrosynthesis), demonstrating how functor boundaries and cobox/window concepts enable modular, cross-level reasoning and derivations. The work offers a modular, diagrammatic methodology to reason about layered descriptions of complex systems, enabling inter-layer translations, enriched 2-categorical reasoning, and formalization of domain-specific formalisms within a single cohesive theory.

Abstract

In the first part, we develop layered monoidal theories - a generalisation of monoidal theories combining descriptions of a system at several levels. Via their representation as string diagrams, monoidal theories provide a graphical syntax with a visually intuitive notions of information flow and composition. 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 define three flavours of layered monoidal theories, provide a recursively generated syntax for each, and construct a free-forgetful adjunction with respect to three closely related semantics: opfibrations, fibrations and deflations. We motivate the general theory by providing several examples from existing literature. In the second part, we develop a formal approach to retrosynthesis - the process of backwards reaction search in synthetic chemistry. Chemical processes are treated at three levels of abstraction: (1) (formal) reactions encode all chemically feasible combinatorial rearrangements of molecules, (2) reaction schemes encode transformations applicable to 'patches' of molecules (including the functional groups), and (3) disconnection rules encode local chemical rewrite rules applicable to a single bond or atom at a time. We show that the three levels are tightly linked: the reactions are generated by the reaction schemes, while there is a functorial translation from the disconnection rules to the reactions. Moreover, the translation from the disconnection rules to the reactions is shown to be sound, complete and universal - allowing one to treat the disconnection rules as a formal syntax with the semantics provided by the reactions. We tie together the two parts by providing a formalisation of retrosynthesis within a certain layered monoidal theory.

Paper Structure

This paper contains 62 sections, 61 theorems, 107 equations, 17 figures, 3 tables.

Table of Contents

  1. Layered string diagrams
  2. Introduction
  3. Layers of abstraction
  4. Layered monoidal theories
  5. A remark on terminology
  6. A motivating example: Digital circuits
  7. A case for 2-cells: Reasoning within the layered theories
  8. Structure of Part \ref{['part:layered']} of the thesis
  9. Summary of contributions
  10. Preliminaries
  11. Notation, conventions and terminology
  12. Categories
  13. Morphisms
  14. Functors
  15. 2-cells
  16. ...and 47 more sections

Key Result

Proposition 5

Any cloven opfibration $p: \mathcal{Y}\rightarrow \mathcal{X}$ induces a pseudofunctor $\mathcal{X}\rightarrow \mathbf{Cat}$ by sending each object to its fibre and each morphism $f$ to the functor $f^*$.

Figures (17)

  • Figure 1: An example translation from a coarser language (English names) to a finer language (molecular graphs).
  • Figure 2: Rules for generating the basic terms of a layered signature
  • Figure 3: 1-equations defining monoidal functors inside the fibres
  • Figure 4: 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']}.
  • Figure 5: Rules for generating the opfibrational terms
  • ...and 12 more figures

Theorems & Definitions (208)

  • Definition 1: Opcartesian map
  • Remark 2: Weakly opcartesian map
  • Definition 3: Opfibration
  • Remark 4: Preopfibration
  • Proposition 5
  • Remark 6
  • Definition 7: Fibration
  • Example 8: Family fibration
  • Definition 9: Morphism of (op)fibrations
  • Proposition 10
  • ...and 198 more