2. Relational Convolution: A Summary

In this section, we summarise the general approach to the construction of quantale-valued convolution algebras from ternary relations.

Relational convolution (Dongol et al. Reference Dongol, Hayes and Struth2021) has its origins in Jónsson and Tarski’s boolean algebras with operators (Jónsson and Tarski Reference Jónsson and Tarski1951), Rota’s foundations of combinatorics (Rota Reference Rota1964), Schützenberger’s approach to language theory (Berstel and Reutenauer Reference Berstel and Reutenauer1984; Droste et al. Reference Droste, Kuich and Vogler2009), Goguen’s L-fuzzy maps and relations (Goguen Reference Goguen1967) and arguably (Connes Reference Connes1995) Heisenberg’s first article on the foundations of quantum mechanics (Heisenberg Reference Heisenberg1925). The group algebras used in the representation theory of finite groups (Lang Reference Lang2003) and, more generally, category algebras are other sources of inspiration.

Here, convolution is an operation in the algebra of functions $X\to Q$ from a set X into a complete lattice Q equipped with an additional operation $\bullet$ of composition and constrained by a ternary relation R on X, which we identify with a predicate of type $X\to X\to X\to \mathbb{B}$ . It is defined as

\begin{equation*} (f\ast g)\, x = \bigvee_{y,z:R^x_{yz}} f\, y\bullet g\, z,\end{equation*}

where the right-hand side abbreviates $\bigvee \{f\, y \bullet g\, z\mid R^x_{yz}\}$ and $\bigvee$ denotes the supremum in Q. It is well known that the function space $Q^X$ forms a complete lattice when the order and sups in Q are extended pointwise (Abramsky and Jung Reference Abramsky and Jung1994). Yet the convolution $\ast$ need not satisfy any algebraic laws on $Q^X$ , unless conditions on R and Q are imposed.

This situation is reminiscent of modal correspondence theory, where conditions on relational Kripke frames force algebraic properties of modal operators and vice versa, or more generally to dualities between categories of $(n+1)$ -ary relational structures and those of boolean algebras with n-ary operators (Jónsson and Tarski Reference Jónsson and Tarski1951; Goldblatt Reference Goldblatt1989). In fact, R is a ternary relational structure and $\ast$ a binary modality similar to the product of the Lambek calculus (Lambek Reference Lambek1958), the chop operation of interval temporal logics (Moszkowski and Manna Reference Moszkowski and Manna1983) or the separating conjunction of separation logic (O’Hearn et al. Reference O’Hearn, Reynolds and Yang2001), but generalised to a Q-weighted setting.

It is well known that chop is associative in the convolution algebra $\mathbb{B}^X$ due to associativity of meet in $\mathbb{B}$ and associativity of interval fusion in X – up to definedness.

Definition 2 (Rosenthal 1990) A quantale Q is a complete lattice equipped with an associative composition $\bullet$ that preserves sups in both arguments: for all $a,b\in Q$ and $A,B\subseteq Q$ ,

\begin{equation*} a\bullet \left(\bigvee B\right) = \bigvee \{a\bullet b\mid b\in B\}\qquad { and }\qquad \left(\bigvee A\right) \bullet b = \bigvee \{a\bullet b\mid a\in A\}.\end{equation*}

A quantale is unital if $\bullet$ has a unit 1.

We write 0 for the least and $\top$ for the greatest element of Q with respect to the lattice order. Sup-preservation implies that $x \bullet 0 = 0 = 0 \bullet x$ .

Convolution is then associative in $Q^X$ if the relational structure (X,R) is relationally associative:

\begin{equation*} \exists y.\ R^y_{uv} \wedge R^x_{yw} \Leftrightarrow \exists y.\ R^x_{uy} \wedge R^y_{vw} \qquad \text{ for all } x,u,v,w\in X.\end{equation*}

This yields one direction of a correspondence between the ternary relation or Kripke frame R and convolution $\ast$ viewed as a binary modality. Similarly, convolution is commutative in $Q^X$ if (X,R) is relationally commutative:

\begin{equation*} R^x_{uv} \Rightarrow R^x_{vu} \qquad \text{ for all } x,u,v\in X.\end{equation*}

To construct a unit of convolution, we first equip (X,R) with a set of units. Their definition is similar to those in an object-free category (Mac Lane Reference Mac Lane1998). An element $e\in X$ is a left relational unit in (X,R) if

\begin{equation*} \exists x\in X.\ R^x_{ex}\qquad\text{ and } \qquad \forall x,y\in X.\ R^x_{ey} \Rightarrow x =y. \end{equation*}

Similarly, x is a right relational unit in (X,R) if $\exists x\in X.\ R^x_{xe}$ and $\forall x,y\in X.\ R^x_{ye}\Rightarrow x =y$ .

We write E for the set of all left and right relational units of (X,R) and call this relational structure unital if every element of X has a left and right unit.

Then, if X, or more precisely (X,R), is unital with set of relational units E and if the quantale Q is unital with unit of composition 1, then convolution has the indicator function $\mathit{id}_E:X\to Q$ as its left and right unit, where

\begin{equation*} \mathit{id}_E\, x = \begin{cases} 1& \text{if } x\in E,\\0 & \text{otherwise}. \end{cases}\end{equation*}

In particular, each $x\in X$ has a unique left unit and a unique right one if the relational structure (X,R) is relationally associative (Cranch et al. Reference Cranch, Doherty and Struth2020). With the Kronecker delta $\delta_x: X\to \mathbb{B}$ defined as $\delta_x\, y$ equal to 1 if $x=y$ and to 0 otherwise, therefore,

\begin{equation*}\mathit{id}_E = \bigvee_{e\in E} \delta_e.\end{equation*}

The convolution algebras on $Q^X$ can now be described as follows.

Relational monoids are well known in category theory. They are monoids in the monoidal category $\mathbf{Rel}$ with the standard tensor.

Theorem. (Reference Dongol, Hayes and StruthDongol et al. 2021)

1. (1) If X is a relational semigroup and Q a quantale, then $Q^X$ is a quantale.

2. (2) If R is an abelian relational semigroup and Q an abelian quantale, then $Q^X$ is an abelian quantale.

3. (3) If R is a relational monoid and Q is a unital quantale, then $Q^X$ is a unital quantale.

Words are finitely decomposable in that each word can only be split into finitely many prefix/suffix pairs. All sups in convolutions therefore remain finite and Q can be replaced by an arbitrary semiring. This yields the usual weighted languages formalised as rational power series in the sense of Schützenberger and Eilenberg (Berstel and Reutenauer Reference Berstel and Reutenauer1984; Droste et al. Reference Droste, Kuich and Vogler2009).

The construction specialises first to quantales of weighted closed intervals in linear orders, as in Example 1, which can be represented by ordered pairs (a,b) in which $a\le b$ . Categorically, it is given by a poset (X,R), for $R\subseteq X\times X$ , regarded as a posetal category. This makes incidence algebras a special case of a category algebra.

A second specialisation are possibly infinitary matrices with matrix product as convolution, as studied by Heisenberg (Reference Heisenberg1925). When X is finite, (semi)rings and similar algebras can be taken again as value algebras. Alternatively, it can be assumed that $f(x)\bullet g(z)=0$ for all buy finitely many $(x,y)\in X\times X$ . Binary relations are of course boolean-valued matrices with relational composition as matrix product.

A third specialisation, using the one-object groupoid, yields group algebras if convolution is finitely supported in the sense just explained.

3. Correspondences for Interchange Laws

Theorem 2 generalises to correspondences between quantales with two compositions and related by seven interchange laws, as they appear in concurrent Kleene algebras, and relational structures with suitable relational constraints. The choice of the interchange laws is explained further in Section 5; the six small interchange laws are precisely those that can be derived from the seventh in the presence of suitable units, using a generalised Eckmann-Hilton argument. We start with the relational structures.

The constraints considered on a bi-magma X are, for $t,u,v,w,x,y,z\in X$ , the relational interchange laws

(RI1)

(RI2)

