In fact, $(\Rel,+)$ is also a biproduct category (Section <ref>), with copying and deleting relations given by the converse of the above relations:

\[
\sem{\Bcomultn{X}}= \{(x, (x,i))\mid x\in X, i=1,2\}
\qquad \sem{\Bcounitn{X}} = \varnothing
\]

One can check that $\Bcomult,\Bcounit$ form a commutative comonoid for any $X$, and that they can copy and delete any relation, i.e., that they satisfy the (dup) and (del) axioms from (<ref>).

Intuitively, we can think of the diagrams $\Wmult,\Wunit,\Bcounit,\Bcomult$ in this category as directing the flow of a single token that travels around the wires. The intuition here is that the $\Wmult$ transfers to the right wire the token that comes through any one of its left wires, $\Wunit$ is able to generate a token, $\Bcomult$ is a non-deterministic forl and $\Bcounit$ a dead-end.
As we have already said, the relations for $\Wmult$ and $\Wunit$ are simply the graphs of the functions defined in the category of sets and functions. This makes sense: functions can only direct the token deterministically from left to right. Hence, they lack the nondeterministic $\Bcomult$ and $\Bcounit$.

Note that the particle intuition for diagrams in $\Rel$ with the disjoint sum as monoidal product is quite different from the intuition for diagrams in $\Rel$ with the Cartesian product, where values for all wires are set to compatible values globally, all at once. For this reason, diagrams in biproduct categories are sometimes called particle-style while those of self-dual compact closed categories are said to be wave-style in some contexts [1].

As in the previous example, we can represent any relation between finite sets, using these basic diagrams. For this, we only need $\Bcomultn{1}$, $\Bcounitn{1}$, $\Wmultn{1}$ and $\Wunitn{1}$ over the set singleton set $1$, which we will once gain write as $\Bcomult$, $\Bcounit$, $\Wmult$ and $\Wunit$.  A relation $R \from X\to Y$ corresponds to a diagram $d$ with $|X|$ wires on the left and $|Y|$ wires on the right. The $j$-th port on the left is connected to the $i$-th port on the right exactly when $(i,j)\in R$. For example,
the relation $R\from \{0,1,2\}\to \{0,1\}$ given by $\{(0,0), (0,1), (2,1)\}$,
can be represented by the following diagram:

\begin{equation}\label{ex:relation}
\tikzfig{ex-relation}
\end{equation}

where a single wire is interpreted as the identity over some choice of singleton set. We see that this representation extends that of functions, by adding the possibility of connecting one wire on the left to several (or none) on the right. This is precisely the difference between functions and relations, reflected in the diagrams.

Note that a relation can also be seen as a matrix with Boolean coefficient. The relationship between the diagrams above and matrices (over more general semirings) will be explained more generally below in Example <ref>.

We have just seen that going straight from functions to relations (with the disjoint sum as product) amounted to adding $\Bcomult$ and $\Bcounit$ to $\Wmult$ and $\Wunit$. These two examples fit into a whole hierarchy of expressiveness:

\[\tikzfig{prop-hierarchy-landscape}\]

Of course, any subset of the generators $\Bcomult,\Bcounit, \Wunit,\Wmult$ gives a well-defined sub-SMC of ($\Rel$,$+$). We have not included all $2^4$ of them as they do not all correspond to well-known mathematical notions.

We should also note that the way in which these theories are combined define distributive laws, a topic we have mentioned briefly in Remark <ref>.

[Spans, $\times$]
The category $\Span{\Set}$ has sets as objects and, as morphisms $X\to Y$, pairs of maps $f:A\to X, g:A\to Y$ with the same set $A$ as domain. We will write spans as $\spn{X}{f}{A}{g}{Y}$. One way to think about spans is as witnessed or proof relevant relations that keep track of the way in which two elements are related: an element $a$ of the apex $A$ can be thought of as a witness or a proof of the fact that $(f(a),g(a))$ are related by the span. Thus, the difference with relations is that there may be several ways in which two elements from $X$ and $Y$ are related by the same span  $(A,f,g)$; if $f(a)=f(a')=x$ and $g(a)=g(a')=y$, then $(x,y)$ are related by two different witnesses $a$ and $a'$. If we forget the additional structure at the apex, we obtain a relation (in fact there is a way of constructing $\Rel$ from $\Span{\Set}$; the interested reader will find this explained in [60, 113]).

The composition of two spans is obtained by computing what is called the pullback of $g$ and $p$ below and composing the resulting outer two functions on each side:

