Dieses Kapitel untersucht die historischen und theoretischen Grundlagen der Relationsrechnung und zeichnet ihre Entwicklung vom 19. Jahrhundert bis zu ihren modernen Anwendungen in der Programmlogik nach. Es beginnt mit einem Überblick über das Beziehungskalkül und betont seine Rolle bei der Entwicklung der Logik erster Ordnung und seine Ausweitung mit transitivem Abschluss. Das Kapitel vertieft sich dann in die Pionierarbeit Lawveres zur kategorischen Logik, indem es das Konzept der funktionalen Semantik und seine Anwendung auf die Beziehungstheorie einführt. Ein wesentlicher Beitrag ist die Einführung von Kleene-Bikategorien, die die Struktur der typisierten Kleene-Algebren erweitern und das Wesen des Kontrollflusses in der Programmlogik erfassen. Das Kapitel entwickelt das Konzept der Kleene-Kartesischen Rigg-Kategorien weiter, die sowohl Daten- als auch Kontrollfluss innerhalb eines einheitlichen kategorialen Rahmens integrieren. Tonbanddiagramme werden als visuelle und kompositorische Notation für diese Kategorien eingeführt und bieten eine intuitive Möglichkeit, Programmlogiken darzustellen und zu begründen. Das Kapitel veranschaulicht die Ausdruckskraft von Tonbanddiagrammen anhand von Beispielen, einschließlich der Axiomatisierung von Peanos natürlichen Zahlen und der Kodierung von Imperativprogrammen. Abschließend wird gezeigt, wie sich die Regeln der Hoare-Logik aus den Gesetzen der Kleene-Kartesischen Rigg-Kategorien ableiten lassen, wobei das Potenzial dieses Ansatzes für die Verifikation von Programmen und die logische Interpretation hervorgehoben wird.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
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 Hoare logic.
1 Introduction
The calculus of relations, originally introduced by De Morgan and Peirce in the late 19th century, is an ancestor of first order logic that has been revitalised by Tarski in 1941. With the dawn of program logics, the calculus of relations – extended with transitive closure – was early recognised [53] to play a key role.
Around the same time, Lawvere was pioneering categorical logic by introducing the concept of functorial semantics [47]. Given an algebraic theory T (in the sense of universal algebra, i.e., a signature \(\Sigma \) and a set of equations E), one can freely generate a Cartesian category \(\mathcal {L}_T\). Models, in the standard algebraic sense, correspond one-to-one with Cartesian functors F from \(\mathcal {L}_T\) to \(\textbf{Set}\), the category of sets and functions. More generally, models of the theory in any Cartesian category \(\textbf{C}\) are represented by Cartesian functors \(F: \mathcal {L}_T \rightarrow \textbf{C}\). However this approach fails if one tries to apply it to relational theories by choosing \(\textbf{C}\) as \(\textbf{Rel}\), the category of sets and relations, because the Cartesian product of sets is not the categorical product in \(\textbf{Rel}\).
Anzeige
A refinement of Lawvere’s method for relational structures has been recently proposed in [13, 15, 26]. Starting from a monoidal signature, one can freely generate a Cartesian bicategory [40] and define models as morphisms into \((\textbf{Rel}, \otimes , 1)\), the monoidal category of relations, where the monoidal product \(\otimes \) is the Cartesian product of sets. This framework captures regular theories, i.e., those involving the \(\{\exists , \wedge , \top \}\)-fragment of first order logic. More recently [10], this approach was extended to full first order logic by deriving negation from the interaction of Cartesian and linear bicategories [21].
In this paper, we extend the Cartesian bicategory framework in a different direction: program logics. In the last decades, there has been an explosion of program logics and many researchers felt the need for more systematic approaches. Our proposal is based on relational and categorical algebra. We propose tape diagrams as an “assembly language” for interpreting various program logics (Remark 3). While the inference rules for each of these logics are usually defined by the ingenuity of the researchers, in our approach such rules follow from the laws of Kleene-Cartesian rig categories. These laws arise from the interaction of canonical categorical structures on the category of sets and relations. Crucially, the same approach has lead to identify various categorical structures corresponding to various well-known logics (Figure 1).
Fig. 1.
Categorical structures correspond to logics.
An idea, originating at least from Bainbridge [4], is to model data flow using the Cartesian product of relations, \((\textbf{Rel}, \otimes , 1)\), and control flow using a different monoidal structure on relations: \((\textbf{Rel}, \oplus , 0)\). In this second structure, the monoidal product \(\oplus \) is the disjoint union of sets, which acts both as a coproduct and a product, hence, a biproduct. Both monoidal categories are traced [39]: the trace in \((\textbf{Rel}, \otimes , 1)\) represents feedback, while in \((\textbf{Rel}, \oplus , 0)\) –the focus of our work– it provides iteration [54].
Our first step is to extract from \((\textbf{Rel}, \oplus , 0)\) the categorical structures essential for modelling control flow, which we term Kleene bicategories. Essentially, a Kleene bicategory is a poset-enriched traced monoidal category where the monoidal product \(\oplus \) is a biproduct, and the induced natural comonoid [27] is right adjoint to the natural monoid. The trace must satisfy a posetal variant of the so-called uniformity condition [20, 33]. The term “Kleene” is justified because every Kleene bicategory forms a (typed) Kleene algebra in Kozen’s sense [41, 43] (Corollary 1), while any Kleene algebra canonically gives rise, through the biproduct completion [48], to a Kleene bicategory.
Anzeige
To model control and data flow within a unified categorical structure, we employ rig categories [46], categories equipped with two monoidal products, \(\oplus \) and \(\otimes \), where \(\otimes \) distributes over \(\oplus \). We define Kleene-Cartesian rig (kc rig) categories, where \(\oplus \) and \(\otimes \) exhibit the structures of Kleene and Cartesian bicategories, respectively. To construct the freely generated kc rig category (Theorem 2), we extend tape diagrams [11], a diagrammatic notation recently introduced for rig categories. Intuitively, tape diagrams are string diagrams [38] in which other string diagrams are nested: the inner diagrams model data flow, and the outer ones model control flow. On one hand, this offers an intuitive unified picture of Bainbridge’s idea; on the other it allows for visualising the laws of kc rig categories (Figures 2, 3 and 4) in a way that enlights several monoidal algebras occurring in different types of systems [3, 12, 14, 16, 18, 22, 28, 29, 36, 51, 56].
We then introduce Kleene-Cartesian theories and their models that, like in Lawvere’s approach, coincide with functors (Proposition 3). We illustrate an example of a Kleene-Cartesian theory which is not first order: Peano’s axiomatisation of natural numbers. We demonstrate how imperative programs and their logics [2, 24, 35, 44, 50] – even more sophisticated ones, like [7], where the interaction of data and control flow play a key role – can be encoded within Kleene-Cartesian tape diagrams. In particular, we show that the rules of Hoare logic follow from the laws of kc rig categories (Proposition 4). Finally, the framework is expressive enough to capture the positive fragment of the calculus of relations with transitive closure, which is the departure of our journey.
The full version of the paper is found in [9] which contains the missing proofs.
2 The calculus of relations
We commence by recalling the positive fragment of the calculus of relations with
reflexive and transitive closure (\(\textsf{CR}\)). Its syntax is given by the grammar on the left, where R is taken from a given set \(\Sigma \) of generating symbols. Beyond the usual relational composition ; , union \(\cup \), intersection \(\cap \) and their units \({id} \), \(\bot \) and \(\top \), the calculus features two unary operations:
$$\begin{aligned} E :\,\!:= \ & R \mid {id} \mid E;E \;\;\mid \end{aligned}$$
(1)
$$\begin{aligned} & E^{\dagger } \mid \top \mid E \cap E \mid \end{aligned}$$
(2)
$$\begin{aligned} & E^{*} \mid \bot \mid E \cup E \end{aligned}$$
(3)
the opposite \((\cdot )^{\dagger }\) and the reflexive and transitive closure \((\cdot )^{*}\). Composition and identities are defined, for sets X, Y, Z, and relations \(R\subseteq X \times Y\), \(S\subseteq Y\times Z\), as
the opposite as \(R^{\dagger }{\mathop {=}\limits ^{\tiny \text {def}}}\{(y,x)\mid (x,y)\in R\}\), while for \(R\subseteq X \times X\), its reflexive and transitive closure is \(R^{*}{\mathop {=}\limits ^{\tiny \text {def}}}\bigcup _{n\in \mathbb {N}}R^n\) where \(R^0{\mathop {=}\limits ^{\tiny \text {def}}}{id}_{X}\) and \(R^{n+1}{\mathop {=}\limits ^{\tiny \text {def}}}R;R^n\).
Its semantics, illustrated below, is defined wrt a relational interpretation\(\mathcal {I}\), that is, a set X together with a binary relation \(\rho (R)\subseteq X \times X\) for each \(R\in \Sigma \).
Two expressions \(E_1\), \(E_2\) are said to be equivalent, written \(E_1 \equiv _{\textsf{CR}} E_2\), iff \(\langle E_1\rangle _\mathcal {I}=\langle E_2\rangle _\mathcal {I}\) for all interpretations \(\mathcal {I}\). For instance, \((R^{*})^{\dagger } \equiv _{\textsf{CR}} (R^{\dagger })^{*}\). Inclusion, denoted by \(\le _{\textsf{CR}}\), is defined analogously by replacing \(=\) with \(\subseteq \). Axiomatisations and decidability of \(\equiv _{\textsf{CR}}\) have been studied focusing on several different fragments: see [52] and the references therein. Particularly interesting are the allegorical fragment, consisting of (1) and (2), and the Kleene fragment consisting of (1) and (3).
Our starting observation is that these two fragments arise from two different traced monoidal structures on \(\textbf{Rel}\), the category of sets and relations: \((\textbf{Rel}, \otimes , 1)\) and \((\textbf{Rel}, \oplus , 0)\). In the former, the monoidal product \(\otimes \) is given by the cartesian product of sets and, for relations \(R:X_1\rightarrow Y_1 \), \(S :X_2 \rightarrow Y_2\), \(R\otimes S :X_1 \otimes X_2 \rightarrow Y_1 \otimes Y_2\) is defined as
$$\begin{aligned} R \otimes S {\mathop {=}\limits ^{\tiny \text {def}}}\{(\,(x_1,x_2),\, (y_1,y_2)\,) \mid (x_1,y_1)\in R \text { and } (x_2,y_2)\in S \} \text { with unit }1{\mathop {=}\limits ^{\tiny \text {def}}}\{\bullet \}\text {.} \end{aligned}$$
In \((\textbf{Rel}, \oplus , 0)\), \(0{\mathop {=}\limits ^{\tiny \text {def}}}\{\}\), \(\oplus \) on sets is their disjoint union and \(R \oplus S :X_1\oplus X_2 \rightarrow Y_1\oplus Y_2\) is
$$\begin{aligned} R \oplus S {\mathop {=}\limits ^{\tiny \text {def}}}\{(\,(x_1,1),\,(y_1,1)\,) \mid (x_1,y_1)\in R \} \cup \{(\,(x_2,2),\,(y_2,2)\,) \mid (x_2,y_2)\in S \}\text {.} \end{aligned}$$
Here, we tag with 1 and 2 the elements of the disjoint union of two arbitrary sets.
For all sets X, the unique function
and the pairing \(\langle {id}_{X},{id}_{X}\rangle {\mathop {=}\limits ^{\tiny \text {def}}}\blacktriangleleft _{X} :X \rightarrow X \otimes X\) form a comonoid in \((\textbf{Rel}, \otimes , 1)\). Similarly the unique function
and the copairing \([{id}_{X},{id}_{X}]{\mathop {=}\limits ^{\tiny \text {def}}}\rhd _{X} :X\oplus X \rightarrow X\) form a monoid in \((\textbf{Rel}, \oplus , 0)\). By taking their opposite relations, we obtain in total the two (co)monoid structures illustrated below.
(4)
The black (co)monoids give to \((\textbf{Rel}, \otimes , 1)\) the structure of a Cartesian bicategory [19], while the white ones give to \((\textbf{Rel}, \oplus , 0)\) the structure of, what we named, a Kleene bicategory. These are illustrated in the next two sections.
3 Cartesian Bicategories
All bicategories considered in this paper are poset enriched symmetric monoidal categories: every homset carries a partial order \(\le \), and composition ; and monoidal product \(\odot \) are monotone. A poset enriched symmetric monoidal functor is a symmetric monoidal functor that preserves the order \(\le \). The notion of adjoint arrows, which will play a key role, amounts to the following: for \(f :X \rightarrow Y\) and \(g :Y \rightarrow X\), f is left adjoint to g, or g is right adjoint to f, written \(f \dashv g\), if \({id}_{X} \le f ; g\) and \(g ; f \le {id}_{Y}\). We extend such terminology to pairs of arrows: (a, b) is left adjoint to (c, d) iff \(a \dashv c\) and \(b \dashv b\).
All monoidal categories and functors considered throughout this paper are tacitly assumed to be strict [48], i.e. \((X\odot Y)\odot Z = X \odot (Y \odot Z)\) and \(I\odot X = X =X \odot I\) for all objects X, Y, Z. This is harmless: strictification [48] allows to transform any monoidal category into a strict one, enabling the sound use of string diagrams. In this and in the next section we will use the string diagrammatic notation for traced monoidal categories from [55]. The unfamiliar reader may check e.g. [9, Sec. 2]. In particular multiplication, unit, comultiplication and counit of the various (co)monoids, always tacitly assumed to be (co)commutative, will be drawn hereafter respectively, as
Definition 1
A Cartesian bicategory is a poset enriched symmetric monoidal category \((\textbf{C}, \otimes , 1)\) and, for every object X in \(\textbf{C}\), a monoid
and a comonoid
satisfying the usual coherence conditions (see e.g. [55, Table 4.7]) such that
1.
is left adjoint to
;
2. arrows \(f :X \rightarrow Y\) are lax comonoid morphisms:
and
;
3.
and
form special Frobenius algebras (see e.g. [45]);
A morphism of Cartesian bicategories is a poset enriched symmetric monoidal functor preserving monoids and comonoids.
The archetypal example of a Cartesian bicategory is \((\textbf{Rel},\otimes ,1)\) with
,
,
,
defined as in (4). Simple computations confirm that all the laws of Definition 1 are satisfied. The operations of \(\textsf{CR}\) in (2) can be defined in any Cartesian bicategory, as
(5)
for all objects X, Y and arrows \(f,g:X \rightarrow Y\). The reader can easily check that, in \(\textbf{Rel}\), these correspond to the intersection \(f\sqcap g\), the top relation \(X\times Y\) and the opposite relation \(f^{\dagger }\), respectively. From now on, we will depict a morphism \(f :X \rightarrow Y\) as
, and use
as syntactic sugar for \(f^{\dagger }\).
Proposition 1
In any Cartesian bicategory, the laws in Table 1 hold.
Table 1.
Derived laws in Cartesian bicategories.
Dummy
An arrow \(f :X \rightarrow Y\) is said to be single valued iff satisfies (SV) below, total iff satisfies (TOT), injective iff satisfies (INJ) and surjective iff satisfies (SUR).
Lemma 1
In a Cartesian bicategory, an arrow \(f :X \rightarrow Y\) is single valued iff (6), it is total iff (7), it is injective iff (8) and it is surjective iff (9).
Any Cartesian bicategory is self-dual compact closed and thus traced. Later on, to deal with tests in imperative programs we will use coreflexives, namely arrows \(f:X \rightarrow X\) such that \(f\le {id}_{X}\). In Cartesian bicategories, they enjoy several useful properties:
Lemma 2
In a Cartesian bicategory, the following hold:
1.
f is a coreflexive iff f is transitive (\(f;f\le f\)), symmetric (\(f^{\dagger }\le f\)) and single valued.
2.
Coreflexives \(X \rightarrow X\) are in bijective correspondece with arrows \(1\rightarrow X\).
3.
For all coreflexives \(f,g :X \rightarrow X\), \(f ; g = f \sqcap g\); Moreover, for \(f':1\rightarrow X\) corresponding to f and \(i:1\rightarrow X\), \(i\sqcap f'= i;f\).
4 Kleene Bicategories
Table 2.
Axioms of (Typed) Kleene Algebras
Dummy
Now, we introduce Kleene bicategories and show that their laws capture the complete axiomatisation of Kleene algebras from [41]. Recall that a category \(\textbf{C}\) is enriched over join-semilattices if every homset carries a join \(\sqcup \) semilattice with bottom \(\bot \) and composition ; distributes over it (see (10) and 11 in Table 2). A (typed) Kleene algebra [41, 43] is a category enriched over join-semilattices equipped with a Kleene star operator, namely a family of operations \((\cdot )^{*} :\textbf{C}[X,X] \rightarrow \textbf{C}[X,X]\) such that for all \(f:X\rightarrow X\), \(r:X \rightarrow Y\) and \(l:Y \rightarrow X\) the four laws in (12) hold.
Definition 2
A finite biproduct (shortly, fb) category with idempotent convolution is a poset enriched symmetric monoidal category \((\textbf{C}, \oplus , 0)\) and, for every object X in \(\textbf{C}\), a monoid
and a comonoid
satisfying the usual coherence conditions s.t.:
1.
is right adjoint to
;
2. arrows \(f :X \rightarrow Y\) are both monoid and comonoid morphisms: \(f;\lhd _{Y}= \lhd _{X};(f \oplus f)\),
, \(\rhd _{Y}; f= (f \oplus f); \rhd _{X}\) and
.
Remark 1
A finite biproduct category is defined as above but without the poset enrichment and the adjointness condition: \(0\) is both final and initial object and \(\oplus \) is both a categorical product and coproduct, i.e., a biproduct [27]. While any finite biproduct category is enriched over commutative monoids, the additional conditions in Definition 2 guarantee that this is enriched over join semilattices where \(\sqcup \) and \(\bot \) are defined for all objects X, Y and arrows \(f,g:X \rightarrow Y\) as on the left below.
(13)
The reader can easily check that \((\textbf{Rel},\oplus ,0)\) with \(\lhd _{X}\),
, \(\rhd _{X}\),
defined as in (4) is a finite biproduct category with idempotent convolution and that \(\sqcup \) and \(\bot \) give union and empty relation. Unfortunately, finite biproduct categories with idempotent convolution do not have enough structure to deal with \((\cdot )^{*}\): differently from Cartesian bicategories they are not necessarily traced. Such structure has to be explicitely added:
Definition 3
A Kleene bicategory\(\textbf{C}\) is both a finite biproduct category with idempotent convolution and a poset enriched traced monoidal category such that
1.
for all objects X, the trace
satisfies the axiom
;
2.
the trace is posetal uniform: for all \(f:S\oplus X \rightarrow S \oplus Y\) and \(g :T\oplus X \rightarrow T \oplus Y\),
(AU1)
if \(\exists r:S \rightarrow T\) such that \(f ; (r \oplus {id}_{Y}) \le (r \oplus {id}_{X}) ; g\), then
;
(AU2)
if \(\exists r:T \rightarrow S\) such that \((r \oplus {id}_{X}) ; f \le g ; (r \oplus {id}_{Y})\), then
.
A morphism of Kleene bicategory is a poset enriched symmetric monoidal functor preserving monoids, comonoids and traces.
The laws in (AU1) and (AU2) are the posetal extension of the uniformity condition for traces (see e.g. [33]). To the best of our knowledge, they have never been studied. Instead, the axioms in 1 already appeared in the literature (see e.g. [51]). Like in any finite biproduct category with trace (see e.g. [20]), in a Kleene bicategory one can define for each endomorphism \(f:X \rightarrow X\), a morphism \(f^{*}:X \rightarrow X\) as in (13). The distinguishing property of Kleene bicategories is that \((\cdot )^{*}\) is a Kleene star operator: see (12). Viceversa, any Kleene star operation gives rise to a trace satisfying the laws of Kleene bicategories.
Theorem 1
Let \(\textbf{C}\) be a fb category with idempotent convolution. \(\textbf{C}\) is a Kleene bicategory iff \(\textbf{C}\) has a Kleene-star operator.
Corollary 1
All Kleene bicategories are typed Kleene algebras.
The opposite does not hold: not all Kleene algebras are monoidal categories. Nevertheless, from a Kleene algebra, one can canonically build a Kleene bicategory by means of the matrix construction, aka biproduct completion [23, 48]. See [9, Sec. 6.3]
5 Rig Categories
We have seen that \(\textbf{Rel}\) carries two monoidal categories \((\textbf{Rel}, \otimes , 1)\) and \((\textbf{Rel}, \oplus , 0)\). The appropriate setting for studying their interaction is given by rig categories [37, 46].
Definition 4
A rig category is a category \(\textbf{C}\) with two symmetric monoidal structures \((\textbf{C}, \otimes , 1)\) and \((\textbf{C}, \oplus , 0)\) and natural isomorphisms
satisfying certain coherence axioms [46]. A rig category is said to be right strict when \(\lambda ^\bullet , \rho ^\bullet \) and \(\delta ^r\) are all identity natural isomorphisms. A right strict rig functor is a strict symmetric monoidal functor for both \(\otimes \) and \(\oplus \) preserving \(\delta ^l\).
A sesquistrict rig category is a functor \(H :\textbf{S} \rightarrow \textbf{C}\), where \(\textbf{S}\) is a discrete category and \(\textbf{C}\) is a right strict rig category, such that for all \(A \in \textbf{S}\)
is an identity morphism. Given \(H \!:\! \textbf{S} \!\rightarrow \! \textbf{C}\) and \(H' \!:\! \textbf{S}' \!\rightarrow \! \textbf{C}'\) two sesquistrict rig categories, a sesquistrict rig functor from H to \(H'\) is a pair \((\alpha \!:\! \textbf{S} \!\rightarrow \! \textbf{S}', \beta \!:\! \textbf{C} \!\rightarrow \! \textbf{C}')\), with \(\alpha \) a functor and \(\beta \) a strict rig functor, such that \(\alpha ; H' = H; \beta \).
Intuitively, a sesquistrict rig category is right strict and, partially (just for the selected class of objects \(\textbf{S}\)), left strict. For more details, we refer the reader to [11, Sec. 4].
From any rig category \(\textbf{C}\), one can construct its (right) strictification \(\overline{\textbf{C}}\) [37] and then embed \(ob(\textbf{C})\), the discrete category of the objects of \(\textbf{C}\), into \(\overline{\textbf{C}}\). The embedding \(ob(\textbf{C}) \rightarrow \overline{\textbf{C}}\) forms a sesquistrict category and it is equivalent (as a rig category) to the original \(\textbf{C}\) [11, Corollary 4.5]. Through the paper, when dealing with a rig category \(\textbf{C}\), we will often implicitly refer to the equivalent sesquistrict \(ob(\textbf{C}) \rightarrow \overline{\textbf{C}}\).
Hereafter, we write \(A,B,\dots \) for the elements of a fixed set \(\mathcal {S}\) and \(U,V, \dots \) for the words in \(\mathcal {S}^\star \). Given two words \(U,V\in \mathcal {S}^\star \), we write \(U \otimes V\), shortly UV, for their concatenation and 1 for the empty word. We use \(P,Q, \dots \) for words of words in \((\mathcal {S}^\star )^\star \) and we write \(P \oplus Q\) for their concatenation and 0 for the empty word of words. Beyond \(\oplus \), one can define \(\otimes \) on \((\mathcal {S}^\star )^\star \): for all \(P =U_0 \oplus \dots \oplus U_n\) and \(Q = V_0 \oplus \dots \oplus V_m\)
For instance, \((A\oplus B) \otimes (C \oplus D)\) is \((A \otimes C) \oplus (A \otimes D) \oplus (B \otimes C) \oplus (B \otimes D)\). One can readily see that elements in \((\mathcal {S}^\star )^\star \) are in bijective correspondence with non-commutative polynomials with variables in \(\mathcal {S}\). Consequently, we will call monomials the words in \(\mathcal {S}^\star \).
Given a set of sorts \(\mathcal {S}\), a monoidal signature is a tuple \((\mathcal {S},\Sigma , ar , coar )\) where \( ar \) and \( coar \) assign to each symbol \(s\in \Sigma \) an arity and a coarity in \(\mathcal {S}^\star \). A rig signature is the same but with arity and coarity in \((\mathcal {S}^\star )^\star \). An interpretation\(\mathcal {I}\) of a rig signature \((\mathcal {S},\Sigma , ar , coar )\) in a sesquistrict rig category \(H :\textbf{M} \rightarrow \textbf{D}\) is a pair of functions \((\alpha _{\mathcal {S}} :\mathcal {S}\rightarrow Ob(\textbf{M}), \alpha _\Sigma :\Sigma \rightarrow Ar(\textbf{D}))\) such that, for all \(s\in \Sigma \), \(\alpha _{\Sigma }(s)\) is an arrow having as domain and codomain \((\alpha _{\mathcal {S}};H)^\sharp ( ar (s))\) and \((\alpha _{\mathcal {S}};H)^\sharp ( coar (s))\). Here, \((\alpha _{\mathcal {S}};H)^\sharp \) stands for inductive extension of \(\alpha _{\mathcal {S}};H :\mathcal {S}\rightarrow Ob(\textbf{D})\) to \((\mathcal {S}^\star )^\star \).
Definition 5
Let \((\mathcal {S},\Sigma , ar , coar )\) (simply \(\Sigma \) for short) be a rig signature. A sesquistrict rig category \(H :\textbf{M} \rightarrow \textbf{D}\) is said to be freely generated by \(\Sigma \) if there is an interpretation \((\alpha _S,\alpha _\Sigma )\) of \(\Sigma \) in H such that for every sesquistrict rig category \(H' :\textbf{M}' \rightarrow \textbf{D}'\) and every interpretation \((\alpha _\mathcal {S}' :\mathcal {S}\rightarrow Ob(\textbf{M}'), \alpha _\Sigma ' :\Sigma \rightarrow Ar(\textbf{D}'))\) there exists a unique sesquistrict rig functor \((\alpha :\textbf{M} \rightarrow \textbf{M}', \beta :\textbf{D} \rightarrow \textbf{D}')\) such that \(\alpha _\mathcal {S}; \alpha = \alpha _\mathcal {S}'\) and \(\alpha _\Sigma ; \beta = \alpha _{\Sigma }'\).
6 Kleene-Cartesian Bicategories
We have seen that Cartesian bicategories provide enough structure for the allegorical fragment of \(\textsf{CR}\), while Kleene bicategories for its Kleene fragment. For the whole \(\textsf{CR}\), we make the Cartesian and Kleene bicategory structures interact as rig categories.
Definition 6
A Kleene-Cartesian rig category (shortly kc rig) is a poset enriched rig category \(\textbf{C}\) such that
1.
\((\textbf{C}, \oplus , 0)\) is a Kleene bicategory;
2.
\((\textbf{C}, \otimes , 1)\) is a Cartesian bicategory;
3.
the (co)monoids satisfy the following coherence conditions:
A morphism of kc rig-categories is a poset enriched rig functor that is a morphism of both Kleene and Cartesian bicategories.
The axioms in (15) rule the interaction of black and white (co)monoids. Recall that in Cartesian and Kleene bicategories, homsets carry respectively meet and join semilattices. In any kc rig category, they carry distributive lattices; also \((\cdot )^{\dagger }\) distributes over \(\oplus \), while \((\cdot )^{*}\) only distributes laxly over \(\otimes \). As expected \((\cdot ^{*})^{\dagger }= (\cdot ^{\dagger })^{*}\).
Any kc rig category is a typed Kleene algebra with converse [8, 17].
We have already seen that \((\textbf{Rel},\oplus , 0)\) is a Kleene bicategory and \((\textbf{Rel},\otimes , 1)\) is a Cartesian bicategory. To conclude that \(\textbf{Rel}\) is a kc rig category, it is enough to check the coherence conditions of the two (co)monoids defined in (4).
6.1 Kleene-Cartesian Tape Diagrams
We identify the kc rig category freely generated by a rig signature \((\mathcal {S},\Sigma )\). This is described as Kleene-Cartesian tape diagrams, which provide a syntax for kc rig categories. These are strictly more expressive than the calculus of relations: thanks to the monoidal product \(\otimes \), they can deal with \(n\)-ary function symbols, e.g. “add” in Equation 22, data flow and relational Hoare logic (Remark 3).
Thanks to Theorem 4.9 in [11], we can restrict, without loss of generality, to the simpler case where \(\Sigma \) is just a monoidal signature. Our work extends [11, Section 7] that identifies a freely generated fb-cb rig category, shortly a kc rig category without traces (\(\oplus \) is just a fb category with idempotent convolution).
As explained in Section 5, we can consider the sesquistrict rig categories having as sets of objects \((\mathcal {S}^\star )^\star \). For arrows, consider the following two-layer grammar
(16)
where \(s \in \Sigma \), \(A,B \in \mathcal {S}\) and \(U,V \in \mathcal {S}^\star \). The terms of the first row, called circuits, intuitively represent arrows of a Cartesian bicategory. The terms of the second row, called tapes, represent arrows of a Kleene bicategory. As expected, we only consider those terms to which is possible to associate source and target objects: the reader may check the simple type system in [9, Table 1]. Constants and operations in (16) can be extended to arbitrary polynomials in \((\mathcal {S}^\star )^\star \). For instance,
is inductively defined as
and
. For the other definitions see [11].
Particularly interesting is the fact that one can define \(\otimes \) on tapes: for \(\mathfrak {t}_1 :P \rightarrow Q\), \(\mathfrak {t}_2 :R \rightarrow S\), \(\mathfrak {t}_1 \otimes \mathfrak {t}_2 {\mathop {=}\limits ^{\tiny \text {def}}}\textsf{L}_{P}({\mathfrak {t}_2}) ; \textsf{R}_{S}({\mathfrak {t}_1}) \) where \(\textsf{L}_{P}({\cdot })\), \(\textsf{R}_{S}({\cdot })\) are the left and right whiskerings that can be defined by extending [11, Def 5.7] with an extra case for the trace:
and
. Left distributors \(\delta ^l_{P,Q,R} :P \otimes (Q\oplus R) \rightarrow (P \otimes Q) \oplus (P\otimes R)\) and \(\otimes \)-symmetries
are defined as in [11, Table 4]. The (co)monoids of \(\otimes \) as in [11, (20),(21)].
Next, we impose the laws of kc rig categories on tapes. However, this should be done carefully, in order to properly tackle the two uniformity laws (AU1) and (AU2) which are implications and not (in)equalities. Let \(\mathbb {I}\) be a a set of pairs
of tapes with the same domain and codomain. We define \(\,{\le }_{{\mathbb {I}}}\,\) to be the set generated by the following inference system (where \(\mathfrak {t}\,{\le }_{{\mathbb {I}}}\,\mathfrak {s}\) is a shorthand for \((\mathfrak {t},\mathfrak {s})\in \,{\le }_{{\mathbb {I}}}\,\)).
The first six laws ensure that \(\,{\le }_{{\mathbb {I}}}\,\) is a precongruence (w.r.t. ; , \(\oplus \) and \(\otimes \)) containing \(\mathbb {I}\). The last two rules force the uniformity laws: observe that, while in (AU1) and (AU2) the same arrow r occurs in both the left and the right- hand-side of the premises, here r is replaced by two different but related tapes \(\mathfrak {s}_1\) and \(\mathfrak {s}_2\). This technicality is needed to guarantee uniformity in the category resulting from the following construction.
We take \(\mathbb{K}\mathbb{C}\) to be the set of all pairs of tapes containing the axioms in Table 71 and define \(\le _{\mathbb{K}\mathbb{C}}\) according to (17). We fix \(\sim _{\mathbb{K}\mathbb{C}} {\mathop {=}\limits ^{\tiny \text {def}}}\le _{\mathbb{K}\mathbb{C}} \cap \ge _{\mathbb{K}\mathbb{C}}\). With these definitions we can construct the category of Kleene-Cartesian tapes \(\textbf{KCT}_{\Sigma }\): objects are polynomials in \((\mathcal {S}^\star )^\star \) with \(\oplus \) and \(\otimes \) defined as in (14); arrows are \(\sim _\mathbb{K}\mathbb{C}\)-equivalence classes of tapes; every homset \(\textbf{KCT}_{\Sigma }[P,Q]\) is ordered by \(\,{\le }_{{\mathbb{K}\mathbb{C}}}\,\). The construction of \(\textbf{KCT}_{\Sigma }\) gives rise to a sesquistrict kc rig category. More importantly, \(\textbf{KCT}_{\Sigma }\) is the freely generated one.
Theorem 2
\(\textbf{KCT}_{\Sigma }\) is the free sesquistrict kc rig category generated by \((\mathcal {S}, \Sigma )\).
In [11], it is shown that a key feature of tapes is that they can be drawn nicely in 2 dimensions despite representing arrows of rig categories. Indeed, both circuits and tapes can be drawn as string diagrams. Note however that inside tapes, there are string diagrams. Thus, the grammar in (16) can be graphically rendered as follows.
The identity \({id}_{0}\) is rendered as the empty tape
, while \({id}_{1}\) is
: a tape filled with the empty circuit. For a monomial \(U \!=\! A_1\dots A_n\), \({id}_{U}\) is depicted as a tape containing n wires labelled by \(A_i\). For instance, \({id}_{AB}\) is rendered as
. When clear from the context, we will simply represent it as a single wire
with the appropriate label. Similarly, for a polynomial
, \({id}_{P}\) is obtained as a vertical composition of tapes, as illustrated below on the left.
The diagonal \(\lhd _{U} :U \!\rightarrow \! U \oplus U\) is represented as a splitting of tapes, while the bang
is a tape closed on its right boundary. Codiagonals and cobangs are represented in the same way but mirrored along the y-axis. Exploiting the usual coherence conditions e.g. in [55, Table 4.7], we can construct (co)diagonals and (co)bangs for arbitrary polynomials. For example, \(\rhd _{A\oplus B \oplus C}\) and
are depicted as the second and third diagrams above.
The copier
is represented as a splitting of wires, while the discharger
is a wire closed on the right. From the coherence laws in (15), one can build (co)copiers and (co)dischargers for arbitrary polynomials. For instance,
and
are drawn as the last two diagrams above. For an arbitrary tape diagram \(\mathfrak {t}:P \rightarrow Q\) we write
.
The graphical representation embodies several axioms such as those of monoidal categories and several axioms for traces. Those axioms which are not implicit in the graphical representation are illustrated in Figures 2 and 3. Figure 4 illustrates the uniformity laws in the form of tape diagrams.
Fig. 2.
Tape axioms for Kleene bicategory
Fig. 3.
Axioms of Cartesian bicategories
Fig. 4.
Posetal uniformity axioms in tape diagrams.
6.2 Kleene-Cartesian Theories and Functorial Semantics
A Kleene-Cartesian theory, shortly kc theory, is a pair \((\Sigma , \mathbb {I})\) where \(\Sigma \) is a monoidal signature and \(\mathbb {I}\) is a set of pairs \((\mathfrak {t}_1, \mathfrak {t}_2)\) of tapes with same domain and codomain. Hereafter, we think of each pair \((\mathfrak {t}_1, \mathfrak {t}_2)\) as an inequation \(\mathfrak {t}_1 \le \mathfrak {t}_2\), but the results that we develop in this section trivially hold also for equations: it is enough to add in \(\mathbb {I}\) a pair \((\mathfrak {t}_2, \mathfrak {t}_1)\) for each \((\mathfrak {t}_1, \mathfrak {t}_2) \in \mathbb {I}\). Hereafter we always keep implicit \(\mathbb{K}\mathbb{C}\) and we write \(\,{\le }_{{\mathbb {I}}}\,\) for \(\,{\le }_{\mathbb{K}\mathbb{C}\cup \mathbb {I}}\,\) where the latter is defined as in (17). We fix \(\sim _{\mathbb {I}}{\mathop {=}\limits ^{\tiny \text {def}}}\le _{\mathbb {I}}\cap \ge _{\mathbb {I}}\).
Recall that an interpretation \(\mathcal {I}=(\alpha _{\mathcal {S}}, \alpha _{\Sigma })\) of a monoidal signature \((\mathcal {S},\Sigma )\) in a sesquistrict rig category \(\textbf{C}\) consists of \(\alpha _{\mathcal {S}}:\mathcal {S}\rightarrow Ob(\textbf{C})\) and \(\alpha _{\Sigma }:\Sigma \rightarrow Ar(\textbf{C})\). Whenever \(\textbf{C}\) is a kc rig category, \(\mathcal {I}\) gives rises uniquely, by freeness of \(\textbf{KCT}_{\Sigma }\), to a morphism of kc rig categories \( \llbracket \cdot \rrbracket _{\mathcal {I}} :\textbf{KCT}_{\Sigma }\rightarrow \textbf{C}\) defined as:
We say that an intepretation \(\mathcal {I}\) of \(\Sigma \) is a model of the theory\((\Sigma , \mathbb {I})\) whenever \( \llbracket \cdot \rrbracket _{\mathcal {I}}\) preserves \(\,{\le }_{{\mathbb {I}}}\,\): if \(\mathfrak {t}_1 \,{\le }_{{\mathbb {I}}}\,\mathfrak {t}_2\), then \( \llbracket \mathfrak {t}_1 \rrbracket _{\mathcal {I}} \) is below \( \llbracket \mathfrak {t}_2 \rrbracket _{\mathcal {I}}\) in \(\textbf{C}\). Models enjoy a beautiful characterisation provided by Proposition 3 below. Let \(\textbf{KCT}_{\Sigma ,\mathbb {I}}\) be the category having the same objects as \(\textbf{KCT}_{\Sigma }\) and arrows \(\sim _{\mathbb {I}}\)-equivalence classes of arrows of \(\textbf{KCT}_{\Sigma }\) ordered by \(\,{\le }_{{\mathbb {I}}}\,\). Since \(\textbf{KCT}_{\Sigma }\) is a kc rig category, then also \(\textbf{KCT}_{\Sigma ,\mathbb {I}}\) is so.
Proposition 3
Let \((\Sigma , \mathbb {I})\) be a kc tape theory and \(\textbf{C}\) a sesquistrict kc rig category. Models of \((\Sigma , \mathbb {I})\) are in bijective correspondence with morphisms of sesquistrict kc rig categories from \(\textbf{KCT}_{\Sigma ,\mathbb {I}}\) to \(\textbf{C}\).
Example 1 (Functions)
[Functions] Let \(\mathcal {S}\) be a set of sorts and \(\Sigma {\mathop {=}\limits ^{\tiny \text {def}}}\{f:U \rightarrow A\}\) for some \(A\in \mathcal {S}\) and \(U\in S^\star \). Let \(\mathbb {I}\) be the set of the two equalities in (18). An interpretation \(\mathcal {I}\) of \((\mathcal {S},\Sigma )\) in \(\textbf{Rel}\), consists of a set \(\alpha _\mathcal {S}(A_i)\) for each \(A_i\in \mathcal {S}\) and a relation \(\alpha _\Sigma (f) \subseteq \alpha _{\mathcal {S}}^\sharp (U) \times \alpha _{\mathcal {S}}(A)\). \(\mathcal {I}\) is a model of \((\Sigma ,\mathbb {I})\) iff \(\alpha _\Sigma (f)\) is single valued (SV) and total (TOT), i.e., a function.
(18)
Example 2 (KAT)
Let \(\mathcal {P}\) be a set of predicate symbols \(R:U \rightarrow 1\) for \(U\in \mathcal {S}^\star \). Take \(\bar{\mathcal {P}}{\mathop {=}\limits ^{\tiny \text {def}}}\{\bar{R}:U \rightarrow 1\mid R\in \mathcal {P}\}\) and \(\Sigma {\mathop {=}\limits ^{\tiny \text {def}}}\mathcal {P}\cup \bar{\mathcal {P}}\). Let \(\mathbb {I}\) be the set of equalities below.
An interpretation \(\mathcal {I}\) of \((\mathcal {S},\Sigma )\) in \(\textbf{Rel}\) is a set \(\alpha _\mathcal {S}(A_i)\) for each \(A_i\in \mathcal {S}\) together with predicates \(R \subseteq X\times 1\) and \(\bar{R} \subseteq X\times 1\) for \(X{\mathop {=}\limits ^{\tiny \text {def}}}\alpha _\mathcal {S}^\sharp (U)\). \(\mathcal {I}\) is a model iff, for all \(R\), \(\bar{R}\) is its set-theoretic complement: by (13) and (5), the equalities above asserts that \(R \cup \bar{R}=X\) and \(R \cap \bar{R}=\{\}\). By Proposition 2, \(\textbf{KCT}_{\Sigma ,\mathbb {I}}[U,1]\) carries a distributive lattice and even a Boolean algebra when defining \(\lnot P\), for all \(P:U \rightarrow 1\) as follows.
Consider the set \(C\) that contains, for each \(P :U \rightarrow 1\), the associated coreflexive:
(21)
Again coreflexives form a Boolean algebra \((C,\sqcup , \mathbin {;}, \lnot , \bot , {id} )\) where composition \(\mathbin {;}\) acts as \(\sqcap \): see Lemma 2.3. Moreover, by Corollary 1, \(\textbf{KCT}_{\Sigma ,\mathbb {I}}[U,U]\) is a Kleene algebra. Thus \((\textbf{KCT}_{\Sigma ,\mathbb {I}}[U,U], C, \sqcup , \mathbin {;}, (\cdot )^{*}, \bot , {id} , \lnot )\) is a Kleene algebra with tests [42].
Remark 2
Recall \(\textsf{CR}\) from Section 2. The set \(\Sigma \) of generating symbols corresponds to a monoidal signature where \(\mathcal {S}=\{A\}\) and each symbol has both arity and coarity A. A relational interpretation of \(\textsf{CR}\) is exactly an interpretation \(\mathcal {I}\) of the monoidal signature \((\mathcal {S},\Sigma )\) into \(\textbf{Rel}\). One can define an inductive encoding \(\mathcal {E}(\cdot )\) from \(\textsf{CR}\) to \(\textbf{KCT}_{\Sigma }\) by using (5) and (13). A simple inductive argument confirms that, for all interpretations \(\mathcal {I}\) and expressions \(E\in \textsf{CR}\), \(\langle E\rangle _\mathcal {I} = \llbracket \mathcal {E}(E) \rrbracket _{\mathcal {I}}\). Thus, if \(\mathcal {E}(E_1)\le _{\mathbb{K}\mathbb{C}}\mathcal {E}(E_2)\), then \(E_1 \le _{\textsf{CR}} E_2\).
7 The Kleene-Cartesian Theory of Peano
In this section we illustrate a further example of kc theory: Peano’s axiomatisation of natural numbers. Recall that such axiomatisation is not a first order theory [32].
We commence by fixing the signature: \(\mathcal {S}{\mathop {=}\limits ^{\tiny \text {def}}}\{A\}\) and
. An interpretation of \(\Sigma \) in \(\textbf{Rel}\) consists of a set X (i.e., \(\alpha _\mathcal {S}(A)\)), a relation \(0 \subseteq 1 \times X\) (i.e.,
) and a relation \(s\subseteq X \times X\) (i.e.,
).
Fig. 5.
The Kleene-Cartesian theory of Peano.
The set of axioms \(\mathbb {P}\) consists of those in Figure 5.
From a universal-algebraic perspective, natural numbers are the smallest set X such that X is isomorphic to \(X \oplus 1\). The two leftmost axioms in Figure 5 force \([s,0] {\mathop {=}\limits ^{\tiny \text {def}}}(s \oplus 0) ; \rhd _{X}\) to be an isomorphism of type \(X \oplus 1\rightarrow X\): (iso-1) states that \([s,0]^{\dagger }\mathbin {;}[s,0] = {id}_{X}\); (iso-2) that \([s,0]\mathbin {;}[s,0]^{\dagger }= {id}_{X \oplus 1}\); the rightmost the fact that it is the smallest: i.e. \(X \subseteq 0 \mathbin {;}s^* :1\rightarrow X\). One can similarly obtain any algebraic data type.
We illustrate that \((\Sigma , \mathbb {P})\) is equivalent to Peano’s axiomatisation of natural numbers. Possibly, the most interesting axiom is the principle of induction: (ind-princ) in Figure 6. This follows easily from posetal uniformity and (ind).
Theorem 3 (Principle of Induction)
Let \((\Pi , \mathbb {Q})\) be a kc theory, such that \(\Sigma \subseteq \Pi \) and \(\mathbb {P}\subseteq \mathbb {Q}\). For all \(P:1\rightarrow A\) in \(\textbf{KCT}_{\Pi ,\mathbb {Q}}\), (ind-princ) in Figure 6 holds
Proof
Observe that the following holds:
Thus, by (AU2) the inclusion below holds and the derivation concludes the proof.
The other Peano’s axioms state that 0 is a natural number, s is an injective function and that 0 is not the successor of any natural number. These are illustrated by means of tapes in Figure 6, where we use the characterisation of total, single valued and injective relations provided by Lemma 1. Observe that (\(\bot \)) states that \(\{x\in X \mid (x,0)\in s \} \subseteq \emptyset \).
In [25], Dedekind showed that any two models of Peano’s axioms are isomorphic, and thus any model of \((\Sigma , \mathbb {P})\) is isomorphic to the one on natural numbers.
Fig. 6.
Peano’s theory of the natural numbers.
To give to the reader a taste of how one can program with tapes, we now illustrate how to start to encode arithmetic within \((\Sigma , \mathbb {P})\). The tape for addition is illustrated on the right. Such tape can be thought as a simple imperative program:
(22)
add(x,y) = while (x>0) { x:=x-1; y:=y+1 }; return y
The variable x corresponds to the top wire in (22), while y to the bottom one. At any iteration, the program checks whether x is 0, in which case it returns y, or the successor of some number, in which case x takes such number, while y takes its own successor.
In [9, Lemma 10.3] we show that (22) satisfies the usual inductive definition of addition, namely:
While, it is straightforward that
terminates on all possible inputs, it is interesting to see how this can be proved within the kc theory \((\Sigma ,\mathbb {P})\).
Lemma 4
The tape
is total, i.e.
.
Proof
First observe that the following holds:
Then, by (AU1), the inequality below holds and the derivation concludes the proof.
8 Diagrammatic Hoare Logic
We now illustrate how tape diagrams can provide a comfortable setting to reason about imperative programs. For the sake of generality, we avoid to fix basic types and operations and, rather, we work parametrically with respect to a triple \((\mathcal {S},\mathcal {F},\mathcal {P})\): \(\mathcal {S}\) is a set of sorts, representing basic types; \(\mathcal {F}\) is a set of function symbols, equipped with an arity in \(\mathcal {S}^*\) and a coarity in \(\mathcal {S}\); \(\mathcal {P}\) is a set of predicate symbols equipped just with an arity in \(\mathcal {S}^*\). The coarity of predicates is fixed to be 1.
We take the signature \(\Sigma {\mathop {=}\limits ^{\tiny \text {def}}}\mathcal {F} \cup \mathcal {P} \cup \bar{\mathcal {P}}\) where \(\bar{\mathcal {P}}\) is as in Example 2. The set \(\mathbb {I}\) contains, for all \(f:U \rightarrow A\) in \(\mathcal {F}\), the axioms in (18) and, for each \(R:U \rightarrow 1\) in \(\mathcal {P}\), those in (19). One may add to \(\mathbb {I}\) other axioms, e.g., those of \(\mathbb {P}\) in Section 7.
We consider terms generated by the following grammar
$$ \begin{array}{rcl} e & ::=& x \mid f(e_{1}, \ldots , e_{n})\\ P & ::=& R(e_1, \dots , e_n) \mid \bar{R}(e_1, \dots , e_n) \mid \top \mid \bot \mid P \vee P \mid P \wedge P \\ C & ::=& \textsf{abort} \mid \textsf{skip} \mid \mathop {\textsf{if}} P \mathop {\textsf{then}} C \mathop {\textsf{else}} D \mid \mathop {\textsf{while}} P \mathop {\textsf{do}} C \mid C ; D \mid x :==e \end{array} $$
where \(f\in \mathcal {F}\), \(R\in \mathcal {P}\) and x is taken from a fixed set of variables. As usual, e are expressions, P predicates and C commands. Negation of predicates can be expressed as in (20). In order to encode terms into diagrams, we need to make copying and discarding of variables explicit; we thus define a simple type systems with judgement of the form
$$\begin{aligned} \Gamma \vdash e :A \qquad \Gamma \vdash P :1 \qquad \Gamma \vdash C \end{aligned}$$
where A is a sort in \(\mathcal {S}\) and \(\Gamma \) is a typing context, i.e., an ordered sequence \(x_1:A_1, \dots x_n :A_n\), where all the \(x_i\) are distinct variables and \(A_i \in \mathcal {S}\). The type system is in Table 4.
Table 4.
Type system for expressions, predicates and commands.
Dummy
Table 5.
Encoding of expressions, predicates and commands into diagrams.
Dummy
The encoding of terms into diagrams, presented in Table 5, is defined inductively on the typing rules. For instance, in the encoding of the assignment \(\Gamma \vdash x :==e\), the context is \(\Gamma = \Gamma ', x :A, \Delta '\), according to the typing rule (Assn).
The encoding \(\mathcal {E}(\cdot )\) maps well typed expressions \(\Gamma \vdash e :A\), predicates \(\Gamma \vdash P :1\) and commands \(\Gamma \vdash C \) into, respectively, diagrams of the following types
where for \(\Gamma =x_1:A_1, \dots , x_n :A_n\), we fix \(\mathcal {E}(\Gamma ) {\mathop {=}\limits ^{\tiny \text {def}}}A_1 \otimes \dots \otimes A_n\). In the encoding of expressions and predicates, we use
to copy n times the content of variables in \(\Gamma \). Formally,
is defined as
and
. Guards in commands are encoded using c(P), defined in (21). The encoding of commands is pretty standard, see e.g. [42], with the only exception of assignment that is depicted as the diagram on the right where, for the sake of readability, we label wires directly with the typing contexts rather than their encodings. Note that, in this case, \(\mathcal {E}(\cdot )\) exploits the structure of Cartesian bicategories to properly take into account data flow. For instance, for \(\Gamma =x:A,y:A,z:A\), the encoding maps \(\Gamma \vdash x :==z ; y:==z\) and \(\Gamma \vdash y :==z ; x :==z\) into the same tape.
The following lemma illustrates the interaction of substitutions with the encoding.
Lemma 5
Let \(\Gamma ' = \Gamma , x:A, \Delta \). If \(\Gamma ' \vdash P:1\) and \(\Gamma ' \vdash t:A\), then
Hoare logic [35] is one of the most influential languages to reason about imperative programs. Its rules –in the version appearing in [57]– are in Figure 6. In partial correctness, a triple \(\{P\}C\{Q\}\) asserts that if, starting from a state satisfying the precondition P, the execution of C terminates, then the resulting state satisfies the postcondition Q.
The following result shows that
Table 6.
Rules of Hoare logic
Dummy
Proposition 4
If \(\{P\}C\{Q\}\) is derivable as in Figure 6, then \(\mathcal {E}(P)^{\dagger } \mathbin {;}\mathcal {E}(C) \le _{\mathbb {I}} \mathcal {E}(Q)^{\dagger }\).
Proof
By induction on the rules in Table 6. We illustrate only two cases: the others can be found in the proof of [9, Proposition 11.5]. For (\(\textsf{assn}\)), observe that by Lemma 5, \(\mathcal {E}(P[e/x])^{\dagger } \mathbin {;}\mathcal {E}(x :==e)\) is the leftmost diagram below. Thus:
For (\(\textsf{while}\)), observe that the following holds:
Then, by (AU2), the inequality below holds and the derivation concludes the proof.
Remark 3 (Other Program Logics)
The above result proves a syntactic correspondence amongst the deduction systems in Table 6 and \(\le _{\mathbb {I}}\). To prove such result we did not need to explicitly give the semantics of command or prove that our encoding preserves the semantics. However, assuming that, for a fixed interpretation \(\mathcal {I}\), \( \llbracket \mathcal {E}(\Gamma \vdash C) \rrbracket _{\mathcal {I}} \) is the intended relational semantics of a command C, one can immediately see that the correspondence at the semantic level –illustrated below on the top-left corner– holds.
The other correspondences concern other logics: \(\text {[}P\text {]} C \text {[}Q\text {]}\) are triples of incorrectness logic [50], \(\langle \!\langle P \rangle \!\rangle C \langle \!\langle Q \rangle \!\rangle \) of sufficient incorrectness [2] and \((P)C(Q)\) of necessary [24]. Interestingly, quadruples of relational Hoare logics [7] can be characterised as
We introduced Kleene bicategories and proved that they form Kleene algebras in Kozen’s sense (Corollary 1). By examining their interaction with Cartesian bicategories, we developed Kleene-Cartesian rig categories and characterised the free one as tape diagrams (Theorem 2). Furthermore, we showed that tape diagrams can express Kleene algebra with tests [42], Peano’s natural numbers, and various program logics. We proved that the rules of Hoare logic follow from the structure of kc rig categories (Proposition 4).
Regarding Kleene bicategories, while we are not the first to explore uniform traces over biproduct categories (see, e.g., [20]), the use of posetal uniformity and the correspondence with Kozen’s axioms are, to the best of our knowledge, novel contributions.
Computer scientists usually find control flow and data flow graphs intuitive. Tapes diagram combine the two in a single diagrammatic representation equipped with compositional semantics. Another key distinction of tape diagrams, compared to other relational or categorical approaches to program logics (e.g., [1, 5, 31, 34, 44, 49]), lies in the \(\otimes \) monoidal and rig structures, which enable direct representation of product programs [6]. Through tape (in)equalities and \(\otimes \), it becomes easy to express complex properties like non-interference [30]. Exploring how such properties can be proved by the laws of kc rig categories remains a promising direction for future research.
Table 7.
Axioms for Kleene-Cartesian Tapes. For each axiom \(l=r\) in top-left corner, the set \(\mathbb{K}\mathbb{C}\) contains the pairs (l, r) and (r, l) where \(\odot \) and \(I\) are replaced by \(\oplus \) and \(0\) and the pairs \((\overline{\underline{\; l \;}},\overline{\underline{\; r \;}})\) and \((\overline{\underline{\; r \;}},\overline{\underline{\; l \;}})\) where \(\odot \) and \(I\) are replaced by \(\otimes \) and \(1\). In the rest, for each \(l\le r\)\(\mathbb{K}\mathbb{C}\) contains a pair (l, r) and, additionally, the pair (r, l) in case of an axiom \(l=r\).
Dummy
Acknowledgements
The authors would like to acknowledge Alessio Santamaria, Chad Nester and the students of the ACT school 2022 for several useful discussions at early stage of this project. Gheorghe Stefanescu and Dexter Kozen provided some wise feedback and offered some guidance through the rather wide literature. This research was partly funded by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme and carried out within the National Centre on HPC, Big Data and Quantum Computing - SPOKE 10 (Quantum Computing) and by the EU Next-GenerationEU - National Recovery and Resilience Plan (NRRP) - MISSION 4 COMPONENT 2, INVESTMENT N. 1.4 - CUP N. I53C22000690001 and by the EPSRC grant No. EP/V002376/1. Bonchi is supported by the Ministero dell’Università e della Ricerca of Italy grant PRIN 2022 PNRR No. P2022HXNSC - RAP (Resource Awareness in Programming). Di Giorgio is supported by the EU grant No. 101087529.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
and the pairing \(\langle {id}_{X},{id}_{X}\rangle {\mathop {=}\limits ^{\tiny \text {def}}}\blacktriangleleft _{X} :X \rightarrow X \otimes X\) form a comonoid in \((\textbf{Rel}, \otimes , 1)\). Similarly the unique function
and the copairing \([{id}_{X},{id}_{X}]{\mathop {=}\limits ^{\tiny \text {def}}}\rhd _{X} :X\oplus X \rightarrow X\) form a monoid in \((\textbf{Rel}, \oplus , 0)\). By taking their opposite relations, we obtain in total the two (co)monoid structures illustrated below.
The black (co)monoids give to \((\textbf{Rel}, \otimes , 1)\) the structure of a Cartesian bicategory [19], while the white ones give to \((\textbf{Rel}, \oplus , 0)\) the structure of, what we named, a Kleene bicategory. These are illustrated in the next two sections.
and a comonoid
satisfying the usual coherence conditions (see e.g. [55, Table 4.7]) such that
is left adjoint to
;
and
;
and
form special Frobenius algebras (see e.g. [
,
,
,
defined as in (4). Simple computations confirm that all the laws of Definition 1 are satisfied. The operations of \(\textsf{CR}\) in (2) can be defined in any Cartesian bicategory, as
for all objects X, Y and arrows \(f,g:X \rightarrow Y\). The reader can easily check that, in \(\textbf{Rel}\), these correspond to the intersection \(f\sqcap g\), the top relation \(X\times Y\) and the opposite relation \(f^{\dagger }\), respectively. From now on, we will depict a morphism \(f :X \rightarrow Y\) as
, and use
as syntactic sugar for \(f^{\dagger }\).
and a comonoid
satisfying the usual coherence conditions s.t.:
is right adjoint to
;
, \(\rhd _{Y}; f= (f \oplus f); \rhd _{X}\) and
.
, \(\rhd _{X}\),
defined as in (4) is a finite biproduct category with idempotent convolution and that \(\sqcup \) and \(\bot \) give union and empty relation. Unfortunately, finite biproduct categories with idempotent convolution do not have enough structure to deal with \((\cdot )^{*}\): differently from Cartesian bicategories they are not necessarily traced. Such structure has to be explicitely added:
satisfies the axiom
;
;
.
where \(s \in \Sigma \), \(A,B \in \mathcal {S}\) and \(U,V \in \mathcal {S}^\star \). The terms of the first row, called circuits, intuitively represent arrows of a Cartesian bicategory. The terms of the second row, called tapes, represent arrows of a Kleene bicategory. As expected, we only consider those terms to which is possible to associate source and target objects: the reader may check the simple type system in [9, Table 1]. Constants and operations in (16) can be extended to arbitrary polynomials in \((\mathcal {S}^\star )^\star \). For instance,
is inductively defined as
and
. For the other definitions see [11].
and
. Left distributors \(\delta ^l_{P,Q,R} :P \otimes (Q\oplus R) \rightarrow (P \otimes Q) \oplus (P\otimes R)\) and \(\otimes \)-symmetries
are defined as in [11, Table 4]. The (co)monoids of \(\otimes \) as in [11, (20),(21)].
of tapes with the same domain and codomain. We define \(\,{\le }_{{\mathbb {I}}}\,\) to be the set generated by the following inference system (where \(\mathfrak {t}\,{\le }_{{\mathbb {I}}}\,\mathfrak {s}\) is a shorthand for \((\mathfrak {t},\mathfrak {s})\in \,{\le }_{{\mathbb {I}}}\,\)).
, while \({id}_{1}\) is
: a tape filled with the empty circuit. For a monomial \(U \!=\! A_1\dots A_n\), \({id}_{U}\) is depicted as a tape containing n wires labelled by \(A_i\). For instance, \({id}_{AB}\) is rendered as
. When clear from the context, we will simply represent it as a single wire
with the appropriate label. Similarly, for a polynomial
, \({id}_{P}\) is obtained as a vertical composition of tapes, as illustrated below on the left.
is a tape closed on its right boundary. Codiagonals and cobangs are represented in the same way but mirrored along the y-axis. Exploiting the usual coherence conditions e.g. in [55, Table 4.7], we can construct (co)diagonals and (co)bangs for arbitrary polynomials. For example, \(\rhd _{A\oplus B \oplus C}\) and
are depicted as the second and third diagrams above.
is represented as a splitting of wires, while the discharger
is a wire closed on the right. From the coherence laws in (15), one can build (co)copiers and (co)dischargers for arbitrary polynomials. For instance,
and
are drawn as the last two diagrams above. For an arbitrary tape diagram \(\mathfrak {t}:P \rightarrow Q\) we write
.
Again coreflexives form a Boolean algebra \((C,\sqcup , \mathbin {;}, \lnot , \bot , {id} )\) where composition \(\mathbin {;}\) acts as \(\sqcap \): see Lemma 2.3. Moreover, by Corollary 1, \(\textbf{KCT}_{\Sigma ,\mathbb {I}}[U,U]\) is a Kleene algebra. Thus \((\textbf{KCT}_{\Sigma ,\mathbb {I}}[U,U], C, \sqcup , \mathbin {;}, (\cdot )^{*}, \bot , {id} , \lnot )\) is a Kleene algebra with tests [42].
. An interpretation of \(\Sigma \) in \(\textbf{Rel}\) consists of a set X (i.e., \(\alpha _\mathcal {S}(A)\)), a relation \(0 \subseteq 1 \times X\) (i.e.,
) and a relation \(s\subseteq X \times X\) (i.e.,
).
terminates on all possible inputs, it is interesting to see how this can be proved within the kc theory \((\Sigma ,\mathbb {P})\).
is total, i.e.
.
to copy n times the content of variables in \(\Gamma \). Formally,
is defined as
and
. Guards in commands are encoded using c(P), defined in (21). The encoding of commands is pretty standard, see e.g. [42], with the only exception of assignment that is depicted as the diagram on the right where, for the sake of readability, we label wires directly with the typing contexts rather than their encodings. Note that, in this case, \(\mathcal {E}(\cdot )\) exploits the structure of Cartesian bicategories to properly take into account data flow. For instance, for \(\Gamma =x:A,y:A,z:A\), the encoding maps \(\Gamma \vdash x :==z ; y:==z\) and \(\Gamma \vdash y :==z ; x :==z\) into the same tape.