(RI3)

(RI4)

(RI5)

(RI6)

(RI7)

They are represented by the relationships between the trees in X shown in Figure 1.

Figure 1. Trees representing the relational interchange laws.

Next, we turn to quantales. As their monoidal structure emerges in our constructions, we generalise.

A quantale is thus nothing but a prequantale with associative composition.

For $a,b,c,d\in Q,$ we define the algebraic interchange laws

(I1)

(I2)

(I3)

(I4)

(I5)

(I6)

(I7)

The interchange laws of odd index are the most significant laws of concurrent Kleene algebra (Hoare et al. Reference Hoare, Möller, Struth and Wehrman2011). Those of even index need to be added if is not commutative.

Interestingly, the syntax trees of these laws in Q, as shown in Figure 2, have the structure of the trees representing the relational interchange laws in X in Figure 1. The following example provides some intuition.

Figure 2. Syntax trees of the algebraic interchange laws.

Example 10. Let $X=Q$ , and . Then, for instance,

and likewise for the other terms in interchange laws. The relational and algebraic interchange laws then translate into each other. For instance, for (RI7) and (I7),

that is,

With this particular encoding, the relational interchange laws simply represent the algebraic ones.

In general, however, the relationship between relational and algebraic convolution is more complex. The left-to-right translation in Example 10 can therefore fail.

For functions $f,g:X\to Q,$ we define the convolutions

They can be represented using trees in X, Q and $Q^X$ as

Convolution thus translates trees with the same structure in X and Q into trees in $Q^X$ .

One can then prove modal correspondences between relational and algebraic interchange laws. First, we show that relational interchange laws in X and algebraic interchange laws in Q yield algebraic interchange laws in the convolution algebra on $Q^X$ . This generalises the well-known modal correspondence from ternary Kripke frames to binary modal operators, which occur for instance in substructural logics, first to more than one relation and second to a weighted setting.

Proof. Suppose that holds in X and further that holds in Q. Then

proves (I7) in $Q^X$ . Alternatively, using trees,

The proofs for the small interchange laws are similar and left to the reader. In particular, that of (I3) from (RI3) and that of (I4) from (RI4) are related by opposition: one can be obtained from the other by swapping the operands of , , and and the lower indices of and , that is, by reversing the algebraic syntax trees in Q and the trees in X for the relational interchange laws. The same holds for the proof of (I5) from (RI5) and that of (I6) from (RI6).

The correspondences from X and Q to $Q^X$ form one of three kinds of ‘two-cells’ in correspondence triangles. They show how Q-valued interchange laws arise in convolution algebras from relational interchange laws and interchange laws on a suitable value algebra.

Next we show the remaining two, namely that, under mild nondegeneracy conditions on Q, algebraic interchange laws in $Q^X$ force relational interchange laws in X, and that under mild nondegeneracy conditions on X, algebraic interchange laws in $Q^X$ force algebraic interchange laws in Q. We begin with a definition and some lemmas.

For all $x,y\in X$ and $a\in Q$ , we define the function $\delta^a_x:X\to Q$ by

\begin{equation*} \delta^a_x\, y =\begin{cases} a, & \text{ if } x= y,\\0 & \text{ otherwise}\end{cases}\end{equation*}

and the function $(-\mid -):Q\to\mathbb{B}\to Q$ , for all $a\in Q$ and $P:\mathbb{B}$ , by

\begin{equation*} (a\mid P) = \begin{cases} a, &\text{ if } P,\\0, & \text{ otherwise}. \end{cases}\end{equation*}

Obviously, $\delta^a_x\, y = (a\mid x = y)$ .

1. (1)

2. (2)

3. (3)

4. (4)

5. (5) properties (1)–(4) hold with colours interchanged.

Proof. For (4), we use the proof of Proposition 11 to calculate

Alternatively, using trees,

All other proofs are similar and left to the reader. In particular, (3) follows from (2) by opposition.

The next lemma shows that the trees represented by the relational interchange laws can be expressed in terms of deltas and convolution in the presence of the following mild nondegeneracy conditions on Q:

(D1)

(D2)

(D3)

(D4)

1. (1) , and the converse implication follows from (D1),

2. (2) and the converse implication follows from (D2),

3. (3) and the converse implication follows from (D3),

4. (4) and the converse implication follows from (D4),

5. (5) properties (1)–(5) hold with colours interchanged, including in the nondegeneracy conditions.

Proof. For (4), suppose . Then

by Lemma 12(4). For the converse implication, using the elements $a,b,c,d\in Q$ that are guaranteed to satisfy by (D4),

by Lemma 12(4) and therefore .

All other proofs are similar and left to the reader. (3) follow from (2) by opposition.

Intuitively, convolutions of delta functions represent trees in X in the function space $Q^X$ by creating their ‘shadows’ in Q – which requires nondegeneracy. The case of Lemma 13(4) and its dual are shown in Figure 3.

Figure 3. representing using in Lemma 13(4) together with its dual.

We are now prepared to prove our second correspondence result, namely that algebraic interchange laws in $Q^X$ force relational interchange laws in X subject to mild nondegeneracy conditions on Q.

Proof. Suppose

for some $a,b,c,d\in Q$ and

Then, using Lemma 13(4),

proves $(RI_7)$ . The remaining proofs are similar. Those for $(RI_3)$ and $(RI_4)$ and those for $(RI_5)$ and $(RI_6)$ are related by opposition.

Finally, we prove the third correspondence result for interchange laws, namely that algebraic interchange laws on $Q^X$ force those on Q, subject to the following mild nondegeneracy conditions on X:

(RD1)

(RD2)

(RD3)

(RD4)

.

Proof. Suppose for some $a,b,c,d\in Q$ and let for some $t,u,v,w\in X$ . Then, using Lemma 13(4),

proves $(I_7)$ in Q. The remaining proofs are similar. Those for $(RD_3)$ and $(RD_4)$ and those for $(RD_5)$ and $(RD_6)$ are related by opposition.

It may be helpful to check the proofs of Propositions 14 and 15 with the diagrams in Figure 3. The nondegeneracy conditions are necessary. Indeed, if Q is a singleton set, then so is $Q^X$ and hence it will obey all axioms independently of X. Similarly, if all products on Q vanish, then $Q^X$ will automatically satisfy many axioms as all convolutions will be trivial.

This finishes the proof of the correspondence triangles for interchange laws in X, Q and $Q^X$ . The result of Proposition 11 shows that interchange laws in X and Q give us interchange laws in $Q^X$ for free; Propositions 14 and 15 show us that all interchange laws in the convolution algebra arise this way. To construct a convolution algebra satisfying an interchange law, it therefore suffices to find a suitable relational structure satisfying a relational interchange law, which is often much easier.

4. Further Correspondences

The next step towards modal correspondence results for concurrent quantales and Kleene algebras consists in the study of correspondence triangles for units and the monoidal structure on a quantale, completing those outlined in Section 2.

We start with units. When the relational bi-magma X and the bi-prequantale Q are both unital, units can be defined in $Q^X$ as in Section 2:

Theorem 2 then shows that $Q^X$ is a unital quantale if Q is a unital quantale and both compositions are associative and unital in X. We restate the three kinds of correspondences for units in the weaker setting of relational magmas and prequantales.

1. (1) If X and Q are unital, then so is $Q^X$ .

2. (2) If $Q^X$ is unital and $1\neq 0$ in Q, then so is X.

3. (3) If $Q^X$ is unital and $E\neq \emptyset$ in X, then so is Q.

Proof. In the following we write $\delta_x$ and likewise for $\delta^1_x$ .

1. (1) If X and Q are unital, then

   \begin{align*}(f\ast \mathit{id}_E)\, x&=\bigvee \{f\, y \bullet \delta_e\, z \mid R^x_{yz} \land E^e\}\\&=\bigvee \{f\, y \bullet 1 \mid \exists e.\ R^x_{ye} \land E^e\}\\&=(f\, x \mid \exists e.\ R^x_{xe} \land E^e)\\&= f\, x,\end{align*}
   where the last two steps use the relational unit axioms. The proof for left units follows by opposition.