\begin{equation*}
%  \label{eq:span-comp}
\xymatrix{
&& A\times_Y B \ar[dl]_{\pi_1}\ar[dr]^{\pi_2}\\
& A \ar[dl]_{f}\ar[dr]^{g} & & B\ar[dl]_{p} \ar[dr]^{q}\\
X\,  & & Y & & \, Z
\end{equation*}

where $A\times_Y B := \{(a,b) \mid (g(a) = p(b)\}$ and $\pi_1,\pi_2$ are the two projections onto $A$ and $B$. Thus, the composition of $\spn{X}{f}{A}{g}{Y}$ followed by $\spn{Y}{p}{B}{q}{Z}$ is $\spn{X}{f\circ \pi_1}{A\times_Y B}{q\circ \pi_2}{Y}$. For a set $X$, the identity span is $\spn{X}{id_X}{X}{id_X}{X}$. As given, this operation is not strictly associative or unital. To make $\Span{\Set}$ into a bona fide category, we need to identify all isomorphic spans: two spans $\spn{X}{f}{A}{g}{Y}$ and $\spn{Y}{p}{B}{q}{Z}$ are isomorphic when there is a bijection $h: A \to B$ such that $p\circ h = f$ and $q\circ h = g$.

$\Span{\Set}$ can be made into a symmetric monoidal category with the Cartesian product of sets: on objects $X_1\times X_2$ is the usual set of pairs of elements of $X_1$ and $X_2$, on morphisms $(\spn{X_1}{f_1}{A_1}{g_1}{Y_1})\otimes (\spn{X_2}{f_2}{A_2}{g_2}{Y_2}) = (\spn{X_1\times X_2}{f_1\times f_2}{A_1\times A_2}{g_1\times g_2}{Y_1\times Y_2})$. With the singleton set as unit and the symmetry as $\spn{X\times Y}{id}{X\times Y}{\sigma_X^Y}{Y\times X}$ where $\sigma_X^Y(x,y) = (y,x)$ as before, this equips $\Span{\Set}$ with a symmetric monoidal structure.

Furthermore, like relations, spans form a hypergraph category, with the choice of Frobenius structure for each set $X$ given by

\begin{equation}\label{eq:span-hypergraph}
\begin{gathered}
\sem{\Bcomultn{X}} = \spn{X}{id_X}{X}{\Delta_X}{X\times X}\qquad \sem{\Bcounitn{X}}= \spn{X}{id_X}{X}{!_X}{1}\\
\sem{\Bmultn{X}} = \spn{X\times X}{\Delta}{X}{id_X}{X}\qquad \sem{\Bunitn{X}} = \spn{1}{!_X}{X}{id_X}{X}
\end{gathered}
\end{equation}

where $\Delta$ is the usual diagonal, defined by $\Delta_X(x) = (x,x)$, and $!_X$ the unique map $X\to 1$. The proof that these satisfy the appropriate axioms can be computer much like for relations, with the added complexity that one has to keep track of the witnesses in each apex.

Notice that if we forget the apex of each of these, and only keep track of the pairs that they relate, the resulting relations are exactly those that give $\Rel$ its hypergraph structure, cf. (<ref>). This is a general fact about spans and relations. If spans (of sets or any category with categorical products) of type $X\to Y$ can be seen as maps $A\to  X\times Y$, relations are precisely injective (or monomorphic, in the general categorical setting) spans. One can always obtain a relation from a span $A\to X\times Y$ by first factorising the map into a surjective map (epimorphism) followed by an injective (monomorphism) one, and keeping only the latter.

As for relations, spans can also be equipped with the disjoint sum as monoidal product. In fact, with this monoidal product, we can use the same diagrammatic language to represent any span of finite sets, $\Bcomult, \Bcounit$, $\Wmult, \Wunit$ with the following slightly modified interpretation:

\[
\sem{\Bcomultn{X}}= \spn{X}{\nabla_X}{X+X}{id_X}{X+X}
\qquad \sem{\Bcounitn{X}} = \spn{X}{0}{\varnothing}{id_X}{\varnothing}
\]

\[
\sem{\Wmultn{X}}= \spn{X+X}{id_X}{X+X}{\nabla_X}{X}
\qquad \sem{\Wunitn{X}} = \spn{\varnothing}{id_X}{\varnothing}{0}{X}
\]

where $\nabla_X:X+X\to X$ is defined by $\nabla_X(x,i)=x$ and $0_X:\varnothing\to X$ is the only map from the empty set to any set $X$.

With these, $(\Span{\fSet},+)$ is also a biproduct category as defined in Section <ref>. In fact, it is the free biproduct category over a single object and no additional morphism <cit.>.

As for relations, we can use $\Bcomultn{1}$, $\Bcounitn{1}$, $\Wmultn{1}$ and $\Wunitn{1}$ to represent any span of finite sets with $+$ as monoidal product: for the span $\spn{n}{f}{A}{g}{m}$, there is a path from the $i$-th wire on the left to the $j$-th one on the right in the corresponding diagram for each element of $\{a\in A\mid f(a)=j, g(a)=i\}$. For example,
the span $\spn{3}{f}{4}{g}{2}$, with $f(0)=f(1)=f(2)=0$, $f(3)=2$ and $g(0)=0,g(1)=g(2)=g(3)=1$,
can be represented by (for example) the following diagram:

\[\tikzfig{ex-span}\]

Notice that this diagram denotes the same relation as in (<ref>), but the two represent different spans.

Another way to understand the correspondence is to notice that spans of finite sets can be seen as matrices with coefficients in $\N$. Because we identify isomorphic spans, the specific label of each witness in the apex plays no role. In this sense a span just keeps track of how many ways two elements in each of its legs are related.
More precisely, given the span $\spn{n}{f}{A}{g}{m}$, we can represent it as an $m\times n$ matrix whose $(i,j)$-th coefficient is the cardinality of $\{a\in A\mid f(a)=j, g(a)=i\}$.  The diagrammatic calculus for matrices (over any semiring) will be explained in more details in Example <ref> below. This perspective is also developed in [25], where the authors study some of the algebraic properties of the SMC of spans and their dual, cospans, which we will introduce next.

The category $\Cospan{\Set}$ has sets as objects and morphisms $X\to Y$ given by pairs of maps $f:X\to A$ and $g: Y\to A$ with the same set $A$ as codomain, which we write as $\cospn{X}{f}{A}{g}{Y}$.
The composition of two cospans is obtained by computing what is called the pushout of $g$ and $p$ below and composing the resulting outer two functions on each side:

\begin{equation*}
%  \label{eq:cospan-comp}
\xymatrix{
&& A+_Y B \\
& A \ar[ur]_{\iota_1} & & B \ar[ul]^{\iota_2} \\
X\ar[ur]_{f} & & Y\ar[ul]^{g}\ar[ur]_{p} & & \, Z \ar[ul]^{q}
\end{equation*}

where $A+_Y B =\big(\{(a,1) \mid a\in A\}\cup \{(b,2) \mid b\in B\}\big)/\sim$ where $\sim$ is the equivalence relation defined by $(a,1)\sim (b,2)$ iff $a=g(y)$ and $b=p(y)$ for some $y\in Y$, and $\iota_1,\iota_2$ are the obvious inclusion maps of $A$ and $B$ into $A+_YB$. Then, the composition of $\cospn{X}{f}{A}{g}{Y}$ with $\cospn{Y}{p}{B}{q}{Z}$ is $\cospn{X}{\iota_1\circ f}{A\times_Y B}{\iota_2\circ q}{Y}$. For a set $X$, the identity cospan is $\cospn{X}{id_X}{X}{id_X}{X}$. As for spans, this operation is not strictly associative or unital. To make $\Cospan{\Set}$ into a bona fide category, we need to identify all isomorphic cospans: two cospans $\cospn{X}{f}{A}{g}{Y}$ and $\cospn{Y}{p}{B}{q}{Z}$ are isomorphic when there is a bijection $h: A \to B$ that makes the two resulting triangles commute.

Like for spans, we can equip cospans with the structure of a SMC—this time with the disjoint sum as monoidal product. Take $X_1+X_2$ to be the monoidal product on objects and, on morphisms, $(\cospn{X_1}{f_1}{A_1}{g_1}{Y_1})\otimes \cospn{X_2}{f_2}{A_2}{g_2}{Y_2} = \cospn{X_1+X_2}{f_1+f_2}{A_1+A_2}{g_1+g_2}{Y_1+Y_2}$ where $(f_1+f_2)(x,i) = f_i(x)$, with the empty set as unit and the symmetry given by $\cospn{X+Y}{id}{X+Y}{\iota_2+\iota_1}{Y+X}$, where $\iota_1 : X\hookrightarrow X$, $\iota_2 : Y\hookrightarrow X$ are the injections into the first and second component given respectively by $\iota_1(x) = (x,1)$ and $\iota_2(y) = (y,2)$.

Once again, this is a hypergraph category. The chosen Frobenius structure is given for each set $X$ by

\begin{equation}
\begin{gathered}
\sem{\Bcomultn{X}} = \cospn{X}{id_X}{X}{\nabla_X}{X+X}\qquad \sem{\Bcounitn{X}} = \cospn{X}{id_X}{X}{0_X}{\varnothing}
\\
\sem{\Bmultn{X}} = \cospn{X+X}{\nabla_X}{X}{id_X}{X} \qquad \sem{\Bunitn{X}} = \cospn{\varnothing}{0_X}{X}{id_X}{0}
\end{gathered}
\end{equation}

where $\nabla_X: X+X\to X$ is defined as before by $\nabla_X(x,i) = x$ and $0_X  : \varnothing \to X$ is the unique map from the empty set to $X$. Notice the similarity (and differences!) with (<ref>).

In fact, there is more than a coincidental relationship between cospans and hypergraph categories: $\Cospan{\fSet}$, the category of cospans restricted to finite sets, is the free hypergraph category on a single object and no morphisms <cit.>, that is, on the signature $\Sigma = (\{\bullet\}, \varnothing)$.
This means in particular that any cospan between finite sets (seen again as ordinals) can be represented as a diagram using only $\Bcomult,\Bcounit,\Bunit,\Bmult$. To build some intuition for this correspondence, take for example the pair $f:\{1,2,3,4\}\to\{1,2,3\}$ and $g: \{1,2\}\to \{1,2,3\}$, given by $f(1)=f(3)=1$, $f(2)=f(4)=2$ and $g(1)=g(2)=2$; this cospan can be depicted as:

\begin{equation}\label{eq:ex-cospan}
\tikzfig{ex-cospan}\qquad \text{ or, using spider  notation }\quad \tikzfig{ex-cospan-spider}
\end{equation}

The rule of thumb is easy to formulate: each element of the apex of the cospan—here, $\{1,2,3\}$—corresponds to one connected network of black generators, and a boundary point is connected to a black dot if it is mapped to the corresponding apex element by (one of the legs of) the cospan. There is only one way of forming such a network from the generators modulo the axioms of special commutative Frobenius structures, by the spider theorem, a result we saw in Example <ref>.

Moreover, researchers noticed that many hypergraph categories can be seen as categories of cospans equipped with additional structure [51]. Interestingly, not all hypergraph categories can be described in this way. For that, we need the notion of corelation, which we cover next.

After seeing the last few examples, it is natural to wonder: spans are to relations as cospans are to what? The answer is equivalence relations, also known as corelations in this context [38]. It turns out that we can organise equivalence relations into a SMC—into a hypergraph category, in fact.

A corelation $C\from X\to Y$ is an equivalence relation (i.e. a reflexive, symmetric and transitive relation) over $X+Y$. Given two corelations $C\from X\to Y$ and $D\from Y\to Z$, their composition $C\poi D \from X\to Z$ is defined by glueing together equivalence classes from $C$ and $D$ along shared elements. To define it formally, we temporarily rename $C.D$ the usual composition of relations (cf. Example <ref>) and let $R^*$ be the transitive closure of a relation $R$; then $C\poi D $ is the restriction of $C\cup D\cup (C.D)^*$ to elements of $X+Z$. Intuitively, two elements $a$ and $b$ are in the same equivalence class of $C\poi D$ if there exists some sequence of elements of $X+Y+Z$, that are equivalent either according to $C$ or $D$, starting with $a$ and ending with $b$.
The disjoint sum of sets can be extended to corelations to give a monoidal product.
Once more, this category is not only symmetric monoidal, but it is a hypergraph category with Frobenius structure on each set $X$ given by

\begin{equation}
\begin{gathered}
\sem{\Bcomultn{X}} = \{((x,i),(x,j))\mid i,j\in\{0,1,2\}\}\qquad \sem{\Bcounitn{X}} = X
\\
\sem{\Bmultn{X}} = \{((x,i),(x,j))\mid i,j\in\{0,1,2\}\} \qquad \sem{\Bunitn{X}} = X
\end{gathered}
\end{equation}

As we did for cospans, it is easy to represent any corelation between finite sets as a diagram using only $\Bcomult,\Bcounit,\Bunit,\Bmult$. For example, the corelation $\{1,2,3\}\to \{1,2\}$ given by the two equivalence classes $\{1,2,3\}\to \{1,2\}$ and $\{1,2,3\}\to \{1,2\}$ can be depicted by any of the following diagrams, using spider notation:

\[\tikzfig{ex-cospan-spider}\qquad\quad \tikzfig{ex-corelation-spider}\]

Notice that the first is the same diagram as in (<ref>). The individual black dot, which represented an element of the apex of the cospan that was not in the image of any of the two leg maps, is absent from the second diagram. These two diagrams represent the same corelation, since an isolated black dot represents an empty equivalence class: $\sem{\bullet} =\sem{\tikzfig{bunit-bcounit}}=\varnothing$.  In diagrammatic terms, this means that we can always remove networks of black generators that are not connected to any boundary points using the fact that $\tikzfig{bunit-bcounit} = \idzero$.

Much like relations can be seen as jointly injective spans, i.e. injective maps $R\hookrightarrow X\times Y$, corelations $C\from X\to Y$ are—dually—jointly surjective cospans, i.e. surjective maps $X+Y\twoheadrightarrow S$. We have already seen that, given a span $A\rightarrow X\times Y$, one can extract a relation $R$ by factorising it into $A\twoheadrightarrow R\hookrightarrow X\times Y$, a surjective map followed by an injective map. Similarly, one can obtain a corelation from a cospan by keeping only the surjective map in the factorisation of the corresponding map $X+Y\to S$. As we have just seen, diagrammatically, this corresponds to removing isolated black dots. In category theory, the factorisation of $\Set$ maps into an surjective map followed by an injective one can be abstracted into a notion called a factorisation system. It turns out that corelations can be defined for different factorisation systems than the surjective-injective one. Moreover, they can be decorated with additional structure. In fact, these two generalisations are so powerful that every hypergraph category can be constructed as a category of decorated corelations [52, 53].

[Linear maps, $\otimes$]
The category $\fVect$ of finite-dimensional vector spaces (over some chosen field $\Field$) and linear maps is also a symmetric monoidal category, in at least two different ways. This example deals with the tensor product, while the next one considers the direct product.

We will not go over the rigorous definition of the tensor product of vector spaces here; suffices to say that $X_1\otimes X_2$ can be defined as a quotient of the free vector space over $X_1\times X_2$ that make $\otimes$ bilinear. On morphisms, it is uniquely specified as the linear map $(f_1\otimes f_2)$ that satisfies $(f_1\otimes f_2)(u_1\otimes u_2) = f(u_1)\otimes f_2(u_2)$. This defines a SMC, with unit the field $\Field$ itself, since $X\otimes \Field \cong X$, and symmetry the map fully characterised by $\sigma(u_1\otimes u_2) =u_2\otimes u_1$.

Crucially, this SMC is not Cartesian. The intuition here is that, when we choose a comultiplication operation $\Bcomult$ over $X$, we also choose some set of elements $v\in X$ that this operation copies, i.e. that verify:

\begin{equation}\label{eq:copyable-states}
\sem{\tikzfig{v-bcomult}} = \sem{\quad\tikzfig{2-v}}
\end{equation}

But then, given two such copyable elements $v_1,v_2$, consider their sum $u= v_1 + v_2$—we should have

\[\sem{\tikzfig{u-bcomult}} = \sem{\tikzfig{v1-bcomult}}+\sem{\tikzfig{v2-bcomult}} = \sem{\:\tikzfig{v1xv1}}+\sem{\:\tikzfig{v2xv2}} = v_1\otimes v_1 + v_2\otimes v_2\]

On the other hand

\[\sem{\:\tikzfig{uxu}} = u\otimes u = (v_1+v_2)\otimes (v_1+v_2) = v_1\otimes v_1 + v_1\otimes v_2 + v_2\otimes v_1 + v_2\otimes v_2\]

Thus, no linear map can copy all elements of a given vector space, as is required for the comonoid structure of a Cartesian category.

In fact, $(\fVect,\otimes)$ is compact closed (recall that the requirement of Cartesian-ness and compact closed-ness are incompatible in the sense explained in Section <ref>). The dual of a vector space defined to be its algebraic dual in the usual sense: $A^*$, the space of linear maps $A\to \Field$. Then, the cap on a vector space $X$ is the unique linear map $X^*\otimes X\to \Field$ that satisfies $\sem{\capx{}}(f\otimes v) = f(v)$ (also known as the evaluation map). The cup is its  adjoint: to describe it explicitly, we need to pick a basis $\{e_i\}_i$ of $X$ and a dual basis $\{f_i\}_i$ of $X^*$ in the sense that $f_i(e_j) =1$ if $i=j$ and $0$ otherwise; $\sem{\cupx{}}$ is then the map $\Field \to X\times X^*$ given by extending $1\mapsto \sum_i e_i\otimes f_i$ by linearity.
In summary, using the bases $\{e_i\}_i$ and $\{f_i\}_i$ for both cups and caps, we have:

\[\sem{\cupx{}}(k) = \sum_i k (e_i\otimes f_i)\qquad \qquad \sem{\capx{}}\left(\sum_{i,j} \lambda_{i,j} (e_i\otimes f_j)\right) = \sum_i \lambda_{i} f_i(e_i)\]

Note however, that the resulting maps are independent of the specific choice of bases. With these expressions, we can verify the yanking equation for $\cupx{}$ and $\capx{}$. Let $u$ be some element of $X$ such that $v=\sum_i \lambda_i e_i$; we have:

\begin{align*}
\sem{\tikzfig{s-yanking-X}}(v) & = \left(\sem{\cupx{}} \otimes \sem{\idright}\right)\poi \left(\sem{\idright}\otimes \sem{\capx{}}\right)(v)
\\
& = \left(\sem{\idright}\otimes \sem{\capx{}}\right)\left(\left(\sum_i (e_i\otimes f_i)\right)\otimes v\right)
\\
& = \sum_i f_i(v) e_i
\\
& = \sum_i f_i\left(\sum_{j}\lambda_j e_j\right) e_i
\\
& = \sum_i \sum_{j}\lambda_j f_j(e_j) e_i
\\
& = \sum_i \lambda_i e_i = v
\end{align*}

Note also that, in this SMC, the elements of a vector space $X$ are precisely the diagrams $\Field \to X$.

As we have seen, every compact closed category is also traced. In fact, the name (partial) trace comes from linear algebra, where the trace $\Tr f$ of a linear map $f:\R^n\to\R^n$ is the sum of the diagonal coefficients of its matrix representation in any basis. Thus, we expect that,

\[\tikzfig{trace-linear-map} = \Tr f = \Tr A = \sum_i a_{ii}\]

where $A = (a_{ij})$ is the matrix that represents the action of $f$ on some chosen basis.
It is a nice exercise to show that this is indeed the case. It is then immediate to derive certain well-known properties of the trace in linear algebra, such as $\Tr(AB) = \Tr(BA)$ (or, more generally, that it is invariant under circular shifts).

Another important feature (with consequences, among other areas, in quantum theory) is that commutative and special Frobenius structure in $(\fVect,\otimes)$ correspond to a choice of a basis for the supporting vector space <cit.>. We have seen above that—even if there is no linear copying map for all the elements of a vector space—when we choose a comultiplication operation $\Bcomult$ over $X$ we also choose some set of elements $v\in X$ that $\Bcomult$ copies. Conversely, given any basis, we can define a comonoid operation that copies its elements, i.e., whose comultiplication and counit are defined respectively by extending the following maps by linearity: $e_i\mapsto e_i\otimes e_i$ and $e_1\mapsto 1$. What about the monoid? A monoid in $(\fVect,\otimes)$ is more commonly known as an algebra. Any basis defines not only a comonoid but an algebra given by extending the comparison map $e_i\otimes e_j\mapsto \delta^i_j e_i$ by linearity. Not only that, the corresponding monoid-comonoid pair satisfies the Frobenius axioms and define a special and commutative Frobenius structure. Conversely, the copyable states of any commutative and special Frobenius structure form a basis of $X$. The last direction is more difficult to prove and we will not do so here. Instead, we refer the interested reader to the lectures notes of Vicary and Heunen, who deal with a related case in details <cit.> and use string diagrams throughout.

Finally, a brief historical note: one of the earliest instances of string diagrams are Penrose graphical notation [96] for working with tensors, which are precisely string diagrams for $(\fVect,\otimes)$, later systematised and generalised in [75].

[Matrices, $\oplus$]
Another possible monoidal product is given by the direct sum of vector spaces $X_1\oplus X_2$ on objects and by $(f_1\oplus f_2)(x_1, x_2) = (f_1(x_1), f_2(x_2))$ on morphisms. The unit of the product is the vector space $\{0\}\cong \mathbb{K}^0$ and, with the symmetry given by $\sigma_X^Y(x,y) = (y,x)$, the resulting structure is a SMC. It is well-known that isomorphic finite-dimensional vector spaces are uniquely identified by their dimension. Therefore, in the same way that we identified finite sets with finite ordinals, we will restrict our attention to the subcategory of  $\fVect$ whose objects are $\mathbb{K}^n$ for some  $n\in\N$. We can go even further: give a linear map $\mathbb{K}^m\to\mathbb{K}^n$, we can identify it with its representation in the canonical bases of $\mathbb{K}^m$ and $\mathbb{K}^n$. We call $\Mat{\Field}$ the category whose objects are natural numbers (representing the dimension of a vector space) and morphisms $m\to n$ are $n\times m$ matrices (notice the reversal). Nothing is lost, since $\Mat{\Field}$ and $\fVect$ are equivalent.

The SMC $(\Mat{\Field},\oplus)$ is Cartesian with the canonical comonoid structure over some vector space $X$ is given by

\[\sem{\Bcomultn{n}}(x)=(x,x)\qquad\qquad \sem{\Bcounitn{n}}(x) = \bullet\]

Since linear maps are maps with extra structure, this comonoid is inherited from $\Set$ (cf. Example <ref>) and the proof that this monoidal category is Cartesian is exactly the same.

$\Mat{\Field}$ also contains a remarkable monoid structure on every object, given by addition and zero:

\[\sem{\Wmultn{n}}(x_1,x_2)=x_1+x_2\qquad\qquad \sem{\Wunitn{n}} = 0\]

Note that the comonoid and monoid do not interact to form a Frobenius structure but a bimonoid (cf. Section <ref>). In fact, we have even more structure: this category satisfies the axioms of biproduct categories (Section <ref>). This means that, maps do not only satisfy the (dup) and (del) axioms of Cartesian categories, but the dual axioms of coCartesian categories (codup) and (codel): in semantic terms, these last two axioms are simply implied by linearity: all maps preserve addition. Note that this structure is very similar to that of relations with the disjoint sum as monoidal product (cf. Example <ref>), the chief difference being that the bimonoid is not idempotent for matrices over a field. The close similarity between the two cases comes from the fact that relations can be seen as matrices, not over field, but over the semiring of the Booleans.

With the bimonoid above, we are very close to being able to express matrices diagrammatically. As before, we will use $\Bcomultn{1}$, $\Bcounitn{1}$, $\Wmultn{1}$ and $\Wunitn{1}$, which we will simply write as $\Bcomult$, $\Bcounit$, $\Wmult$ and $\Wunit$. Contrary to the case of relations, we cannot express arbitrary matrices with just these; we need to add generating diagrams $\scalar{a}$ for scalar multiplication by some $a\in\Field$, interpreted as $\sem{\scalar{a}}(x) = ax$. There are few special cases of interest: multiplying by $1$ is the same as the identity, so $\sem{\scalar{1}} = \sem{\idone}$, and multiplying by zero always yields zero, so $\sem{\scalar{0}} = \sem{\tikzfig{bcounit-wunit}}$.

Putting all these ingredients together, we are now ready to represent matrices. An $n\times m$ matrix $A = (a_{ij})$ corresponds to a diagram $d$ with $m$ wires on the left and $n$ wires on the right—the left ports can be interpreted as the columns and the right ports as the rows of $A$. The left $j$-th port is connected to the $i$-th port on the right through an $a$-weighted wire whenever coefficient $a_{ij}$ is a scalar $a\in \Field$. When coefficient $a_{ij}$ is $0$, they are disconnected. In addition, given that $\sem{\scalar{a}} = \sem{\idone}$, we can simply draw the connection as a plain wire when $a_{ij}=1$ and since $\sem{\scalar{0}} = \sem{\tikzfig{bcounit-wunit}}$ we can also omit a connecting wire when $a_{ij}=0$. Conversely, given a diagram, we recover the matrix by summing weighted paths from left to right ports. For example, the matrix

\begin{equation*}
\label{eq:matrix-diagram}
A =
\begin{pmatrix}
a & 0 & 0 \\
b & 0 & 1
\end{pmatrix}
\end{equation*}

can be represented by any of the following diagrams, which are all semantically equal (i.e., represent the same matrix):

\[\tikzfig{ex-matrix-coeffs-1} \:\text{ or }\quad \tikzfig{ex-matrix-coeffs} \:\text{ or }\quad\tikzfig{ex-matrix}\]

The dotted boxes in the diagram on the left represent the columns of the corresponding matrix.
As we will see, we can then quotient the diagrammatic syntax by an equational theory that makes these three equal. In fact, we can define an equational theory $E$ such that the diagrams modulo $\eqE{E}$ form a SMC isomorphic to $\Mat{\Field}$. Such a theory is called complete. We will come back to completeness of equational theories in Section <ref> and give a complete theory for matrices in Example <ref>.

Finally, everything we have claimed in this example, would have worked as well with an arbitrary semiring $\Rig$, instead of a field: we would just need to consider matrices with coefficients in $\Rig$ and have diagrams $\scalar{a}$ for all $a\in\Rig$.

[Linear relations, $\times$]
In the last two examples, we have considered linear maps with different monoidal products. It is possible to extend the notion of linearity to relations: given two vector spaces $X$ and $Y$, a linear relation $X\to Y$ is a linear subspace of $X\oplus Y$, i.e. a subset of the direct sum that is closed under linear combinations. The composition (as relations) of two linear relations is still a linear relation (exercise), and the identity relation is linear. Therefore, linear relations can be organised into a category. We call $\LinRel$, the category whose objects are natural numbers and morphisms $m\to n$ are linear relation $\Field^m\to \Field^n$. With the Cartesian product, $\LinRel$ become a SMC, with unit and symmetry the same as those of $\Mat{\Field}$ (cf. previous example).

This SMC has a very rich structure. Firstly, just like any function can be seen as a relation, any linear map $f$ can be seen as a linear relation $\mathsf{Graph}(f)$, by taking its graph: $\mathsf{Graph}(f):=\{(x,y)\mid y=f(x)\}$. Thus, $\LinRel$ also contains the diagrams that allowed us to depict linear maps/matrices diagrammatically in the previous example, namely $\Bcomult,\Bcounit,\Wunit,\Wmult$ for any choice of underlying vector space $\Field^n$. Their interpretation as relation is given by the graph of their corresponding maps:

\begin{align*}
\sem{\Bcomultn{n}} = \{(x,(x,x))\mid x\in X\}\qquad\quad \sem{\Bcounitn{n}} = \{(x,\bullet)\mid x\in X\}\\
\sem{\Wmultn{n}} = \{((x_1,x_2), x_1+x_2)\mid x_1,x_2\in X\}\qquad\quad \sem{\Wunitn{n}} = \{(0,\bullet)\}
\end{align*}

Interestingly, the converse of these relations are also linear, and we adopt the mirror image of the corresponding diagrams to depict them: $\Bmult,\Bunit,\Wcounit,\Wcomult$, with semantics given by

\begin{align*}
\sem{\Bmultn{n}} = \{((x,x),x)\mid x\in X\}\qquad\quad \sem{\Bunitn{n}} = \{(\bullet,x)\mid x\in X\}\\
\sem{\Wcomultn{n}} = \{(x_1+x_2, (x_1,x_2))\mid x_1,x_2\in X\}\qquad\quad \sem{\Wcounitn{n}} = \{(\bullet,0)\}\\
\end{align*}

Notice that these are the same relations as the first two, with the pairs flipped. We can do this for any map $f$: let $\mathsf{coGraph}(f):=\{(y,x)\mid f(x)=y\}$. If $f$ is linear, its cograph will also be a linear relation. This duality will translate into a pleasant symmetry of the equational theory, which we will cover in Example <ref>.

[Monotone relations, $\times$]
So far all the examples of compact closed categories we have covered (spans, relations, cospans, corelations) have been hypergraph categories. Of course, there are compact closed categories where the compact structure does not come from some chosen Frobenius structure. The category of monotone relations is one such example. It has pre-ordered sets as objects (that is, sets equipped with a pre-order: a reflexive and transitive binary relation), and, as morphisms $(X,\preceq)\to (Y,\leq)$, relations $R\subseteq X\times Y$ that preserve the order in the following sense: if $(x,y)\in R$ and $x'\preceq x$, $y\leq y'$ then $(x',y')\in R$. The composition of monotone relation is the same as the usual composition of relations (recalled in Example <ref>). Since the composition of two monotone relations is monotone, they form a category, with identity on each object $(X,\preceq)$ given by the pre-order relation $\preceq\subseteq X\times X$ itself.

As for plain relations, the Cartesian product defines a monoidal product: $(X,\preceq)\times(Y,\leq) := (X\times Y, \preceq\times \leq)$ with $(x,y)\preceq\times \leq(x',y')$ iff $x\preceq x'$ and $y\leq y'$. The unit is still the singleton set $1=\{\bullet\}$ with the only possible pre-order.

As we anticipated, this category is compact closed. The dual $(X,\succeq)^*$ of $(X,\preceq)$ is $(X,\succeq)$, i.e., the same underlying set with the opposite pre-order relation $\succeq :=\preceq^{op}$. The cups and caps on each object are then given by

\[\sem{\cupx{}}= \{(\bullet, (x',x))\mid x\preceq x'\}\qquad\qquad  \sem{\capx{}}= \{( (x,x'),\bullet)\mid x'\preceq x\}\]

Let us check one of the defining equations of compact closed categories:

\[\tikzfig{s-yanking-X} =\idxright{}\]

The lhs of this equation has the following semantics:

\begin{align*}
\sem{\tikzfig{s-yanking-X}}& = \left(\sem{\cupx{}} \times \sem{\idxright{}}\right)\poi \left(\sem{\idxright{}}\times \sem{\capx{}}\right)
\\
& = \big(\{(\bullet, (x,x'))\mid x\preceq x'\}\times \preceq\big)\poi \big(\preceq \times \{( (x,x'),\bullet)\mid x\preceq x'\}\big)
\\
& = \big(\{(x,(x_1,x_2,x_3))\mid x_2\preceq x_1\land x\preceq x_3\}\big)\poi \big(\{(x_1,(x_2,x_3),x')\mid x_1\preceq x'\land x_3\preceq x_2 \}\big)
\\
& = \left\{(x,x')\mid \exists x_1\exists x_2 \exists x_3\big[x\preceq x_3 \land x_3\preceq x_2\land  x_2\preceq x_1\land x_1\preceq x' \big]\right\}
\\
& = \{(x,x')\mid x\preceq x'\}
\end{align*}

where the last step hold by transitivity of $\preceq$. This is clearly the same relation as $\preceq$ itself, which is the identity on $(X,\preceq)$, as we wanted.

Finally, in this SMC, every partial order is equipped with a canonical monoid and comonoid. They are given by the following monotone relations:

\begin{align}\label{eq:comonoid-monrel}
\sem{\tikzfig{lr-copy}} = \left\{(x,(x'_1,x'_2)\mid x\leq x'_1\text{ and } x\leq x'_2)\right\}\qquad\quad \sem{\tikzfig{lr-delete}} = \{(x,\bullet)\mid x\in X\}\\
\label{eq:monoid-monrel}
\sem{\tikzfig{lr-merge}} = \left\{((x_1,x_2),x')\mid x_1\leq x'\text{ and } x_2\leq x')\right\}\qquad\quad \sem{\tikzfig{lr-generate}} = \{(\bullet,x)\mid x\in X\}
\end{align}

Note that they are very similar to their standard relational cousins from Example <ref>. In fact, the former can be seen as the latter, composed with the partial order relation on each branch, to make them monotone: for example, if we momentarily reinterpret $\sem{-}$ as a mapping into $\Rel$, we have

\[\sem{\tikzfig{lr-copy}} = \sem{\idxright{}}\poi\sem{\tikzfig{bcomult}}\poi\sem{\tikzfig{leqxleq}}\]

since $\sem{\idxright{}} = \preceq = \{(x,x')\mid x\preceq x'\}$.

However, $\tikzfig{lr-copy}, \tikzfig{lr-delete},\tikzfig{lr-generate},\tikzfig{lr-merge}$ do not form a Frobenius structure, nor do they give rise to a (co)Cartesian structure. Their interaction is still interesting and can be axiomatised, but doing so requires turning to theories with inequalities rather than just equalities. We will look at these briefly in Section <ref> and at monotone relations again in Example <ref>.

§.§ Soundness and Completeness

Recall that we write $\FreeX{\Sigma}$ for the free $X$-category over some signature. Let  $\sem{-} \from  \FreeX{\Sigma} \to \mathsf{Sem}$ be an $X$-preserving functor into some $X$-category $\mathsf{Sem}$ working as our semantics. In this context, it is common to study those diagrams that the semantics identifies; in other words, we are interested in equalities $\sem{c}=\sem{d}$ for diagrams $c$ and $d$. Sometimes (if we are lucky) it is possible to characterise semantic equality completely by a set of axioms, called a theory.

We have already covered (symmetric monoidal) theories in Section <ref>. The same notion can be extended straightforwardly to other categories: Cartesian, traced, hypergraph etc. In all these cases, an (equational) theory $E$ is still a set a set of pairs of diagrams of $\FreeX{\Sigma}$ with the same arity and co-arity and $\myeq{E}$ is the smallest congruence relation (w.r.t. $\poi$ and $\otimes$) containing $E$.  We are now in a position to study their compatibility with a given semantics.

For this, we will need a bit more terminology: we say that a theory $E$ is sound (for $\sem{-}$) whenever $c\myeq{E}d$  implies that $\sem{c} = \sem{d}$; furthermore $E$ is said to be complete if the reverse implication holds. When $c\eqE{E}d$  iff $\sem{c} = \sem{d}$ the theory is sound and complete and sometimes called an axiomatisation of the target category. The reader will often read that a theory is “complete for $\Sem$", rather than $\sem{-}$, when the functor $\sem{-}$ is obvious and therefore left implicit.

Moreover, as we saw in Section <ref>, given a signature and a theory we can form the $X$ category $\FreeX{\Sigma,E}$ obtained by quotienting the free $X$ category $\FreeX{\Sigma}$ by the equivalence relation over diagrams given by $\eqE{E}$. There is then an $X$ functor $q\from \FreeX{\Sigma}\to\FreeX{\Sigma,E}$ witnessing this quotient.

We may also wonder what the expressive power of our diagrammatic language is. In terms of $X$ categories, we look to characterise precisely the image $\mathsf{Im}(\sem{\cdot})$ of the syntax via $\sem{\cdot}$.

The situation for a sound and complete theory is summarised in the commutative diagram below. Soundness simply means that $\sem{\cdot}$ factors as $s\circ q$ through $\FreeX{\Sigma,E}$ and completeness means that $s$ is a faithful $X$ functor.

\[
\begin{tikzcd}
\FreeX{\Sigma,E} \arrow[rr, "\cong"] \arrow[rrd, "s"]                  &  & \mathsf{Im}(\sem{\cdot}) \arrow[d, "i", hook] \\
\FreeX{\Sigma} \arrow[u, "q", two heads] \arrow[rr, "\sem{\cdot}"'] &  & \Sem
\end{tikzcd}
\]

Recall from Example <ref> that the SMC $(\fRel,+)$ of relations between finite sets with the disjoint sum is a symmetric monoidal category. We can give ourselves the signature

\[\Sigma =\left( \{1\}, \left\{\Bcomult, \Bcounit,\Wunit,\Wmult\right\}\right)\]

and quotient $\Sigma$-diagrams by the axioms of an idempotent, commutative bimonoid, which we recall below:

\begin{equation}\label{eq:axioms-idpt-bimonoid}
\begin{gathered}
\tikzfig{copy-associative} = \tikzfig{copy-associative-1}\qquad   \tikzfig{copy-unital-left}=\idx{} =\;\tikzfig{copy-unital-right}\qquad \tikzfig{copy-commutative}=\; \Bcomult
\\
\tikzfig{wmult-associative} = \tikzfig{wmult-associative-1}\qquad   \tikzfig{wmult-unital-left}=\idx{} =\;\tikzfig{wmult-unital-right}\qquad \tikzfig{wmult-commutative}=\; \Wmult
\\
\tikzfig{wmult-bcomult}\:=\:\tikzfig{2-bcomult-sym-2-wmult}\quad\qquad \tikzfig{wunit-bcomult}\:=\:\tikzfig{2-wunit}\quad\qquad \tikzfig{wmult-bcounit}\:=\:\tikzfig{2-bcounit}\quad\qquad \tikzfig{wunit-bcounit}\:=\: \quad \\
\tikzfig{bcomult-wmult}= \idx{}
\end{gathered}
\end{equation}

This equational theory turns out to be complete $\sem{-}$ as defined in Example <ref>. In other words, any two diagrams $c,d$ made from $\Bcomult, \Bcounit,\Wunit,\Wmult$ are equal modulo the axioms in (<ref>) iff they denote the same relation. The proof of this fact is typical: it works by showing how, given an arbitrary $\Sigma$-diagram $d$, we can rewrite it to some normal form, using only the equations of  (<ref>). The chosen normal form is the one from Example <ref>, from which the corresponding semantic entity—here, the corresponding relation—can be recovered uniquely. The fact that any diagram can be rewritten to a normal form using only the axioms above, is typically proven by induction, consider each individual cases, much like normalisation proofs in PL theory or cut elimination proofs in logic. And, much like these, they tend to be quite tedious and combinatorial.

Note that, depending on the context and the structure that one takes as a given, there are several ways of formulating the result above. For example, we could have also said that the Cartesian theory of an idempotent, commutative monoid is complete for $\sem{-}$, (now redefined to have the free Cartesian category over the specified theory as domain).

[Matrices, $\oplus$]
As we have already said, relations (resp. spans) with the disjoint sum as monoidal product can be seen as matrices with Boolean (resp. natural) coefficients. In fact, the equational theory of the previous example can be modified easily to accommodate any semiring. For the syntax, we've already seen in Example <ref>, that it suffices to add a generator for each scalar $r\in \Rig$, giving the signature

\[\Sigma =\left( \{1\}, \left\{\Bcomult, \Bcounit,\Wunit,\Wmult\right\}\cup \{\scalar{r} \mid r\in \Rig\}\right)\]

The equational theory is very similar to that of the previous example. It has all axioms of  (<ref>), except the last one, $\tikzfig{bcomult-wmult}= \idx{}$ (which encodes $x+x=x$, a specific feature of the Boolean semiring). In addition, we need axioms that encode the additive and multiplicative structure of the chosen semiring $\Rig$, namely:

\begin{equation}\label{eq:scalar-semiring-axioms}
\begin{gathered}
\tikzfig{bcomult-r+s-wmult}=\scalar{r+s}\qquad \quad \tikzfig{bcounit-wunit}= \scalar{0}
\\
\tikzfig{r-s}=\scalar{rs}\qquad \quad \idx{}= \scalar{1}
\end{gathered}
\end{equation}

Furthermore, we need to make sure that the scalars can be copied/deleted and that scalar multiplication distributes over addition; we can obtain these from the usual (dup)-(del) and (codup)-(codel) for scalars:

\begin{equation}\label{eq:scalar-copy-del}
\begin{gathered}
\tikzfig{r-bcomult}=\tikzfig{bcomult-r+r}\qquad \quad \tikzfig{r-bcounit} = \Bcounit
\\
\tikzfig{r+r-wmult}=\tikzfig{wmult-r}\qquad \quad \tikzfig{Wunit-r} = \Wunit
\end{gathered}
\end{equation}

Taken with the axioms of (<ref>) minus the last one, the axioms listed in (<ref>)-(<ref>) give a complete theory for matrices over $\Rig$: diagrams modulo these equations are equal iff they denote the same matrix.

From this general result, combined with the equivalence between spans and matrices with coefficients in $\N$, we can derive the following corollary: the free biproduct category over a single generating object (and no morphism) is an axiomatisation of the SMC $(\Span{\fSet},+)$ (Example <ref>).

One often hears that string diagrams are a resource-sensitive syntax. This somewhat cryptic incantation means something more simple than it lets on: instead of variables, diagrams use wires.  While variables can be used more (or less) than once—names cost little, at least when we are not concerned with computer implementations[Quantum computers present in this respect an interesting challenge, as quantum information, unlike classical one, cannot be perfectly copied. This is one of the starting point to the diagrammatic approach to quantum theory, see e.g. [2]]—there is not necessarily a natural way to copy wires in order to plug them into multiple diagrams. We saw above that some diagrammatic languages allow copying and erasing of wires. It turns out that the diagrammatic syntax of Cartesian categories is the diagrammatic counterpart of the standard symbolic notation for algebraic theories. Key in this correspondence is the ability to copy and delete arbitrary diagrams using the wire splitting and ending. These diagrammatic laws formalise the correspondence between composition and the all-important logical operation of substitution.   Let us see the correspondence on a simple example; the general formal correspondence between algebraic theories and Cartesian monoidal categories is worked out (for the single-sorted case) in  [24].

Consider the algebraic theory of monoids. It can be presented by two generating operations, $m(-,-)$ of arity $2$ and $e$ of arity $0$ (a constant) satisfying the following three axioms: $m(m(x,y),z) =m(x,m(y,z))$ and $m(e,x) = x = m(x,e)$. Terms of this algebraic theory are syntax trees whose leaves are labelled with variable names, as on the left below.

\[\tikzfig{ex-syntax-tree-monoid}\qquad\leadsto \qquad \tikzfig{ex-diagram-monoid}\]

By simply turning the tree on its side and gathering all leaves labelled by the same variable with $\Bcomult$ (or deleting those that we do not use with $\Bcounit$) we obtain the corresponding string diagram in the theory of Cartesian categories, as on the right above.

Two terms are equal if they one can be obtained from the other by applying a sequence of the defining equations of monoids. Similarly, two diagrams are equal if we can obtain one from the other by applying the following diagrammatic equalities (already encountered in Ex. <ref>):

\[\tikzfig{monoid-axioms}\]

with the axioms of Cartesian categories (cf. Section <ref>), which we recall here

\[\tikzfig{Lawvere-distributive-copy}\; \myeq{dup}\; \tikzfig{Lawvere-distributive-copy-1} \qquad \qquad \tikzfig{Lawvere-distributive-del}\;\myeq{del}\;\Bcounitn{x} \]

where $d$ can be any diagram.

What about models (in the usual algebraic sense) of algebraic theories? They are in one-to-one correspondence with Cartesian functors out of the free Cartesian category over the theory in question into the SMC $(\Set,\times)$. For example, to specify such a functor for the Cartesian theory of monoids involves choosing a carrier set $X$ and functions $\sem{m} : X\times X\to X$, $\sem{e} : 1\to X$ of the appropriate arity that satisfy the relevant axioms.

[Linear Relations]
Recall the interpretation $\sem{-}$ of $\Bcomult,\Bcounit,\Wunit,\Wmult$ and their duals $\Wcomult,\Wcounit,\Bunit,\Bmult$  in terms of linear relations, from Example <ref>. The symmetry of the corresponding equational theory is particularly pleasing. As for Example <ref>, $\Bcomult,\Bcounit,\Wunit,\Wmult$ are precisely those relations that are the graph of some linear map (aka a matrix) and so the equational theory is the same as in that example: essentially, a commutative bimonoid, with additional axioms to encode scalar multiplication and addition. The nice thing is that their colour-swamp $\Wcomult,\Wcounit,\Bunit,\Bmult$ satisfy exactly the same axioms. These two facts take care of all interactions between the black and white generators. It only remains to specify how diagrams of the same colour interact: $\Bcomult,\Bcounit,\Bunit,\Bmult$ and $\Wcomult,\Wcounit,\Wunit,\Wmult$ both form an extraspecial commutative Frobenius structures (Example <ref>)! The other axioms axiomatise the behaviour of scalars $\scalar{a}$ further, as they may now encounter their mirrored version:

\[\tikzfig{scalar-inverse}\;\;\text{ for } a\neq 0, \text{ where }\tikzfig{scalar-inverse-def}\]

The two cups and caps are also related in an obvious way:

\[\tikzfig{ih-cup-cap}\]

This theory is sometimes called the theory of Interacting Hopf algebras of IH for short. The reader will find the whole theory and further details in [23]. From these axioms, most of textbook linear algebra can be reworked, with subspaces and linear maps on an equal (diagrammatic) footing. The blog <graphicallinearalgebra.net> does just that.

As an elementary illustration of the basic principles, let us look at systems of linear equations. The idea is simple: a system of linear equations in the form $Ax=0$ can be expressed by simply plugging $\Wcounit$ into the right side of a diagram that encodes the matrix $A$ (Example <ref>), i.e., by the diagram $\tikzfig{kernel}$. For example,

\[  \begin{pmatrix} a & 1 & 0\\ b & 0 & 1\end{pmatrix} \begin{pmatrix} x_1\\ x_2\\x_3\end{pmatrix} = \begin{pmatrix} 0\\ 0\end{pmatrix}\quad \text{ becomes }\quad  \tikzfig{ex-kernel}\]

Computing a basis of the set of solutions then involves rewriting the diagram into a form from which any solution can be generated easily:

\[\tikzfig{ex-kernel-computation}\]

Here we find that the kernel of $A$ has dimension $1$, with basis vector, e.g., $\begin{pmatrix} 1 & -a & -b\end{pmatrix}^T$.

An interesting aspect of identifying the equational theory of a particular structure in a given semantic model is that we can find it again in a different model, and thereby identify seemingly unrelated algebraic objects as instances of the same abstract structure. For example, we have seen many different interpretations of Frobenius structures or bimonoids in different models (i.e. in different symmetric monoidal categories). Another common example is that of  groups and Hopf algebras, both instances of bimonoids in different symmetric monoidal categories (sets and functions with the Cartesian product for the former, and vector spaces and linear maps with the tensor product for the latter). Even a complicated theory such as IH occurs in other contexts than that of linear relations. Indeed, IH can be interpreted in in the category of vector spaces with the tensor product as monoidal product, where its models are closely related to the notion of complementary observables in quantum physics [34, 46].

[Cospans and corelations]
We have mentioned that cospans with the disjoint sum as monoidal product (Example <ref>) not only form a hypegraph category, but are the free hypergraph category on a single object (and no additional morphism). In the language of this section, this means that the theory of a special commutative Frobenius structure is sound and complete for (the interpretation $\sem{-}$ into) $(\Cospan{\fSet},+)$ <cit.>.

The proof of this fact is essentially the spider theorem from Example <ref>. This theorem gives a normal form from which we can uniquely read the corresponding cospan: any diagram of the free hypergraph category on a single object is fully and uniquely characterised by the number of disconnected components (spiders) and to which of these each boundary point is connected. That's it.

The only difference between corelations (also with the disjoint sum as monoidal product) and cospans is that the former do not allow empty equivalence classes (they are joint surjective cospans, as we saw). Diagrammatically, these correspond to isolated black dot: $\sem{\bullet} =\sem{\tikzfig{bunit-bcounit}}=\varnothing$.  Since a network of black generators is fully characterised by its number of legs, there is—up to the laws of special commutative Frobenius structure—only one such network: the single dot $\bullet := \tikzfig{bunit-bcounit}$. Thus, we need only add an axiom to remove isolated dots to obtain a complete theory for the SMC corelations: $\tikzfig{bunit-bcounit} = \idzero$. The resulting theory is that of extraspecial commutative Frobenius structures <cit.>.

§ OTHER TRENDS IN STRING DIAGRAM THEORY

§.§ Rewriting
When reasoning about programs, reductions of a program $p$ into another one $q$ are important objects of study: such reduction may witness for instance the evaluation of $p$ on a certain input (akin to $\beta$-reduction  in the $\lambda$-calculus [9]), or more generically its transformation into a simpler program $q$. When considering programs as terms of an algebraic theory, reductions are typically formalised as rewriting steps: we may apply a rewrite rule $l \Rightarrow r$ inside $p$ if the term $l$ appears as a subterm of $p$, in which case we say that the rule has a matching in $p$; if there is such a matching, then the outcome $q$ of the rewriting step is the term $p[r/l]$ obtained by replacing $r$ for $l$ in $p$.

When it comes to string diagrams, rewriting presents additional challenges, that we do not experience on terms. The crux of the matter is matching: as string diagrams are invariant under certain topological transformations—crossing of wires, shifting of boxes, etc.—we would like matchings to exist or not regardless of which graphical presentation we choose for our string diagram. For example, consider the rule

\[
\tikzfig{monoid-unitality-left}
\]

We claim the rule has a matching on the string diagram below left. However, strictly speaking, the matching isolates a subterm only when we `massage' the string diagram as on the right.

\[
\tikzfig{unitality-ex-deformed}
\]

More formally, the point is that string diagrams are equivalence classes of terms, modulo the laws of SMCs. We want to be able to match a rewriting rule $l \rightsquigarrow r$ on a string diagram $c$ whenever a term in the equivalence class of the string diagram $l$ appears as a subterm in the equivalence class of the string diagram $c$.

Let $\Sigma_0$ be a signature, $l \rightsquigarrow r$ be a rewrite rule of $\Sigma_0$-terms, and $c$ be a $\Sigma_0$-term. We say that $c$ rewrites into $d$ modulo $E$ if

\begin{equation}
\diagbox{c}{}{} =_E \diagbox{c'}{}{} \text{ and } \diagbox{c'}{}{} = \tikzfig{rewrite-l} \text{ and } \diagbox{d}{}{} = \tikzfig{rewrite-r}
\end{equation}

The standard case is when $E$ are the laws of SMCs, but the notion can be adapted to fit other categorical structures where string diagrams occur—cf. Section <ref>. This definition seems reasonable enough from a mathematical viewpoint. However, it is completely unpractical when it comes to implementing string diagram rewriting. Exploring the space of all $\Sigma$-terms equivalent to a given one is an expensive computational task, and if done naively it may even not terminate, given that on principle there are infinitely many equivalent terms to be checked for a matching. This is an issue especially because rewriting is the way we formally reason about string diagrams in a computer: whenever we want to apply the equations of a theory such as those considered in Section <ref>, the first thing to do is orienting such equations as rewrite rules.

The solution from this impasse comes from the combinatorial interpretation of string diagrams, as introduced in Section <ref>. Recall that, under that interpretation, a string diagram is always mapped onto a single open hypergraph. In other words, if $c$ is mapped onto $g$, and $c$ and $d$ are string diagrams equivalent modulo the laws of SMCs, then also $d$ is mapped onto $g$. This feature makes open hypergraphs suitable data structures to reason about string diagram rewriting: if we want to rewrite with a rule $l \rightsquigarrow r$ and a string diagram $c$ as above, we do not need to bother with the many equivalent syntactic presentations of these diagrams, but just need to consider the corresponding open hypergraphs. In fact, open hypergraphs do come with their own rewriting theory, called double-pushout rewriting [49]. The fundamental result linking double-pushout rewriting and syntactic rewriting is the following:

$c$ rewrites into $d$ modulo $\scFrob$ if and only if $\CspGraph{c}$ rewrites into $\CspGraph{d}$ modulo double-pushout rewriting.

\[
\tikzfig{monoid-unitality-left} \text{ is interpreted as the span }\:
\tikzfig{rewrite-dpo-unitality}\]

and therefore

\[
\tikzfig{monoid-unitality-ex} \: \text{ becomes } \: \tikzfig{rewrite-dpo-unitality-match}
\]

Example of how string diagram rewriting is interpreted as double-pushout rewriting. Intuitively, double-pushout rewriting matches the left-hand side of the rewrite rule to a subgraph and replaces it with the right-hand side. Here, the unitality rule of a monoid is applied in context.

Theorem <ref> is a consequence of the correspondence established by Theorem <ref> between string diagrams modulo Frobenius structure and open hypergraphs. However, it is not completely satisfactory: we would like to interpret faithfully rewriting modulo the laws of SMCs, without the need of considering Frobenius equations too. It turns out it is still possible to obtain a correspondence, with a more restrictive notion of double-pushout rewriting, called convex.

$c$ rewrites into $d$ modulo the laws of SMCs if and only if $\CspGraph{c}$ rewrites into $\CspGraph{d}$ modulo convex double-pushout rewriting.

We omit the details of the definition of convexity, which would require us delving into the theory of double-pushout rewriting, and refer the interested reader to the overview of string diagram rewriting offered in [15].

The above two theorems settle the question of rewriting for string diagrams in symmetric monoidal categories (Theorem <ref>) and hypergraph categories (Theorem <ref>). However, as we saw in Section <ref>, there are other  structures for which we can draw string diagrams considered both of lower and higher complexity. Among the ones we have covered here, the question is not settled for monoidal, braided monoidal, traced monoidal, (self-dual) compact closed, and Cartesian monoidal categories. It has been answered recently in [90] for copy-delete monoidal categories[The work [58], which appeared at the same time as [90], also establishes the correspondence between string diagrams in copy-delete categories and suitably defined open hypergraphs, but without considering the rewriting angle.], and in [65] for traced copy-delete categories. Finally, we point out the recent work [3], which studied rewriting for monoidal closed categories: classes of monoidal categories with a `function space' which are relevant to the semantics of programming languages.

§.§ Higher-Dimensional Diagrams

The string diagrams we have presented in this survey are a particular case of a more general notation for higher-categories. It is helpful to highlight the connection. First, we need to explain what a $n$-category is. We will not do this here with any degree of rigour as this is not the topic of this survey. Instead, we will limit ourselves to giving some intuition and explain the link between their graphical language(s) and string diagrams. The reader should also know that there are several competing definitions of $n$-categories and that our lack of precision allows us to avoid committing to any one definition.

Very roughly, a $n$-category is a category that may have $2$-morphisms between morphisms, 3-morphisms between 2-morphisms etc. For example, in a 2-category there can be 2-morphisms between morphisms:

\[\begin{tikzcd}
A \arrow[r, bend left, "f", ""{name=U, inner sep=1pt, below}]
\arrow[r, bend right, "g"{below}, ""{name=D, inner sep=1pt}]
& B
\arrow[Rightarrow, from=U, to=D, "\phi"]
\end{tikzcd}\]

Like categories, 2-categories also admit a visual representation that generalises string diagrams, called surface diagrams: objects are represented as (labelled/coloured) regions of space, morphisms as (labelled) strings or wires, and 2-morphisms as (labelled) dots.

\[\tikzfig{2-cell}\]

Let us see how these compose. There are two ways, just like there are two directions of composition for string diagrams:

\[\begin{tikzcd}
A \arrow[r, bend left, "f", ""{name=f, inner sep=1pt, below}]
\arrow[r, bend right, "g"{below}, ""{name=g, inner sep=1pt, above}]
& B \arrow[r, bend left, "p", ""{name=p, inner sep=1pt, below}]
\arrow[r, bend right, "q"{below}, ""{name=q, inner sep=1pt, above}]
& C
\arrow[Rightarrow, from=f, to=g, "\phi"]
\arrow[Rightarrow, from=p, to=q, "\psi"]
\end{tikzcd}
\qquad\quad \tikzfig{2-cell-horizontal-comp}\]

and vertically

\[\begin{tikzcd}
A \arrow[r, bend left=50, "f", ""{name=f, inner sep=1pt, below}]
\arrow[r, "g"{name=g, anchor=center, fill=white}]
\arrow[r, bend right=50, "h"{below}, ""{name=h, inner sep=1pt, above}]
& B
\arrow[Rightarrow, from=f, to=g, "\phi", shorten <=0.5pt]
\arrow[Rightarrow, from=g, to=h, "\psi", shorten <=0.5pt]
\end{tikzcd}
\qquad\quad \tikzfig{2-cell-vertical-comp}\]

The identity (1-)morphism $id_A: A\to A$ can be depicted as a single-coloured region of 2D space, while the identity 2-morphism $id_f: f\Rightarrow f$ can be depicted as a plain wire separating the domain and codomain objects of $f: A\to B$:

\[\tikzfig{id-2-cell}\]

For these diagrams to make sense, horizontal and vertical compositions should satisfy additional associativity and unitality requirements, much like those of (1-)categories. In addition, for the diagrams to work, horizontal and vertical composition need to interact nicely; 2-categories should also verify a form of interchange law between horizontal and vertical composition. This law says that the two ways of decomposing the following diagram are equal:

\[\tikzfig{interchange-2-cells}\]

There is a surprising correspondence between certain 2-categories and monoidal categories: a monoidal category is simply a 2-category with a single object! Take the 2-morphisms to be the ordinary morphisms of the corresponding monoidal category, the 1-morphisms to be its objects, and the monoidal product to be composition of 1-morphisms. Diagrammatically, we can simply depict the single object as the (white in this paper, but feel free to pick a nicer colour) background on which we draw our diagrams. In this sense, 2-categories can be thought of as typed monoidal categories (where the monoidal product cannot be applied uniformly, but has to match at the boundary 1-morphisms).

Note however that this correspondence is limited to monoidal categories, without any braiding or symmetry. To recover the ability to swap wires of symmetric monoidal categories a lot more structure is required. Intuitively this is because, strictly speaking, if all we have are two dimensions of ambient space, wires cannot cross—what would that even mean? Braidings can occur in at least three dimensions where it makes sense to ask the question of which wire went over or under which other wire. This is why we need to move from 2-categories to 3-or more-categories. This may sound complicated, but just like 2-categories have morphisms between morphisms, we can define 3-categories, which have 3-morphisms between 2-morphisms, 4-categories, which have 4-morphisms between 3-morphisms etc. Each of these come with different ways of composing $n$-morphisms. As it turns out, braided or symmetric monoidal categories, and their graphical languages can be recovered as special cases of  degenerate 3-and 4-categories, respectively. More precisely, a braided monoidal category is a 3-category with only a single object and (1-)morphism, while a symmetric monoidal category is a 4-category with a single object, 1-and 2-morphism. Phew! These correspondences are known as the periodic table of $n$-categories  [7].

One last point: the category of categories is itself a 2-category in which objects are categories, (1-)morphisms are functors, and 2-morphisms are natural transformations between them. The graphical language of 2-categories can therefore be used to present key concepts in category theory. For an excellent introduction to category theory using this diagrammatic language (and an excellent introduction to the diagrammatic language of 2-categories itself) we warmly recommend [88].

§.§ Inequalities

In the same way that we can reason equationally about string diagrams (see Section <ref>), it is also possible to reason with inequalities. From the syntactic point of view, the changes are minimal: we can define theory with inequalities in the same way that we defined equational theories (equalities are recovered as two inequalities in both directions). To interpret inequalities requires a SMC with an order between the morphisms of the semantics that is coherent with the rest of the structure (composition, monoidal product etc.). More formally, we need a SMC in which the morphisms are partially ordered and for which the composition and monoidal product are monotone. This kind of structure appears naturally in the examples of relations that we have covered above, where morphisms can be ordered by inclusion: for two relations $R,S\from X\to Y$, we write $R\leq S$ if $R$ is included in $S$ as a subset of $X\times Y$. If we look at inequalities, some fascinating structure starts to emerge.

[Cartesian bicategories]
Cartesian bicategories [28] are SMCs in which each object $X$ has a distinguished monoid and comonoid structures, which we draw as $\Bmultn{X},\Bunitn{X}$ and $\Bcomultn{X},\Bcounitn{X}$, respectively. These have to satisfy the following additional axioms[The categorically-minded reader will notice that these define an adjunction in the 2-categorical sense, between the comonoid and monoid structure, between $\Bcomult$ and $\Bmult$ on the one hand, and $\Bcounit$ and $\Bunit$ on the other.]:

\begin{equation}\label{eq:Cartesian-bicategories}
\tikzfig{bmult-bcomult}\leq \tikzfig{2-id}\qquad \idx{}\leq \tikzfig{copy-special}\qquad
\idx{}\leq \tikzfig{bcounit-bunit} \qquad \tikzfig{bone-black}\;\leq\;\tikzfig{empty-diag}
\end{equation}

The SMC of monotone relations (Example <ref>) is an example of a Cartesian bicategory, with monoid-comonoid pair given by those of (<ref>)-(<ref>) for each pre-ordered set $(X,\preceq)$. Note however that these, as we have seen, do not form a Frobenius structure in general. In fact, one can show that this is only the case when the underlying partial order is given by equality. In other words, the objects $X$ in the category of monotone relations for which $\Bmultn{X},\Bunitn{X}$ and $\Bcomultn{X},\Bcounitn{X}$ form a Frobenius structure are just plain sets and monotone relations between them are just ordinary relations! This precisely characterises the SMC of relations within the larger SMC of monotone relations.

We can characterise other well-known structures in this SMC. For example,  we can require that there exists two more generators on the same object $X$—that we write $\Wmultn{X},\Wunitn{X}$ such that the dual of the inequalities (<ref>) hold:

\[\tikzfig{2-id}\:\leq\:\tikzfig{wmult-bcomult}\quad\qquad \tikzfig{bcomult-wmult}\leq \idx{}\quad \qquad \tikzfig{bcounit-wunit}\;\leq\;\idx{}\quad \qquad \tikzfig{empty-diag}\;\leq\; \tikzfig{wunit-bcounit} \quad
\]

A set equipped with this structure in the SMC of monotone relations is precisely a semi-lattice whose binary meet and top can be identified with  $\Wmultn{X}$ and $\Wunitn{X}$ respectively. To get a lattice, we need to add $\Wcomultn{X},\Wcounitn{X}$ satisfying the same inequalities:

\[\tikzfig{2-id}\:\leq\:\tikzfig{bmult-wcomult}\quad\qquad \tikzfig{wcomult-bmult}\leq \idx{}\quad \qquad \tikzfig{wcounit-bunit}\;\leq\;\idx{}\quad \qquad \tikzfig{empty-diag}\;\leq\; \tikzfig{bunit-wcounit} \quad
\]

One might also wonder how $\Wmult,\Wunit$ and $\Wmult, \Wunit$ interact. For an arbitrary lattice, there is not much one can say. However, when the lattice is a Boolean algebra, they form a commutative  Frobenius structure!

§.§ Relationship with Proof Nets

Readers who have encountered proof nets before might wonder if there is a relationship with string diagrams. Given that proof nets are a graphical proof system for (multiplicative) linear logic [67] and that the natural categorical semantics for linear logic takes place in monoidal categories [89], there should be a connection between the two. However, classical multiplicative linear logic usually requires two different monoidal products: one for the multiplicative conjunction, usually written $\otimes$, and one for the multiplicative disjunction, usually written $\parr$. These have  nontrivial interplay, axiomatised in the notion of linearly (or weakly) distributive category [33]; if we also want a classical negation, they are related via the usual DeMorgan duality, and the relevant semantics given by $*$-autonomous categories [10].

The problem is that our diagrams already use two dimensions—one for the composition operation and one for the monoidal product. How should we deal with two monoidal products? There are different answers. The first (though not the first one historically) is to move one dimension up, from string diagrams in two-dimensional space, to surface diagrams in three-dimensional space. This is what the authors in [48] propose.

However, if we prefer to retain the typesetting ease of a two-dimensional notation, proof nets come to the rescue. Unlike standard string diagrams (for strict SMCs that is) proof nets include explicit generators for the two monoidal products[Note that, in the literature, proof nets are usually depicted going from top to bottom, but we prefer to maintain our convention here in order to make the link with string diagrams clearer.]

\[\tikzfig{otimes}\quad\qquad \tikzfig{par}\]

Like for compact closed categories, we also need cups and caps satisfying the usual snake equations, which the proof net literature tends to depict as undirected:

\[\tikzfig{cup-cap-ll}\]

However, not all diagrams we can draw in the free SMC over these generators are proof nets, in the sense they do not necessarily denote well-formed proofs in linear logic. For example, the following diagram is not a proof net and its conclusion ($A\otimes A^*$) is not a theorem of linear logic:

\[\tikzfig{non-proof-net}\]

This is why we need an additional criterion to distinguish correct proof nets among all the diagrams we are allowed to draw. There are several such criteria in the literature, under the name of correctness criteria [67, 40]. We will not cover these criteria here—the reader should just know that they usually boil down to detecting some form of acyclicity in graphs derived from the string diagram.

Proof nets can also be understood as a two-dimensional shadow of the natural three-dimensional notation used to represent both monoidal products in [48]. This projection comes at a cost: not all two-dimensional diagrams are shadows of a three-dimensional surface. Correctness criteria can therefore be seen as conditions guaranteeing that a proof net is the projection of some higher-dimensional surface diagram.

In the most degenerate cases (from the logic perspective), $\otimes = \parr$, and we are left with the diagrammatic language of compact closed categories (Section <ref>).

§.§ Software

With the spread of diagrammatic reasoning, it is natural to wonder to what extent it may be automated, and more generally how computers can assist humans in manipulating string diagrams. There are several tools dedicated to this task, each with their specific focus and area of predilection. Here is a (non-exhaustive) list.

* Cartographer [103] deals with string diagrams for SMCs, the central concept of this introduction. It allows the user to specify arbitrary theories in this setting, and rewrite with them. String diagram rewriting is implemented as DPO hypergraph rewriting, following the approach of Section <ref>.

* Chyp (available at <https://github.com/akissinger/chyp>) is an interactive proof assistant for free SMCs over some signature and equational theory. The application works both with a conventional term syntax and with string diagrams. It also supports a hole-directed rewriting of terms (in the style of Agda).

* DisCoPy [42] is a Python library that defines a DSL for diagrams given by either, a free monoidal category or a free SMC over some signature. Furthermore, DisCoPy allows the user to define a semantics for diagrams, that is, to define functors out of free (symmetric) monoidal categories— through these, diagrams can be evaluated to some Python programs (as linear maps, for example). Note however that the package does not act as a proof assistant for diagrammatic equational theories, contrary to some of the other tools in the list.

*  (itself the successor of a tool known as Globular [106])  is a more general tool that allows the user to construct finitely-generated $n$-categories. As a result, it is possible to encode string diagrams for SMCs into  (using a correspondence that we have briefly covered in Section <ref>). However, the increased generality comes at the cost of significant sophistication: the user has to explicitly use the laws of SMCs in proofs, having to show the functoriality of the monoidal product by sliding two generators past each other, for example, instead of the two diagrams being equal.

*  [68] is a Python library for higher-dimensional diagrammatic rewriting in which it is possible to, among other applications to algebraic topology and algebra, build presentations of higher and monoidal categories. For SMCs, this requires an encoding similar to what  was needed with . As a bonus,  can generate TikZ output to embed diagrams directly into a  document.

* Quantomatic [81] is one of the earliest tools, which deals with a restricted subset of signatures (initially motivated by the ZX-calculus, see the paragraph on quantum physics in Section <ref>), namely signatures containing only commutative operations in compact closed categories. It allows the user to specify theories and rewriting strategies, as well as higher-order rules using so called !-boxes.

An important theoretical question for the above tools is which data structures best implement string diagrams and diagrammatic reasoning. Considering that string diagrams themselves are quotients of terms, it is a non-trivial task to represent their manipulation efficiently. This question has been explored recently in [110, 107].

Finally, if one is exclusively interested in the typesetting of string diagrams into documents, we mention the TikZ library, which is especially convenient when paired with TikZit (<https://tikzit.github.io/>), a GUI editor designed to handle PGF/TikZ pictures.

§ STRING DIAGRAMS IN SCIENCE AND ENGINEERING: SOME APPLICATIONS

In the last few years, string diagrams have found application in several different fields of science and engineering. This section is intended as a succinct overview of such applications, with the main aim of providing to the reader references for a more focussed study. Clearly, a survey of this type cannot possibly begin to cover all the relevant material, and it will necessarily be a partial account. Our perspective will be pedagogical rather than historical: we will typically point to the most recent surveys and introductory materials, when available. A comprehensive literature review, including a rigorous reconstruction of “who did what first”, is out of our scope.

Many of the applications that we will describe share the same methodology. They involve noticing that the kind of systems and/or processes which constitute the focus of a given research area can be understood as the objects and/or morphisms of some SMC. This opens up the possibility of studying the topic from a functorial standpoint, using string diagrams as a syntax and the relevant systems and/or processes as semantics. In many cases the same approach also also opens up the possibility of studying the equational properties of the resulting diagrammatic language. In some particular cases (this does not apply to all examples below), a universal set of generators can be found for the syntax and, if we are even luckier, the equational theory can be axiomatised by a complete monoidal theory.

It is fitting that we should start this section by applications of string diagrams in physics, since one of their ancestors were invented by Penrose to carry out the complex tensor calculations involved in the differential geometry of general relativity [96], see [95] for a more recent overview.

Quantum Physics.
One of the most outstanding modern applications of diagrammatic reasoning has been to quantum computing.

Mathematically, quantum systems are modelled as Hilbert spaces, where joining two systems is represented by taking the tensor product of the respective spaces, and processes acting on a system are linear (unitary) maps. Linear maps between Hilbert spaces with the tensor product as monoidal product form a SMC, and are thus amenable to a string diagrammatic study.

There are several diagrammatic calculi to reason about linear maps between qubits (represented as vector spaces of dimension $2^d$ for some natural $d$) with the tensor product as monoidal product. These generalise and formalise the circuits representation that is ubiquitous in quantum computing. The first and most well-known such calculus is the ZX-calculus: its diagrams consist of nodes of two different colours[Traditionally, green and red, but white and gray have been used more recently, for accessibility.] called spiders, each labelled by an angle:

\[\tikzfig{z-spider} \qquad \tikzfig{x-spider}\]

The two colours denote one of two classical observables or measurement bases—the Z (or computational) basis and X (or Hadamard) basis respectively—and the angle denotes a phase relative to this basis, i.e. a rotation of the Bloch sphere along the axis determined by the chosen observable.

Equationally, the spiders form a special commutative Frobenius algebra and the two colours interact with each other to form bimonoid (more specifically, a Hopf algebra which is to a bimonoid what a group is to a monoid). Together with some other more complex equalities, the ZX-calculus completely axiomatises linear maps between qubits so that any semantic equality can be obtained by purely equational reasoning at the level of the diagrams themselves.

Because the ZX-calculus generalises quantum circuits, its axiomatisation provides a completely equational way to reason about those. Reasoning equationally at the level of circuits is much more difficult, so the ZX-calculus provides a more compositional setting in which to study the behaviour of circuits. In fact, one of its most successful applications has been to quantum circuit synthesis and simplification. Given some measure of complexity of circuits (usually based on the cost of implementing certain gates in a lab) one can compile a given circuit to its corresponding ZX diagram and simplify it using the axioms of the calculus, with the important caveat that one needs to guarantee that a bona fide circuit can be recovered at the end. (There are many technical papers on this topic; we could not find a more accessible survey, though the general introduction [105] contains some pointers to the literature.) String diagrams have now reached the mainstream quantum computing community, as even one of the founders of the field has adopted the ZX-calculus in a recent preprint [79].

\[\tikzfig{ghz-circuit}\;\;\mapsto\;\;\tikzfig{ghz-preparation}\]

The quantum circuit on the left prepares the GHZ state $\ket{000}+\ket{111}$; the ZX-calculus derivation is a diagrammatic proof of this (unlabelled spiders have $0$ phase and the square box is a Hadamard gate). See <cit.> for similar examples of ZX-calculus proofs.

There are other calculi with the same target semantics—linear maps between qubits—with different sets of generators as building blocks. The ZW-calculus was the first for which a completeness result was found and was instrumental in deriving a complete equational theory for the ZX-calculus (by translating one into the other). Its generators are further from the conventional gates of the classical quantum circuit model, but closely related to linear optical quantum circuits [41, 98].  This last reference builds a calculus that unifies both ZX-and ZW-calculus and is shown complete for arbitrary dimension. The ZH-calculus is a variation of the ZX-calculus with which it is easier to represent certain multiply-controlled logic gates, like the Toffoli or AND gates (on the computational basis), and other related operations.

For a diagrammatic introduction to quantum computing and the foundations of quantum theory, the reference textbook is [35]. Alternatively, [71] provides a complementary (and more categorically minded) approach to some of the same topics. A comprehensive survey of the ZX-calculus (and its cousins) for the working computer scientist can be found in [105].
Beyond these, there is a wealth of recent developments that have taken the original work in different directions: a calculus which incorporates finite memory elements to the ZX-calculus [29], several calculi for quantum linear optical circuits [41, 31], and more... There are also automated tools to reason about large-scale ZX diagrams: the python library PyZX which we have already mentioned is the most recent [80]. Finally, the website <https://zxcalculus.com/> contains tutorials, a helpful guide to the publications in the field and even a map of ZX research community.

Signal flow graphs and control theory. Engineers and control theorists have long expressed causal flow of information between different components of a system by graphical means. One popular formalism is that of signal flow graphs, sometimes called block diagrams. They are directed graphs whose nodes represent system variables and edges functional dependencies between variables. They are used to represent networks of interconnected electronic components, amplifiers, filters etc. In signal flow graphs, cycles represent feedback between different parts of the system.

\[\tikzfig{fibonacci-gf} = \tikzfig{fibonacci-gf-1}=\tikzfig{fibonacci-gf-2}= \tikzfig{fibonacci-gf-3}\]

Steps of a derivation transforming the Fibonacci generating function $\frac{x}{1-x-x^2}$ into a signal flow graph [22]. The $x$ can be interpreted as derivation in the field $\R(x)$ of rational functions or as a time delay. Note that both the specification (on the left), the signal flow graph which realises it (on the right), and the intermediate steps are all string diagrams of the same calculus, and all the steps apply laws of IH over $\R(x)$.

Giving signal flow graphs a functorial semantics, required a change of perspective: instead of only allowing functional dependencies between variables, we can generalise signal flow graphs to allow relational dependencies between them, i.e. arbitrary systems of (usually linear) equations. This is entirely consistent with the underlying physics, where laws tend to express relationships between variables, without any explicit assumption about the direction of causality. This change of perspective allowed the reinterpretation of the fundamental building blocks of signal flow graphs as relations, their connection as relation composition, and their juxtaposition as taking the Cartesian product of the corresponding relations. In other words, these generalised signal flow graphs are string diagrams for a sub-category of the category of sets and relations! One important such subcategory is that of vector spaces over a field and linear relations – subset of the product that are also linear subspaces – between them. It turns out that signal flow graphs are intimately related to linear relations over the field of rational functions over $\R$. The connection was established independently in [21, 22]  and [5], where the authors also give a complete equational theory, called Interacting Hopf Algebra (IH) by the first set of authors, to reason about the behaviour of these systems entirely diagrammatically. Since these early developments, the theory IH has been employed to reason algebraically about various tasks related to signal flow graphs: we mention the realisability of rational behaviours as circuits [21], semantic refinement [16], and a compositional criterion for controllability [54].
The interested reader should note however that there are some subtle discrepancies between this generalisation of signal flow graphs and the standard control-theoretic interpretation of their behaviour: an more accurate, but closely related semantics in terms of bi-infinite streams is given in [54], along with a complete equational theory.

Finally, linear relations are not just important because of the relationship with signal flow graphs; more generally the diagrammatic calculus and the equational theory IH provide a playground in which a substantial amount of standard linear algebra can be reformulated entirely diagrammatically. The blog <graphicallinearalgebra.net> is a great introduction  to this topic, aimed at a general audience.

Circuit Theory. String diagrams are particularly compelling where they can give an algebraic foundation to existing graphical representations that are usually treated purely combinatorially. This is the case of many existing approaches to electrical or digital circuits. Despite the existence of a standard graphical representation for circuits, the string diagrammatic approach is not without challenges: taking the original graphical representation as a starting point, one needs to decompose them into a an suitable set of generators from which all other circuits can be built and, more importantly, give this syntax a functorial interpretation that assigns to each circuit its intended behaviour. In traditional introductions to electrical circuits, this last step usually appeals informally to some intuitive connection between a circuit and the set of differential equations that it specifies. String diagrams can make this connection precise and compositional. In some particular cases, it is even possible to equip the resulting syntax with a complete equational theory that axiomatises semantic equivalence of circuits.

For electrical circuits with linear/affine behaviour (including resistors, inductors, capacitors, for example) this ambitious goal has not yet been achieved, though it is possible to compile them down to an intermediate representation in IH (or its affine extension) for which, as mentioned in the paragraph above, we do have a complete diagrammatic calculus. The case of circuits with passive components is treated in [6] while the extension to active components (current and voltage sources in AC regime only) is carried out in [18]. Building on this, [12] develop a convenient calculus that blends both circuit elements and their compilation in IH, cf. Figure <ref>. The resulting language allows for entirely diagrammatic proofs of standard textbook results of electrical engineering such as the superposition theorem or Thévenin/Norton's theorem.

\[
\begin{tikzpicture}[color=blue]
\draw (-1,0) -- (0,0);
\draw (0,0) -- (0,1);
\node[elecdot] at (0,0) {};
\draw (0,0) -- (0,-1);
\draw (0,1) to[R=$R_1$] (4,1);
\draw (0,-1) to[R=$R_2$] (4,-1);
\draw (4,1) -- (4,-1);
\node[elecdot] at (4,0) {};
\draw (4,0) -- (5,0);
\end{tikzpicture}
= \tikzfig{parallel-resistors-unboxed}
= \tikzfig{parallel-resistors-unboxed-1} = \tikzfig{parallel-resistors-unboxed-2} = \begin{tikzpicture}[color=blue]
\draw (0,0) to[R=$\frac{R_1R_2}{R_1+R_2}$] (3,0);
\end{tikzpicture}
\]

Deriving textbook properties of electrical circuits by compiling them to graphical linear algebra—the black diagrams represent the voltage-current pairs enforced by elements of the circuit [12].

For digital circuits, there are many possible variants of interest to consider, each at their own level of abstraction (and each, with their own limitations). The simple case of acyclic circuits consisting only of logic gates, without any memory elements, reduces to boolean algebra and thus defines a Cartesian monoidal category, which can be presented by the symmetric monoidal version of the algebraic theory of boolean algebras, with only minor adaptations (as explained in Section <ref>, in particular Remark <ref>)—details can be found in the pioneering [83].

More complex cases, involving delays or cycles are more delicate and no comprehensive account has ever  been given. Recently, the sequential synchronous (i.e. where a global clock is assumed to define the time at which signals can meaningfully change) case has found a complete axiomatisation in [66]. Notably, this work also allows combinational (that is, without any delay) cycles in the syntax. This feature is usually avoided in traditional treatments of digital circuits because of the difficulty of handling these types of cycles compositionally. The case of asynchronous (cyclic) circuits remains elusive and an important open problem, although some work has been done in this direction [64].

Probability and statistics.
Issues with the encoding of probability theory in set-theoretic measure theory have pushed researchers to develop a different, synthetic approach to probability theory. In recent years, some have sought alternative categorical foundations.

One approach studies categories of measurable spaces and Markov kernels (conditional probability measures) in an attempt to find an axiomatic setting for probability theory. This category is not only symmetric monoidal but a CD category. Moreover, in general, its morphisms satisfy only the (del) equation below:

\[\tikzfig{Lawvere-distributive-copy}\; \myeq{dup}\; \tikzfig{Lawvere-distributive-copy-1} \qquad \qquad \tikzfig{Lawvere-distributive-del}\;\myeq{del}\;\Bcounitn{v} \]

At the semantic level, this equation simply means that conditional probabilities are measures that normalise to $1$. Crucially, not all morphisms satisfy the (dup) equation above, so that categories of Markov kernels are not Cartesian; those morphisms that can be copied and do satisfy (dup) are precisely deterministic kernels, i.e. those that, given a element of their domain, map it to a single element in their codomain with probability one. We already see that a few elementary properties of random variables can be expressed in these categories, called Markov categories; their string diagrams for Markov categories give a graphical language to treat standard properties such as conditional independence, disintegration, almost sure properties, sufficient statistics and more. The interested reader will find [56] to be a good introduction to the topic, with applications to statistics.

\[\tikzfig{ex-bayesian-net-diag}\quad \mapsto \quad \tikzfig{ex-bayesian-net-intervention}\]

In [73], the authors model a scenario in which we seek to identify the causal effect of smoking on cancer. Here, string diagrams represent generalised Bayesian networks, encoding causal dependencies between a set of variables. The prior is $\omega$, the joint probability distribution of smoking (variable $S$), presence of tar in the lungs (variable $T$), and developing cancer (variable $C$). A tobacco company contends that, even though there is a statistical correlation between $S$ and $C$, there might be some confounding factor $H$ (perhaps genetic) which causes both smoking and cancer (decomposition of $\omega$, on the left). How can we rule out this causal scenario, when direct intervention is impossible? We see that performing a `cut' at $S$ and replacing it with the uniform distribution ($u$), as on the right, would remove any confounding influence of $H$ over $S$. In this case, we can infer from the structure of the diagram that the distribution corresponding to the resulting diagram $\omega'$ can be computed from observational data only. If, under $\omega'$, a smoker is still more likely to develop cancer, then we have demonstrated that there is a causal relationship between $S$ and $C$.

Much like the existing graphical methods of Bayesian networks and related representations, string diagrams make the flow of information between different variables explicit, highlighting structural properties, such as (conditional) independence. In fact, this connection was already explored in [50] which gave a functorial account of Bayesian networks. Around the same time, the authors of [37] proposed a diagrammatic calculus for Bayesian inference. Since then, a surprising amount of probability theory has been recast in this synthetic mold:   a growing list of results have been reproven in this more general setting, many of which use string diagrams to streamline proofs, including zero-one laws [59], de Finetti theorem [57], the ergodic decomposition theorem [91], and more.

The same diagrams (in Markov or CD categories) also allow for a treatment of standard concepts in causal reasoning. In [73], the authors give a diagrammatic account of interventions and a sufficient criterion to identify when a given causal effect can be reliably estimated from observational data, see Figure <ref>. The recent [84] extends this work to counterfactuals and shows how causal inference calculations can be carried out fully diagrammatically. Beyond its pedagogical value, one advantage of the diagrammatic approach is that it is axiomatic: as such, it is not restricted to the category of Markov kernels, but applies in all categories with the relevant structure.

Machine Learning with Neural Networks. Having mentioned string diagrammatic treatments of Bayesian networks, it is natural to wonder about analogous studies of neural networks, another chief graphical model of machine learning. Categorical approaches to these structures are fairly recent — see e.g. [102] for an overview — and so far have mainly focussed on providing a formal account of the gradient-based learning process — see in particular [55, 39, 62]. Use of string diagrams to describe the network structure only cursorily appear in [55]. String diagrams are heavily used in [39] to represent the categorical language of lenses in the context of machine learning, but presentations by generators and equations of these diagrams are not investigated. The works on gradient-based learning with “quantised” versions of neural networks, such as Boolean circuits [109] and polynomial circuits [111], adopt string diagrams in a more decisive way. These works define reverse derivatives compositionally on the diagrammatic syntax for circuits, building on the theory of reverse derivative categories [32] and Lafont's algebraic presentation of Boolean circuits [83]. Going forward, the expectation is that such an approach may work also for real-valued networks, once the different neural network architectures are properly understood in terms of algebraic presentations. A starting point is provided in [55] for feedforward neural networks — see also the diagrammatic presentation of piecewise-linear relations found in [11], which may be used to model ReLu activation units. Another important research thread concerns automatic differentiation (AD): the work [4] uses rewriting of string diagrams in monoidal closed categories to describe an algorithm for AD and prove its soundness. In this context, string diagrams are appealing as they can be reasoned about as a high-level language, while at the same time exhibiting the same information of lower-level combinatorial formalisms, which in traditional AD are introduced via compilation. Finally, the webpage [61] is recommended as it maintains a list of papers at the intersection of category theory and machine learning.

Automata Theory.

Automata have always been represented graphically, as state-transition graphs. However, the graphical representation is usually treated as a visual aid to convey intuition, not a formal syntax.  Kleene introduced regular expressions to give finite-state automata an algebraic syntax. Their equational theory—under the name of Kleene algebra—is now well-understood and multiple complete axiomatisations have been given, for both language and relational models.

With string diagrams however, it is possible to go directly from the operational model of automata to their equational properties, without going through a symbolic algebraic syntax [97]. This approach lets us axiomatise the behaviour of automata directly, freeing us from the necessity of compressing them down to a one-dimensional notation like regular expressions.
In addition, embracing the two-dimensional nature of automata guarantees a strong form of compositionality that the one-dimensional syntax of regular expressions does not have. In the string diagrammatic setting, automata may have multiple inputs and outputs and, as a result, can be decomposed into subcomponents that retain a meaningful interpretation.
For example, the Kleene star can be decomposed into more elementary building blocks—generators of some monoidal signature—which come together to form a feedback loop:

\[\tikzfig{star-decomposed}\]

A similar insight was already present in the work of  Stefanascu [104] who studied the algebraic properties of traced monoidal categories (cf. Section <ref>) with several additional axioms in order to interpret automata, flowchart schemes, Petri nets, data-flow networks, and more.

Databases and Logic. As we have discussed above in several places, string diagrams are a convenient syntax for relations. They are particularly well-suited to conjunctive queries, the first-order language that contains relation symbols, equality, truth, conjunction, and existential quantification. This is a core fragment of query languages for relational databases with appealing theoretical property, such as NP-completeness (and thus, decidability) of query inclusion. Moreover, it admits a flexible diagrammatic language, which is exactly that of Cartesian bicategories (Example <ref>). These were introduced in [28] in the 1980s (without a diagrammatic syntax, most likely for typesetting reasons, though the authors give an axiomatisation that is easy to translate to string diagrams). The precise connection with conventional conjunctive query languages is worked out in [19]. More recently, the authors of [70] have generalised these diagrams to all of (classical) predicate logic. This requires adding boxes that represent negation to the diagrams of [28, 19].

Computability Theory.  Computers are machines that can be programmed to exhibit a certain behaviour. The range of behaviours that they can exhibit (its processes) can be axiomatised into a monoidal category with additional properties: we require that every process the machine can perform has a name—its corresponding program—encoding the intentional content of the process. In turn, the category contains distinguished processes—called evaluators—which , given a program and an input state of the machine, runs the program on the given input. These  simple requirements, with the ability to copy and delete data, are what [93] calls a monoidal computer. This structure is sufficient to reproduce a substantial chunk of computability (and complexity) theory using string diagrams. A textbook that does just that can be found online [94].

Concurrency. Concurrency lends itself to graphical methods, a fact noticed early by Petri. Initially, like so many other graphical representations, Petri nets were treated monolithically, and little attention was given to their composition. Once again, it is possible to take Petri nets seriously as a diagrammatic syntax with a functorial semantics. There are several ways to do so: one can either compose Petri nets along shared state (places) or shared actions (transitions). The  former was developed in [8], while the latter was initiated in [26, 27]. The authors have contributed to developing this last approach further, by studying and axiomatising the algebra of Petri net transitions [17]. Significantly, the syntax is the same as that of signal flow graphs (see above)—only the semantics changes, replacing real numbers (modelling signals) with natural numbers (modelling non-negative finite resources like the tokens of Petri net). This simple change also changes the equational theory dramatically.

String diagrams have made a surprising appearance in formal linguistics and natural language processing. The core idea relies on a formal analogy between syntax and semantics of natural language. On the semantic side, vectors (in other words, arrays of numbers) are a convenient way of encoding statistical properties of words or features (word embeddings) extracted from large amounts of text by training machine learning model. The semantics obtained in this way is often called distributional.

On the syntactic side, various formal structures of increasing complexity have been used to study the grammatical properties of languages and explain what distinguishes a well-formed sentence from an incorrect one.

Reconciling—or rather, combining the insights of—these two perspectives has been a long standing problem. One possible approach is premised on a formal correspondence between grammatical structure and distributional semantics: both fit into monoidal categories! We have already seen before that vector spaces and linear maps form a SMC, with the tensor as monoidal product. Similarly, formal grammars can be recast as certain (non-symmetric) monoidal categories in which objects are parts-of-speech (think nouns, adjectives, transitive verbs etc.) and morphisms derivations of well-formed sentences. The analogy allows for a functorial mapping from one to the other. With this correspondence in place, it becomes possible to interpret grammatical derivations of sentences as string diagrams in the category of vector spaces and linear maps. This gives a compositional way to build the meaning of sentences from the individual meaning of words. Moreover, algebraic structures with the right properties can model grammatical features of language whose distributional semantics is less clear. Relative pronouns, for example, have been successfully interpreted as certain Frobenius algebras [99, 100], allowing equational reasoning about the meaning of sentences that contain them.

Game Theory. In classical game theory, games and their various solution concepts are usually studied monolithically. Remarkably, a compositional approach was shown possible in [63]. In this paper, the authors build games from smaller pieces, called open games. An open game is a component that chooses its next move strategically, given the state of its environment and some counterfactual reasoning about how the environment might react to its move (and what payoff it would derive from it). They form a SMC with an interesting diagrammatic syntax which contains forward and backward flowing wires (the latter represent this counterfactual reasoning, flowing from future to present). In fact, these diagrams are related to those for lenses, which we have encountered in the paragraph on machine learning. Closed diagrams represent classical games, whose semantics is given by the appropriate equilibrium condition. Initially developed only for standard games with pure Nash equilibria as solution concept, open games have been extended to more general settings, such as Bayesian games [13] with the appropriate solution concept.

[1]
Samson Abramsky.
Retracing some paths in process algebra.
In CONCUR'96 Proceedings, pages 1–17. Springer, 2005.

[2]
Samson Abramsky.
No-cloning in categorical quantum mechanics.
Semantic Techniques in Quantum Computation, pages 1–28, 2009.

[3]
Mario Alvarez-Picallo, Dan R. Ghica, David Sprunger, and Fabio Zanasi.
Rewriting for monoidal closed categories.
In FSCD'22 Proceedings, volume 228 of LIPIcs, pages
29:1–29:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

[4]
Mario Alvarez-Picallo, Dan R. Ghica, David Sprunger, and Fabio Zanasi.
Functorial string diagrams for reverse-mode automatic
In CSL'23 Proceedings, volume 252 of LIPIcs, pages
6:1–6:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.

[5]
John Baez and Jason Erbele.
Categories in control.
Theory and Applications of Categories, 30:836–881, 2015.

[6]
John C Baez, Brandon Coya, and Franciscus Rebro.
Props in network theory.
Theory and Applications of Categories, 33(25):727–783, 2018.

[7]
John C Baez and James Dolan.
Higher-dimensional algebra and topological quantum field theory.
Journal of mathematical physics, 36(11):6073–6105, 1995.

[8]
John C. Baez and Jade Master.
Open petri nets.
Math. Struct. Comput. Sci., 30(3):314–341, 2020.

[9]
Hendrik Pieter Barendregt.
The lambda calculus - its syntax and semantics, volume 103 of
Studies in logic and the foundations of mathematics.
North-Holland, 1985.

[10]
Michael Barr.
$*$-Autonomous categories, volume 752.
Springer, 2006.

[11]
Guillaume Boisseau and Robin Piedeleu.
Graphical piecewise-linear algebra.
In FOSSACS'22 (ETAPS) Proceedings, pages 101–119. Springer
International Publishing Cham, 2022.

[12]
Guillaume Boisseau and Paweł Sobociński.
String diagrammatic electrical circuit theory.
arXiv:2106.07763, 2021.

[13]
Joe Bolt, Jules Hedges, and Philipp Zahn.
Bayesian open games.
arXiv preprint arXiv:1910.03656, 2019.

[14]
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, and
Fabio Zanasi.
Rewriting modulo symmetric monoidal structure.
In LICS'16 Proceedings, pages 710–719. IEEE, 2016.

[15]
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio
String diagram rewrite theory I: rewriting with Frobenius
J. ACM, 69(2):14:1–14:58, 2022.

[16]
Filippo Bonchi, Joshua Holland, Dusko Pavlovic, and Paweł Sobociński.
Refinement for signal flow graphs.
In CONCUR'17 Proceedings, pages 24:1–24:16, 2017.

[17]
Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and
Fabio Zanasi.
Diagrammatic algebra: from linear to concurrent systems.
POPL'19 Proceedings, 3:1–28, 2019.

[18]
Filippo Bonchi, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi.
Graphical affine algebra.
In LICS'19 Proceedings, pages 1–12, 2019.

[19]
Filippo Bonchi, Jens Seeber, and Pawel Sobocinski.
Graphical conjunctive queries.
In CSL'18 Proceedings. Schloss Dagstuhl-Leibniz-Zentrum fuer
Informatik, 2018.

[20]
Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi.
Interacting bialgebras are Frobenius.
In FOSSACS'14 Proceedings, volume 8412 of LNCS, pages
351–365. Springer Berlin Heidelberg, 2014.

[21]
Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi.
Full abstraction for signal flow graphs.
In POPL'15 Proceedings, volume 50 of ACM Sigplan Notices,
pages 515–526. ACM, 2015.

[22]
Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi.
The calculus of signal flow diagrams I: linear relations on
Information and Computation, 252:2–29, 2017.

[23]
Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi.
Interacting Hopf algebras.
Journal of Pure and Applied Algebra, 221(1):144–184, 2017.

[24]
Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi.
Deconstructing Lawvere with distributive laws.
J. Log. Algebraic Methods Program., 95:128–146, 2018.

[25]
Roberto Bruni and Fabio Gadducci.
Some algebraic laws for spans (and their connections with
In RelMiS'01 Proceedings, ENTCS, volume 44. Elsevier, 2001.

[26]
Roberto Bruni, Hernán Melgratti, and Ugo Montanari.
Connector algebras, Petri nets, and BIP.
In International Andrei Ershov Memorial Conference on
Perspectives of System Informatics, pages 19–38. Springer, 2011.

[27]
Roberto Bruni, Hernán C. Melgratti, Ugo Montanari, and Paweł
Connector algebras for C/E and P/T nets' interactions.
Log Meth Comput Sci, 9(16), 2013.

[28]
Aurelio Carboni and R. F. C. Walters.
Cartesian bicategories I.
Journal of Pure and Applied Algebra, 49:11–32, 1987.

[29]
Titouan Carette, Marc De Visme, and Simon Perdrix.
Graphical language with delayed trace: Picturing quantum computing
with finite memory.
In LICS'21 Proceedings, pages 1–13. IEEE, 2021.

[30]
Eugenia Cheng.
Iterated distributive laws.
Math. Proc. Camb. Philos. Soc., 150(3):459–487, 2011.

[31]
Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and
Benoît Valiron.
LOv-calculus: A graphical language for linear optical quantum
In MFCS'22 Proceedings. Schloss Dagstuhl-Leibniz-Zentrum
für Informatik, 2022.

[32]
J. Robin B. Cockett, Geoff S. H. Cruttwell, Jonathan Gallagher,
Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon D. Plotkin, and Dorette
Reverse derivative categories.
In CSL'20 Proceedings, volume 152 of LIPIcs, pages
18:1–18:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.

[33]
J Robin B Cockett and Robert AG Seely.
Weakly distributive categories.
Journal of Pure and Applied Algebra, 114(2):133–173, 1997.

[34]
Bob Coecke and Ross Duncan.
Interacting quantum observables.
In ICALP'08 Proceedings, Part II, pages 298–310, 2008.

[35]
Bob Coecke and Aleks Kissinger.
Picturing Quantum Processes - A first course in Quantum Theory
and Diagrammatic Reasoning.
Cambridge University Press, 2017.

[36]
Bob Coecke, Dusko Pavlovic, and Jamie Vicary.
A new description of orthogonal bases.
Math. Struct. Comp. Sci., 23(3):557–567, 2012.

[37]
Bob Coecke and Robert W Spekkens.
Picturing classical and quantum bayesian inference.
Synthese, 186:651–696, 2012.

[38]
B Coya and Brendan Fong.
Corelations are the prop for extraspecial commutative Frobenius
Theory and Applications of Categories, 32(11):380–395, 2017.

[39]
Geoffrey S. H. Cruttwell, Bruno Gavranovic, Neil Ghani, Paul W. Wilson, and
Fabio Zanasi.
Categorical foundations of gradient-based learning.
In ESOP'22, volume 13240 of LNCS, pages 1–28.
Springer, 2022.

[40]
Vincent Danos and Laurent Regnier.
The structure of multiplicatives.
Archive for Mathematical Logic, 28(3):181–203, 1989.

[41]
Giovanni De Felice and Bob Coecke.
Quantum linear optics via string diagrams.
arXiv:2204.12985, 2022.

[42]
Giovanni de Felice, Alexis Toumi, and Bob Coecke.
DisCoPy: Monoidal categories in python.
Electronic Proceedings in Theoretical Computer Science,
333:183–197, feb 2021.

[43]
Elena Di Lavore, Giovanni de Felice, and Mario Román.
Monoidal streams for dataflow programming.
In LICS'22 Proceedings, pages 1–14, 2022.

[44]
Elena Di Lavore, Alessandro Gianola, Mario Román, Nicoletta Sabadini, and
Paweł Sobociński.
A canonical algebra of open transition systems.
In FACS'21 Proceedings 17, pages 63–81. Springer, 2021.

[45]
Lucs Dixon and Aleks Kissinger.
Open-graphs and monoidal theories.
Mathematical Structures in Computer Science, 23(2):308–359,

[46]
Ross Duncan and Kevin Dunne.
Interacting Frobenius algebras are Hopf.
In LICS'16, pages 535–544, 2016.

[47]
Ross Duncan, Aleks Kissinger, Simon Perdrix, and John Van De Wetering.
Graph-theoretic simplification of quantum circuits with the
Quantum, 4:279, 2020.

[48]
Lawrence Dunn and Jamie Vicary.
Coherence for Frobenius pseudomonoids and the geometry of linear
Logical Methods in Computer Science, 15, 2019.

[49]
Hartmut Ehrig, Michael Pfender, and Hans Jürgen Schneider.
Graph-grammars: An algebraic approach.
In SWAT'73 Proceedings, pages 167–180. IEEE, 1973.

[50]
Brendan Fong.
Causal theories: A categorical perspective on Bayesian networks.
Master's thesis, Univ. of Oxford, 2012.

[51]
Brendan Fong.
Decorated cospans.
Theory and Applications of Categories, 30(33):1096–1120, 2015.

[52]
Brendan Fong.
The Algebra of Open and Interconnected Systems.
PhD thesis, University of Oxford, 2016.

[53]
Brendan Fong.
Decorated corelations.
Theory & Applications of Categories, 33, 2018.

[54]
Brendan Fong, Paweł Sobociński, and Paolo Rapisarda.
A categorical approach to open and interconnected dynamical systems.
In LICS'16 Proceedings, pages 495–504, 2016.

[55]
Brendan Fong, David I. Spivak, and Rémy Tuyéras.
Backprop as functor: A compositional perspective on supervised
In LICS'16 Proceedings, pages 1–13. IEEE, 2019.

[56]
Tobias Fritz.
A synthetic approach to Markov kernels, conditional independence
and theorems on sufficient statistics.
Advances in Mathematics, 370:107239, 2020.

[57]
Tobias Fritz, Tomáš Gonda, and Paolo Perrone.
De finetti’s theorem in categorical probability.
Journal of Stochastic Analysis, 2(4):6, 2021.

[58]
Tobias Fritz and Wendong Liang.
Free gs-monoidal categories and free Markov categories.
Applied Categorical Structures, 31(2):21, 2023.

[59]
Tobias Fritz and Eigil Fjeldgren Rischel.
The zero-one laws of Kolmogorov and Hewitt–Savage in
categorical probability.
Compositionality, 2:3, 2020.

[60]
Fabio Gadducci and Reiko Heckel.
An inductive view of graph transformation.
In WADT'97 Proceedings, pages 223–237, 1997.

[61]
Bruno Gavranovic.
Category theory $\cap$ machine learning.
Accessed: 2023-09-06.

[62]
Bruno Gavranovic.
Compositional deep learning.
arXiv:1907.08292, 2019.

[63]
Neil Ghani, Jules Hedges, Viktor Winschel, and Philipp Zahn.
Compositional game theory.
In LICS'18 Proceedings, pages 472–481, 2018.

[64]
Dan R. Ghica.
Diagrammatic reasoning for delay-insensitive asynchronous circuits.
In Computation, Logic, Games, and Quantum Foundations. The Many
Facets of Samson Abramsky, pages 52–68. Springer, 2013.

[65]
Dan R Ghica and George Kaye.
Rewriting modulo traced comonoid structure.
arXiv:2302.09631, 2023.

[66]
Dan R Ghica, George Kaye, and David Sprunger.
Full abstraction for digital circuits.
arXiv:2201.10456, 2022.

[67]
Jean-Yves Girard.
Linear logic.
Theor. Comput. Sci., 50:1–102, 1987.

[68]
Amar Hadzihasanovic and Diana Kessler.
Data structures for topologically sound higher-dimensional diagram
In ACT'22 Proceedings, 2022.

[69]
Masahito Hasegawa.
Recursion from cyclic sharing: traced monoidal categories and models
of cyclic lambda calculi.
In TLCA'97 Proceedings, pages 196–213. Springer, 1997.

[70]
Nathan Haydon and Paweł Sobociński.
Compositional diagrammatic first-order logic.
In Diagrams'20 Proceedings, pages 402–418. Springer, 2020.

[71]
Chris Heunen and Jamie Vicary.
Categories for Quantum Theory: an introduction.
Oxford University Press, 2019.

[72]
Martin Hyland and John Power.
The category theoretic understanding of universal algebra: Lawvere
theories and monads.
In Computation, Meaning, and Logic: Articles dedicated to Gordon
Plotkin, volume 172 of Electronic Notes in Theoretical Computer
Science, pages 437–458. Elsevier, 2007.

[73]
Bart Jacobs, Aleks Kissinger, and Fabio Zanasi.
Causal inference via string diagram surgery: A diagrammatic approach
to interventions and counterfactuals.
Mathematical Structures in Computer Science, 31(5):553–574,

[74]
André Joyal and Ross Street.
Braided monoidal categories.
Mathematics Reports, 86008, 1986.

[75]
André Joyal and Ross Street.
The geometry of tensor calculus, I.
Advances in Mathematics, 88(1):55–112, 1991.

[76]
Piergiulio Katis, Nicoletta Sabadini, and Robert FC Walters.
Feedback, trace and fixed-point semantics.
RAIRO-Theoretical Informatics and Applications, 36(2):181–194,

[77]
G Maxwell Kelly.
Many-variable functorial calculus. I.
In Coherence in categories, pages 66–105. Springer, 1972.

[78]
Gregory M Kelly and Miguel L Laplaza.
Coherence for compact closed categories.
Journal of Pure and Applied Algebra, 19:193–213, 1980.

[79]
Andrey Boris Khesin, Jonathan Z Lu, and Peter W Shor.
Graphical quantum Clifford-encoder compilers from the ZX
arXiv:2301.02356, 2023.

[80]
Aleks Kissinger and John van de Wetering.
PyZX: Large scale automated diagrammatic reasoning.
arXiv:1904.04735, 2019.

[81]
Aleks Kissinger and Vladimir Zamdzhiev.
Quantomatic: A proof assistant for diagrammatic reasoning.
CoRR, abs/1503.01034, 2015.

[82]
Stephen Lack.
Composing PROPs.
Theory and Application of Categories, 13(9):147–163, 2004.

[83]
Yves Lafont.
Towards an algebraic theory of Boolean circuits.
Journal of Pure and Applied Algebra, 184(2–3):257–310, 2003.

[84]
Robin Lorenz and Sean Tull.
Causal models in string diagrams.
arXiv:2304.07638, 2023.

[85]
Saunders Mac Lane.
Categorical algebra.
Bulletin of the American Mathematical Society, 71:40–106,

[86]
Saunders MacLane.
Categories for the Working Mathematician.
Springer-Verlag, New York, 1971.
Graduate Texts in Mathematics, Vol. 5.

[87]
Dan Marsden and Fabrizio Genovese.
Custom hypergraph categories via generalized relations.
In CALCO'17 Proceedings. Schloss Dagstuhl-Leibniz-Zentrum
fuer Informatik, 2017.

[88]
Daniel Marsden.
Category theory using string diagrams.
arXiv:1401.7220, 2014.

[89]
Paul-André Mellies.
Categorical semantics of linear logic.
Panoramas et syntheses, 27:15–215, 2009.

[90]
Aleksandar Milosavljevic and Fabio Zanasi.
String diagram rewriting modulo commutative monoid structure.
To appear in CALCO'23 Proceedings, arXiv:2204.04274, 2023.

[91]
Sean Moss and Paolo Perrone.
A category-theoretic proof of the ergodic decomposition theorem.
arXiv preprint arXiv:2207.07353, 2022.

[92]
Koko Muroya and Dan R Ghica.
The dynamic geometry of interaction machine: A call-by-need graph
CSL'17 Proceedings, 2017.

[93]
Dusko Pavlovic.
Monoidal computer I: Basic computability by string diagrams.
Information and computation, 226:94–116, 2013.

[94]
Dusko Pavlovic.
Categorical computability in monoidal computer: Programs as diagrams.
arXiv:2208.03817, 2022.

[95]
R. Penrose.
Applications of negative dimension tensors.
In D. J. A. Welsh, editor, Combinatorial Mathematics and its
Applications, pages 221–244. Academic Press, 1971.

[96]
Roger Penrose.
Applications of negative dimensional tensors.
Combinatorial mathematics and its applications, 1:221–244,

[97]
Robin Piedeleu and Fabio Zanasi.
A finite axiomatisation of finite-state automata using string
Logical Methods in Computer Science, 19, 2023.

[98]
Boldizsár Poór, Quanlong Wang, Razin A Shaikh, Lia Yeh, Richie Yeung,
and Bob Coecke.
Completeness for arbitrary finite dimensions of ZXW-calculus, a
unifying calculus.
arXiv:2302.12135, 2023.

[99]
Mehrnoosh Sadrzadeh, Stephen Clark, and Bob Coecke.
The Frobenius anatomy of word meanings I: subject and object
relative pronouns.
Journal of Logic and Computation, 23(6):1293–1317, 2013.

[100]
Mehrnoosh Sadrzadeh, Stephen Clark, and Bob Coecke.
The Frobenius anatomy of word meanings II: possessive relative
Journal of Logic and Computation, 26(2):785–815, 2014.

[101]
Peter Selinger.
A survey of graphical languages for monoidal categories.
Springer Lecture Notes in Physics, 13(813):289–355, 2011.

[102]
Dan Shiebler, Bruno Gavranovic, and Paul W. Wilson.
Category theory in machine learning.
arXiv:2106.07032, 2021.

[103]
Paweł Sobociński, Paul W Wilson, and Fabio Zanasi.
Cartographer: A tool for string diagrammatic reasoning.
In CALCO'19 Proceedings, page 25, 2019.

[104]
G. Stefanescu.
Network Algebra.
Discrete Mathematics and Theoretical Computer Science. Springer
London, 2000.

[105]
John van de Wetering.
ZX-calculus for the working quantum computer scientist.
arXiv:2012.13966, 2020.

[106]
Jamie Vicary, Aleks Kissinger, and Krzysztof Bar.
Globular: an online proof assistant for higher-dimensional rewriting.
Logical Methods in Computer Science, 14, 2018.

[107]
Paul Wilson and Fabio Zanasi.
Data-parallel algorithms for string diagrams.
arXiv:2305.01041, 2023.

[108]
Paul W. Wilson, Dan R. Ghica, and Fabio Zanasi.
String diagrams for non-strict monoidal categories.
In CSL, volume 252 of LIPIcs, pages 37:1–37:19.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.

[109]
Paul W. Wilson and Fabio Zanasi.
Reverse derivative ascent: A categorical approach to learning
boolean circuits.
In ACT'20 Proceedings, volume 333 of EPTCS, pages
247–260, 2020.

[110]
Paul W. Wilson and Fabio Zanasi.
The cost of compositionality: A high-performance implementation of
string diagram composition.
In ACT'21 Proceedings, volume 372 of EPTCS, pages
262–275, 2021.

[111]
Paul W. Wilson and Fabio Zanasi.
Categories of differentiable polynomial circuits for machine
In ICGT, volume 13349 of Lecture Notes in Computer
Science, pages 77–93. Springer, 2022.

[112]
Fabio Zanasi.
Interacting Hopf Algebras: the theory of linear systems.
PhD thesis, Ecole Normale Supérieure de Lyon, 2015.

[113]
Fabio Zanasi.
The algebra of partial equivalence relations.
Electronic Notes in Theoretical Computer Science, 325:313–333,