A Diagrammatic Algebra for Program Logics

TL;DR

The paper introduces tape diagrams as a diagrammatic calculus for rig categories, enabling explicit representation of data-flow (⊗) and control-flow (⊕) alongside iteration via uniform traces. It defines Kleene-Cartesian rig categories, where the ⊗ structure is cartesian and the ⊕ structure is Kleene, and develops a model theory with Lawvere-style semantics, including an example based on Rel. The main theoretical contributions are: (i) extending tape diagrams with uniform traces to capture iteration, (ii) establishing Kleene bicategories and showing a correspondence between typed Kleene algebras and Kleene bicategories, and (iii) proving that Kleene-Cartesian tape theories yield a freely generated framework that is expressive enough to encode imperative programs and form a Hoare-logical proof system. The framework provides a unified, diagrammatic, and algebraic approach to reasoning about imperative computation, with potential for formal verification and automated reasoning within a categorical setting.

Abstract

Tape diagrams provide a convenient notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$, where $\otimes$ distributes over $\oplus $. In this work, we extend tape diagrams with traces over $\oplus$ in order to deal with iteration in imperative programming languages. More precisely, we introduce Kleene-Cartesian bicategories, namely rig categories where the monoidal structure provided by $\otimes$ is a cartesian bicategory, while the one provided by $\oplus$ is what we name a Kleene bicategory. We show that the associated language of tape diagrams is expressive enough to deal with imperative programs and the corresponding laws provide a proof system that is at least as powerful as the one of Hoare logic.