2. (2) If $\mathit{id}_E$ is the right unit in $Q^X$ , then

   \begin{equation*}(1\mid (y=x))= \delta_y\, x= (\delta_y\ast \mathit{id}_E)\, x= (1\mid \exists e.\ R^x_{ye} \land E^e). \end{equation*}
   Suppose $1\neq 0$ . Then, $x=y$ implies $\exists e.\ R^x_{xe} \land E^e$ , the existence axiom for right relational units, and $\exists e.\ R^x_{ye} \land E^e$ implies that $x=y$ , the uniqueness axiom. The proofs for left units follow by opposition.

3. (3) If $\mathit{id}_E$ is the right unit in $Q^X$ , then

   \begin{equation*} a\bullet 1= (a\bullet 1\mid \exists e.\ R^x_{xe} \land E^e)=\bigvee\{\delta_x\, x \mid \exists e.\ R^x_{xe} \land E^e\}= (\delta^a_x \ast \mathit{id}_E)\, x= \delta^a_x\, x= a \end{equation*}
   proves that 1 is a right unit in Q. The left unit law follows by opposition.

In the presence of non-trivial units in X and Q, the nondegeneracy conditions for interchange laws in Propositions 14 and 15 simplify. Condition (D1) becomes trivial with , condition (D2) with and condition (D3) by opposition. Condition (D4) reduces to but remains non-trivial. It becomes trivial when . It is easy to check that the nondegeneracy conditions (RD1)–(RD3) become trivial in a similar way, using the fact that holds for all and for all . Once again, (RD4) becomes trivial when .

In the only-if directions, functions $\delta_x$ can now be used. This leads to a simpler relationship between deltas and ternary relations than in Lemma 13.

Corollary 18. Let X be a relational magma and Q a unital prequantale with $1\neq 0$ . Then

\begin{equation*} R^x_{yz} \Leftrightarrow (\delta_y \ast \delta_z)\, x = 1. \end{equation*}

It is therefore compelling to see $\mathbb{B}$ as the sublattice over $\{0,1\}$ of Q and write $R^x_{yz} = (\delta_y\ast\delta_z)\, x$ or even $(f\ast g)\, x = \bigvee_{y,z} f\, y \bullet g\, z \bullet R^x_{yz}$ , similar to a coend. Figure 4 shows how the presence of units affects the right-hand term in (RI7).

Figure 4. Nondegeneracy condition (D4) in the presence of units.

Next, we present a correspondence result for relational units that is useful in Section 5.

1. (1) If in X and in Q, then in $Q^X$ .

2. (2) If in $Q^X$ and in Q, then in X.

3. (3) If in $Q^X$ and in X, then in Q.

Proof.

1. (1) Let and . Then, , for all $x\in X$ , and therefore .

2. (2) Let . If , then , for all $x\in X$ , and therefore .

3. (3) Let and . Then, , for all $x\in X$ .

Because of the symmetry in the definitions of unital bi-magmas and bi-prequantales, Lemma 19 and Corollary 20 hold with colours swapped. We do not spell them out explicitly.

Next we turn to correspondence triangles for relational monoids and quantales. In fact, the correspondences between interchange laws can be specialised to obtain the associativity laws for a quantale. The relational interchange law (RI3), , becomes the relational semi-associativity law $\exists y. R^x_{uy} \wedge R^y_{vw}\Rightarrow \exists y.\ R^y_{u\, v} \wedge R^x_{y\, w}$ when colours are switched off; (RI4) translates into the opposite implication. Both laws establish relational associativity. Similarly, the interchange laws (I3) and (I4), and , become the semi-associativity laws $a\bullet (b\bullet c)\le (a\bullet b)\bullet c$ and $(a\bullet b)\bullet c\le a \bullet (b\bullet c)$ . This yields the following corollary to Propositions 11, 14 and 15.

1. (1) If X is relationally associative and Q associative, then $Q^X$ is associative.

2. (2) If $Q^X$ is associative and some $a,b,c\in Q$ satisfy $a\bullet (b\bullet c)\neq 0\neq (a\bullet b) \bullet c$ , then X is relationally associative.

3. (3) If $Q^X$ is associative and some $x,y,z,u,v,w\in X$ satisfy $R^x_{uz}$ , $R^x_{yw}$ $R^z_{vw}$ and $R^y_{uv}$ , then Q is associative.

Similar correspondences between semi-associativity laws are straightforward, but not as interesting for our purposes. In the presence of units, Corollary 21 simplifies further.

Finally, the correspondence triangles between interchange laws can also be specialised to commutativity laws. The relational interchange law (RI2), , specialises to $R^x_{uv} \Rightarrow R^x_{vu}$ when colours are switched off while the interchange law (I2), , becomes $a\bullet b\le b\bullet a$ . This yields another corollary to Propositions 11, 14 and 15.

1. (1) If X is relationally commutative and Q abelian, then $Q^X$ is abelian.

2. (2) If $Q^X$ is abelian and there exist $a,b\in Q$ with $a\bullet b\neq 0$ , then X is relationally commutative.

3. (3) If $Q^X$ is abelian and there exist $x,y,z\in X$ with $R^x_{yz}$ , then Q is abelian.

In the presence of units, this corollary simplifies further.

The correspondence triangles in this section thus extend those for interchange laws in a compositional way to units and monoidal laws by specialisation. We summarise them in the following sections to correspondence triangles for concurrent quantales and Kleene algebras.

5. Relational Interchange Monoids and Interchange Quantales

We now start shifting the focus from correspondence theory to construction recipes for quantales with interchange laws, and in particular concurrent quantales. To avoid nondegeneracy conditions, we assume that relational magmas and quantales are unital and impose an order between units: and .

Yet first we prove a weak variant of the classical Eckmann-Hilton argument (Eckmann and Hilton Reference Eckmann and Hilton1962). Its standard version shows that if a unital bi-magma, a set equipped with composition and unit and composition with unit , satisfies the strong interchange law , then , and coincide, and they are associative and commutative. We show how these properties generalise if strong interchange is weakened to (I7). In this case, all interchange laws with lower indices become derivable. This of course requires ordered bi-magmas, where the underlying set is partially ordered and the two compositions l and l preserve the order in both arguments.

Proof. First, for all $e\in S$ , and with (RI7) in the fourth step,

Second, let and assume (RI7). Then,

proves (RI6). The proofs of (RI1), (RI2), (RI3) and (RI5) from (RI7) are similar and left to the reader.

Next we package the correspondence results from previous sections using suitable algebraic structures and relate these with concurrent quantales and later with concurrent Kleene algebras.

Proof. The correspondence for associativity and units in the subquantales is given by Corollary 21 and Proposition 16; that for interchange between the subquantales is given by Propositions 11, 14 and 15.

Theorem 5 shows that, up to mild nondegeneracy assumptions, all interchange quantales of type $X\to Q$ are obtained from a relational interchange monoid on X and an interchange quantale Q. To build such quantales, one should therefore look for relational interchange monoids, and the advantage is that fewer properties need to be checked.

Interchange quantales generalise concurrent quantales and are strongly related to concurrent Kleene algebras (Hoare et al. Reference Hoare, Möller, Struth and Wehrman2011). The difference is that here we do not assume that ‘parallel composition’ is commutative. Yet Theorem 5 adapts easily to the commutative case. For a concurrent quantale in $Q^X$ , an interchange monoid X with relationally commutative and an interchange quantale Q with commutative is needed. A variant of Theorem 5 then follows from Corollaries 24 and 17. In particular, the nondegeneracy assumptions simplify to non-triviality assumptions for units and unit sets.

An interesting specialisation of Theorem 5 is the case of $Q=\mathbb{B}$ , which forms an interchange quantale with both compositions being meet and both units of composition 1. In particular, in the booleans, $0\neq 1$ . The interchange law (I7) holds trivially because

\begin{equation*} (w\wedge x)\wedge (y\wedge z) = (w \wedge y)\wedge (x\wedge z)\end{equation*}

