Das Kapitel vertieft sich in die Vereinheitlichung von Prozess-Algebren durch die Einführung übersprungener Unified-Star-Ausdrücke, einer Verallgemeinerung von 1-free-Star-Ausdrücken und übersprungenen GKAT-Programmen. Es untersucht die Axiomatisierung der Doppelähnlichkeit dieser Ausdrücke und bietet ein umfassendes Rahmenwerk, das verschiedene rechnerische Effekte wie Nichtdeterminismus und Wahrscheinlichkeit umfasst. Der Text baut auf bestehenden Arbeiten von Grabmayer und Fokkink auf und erweitert deren Vollständigkeitstheorem auf eine breitere Klasse von Prozess-Algebren. Sie stellt Schlüsselkonzepte wie unterstützte und formbare Gleichungstheorien vor, die für die Vollständigkeit der Axiomatisierung entscheidend sind. Das Kapitel stellt auch neue Vollständigkeitstheoreme für spezifische Prozess-Algebren vor, einschließlich probabilistischer regulärer Ausdrücke und probabilistischer GKAT. Die detaillierte Erforschung gut geschichteter Diagramme und ihrer Lösungen sowie die Anpassung der Korrekturtechniken von Grabmayer und Fokkink machen dieses Kapitel zu einem bedeutenden Beitrag auf dem Gebiet der Prozess-Algebren und ihrer Axiomatisierung. Der Text diskutiert auch die Implikationen des vereinheitlichenden Rahmenwerks für zukünftige Forschung und potenzielle Erweiterungen und betont seine Relevanz und potenziellen Auswirkungen auf die Untersuchung von Computereffekten und Prozesssemantik.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We consider process algebras with branching parametrized by an equational theory \(\textsf{T}\), and show that it is possible to axiomatize bisimilarity under certain conditions on \(\textsf{T}\). Our proof abstracts an earlier argument due to Grabmayer and Fokkink (LICS’20), and yields new completeness theorems for skip-free process algebras with probabilistic (guarded) branching, while also covering existing completeness results.
1 Introduction
Regular expressions generated by a set of action symbols \( Act \) are classically interpreted as regular languages, i.e., sets of words over \( Act \) obtained by the usual union, concatenation, and Kleene star operations [11]. Inspired by the introduction of process algebra as a formalization of communicating and concurrent processes, Milner gave an interpretation of regular expressions in terms of nondeterministic machine behaviours, i.e., up to bisimilarity [15]. The labelled transition system obtained from a regular expression is constructed by interpreting the union operation as nondeterministic choice instead of language union and the Kleene star operation as a (finite) loop instead of repeated language concatenation. Although introduced many years apart, Milner’s interpretation of regular expressions is now known to be equivalent to Antimirov’s derivative construction [2].
Milner transformed Salomaa’s axioms for language equivalence of regular expressions [24] into sound axioms for his behavioural semantics, and left completeness as an open problem. This problem was only recently solved by Grabmayer [5], who was able to reduce the problem to results in a prior collaborative work with Fokkink [6]. In op. cit., the authors prove that Milner’s axioms are complete when restricted to a subset of regular expressions that they call 1-free star expressions, which are regular expressions in which 1 (the unit for concatenation) does not appear, and the Kleene star is replaced by a binary star operation \(r_1 * r_2\).
Anzeige
Around the same time, Smolka et al. [29] introduced guarded Kleene algebra with tests (or GKAT) for reasoning about simple imperative programs. Essentially, GKAT is a restriction of Kleene algebra with tests (or KAT) [12] to programs constructed out of if-then-else and while.1 In [29], the authors proposed an infinitary axiomatization of equivalence between GKAT programs. They left open whether a finitary version of these axioms, similar to Milner’s, is also complete.
More recently, a step towards proving completeness of GKAT was taken in [9]. In that paper, it was shown that the finitary axiomatization of GKAT proposed in [29] is complete when restricted to GKAT programs that are 1-free in a sense similar to 1-free star expressions. The program that acts like \(1\) in GKAT is skip, so the authors of [9] refer to these programs as skip-free GKAT programs. To achieve this result, it was necessary to analyze some tricky steps in the original completeness proof from [6], and adapt them to the setting of skip-free GKAT.
In this paper, we study a unifying generalization of 1-free star expressions and skip-free GKAT programs that we call skip-free unified-star expressions. This generalization is based on the observation in [25, 28] that 1-free star expressions and skip-free GKAT programs can be seen as instances of process algebras parametrized by equational theories, which capture computational effects such as nondeterminism and probability via their corresponding monads [18, 19].
Our main contribution is a complete axiomatization for each process algebra in this class, provided the equational theory satisfies two conditions that we refer to as admitting a support and malleability. These properties essentially allow us to employ the strategy used by Grabmayer and Fokkink in [6], but in a much more abstract setting. The equational theories that correspond to 1-free star expressions and skip-free GKAT admit a support and are malleable, and so our abstract completeness theorem generalizes the results from [6, 9]. We furthermore obtain several new completeness theorems for bisimilarity semantics of process algebras considered in the literature, including one for the skip-free fragment of probabilistic regular expressions studied in [22] and another for a skip-free variation of the probabilistic version of GKAT studied in [21].
Anzeige
We assume the reader is familiar with the basics of category theory, i.e., functors, universal properties, and natural transformations (see, for example, [20]). Omitted proofs can be found in the full version of the paper [8].
2 1-free Star Expressions
To set the stage, we begin with a brief description of Grabmayer and Fokkink’s completeness theorem and its proof technique [6]. Fix a set of action symbols\( Act \). The set of 1-free star expressions\( StExp \) is generated by the grammar below.
The operators \(+\) and \(\cdot \) are to be interpreted as nondeterministic choice and sequential composition, respectively. The expression \(r_1*r_2\) is intended to mean “run \(r_1\) some number of times, and then run \(r_2\)” (cf. the regular expression \(r_1^* r_2\)). In the absence of parentheses, \(*\) takes precedence over \(\cdot \), which is evaluated before \(+\). So, \(a + b\cdot c * d\) should be read as \(a + (b \cdot (c * d))\). We typically write \(r_1r_2\) instead of \(r_1 \cdot r_2\). The process semantics for 1-free star expressions can be phrased in terms of a variant of labelled transition systems called charts.
Definition 2.1
A chart is a pair \((X, \delta )\) consisting of a set of states\(X\) and a transition function\(\delta :X \rightarrow \mathcal {P}( Act \times (\checkmark + X))\). Here, \(\mathcal {P}\) is the finite powerset functor, \(\checkmark \) denotes the set \(\{\checkmark \}\), and \(+\) is disjoint union. Given \(x,y \in X\) and \(a \in Act \), we write
if \((a, y) \in \delta (x)\), and
if \((a, \checkmark ) \in \delta (x)\).
Immediately we see that \(\delta \) can be either specified as a function or as a set of transition relations
, one for each \(a \in Act \). We usually drop subscripts if the transition function can be inferred from context. We write \({\rightarrow }\) for the union of the transition relations and say that \(x\)transitions to \(y\) if \(x \rightarrow y\).
Given \((X, \delta )\) and \(U \subseteq X\), define \(\langle U \rangle _\delta = \{y \mid \exists x \in U, x \rightarrow _\delta ^* y\}\). The subchart of\((X, \delta )\)generated by U is \((\langle U\rangle _\delta , \delta _U)\), where \(\delta _U: \langle U \rangle _\delta \rightarrow \mathcal {P}( Act \times (\checkmark + \langle U \rangle _\delta ))\) is simply \(\delta \) restricted to \(\langle U \rangle _\delta \); we also write \(\langle U \rangle _\delta \) for this chart. When \(x \in X\), we may write \(\langle x \rangle _\delta \) for \(\langle \{x\}\rangle _\delta \), and speak of the subchart of\((X, \delta )\)generated byx.
The set of 1-free star expressions itself carries a chart structure, whose transitions are derived inductively from the inference rules in Fig. 1, in a way that is reminiscent of Antimirov’s automaton construction [2]. We use \(( StExp , \delta )\) to denote this chart structure, and refer to it as the syntactic chart.
Fig. 1.
Rules defining the transition structure of the syntactic chart \(( StExp , \delta )\). In the above, \(a \in Act \), \(r_1,r_2,s \in StExp \), and \(\xi \in \checkmark + StExp \).
Every 1-free star expression \(r\) generates a finite subchart \(\langle r\rangle \) of \(( StExp , \delta )\): the syntactic chart of \(r\). The equivalence for 1-free star expressions that Grabmayer, Fokkink, and Milner sought to axiomatize is bisimilarity, defined as follows.
Definition 2.2
A bisimulation between charts \((X, \delta _X)\) and \((Y, \delta _Y)\) is a relation \(R \subseteq X \times Y\) such that for any \((x,y) \in R\) and \(a \in Act \), (1)
if and only if
, (2) if
, then there is a \((x',y') \in R\) such that
, and (3) if
, then there is a \((x',y') \in R\) such that
. We write
and say that \(x\) and \(y\) are bisimilar if \((x, y) \in R\) for some bisimulation \(R\).
Note that the relation
is the largest bisimulation between two charts. Furthermore,
is an equivalence relation when restricted to a single chart. Another notion that we will rely on is that of a chart homomorphism.
Definition 2.3
A homomorphism of charts \(h :(X, \delta _X) \rightarrow (Y, \delta _Y)\) is a function \(h :X \rightarrow Y\) such that the graph of \(h\) is a bisimulation.
It is straightforward to show that charts and chart homomorphisms form a category, i.e., identity maps \(\textrm{id}:(X, \delta ) \rightarrow (X, \delta )\) are homomorphisms and any composition of homomorphisms is a homomorphism. Furthermore, bisimilarity can be characterized using chart homomorphisms, via the following lemma.
Lemma 2.4
Given states \(x \in X\) and \(y \in Y\) of charts \((X, \delta _X)\) and \((Y, \delta _Y)\),
if and only if there is a third chart \((Z, \delta _Z)\) and chart homomorphisms \(h :(X, \delta _X) \rightarrow (Z, \delta _Z)\) and \(k :(X, \delta _X) \rightarrow (Z, \delta _Z)\) such that \(h(x) = k(y)\).
This characterization is useful in several ways; for one, it connects the existing notion of bisimilarity of charts to the more abstract definition in the next section. Another consequence of Lemma 2.4 is that for charts \((U, \delta _U)\) and \((X, \delta )\) with \(U \subseteq X\), \((U, \delta _U)\) is a subchart of \((X, \delta )\) generated by U if and only if the inclusion map \(U \hookrightarrow X\) is a chart homomorphism. Furthermore, for any \(r,s \in StExp \),
as states of \(( StExp , \delta )\) iff they are bisimilar as states of \(\langle r \rangle \) and \(\langle s\rangle \) respectively.
Axiomatization. Milner showed that bisimilarity is a congruence with respect to the regular expression operations [15]. This led him to give axioms for bisimilarity using a variation on Salomaa’s axioms for language equivalence of regular expressions [24]. Grabmayer and Fokkink adapted these axioms for 1-free regular expressions in [6], which we recall in Fig. 2.2 For reasons that will become clear in Section 3, we write \(\textsf{SL}^*\) to denote the theory in the figure.
Fig. 2.
The axioms proposed by Grabmayer and Fokkink in [6]. The theory \(\textsf{SL}^*\) consists of the axioms above and equational logic (not pictured above).
Definition 2.5
Given \(r_1,r_2 \in StExp \), we write \(\textsf{SL}^* \vdash r_1 = r_2\) if there is a derivation of the equation \(r_1 = r_2\) from the axioms of \(\textsf{SL}^*\).
(Soundness and completeness of\(\textsf{SL}^*\)). Let \(r_1, r_2 \in StExp \). Then \(\textsf{SL}^* \vdash r_1 = r_2\) if and only if
as states in \(( StExp , \delta )\).
The forward direction is called soundness, and it can be proven by induction on derivations. The reverse direction is completeness, and requires a more involved proof with several steps. To arrive at the completeness result, some mathematical machinery has to be developed, and two particularly treacherous proofs have to be worked out. In the remainder of this section, we give an overview of the necessary techniques as preparation for our abstract approach in the sequel.
The Completeness Proof. The first step on our journey is to cast a chart as a system of equations and to study its solutions. Formally, given a chart \((X, \delta )\), we treat each state \(x \in X\) as an unknown, and add the formal equation \(x = a_1 x_1 + \cdots + a_n x_n + b_1 + \cdots + b_m\), with the right-hand side determined by the transition function at \(x\), \(\delta (x) = \{(a_1, x_1), \dots , (a_n, x_n), (b_1, \checkmark ), \dots , (b_m, \checkmark )\}\).
A solution to the system of equations for \((X, \delta )\) maps states to expressions in a way that satisfies the equations, up to equivalence. To formalize this, we need some notation: for a finite set of 1-free star expressions \(S = \{r_1, \dots , r_n\}\), we write \(\sum _{r \in S} r\) to denote \(r_1 + \cdots + r_n\). This is well-defined up to equivalence, because the axioms in Fig. 2 include commutativity and associativity. If \(S = \{r \in StExp \mid P(r)\}\) for some finite predicate \(P\), we write \(\sum _{P(r)} r\) instead of \(\sum _{r \in S} r\).
Definition 2.7
A solution to a chart \((X, \delta )\) is a map \(\phi :X \rightarrow StExp \) such that for any \(x \in X\),
. Two solutions \(\phi ,\psi \) are equivalent if for any \(x \in X\), \(\textsf{SL}^* \vdash \phi (x) = \psi (x)\). A chart \((X, \delta )\) is said to have a unique solution if it has exactly one solution up to equivalence.
Example 2.8
Let \(X = \{ x, x' \}\) and suppose \((X, \delta _X)\) is the chart below.
A solution to \((X, \delta _X)\) is a function \(\phi : X \rightarrow StExp \) such that \( \textsf{SL}^* \vdash \phi (x) = a \cdot \phi (x') +~\hbox {b} \) and \( \textsf{SL}^* \vdash \phi (x') = c \cdot \phi (x') +~\hbox {d} \). The trick to solving this system is to apply the last axiom in Figure 2 to the second equation, and choose \(\phi (x') = c*d\). If we also set \(\phi (x) = b + a(c*d)\), then \(\phi \) is a solution by construction.
The following property corresponds to [27, Lemma 2.2] and [27, Theorem 2.2], which characterize solutions to charts as chart homomorphisms into the quotient of \( StExp \) by provable equivalence. Given \(r_1,r_2 \in StExp \), write \(r_1 \equiv r_2\) to denote that \(\textsf{SL}^* \vdash r_1 = r_2\), and write \([r_1]_\equiv \) to denote the \(\equiv \)-equivalence class of \(r_1\).
Proposition 2.9
There is a unique \([\delta ]_\equiv : StExp /{\equiv } \rightarrow \mathcal {P}( Act \times (\checkmark + StExp /{\equiv }))\) such that the quotient \([-]_\equiv : StExp \rightarrow StExp /{\equiv }\) is a chart homomorphism from \(( StExp , \delta )\) to \(( StExp /{\equiv }, [\delta ]_\equiv )\). Moreover, \(\phi :X \rightarrow StExp \) is a solution to a chart \((X, \delta )\) if and only if \([-]_\equiv \circ \phi :(X, \delta ) \rightarrow ( StExp /{\equiv }, [\delta ]_\equiv )\) is a chart homomorphism.
Proposition 2.9 has several consequences, including the following two observations, which appear as [6, Proposition 5.1] and [6, Proposition 2.9].
Proposition 2.10
Let \(h :(X, \delta _X) \rightarrow (Y, \delta _Y)\) be a chart homomorphism, and let \(\phi :Y \rightarrow StExp \) be a solution to \((Y, \delta _Y)\). Then \(\phi \circ h\) is a solution to \((X, \delta _X)\). Also, for any \(r \in StExp \), the inclusion map \(\langle r \rangle \hookrightarrow StExp \) is a solution to \(\langle r \rangle \).
Grabmayer and Fokkink’s completeness proof strategy requires the construction of a distinguished class of charts \(\mathcal C\) satisfying all of the following properties:
(Expressivity)
For each \(r \in StExp \), the chart \(\langle r \rangle \) is in \(\mathcal C\).
(Closure)
\(\mathcal C\) is closed under homomorphic images. That is, if there is a surjective chart homomorphism \((X, \delta _X) \rightarrow (Y, \delta _Y)\) and \((X, \delta _X) \in \mathcal C\), then \((Y, \delta _Y) \in \mathcal C\).
(Solvability)
Every chart \((X, \delta ) \in \mathcal C\) admits a unique solution.
The restriction of surjectivity in the second property is relatively mild: any chart homomorphism \(h: (X, \delta _X) \rightarrow (Y, \delta _Y)\) can be restricted to a homomorphism onto its image via standard techniques [23]. If a class satisfying these properties exists, then the completeness of \(\textsf{SL}^*\) for bisimilarity can be argued as follows.
Proof
(Theorem 2.6,2.6, completeness direction). Let \(r_1,r_2 \in StExp \) and suppose
. Then there is a chart \((Z, \delta )\) and chart homomorphisms \(h_i :\langle r_i\rangle \rightarrow (Z, \delta )\) for \(i \in \{1, 2\}\) such that \(h_1(r_1) = h_2(r_2)\). Let \(z = h_1(r_1) = h_2(r_2)\), and note that \(\langle z\rangle = h_1(\langle r_1\rangle ) = h_2(\langle r_2 \rangle )\). In particular, \(\langle z\rangle \) is the homomorphic image of \(\langle r_1\rangle \). By (Expressivity), \(\langle r_1\rangle \in \mathcal C\). By (Closure), \(\langle z\rangle \in \mathcal C\), because it is the homomorphic image of \(\langle r_1\rangle \). By (Solvability), \(\langle r_1\rangle \), \(\langle r_2\rangle \), and \(\langle z\rangle \) all admit unique solutions. Let \(\phi :\langle z \rangle \rightarrow StExp \) be the solution to \(\langle z \rangle \). By Proposition 2.10, \(\phi \circ h_i\) is a solution to \(\langle r_i \rangle \) for \(i \in \{1,2\}\). Since the inclusions \(\langle r_i \rangle \hookrightarrow StExp \) are also solutions, by uniqueness \( \textsf{SL}^* \vdash r_1 = \phi \circ h_1(r_1) = \phi \circ h_2(r_2) = r_2 \), as desired.
Well-layered Charts and Solutions. For the rest of the section, we focus on a class \(\mathcal C\) that satisfies the three properties above. Milner already observed that not every chart admits a solution [15]. This stands in sharp contrast with the situation for regular expressions considered up to language equivalence, where every automaton can be transformed into an equivalent regular expression by Kleene’s theorem. To address this, Grabmayer and Fokkink proposed LLEE charts, which were later refined into well-layered charts in [27].
Definition 2.11
([27, Definition 4.1]). Let \((X, \delta )\) be a chart. An entry/body labelling of \((X, \delta )\) is a partition of \({\rightarrow _\delta } \subseteq X \times X\) into two relations: loop entry transitions, denoted
, and body transitions, denoted
.
We write \(x \curvearrowright y\) and say that \(x\)loops-around-to\(y\) if there is a sequence of transitions
such that \(x \notin \{x_1, \dots , x_n\}\).
An entry/body labelling of \((X, \delta )\) is well-layered if it satisfies the following additional properties. Write \((-)^+\) for transitive closure.
1.
We do not have
for any \(x \in X\).
2.
For any \(x,y \in X\), if
, then
.
3.
The directed graph \((X, \curvearrowright )\) is acyclic.
4.
For any \(x,y \in X\), if \(x \curvearrowright y\), then we do not have \(y \rightarrow \checkmark \).
A chart is well-layered if (1) it has a well-layered entry-body labelling, and (2) is locally finite in the sense that for any \(x \in X\), \(\langle x \rangle \) is finite.
As we have already seen, \(( StExp , \delta )\) is locally finite. The equivalence between LLEE charts and well-layered charts is explained in [27, Remark 4.1].
The loop entry transitions in a well-layered entry/body labelling are to be interpreted as the first transition that enters a program loop. This is formally captured by the entry/body labelling on \(( StExp , \delta )\) given as follows: loop entry transitions are those that can be derived from the rules
(2)
Body transitions are all other transitions. The following result is stated as [27, Lemma 4.1], but follows directly from [6, Proposition 3.7] and the equivalence between LLEE charts and well-layered charts.
Proposition 2.12
The entry/body labelling of the chart \(( StExp , \delta )\) given in (2) is well-layered. It follows that \(\langle r \rangle \) is well-layered for any \(r \in StExp \).
The second statement in Proposition 2.12 follows from the first: it is a direct consequence of Definition 2.11 and the properties of subcharts that if
is a well-layered entry/body labelling of \((X, \delta )\), then
is also a well-layered entry/body labelling of the generated subchart \(\langle U \rangle _\delta \).
If we choose the class of well-layered charts for \(\mathcal {C}\), then Proposition 2.12 is (Expressivity). (Closure) is stated below as Theorem 2.13, which is a mild strengthening of [6, Theorem 6.9] that appears as [27, Theorem 4.1].
Theorem 2.13
(Grabmayer-Fokkink). The class of well-layered charts is closed under homomorphic images.
Theorem 2.13 is the crux of the completeness proof in [6], and took an enormous amount of ingenuity to prove. We will rely on this result later, in Section 5, when we prove our general completeness theorem.
Finally, let us discuss (Solvability), i.e., existence and uniqueness of solutions, which is the last of the pieces needed in the completeness proof for 1-free star expressions. Grabmayer and Fokkink offer the following inductively defined formula for computing the unique solution to a well-layered chart at each state.
Definition 2.14
Given a well-layered entry/body labelling
of a chart \((X, \delta )\), define the following two quantities: given \(x \in X\), let \( |x|_{en} = \max \{n \mid \exists y \in Y, x \curvearrowright ^n y\} \) and
.
We define \(\phi _\delta : X \rightarrow StExp \) inductively on \(|x|_{bo}\) as follows:
(3)
in which we define for each pair of states such that \(x \curvearrowright y\) the term \(t_\delta (y, x)\) below, by induction on the lexicographical ordering of \(\mathbb {N}\times \mathbb {N}\):
(4)
The following corresponds to [6, Proposition 5.5] and [6, Proposition 5.8], and establishes (Solvability) for well-layered charts.
Proposition 2.15
Let \((X, \delta )\) be a well-layered chart with entry/body labeling
. Then \(\phi _\delta \) as derived from
in Definition 2.14 is the unique solution to \((X, \delta )\). In particular, \(\phi _\delta \) does not depend on
up to equivalence.
3 Equational Theories and \(M\)-systems
1-free star expressions denote processes that can be composed nondeterministically using \(+\), and include the constant 0 for the process without outgoing transitions. The axioms involving \(+\) and 0 are precisely those of a join-semilattice with bottom (see Instantiation 1 below). At the same time, the free semilattice with bottom generated by a set \(X\) is \(\mathcal {P}(X)\), the finite powerset of \(X\). This monad also pops up in the transition functions for charts, which are of the form \(X \rightarrow \mathcal {P}( Act \times ( \checkmark + X))\).
This is not a coincidence, and in this section we study the connection more formally. First, we recall equational theories, and touch on a well-known correspondence to free algebra constructions. This leads to an abstracted notion of a chart, parametrized by an equational theory, with its own notion of bisimilarity. The sections that follow develop these ideas to obtain a parametrized axiomatization.
Equational Theories. A signature is a set of operation symbols\(S\) paired with a function \(\textrm{ar}:S\rightarrow \mathbb {N}\). The value \(\textrm{ar}(\sigma )\) is called the arity of \(\sigma \in S\). The set of \(S\)-terms over\(X\), \(S^*X\), is the smallest set of formal expressions containing X, and such that if \(\sigma \in S\) with \(\textrm{ar}(\sigma ) = n\) and \(t_1, \dots , t_n \in S^*X\), then \(\sigma (t_1, \dots , t_n) \in S^*X\).
Given \(t \in S^*X\) and \(\nu :X \rightarrow S^*Y\), we write \(t(\nu )\) to denote the term in \(S^*Y\) obtained by replacing each \(x\) in \(t\) with \(\nu (x)\). We will often write \(t = t(x_1, \dots , x_n)\) for distinct \(x_1, \dots , x_n\) to signal that the variables in \(t\) are among \(x_1, \dots , x_n\), and more compactly \(t(\vec x)\) where \(\vec x = (x_1, \dots , x_n)\). Given \(t = t(\vec x)\) and \(t_1, \dots , t_n \in S^*Y\), we write \(t(t_1, \dots , t_n)\) for the term \(t(\nu )\) where \(\nu :X \rightarrow S^*Y\) is such that \(\nu (x_i) = t_i\).
Fix a set of variables\( Var \) and a signature S. Any relation on \(S^* Var \) can be seen as a set of (formal) equations over S-terms. Given \(S\)-terms \(t, s\) over \( Var \) and a set of equations \(\mathsf E\), we write \(\mathsf E \vdash t = s\) if \(t = s\) can be derived from the equations in \(\mathsf E\) and the laws of equational logic (reflexivity, symmetry, transitivity, substitution, and congruence). An equational theory for S is a set of equations that is closed under the inference rules of equational logic. A set of equations \(\mathsf E\) is an axiomatization of \(\mathsf T\) if \(\mathsf T\) is the smallest equational theory containing \(\mathsf E\). In the future, we abuse terminology and simply refer to \(\mathsf E\) as an equational theory when we are in fact referring to the equational theory it axiomatizes.
An \(S\)-algebra is a pair \((X, \rho )\) consisting of a set \(X\) and for each \(\sigma \in S\) an operation \(\sigma ^\rho :X^{\textrm{ar}(\sigma )} \rightarrow X\). An \(S\)-algebra homomorphism \(h :(X, \rho _X) \rightarrow (Y, \rho _Y)\) is a function \(h :X \rightarrow Y\) such that \(h(\sigma ^{\rho _X}(x_1, \dots , x_n)) = \sigma ^{\rho _Y}(h(x_1), \dots , h(x_n))\).
Given an \(S\)-algebra \((X, \rho )\) and \(t \in S^*X\), we can evaluate \(t\) to \(t^\rho \in X\) by setting \(x^\rho = x\) and \(\sigma (t_1, \dots , t_n)^\rho = \sigma ^\rho (t_1^\rho , \dots , t_n^\rho )\). An \(S\)-algebra \((X, \rho )\)satisfies a set of equations \(E\), written \((X, \rho ) \models E\), if \((t_1, t_2) \in E\) implies \(t_1^\rho = t_2^\rho \).
We can give an equivalent description of \(S\)-algebras using some categorical language. If we write \(\textbf{Set}\) for the category of sets and functions, we can form the signature functor \(\varSigma _S = \bigsqcup _{\sigma \in S} \{\sigma \}\times \textrm{Id}^{\textrm{ar}(\sigma )}\) out of a signature \(S\), where \(\textrm{Id}\) is the identity functor on \(\textbf{Set}\). Then an \(S\)-algebra is the same data as a function \(\rho :\varSigma _S X \rightarrow X\). We usually abuse notation and simply write \(S\) instead of \(\varSigma _S\).
Definition 3.1
Let \(\textsf{T}\) be an equational theory for the signature \(S\). A free-algebra construction for \(\textsf{T}\) is a triple \((M, \eta , \rho )\) consisting of an endofunctor \(M\) on \(\textbf{Set}\) and natural transformations \(\eta :\textrm{Id}\Rightarrow M\) and \(\rho :SM \Rightarrow M\) such that \((MX, \rho _X) \models \textsf{T}\) for all \(X\), satisfying the following: given an \(S\)-algebra \((Y, \mu )\) that satisfies \(\textsf{T}\), and given \(f :X \rightarrow Y\), there is a unique \(S\)-algebra homomorphism \(f^\# :(MX, \rho _X) \rightarrow (Y, \mu )\) such that \(f^\# \circ \eta = f\), called the Kleisli extension of \(f\).
Any two free-algebra constructions for the same equational theory are isomorphic, in the sense that there exist a natural isomorphism between their functors that interacts well with the other structure. Thus, we often refer to a free-algebra construction for \(\textsf{T}\) as the free-algebra construction for \(\textsf{T}\).
Remark 3.2
Free-algebra constructions for equational theories as we have described them have a close relationship with finitary monads on \(\textbf{Set}\). In particular, the free-algebra constructions for an equational theory are in one-to-one correspondence with monads presented by the theory [4], and it is known that a monad is finitary if and only if it has an equational presentation [1].
We will use these instantiations of Definition 3.1 in the rest of the paper.
Instantiation 1
The theory of semilattices (with bottom) is the equational theory \(\textsf{SL}\) for the signature \(S = \{+,0\}\) axiomatized by the following equations:
$$\begin{aligned} x + 0 = x \quad x + x = x \quad x + y = y + x \quad x + (y + z) = (x + y) + z \end{aligned}$$
If we define \(\eta _X(x) = \{x\}\) and \(\rho _X :S\mathcal {P}X \rightarrow \mathcal {P}X \) by \(V_1 +^{\rho _X} V_2 = V_1 \cup V_1\) and \(0^{\rho _X} = \emptyset \), then \((\mathcal {P}, \{-\}, \rho )\) is a free-algebra construction for \(\textsf{SL}\) (keep in mind that we use \(\mathcal {P}\) for the finite powerset). The Kleisli extension of \(f:X \rightarrow Y\) with \((Y, +^\mu , 0^\mu )\) a semilattice is \(f^\#:\mathcal {P}X \rightarrow Y\) defined by \(f^\#(\{ x_1, x_2, \dots , x_n \}) = f(x_1) +^\mu f(x_2) +^\mu \cdots +^\mu f(x_n)\), with the empty sum being \(0^\mu \). The theory of semilattices describes the branching type of 1-free star expressions.
Instantiation 2
Let \(T\) be a finite set of primitive tests and let \( BA \) be the free Boolean algebra on \(T\), i.e., the set of Boolean expressions generated from \(T\) using \(\bot \), \(\wedge \) and \(\lnot \), modulo the axioms of Boolean algebra. The signature S of guarded algebra has a constant \(0\) and a binary operation \(+_b\) for each \(b \in BA \). Its theory \(\textsf{GA}\) is axiomatized by the following equations for all \(b, c \in BA \):
$$\begin{aligned} x +_b x = x \quad x +_b y = y +_{\lnot b} x \quad (x +_b y) +_c z = x +_{b\wedge c} (y +_c z) \end{aligned}$$
Let \( At \) be the set of atomic elements of the Boolean algebra \( BA \) and note that this set is finite. Then the free algebra construction for \(\textsf{GA}\) is the triple \((\mathcal {R}, \eta , \rho )\) where \(\mathcal {R}\) is the reader-with-exception functor\(\mathcal {R}X = (\bot + X)^{ At }\), and for each \(\alpha \in At \), \(\eta _X(x)(\alpha ) = x\), \((\theta _1 +_b^{\rho _X} \theta _2)(\alpha ) = \textbf{if}~\alpha \le b~\textbf{then}~\theta _1(\alpha )~\textbf{else}~\theta _2(\alpha )\), and \(0^{\rho _X}(\alpha ) = \bot \). It is helpful to think of \(x +_b y\) as notation for \(\textbf{if}~b~\textbf{then}~x~\textbf{else}~y\). The theory of guarded algebra captures the branching of skip-free GKAT programs [9].
Instantiation 3
The signature S of (positive) convex algebra consists of one constant symbol \(0\) and a binary operation \(\oplus _p\) for each \(p \in [0,1]\). Its theory \(\textsf{CA}\) is axiomatized by the following equations for all \(p, q \in [0,1]\):
$$\begin{aligned}\begin{gathered} x \oplus _1 y = x \qquad x \oplus _p x = x \qquad x \oplus _p y = y \oplus _{(1 - p)} x \\ (x \oplus _p y) \oplus _q z = x \oplus _{pq} (y \oplus _{(q(1-p)/(1 - pq))}) \quad \text {(if pq < 1)} \end{gathered}\end{aligned}$$
Let \(\mathcal {D}X\) denote the set of finitely supported probability distributions on \(X\), and for each \(x \in X\) define the Dirac delta distribution \(\delta _x(y) = {\textbf {if}}~x = y~{\textbf {then}}~1~{\textbf {else}}~0\). Then the triple \((\mathcal {D}(\bot + (-)), \eta , \rho )\) is a free algebra construction for \(\textsf{CA}\) [32], where \(\eta _X(x) = \delta _x\), \(\theta _1 \oplus _p^{\rho _X} \theta _2 = p\theta _1 + (1-p)\theta _2\), and \(0^{\rho _X} = \delta _\bot \). The theory of convex algebra captures the branching of probabilistic processes [31].
M-systems. Fix an equational theory \(\textsf{T}\) for the signature \(S\) and a free-algebra construction \((M, \eta , \rho )\) for \(\textsf{T}\). At the core of a free-algebra construction \((M, \eta , \rho )\) for \(\textsf{T}\) is its endofunctor \(M\) on \(\textbf{Set}\). By replacing the finite powerset functor \(\mathcal {P}\) in the transition function type for charts \(X \rightarrow \mathcal {P}( Act \times (\checkmark + X))\) with \(M\), we obtain a transition function type for processes whose branching is captured by \(\textsf{T}\).
Definition 3.3
Let \(B_M\) be the endofunctor \(M( Act \times (\checkmark + (-)))\) on \(\textbf{Set}\). Then an \(M\)-system is a pair \((X, \beta )\) consisting of a set of states\(X\) and a transition function\(\beta :X \rightarrow B_M X\). A homomorphism of \(M\)-systems \(h:(X, \beta _X) \rightarrow (Y, \beta _Y)\) is a function \(h :X \rightarrow Y\) such that \(B_M(h) \circ \beta _X = \beta _Y \circ h\).
\(M\)-systems are precisely \(B_M\)-coalgebras, and homomorphisms of \(M\)-systems are precisely \(B_M\)-coalgebra homomorphisms. This unlocks many useful results from coalgebra [23]. In particular, \(M\)-systems and their homomorphisms form a category, which we will call \(\operatorname {Coalg}(B_M)\). The theory of coalgebras also prescribes a general notion of bisimilarity, which instantiates to Definition 2.2 via Lemma 2.4.
Definition 3.4
Let \((X, \beta _X)\) and \((Y, \beta _Y)\) be \(M\)-systems. We call \(x \in X\) and \(y \in Y\)bisimilar (written
) if there is an \(M\)-system \((Z, \beta _Z)\) and homomorphisms \(h :(X, \beta _X) \rightarrow (Z, \beta _Z)\) and \(k :(Y, \beta _Y) \rightarrow (Z, \beta _Z)\) such that \(h(x) = k(y)\).
A standard argument tells us that bisimilarity is an equivalence relation [7].
4 Skip-free Star Expressions
Grabmayer and Fokkink introduced 1-free star expressions as a specification language for processes with non-deterministic branching behaviour captured by charts. As we saw, charts coincide with \(\mathcal {P}\)-systems. Moreover, the algebraic signature of the theory of semilattices — for which \(\mathcal {P}\) provides the free algebra construction — suggests a syntax for behaviour expressed by well-layered charts, as well some axioms. In this section, we expand on these ideas, using equational theories and free algebra constructions to develop a syntax for M-systems, as well as a candidate set of axioms for equivalence expressed in this syntax.
For the remainder of this section, we fix an equational theory \(\textsf{T}\) for the signature \(S\), which admits a free algebra construction \((M, \eta , \rho )\).
Definition 4.1
The skip-free unified-star expressions\( Exp \) are generated by
In the above, \(\sigma \in S\) with \(\textrm{ar}(\sigma ) = n\) and \(s = s(u, v)\) is an \(S\)-term in two variables.
The small-step semantics of skip-free star expressions is captured by giving \( Exp \) the structure of an \(M\)-system. This automatically equips these expressions with a notion of equivalence, namely bisimilarity as states in this system. We call the \(M\)-system \(( Exp , \gamma )\), defined recursively in Fig. 3, the syntactic\(M\)-system.
Note that we use the following shorthands from now on: \((\vec a, \vec e)\) denotes the list of tuples \((a_1, x_1), \dots , (a_n, x_n)\); \(\vec b \vec e\) denotes the list \(b_1e_1, \dots , b_n e_n\); \(\vec e f\) denotes the list \(e_1f,\dots ,e_n f\); and generally, where \(h\) is a function defined on the set \(\{x_1, \dots , x_n\}\), \(h(\vec x)\) denotes the list \(h(x_1), \dots , h(x_n)\).
Fig. 3.
The definition of \(( Exp , \gamma )\) w.r.t. the free-algebra construction \((M, \eta , \rho )\). Above, \(e_i \in Exp \), \(a \in Act \), and \(s = s(u,v) \in S^* Var \). In the formulas for \(e_1e_2\) and \(e_1^{(s)}e_2\) above, \(\gamma (e_1) = t^\rho = t^\rho ((\vec b, \checkmark ), (\vec a, \vec f))\). In the last formula, we have used
to indicate the portion of the formula that corresponds to the \(s\) in \(e_1^{(s)}e_2\).
Intuitively, the skip-free star expressions of the form \(a \in Act \) and \(e_1 \cdot e_2\) have the usual interpretation: \(a\) is the process that emits \(a\) and accepts, and \(e_1 \cdot e_2\) is the sequential composition of \(e_1\) and \(e_2\). As before, we usually write \(e_1e_2\) instead of \(e_1\cdot e_2\). The expression \(\sigma (e_1, \dots , e_n)\) denotes the process that branches into \(e_1, \dots , e_n\) and whose outgoing transitions carry the structure defined by \(\sigma \).
Example 4.2
Let \(\textsf{T}= \textsf{SL}\) be the theory of join-semilattices with bottom discussed in Instantiation 1. The free-algebra construction \((M, \eta , \rho )\) for \(\textsf{T}\) is \((\mathcal {P}, \{{-}\}, \rho )\), and the behaviour of \(( Exp , \gamma )\) corresponds closely to that of \(( StExp , \delta )\) (cf. Figure 1).
For instance, \(\gamma (a) = \eta (a, \checkmark ) = \{ (a, \checkmark ) \}\), and similarly \(\gamma (b) = \{ (b, \checkmark ) \}\). This matches the transitions of \(a, b \in StExp \) as prescribed by \(\delta \). Furthermore, \(\gamma (a + b) = \gamma (a) +^\rho \gamma (b) = \gamma (a) \cup \gamma (b) = \{ (a, \checkmark ), (b, \checkmark ) \}\), which matches \(\delta (a+b)\).
If we look at \((a + b)c \in Exp \), then Figure 3 tells us that because \(\gamma (a + b) = \eta (a, \checkmark ) +^\rho \eta (b, \checkmark )\), we have \(\gamma ((a + b)c) = \eta (a, c) +^\rho \eta (b, c) = \{ (a, c), (b, c) \}\); this also corresponds to the transitions exiting \((a + b)c \in StExp \) as specified by \(\delta \).
The process denoted \(e_1^{(s)}e_2\), given by the \(s\)-star of \(e_1\) and \(e_2\), is a bit more complicated: it represents the process that loops on the branches of \(e_1\) wherever the variable \(u\) appears in \(s(u, v)\), and otherwise moves on to the branches of \(e_2\) wherever the variable \(v\) appears. In the future, if \(s(u, v) = \sigma (u, v)\) for some binary operation \(\sigma \in S\), we will write \(e_1^{(\sigma )}e_2\) in place of \(e_1^{(\sigma (u, v))}e_2\).
Example 4.3
Let M, \(\textsf{T}\) and the free-algebra construction be as in the previous example. We can recover the behaviour of the binary star operator from 1-free regular expressions as a particular instance of skip-free unified-star expressions.
For example, if we look at \((a + b) * c\), then Figure 1 tells us that
$$ \gamma (a * b) = \{ (a, (a+b)*c), (b, (a+b)*c), (c, \checkmark ) \} $$
At the same time, if we consider \(a^{(+)}b\), then Figure 3 tells us that because \(\gamma (a + b) = \eta (a, \checkmark ) +^\rho \eta (b, \checkmark )\), we have that
In fact, the above can be used to show that \((a+b)*c\) as a state in \(( StExp , \delta )\) is bisimilar to \((a+b)^{(+)}c\) as a state in \(( Exp , \gamma )\).
Up to equivalence, there are three more choices for \(s = s(u, v)\) in \(e_1^{(s)}e_2\), namely the variables u and v, and the constant 0. The behaviours obtained by these expressions can still be modelled by 1-free regular expressions: \(a^{(u)}b\) corresponds to \(a * 0\), \(a^{(v)}b\) corresponds to \(0 * a\), and \(a^{(0)}b\) is simply 0.
Given \(M\)-systems \((U, \beta _U)\) and \((X, \beta )\), \((U, \beta _U)\) is a subsystem of \((X, \beta )\) if \(U \subseteq X\) and the inclusion map \((U, \beta _U) \hookrightarrow (X, \beta )\) is a homomorphism of \(M\)-systems. The syntactic M-system has a finite subsystem for each expression.
Proposition 4.4
For each \(e \in Exp \), there is a smallest finite subsystem \(\langle e \rangle \) of \(( Exp , \gamma )\) containing \(e\), called the subsystem generated by\(e\).
Fig. 4.
The theory \(\textsf{T}^*\) that axiomatizes bisimilarity of star expressions. Above, \(e_1,\dots ,e_n \in Exp \), \(e,f,g \in Exp \), \(t = t(\vec v) \in S^* Var \), and \(s(u, v) \in S^* Var \) is a binary term with free variables \(u, v\). Recall that the notation \(\vec e f\) means \(e_1f, \dots , e_n f\).
We now present a set of axioms that aims to capture bisimilarity in \(( Exp , \gamma )\).
Definition 4.5
The skip-free unified-star theory\(\textsf{T}^*\) consists of the axioms in Fig. 4 and the laws of equational logic. We write \(\textsf{T}^* \vdash e_1 = e_2\) if \(e_1 = e_2\) is derivable from \(\textsf{T}^*\) and say that \(e_1\) and \(e_2\) are provably equivalent.
Intuitively, the first inference rule in Fig. 4 says that two terms that are equivalent up to \(\textsf{T}\) are equivalent as branching structures. The rules (A) and (D) express standard properties of sequential composition: associativity and right distributivity over branches. The rules (U) and (RSP) state that \(e_1^{(s)}e_2\) is the unique process z that satisfies the recursion equation \(z = s(e_1z, e_2)\).
Theorem 4.6
(Soundness). Let \(e_1, e_2 \in Exp \). If \(\textsf{T}^* \vdash e_1 = e_2\), then
.
Even working with an arbitrary equational theory, a number of interesting equivalences can be proven using the axioms of \(\textsf{T}^*\). For example, \(\textsf{T}^* \vdash e_1^{(s)}(e_2e_3) = (e_1^{(s)}e_2)e_3\) is a consequence of (A), (D), (U), and (RSP). Also, if \(\textsf{T}\vdash s_1 = s_2\), then \(\textsf{T}^* \vdash e_1^{(s_1)}e_2 = e_1^{(s_2)}e_2\), which is a consequence of (\(\textsf{T}\)), (U), and (RSP).
In Examples 4.2 and 4.3, we have already seen that for \(\textsf{SL}\), we recover a system that corresponds to 1-free star expressions. For \(\textsf{GA}\) and \(\textsf{CA}\), we are in a similar situation: every \(s\)-star operation \(e_1^{(s)}e_2\) is equivalent (up to the unified-star axioms) to a binary star, i.e., either \(e_1^{(+_b)}e_2\) or \(e_1^{(\oplus _p)}e_2\) respectively. These correspond precisely to the binary stars in the syntax for skip-free GKAT [9] and in the probabilistic regular expressions in [22]. Thus, our parametrized class of skip-free process algebras does indeed capture both skip-free GKAT and the algebra of skip-free probabilistic regular expressions (modulo bisimilarity).
5 Completeness
We are now ready to start proving the completeness of \(\textsf{T}^*\) w.r.t. bisimilarity in \(( Exp , \gamma )\), at least for a large class of equational theories \(\textsf{T}\). We follow the same steps as Grabmayer and Fokkink, adapting and generalizing each step to other equational theories. Specifically, we will construct a class \(\mathcal C\) of \(M\)-systems that satisfies analogues of (Expressivity), (Closure) and (Solvability).
Note that we are not able to prove completeness of \(\textsf{T}^*\) for arbitrary \(\textsf{T}\). We will discuss which equational theories we have to restrict our attention to later in this section. We delay the restriction for now because the first few results presented below are true for arbitrary equational theories.
Solutions to M-systems. The completeness proof to follow casts \(M\)-systems as systems of equations of a certain form. For a given \(M\)-system \((X, \beta )\), we associate each state \(x \in X\) with an equation \(x = t(\vec b, \vec a \vec x)\) with unknowns \(x_1, \dots , x_n\), where \(t \in S^*X\) and \(\beta (x) = t^\rho ((\vec b, \checkmark ), (\vec a, \vec x))\).
Definition 5.1
A solution to an \(M\)-system \((X, \beta )\) is a map \(\phi :X \rightarrow Exp \) such that for any \(x \in X\) with \(\beta (x) = t^\rho ((\vec b, \checkmark ), (\vec a, \vec x))\), \(\textsf{T}^* \vdash \phi (x) = t(\vec b, \vec a\phi (\vec x))\). Two solutions \(\phi ,\psi \) are equivalent if \(\textsf{T}^*\vdash \phi (x) = \psi (x)\) for all \(x \in X\). The \(M\)-system \((X, \beta )\)admits a unique solution if it has exactly one solution up to equivalence.
Note that the specific choice of \(t\) in Definition 5.1 does not change the space of solutions to \((X, \beta )\). The following result is analogous to Proposition 2.9.
Proposition 5.2
There is a unique \(M\)-system structure \(( Exp /{\equiv }, [\gamma ]_\equiv )\) such that the quotient map \([-]_\equiv :( Exp , \gamma ) \rightarrow ( Exp /{\equiv }, [\gamma ]_\equiv )\) is a homomorphism of \(M\)-systems. Moreover, for any \(M\)-system \((X, \beta )\), a map \(\phi :X \rightarrow Exp \) is a solution if and only if \([-]_\equiv \circ \phi :(X, \beta ) \rightarrow ( Exp /{\equiv }, [\gamma ]_\equiv )\) is a homomorphism of \(M\)-systems.
As before, Proposition 5.2 has the following immediate consequences.
Proposition 5.3
Let \(h :(X, \beta _X) \rightarrow (Y, \beta _Y)\) be a homomorphism of \(M\)-systems, and let \(\phi :Y \rightarrow Exp \) be a solution to \((Y, \beta _Y)\). Then \(\phi \circ h\) is a solution to \((X, \beta _X)\). Furthermore, for any \(e \in Exp \), the inclusion map \(\langle e\rangle \hookrightarrow Exp \) is a solution to \(\langle e\rangle \).
We would now like to reuse Theorem 2.13, which says that well-layered charts are closed under homomorphic images, and Definition 2.14, which computes the canonical solution to a well-layered chart. To do this, we need to restrict \(\textsf{T}\).
Support. We start by generalizing the notion of well-layeredness. Here, the idea is that we need a way to talk about how the states of an M-system are connected. This is encapsulated by the notion of support, defined below.
Definition 5.4
A support for \(\textsf{T}\) is a natural transformation \(\textsf{supp}:M \Rightarrow \mathcal {P}\) s.t. (1) \(\textsf{supp}\circ \eta = \{-\}\) and (2) for \(\sigma \in S\) and \(t_1, \dots , t_n \in S^*X\), \(\textsf{supp}(\sigma ^{\rho }(t_1^{\rho }, \dots , t_n^{\rho })) \subseteq \textsf{supp}(t_1^{\rho }) \cup \dots \cup \textsf{supp}(t_n^{\rho })\). \(\textsf{T}\) is supported if a support for \(\textsf{T}\) exists.
Intuitively, an equational theory is supported if every term has a well-defined set of “essential variables” up to provable equivalence. For example, in the theory of semilattices \(\textsf{SL}\), the set of essential variables of a term \(x_1 + \cdots + x_n\) is precisely \(\{x_1, \dots , x_n\}\) — i.e., the support is the identity transformation on \(\mathcal {P}\). For guarded algebra (\(\textsf{GA}\)), the support takes a function \(\theta : At \rightarrow \bot + X\) to its image without \(\bot \), \(\textsf{supp}(\theta ) = \theta ( At )\setminus \{\bot \}\). For convex algebra, the support of \(\theta \in \mathcal {D}(\bot + X)\) is its support as a subprobability distribution, \(\textsf{supp}(\theta ) = \{ x \in X \mid \theta (x) > 0\}\).
Not every equational theory is supported. For a trivial nonexample, the theory axiomatized by \(\mathsf E = \{(u, v)\}\) identifies all terms and has the constant functor \(M = \{\star \}\) and \(\eta _X(x) = \star \) in its free-algebra construction. The only natural transformation \(\lambda :M \Rightarrow \mathcal {P}\) maps \(\star \) to \(\emptyset \), which does not satisfy \(\lambda \circ \eta = \{-\}\).
Remark 5.5
The existence of a support does not depend on the choice of \((M, \eta , \rho )\), since all free-algebra constructions for \(\textsf{T}\) are isomorphic. So, if one \((M,\eta ,\rho )\) has a support, then all do. However, more than one support may exist.
In an \(M\)-system corresponding to a supported equational theory, branching is essentially given by transitions, in the sense of charts, with extra structure. The underlying chart of an \(M\)-system is the chart obtained by forgetting this structure. This extends the notion of well-layered charts to \(M\)-systems.
Definition 5.6
Let \(\textsf{supp}\) be a support for \(\textsf{T}\). The underlying chart of an \(M\)-system \((X, \beta )\) is the chart \(\textsf{supp}_*(X, \beta ) = (X, \textsf{supp}_X \circ \beta )\). An \(M\)-system is called well-layered if its underlying chart is well-layered.
For the remainder of this section, we shall assume that \(\textsf{T}\) is supported. In an \(M\)-system \((X, \beta )\), write
if
in its underlying chart, and \(x \rightarrow _\beta y\) if
for some a. By Definition 5.6, a well-layered \(M\)-system \((X, \beta )\) admits an entry/body labelling
,
of \(\textsf{supp}_*(X, \beta )\) that satisfies Definition 2.11. We can then write \(x \curvearrowright y\) for states \(x,y \in X\) if \(x \curvearrowright y\) in this entry/body labelling, and furthermore define \(|{x}|_{en}\) and \(|{x}|_{bo}\) as in Definition 2.14 for \(x \in X\).
With this candidate class of M-systems, we can recover (Expressivity).
Proposition 5.7
Let \(\textsf{supp}\) be a support for \(\textsf{T}\). Then \(( Exp , \gamma )\) is well-layered. Consequently, for any \(e \in Exp \), the \(M\)-system \(\langle e \rangle \) generated by \(e\) is well-layered.
Recall that M-systems are just \(B_M\)-coalgebras. The transformation of \(M\)-systems, being a natural transformation, defines a functor \(\textsf{supp}_* :\operatorname {Coalg}(B_M) \rightarrow \operatorname {Coalg}(B_\mathcal {P})\) that has some nice properties [23]. The following is true for general \(F\)-coalgebras for an endofunctor on \(\textbf{Set}\), and so we state it in full generality.
Lemma 5.8
Let \(F\) and \(G\) be endofunctors on \(\textbf{Set}\) and let \(\lambda :F \Rightarrow G\) be a natural transformation. Define \(\lambda _* :\operatorname {Coalg}(F) \rightarrow \operatorname {Coalg}(G)\) to be the functor with \(\lambda _*(X, \beta ) = (X, \lambda _X \circ \beta )\) and \(\lambda _*(h) = h\) for any coalgebra homomorphism \(h\). Let \(\mathcal C\) be a class of \(G\)-coalgebras that is closed under homomorphic images. Then \(\lambda ^{-1}\mathcal C = \{(X, \beta ) \mid \lambda _*(X, \beta ) \in \mathcal C\}\) is also closed under homomorphic images.
In our situation, \(F = B_M\), \(G = B_\mathcal {P}\), and \(\lambda = \textsf{supp}_*\). As we have defined it, the class of well-layered \(M\)-systems is precisely the inverse image of \(\textsf{supp}_*\). From Theorem 2.13 and 5.8, we immediately obtain a version of (Closure):
Theorem 5.9
Well-layered \(M\)-systems are closed under homomorphic images.
Malleability. The point of well-layered systems is that we can solve them uniquely. To this end, we want to replay the strategy from Definition 2.14. The following notion helps to do that, by letting us isolate variables into a subterm.
Definition 5.10
We say that \(\textsf{T}\) is malleable if for any set \(X\), any partition \(U + V = X\), and any term \(t \in S^*X\), there are terms \(t_1 \in S^*U\), \(t_2 \in S^*V\), and a term \(s = s(u, v) \in S^* Var \) such that \(\textsf{T}\vdash t = s(t_1, t_2)\).
Example 5.11
In the case of \(\textsf{GA}\), if \(t = x +_b (y +_c z)\) and \(U = \{x, y\}\) while \(V = \{ z\}\), then we can choose \(s = u +_{b \vee c} v\), \(t_1 = x +_b y\) and \(t_2 = z\) to find that \(\textsf{T}\vdash t = s(t_1, t_2)\). More generally, due to the associativity and commutativity properties of \(\textsf{SL}\), \(\textsf{GA}\), and \(\textsf{CA}\), all three of these equational theories are malleable.3
Remark 5.12
Not all equational theories are malleable. For a trivial example, consider the theory \(\textsf{T}= \emptyset \) for a signature with two binary operations \(\star ,\bullet \). Clearly, the term \(x \star (y \bullet z)\) is not of the form \(s(t_1(x, y), t_2(z))\) for any terms \(t_1, t_2, s\). In Section 6, we will also see an example of a richer equational theory, which captures branching that mixes nondeterminism and probability, that is not malleable.
For the rest of this section, we assume that \(\textsf{T}\) is malleable. We can now use this to recover the solution strategy for well-layered charts in Definition 2.14.
Definition 5.13
Let
be a well-layered entry/body labelling of \((X, \beta )\). We define the canonical solution to \((X, \beta )\)given by
as follows. Let
where \(\vec {x}\) is a vector such that \(x \ne x_i\) and
for each \(i\), and \(\vec {y}\) is a vector such that
for each \(j\). By induction on \(|x|_{bo} \in \mathbb N\), we define
where, by induction on \((|x|_{en}, |y|_{bo})\) in the lexicographical ordering of \(\mathbb {N}\times \mathbb {N}\), for each pair of states such that \(x \curvearrowright y\) we define \(\tau _\beta (y, x)\) as follows. First, let
where \(\vec {x}\) is a vector such that \(y \ne x_i\) and
for each \(i\), and \(\vec {y}\) is a vector such that \(x \ne y_k\) and
for each \(k\). Then
In the above, we assumed that \(\beta (x)\) and \(\beta (y)\) were in a specific form. This is where malleability comes in: we partitioned the support of \(\beta (x)\) into pairs that correspond to self loops
or loop entry transitions
, and those that come from body transitions
or accepting transitions \(x \rightarrow \checkmark \). Malleability assures us that we can write \(\beta (x)\) as described, and similarly for \(\beta (y)\).
Unravelling the definitions in the case of \(\textsf{SL}^*\), one obtains the canonical solution formula in Definition 2.14, which appeared in [6]. In this case also, \(\phi _\beta \) is the unique solution to a well-layered \(M\)-system, so we recover (Solvability).
Proposition 5.14
Let \((X, \beta )\) be a well-layered \(M\)-system, with entry/body labeling
. Then the canonical solution \(\phi _\beta \) given by
is the unique solution to \((X, \beta )\). In particular, up to \(\textsf{T}^*\), \(\phi _\beta \) does not depend on
.
Completeness. Following the same steps in the first completeness proof we saw (of Theorem 2.6) with \(\mathcal C\) the class of well-layered \(M\)-systems (and replacing the word “chart” with “\(M\)-system” everywhere), we can apply Propositions 2.12 and 5.14 and 5.9 to obtain the main result of the paper.
Theorem 5.15
(Completeness). Let \(\textsf{T}\) be a supported malleable theory for the signature \(S\). Given \(e_1, e_2 \in Exp \), if
, then \(\textsf{T}^* \vdash e_1 = e_2\).
6 Examples and Nonexamples
As we have hinted at, the theory of semilattices \(\textsf{SL}\), guarded algebra \(\textsf{GA}\), and convex algebra \(\textsf{CA}\) are supported and malleable, and therefore fit our framework. But, as we have already seen, some equational theories do not admit support, and others are not malleable. In this section, we discuss the scope of our story.
The following result gives a sufficient condition for malleability.
Proposition 6.1
Let \(\textsf{T}\) be an equational theory for a signature \(S\) consisting of constants and binary operations. \(\textsf{T}\) is malleable if both of the following hold:
1.
Skew commutativity. For any binary operation \(\sigma \in S\), there is a binary operation \(\tau \in S\) such that \(\textsf{T}\vdash \sigma (x, y) = \tau (y, x)\).
2.
Skew associativity. For any binary operations \(\sigma _1,\sigma _2 \in S\), there are binary operations \(\tau _1,\tau _2 \in S\) such that \(\textsf{T}\vdash \sigma _1(x, \sigma _2(y, z)) = \tau _1(\tau _2(x, y), z)\).
It is immediate from the axioms of \(\textsf{SL}\), \(\textsf{GA}\), and \(\textsf{CA}\) that all three satisfy these properties. However, some malleable theories are not skew-associative.
Instantiation 4
The theory of guarded convex algebra\(\textsf{GC}\) consists of one constant symbol \(0\), one binary operation \(+_b\) for each Boolean expression \(b \in BA \) (see Inst. 2), one binary operation \(\oplus _p\) for each \(p \in [0,1]\), and is axiomatized by the equations of \(\textsf{GA}\), \(\textsf{CA}\), and the distribution law\(x \oplus _p (y +_b z) = (x \oplus _p y ) +_b (x \oplus _p z)\). Its free-algebra construction is given by \((\mathcal {D}(\bot + (-))^ At , \eta , \rho )\) where \(\eta _X(x)(\alpha ) = \delta _x\); \((\chi _1 +_b^\rho \chi _2)(\alpha )(x) = \chi _1(\alpha )(x)\) if \(\alpha \le b\), and \((\chi _1 +_b^\rho \chi _2)(\alpha )(x) = \chi _2(\alpha )(x)\) otherwise; \((\chi _1 \oplus _p^\rho \chi _2)(\alpha )(x) = p\chi _1(\alpha )(x) + (1-p)\chi _2(\alpha )(x)\), and \(0^\rho (\alpha ) = \delta _\bot \).
Guarded convex algebra is a supported malleable theory that is not skew associative. Indeed, we can take \(\textsf{supp}:\mathcal {D}(\bot + (-))^ At \Rightarrow \mathcal {P}\) to be \(\textsf{supp}_X(\chi ) = \bigcup _{\alpha \in At }\{x \in X \mid \chi (\alpha )(x) > 0\}\). It is not difficult to show that this is a natural transformation that satisfies the requirements of a support. To see why \(\textsf{GC}\) is not skew-associative, consider the term \(x +_{0.5} (y +_b z)\). A simple case analysis reveals that it is not equivalent to \(\tau _1(\tau _2(x, y), z)\) for any binary operations \(\tau _1\) and \(\tau _2\).
We illustrate the proof that \(\textsf{GC}\) is malleable in the special case of \(X = \{x, y, z\}\) and \( At = \{\alpha _1, \alpha _2\}\). Consider \(\chi = \theta _1 +_{\alpha _1} \theta _2\) for some probability distributions \(\theta _1,\theta _2\) on \(X\). The convex algebra \(\mathcal {D}(\bot + X)\) can be visualized as the \(3\)-simplex in \(\mathbb R^4\) [30] with extremal points \(\delta _x, \delta _y, \delta _z, \delta _\bot \). We only need one of its faces, the convex hull of \(\delta _x, \delta _y, \delta _z\), depicted in (5). There, \(\chi \) represents two points, one for each of \(\alpha _1,\alpha _2\). To obtain terms \(s(u, v)\), \(t_1(x, y)\) and \(t_2(z)\) such that \(\chi = s^\rho (t_1^\rho , t_2^\rho )\), draw straight lines from \(\delta _z\) through \(\theta _1\) to the segment between \(\delta _x\) and \(\delta _y\).
The endpoints of the drawn lines represent distributions obtained from terms of the form \(r_1(x,y),r_2(x,y)\), i.e., \(\theta _1' = r_1^\rho (x, y)\) and \(\theta _2' = r_2^\rho (x, y)\). Then \(\chi = (\theta _1' \oplus _p \delta _z) +_{\alpha _1} (\theta _2' \oplus _q \delta _z)\) for some \(p,q \in [0,1]\). If we choose \(s(u, v) = (u \oplus _p v) +_{\alpha _1} (u \oplus _q v)\), \(t_1(x, y) = r_1(x, y) +_{\alpha _1} r_2(x, y)\) and \(t_2 = z\), then \(\chi = s^\rho (t_1^\rho , t_2^\rho )\).
Guarded convex algebra is the equational theory \(\textsf{GC}\) underlying the recently introduced probabilistic guarded Kleene algebra with tests (or ProbGKAT) [21, 25]. However, the skip-free universal-star fragment of \(\textsf{GC}\) is not the obvious skip-free fragment of ProbGKAT, because the latter allows only the binary stars \(e_1^{(s)}e_2\) for \(s(u, v) = u +_b v\) and \(s = u \oplus _p v\). In contrast, skip-free unified-star expressions for \(\textsf{GC}\) allow mixed loops, like \(e_1^{(s)}e_2\) with \(s = u \oplus _p (u +_b v)\), which enters the loop body with probability p, and with probability \(1-p\) does this iff b is true.
Instantiation 5
A (unital) semiring is a set \(\mathbb {S}\) equipped with two constants \(0\) and \(1\) and two binary operations \(+\) and \(\times \) (written as juxtaposition) such that \((\mathbb {S}, +, 0)\) is a commutative monoid, \((\mathbb {S}, \times , 1)\) is a monoid, and the distributive laws \(p (q + r) = p q + p r\) and \((p + q) r = pr + qr\) hold. The theory \(\mathbb {S}{\textsf{Mod}}\) of semimodules over a semiring \(\mathbb {S}\) has a signature consisting of a constant \(0\), a binary operation \(\oplus \), and a unary operation \(p \cdot (-)\) for each \(p \in \mathbb {S}\). The axioms of \(\mathbb {S}{\textsf{Mod}}\) state that \(\oplus \) is commutative, associative, and has \(0\) as a neutral element (the commutative monoid axioms), as well as \(0 \cdot x = 0\), \(1 \cdot x = x\), \(p \cdot (q \cdot x) = (pq) \cdot x\), \(p\cdot (x \oplus y) = (p\cdot x) \oplus (p \cdot y)\), and \((p + q) \cdot x = (p \cdot x) \oplus (q \cdot x)\), for any \(p,q \in \mathbb {S}\).
Given a function \(\theta :X \rightarrow \mathbb {S}\), define \(\textsf{supp}_X(\theta ) = \{x \in X \mid \theta (x) \ne 0\}\). The free algebra construction for \(\mathbb {S}{\textsf{Mod}}\) is given by \((\mathcal O_\mathbb {S}, \eta , \rho )\), where \(\mathcal O_\mathbb {S}X = \{\theta :X \rightarrow \mathbb {S}\mid \textsf{supp}_X(\theta )\text { is finite}\}\); \(\eta (x)(y) = {\textbf {if x = y then 1 else 0}}\); and where \( 0^\rho (x) = 0 \), \( (\theta _1 \oplus ^\rho \theta _2)(x) = \theta _1(x) + \theta _2(x) \), and \( (p \cdot ^\rho \theta )(x) = p\theta (x) \). An \(\mathcal O_\mathbb {S}\)-system is essentially a weighted transition system with weights that live in \(\mathbb {S}\).
The theory \(\mathbb {S}{\textsf{Mod}}\) is supported malleable: \(\textsf{supp}_X(\theta )\) is finite for each \(\theta \in \mathcal O_\mathbb {S}X\) by definition, so we obtain a natural transformation \(\textsf{supp}:\mathcal O_\mathbb {S}\Rightarrow \mathcal {P}\) that clearly satisfies the requirements of a support for \(\mathbb {S}{\textsf{Mod}}\). To see malleability, observe that up to \(\mathbb {S}{\textsf{Mod}}\), every term \(t(\vec x, \vec y)\) with disjoint \(\vec x,\vec y\) is equivalent to one of the form \([(p_1 \cdot x_1) \oplus \cdots \oplus (p_n \cdot x_n)] \oplus [(q_1 \cdot y_1) \oplus \cdots \oplus (q_m \cdot y_m)]\) for some \(p_i,q_j\in \mathbb {S}\).
An Unfortunate Nonexample. Several authors have taken an interest in mixing nondeterminism with probability [4, 10, 14, 16, 34]. A natural choice for the underlying equational theory in this case is the theory of convex semilattices\(\textsf{CS}\) [4], which consists of \(\textsf{SL}\), \(\textsf{CA}\) and the distributive law \(x \oplus _p (y + z) = (x \oplus _p y) + (x \oplus _p z)\). The free-algebra construction for \(\textsf{CS}\) is \((\mathcal C, \eta , \rho )\) where \(\mathcal CX\) is the set of convex subsets of \(\mathcal {D}(\bot + (-))\) that include \(\delta _\bot \), \(\eta _X(x) = \{p\delta _x + (1-p)\delta _\bot \mid p \in [0,1]\}\), \(0^{\rho _X} = \{\delta _\bot \}\), \(U \oplus _p^{\rho _X} V = \{p\theta _1 + (1-p)\theta _2 \mid \theta _1 \in U,\theta _2 \in V\}\), and \(U +^{\rho _X} V = \operatorname {conv}(U \cup V)\) is the convex hull of \(U \cup V\) [4] (see also [25, Example 4.1.14]).
The theory of convex semilattices admits the obvious support but, despite the similarity to \(\textsf{GC}\), it is not malleable. Indeed, there are no terms \(s(u, v)\), \(t_1(x, y)\), and \(t_2(z)\) such that \(\textsf{CS}\vdash s(t_1(x, y), t_2(z)) = x + (y \oplus _{\frac{1}{2}} z)\). To see why, recall that the space of probability distributions on \(X = \{x,y,z\}\) can be identified with a face of the \(3\)-simplex, depicted as a black triangle in (6).
The line down the middle of the left triangle in (6) is the convex set of probability distributions that corresponds to the term \(x + (y \oplus _{\frac{1}{2}} z)\) (cf. [17, Fig. 1]). The highlighted region in the center of the right triangle is the general shape that any convex set of the form \(s(t_1(x, y), t_2(z))\) must take. No convex set of this form is equal to the line segment in (6). Thus, \(\textsf{CS}\) is not malleable.
On the other hand, the theory of convex semilattices still obtains a syntax of skip-free unified-star expressions, a bisimilarity semantics, and a sound set of axioms \(\textsf{CS}^*\) from the framework presented in the paper. So, we ask: is \(\textsf{CS}^*\) complete with respect to bisimilarity of skip-free unified-star expressions?
7 Discussion and Future Work
Given a supported and malleable equational theory \(\textsf{T}\), we can derive a notion of bisimilarity and a complete axiomatization for “skip-free” processes with \(\textsf{T}\)-branching. This framework recovers existing completeness theorems for \(\textsf{SL}^*\) (the result by Grabmayer and Fokkink [6]) and \(\textsf{GA}^*\) (skip-free GKAT up to bisimilarity [9]), and yields new ones for \(\textsf{CA}^*\) (1-free probabilistic regular expressions up to bisimilarity [22]) and \(\textsf{GC}^*\) (a slightly generalized skip-free ProbGKAT [21]).
We would like our framework to abstract the completeness theorem of regular expressions up to bisimilarity [5]. This could settle the open completeness problem for full GKAT up to bisimilarity [26], and possibly its trace semantics [29].
The theories we consider all contain a constant 0, which stands for the deadlocked process, which does not allow any branching and satisfies \(0e = 0\). It would be interesting to see what would be necessary to guarantee that \(e0 = 0\). This would make 0 act like the “predictable failure” studied by Baeten and Bergstra in [3]. Earlier work in the setting of GKAT has shown that completeness for this extended system can be derived from the original [9, 26].
Unified star-expressions give a middle ground between a Kleene-star and general recursion, by focusing on loops that derive from \(\textsf{T}\). We would also like to investigate the hierarchy of expressiveness of star-expressions for n-ary operators. Perhaps such an extension would help to get a completeness theorem for \(\textsf{CS}^*\).
A natural question to ask is which equational theories are supported malleable. For example, all of our examples are skew commutative (in the sense of Proposition 6.1), but it is currently not clear if this is a necessary condition. Also, conspicuously, the distributive law in \(\textsf{GC}\) allowed us to mix \(\textsf{GA}\) with \(\textsf{CA}\) to produce a malleable theory, while the distributive law in \(\textsf{CS}\) did not. We would like know if this is related to the existence of a distributive law of monads \(\mathcal {D}\mathcal {R}\Rightarrow \mathcal {R}\mathcal {D}\) and the lack of a distributive law \(\mathcal {D}\mathcal {P}\Rightarrow \mathcal {P}\mathcal {D}\) [34], or at least to the composite theories of [17] that guarantee the existence of a distributive law.
Finally, because bisimilarity coincides with provable equivalence for the equational theories satisfying our constraints, it is also a congruence. We wonder whether this implies the existence of a distributive law à la Turi and Plotkin [33].
Acknowledgements
T. Kappé was partially supported by the European Union’s Horizon 2020 research and innovation programme under grant no. 101027412 (VERLAN), and partially by the Dutch research council (NWO) under grant no. VI.Veni.232.286 (ChEOpS).
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
The syntax and significance of this fragment of KAT was already noticed by Kozen and Tseng in [13]. The innovations of [29] are the axiomatization and complexity results, as well as a number of different interpretations of GKAT.
These are not necessary conditions for malleability, though. In Section 6, we will see an example of a malleable equational theory that does not enjoy associativity.
if \((a, y) \in \delta (x)\), and
if \((a, \checkmark ) \in \delta (x)\).
, one for each \(a \in Act \). We usually drop subscripts if the transition function can be inferred from context. We write \({\rightarrow }\) for the union of the transition relations and say that \(x\) transitions to \(y\) if \(x \rightarrow y\).
if and only if
, (2) if
, then there is a \((x',y') \in R\) such that
, and (3) if
, then there is a \((x',y') \in R\) such that
. We write
and say that \(x\) and \(y\) are bisimilar if \((x, y) \in R\) for some bisimulation \(R\).
is the largest bisimulation between two charts. Furthermore,
is an equivalence relation when restricted to a single chart. Another notion that we will rely on is that of a chart homomorphism.
if and only if there is a third chart \((Z, \delta _Z)\) and chart homomorphisms \(h :(X, \delta _X) \rightarrow (Z, \delta _Z)\) and \(k :(X, \delta _X) \rightarrow (Z, \delta _Z)\) such that \(h(x) = k(y)\).
as states of \(( StExp , \delta )\) iff they are bisimilar as states of \(\langle r \rangle \) and \(\langle s\rangle \) respectively.
as states in \(( StExp , \delta )\).
. Two solutions \(\phi ,\psi \) are equivalent if for any \(x \in X\), \(\textsf{SL}^* \vdash \phi (x) = \psi (x)\). A chart \((X, \delta )\) is said to have a unique solution if it has exactly one solution up to equivalence.
. Then there is a chart \((Z, \delta )\) and chart homomorphisms \(h_i :\langle r_i\rangle \rightarrow (Z, \delta )\) for \(i \in \{1, 2\}\) such that \(h_1(r_1) = h_2(r_2)\). Let \(z = h_1(r_1) = h_2(r_2)\), and note that \(\langle z\rangle = h_1(\langle r_1\rangle ) = h_2(\langle r_2 \rangle )\). In particular, \(\langle z\rangle \) is the homomorphic image of \(\langle r_1\rangle \). By (Expressivity), \(\langle r_1\rangle \in \mathcal C\). By (Closure), \(\langle z\rangle \in \mathcal C\), because it is the homomorphic image of \(\langle r_1\rangle \). By (Solvability), \(\langle r_1\rangle \), \(\langle r_2\rangle \), and \(\langle z\rangle \) all admit unique solutions. Let \(\phi :\langle z \rangle \rightarrow StExp \) be the solution to \(\langle z \rangle \). By Proposition 2.10, \(\phi \circ h_i\) is a solution to \(\langle r_i \rangle \) for \(i \in \{1,2\}\). Since the inclusions \(\langle r_i \rangle \hookrightarrow StExp \) are also solutions, by uniqueness \( \textsf{SL}^* \vdash r_1 = \phi \circ h_1(r_1) = \phi \circ h_2(r_2) = r_2 \), as desired.
, and body transitions, denoted
.
such that \(x \notin \{x_1, \dots , x_n\}\).
for any \(x \in X\).
, then
.
Body transitions are all other transitions. The following result is stated as [27, Lemma 4.1], but follows directly from [6, Proposition 3.7] and the equivalence between LLEE charts and well-layered charts.
is a well-layered entry/body labelling of \((X, \delta )\), then
is also a well-layered entry/body labelling of the generated subchart \(\langle U \rangle _\delta \).
of a chart \((X, \delta )\), define the following two quantities: given \(x \in X\), let \( |x|_{en} = \max \{n \mid \exists y \in Y, x \curvearrowright ^n y\} \) and
.
in which we define for each pair of states such that \(x \curvearrowright y\) the term \(t_\delta (y, x)\) below, by induction on the lexicographical ordering of \(\mathbb {N}\times \mathbb {N}\):
. Then \(\phi _\delta \) as derived from
in Definition 2.14 is the unique solution to \((X, \delta )\). In particular, \(\phi _\delta \) does not depend on
up to equivalence.
) if there is an \(M\)-system \((Z, \beta _Z)\) and homomorphisms \(h :(X, \beta _X) \rightarrow (Z, \beta _Z)\) and \(k :(Y, \beta _Y) \rightarrow (Z, \beta _Z)\) such that \(h(x) = k(y)\).
to indicate the portion of the formula that corresponds to the \(s\) in \(e_1^{(s)}e_2\).
.
if
in its underlying chart, and \(x \rightarrow _\beta y\) if
for some a. By Definition 5.6, a well-layered \(M\)-system \((X, \beta )\) admits an entry/body labelling
,
of \(\textsf{supp}_*(X, \beta )\) that satisfies Definition 2.11. We can then write \(x \curvearrowright y\) for states \(x,y \in X\) if \(x \curvearrowright y\) in this entry/body labelling, and furthermore define \(|{x}|_{en}\) and \(|{x}|_{bo}\) as in Definition 2.14 for \(x \in X\).
be a well-layered entry/body labelling of \((X, \beta )\). We define the canonical solution to \((X, \beta )\) given by
as follows. Let 
for each \(i\), and \(\vec {y}\) is a vector such that
for each \(j\). By induction on \(|x|_{bo} \in \mathbb N\), we definewhere, by induction on \((|x|_{en}, |y|_{bo})\) in the lexicographical ordering of \(\mathbb {N}\times \mathbb {N}\), for each pair of states such that \(x \curvearrowright y\) we define \(\tau _\beta (y, x)\) as follows. First, let 
for each \(i\), and \(\vec {y}\) is a vector such that \(x \ne y_k\) and
for each \(k\). Then
or loop entry transitions
, and those that come from body transitions
or accepting transitions \(x \rightarrow \checkmark \). Malleability assures us that we can write \(\beta (x)\) as described, and similarly for \(\beta (y)\).
. Then the canonical solution \(\phi _\beta \) given by
is the unique solution to \((X, \beta )\). In particular, up to \(\textsf{T}^*\), \(\phi _\beta \) does not depend on
.
, then \(\textsf{T}^* \vdash e_1 = e_2\).
