Regular Calculi I: Graphical Regular Logic
Tslil Clingman, Brendan Fong, David I. Spivak

TL;DR
This paper introduces regular calculi, a structured graphical framework for regular logic relations, establishing a 2-dimensional adjunction between syntax and semantics in regular categories.
Contribution
It defines regular calculi as functors from regular logic syntax to posets, providing a graphical framework and proving a key adjunction with regular categories.
Findings
Defines regular calculi as structured functors for regular logic relations.
Introduces a graphical framework based on primitive moves of regular logic.
Establishes a syntax-semantics 2-dimensional adjunction to regular categories.
Abstract
What is ergonomic syntax for relations? In this first paper in a series of two, to answer the question we define regular calculi: a suitably structured functor from a category representing the syntax of regular logic to the category of posets, that takes each object to the poset of relations on that type. We introduce two major classes of examples, regular calculi corresponding to regular theories, and regular calculi corresponding to regular categories. For working in regular calculi, we present a graphical framework which takes as primitive the various moves of regular logic. Our main theorem for regular calculi is a syntax-semantics -dimensional adjunction to regular categories.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Advanced Algebra and Logic