in any semilattice by associativity and commutativity of meet.

In this case, by Corollary 18 and Lemma 13, , and likewise for the other relational nondegeneracy conditions.

6. Interchange Kleene Algebras

We mentioned in Section 2 that in many classical convolution algebras, including Rota’s incidence algebras and the formal power series of Schützenberger and Eilenberg’s approach to formal languages, the underlying set X has a finite decomposition property (Rota calls partial orders with this property locally finite Rota Reference Rota1964). As infinite sups are then not needed to express convolutions, one can specialise quantales to semirings and Kleene algebras, and in particular concurrent Kleene algebras. We work out the details in this section.

We write $(-)^\star$ instead of the usual $(-)^\ast$ to distinguish the Kleene star from the convolution operation. Note also that equational variants of the two unfold axioms are derivable from the Kleene algebra axioms. We use them in proofs below.

To translate Theorem 5 from quantales to Kleene algebras, all sups must be guaranteed to be finite. This can be achieved by imposing that all functions have finite support or that the relations and are finitely decomposable, that is, for each x the fibres and are finite. If this is the case, we call the relational interchange monoid finitely decomposable as well.

Theorem. If X is a finitely decomposable relational interchange monoid and S an interchange semiring, then $S^X$ is an interchange semiring.

Proof. In the construction of the convolution algebra on $S^X,$ it is routine to check that all sups remain finite.

It is easy to generalise these results from dioids to proper semirings that are ordered. We do not spell out the details. Beyond that it seems interesting to extend Theorem 6 to interchange Kleene algebras. First of all, every interchange quantale is an interchange Kleene algebra, because and can be defined explicitly in this setting using Kleene’s fixpoint theorem: and satisfy the star axioms, with powers defined recursively in the standard way as and and likewise for .

When infinite sups and the sup-preservation properties needed for Kleene’s fixpoint theorem are not available, another approach is needed. It is known (Armstrong et al. Reference Armstrong, Struth and Weber2014) that formal power series – functions of type $\Sigma^\ast\to K$ , where $\Sigma^\ast$ is the free monoid over the finite alphabet $\Sigma$ and K a Kleene algebra – form Kleene algebras. In this setting, the star of a power series can be defined recursively as

\begin{equation*} f^\star\, \varepsilon = (f\, \varepsilon)^\star, \qquad f^\star\, x = (f\, \varepsilon)^\star\bullet \sum_{y,z:x=y\cdot z,y\neq \varepsilon} f\, y \bullet f^\star\, z,\end{equation*}

where $\sum$ indicates a finite sup (Kuich and Salomaa Reference Kuich and Salomaa1986). The verification of the star axioms for power series uses structural induction over finite words. Yet this is not applicable for general ternary relations. Instead we use a notion of grading that has been introduced for arbitrary monoids by Sakarovitch (Reference Sakarovitch2003).

The function $|-|:X\to\mathbb{N}$ is a grading on the relational monoid (X,R,E) if

• $|x|>0$ for all $x\in X$ such that $x\notin E$ ,

• $|x|=|y|+|z|$ whenever $R^x_{yz}$ .

Then, (X,R,E) is graded if there is a grading on X. Thus, in a graded monoid, $|e|=0$ if and only if $e\in E$ .

Proposition 34. If $(X,R,\{e\})$ is a graded, finitely decomposable, relational monoid and K a Kleene algebra, then $K^X$ is a Kleene algebra with

\begin{equation*} f^\star\, e = (f\, e)^\star, \qquad f^\star\, x = (f\, e)^\star \bullet \sum_{y,z:R^x_{yz},y\neq e} f\, y \bullet f^\star\, z.\end{equation*}

Proof. We need to check the unfold and induction axioms of Kleene algebra. First, the axiom $1+a^\star\bullet a \le a^\star$ is implied by the other axioms in any Kleene algebra and can be ignored (von Wright Reference von Wright2002): the first unfold axiom implies $1\le a^\star$ and $a+a\bullet a^\star\le a\bullet a^\star \le a^\star$ , so that $1+a^\star\bullet a \le a^\star$ follows using the second induction axiom. Second, $c+a\bullet b\le b\Rightarrow a^\star \bullet c\le b$ follows from the simpler formula $a\bullet b\le b\Rightarrow a^\star \bullet b \le b$ , and likewise, by opposition, $c+b\bullet a\le b\Rightarrow c \bullet a^\star \le b$ follows from $b\bullet a\le b\Rightarrow b \bullet a^\star \le b$ , in any Kleene algebra (Kozen Reference Kozen1994). It thus remains to check that

\begin{equation*}\mathit{id}_e+f\ast f^\star\le f^\star,\qquad f \ast g \le g\Rightarrow f^\star \ast g \le g,\qquad g \ast f \le g\Rightarrow g \ast f^\star \le g\end{equation*}

hold in the convolution algebra $K^X$ , where $\mathit{id}_e$ indicates the single unit e in E.

1. (1) $\mathit{id}_e+f\ast f^\star = f^\star$ . If $x=e$ , then $(\mathit{id}_e + f \ast f^\star)\, e = 1 + (f\, e) \bullet (f\, e)^\star = (f\, e)^\star = f^\star \, e$ . Otherwise, if $x\neq e$ ,

   \begin{align*} (\mathit{id}_e + f \ast f^\star)\, x &= \sum \left\{f\, y\bullet f^\star\, z \mid R^x_{yz}\right\}\\&= f\, e \bullet f^\star \, x + \sum \left\{f\, y\bullet f^\star\, z \mid R^x_{yz}\land y \neq e\right\}\\&= f\, e \bullet f^\star \, e \bullet \sum \left\{f\, y\bullet f^\star\, z \mid R^x_{yz}\land y \neq e\right\} + \sum \left\{f\, y\bullet f^\star\, z \mid R^x_{yz} \land y\neq e \right\}\\&= \left(f\, e \bullet f^\star \, e + \mathit{id}_e\, e\right) \bullet \sum \left\{f\, y\bullet f^\star\, z \mid R^x_{yz} \land y \neq e\right\}\\&= \left(f\, e\right)^\star \bullet \sum \left\{f\, y\bullet f^\star\, z \mid R^x_{yz}\land y\neq e\right\}\\&=f^\star \, x.\end{align*}

2. (2) $\left(\forall x.\ (f \ast g)\, x \le gx\right)\Rightarrow \left(\forall x.\ (f^\star \ast g)\, x \le gx\right)$ . We proceed by induction on $|x|$ .

3. a. Let $|x|=0$ and hence $x=e$ . Then, $(f^\star \ast g)\, e = (f\, e)^\star \bullet g\, e \le g\, e$ follows from the assumption $f\, e\bullet g\, e\le g\, e$ and the first induction axiom of Kleene algebra.

4. b. Let $|x|>0$ and therefore $x\neq e$ . Then, by the induction hypothesis, $\left(f\ast g\right)\, y\le g\, y$ holds for all y with $|y|< |x|$ . In addition, the assumption implies that

   \begin{equation*} \forall x,y,z.\ R^x_{yz} \Rightarrow f\, y\bullet g\, z\le g\, x, \end{equation*}
   from which $(f\, e)^\star\bullet g\, x = f^\star\, e \bullet g\, x \le g\, x$ follows by star induction in K. With this property,
   \begin{align*} (f^\star \ast g)\, x &= f^\star\, e \bullet g\, x +\sum \left\{f^\star\, e\bullet \sum\left\{f\, u \bullet f^\star\, v\mid R^y_{uv}\land u\neq e\right\} \bullet g\, z \mid R^x_{yz}\land y \neq e\right\}\\&= f^\star\, e \bullet \left(g\, x + \sum\left\{(f\, u \bullet f^\star\, v) \bullet g\, z \mid \exists y.\ R^y_{uv}\land R^x_{yz} \land u\neq e \wedge y\neq e\right\}\right)\\&= f^\star\, e \bullet \left(g\, x + \sum\left\{ f\, u \bullet (f^\star\, v \bullet g\, z) \mid \exists y.\ R^x_{uy}\land R^y_{vz} \land u\neq e \land y\neq e\right\}\right)\\&\le f^\star\, e \bullet \left(g\, x + \sum\left\{ f\, u \bullet (f^\star \ast g)\, y \mid R^x_{uy}\land u\neq e \right\}\right)\\&\le f^\star\, e \bullet \left(g\, x + \sum\left\{ f\, u \bullet g\, y\mid R^x_{uy} \right\}\right)\\&\le f^\star\, e \bullet \left(g\, x + (f\ast g)\, x\right)\\&= f^\star\, e \bullet \left(g\, x + g\, x\right)\\&\le g\, x.\end{align*}
   The first step unfolds the definition of convolution and the Kleene star in $K^X$ . The second step applies distributivity laws in K; the third one associativity in X and K. The fourth step introduces a convolution as an upper bound, thus dropping the constraint $y\neq e$ . The fifth step applies the induction hypothesis to y. The condition $u\neq e$ guarantees that $|y|<|x|$ . The sixth step applies the assumption; the last step the derived property.

