String Diagrams for Regular Logic (Extended Abstract)

Abstract

Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment. In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category FRg(T) on a set T. From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-category of contexts -- the 2-category of relations in FRg(T) -- to that of posets. Such functors assign to each context the set of formulas in that context, ordered by entailment. We refer to such a 2-functor as a regular calculus because it naturally gives rise to a graphical string diagram calculus in the spirit of Joyal and Street. We shall show that every natural category has an associated regular calculus, and conversely from every regular calculus one can construct a regular category.

In Proceedings ACT 2019, arXiv:2009.06334. Condensed version of arXiv:1812.05765

References in corpus (9)

• A Universal Construction for (Co)Relations
• A Compositional Framework for Reaction Networks
• Monoidal Grothendieck construction
• String diagrams for traced and compact categories are oriented 1-cobordisms
• A categorical approach to open and interconnected dynamical systems
• Knowledge Representation in Bicategories of Relations
• Decorated Corelations
• Graphical Conjunctive Queries
• Regular and relational categories: Revisiting 'Cartesian bicategories I'

Cited by in corpus (3)

• Deconstructing the Calculus of Relations with Tape Diagrams
• Compositional Separation of Control Flow and Data Flow
• On Doctrines and Cartesian Bicategories