A Diagrammatic Basis for Computer Programming

TL;DR

This paper introduces tape diagrams as a graphical notation for rig categories with two monoidal products, enabling intuitive reasoning about imperative programs and program logic.

Contribution

It defines Kleene-Cartesian rig categories and demonstrates how tape diagrams effectively model imperative programming and logic.

Findings

Tape diagrams provide a graphical notation for rig categories.

Kleene-Cartesian rig categories combine Cartesian and Kleene bicategories.

Tape diagrams facilitate reasoning about imperative programs.

Abstract

Tape diagrams provide a convenient graphical notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$. In this work, we introduce Kleene-Cartesian rig categories, namely rig categories where $\otimes$ provides a Cartesian bicategory, while $\oplus$ a Kleene bicategory. We show that the associated tape diagrams can conveniently deal with imperative programs and various program logic.