5. (3) $g \ast f \le g\Rightarrow g \ast f^\star \le g$ follows by opposition from (2).

The following theorem is then immediate.

Theorem. If X is a graded relational interchange monoid with unit e and K an interchange Kleene algebra, then $K^X$ is an interchange Kleene algebra.

A generalisation of this theorem to more than one relational unit is left for future work; it seems to require a different proof technique.

We have already discussed the relationship between interchange quantales and concurrent quantales in Section 5, namely that concurrent quantales are interchange quantales in which is commutative and . Similarly, concurrent semirings and concurrent Kleene algebras are interchange semirings and interchange Kleene algebras satisfying these two conditions. It is then a trivial consequence of Theorem 6, Corollaries 24 and 17 that $S^X$ is a concurrent semiring if S is a concurrent semiring and X a finitely decomposable relational monoid. Similarly, by Theorem 6 and these corollaries, $K^X$ is a concurrent Kleene algebra if K is a concurrent Kleene algebra and X a graded relational monoid.

In the setting of concurrent Kleene algebras (Hoare et al. Reference Hoare, Möller, Struth and Wehrman2011), Theorem 6 thus shows that for every graded relational interchange monoid with a single unit we get a concurrent Kleene algebra as a convolution algebra for free.

For $Q=\mathbb{B}$ , the situation becomes much simpler. Then, convolution specialises to a product between sets, $A\ast B= \{x \cdot y\mid x\in A, y\in B\}$ , as explained in the introduction; the star can be defined as a union of powers taken with respect to $\ast$ . Many models under consideration form a fortiori quantales. Others that are finitely generated, such as generalisations of regular languages to posets and pomsets, form concurrent Kleene algebras, but not necessarily concurrent quantales. They are best characterised as subalgebras of concurrent quantales that are closed under operations such as the two compositions, finite unions and the two Kleene stars mentioned at the beginning of this section.

7. Weighted Shuffle Languages

This extended example shows how weighted shuffle languages (Droste et al. Reference Droste, Kuich and Vogler2009) can be constructed with our approach. Yet an alternative view on relational interchange monoids is helpful. Obviously, the sets $\mathcal{P}\, (X\times X\times X)$ and $X\times X\to \mathcal{P}\, X$ are isomorphic. A ternary relation R can thus be seen as a multioperation $\odot:X\times X\to \mathcal{P}\, X$ defined by

\begin{equation*} x \in y\odot z \Leftrightarrow R^x_{yz}.\end{equation*}

It can be extended Kleisli-style to $\odot: \mathcal{P}\, S\to\mathcal{P}\, S\to \mathcal{P}\, S$ defined, for all $A,B\subseteq X$ , by

\begin{equation*}A\odot B = \bigcup \{x\odot y\mid x\in A\land y\in B\}.\end{equation*}

It follows that $(A\odot B)\, x = \bigvee\{A\, y \wedge B\, z\mid R^x_{yz}\}$ if the sets A and B are identified with their indicator functions. This turns $\odot$ into a convolution.

Overloading the multioperation $\odot$ and its extension allows rewriting the relational interchange laws more compactly in algebraic form. It is easy to see that relational associativity becomes

\begin{equation*} \{x\}\odot (x\odot z)= (x\odot y)\odot \{z\};\end{equation*}

the relational interchange law (RI7) becomes

Multisemigroups, multimonoids and other multialgebras have been studied in mathematics for many decades (Marty Reference Marty1934; Krasner Reference Krasner1983; Connes and Consani Reference Connes and Consani2010; Kudryavtseva and Mazorchuk Reference Kudryavtseva and Mazorchuk2015). In computer science, they appear in the semantics of separation logic (Galmiche and Larchey-Wendling Reference Galmiche and Larchey-Wendling2006) and, very naturally, the algebra of shuffle. We have developed a multioperational approach to convolution, but for modal quantales and Kleene algebras instead of concurrent ones, in a companion article (Fahrenberg et al. 2021 b), see also Cranch et al. (Reference Cranch, Doherty and Struth2020) for the relationship between relational monoids and multimonoids.

The shuffle of two words from an alphabet $\Sigma$ is a multioperation $\|: \Sigma^\ast \to \Sigma^\ast \to \mathcal{P}\,\Sigma^\ast$ . It can be defined recursively as

\begin{equation*} v\| \varepsilon = \{v\} = \varepsilon\| v,\qquad\text{ and }\qquad (av) \| (bw)= \{a\}\cdot (v\| (bw)) \cup \{b\} \cdot ((av)\|w),\end{equation*}

where a and b are letters, v and w words, and the language product $\cdot$ has been tacitly used in the second identity. It yields the shuffle or Hurwitz product

\begin{equation*}A\| B=\bigcup\{x\| y\mid x\in A \land y\in B\}\end{equation*}

for $A,B\subseteq \Sigma^\ast$ at language level.

To construct the quantale of Q-weighted shuffle languages using Theorem 5(1), it remains to check that the structure is a relational interchange monoid with shared unit where for word concatenation $\cdot$ and for shuffle.

It is of course straightforward to verify that is a relational monoid: it is in fact isomorphic to the free monoid $(\Sigma^\ast,\cdot,\varepsilon)$ and checking the relational associativity and relational unit laws in the first monoid amounts to checking their algebraic counterparts in the second one. Verifying that is a relational monoid – or $(\Sigma^\ast,\|,\varepsilon)$ a multimonoid – and that the relational interchange law (RI7) holds – or the interchange law $(w\|x)\cdot (y\| z) \subseteq (w\cdot y) \| (x\cdot z)$ with language product $\cdot$ in the left-hand term and word concatenation $\cdot$ in the right-hand one – is a surprisingly tedious exercise that requires nested inductions.

The result of this verification is summarised as follows.

The following corollary to Theorem 5(1) is then automatic.

Corollary 36. If Q is an interchange quantale with unit and commutative, then $Q^M$ is an interchange quantale with commutative and

The operation is similar to the standard convolution of formal power series, a Q-valued generalisation of the standard language product. The operation generalises the standard shuffle product $\|$ of languages to the Q-valued setting. Yet semirings or at least Kleene algebras are normally used as weight algebras. A grading on words is needed, and in this particular case, the length of words can be used. It is then obvious that $\Sigma^\ast_n$ – the set of words of length n – is finite whenever $\Sigma$ is finite. This yields the following corollary to Theorem 6.

Weighted languages are usually defined over semirings instead of dioids. Instead of Kleene algebras, one can then use star semirings (Droste et al. Reference Droste, Kuich and Vogler2009). The Kleene star can then be defined on $Q^M$ as before. We conjecture that Corollary 37 still holds for ordered star semirings, though we have not checked all details.

Shuffle languages are widely used in the interleaving semantics of concurrent programmes. The finite transition and Aczel traces of the rely-guarantee calculus (de Roever et al. Reference de Roever, de Boer, Hannemann, Hooman, Lakhnech, Poel and Zwiers2001), in particular, form concurrent quantales, which suffices at least for the analysis of safety and invariant properties. We expect that our generic recipe for building shuffle quantales and Kleene algebra from underlying relational interchange monoids can be beneficial for building more refined rely-guarantee algebras. In particular, our results open the door to probabilistic and other quantitative variants, using for instance the standard value quantale on the unit interval that is popular with such applications (Dongol et al. Reference Dongol, Hayes and Struth2021).

8. Partial Interchange Monoids

Next we prepare for our second example, namely of digraphs under serial and parallel composition. It is then natural to consider these compositions not as ternary relations, but as partial operations on graphs. This leads to more general notions of partial semigroups and monoids. Convolution based on partial semigroups and monoids has previously been studied in Dongol et al. (Reference Dongol, Hayes and Struth2016). First, we briefly recall the relationship between relational and partial monoids.

Definition 38 (Dongol et al. Reference Dongol, Hayes and Struth2016) A partial monoid is a structure $(S,\otimes, D, E)$ where S is a set, $D\subseteq S\times S$ the domain of definition of the composition $\otimes :D\to S$ , which is associative in the sense that

\begin{equation*} D\, x\, y \wedge D\, (x\otimes y)\, z \Leftrightarrow D\, y\, z\wedge D\, x\, (y\otimes z),\qquad D\, x\, y \wedge D\, (x\otimes y)\, z \Rightarrow x\otimes (y \otimes z) = (x\otimes y)\otimes z,\end{equation*}

and $E\subseteq X$ is a set of units, which satisfy

\begin{equation*} \exists e\in E.\ D\, e\, x\wedge e\otimes x= x,\qquad \exists e\in E.\ D\, x\, e\wedge x\otimes e= x,\qquad \forall e_1,e_2\in E.\ D\, e_1\, e_2 \Rightarrow e_1= e_2.\end{equation*}

This definition captures the following intuition of partiality, namely that the left-hand side of the identity $x\otimes (y \otimes z) = (x\otimes y)\otimes z$ is defined if and only if the right-hand side is, and, if either side is defined, then the two sides are equal. This notion of equality is known as Kleene equality. Categories, monoids and the interval algebras in Example 1, ordered pair algebras in Example 3 and heaplet algebras in Example 5 all form partial monoids. Instead of the unit axioms presented here, we could equally use those of object-free categories (Mac Lane 1998). The precise relationship between partial monoids and object-free categories is discussed in Cranch et al. (2020).

The relationship between partial and relational monoids is straightforward. A relational monoid (X,R,E) is functional if

\begin{equation*} R^x_{yz} = R^{x'}_{yz} \Rightarrow x = x' \qquad \text{ for all }x,x',y,z\in X.\end{equation*}

With every functional relational monoid (X,R,E), one can then associate a partial monoid $(X,\otimes,D,E)$ with $D\, y \,z \Leftrightarrow \exists x.\ R^x_{yz}$ and $y\otimes z$ being the unique $x\in X$ that satisfies $R^x_{yz}$ – if $D\, y\, z$ is defined. We are particularly interested in the converse construction.

Lemma 39. (Dongol et al. Reference Dongol, Hayes and Struth2021) If $(S,\otimes,D,E)$ is a partial monoid, then (S,R,E) is a (functional) relational monoid with

\begin{equation*}R^x_{yz}\Leftrightarrow x=y\otimes z\land D\, y\, z.\end{equation*}

Next we relate partial monoids with relational interchange monoids. Expressing a variant of the interchange law (I7) in the context of partial monoids requires once again an ordering on S. This motivates the following definition.

Definition 40. A preordered partial monoid is a structure $(S,\preceq,\otimes,D,E)$ such that $(S,\preceq)$ is a preorder, $(S,\otimes,D,E)$ a partial monoid, and $\otimes$ is order preserving in the sense that

\begin{equation*} x\preceq y \wedge D\, z\, x \Rightarrow z \otimes x\preceq z\otimes y \wedge D\, z\, y,\qquad x\preceq y \wedge D\, x\, z \Rightarrow x \otimes z\preceq y\otimes z \wedge D\, y\, z. \end{equation*}

Lemma 39 can then be generalised.

Lemma 41. Let $(S,\preceq,\otimes,D,E)$ be a preordered partial monoid. Then, (S,R) is a relational semigroup with

\begin{equation*}R^x_{yz}\Leftrightarrow x\preceq y\otimes z\land D\, y\, z.\end{equation*}

Proof. For relational associativity,

\begin{align*} \exists y.\ R^x_{uy} \land R^y_{vw}& \Leftrightarrow \exists y.\ x\preceq u\otimes y \land D\, u\, y \land y\preceq v\otimes w\land D\, v\, w\\& \Leftrightarrow x\preceq u\otimes (v\otimes w) \land D\, v\, w \land D\, u\, (v\otimes w)\\& \Leftrightarrow x\preceq (u\otimes v)\otimes w \land D\, u\, v \land D\, (u\otimes v)\, w\\& \Leftrightarrow \exists y.\ D\, y \, w \land y \preceq u\otimes v \land D\, u\, v \land x\preceq y \otimes w\\&\Leftrightarrow \exists y.\ R^y_{uv}\land R^x_{yw}. \end{align*}

However, the unit laws of preordered partial monoids need not translate to units in relational semigroups.

1. (1) $\exists e\in E.\ R^x_{ex}$ and $\exists e\in E.\ R^x_{xe}$ ,

2. (2) $\exists e\in E.\ R^x_{ey} \Rightarrow x\preceq y$ and $\exists e\in E.\ R^x_{ye} \Rightarrow x\preceq y$ .

In (2), it cannot generally be expected that $x=y$ . The relationship $x\preceq y$ cannot be captured directly within relational semigroups or monoids.

Definition 43. A partial interchange monoid is a structure such that and are preordered partial monoids, and the following interchange law holds:

(PI7)

In light of Lemmas 41 and 42, we cannot expect to relate partial interchange monoids directly with relational interchange monoids. But the relationship is straightforward if we forget relational units and restrict to a single monoidal unit.

1. (1) ,

2. (2) ,

3. (3) ,

4. (4) ,

5. (5) ,

6. (6) .

Proof. We show (3) as an example. Suppose and . Then, and and therefore , , and by (PI7). Hence, by the unit laws of partial monoids. The other proofs are similar and left to the reader.

With multiple units, it seems necessary to require that parallel units are sequential units for all elements, which is artificial.

From now on, we call relational interchange semigroup a relational interchange monoid in which units may be absent, and the small interchange laws (RI1)–(RI6) hold in addition to (RI7).

Lemma 45. If is a partial interchange monoid, then is a relational interchange semigroup with

Proof. We need to check that (PI7) implies (RI7).

This calculation does not depend on the presence of units. Small interchange laws hold in S by Lemma 44. These allow deriving the small relational interchange laws (RI1)–(RI6) as in the proof of (RI7). Hence, S is a relational interchange semigroup.

We could have used instead of in the proof of Lemma 45. Using an equational encoding for R, however, would have broken the proof. The following example shows that even (RI1) would break if two equational encodings were used.

Lemma 45 yields the following corollary to Theorem 5(1).

Corollary 47. If S is a partial interchange monoid with unit e and Q an interchange quantale, then $Q^S$ is a non-unital interchange quantale with convolutions

that satisfies the small interchange laws (I1)–(I6) in addition to (I7).

Unitality fails in general because the unit $\mathit{id}$ of need not be the unit of :

using Lemma 42(2), but not necessarily and similarly for . Obviously, the retract has unit $\mathit{id}$ ; only the retract does not have $\mathit{id}$ as a unit. To obtain equality, and hence unital interchange quantales, conditions on f are needed.

A partial interchange monoid is positive if e is a minimal element of S with respect to $\preceq$ . It satisfies the serial Riesz decomposition property if implies that there exists $x_1$ , $x_2$ such that $x_1\preceq y_1$ , $x_2\preceq y_2$ and . An analogous property is well-known from ordered vector spaces.

Proof. . The $\le$ -direction holds by antitonicity, the $\ge$ -direction by the above calculation. The proof of is similar.

To make $\mathit{id}$ antitone, it seems appropriate to require that e is minimal with respect to $\preceq$ and hence that the partial interchange monoid is positive. We also need to check that and preserve antitonicity.

Proof. Unitality follows from Lemma 48. It remains to show that $\mathit{id}$ is antitone and that and preserve antitonicity. The first fact follows from positivity. For preservation of , suppose $x\preceq y$ . Then,

For preservation of , suppose once again $x\preceq y$ . Then,

by Riesz decomposability of .

In sum, the results of this section show how the general lifting result from Theorem 5(1) specialised from relational interchange monoids to partial interchange monoids, which are preordered. But, perhaps surprisingly, units cannot generally be lifted. We have thus identified conditions on partial interchange monoids – positivity and a serial Riesz decomposition property – and restricted the convolution algebra to antitone functions that enable such a lifting. In the next section, we apply these results to weighted graph languages.

9. Weighted Graph Languages

Our second extended example shows how weighted graph languages can be constructed with our approach. A partial interchange monoid structure can be imposed on graphs in various ways. Partiality arises because, typically, the vertices of the graph operands are supposed to be disjoint. Henceforth, we mean digraph when we say graph. Graphs with undirected edges can be obtained from these in the obvious way.

Formally, we view graphs as binary relations on some set X. Let graphs $G_1$ and $G_2$ be disjoint, that is, they have disjoint vertex sets: $V_{G_1}\cap V_{G_2}=\emptyset$ . Their serial composition (complete join) and disjoint union (parallel composition) are defined as

\begin{equation*} G_1\cdot G_2=G_1\sqcup G_2\sqcup \, (V_{G_1} \times V_{G_2}),\qquad G_1\| G_2 = G_1\sqcup G_2,\end{equation*}

where $\sqcup$ denotes disjoint union. Both operations are standard (Courcelle and Engelfriet Reference Courcelle and Engelfriet2012). This turns graphs under serial composition into partial monoids, and graphs under parallel composition into partial abelian monoids.

A graph morphism $\varphi:G_1\to G_2$ between graphs $G_1$ and $G_2$ preserves edges:

\begin{equation*} (x,y)\in G_1\Rightarrow (\varphi\, x,\varphi\, y)\in G_2.\end{equation*}

A morphism $\varphi$ is faithful, or a graph embedding, if $(\varphi\, x,\varphi\, y)\in G_2$ implies $(x,y)\in G_1$ . A graph isomorphism is a bijective (on vertices) graph embedding. We write $G_1\cong G_2$ if there exists a graph isomorphism between $G_1$ and $G_2$ . We say that $G_1$ and $G_2$ are isomorphic or have the same graph type if $G_1\cong G_2$ and call $G/{\cong}$ the isomorphism class or graph type of G.

The subsumption relation $\preceq$ between graphs, which is defined by $G_1\preceq G_2$ if and only if there exists a bijective (on vertices) graph morphism $\varphi:G_2\to G_1$ , is a preorder. The associated subsumption equivalence $\simeq$ need not coincide with $\cong$ , as will be explained in Section 10. We now fix any set $\mathcal{G}$ of (di)graphs that contains the empty graph $\varepsilon$ and is closed under serial and parallel composition.

Proof. First, the partial associativity and unit laws, partial commutativity of disjoint union as well as partial isotonicity of the two compositions must be shown. This is routine. In the presence of a shared unit $\varepsilon,$ it then remains to verify (PI7). For this, we need the following isotonicity property of Cartesian products: $A\subseteq B$ implies $A\times C\subseteq B\times C$ and $C\times A\subseteq C\times B$ .

We only show that the weak interchange law

\begin{equation*} (G_1\| G_2)\cdot (G_3\| G_4)\preceq (G_1\cdot G_2)\|(G_2\cdot G_4) \end{equation*}

holds and leaves the remaining laws to the reader. We use the identity function on the $G_i$ to construct the bijective morphism. We need to show that $V_{(G_1\| G_2)\cdot (G_3\| G_4)}= V_{(G_1\cdot G_3)\|(G_2\cdot G_4)}$ and $(G_1\cdot G_1)\|(G_3\cdot G_4) \subseteq (G_1\| G_3)\cdot (G_2\| G_4)$ as a relation. First, $V_{G_i\cdot G_j} = V_{G_i}\cup V_{G_j} = V_{G_i\| G_j}$ and therefore

\begin{equation*} V_{(G_1\| G_2)\cdot (G_3\| G_4) }= V_{G_1} \cup V_{G_2}\cup V_{G_3}\cup V_{G_4}=V_{(G_1\cdot G_3)\|(G_2\cdot G_4)}. \end{equation*}

Second,

\begin{align*} (G_1\cdot G_1)\|(G_3\cdot G_4) &= (G_1\cup G_2\cup V_{G_1}\times V_{G_2})\|(G_3\cup G_4\cup V_{G_3}\times V_{G_4})\\ &= G_1\cup G_2\cup V_{G_1}\times V_{G_2}\cup G_3\cup G_4\cup V_{G_3}\times V_{G_4}\\ &\subseteq G_1\cup G_3\cup G_2\cup G_4 \cup (V_{G_1}\cup V_{G_3})\times (V_{G_2}\cup V_{G_4})\\&= (G_1\| G_3) \cup (G_2\| G_4) \cup V_{G_1\| G_3}\times V_{G_2\| G_4}\\& = (G_1\| G_3)\cdot (G_2\| G_4). \end{align*}

Lemma 45 and Corollary 47 then imply that weighted graph languages form interchange quantales up to unitality of the parallel quantale retract. But one can do better.

Proof. It is clear that $\varepsilon$ is an isolated point with respect to $\preceq$ and hence minimal. This proves positivity. The proof of serial decomposability is intuitive, but somewhat tedious to spell out formally. Suppose $G\preceq G_1\cdot G_2$ . Then, the vertices of $G_1$ and $G_2$ are disjoint, and in addition to the arrows of $G_1$ and $G_2,$ we have $V_{G_1}\times V_{G_2}$ . Hence if $G\preceq G_1\cdot G_2$ , then the arrows added by the bijective graph morphism $\varphi:G_1\cdot G_1 \to G$ must either be added to $G_1$ or to $G_2$ , while $V_{G_1}\times V_{G_2}$ stays the same. There must thus be $G_1'\preceq G_1$ and $G_2'\preceq G$ such that $G=G_1'\cdot G_2'$ .

Proposition 49 then specialises as follows.

Corollary 52. If Q is an interchange quantale with unit 1 and commutative, then $Q^\mathcal{G}$ is a (generally non-unital) interchange quantale with commutative and

The subquantale of antitone functions in $Q^\mathcal{G}$ is unital.

Labels can be added to vertices ad libitum, which yields proper weighted graph languages. Both the serial and the parallel composition preserve order properties, and it must be required that graph morphisms preserve labels. Corollary 52 then specialises immediately to weighted partial orders and weighted labelled partial orders. Their non-weighted variants are widely used in concurrency theory as partial order semantics (Vogler 1992) and in the theory of distributed systems (Lamport 1978). Our results thus yield quantitative variants.

Next we briefly consider such qualitative convolution algebras, which are based on powerset liftings, that is, $Q= \mathbb{B}$ . Then, $f:\mathcal{G}\to \mathbb{B}$ is a set indicator function, and we may write $x\in f$ instead of $f\, x$ , identifying the indicator function with the set it represents. Then,

rewrites as , and hence,

Similarly,

where $\downarrow$ denotes the down-closure with respect to $\preceq$ . Moreover, the antitonicity condition rewrites as $x\preceq y\land f\, y \Rightarrow f\, x$ , which is precisely $f=f{\downarrow}$ , that is, f is a down-set with respect to $\preceq$ .

10. Weighted Languages of Types of Finite Graphs

Many applications, including those in concurrency and distributed systems mentioned, require equivalence or isomorphism classes and hence types of (labelled) graphs or (labelled) partial orders. Lifting the results from Section 9 to these is not entirely straightforward. This is well known (Ésik Reference Ésik2002), but we spell out details to make them easier to access.

Example 55 (Ésik Reference Ésik2002). Consider the infinite poset $(P,\le_P)$ with

\begin{equation*} P=\{p_{i,j}\mid i,j\in \mathbb{N}\land (i=0\lor j=0)\} \end{equation*}

and $p_{i,j}\le_P p_{k,l}$ if and only if $i = k = 0$ and $j \le l$ . Consider also the infinite poset $(Q,\le_Q)$ with

\begin{equation*} Q=\{q_{i,j}\mid i,j\in \mathbb{N}\land (i=0\lor i=1 \lor j=0)\} \end{equation*}

and $q_{i,j}\le_P q_{k,l}$ if and only if $i = k = 0$ or $i=k=1$ , and $j\le l$ .

Intuitively, P consists of the disjoint union of the infinite chain formed by the $p_{0,j}$ and the $p_{i,0}$ with $i> 0$ , whereas Q consists of the disjoint union of the infinite chain formed by the $p_{0,j}$ , the infinite chain formed by the $p_{1,j}$ and the elements $p_{i,0}$ with $i\ge 1$ .

Define the functions $\varphi:P\to Q$ and $\psi:Q\to P$ by

\begin{equation*} \varphi\, p_{i,j} = \begin{cases} q_{0,j} & \text{ if } i=0,\\q_{1,k} & \text{ if } i > 0 \land j = 2k+1,\\q_{k,0} & \text{ if } i > 0 \land j = 2k, \end{cases}\qquad \psi\, q_{i,j} = \begin{cases} p_{0,2k} & \text{ if } i=0,\\p_{1,2k+1} &\text{ if } i=1,\\p_{i-1,0} & \text{ if } i > 1. \end{cases}\end{equation*}

Intuitively, $\varphi$ maps the chain in P onto the first chain in Q and the isolated elements in P alternatingly onto the second chain and the isolated elements in Q, whereas $\psi$ maps the elements of the two chains in Q alternatingly onto the chain in P, and isolated points in Q onto isolated points in P. The morphisms are shown in Figure 5.

Figure 5. Posets P and Q with bijective morphisms $\varphi$ in left diagram and $\psi$ in right diagram.

By construction, $\varphi$ and $\psi$ are both bijective and order preserving. Hence $P\preceq Q$ and $Q\preceq P$ , but of course neither $P=Q$ nor $P\cong Q$ .

At least in the finite case, the situation is simpler. An explanation requires two simple standard facts about groups, which we recall without proofs.

Lemma 57. Let G be a finite cyclic group of order n generated by x. Then

\begin{equation*} G=\left\{1,x,x^2,\dots, x^{n-1}\right\}\qquad { and }\qquad x^n=1. \end{equation*}

Proof. By assumption, there exist order preserving bijections $\varphi:G_2\to G_1$ and $\psi:G_1\to G_2;$ hence $, \chi=\psi\circ \varphi$ is an order preserving bijection on $G_1$ . As $\chi$ can be seen as a group action on the finite set $V_1$ , it generates a finite cyclic group. Hence there is some $k\in\mathbb{N}$ such that $\chi^k=\mathit{id}_{V_1}$ by Lemma 57. It then follows that f is faithful: Suppose $(\varphi\, x,\varphi\, y)\in G_2$ . Then

\begin{equation*} x = \chi^k\, x = \chi^{k-1}(\psi(\varphi\, x))\to_{R _1} \chi^{k-1}(\psi(\varphi\, y)) = \chi^k\, y = y. \end{equation*}

It follows that $\varphi$ is a graph isomorphism and $G_1\cong G_2$ .

A similar fact has been proved by Ésik (Reference Ésik2002). We henceforth restrict our attention to finite graphs.

Let $[G]=\{G'\mid G'\cong G\}$ denote the type of G. We extend the subsumption preorder $\preceq$ to equivalence classes by $[G_1]\preceq [G_2]\Leftrightarrow G_1\preceq G_2$ , overloading notation. This relation is well defined.

Proof. Let $\varphi_1$ be the graph isomorphism of type $G_1\to G_1'$ , $\varphi_2$ the graph isomorphism of type $G_2'\to G_2$ and $\psi$ the bijective graph morphism of type $G_2\to G_1$ . Then, $\varphi_1\circ \psi\circ \varphi_2:G_2'\to G_1'$ is a bijective graph morphism as well. Hence $G_1' \preceq G_2'$ .

Proof. Reflexivity and transitivity for $\preceq$ on $\mathcal{G}/{\cong}$ follows from reflexivity and transitivity of $\preceq$ on $\mathcal{G}$ . For antisymmetry, $[G_1]\preceq [G_2]$ and $[G_2]\preceq [G_1]$ imply $[G_1]=[G_2]$ for all $G_1,G_2\in\mathcal{G}$ by Lemma 58.

Extending serial and parallel composition of graphs is standard:

\begin{equation*} [G_1]\cdot [G_2]=\{G_1'\cdot G_2'\mid G_1'\cong G\wedge G_2'\cong G\}\end{equation*}

and likewise for $[G_1]\| [G_2]$ . It is also known that both compositions are well defined: if $G_1\cong G_1'$ and $G_2\cong G_2'$ , then $[G_1]\cdot[G_2]=[G_1']\cdot [G_2']$ and $[G_1]\|[G_2]=[G_1']\| [G_2']$ . By contrast to serial and parallel compositions of graphs, those operations on graph types are total. Finally, equivalence classes are closed with respect to serial and parallel composition.

1. (1) $[G_1\cdot G_2] = [G_1]\cdot [G_2]$ ,

2. (2) $[G_1\| G_2] = [G_1]\|[G_2]$ .

Proof. $H\in [G_1\cdot G_2]$ if and only if $H\cong G_1\cdot G_2$ . This is the case if and only if there are graphs $G_1'$ and $G_2'$ such that $H=G_1'\cdot G_2'$ and $G_1'\cong G_1$ and $G_2'\cong G_2$ , which, in turn, holds if and only if $H\in [G_1]\cdot [G_2]$ . The proof for $\|$ is similar.

Proof. The associativity, commutativity and unit laws are easy to check, noting that $[\varepsilon]=\{\varepsilon\}$ . For the interchange law, $[(G_1\| G_2)\cdot (G_3\| G_4)]\preceq [(G_1\cdot G_3)\|(G_2\cdot G_4)]$ , by definition of $\preceq$ on equivalence classes, it suffices to show that $(G_1\| G_2)\cdot (G_3\| G_4)\preceq (G_1\cdot G_3)\|(G_2\cdot G_4)$ , which holds by Proposition 9.

Proposition 62 specialises immediately to types of finite partial orders with serial and parallel composition, which are known as partial words or pomsets in concurrency theory – when vertex labels are added (Grabowski Reference Grabowski1981; Gischer Reference Gischer1988). The instance of Proposition 62 for pomsets is due to Gischer (Reference Gischer1988).

Because compositions in $\mathcal{G}/{\cong}$ may result in the empty set, the interchange monoid usually has an annihilator 0, that is, an element for which $x\cdot 0=0= 0\cdot x$ and $x\| 0 = 0$ holds for any x.

The lifting to convolution algebras – interchange quantales, unital interchange quantales, interchange Kleene algebras – then follows the results of the previous section, and of course Theorem 5(1). The result that the powerset lifting of finite pomsets yields concurrent semirings, interchange semirings in which is commutative and $Q=\mathbb{B}$ , is due to Gischer (Reference Gischer1988). Extensions to concurrent Kleene algebras and concurrent quantales have been proved more recently (Hoare et al. Reference Hoare, Möller, Struth and Wehrman2011).

This finishes the construction of the graph and pomset language models of concurrent quantales and Kleene algebras as a second paradigmatic model of concurrency within our convolution algebra framework and its extension to quantitative applications.