Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages

TL;DR

This paper introduces a new automaton model and a Kleene-like theorem for Concurrent Kleene Algebra, advancing the understanding of concurrent program behaviors and their formal language representations.

Contribution

It presents a novel automaton construction using Brzozowski derivatives and characterizes automata that represent valid CKA behaviors, addressing a longstanding open problem.

Findings

Automaton model for CKA behaviors established

Kleene-like theorem relating CKA to pomset languages proved

Syntactic characterization of automata for CKA behaviors provided

Abstract

Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We present a new automaton model and a Kleene-like theorem that relates a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours.

Equations

$$\mathcal{U}\cdot \mathcal{V}$$

$$e,f::=0|1|a\in \Sigma |e+f|e\cdot f|e\parallel f|e^{\ast }$$

$$\displaystyle\left\ldbrack 0\right\rdbrack$$

$$\displaystyle\left\ldbrack 1\right\rdbrack$$

$$\displaystyle\left\ldbrack a\right\rdbrack$$

$$\displaystyle\left\ldbrack e+f\right\rdbrack$$

$$\displaystyle\left\ldbrack e\cdot f\right\rdbrack$$

$$\displaystyle\left\ldbrack e\parallel f\right\rdbrack$$

$$\displaystyle\left\ldbrack e^{*}\right\rdbrack$$

$$0ptU=0ptV+0ptW\le 2^{n_r}+2^{n_s}\le 2\cdot 2^{\max (n_r,n_s)}=2^{\max (n_r,n_s)+1}\le 2^{n_q}$$

$$Q_q=\{\perp \}\cup {\rho }_A(q)\cup \bigcup \{Q_r:q^{\prime }\in {\rho }_A(q),\{|r,s|\}\in {\pi }_A(q^{\prime })\}$$

$${\delta }_{\Sigma }(0,a)$$

$${\delta }_{\Sigma }(1,a)$$

$${\delta }_{\Sigma }(b,a)$$

$${\delta }_{\Sigma }(e+f,a)$$

$${\delta }_{\Sigma }(e\cdot f,a)$$

$${\delta }_{\Sigma }(e\parallel f,a)$$

$${\delta }_{\Sigma }(e^{\ast },a)$$

$$f_i^{\prime }$$

$$f\simeq h+\sum _{j\in J}{d}_j\simeq h^{\prime }\cdot e_2+\sum _{k\in K}{h}_k+\sum _{j\in J}{d}_j\simeq f^{\prime }\cdot e_2+\sum _{i\in I}{f}_i$$

$$J_i$$

$$U_i$$

$$f_{i,j}$$

$$U_{i,j}$$

$$f\simeq \sum _{i\in I^{\prime }}{h}_i\simeq \sum _{i\in I^{\prime }}\left(h_i^{\prime }\cdot e^{\ast }+\sum _{i\in K_i}{h}_{i,k}\right)\simeq \sum _{i\in I^{\prime }}\left(h_i^{\prime }\cdot e^{\ast }+\sum _{k\in K_i}\sum _{\ell \in L_{i,k}}{h}_{i,k,\ell }\cdot e^{\ast }\right)\simeq \sum _{i\in I}{f}_i\cdot e^{\ast }$$

$$L_{\Sigma }(0)$$

$$L_{\Sigma }(1)$$

$$L_{\Sigma }(a)$$

$$L_{\Sigma }(e_1+e_2)$$

$$L_{\Sigma }(e_1\cdot e_2)$$

$$L_{\Sigma }(e_1\parallel e_2)$$

$$L_{\Sigma }(e_1^{\ast })$$

$$0pt{\delta }_{\Sigma }(e,a)=0pt{\delta }_{\Sigma }(e_1,a)+{\delta }_{\Sigma }(e_2,a)=\max (0pt{\delta }_{\Sigma }(e_1,a),0pt{\delta }_{\Sigma }(e_2,a))\le \max (0pt{e}_1,0pt{e}_2)=0pte$$

$$0pt{\delta }_{\Sigma }(e,a)$$

$$\le \max (0pt{\delta }_{\Sigma }(e_1,a),0pt{e}_2,0pt{\delta }_{\Sigma }(e_2,a))$$

$$\le \max (0pt{e}_1,0pt{e}_2)=0pte$$

$$0pt{\delta }_{\Sigma }(e,a)$$

$$\le \max (0pt{\delta }_{\Sigma }(e_1,a),0pt{\delta }_{\Sigma }(e_2,a))$$

$$\le \max (0pt{e}_1,0pt{e}_2)=0pt{e}_1\parallel e_2$$

$$0pt{\delta }_{\Sigma }(e,a)=0pt{\delta }_{\Sigma }(e_1,a)\cdot e_1^{\ast }\le \max (0pt{\delta }_{\Sigma }(e_1,a),0pt{e}_1^{\ast })\le 0pte$$

$$e_{q{q}^{\prime }}^{Q^{\prime \prime }}=\sum _{a\in \tilde{\Sigma }}a+\sum _{\{|r,s|\}\in \tilde{Q}}{e}_r^{+}\parallel e_s^{+}.$$

$$e_{q{q}^{\prime }}^{Q^{\prime \prime }}=e_{q{q}^{\prime }}^{Q^{\prime \prime }-\{q^{\prime \prime }\}}+e_{q{q}^{\prime \prime }}^{Q^{\prime \prime }-\{q^{\prime \prime }\}}\cdot {(e_{q^{\prime \prime }{q}^{\prime \prime }}^{Q^{\prime \prime }-\{q^{\prime \prime }\}})}^{\ast }\cdot e_{q^{\prime \prime }{q}^{\prime }}^{Q^{\prime \prime }-\{q^{\prime \prime }\}}.$$

Full text

1 Introduction

In their CONCUR’09 paper [5], Hoare, Möller, Struth, and Wehrman introduced Concurrent Kleene Algebra (CKA) as a suitable mathematical framework to study concurrent programs, in the hope of achieving the same elegance that Kozen did when using Kleene Algebra (and extensions) to provide a verification platform for sequential programs.

CKA is a seemingly simple extension of Kleene Algebra (KA): it adds a parallel operator that allows to specify concurrent behaviours compositionally. However, extending the existing KA toolkit — importantly, completeness and decidability results — turns out to be challenging. A fundamental missing ingredient is a characterization of the free model for CKA. This is in striking contrast with KA, where these topics are well understood. Several authors [6, 8] have conjectured the free model to be series-parallel pomset languages — a generalization of regular languages to sets of partially ordered words.

In KA, Kleene’s theorem provided a pillar for developing the toolkit and axiomatization [12], and, by extension, characterizing the free model. In this light, we pursue a Kleene Theorem for CKA. Specifically, we study series-rational expressions, with a denotational model in terms of pomset languages. Our main contribution is a Kleene Theorem for series-rational expressions, based on constructions faithfully translating between the denotational model and a newly defined operational model, which we call pomset automata. In a nutshell, these are finite-state automata in which computations from a certain state $s$ may branch into parallel threads that contribute to the language of $s$ whenever they both reach a final state.

We are not the first to attempt such a Kleene theorem. However, earlier works [15, 8] fall short of giving a precise correspondence between the denotational and operational models, due to the lack of a suitable automata restriction ensuring that only valid behaviours are accepted. We overcome this situation by introducing a generalization of Brzozowski derivatives [3] in the translation from expressions to automata. This guides us to a syntactic restriction on automata (rather than the semantic condition put forward in previous works), which guarantees the existence of a reverse construction, from automata to expressions. Moreover, following the Brzozowski route allows us to bypass a Thompson-like construction [18], avoiding the introduction of $\epsilon$-transitions and non-determinism present in the aforementioned works.

Since series-parallel expressions do not include the parallel analogue of the Kleene star (the “parallel star”), and our denotational model is not sound for the exchange law (which governs the interaction between sequential and parallel composition), our contribution is most accurately described as an operational model for weak Bi-Kleene Algebra. We leave it to future work to extend our construction to work with a denotational model that is sound for the exchange law (thus moving to weak Concurrent Kleene Algebra), as well as add the parallel star operator (arriving at Concurrent Kleene Algebra proper).

The remainder of this paper is organized as follows. In Section 2, we introduce the necessary notation. In Section 3, we introduce our automaton model as well as some notable subclasses of automata. In Section 4, we discuss how to translate a series-rational expression to a semantically equivalent pomset automaton, while in Section 5 we show how to translate a suitably restricted class of pomset automata to series-rational expressions. We contrast results with earlier work in Section 6. Directions for further work in are listed in Section 7.

To preserve the flow of the narrative, proofs of the more routine lemmas appear in Appendix A.

Acknowledgements

We thank the anonymous reviewers for their insightful comments. This work was partially supported by the ERC Starting Grant ProFoundNet (grant code 679127).

2 Preliminaries

Let $S$ be a set; we write $2^{S}$ for the set of all subsets of $S$, and $\binom{S}{2}$ for the set of multisets over $S$ of size two. An element of $\binom{S}{2}$ containing $s_{1},s_{2}\in S$ is written $\{\mskip-4.0mu|s_{1},s_{2}|\mskip-4.0mu\}$; note that $\{\mskip-4.0mu|s_{1},s_{2}|\mskip-4.0mu\}=\{\mskip-4.0mu|s_{2},s_{1}|\mskip-4.0mu\}$, and that $s_{1}$ may be the same as $s_{2}$. We use the symbols $\phi$ and $\psi$ to denote multisets. If $S$ and $I$ are sets, and for every $i\in I$ there exists an $s_{i}\in S$, we call ${(s_{i})}_{i\in I}$ an $I$-indexed family over $S$. We say that a relation $\prec\ \subseteq S\times S$ is a strict order on $S$ if it is irreflexive and transitive. We refer to $\prec$ as well-founded if there are no infinite descending $\prec$-chains, i.e., no family ${(s_{n})}_{n\in\mathbb{N}}$ over $S$ such that $\forall n\in\mathbb{N},s_{n+1}\prec s_{n}$. Throughout the paper we fix a finite set $\Sigma$ called the alphabet, whose elements are symbols usually denoted with $a$ and $b$. Lastly, if $\rightarrow\ \subseteq X\times Y\times Z$ is a ternary relation, we write $x\xrightarrow{y}z$ instead of $\left\langle x,y,z\right\rangle\in\ \rightarrow$.

2.1 Pomsets

Partially-ordered multisets, or pomsets [4] for short, generalise words to a setting where events (elements from $\Sigma$) may take place not just sequentially, but also in parallel.

Definition \thedefinition.

A labelled poset is a tuple $\left\langle U,\leq_{U},\lambda_{U}\right\rangle$ consisting of a carrier set $U$, a partial order $\leq_{U}$ on $U$ and a labelling function $\lambda_{U}:U\to\Sigma$. A labelled poset isomorphism is a bijection between poset carriers that bijectively preserves the labels and the ordering. A pomset is an isomorphism class of labelled posets; equivalently, it is a labelled poset up-to bijective renaming of elements in $U$. We write $1$ for the empty pomset, $\mathsf{Pom}_{\Sigma}$ for the set of all pomsets and $\mathsf{Pom}_{\Sigma}^{+}$ for the set of all the non-empty pomsets.

For instance, suppose a recipe for caramel-glazed cookies tells us to

(i) preparecookie dough

(ii) bakecookies in the oven

(iii) caramelizesugar

(iv) glazethe finished cookies.

Here, step (i) precedes steps (ii) and (iii). Furthermore, step (iv) succeeds both steps (ii) and (iii). A pomset representing this process could be $\left\langle C,\leq_{C},\lambda_{C}\right\rangle$, where $C=\{\eqref{recipe:dough},\eqref{recipe:bake},\eqref{recipe:caramelize},\eqref{recipe:glaze}\}$ and $\leq_{C}$ is such that $\eqref{recipe:dough}\leq_{C}\eqref{recipe:bake}\leq_{C}\eqref{recipe:glaze}$ and $\eqref{recipe:dough}\leq_{C}\eqref{recipe:caramelize}\leq_{C}\eqref{recipe:glaze}$; $\lambda_{C}$ is as in the recipe.

Note that words are just finite pomsets with a total order. We will sometimes use $a\in\Sigma$ to refer to the pomset with a single point labelled $a$ (and the obvious order); such a pomset is called primitive. A pomset can be represented as a Hasse diagram, where nodes have labels in $\Sigma$. For instance, the Hasse diagram for the pomset $C$ above is drawn in Figure 1(a).

To simplify notation, we refer to a pomset by the carrier $U$ of a labelled poset $\left\langle U,\leq_{U},\lambda_{U}\right\rangle$ in its isomorphism class. We use the symbols $U$, $V$, $W$ and $X$ to denote pomsets. Pomsets being isomorphism classes, the content of the carrier of the chosen representative is of very little importance; it is the order and labelling that matters. For this reason, we tacitly assume that whenever we have two pomsets, we pick representatives that have disjoint carrier sets.

Definition \thedefinition.

The width of a pomset $U$, denoted $0pt{U}$, is the size of the largest antichain in $U$ with respect to $\leq_{U}$, i.e., the maximum $n\in\mathbb{N}$ such that there exist $u_{1},u_{2},\dots,u_{n}\in U$ that are not related by $\leq_{U}$.

The pomsets we work with in this paper have a finite carrier. As a result, $0pt{U}$ is always defined. For instance, the width of the pomset $C$ above is $2$, because the nodes $\eqref{recipe:bake}$ and $\eqref{recipe:caramelize}$ are an antichain of size $2$, and there is no antichain of size $3$.

Definition \thedefinition.

Let $U$ and $V$ be pomsets. The sequential composition of $U$ and $V$, denoted $U\cdot V$, is the pomset $\left\langle U\cup V,\leq_{U}\cup\leq_{V}\cup\,(U\times V),\lambda_{U}\cup\lambda_{V}\right\rangle$. The parallel composition of $U$ and $V$, denoted $U\parallel V$, is the pomset $\left\langle U\cup V,\leq_{U}\cup\leq_{V},\lambda_{U}\cup\lambda_{V}\right\rangle$. Here, $\lambda_{U}\cup\lambda_{V}$ is the function from $U\cup V$ to $\Sigma$ that agrees with $\lambda_{U}$ on $U$, and with $\lambda_{V}$ on $V$.

Note that $1$ is the unit for both sequential and parallel composition. Sequential composition forces the events in the left pomset to be ordered before those in the right pomset. An example, describing the pomset $C\cdot C$, is depicted in Figure 1(b).

Definition \thedefinition.

The set of series-parallel pomsets, $\mathsf{Pom}_{\Sigma}^{\mathsf{sp}}$, is the smallest set that includes the empty and primitive pomsets and is closed under sequential and parallel composition.

In this paper we will be mostly concerned with series-parallel pomsets. For inductive reasoning about them, it is useful to record the following lemma.

Lemma \thelemma.

*Let $U\in\mathsf{Pom}_{\Sigma}^{\mathsf{sp}}$. If $U$ is non-empty, then exactly one of the following is true:

(i) $U=a$for some $a\in\Sigma$, or

(ii) $U=V\cdot W$for non-empty $V,W\in\mathsf{Pom}_{\Sigma}^{\mathsf{sp}}$, strictly smaller than $U$, or

(iii) $U=V\parallel W$for non-empty $V,W\in\mathsf{Pom}_{\Sigma}^{\mathsf{sp}}$, strictly smaller than $U$.

Proof.

We first show that at least one case must hold. The proof proceeds by induction on the construction of $\mathsf{Pom}_{\Sigma}^{\mathsf{sp}}$. In the base, $U$ is a primitive pomset (since it is non-empty), and thus $U=a$ for some $a\in\Sigma$; (i) holds. In the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ for $V$ and $W$ series-parallel, suppose that either $V$ or $W$ is empty. Then $U=W$ or $U=V$ respectively, and thus the claim follows by induction. If neither $V$ nor $W$ is empty, they must both be strictly smaller than $U$, and thus (ii) holds.

• •

If $U=V\parallel W$ for $V$ and $W$ series-parallel, suppose that either $V$ or $W$ is empty. Then $U=W$ or $U=V$ respectively, and thus the claim follows by induction. If neither $V$ nor $W$ is empty, they must both be strictly smaller than $U$, and thus (iii) holds.

To see that at most one of (i), (ii) and (iii) can hold, assume that at least two of them hold. There are three combinations to consider; we derive a contradiction for each.

• •

If (i) and (ii) hold, then $a=U=V\cdot W$ for some $a\in\Sigma$ and non-empty $V,W\in\mathsf{Pom}_{\Sigma}^{\mathsf{sp}}$, strictly smaller than $U$. But then $V$ and $W$ must both be empty (since $U=a$, and thus $U$ must be of size one), and thus it follows that $U$ must be empty as well — a contradiction.

• •

If (i) and (iii) hold, then a contradiction is reached by an argument similar to the above.

• •

If (ii) and (iii) hold, then $U=V_{1}\cdot W_{1}$ and $U=V_{2}\parallel W_{2}$ for non-empty $V_{1},W_{1},V_{2},W_{2}\in\mathsf{Pom}_{\Sigma}^{\mathsf{sp}}$, all strictly smaller than $U$. Suppose $v$ is in $V_{1}$, and $w$ is in $W_{1}$ (such a $v$ and $w$ exist, since $V_{1}$ and $W_{1}$ are non-empty). Then $v$ is ordered before $w$ in $V_{1}\parallel W_{2}$, since $V_{1}\cdot W_{1}=V_{2}\parallel W_{2}$. But then $v$ and $w$ are either both in $V_{2}$ or both in $W_{2}$ — if they were not, this would contradict the definition of parallel composition. Suppose $v$ and $w$ are both in $V_{2}$, and let $w^{\prime}$ be in $W_{2}$ (such a $w^{\prime}$ exists, since $W_{2}$ is non-empty). Then $w^{\prime}$ is ordered neither before nor after $v$ or $w$ in $V_{2}\parallel W_{2}$, and thus the same holds in $V_{1}\cdot W_{2}$. But then $w^{\prime}$ is not in $V_{1}$ (otherwise, $w^{\prime}$ would be ordered before $w$), nor in $W_{1}$ (otherwise, $w^{\prime}$ would be ordered after $v$). This contradicts that $V_{1}\cdot W_{1}=V_{2}\parallel W_{2}$. A similar argument can be made for the case where $v$ and $w$ are both in $W_{2}$. ∎

2.2 Pomset languages

If a sequential program can exhibit multiple traces, we can group the words that represent these traces into a set called a language. By analogy, we can group the pomsets that represent the traces that arise from a parallel program into a set, which we refer to as a pomset language. Pomset languages are denoted by the symbols $\mathcal{U}$ and $\mathcal{V}$.

For instance, suppose that the recipe for glazed cookies may has an optional fifth step where chocolate sprinkles are spread over the cookies. In that case, there are two pomsets that describe a trace arising from the recipe, $C^{+}$ and $C^{-}$, either with or without the chocolate sprinkles. The pomset language $\mathcal{C}=\{C^{-},C^{+}\}$ describes the new recipe.

Definition \thedefinition.

Let $\mathcal{U}$ be a pomset language. $\mathcal{U}$ has bounded width if there is $n\in\mathbb{N}$ such that for all $U\in\mathcal{U}$ we have $0pt{U}\leq n$. The minimal such $n$ is the width of $\mathcal{U}$, written $0pt{\mathcal{U}}$.

The pomset languages considered in this paper have bounded width, and hence $0pt{\mathcal{U}}$ is always defined. For instance, the width of $\mathcal{C}$ is $2$, because the width of both $C^{+}$ and $C^{-}$ is $2$.

The sequential and parallel compositions of pomsets can be lifted to pomset languages. We also define a Kleene closure operator, similar to the one defined on languages of words.

Definition \thedefinition.

Let $\mathcal{U}$ and $\mathcal{V}$ be pomset languages. We define:

[TABLE]

Where $\mathcal{U}^{0}=\{1\}$, and $\mathcal{U}^{n+1}=\mathcal{U}\cdot\mathcal{U}^{n}$ for all $n\in\mathbb{N}$.

Kleene closure models indefinite repetition. For instance, if our cookie recipe has a final step “repeat until enough cookies have been made”, the pomset language $\mathcal{C}^{*}$ represents all possible traces of repetitions of the recipe; e.g., $C^{+}\cdot C^{+}\cdot C^{-}\in\mathcal{C}^{*}$ is the trace where first two batches of sprinkled cookies are made, followed by one without sprinkles.

2.3 Series-rational expressions

Just like a rational expression can be used to describe a regular structure of sequential events, a series-rational expression can be used to describe a regular structure of possibly parallel events. Series-rational expressions are rational expressions with parallel composition.

Definition \thedefinition.

The series-rational expressions, denoted ${\mathcal{T}_{\Sigma}}$, are formed by the grammar

[TABLE]

We use the symbols $d$, $e$, $f$, $g$ and $h$ to denote series-rational expressions.

The semantics of a series-rational expression is given by a pomset language.

Definition \thedefinition.

The function \left\ldbrack-\right\rdbrack:{\mathcal{T}_{\Sigma}}\to 2^{\mathsf{Pom}_{\Sigma}} is defined inductively, as follows:

[TABLE]

If $\mathcal{U}\in 2^{\mathsf{Pom}_{\Sigma}}$ such that \mathcal{U}=\left\ldbrack e\right\rdbrack for some $e\in{\mathcal{T}_{\Sigma}}$, then $\mathcal{U}$ is a series-rational language.

To illustrate, consider the pomset language $\mathcal{C}^{*}={\{C^{+},C^{-}\}}^{*}$, which describes the possible traces arising from indefinitely repeating the cookie recipe, optionally adding chocolate sprinkles at every repetition. We can describe the pomset language $\{C^{-}\}$ with the series-rational expression $c^{-}=\mathsf{prepare}\cdot(\mathsf{bake}\parallel\mathsf{caramelize})\cdot\mathsf{glaze}$, and $\{C^{+}\}$ by $c^{+}=c^{-}\cdot\mathsf{sprinkle}$, which yields the series-rational expression $c=c^{-}+c^{+}$ for $\mathcal{C}$. By construction, \left\ldbrack c^{*}\right\rdbrack=\mathcal{C}^{*}.

2.4 Additive congruence

The following congruence on series-rational expressions will be instrumental in analyzing the automaton we introduce in Section 4, and for restricting said automaton to be finite in Section 4.5.

Definition \thedefinition.

We define $\simeq$ as the smallest congruence on ${\mathcal{T}_{\Sigma}}$ such that: {mathpar} e_1 + 0 ≃e_1 e_1 + e_1 ≃e_1 e_1 + e_2 ≃e_2 + e_1 e_1 + (e_2 + e_3) ≃(e_1 + e_2) + e_3

0 ⋅e_1 ≃0 e_1 ⋅0 ≃0 0 ∥e ≃0 e ∥0 ≃0

When $\{\mskip-4.0mu|g,h|\mskip-4.0mu\},\{\mskip-4.0mu|g^{\prime},h^{\prime}|\mskip-4.0mu\}\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ such that $g\simeq g^{\prime}$ and $h\simeq h^{\prime}$, we write $\{\mskip-4.0mu|g,h|\mskip-4.0mu\}\simeq\{\mskip-4.0mu|g^{\prime},h^{\prime}|\mskip-4.0mu\}$.

Thus, when we claim that $e\simeq e^{\prime}$, we say that $e$ is equal to $e^{\prime}$, modulo associativity, commutativity and idempotence of $+$, as well as its unit [math], and possibly annihilation of sequential and parallel composition by [math]. Moreover, this congruence is sound with respect to the semantics, and it identifies all expressions that have an empty denotational semantics.

Lemma \thelemma.

Let $e,f\in{\mathcal{T}_{\Sigma}}$. If $e\simeq f$, then \left\ldbrack e\right\rdbrack=\left\ldbrack f\right\rdbrack. Also, $e\simeq 0$ if and only if \left\ldbrack e\right\rdbrack=\emptyset.

Proof.

Refer to Appendix A. ∎

There is a simple linear time decision procedure to test whether two expressions are congruent. This justifies our using this relation to build finite automata later on. As a by-product, we get that the emptiness problem for series-rational expressions is linear time decidable.

3 Pomset Automata

We are now ready to describe an automaton model that recognises series-rational languages.

Definition \thedefinition.

A pomset automaton (PA) is a tuple $\left\langle Q,\delta,\gamma,F\right\rangle$ where $Q$ is a set of states, with $F\subseteq Q$ the accepting states, $\delta:Q\times\Sigma\to Q$ is a function called the sequential transition function, $\gamma:Q\times\binom{Q}{2}\to Q$ is a function called the parallel transition function.

Note that we do not fix an initial state. As a result, a PA does not define a single pomset language but rather a mapping from its states to pomset languages. The language of a state is defined in terms of a trace relation that involves the transitions of both $\delta$ and $\gamma$. Here, $\delta$ plays the same role as in classic finite automata: given a state and a symbol, it returns the new state after reading that symbol. The function $\gamma$ warrants a bit more explanation. Given a state $q$ and a binary multiset of states $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}$, $\gamma$ tells us the state that is reached after reading two input streams in parallel starting at states $r$ and $s$, and having both “subprocesses” reach an accepting state. The precise meaning is given in Definition 3 below.

Definition \thedefinition.

$\mathrel{\rightarrow}_{A}\ \subseteq Q\times\mathsf{Pom}_{\Sigma}^{+}\times Q$ is the smallest relation satisfying the rules {mathpar} \inferrule q $\xrightarrow[]{a}$_A δ(q, a) \inferruleq $\xrightarrow[]{U}$_A q”

q” $\xrightarrow[]{V}$_A q’ q $\xrightarrow[]{U\cdot V}$_A q’ \inferruler $\xrightarrow[]{U}$_A r’ ∈F

s $\xrightarrow[]{V}$_A s’ ∈F q $\xrightarrow[]{U\parallel V}$_A γ(q, {|r, s|})

We also define $\mathrel{\rightarrow\mkern-14.0mu}\rightarrow_{A}\ \subseteq Q\times\mathsf{Pom}_{\Sigma}\times Q$ by q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{A}q^{\prime} if and only if $q^{\prime}=q$ and $U=1$, or q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime}. The language of $A$ at $q\in Q$, denoted $L_{A}(q)$, is the set \{U:\exists q^{\prime}\in F.\ q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{A}q^{\prime}\}. We say that $A$ accepts the language $\mathcal{U}$ if there exists a $q\in Q$ such that $L_{A}(q)=\mathcal{U}$.

Intuitively, $\gamma$ ensures that when a process forks at state $q$ into subprocesses starting at $r$ and $s$, if each of those reaches an accepting state, then the processes can join at $\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$.

We purposefully omit the empty pomset $1$ as a label in $\mathrel{\rightarrow}_{A}$; doing so would open up the possibility of having traces of the form q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{1}}}_{A}q^{\prime} with $q\neq q^{\prime}$ (i.e., “silent transitions” or “$\epsilon$-transitions”) for example by defining $\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})=q^{\prime}$ for some $r,s\in F$. Avoiding transitions of this kind allows us to prove claims about $\mathrel{\rightarrow}_{A}$ by induction on the pomset size, and leverage Lemma 2.1 in the process to disambiguate between the rules that apply. By extension, we can prove claims about $\mathrel{\rightarrow\mkern-14.0mu}\rightarrow_{A}$ and $L_{A}$ by treating $U=1$ as a special case.

For the remainder of this section, we fix a PA $A=\left\langle Q,\delta,\gamma,F\right\rangle$, and a state $q\in Q$. To simplify matters later on, we assume that $A$ has a state $\bot\in Q-F$ such that, for every $a\in\Sigma$, it holds that $\delta(\bot,a)=\bot$ and, for every $\phi\in\binom{Q}{2}$, it holds that $\gamma(\bot,\phi)=\bot$. Such a sink state is particularly useful when defining $\gamma$: for a fixed $q\in Q$ not all $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\binom{Q}{2}$ may give a value of $\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$ that contributes to the language accepted by $q$. In such cases, we can define $\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})=\bot$. Alternatively, we could have allowed $\gamma$ to be a partial function; we chose $\gamma$ as a total function so as not to clutter the definition of derivatives in Section 4.

We draw a PA in a way similar to finite automata: each state (except $\bot$) is a vertex, and accepting states are marked by a double border. To represent sequential transitions, we draw labelled edges; for instance, in Figure 1(c), $\delta(q_{0},\mathsf{prepare})=q_{1}$. To represent parallel transitions, we draw hyper-edges; for instance, in Figure 1(c), $\gamma(q_{1},\{\mskip-4.0mu|q_{3},q_{4}|\mskip-4.0mu\})=q_{2}$. To avoid clutter, we do not draw either of these edges types the target state is $\bot$. It is not hard to verify that the pomset $C$ of the earlier example is accepted by the PA in Figure 1(c).

In principle, the state space of a PA can be infinite; we use this in Section 4 to define a PA that has all possible series-rational expressions as states. It is however also useful to know when we can prune an infinite PA into a finite PA while preserving the languages of the retained states. In Section 5, we use this to translate the PA to a series-rational expression.

Note that it is not sufficient to talk about reachable states, i.e., states that appear in the target of some trace; we must also include states that are “meaningful” starting points for subprocesses. To do this, we first need a handle on these starting points. Specifically, we are interested in the states where

(1) the eventual join of the states yields a state that contributes to the behaviour of the PA, and

(2) the states may join again, because they are not the sink state.

This is captured in the definition below.

Definition \thedefinition.

The support of $q$, written $\pi_{A}(q)$, is $\{\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\binom{Q}{2}:\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\}),r,s\neq\bot\}$.

We can now talk about subsets of states of an automaton that are closed, in the sense that the relevant part of a transition function has input and output confined to this set. As a result, we can confine the structure of a given PA to a closed set.

Definition \thedefinition.

A set of states $Q^{\prime}\subseteq Q$ is closed when the following rules are satisfied {mathpar} \inferrule ⊥∈Q’ \inferruleq ∈Q’

a ∈Σδ(q, a) ∈Q’ \inferruleq ∈Q’

ϕ∈π_A(q) γ(q, ϕ) ∈Q’ \inferruleq ∈Q’

{|r, s|} ∈π_A(q) r, s ∈Q’

If $Q^{\prime}$ is closed, the generated sub-PA of $A$ induced by $Q^{\prime}$, denoted $A\!\upharpoonright_{Q^{\prime}}$, is the tuple $\left\langle Q^{\prime},\delta\!\upharpoonright_{Q^{\prime}},\gamma\!\upharpoonright_{Q^{\prime}},Q^{\prime}\cap F\right\rangle$ where $\delta\!\upharpoonright_{Q^{\prime}}$ and $\gamma\!\upharpoonright_{Q^{\prime}}$ are the restrictions of $\delta$ and $\gamma$ to $Q^{\prime}$.

Because the relevant parts of the transition functions are preserved, it is not surprising that the language of a state in a generated sub-PA coincides with the language of that state in the original PA.

Lemma \thelemma.

Let $Q^{\prime}\subseteq Q$ be closed. If $q\in Q^{\prime}$, then $L_{A\!\upharpoonright_{Q^{\prime}}}(q)=L_{A}(q)$.

Proof.

First, observe that $1\in L_{A^{\prime}}(q)$ if and only if $1\in L_{A}(q)$, since $q\in Q^{\prime}\cap F$ if and only if $q\in F$. Now, suppose that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A^{\prime}}q^{\prime}; we show that in this case q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime} follows. The proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$, and $q^{\prime}=\delta\!\upharpoonright_{Q^{\prime}}(q,a)$. But then $q^{\prime}=\delta(q,a)$, and so q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime}. For the inductive step, there are two cases to consider:

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, there exists a $q^{\prime\prime}\in Q^{\prime}$ such that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A^{\prime}}q^{\prime\prime} and q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A^{\prime}}q^{\prime}. By induction, we find q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}q^{\prime\prime} and q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}q^{\prime}, and thus q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime}.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, then there exist $r,s\in Q^{\prime}$ and $r^{\prime},s^{\prime}\in F\cap Q^{\prime}$ such that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A^{\prime}}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A^{\prime}}s^{\prime}, and $q^{\prime}=\gamma\!\upharpoonright_{Q^{\prime}}(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$. By induction we find that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}s^{\prime}; note that $r^{\prime},s^{\prime}\in F$. It then follows that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})=q^{\prime}.

For the other direction, suppose that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime} and $q\neq\bot$; we show that in this case q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A^{\prime}}q^{\prime} follows. The proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$ and $q^{\prime}=\delta(q,a)$. But then $q^{\prime}=\delta\!\upharpoonright_{Q^{\prime}}(q,a)$ and so q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A^{\prime}}q^{\prime}. For the inductive step, there are two cases to consider:

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, there exists a $q^{\prime\prime}\in Q$ such that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}q^{\prime\prime} and q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}q^{\prime}. Since $q^{\prime}\neq\bot$, we have that $q^{\prime\prime}\neq\bot$. By induction we then find that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A^{\prime}}q^{\prime\prime} (thus $q^{\prime\prime}\in Q^{\prime}$) and so again by induction q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A^{\prime}}q^{\prime}. In total, we obtain q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A^{\prime}}q^{\prime}.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, there exist $r,s\in Q$ and $r^{\prime},s^{\prime}\in F$ such that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}s^{\prime}, and $q^{\prime}=\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$. Since $q^{\prime}\neq\bot$, it holds that $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\pi_{A}(q)$, thus $r,s\in Q^{\prime}$; also, since $r^{\prime},s^{\prime}\in F$, we know that $r^{\prime},s^{\prime}\neq\bot$. By induction we find that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A^{\prime}}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A^{\prime}}s^{\prime}. Note that, since $r^{\prime},s^{\prime}\in F$, also $r,s\neq\bot$, and therefore $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\pi_{A}(q)$. We then conclude that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A^{\prime}}\gamma\!\upharpoonright_{Q^{\prime}}(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})=\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})=q^{\prime}. ∎

We now work out how to find a closed subset of states that contains a particular state. The first step is to characterize the states reachable from $q$ by means of transitions.

Definition \thedefinition.

The reach of $q$, written $\rho_{A}(q)$, is the smallest set satisfying the rules {mathpar} \inferrule q ∈ρ_A(q) \inferruleq’ ∈ρ_A(q)

a ∈Σδ(q’, a) ∈ρ_A(q) \inferruleq’ ∈ρ_A(q)

ϕ∈π_A(q) γ(q’, ϕ) ∈ρ_A(q)

The reach of a state is closely connected to the states that can be reached from $q$ through the trace relation of the automaton, in the following way:

Lemma \thelemma.

The set $\rho_{A}(q)\cup\{\bot\}$ contains \{q^{\prime}\in Q:\exists U\in\mathsf{Pom}_{\Sigma}^{+}.\ q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime}\}\cup\{q\}. Moreover, if $\bot$ is the only state of $A$ whose language is empty, this containment is an equality.

Proof.

Refer to Appendix A. ∎

Note that $\rho_{A}(q)\cup\{\bot\}$ is not necessarily closed: we also need the states required by the fourth rule of closure in Definition 3. Thus, if we want to “close” $\rho_{A}(q)\cup\{\bot\}$ by adding the support of its contents, we need to find closed sets of states that contain branching points. In order to do this inductively, we propose the following subclass of PAs.

Definition \thedefinition.

We say that $A$ is fork-acyclic if there exists a fork hierarchy, which is a strict order $\prec_{A}\ \subseteq Q\times Q$ such that the following rules are satisfied. {mathpar} \inferrule{|r, s|} ∈π_A(q) r, s ≺_A q \inferrulea ∈Σ

r ≺_A δ(q, a) r ≺_A q \inferruleϕ∈π_A(q)

r ≺_A γ(q, ϕ) r ≺_A q

The fork hierarchy is connected with the reach of a state in the following way.

Lemma \thelemma.

Let $q^{\prime},r\in Q$. If $A$ is fork-acyclic, $q^{\prime}\in\rho_{A}(q)$ and $r\prec_{A}q^{\prime}$, then $r\prec_{A}q$.

Proof.

The proof proceeds by induction on the construction of $\rho_{A}(q)$. In the base, $q=q^{\prime}$, in which case the claim holds vacuously.

For the inductive step, there are two cases to consider.

• •

If $q^{\prime}=\delta(q^{\prime\prime},a)$ for some $q^{\prime\prime}\in\rho_{A}(q)$ and $a\in\Sigma$, then we know that $r\prec_{A}q^{\prime\prime}$ by definition of $\prec_{A}$. But then $r\prec_{A}q$ by induction.

• •

If $q^{\prime}=\gamma(q^{\prime\prime},\phi)$ for some $q^{\prime\prime}\in\rho_{A}(q)$ and $\phi\in\pi_{A}(q^{\prime\prime})$, then we know that $r\prec_{A}q^{\prime\prime}$ by definition of $\prec_{A}$. But then $r\prec_{A}q$ by induction. ∎

The term fork-acyclic has been used in literature for similar automata [15, 7]. However, in op. cit., it is defined in terms of the traces that arise from the transition structure of the automaton. In contrast, our definition is purely syntactic: it imposes an order on states such that forks cannot be nested. To show that, as in [15], our definition implies that languages of the PA have bounded width, we present the following lemma. Since the state space of a PA can be infinite, we additionally require that the fork hierarchy is well-founded.

Lemma \thelemma.

If $A$ is fork-acyclic and $\prec_{A}$ is well-founded then $L_{A}(q)$ is of finite width.

Proof.

If $q\in Q$, let $n_{q}\in\mathbb{N}$ be the lowest upper bound on the length of a descending chain starting at $q$, i.e., if $r_{1},r_{2},\dots,r_{m}\in Q$ are such that $r_{1}\prec_{A}r_{2}\prec_{A}\dots\prec_{A}r_{m}\prec_{A}q$, then $m\leq n_{q}$. Such an $n_{q}$ exists uniquely, for $\prec_{A}$ is well-founded. We strengthen our claim as follows: if $q\in Q$, then $0pt{L_{A}(q)}\leq 2^{n_{q}}$.

It suffices to show that if $q^{\prime}\in Q$ and $U\in\mathsf{Pom}_{\Sigma}^{+}$ are such that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime} and $q^{\prime}\neq\bot$, then $0pt{U}\leq 2^{n_{q}}$. The proof proceeds by nested induction. The outer induction is on $n_{q}$; here, we assume the claim holds for all $r\in Q$ with $n_{r}<n_{q}$ (note that this implicitly covers the base, where $n_{q}=0$). The inner induction is on $U$. In the base of the inner induction, $U=a\in\Sigma$ and the claim holds immediately, for $0pt{a}=1\leq 2^{n_{q}}$.

For the inductive step of the inner induction, there are two cases to consider.

• •

If $U=V\cdot W$, with $V$ and $W$ smaller than $U$, then there exists a $q^{\prime\prime}\in Q$ such that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}q^{\prime\prime} and q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}q^{\prime}. Since $q^{\prime}\neq\bot$, we know that $q^{\prime\prime}\neq\bot$ as well. Therefore, we know by the (inner and outer) induction hypothesis that $0pt{V}\leq 2^{n_{q}}$. Furthermore, since $q^{\prime\prime}\in\rho_{A}(q)$ by Lemma 3 (the case where $q^{\prime\prime}=\bot$ was excluded), we know that $q^{\prime\prime}\prec_{A}q$ by Lemma 3, therefore $n_{q^{\prime\prime}}<n_{q}$. Thus, by the (inner) induction hypothesis, it follows that that $0pt{W}\leq 2^{n_{q^{\prime\prime}}}$. But then $0pt{U}=\max(0pt{V},0pt{W})\leq\max(2^{n_{q}},2^{n_{q^{\prime\prime}}})=2^{n_{q}}$ as well.

• •

If $U=V\parallel W$, with $V$ and $W$ smaller than $U$, then there exist $r,s\in Q$ and $r^{\prime},s^{\prime}\in F$ such that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}s^{\prime}. By the outer induction hypothesis, we know that $0pt{V}\leq 0pt{L_{A}(r)}\leq 2^{n_{r}}$ and $0pt{W}\leq 0pt{L_{A}(s)}\leq 2^{n_{s}}$. Furthermore, since $q^{\prime},r,s\neq\bot$, we know that $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\pi_{A}(q)$, thus $r,s\prec_{A}q$ and therefore $n_{s},n_{r}<n_{q}$. We then derive

[TABLE]

This completes the proof. ∎

We introduce the notion of a bounded PA, which is sufficient to guarantee the existence of a closed, finite subset containing a given state, even when the PA has infinitely many states.

Definition \thedefinition.

Let $A$ be fork-acyclic. We say that $A$ is bounded if $\prec_{A}$ is well-founded, and for all $q\in Q$, both $\pi_{A}(q)$ and $\rho_{A}(q)$ are finite.

Theorem 3.1**.**

If $A$ is bounded, then for every state $q$ of $A$ there exists a finite set of states ${Q}_{q}\subseteq Q$ that is closed and contains $q$.

Proof.

The proof proceeds by $\prec_{A}$-induction; this is sound, because $\prec_{A}$ is well-founded.

Suppose the claim holds for all $r\in Q$ with $r\prec_{A}q$. If $q^{\prime}\in\rho_{A}(q)$ and $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\pi_{A}(q^{\prime})$, then $r\prec_{A}q^{\prime}$ and thus $r\prec_{A}q$ by Lemma 3; by induction we obtain for every such $r$ a finite set of states ${Q}_{r}\subseteq Q$ that is closed and contains $r$. We choose:

[TABLE]

This set is finite because $\rho_{A}(q)$ and $\pi_{A}(q^{\prime})$ are finite for all $q,q^{\prime}\in Q$ since $A$ is bounded. To see that ${Q}_{q}$ is closed, it suffices to show that the last rule of closure holds for $q^{\prime}\in\rho_{A}(q)$; it does, since if $q^{\prime}\in\rho_{A}(q)$ and $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\pi_{A}(q^{\prime})$, then $r\in{Q}_{r}$ and $s\in{Q}_{s}$, thus $r,s\in{Q}_{q}$. ∎

3.1 Lock-step traces

Note that while the transition functions of a PA are deterministic in that their output is a single state rather than a set of states, the transition relation of a PA $A=\left\langle Q,\delta,\gamma,F\right\rangle$ should not be thought of as deterministic. In particular, if q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime} and q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime\prime}, then $q^{\prime}=q^{\prime\prime}$ does not hold in general. For instance, consider the case where $\gamma(q,\{\mskip-4.0mu|r_{1},s_{1}|\mskip-4.0mu\})=q^{\prime}$ and $\gamma(q,\{\mskip-4.0mu|r_{2},s_{2}|\mskip-4.0mu\})=q^{\prime\prime}$ and furthermore s_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}s_{1}^{\prime}\in F and s_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}s_{2}^{\prime}\in F as well as r_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}r_{1}^{\prime}\in F and r_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}r_{2}^{\prime}\in F. Here, q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V\parallel W}}}_{A}q^{\prime} and q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V\parallel W}}}_{A}q^{\prime\prime}, but $q^{\prime}$ and $q^{\prime\prime}$ may not be equal.

When working with traces in a PA, it is may be useful to be able to relate traces of the same pomset in the presence of this kind of determinism. To this end, we introduce the notion of lock-step traces. Intuitively, lock-step traces prevent the counterexample discussed above by requiring that the application of the third rule must use the same starting states in the construction of both traces.

Definition \thedefinition.

Let $A=\left\langle Q,\delta,\gamma,F\right\rangle$ be a PA and let $U\in\mathsf{Pom}_{\Sigma}^{+}$. Suppose that q_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q_{1}^{\prime} and q_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q_{2}^{\prime}; these traces are in lock-step if one of the following is true:

1. (i)

$U=a$ for some $a\in\Sigma$ 2. (ii)

$U=V\cdot W$, for $V$ and $W$ smaller than $U$, and there exist $q_{1}^{\prime\prime},q_{2}^{\prime\prime}\in Q$ such that q_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}q_{1}^{\prime\prime} and q_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}q_{2}^{\prime\prime} are in lock step, as well as q_{1}^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}q_{1}^{\prime} and q_{2}^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}q_{2}^{\prime} 3. (iii)

$U=V\parallel W$, for $V$ and $W$ smaller than $U$, and there exist $r,s\in Q$ and $r^{\prime},s^{\prime}\in F$ such that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}s^{\prime}, as well as $q_{1}^{\prime}=\gamma(q_{1},\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$ and $q_{2}^{\prime}=\gamma(q_{2},\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$.

It is easy to see that “being in lock-step” is an equivalence relation on traces.

The lemma below observes that traces that are in lock-step do enjoy determinism.

Lemma \thelemma.

Let $A=\left\langle Q,\delta,\gamma,F\right\rangle$ be a PA and let $q,q_{1}^{\prime},q_{2}^{\prime}\in Q$ and $U\in\mathsf{Pom}_{\Sigma}^{+}$. If q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q_{1}^{\prime} and q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q_{2}^{\prime} are in lock-step, then $q_{1}^{\prime}=q_{2}^{\prime}$.

Proof.

The proof proceeds by induction on $U$. If $U=a\in\Sigma$, then $q_{1}^{\prime}=\delta(q,a)$ and $q_{2}^{\prime}=\delta(q,a)$, and so the claim follows.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, then there exist $q_{1}^{\prime\prime},q_{2}^{\prime\prime}\in Q$ such that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}q_{1}^{\prime\prime} and q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}q_{2}^{\prime\prime} are in lock-step, as well as q_{1}^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}q_{1}^{\prime} and q_{2}^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}q_{2}^{\prime}. By induction, $q_{1}^{\prime\prime}=q_{2}^{\prime\prime}$, and thus again by induction $q_{1}^{\prime}=q_{2}^{\prime}$.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, then there exist $r,s\in Q$ and $r^{\prime},s^{\prime}\in F$ such that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}r^{\prime} and S\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}s^{\prime}, and $q_{1}^{\prime}=\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$ and $q_{2}^{\prime}=\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$. The claim then follows. ∎

4 Expressions to automata

We now turn our attention to the task of translating a series-rational expression $e$ into a PA that accepts \left\ldbrack e\right\rdbrack. We employ Brzozowski’s method [3] to construct a single syntactic PA where every series-rational expression is a state accepting exactly its denotational semantics. To this end we must define which expressions are accepting, and how the sequential and parallel transition functions transform states — what are, in Brzozowski’s vocabulary, their sequential and parallel derivatives?

We start with the accepting states. In Brzozowski’s construction, a rational expression is accepting if its denotational semantics includes the empty word. Analogously, a series-rational expression is accepting if its denotational semantics includes the empty pomset.

Definition \thedefinition.

We define the set $F_{\Sigma}$ to be the smallest subset of ${\mathcal{T}_{\Sigma}}$ satisfying the rules: {mathpar} \inferrule 1 ∈F_Σ\inferrulee ∈F_Σ

f ∈${\mathcal{T}_{\Sigma}}$e + f, f + e ∈F_Σ\inferrulee, f ∈F_Σe ⋅f, f ⋅e ∈F_Σ\inferrulee, f ∈F_Σe ∥f, f ∥e ∈F_Σ\inferrulee ∈${\mathcal{T}_{\Sigma}}$e^* ∈F_Σ

It is not hard to see that $e\in F_{\Sigma}$ if and only if 1\in\left\ldbrack e\right\rdbrack. We use $e\star f$ as a shorthand for $f$ if $e\in F_{\Sigma}$, and [math] otherwise. For an equation $\mathcal{E}$, we write $[\mathcal{E}]$ as a shorthand for $1$ if $\mathcal{E}$ holds, and [math] otherwise. We now define sequential and parallel derivatives:

Definition \thedefinition.

We define the functions $\delta_{\Sigma}:{\mathcal{T}_{\Sigma}}\times\Sigma\to{\mathcal{T}_{\Sigma}}$ and $\gamma_{\Sigma}:{\mathcal{T}_{\Sigma}}\times\binom{{\mathcal{T}_{\Sigma}}}{2}\to{\mathcal{T}_{\Sigma}}$ as follows:

[TABLE]

The definition of $\delta_{\Sigma}$ coincides with Brzozowski’s derivative on rational expressions. The definition of $\gamma_{\Sigma}$ mimics the definition of $\delta_{\Sigma}$ on non-parallel terms except $b\in\Sigma$.

The definition of $\gamma_{\Sigma}$ on parallel terms includes (in the first term) the possibility that the starting states provided to the parallel transition function are (congruent to) the operands of the parallel, in which case the target join state is the accepting state $1$. The other two terms (as well as the definition of $\delta_{\Sigma}$ on a parallel term) account for the fact that if 1\in\left\ldbrack e\right\rdbrack, then \left\ldbrack f\right\rdbrack\subseteq\left\ldbrack e\parallel f\right\rdbrack. Since we do not allow traces labelled with the empty pomset, traces that originate from these operands are thus lifted to the composition when necessary.

Definition \thedefinition.

The syntactic PA is the PA $A_{\Sigma}=\left\langle{\mathcal{T}_{\Sigma}},\delta_{\Sigma},\gamma_{\Sigma},F_{\Sigma}\right\rangle$.

We use $L_{\Sigma}$ as a shorthand for $L_{A_{\Sigma}}$, and $\mathrel{\rightarrow}_{\Sigma}$ ($\mathrel{\rightarrow\mkern-14.0mu}\rightarrow_{\Sigma}$) as a shorthand for $\mathrel{\rightarrow}_{A_{\Sigma}}$ ($\mathrel{\rightarrow\mkern-14.0mu}\rightarrow_{A_{\Sigma}}$).

The remainder of this section is devoted to showing that if $e\in{\mathcal{T}_{\Sigma}}$, then L_{\Sigma}(e)=\left\ldbrack e\right\rdbrack.

4.1 Traces of congruent states

In the analysis of the syntactic trace relation $\mathrel{\rightarrow}_{\Sigma}$, we often encounter sums of terms. To work with these, it is useful to identify terms modulo $\simeq$. In this section, we establish that such an identification is in fact sound, in the sense that if two expressions are related by $\simeq$, then the languages accepted by the states representing those expressions are also identical.

In the first step towards this goal, we show that $F_{\Sigma}$ is well-defined with respect to $\simeq$.

Lemma \thelemma.

Let $e,f\in{\mathcal{T}_{\Sigma}}$ be such that $e\simeq f$. Then $e\in F_{\Sigma}$ if and only if $f\in F_{\Sigma}$.

Proof.

Refer to Appendix A. ∎

Also, $\delta_{\Sigma}$ and $\gamma_{\Sigma}$ are well-defined with respect to $\simeq$, in the following sense:

Lemma \thelemma.

Let $e,f\in{\mathcal{T}_{\Sigma}}$ such that $e\simeq f$. If $a\in\Sigma$, then $\delta_{\Sigma}(e,a)\simeq\delta_{\Sigma}(f,a)$. Moreover, if $\phi=\{\mskip-4.0mu|g,h|\mskip-4.0mu\}\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ with $g,h\not\simeq 0$, then $\gamma_{\Sigma}(e,\phi)\simeq\gamma_{\Sigma}(f,\phi)$, and if $\psi\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ with $\phi\simeq\psi$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e,\psi)$.

Proof.

Refer to Appendix A. ∎

With these lemmas in hand, we can show that $\simeq$ is a “bisimulation” with respect to $\mathrel{\rightarrow}_{\Sigma}$.

Lemma \thelemma.

Let $e,f\in{\mathcal{T}_{\Sigma}}$ be such that $e\simeq f$. If e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}e^{\prime}, then there exists an $f^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} and $e^{\prime}\simeq f^{\prime}$.

Proof.

The proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$. But then $e^{\prime}=\delta_{\Sigma}(e,a)$. If we choose $f^{\prime}=\delta_{\Sigma}(f,a)$, we find that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} and $e^{\prime}\simeq f^{\prime}$ by Lemma 4.1.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, there exists an $e^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}e^{\prime\prime} and e^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}e^{\prime}. By induction, we find an $f^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f^{\prime\prime} and $e^{\prime\prime}\simeq f^{\prime\prime}$. Again by induction, we find $f^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that f^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f^{\prime} and $e^{\prime}\simeq f^{\prime}$. This means that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} with $e^{\prime}\simeq f^{\prime}$.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, and $e^{\prime}=\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. Note that, in this case, $g,h\neq 0$ by Lemma 4.2 (which will be proved shortly). If we choose $f^{\prime}=\gamma_{\Sigma}(f,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$ we find that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} with $e^{\prime}\simeq f^{\prime}$ by Lemma 4.1. ∎

Let $I$ be a finite set, and let ${(e_{i})}_{i\in I}$ be an $I$-indexed family of terms. In the sequel, we treat $\sum_{i\in I}e_{i}$ as a term, where the $e_{i}$ are summed in some arbitrary order or bracketing. The lemmas above guarantee that the precise choice of representing this sum as a term makes no matter with regard to the traces allowed.

4.2 Trace deconstruction

We proceed with a series of lemmas that characterise reachable states in the syntactic PA. More precisely, we show that the expressions reachable from some expression $e$ can be written as sums of expressions reachable from subexpressions of $e$. For this reason, we refer to these observations as trace deconstruction lemmas: they deconstruct a trace of an expression into traces of “smaller” expressions. The purpose of these lemmas is twofold; in Section 4.4, they are used to characterise the languages of expressions as they appear in the syntactic PA, while in Section 4.5 they allow us to bound the reach of an expression.

We start by analysing the traces that originate in base terms, such as [math], $1$, or $a\in\Sigma$.

Lemma \thelemma.

Let $e,e^{\prime}\in{\mathcal{T}_{\Sigma}}$ and $U\in\mathsf{Pom}_{\Sigma}^{+}$ such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}e^{\prime}. If $e\in\{0,1\}$, then $e^{\prime}=0$. Furthermore, if $e=b\in\Sigma$, then either $e^{\prime}=1$ and $U=b$, or $e^{\prime}=0$.

Proof.

The proof of the first claim proceeds by induction on $U$. In the base, $U=a\in\Sigma$, and $e^{\prime}=\delta_{\Sigma}(e,a)=0$, thus the claim holds.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$, with $V$ and $W$ smaller than $U$, then there exists an $e^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}e^{\prime\prime} and e^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}e^{\prime}. By induction, $e^{\prime\prime}=0$, and thus again by induction $e^{\prime}=0$.

• •

If $U=V\parallel W$, with $V$ and $W$ smaller than $U$, then there exist $f,g\in{\mathcal{T}_{\Sigma}}$ and $f^{\prime},g^{\prime}\in F_{\Sigma}$ such that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f^{\prime} and g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g^{\prime}, and furthermore $e^{\prime}=\gamma_{\Sigma}(e,\{\mskip-4.0mu|f,g|\mskip-4.0mu\})=0$.

The proof of the second claim also proceeds by induction on $U$. In the base, $U=a\in\Sigma$. Then $e^{\prime}=\delta_{\Sigma}(b,a)$. If $a=b$, then $e^{\prime}=1$, otherwise $e^{\prime}=0$; thus the claim holds.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, then there exists an $e^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that b\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}e^{\prime\prime} and e^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}e^{\prime}. By induction, either $V=b$ and $e^{\prime\prime}=1$, or $e^{\prime\prime}=0$. In either case, $e^{\prime}=0$ by the first claim.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, then there exist $f,g\in{\mathcal{T}_{\Sigma}}$ and $f^{\prime},g^{\prime}\in F_{\Sigma}$ such that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f^{\prime} and g^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g^{\prime}, and $e^{\prime}=\gamma_{\Sigma}(e,\{\mskip-4.0mu|f,g|\mskip-4.0mu\})=0$. The claim thus holds immediately. ∎

Note, however, that [math] and $1$ are not indistinguishable, for $0\not\in F_{\Sigma}$ while $1\in F_{\Sigma}$.

We also consider the traces that originate in a sum of terms. The intuition here is that the input is processed by both terms simultaneously, and thus the target state must be the sum of the states that are the result of processing the input for each term individually.

Lemma \thelemma.

Let $e_{1},e_{2}\in{\mathcal{T}_{\Sigma}}$ and $U\in\mathsf{Pom}_{\Sigma}^{+}$. If e_{1}+e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}e^{\prime}, then there exist $e_{1}^{\prime},e_{2}^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that $e^{\prime}=e_{1}^{\prime}+e_{2}^{\prime}$, and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}e_{1}^{\prime} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}e_{2}^{\prime}.

Proof.

The proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$, and $e^{\prime}=\delta_{\Sigma}(e_{1}+e_{2},a)=\delta_{\Sigma}(e_{1},a)+\delta_{\Sigma}(e_{2},a)$. We can then choose $e_{1}^{\prime}=\delta_{\Sigma}(e_{1},a)$ and $e_{2}^{\prime}=\delta_{\Sigma}(e_{2},a)$ to validate the claim.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, then there exists an $e^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that e_{1}+e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}e^{\prime\prime} and e^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}e^{\prime}. By induction, we find $e_{1}^{\prime\prime},e_{2}^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that $e^{\prime\prime}=e_{1}^{\prime\prime}+e_{2}^{\prime\prime}$, and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}e_{1}^{\prime\prime} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}e_{2}^{\prime\prime}. Again by induction, we find $e_{1}^{\prime},e_{2}^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that $e^{\prime}=e_{1}^{\prime}+e_{2}^{\prime}$, and e_{1}^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}e_{1}^{\prime} and e_{2}^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}e_{2}^{\prime}. In conclusion, we find that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}e_{1}^{\prime} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}e_{2}^{\prime}.

• •

If $U=V\parallel W$, with $V$ and $W$ smaller than $U$, then there exist $f,g\in{\mathcal{T}_{\Sigma}}$ such that $e^{\prime}=\gamma_{\Sigma}(e_{1}+e_{2},\{\mskip-4.0mu|f,g|\mskip-4.0mu\})=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|f,g|\mskip-4.0mu\})+\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|f,g|\mskip-4.0mu\})$, and furthermore there exist $f^{\prime},g^{\prime}\in F_{\Sigma}$ such that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f^{\prime} and g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g^{\prime}. We can choose $e_{1}^{\prime}=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|f,g|\mskip-4.0mu\})$ and $e_{2}^{\prime}=\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|f,g|\mskip-4.0mu\})$ to validate the claim. ∎

We now consider the traces starting in a sequential composition. The intuition here is that the syntactic PA must first proceed through the left operand, before it can proceed to process the right operand. Thus, either the pomset is processed by the left operand entirely, or we should be able to split the pomset in two sequential parts: the first part is processed by the left operand, and the second by the right operand.

Lemma \thelemma.

Let $e_{1},e_{2}\in{\mathcal{T}_{\Sigma}}$ and $U\in\mathsf{Pom}_{\Sigma}^{+}$ be such that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f. There exist an $f^{\prime}\in{\mathcal{T}_{\Sigma}}$ and a finite set $I$, as well as $I$-indexed families ${(f_{i}^{\prime})}_{i\in I}$ over $F_{\Sigma}$ and ${(f_{i})}_{i\in I}$ over ${\mathcal{T}_{\Sigma}}$, and $I$-indexed families ${(U_{i}^{\prime})}_{i\in I}$, ${(U_{i})}_{i\in I}$ over $\mathsf{Pom}_{\Sigma}^{+}$, such that:

• •

$f\simeq f^{\prime}\cdot e_{2}+\sum_{i\in I}f_{i}$* and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime}, and*

• •

for all $i\in I$, e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}f_{i}^{\prime}, e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i}, and $U=U_{i}^{\prime}\cdot U_{i}$.

Proof.

The proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$, and $f=\delta_{\Sigma}(e_{1}\cdot e_{2},a)$. If on the one hand $e_{1}\not\in F_{\Sigma}$, then $f\simeq\delta_{\Sigma}(e_{1},a)\cdot e_{2}$; we choose $f^{\prime}=\delta_{\Sigma}(e_{1},a)$ and $I=\emptyset$. If on the other hand $e_{1}\in F_{\Sigma}$, then $f\simeq\delta_{\Sigma}(e_{1},a)\cdot e_{2}+\delta_{\Sigma}(e_{2},a)$; we choose $f^{\prime}=\delta_{\Sigma}(e_{1},a)$, $I=\{*\}$, $f_{*}^{\prime}=e_{1}$, $f_{*}=\delta_{\Sigma}(e_{2},a)$, $U_{*}^{\prime}=1$ and $U_{*}=U$. In either case, our choices validate the claim.

For the inductive step, we consider two cases.

• •

If $U=V\cdot W$, with $V$ and $W$ smaller than $U$, then there exists a $g$ such that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g and g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f. By induction, we obtain a $g^{\prime}\in{\mathcal{T}_{\Sigma}}$ and a finite set $J$, as well as $J$-indexed families ${(g_{j}^{\prime})}_{j\in J}$ over $F_{\Sigma}$ and ${(g_{j})}_{j\in J}$ over ${\mathcal{T}_{\Sigma}}$, and $J$-indexed families ${(V_{j}^{\prime})}_{j\in J}$ and ${(V_{j})}_{j\in J}$ over $\mathsf{Pom}_{\Sigma}^{+}$, such that

• –

$g\simeq g^{\prime}\cdot e_{2}+\sum_{j\in J}g_{j}$ and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime}, and

• –

for all $j\in J$, e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{j}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}g_{j}^{\prime}, e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{j}}}}_{\Sigma}g_{j} and $V=V_{j}^{\prime}\cdot V_{j}$.

By Lemma 4.1 and $g\simeq g^{\prime}\cdot e_{2}+\sum_{j\in J}g_{i}$, as well as Lemma 4.2 and g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f, there exist $h\in{\mathcal{T}_{\Sigma}}$ and a $J$-indexed family of terms ${(d_{j})}_{j\in J}$ over ${\mathcal{T}_{\Sigma}}$ such that $f\simeq h+\sum_{j\in J}d_{j}$, g^{\prime}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h and for all $j\in J$, also g_{j}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}d_{j}.

Since g^{\prime}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h, we can find (again by induction) an $h^{\prime}\in{\mathcal{T}_{\Sigma}}$, and a finite set $K$ (without loss of generality, disjoint from $J$) and $K$-indexed families ${(h_{k}^{\prime})}_{k\in K}$ over $F_{\Sigma}$ and ${(h_{k})}_{k\in K}$ over ${\mathcal{T}_{\Sigma}}$, as well as $K$-indexed families ${(W_{k}^{\prime})}_{k\in K}$ over $\mathsf{Pom}_{\Sigma}$ and ${(W_{k})}_{k\in K}$ over $\mathsf{Pom}_{\Sigma}^{+}$ such that

• –

$h\simeq h^{\prime}\cdot e_{2}+\sum_{k\in K}h_{k}$ and g^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, and

• –

for all $k\in K$, g^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{k}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}h_{k}^{\prime}, e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{k}}}}_{\Sigma}h_{k} and $W=W_{k}^{\prime}\cdot W_{k}$.

We now choose $I=J\cup K$, and $f^{\prime}=h^{\prime}$. Furthermore, we choose $I$-indexed families ${(f_{i}^{\prime})}_{i\in I}$ over $F_{\Sigma}$ and ${(f_{i})}_{i\in I}$ over ${\mathcal{T}_{\Sigma}}$, as well as $I$-indexed families ${(U_{i}^{\prime})}_{i\in I}$ over $\mathsf{Pom}_{\Sigma}$ and ${(U_{i})}_{i\in I}$ over $\mathsf{Pom}_{\Sigma}^{+}$ as follows:

[TABLE]

It remains to verify the requirements on our choices one by one. For the first claim, we can derive

[TABLE]

Furthermore, since e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and g^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, we have that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}h^{\prime}=f^{\prime}. For the second claim, let us fix an $i\in I$. Suppose first that $i\in J$, then:

• –

e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{i}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}g_{i}^{\prime}, thus e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}f_{i}^{\prime}

• –

e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{i}}}}_{\Sigma}g_{i} and g_{i}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}d_{i}, thus e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i}

• –

$U_{i}^{\prime}\cdot U_{i}=V_{i}^{\prime}\cdot V_{i}\cdot W=V\cdot W=U$.

Secondly, suppose that $i\in K$, then:

• –

e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and g^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}h_{i}^{\prime}, thus e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}f_{i}^{\prime}

• –

e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i}}}}_{\Sigma}h_{i}, thus e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i}

• –

$U_{i}^{\prime}\cdot U_{i}=V\cdot W_{i}^{\prime}\cdot W_{i}=V\cdot W=U$.

All requirements are thus validated for our choices in this case.

• •

If $U=V\parallel W$, then there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, and we know that $f=\gamma_{\Sigma}(e_{1}\cdot e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. If on the one hand $e_{1}\not\in F_{\Sigma}$, then $f\simeq\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\cdot e_{2}$; we choose $f^{\prime}=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g_{1},g_{2}|\mskip-4.0mu\})$ and $I=\emptyset$. If on the other hand $e_{1}\in F_{\Sigma}$, then $f\simeq\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\cdot e_{2}+\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$; we choose $f^{\prime}=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g_{1},g_{2}|\mskip-4.0mu\})$ and $I=1$, as well as $f_{*}^{\prime}=e_{1}$, $f_{*}=\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g_{1},g_{2}|\mskip-4.0mu\})$, $U_{*}^{\prime}=1$ and $U_{*}^{\prime}=U$. In both cases, our choices validate the claim. ∎

The next deconstruction lemma concerns traces originating in a parallel composition. Intuitively, the syntactic PA either processes parallel components of the pomset, or processes according to one operand, provided that the other operand allows immediate acceptance.

Lemma \thelemma.

If e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f, then there exist $f_{1},f_{2},f_{3}\in{\mathcal{T}_{\Sigma}}$, such that

• •

$f\simeq f_{1}+f_{2}+f_{3}$,

• •

either $f_{1}=0$, or $e_{2}\in F_{\Sigma}$ and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1},

• •

either $f_{2}=0$, or $e_{1}\in F_{\Sigma}$ and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{2}, and

• •

either $f_{3}=0$, or $f_{3}=1$ and there exist $f_{1}^{\prime},f_{2}^{\prime}\in F_{\Sigma}$ and $U_{1},U_{2}\in\mathsf{Pom}_{\Sigma}^{+}$ such that $U=U_{1}\parallel U_{2}$ and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{1}}}}_{\Sigma}f_{1}^{\prime} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{2}}}}_{\Sigma}f_{2}^{\prime}.

Proof.

The proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$. Now, choose $f_{2}=e_{1}\star\delta_{\Sigma}(e_{2},a)$ and $f_{1}=e_{2}\star\delta_{\Sigma}(e_{1},a)$. We also choose $f_{3}=0$. It is easy to validate that the claim holds for these choices.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, then there exists a $g\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g and g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f. By induction, we obtain $g_{1},g_{2},g_{3}$ such that:

• –

$g\simeq g_{1}+g_{2}+g_{3}$,

• –

either $g_{1}=0$, or $e_{2}\in F_{\Sigma}$ and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g_{1},

• –

either $g_{2}=0$, or $e_{1}\in F_{\Sigma}$ and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g_{2}, and

• –

either $g_{3}=0$, or $g_{3}=1$ and there exist $e_{1}^{\prime},e_{2}^{\prime}\in{\mathcal{T}_{\Sigma}}$ and $g_{1}^{\prime},g_{2}^{\prime}\in F_{\Sigma}$ and $V_{1},V_{2}\in\mathsf{Pom}_{\Sigma}^{+}$ such that $e_{1}\simeq e_{1}^{\prime}$ and $e_{2}\simeq e_{2}^{\prime}$ and $V=V_{1}\parallel V_{2}$ and e_{1}^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{1}}}}_{\Sigma}g_{1}^{\prime} and e_{2}^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{2}}}}_{\Sigma}g_{2}^{\prime}.

By $g\simeq g_{1}+g_{2}+g_{3}$ and Lemma 4.1, as well as g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f and Lemma 4.2, we obtain $f_{1},f_{2},f_{3}\in{\mathcal{T}_{\Sigma}}$ such that $f\simeq f_{1}+f_{2}+f_{3}$, and g_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f_{1}, g_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f_{2} and g_{3}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f_{3}. We now validate the remaining claims. First, note that if $g_{i}=0$ for all $i\in\{1,2,3\}$, then $f_{i}=0$ by Lemma 4.2. As to the remaining possibilities:

• –

If $g_{1}\neq 0$, then $e_{2}\in F_{\Sigma}$ and by e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g_{1} and g_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f_{1} we conclude that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1}.

• –

If $g_{2}\neq 0$, then $e_{1}\in F_{\Sigma}$ and by e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g_{2} and g_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f_{2} we conclude that e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{2}.

• –

If $g_{3}\neq 0$, then $g_{3}=1$ and we conclude that $f_{3}=0$ by Lemma 4.2.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, then there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that $f=\gamma_{\Sigma}(e_{1}\parallel e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$, and g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime}\in F_{\Sigma} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}\in F_{\Sigma}. We choose $f_{1}=e_{2}\star\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$ and $f_{2}=e_{1}\star\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. Furthermore, we set $f_{3}=[\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}=\{\mskip-4.0mu|g,h|\mskip-4.0mu\}]$. It is now easy to see that $f\simeq f_{1}+f_{2}+f_{3}$. We validate the remaining claims.

• –

If $e_{2}\not\in F_{\Sigma}$, then $f_{1}=0$. Otherwise, $e_{2}\in F_{\Sigma}$ and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=f_{1}.

• –

If $e_{1}\not\in F_{\Sigma}$, then $f_{2}=0$. Otherwise, $e_{1}\in F_{\Sigma}$ and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=f_{2}.

• –

If $\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}\not\simeq\{\mskip-4.0mu|g,h|\mskip-4.0mu\}$, then $f_{3}=0$. Otherwise, assume (without loss of generality) that $e_{1}\simeq g$ and $e_{2}\simeq h$. By Lemma 4.1 and the fact that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} as well as h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, there exist $f_{1}^{\prime},f_{2}^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f_{1}^{\prime} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f_{2}^{\prime}, with $f_{1}^{\prime}\simeq g^{\prime}$ and $f_{2}^{\prime}\simeq h^{\prime}$. By Lemma 4.1 and the fact that $g^{\prime},h^{\prime}\in F_{\Sigma}$, it then follows that $f_{1},f_{2}^{\prime}\in F_{\Sigma}$. Choosing $U_{1}=V$ and $U_{2}=W$ now validates the claim. ∎

Finally, we analyse the reachable states of an expression of the form $e^{*}$. The intuition here is that, starting in $e^{*}$, the PA can iterate traces originating in $e$ indefinitely. The trace should thus be sequentially decomposable, with each component the label of a trace originating in $e$. Furthermore, all but the last target state of these traces should be accepting.

Lemma \thelemma.

If e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f, then there exists a finite set $I$ and an $I$-indexed family of finite sets ${(J_{i})}_{i\in I}$, as well as $I$-indexed families ${(f_{i})}_{i\in I}$ over ${\mathcal{T}_{\Sigma}}$ and ${(U_{i})}_{i\in I}$ over $\mathsf{Pom}_{\Sigma}^{+}$, and for all $i\in I$ also $J_{i}$-indexed families ${(f_{i,j})}_{j\in J_{i}}$ over $F_{\Sigma}$ and ${(U_{i,j})}_{j\in J_{i}}$ over $\mathsf{Pom}_{\Sigma}^{+}$, such that $f\simeq\sum_{i\in I}f_{i}\cdot e^{*}$, and for all $i\in I$:

• •

e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i},

• •

for all $j\in J_{i}$ we have that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i,j}}}}_{\Sigma}f_{i,j}, and

• •

$U=U_{i}^{\prime}\cdot U_{i}$, where $U_{i}^{\prime}$ is some concatenation of all $U_{i,j}$ for all $j\in J_{i}$.

Proof.

The proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$, and so $f=\delta_{\Sigma}(e^{*},a)=\delta_{\Sigma}(e,a)\cdot e^{*}$. We can choose $I=\{*\}$, $J_{*}=\emptyset$ and $U_{*}=a$ to validate the claim.

For the inductive step, we consider two cases.

• •

If $U=V\cdot W$, with $V$ and $W$ smaller than $U$, there exists a $g$ such that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g and g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f. Since the remainder of this part of the proof is somewhat involved, we begin by outlining our strategy. First, we deconstruct the trace e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g, by induction. Then we deconstruct the trace g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f, making use of the fact that $g$ can be seen a sum of the form found in the claim, i.e., where each term is of the form $g^{\prime}\cdot e^{*}$, and thus (by Lemma 4.2) $f$ can be seen as a sum of terms $f^{\prime}$ such that g^{\prime}\cdot e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f^{\prime}. We then leverage Lemma 4.2 to deconstruct each of the latter traces. In the end, we have a big cache of variables, which we use to construct the families of terms and pomsets required by the claim. Since we will be dealing with a fair number of index sets, we tacitly assume (without loss of generality) that of them are disjoint.

As for the proof, consider the trace e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g. By induction, we obtain a finite set $I^{\prime}$ and an $I^{\prime}$-indexed family of finite sets ${(J_{i}^{\prime})}_{i\in I^{\prime}}$, as well as $I^{\prime}$-indexed families ${(g_{i})}_{i\in I^{\prime}}$ over ${\mathcal{T}_{\Sigma}}$ and ${(V_{i})}_{i\in I^{\prime}}$ over $\mathsf{Pom}_{\Sigma}^{+}$ and for all $i\in I^{\prime}$ also $J_{i}^{\prime}$-indexed families ${(g_{i,j})}_{j\in J_{i}^{\prime}}$ over $F_{\Sigma}$ and ${(V_{i,j})}_{j\in J_{i}^{\prime}}$ over $\mathsf{Pom}_{\Sigma}^{+}$, such that $g\simeq\sum_{i\in I^{\prime}}g_{i}\cdot e^{*}$, and for all $i\in I^{\prime}$:

• –

e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{i}}}}_{\Sigma}g_{i},

• –

for all $j\in J_{i}^{\prime}$ we have that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{i,j}}}}_{\Sigma}g_{i,j}\in F_{\Sigma}, and

• –

$V=V_{i}^{\prime}\cdot V_{i}$, where $V_{i}^{\prime}$ is some concatenation of $V_{i,j}$ for all $j\in J_{i}^{\prime}$.

By the fact that $g\simeq\sum_{i\in I^{\prime}}g_{i}\cdot e^{*}$ and by Lemma 4.1, as well as g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f and Lemma 4.2, we find an $I^{\prime}$-indexed family ${(h_{i})}_{i\in I^{\prime}}$ over ${\mathcal{T}_{\Sigma}}$ such that $f\simeq\sum_{i\in I^{\prime}}h_{i}$, and for all $i\in I^{\prime}$ also g_{i}\cdot e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h_{i}. Then, by Lemma 4.2, we find for all $i\in I^{\prime}$ a term $h_{i}^{\prime}$ and finite set $K_{i}$ as well as $K_{i}$-indexed families ${(h_{i,k}^{\prime})}_{k\in K_{i}}$ over $F_{\Sigma}$ and ${(h_{i,k})}_{k\in K_{i}}$ over ${\mathcal{T}_{\Sigma}}$ and ${(W_{i,k}^{\prime})}_{k\in K_{i}}$ over $\mathsf{Pom}_{\Sigma}$ and ${(W_{i,k})}_{k\in K_{i}}$ over $\mathsf{Pom}_{\Sigma}^{+}$, such that

• –

$h_{i}\simeq h_{i}^{\prime}\cdot e^{*}+\sum_{k\in K_{i}}h_{i,k}$ and g_{i}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h_{i}^{\prime}, and

• –

for all $k\in K_{i}$, g_{i}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}h_{i,k}^{\prime}, e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i}}}}_{\Sigma}h_{i,k} and $W=W_{k}^{\prime}\cdot W_{k}$.

By induction and since for all $i\in I^{\prime}$ and $k\in K_{i}$ we have that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i}}}}_{\Sigma}h_{i,k}, we obtain for this $i$ and $k$ a finite set $L_{i,k}$ and an $L_{i,k}$-indexed family of finite sets ${(M_{i,k,\ell})}_{\ell\in L_{i,k}}$, as well as $L_{i,k}$-indexed families ${(h_{i,k,\ell})}_{\ell\in L_{i,k}}$ over ${\mathcal{T}_{\Sigma}}$ and ${(W_{i,k,\ell})}_{\ell\in L_{i,k}}$ over $\mathsf{Pom}_{\Sigma}^{+}$, and for all $\ell\in L_{i,k}$ also $M_{i,k,\ell}$-indexed families ${(h_{i,k,\ell,m})}_{m\in M_{i,k,\ell}}$ over $F_{\Sigma}$ and ${(V_{i,k,\ell,m})}_{m\in M_{i,k,\ell}}$ over $\mathsf{Pom}_{\Sigma}^{+}$ such that $h_{i,k}\simeq\sum_{\ell\in L_{i,k}}h_{i,k,\ell}\cdot e^{*}$, and for all $\ell\in L_{i,k}$:

• –

e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i,k,\ell}}}}_{\Sigma}h_{i,k,\ell},

• –

for all $m\in M_{i,k,\ell}$ we have that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i,k,\ell,m}}}}_{\Sigma}h_{i,k,\ell,m}, and

• –

$W_{i}=W_{i,k,\ell}^{\prime}\cdot W_{i,k,\ell}$, where $W_{i,k,\ell}^{\prime}$ is some concatenation of $W_{i,k,\ell,m}$ for $m\in M_{i,k,\ell}$.

We are now ready to choose the required (families of) sets, terms and pomsets, as follows:

• –

$I=I^{\prime}+\bigcup_{k\in K_{i}}L_{i,k}$

• –

for all $i\in I$, we set

[TABLE]

• –

for all $i\in I$ and $j\in J_{i}$, we set

[TABLE]

It remains to check the requirements on our choices.

• –

One easily verifies that

[TABLE]

• –

If $i\in I$, there are two cases to consider.

If $i\in I^{\prime}$, then since e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{i}}}}_{\Sigma}g_{i} and g_{i}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h_{i}^{\prime}, we find that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i}.

• *

If $i\in L_{i^{\prime},k}$ for some $i^{\prime}\in I^{\prime}$ and $k\in K_{i^{\prime}}$, then since e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i^{\prime},k,i}}}}_{\Sigma}h_{i^{\prime},k,i} we find that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i}.

• –

If $i\in I$ and $j\in J_{i}$, there are three cases to consider.

If $i\in I^{\prime}$ and $j\in J_{i}^{\prime}$, then since e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{i,j}}}}_{\Sigma}g_{i,j}, we find that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i,j}}}}_{\Sigma}f_{i,j}.

• *

If $i\in L_{i^{\prime},k}$ for some $i^{\prime}\in I^{\prime}$ and $k\in K_{i^{\prime}}$, and $j=*_{i}$, then since e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{i^{\prime}}}}}_{\Sigma}g_{i} and g_{i}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i^{\prime}}^{\prime}}\mkern-14.0mu\rightarrow}}_{\Sigma}h_{i^{\prime},k}^{\prime}, we find that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i,j}}}}_{\Sigma}f_{i,j}.

• *

If $i\in L_{i^{\prime},k}$ for some $i^{\prime}\in I^{\prime}$ and $k\in K_{i^{\prime}}$, and $j\neq*_{i}$ (thus $j\in M_{i^{\prime},k,i}$), then since e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i^{\prime},k,i,j}}}}_{\Sigma}h_{i^{\prime},k,i,j} we find that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i,j}}}}_{\Sigma}f_{i,j}.

• –

If $i\in I$, there are two cases to consider.

If $i\in I^{\prime}$, then $V=V_{i}^{\prime}\cdot V_{i}$, where $V_{i}^{\prime}$ is some concatenation of $V_{i,j}$ for all $j\in J_{i}^{\prime}$. But then we can choose $U_{i}^{\prime}=V_{i}^{\prime}$ as a concatenation of $U_{i,j}$ for all $j\in J_{i}$, to find that $U_{i}^{\prime}\cdot U_{i}=V_{i}^{\prime}\cdot V_{i}\cdot W=V\cdot W=U$.

• *

If $i\in L_{i^{\prime},k}$ for all $i^{\prime}\in I^{\prime}$ and $k\in K_{i^{\prime}}$, then we know that there exists a pomset $W_{i^{\prime},k,i}^{\prime}$ which is a concatenation of $W_{i^{\prime},k,i,m}$ for all $m\in M_{i^{\prime},k,i}$, such that $W_{i^{\prime},k,i}^{\prime}\cdot W_{i^{\prime},k,i}=W_{i^{\prime}}$. We can then choose $U_{i}^{\prime}=V\cdot W_{i^{\prime}}^{\prime}\cdot W_{i^{\prime},k,i}^{\prime}$ as a concatenation of $U_{i,j}$ with $j\in J_{i}$, and find that $U_{i}^{\prime}\cdot U_{i}=V\cdot W_{i^{\prime}}^{\prime}\cdot W_{i^{\prime},k,i}^{\prime}\cdot W_{i^{\prime},k,i}=V\cdot W_{i^{\prime}}^{\prime}\cdot W_{i^{\prime}}=V\cdot W=U$.

• •

If $U=V\parallel W$, then there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, and $f=\gamma_{\Sigma}(e^{*},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\cdot e^{*}$. In this case, we choose $I=\{*\}$, and $J_{*}=\emptyset$ and $U_{*}=U$ to find that the claims are validated. ∎

4.3 Trace construction

In the above, we learned how to deconstruct traces in the syntactic PA. To verify that the state in the syntactic PA associated with a series-rational expression $e$ indeed accepts the series-rational pomset language \left\ldbrack e\right\rdbrack, we also need to show the converse, that is, how to construct traces in the syntactic PA from smaller traces. In this context it is often useful to work with the preorder obtained from $\simeq$.

Definition \thedefinition.

The relation $\lesssim\ \subseteq{\mathcal{T}_{\Sigma}}\times{\mathcal{T}_{\Sigma}}$ is defined by $e\lesssim f$ if and only if $e+f\simeq f$.

The intuition to $e\lesssim f$ is that $e$ consists of one or more terms that also appear in $f$, up to $\simeq$.

In analogy to Lemma 4.1, we show that $\lesssim$ is a “simulation” with respect to traces.

Lemma \thelemma.

Let $e,e^{\prime},f\in{\mathcal{T}_{\Sigma}}$ be such that $e\lesssim f$. If e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}e^{\prime}, then there exists an $f^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} and $e^{\prime}\lesssim f^{\prime}$. Furthermore, if $e\in F_{\Sigma}$, then $f\in F_{\Sigma}$.

Proof.

We prove the first claim by induction on $U$. In the base, $U=a\in\Sigma$ and $e^{\prime}=\delta_{\Sigma}(e,a)$. Note that $\delta_{\Sigma}(e,a)+\delta_{\Sigma}(f,a)=\delta_{\Sigma}(e+f,a)\simeq\delta_{\Sigma}(f,a)$ by Lemma 4.1. We choose $f^{\prime}=\delta_{\Sigma}(f,a)$ to find that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} with $e^{\prime}=\delta_{\Sigma}(e,a)\lesssim\delta_{\Sigma}(f,a)=f^{\prime}$.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, then there exists an $e^{\prime\prime}$ such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}e^{\prime\prime} and e^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}e^{\prime}. By induction, we find an $f^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f^{\prime\prime} and $e^{\prime\prime}\lesssim f^{\prime\prime}$, and again by induction we find an $f^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that f^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f^{\prime} with $e^{\prime}\lesssim f^{\prime}$. In total, we know that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $e^{\prime}\lesssim f^{\prime}$.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, then there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime} and $e^{\prime}=\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. Note that $\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})+\gamma_{\Sigma}(f,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=\gamma_{\Sigma}(e+f,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\simeq\gamma_{\Sigma}(f,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$ by Lemma 4.1. We choose $f^{\prime}=\gamma_{\Sigma}(f,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$ to find that f\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} with $e^{\prime}=\gamma_{\Sigma}(e,\phi)\lesssim\gamma_{\Sigma}(f,\phi)=f^{\prime}$.

For the second claim, suppose that $e\in F_{\Sigma}$, then also $e+f\in F_{\Sigma}$. But then $f\in F_{\Sigma}$ by Lemma 4.1. ∎

The following lemma tells us that we can create a trace labelled with the concatenation of the labels of two smaller traces, and starting in the sequential composition of the original starting states, provided that the first trace ends in an accepting state. Furthermore, the target state of the newly constructed trace contains the target state of the second trace. We also prove two auxiliary claims towards this end, which will be useful later on.

Lemma \thelemma.

Let $e_{1},e_{2},f_{1},f_{2}\in{\mathcal{T}_{\Sigma}}$ and $U,V\in\mathsf{Pom}_{\Sigma}^{+}$ be such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f_{2}. The following hold:

• •

There exists an $f\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\cdot e_{2}\lesssim f$.

• •

If $f_{1}\in F_{\Sigma}$, then there exists an $f\in{\mathcal{T}_{\Sigma}}$ such that f_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f with $f_{2}\lesssim f$.

• •

If $f_{1}\in F_{\Sigma}$, then there exists an $f\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U\cdot V}}}_{\Sigma}f with $f_{2}\lesssim f$.

Proof.

The proof of the first claim proceeds by induction on $U$. In the base, $U=a\in\Sigma$ and $f_{1}=\delta_{\Sigma}(e_{1},a)$. We choose $f=\delta_{\Sigma}(e_{1}\cdot e_{2},a)$. It is now easy to show that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\cdot e_{2}\lesssim f$.

For the inductive step, there are two cases to consider.

• •

If $U=W\cdot X$ with $W$ and $X$ smaller than $U$, there exists a $g_{1}$ such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g_{1} and g_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{X}}}_{\Sigma}f_{1}. By induction, we obtain $g\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g with $g_{1}\cdot e_{2}\lesssim g$. Again by induction, we find $h\in{\mathcal{T}_{\Sigma}}$ such that g_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{X}}}_{\Sigma}h with $f_{1}\cdot e_{2}\lesssim h$. By Lemma 4.3, we then know that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f for some $f$ with $h\lesssim f$. In total, we find that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\cdot e_{2}\lesssim f$ (by transitivity of $\lesssim$).

• •

If $U=W\parallel X$ with $W$ and $X$ smaller than $U$, there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g^{\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{X}}}_{\Sigma}h^{\prime}, and $f_{1}=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. We choose $f=\gamma_{\Sigma}(e_{1}\cdot e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. It is now easy to show that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\cdot e_{2}\lesssim f$.

The proof of the second claim proceeds by induction on $V$. In the base, $V=a\in\Sigma$ and $f_{2}=\delta_{\Sigma}(e_{2},a)$. We can then choose $f=\delta_{\Sigma}(f_{1}\cdot e_{2},a)$. It is now easy to show that f_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f with $f_{2}\lesssim f$.

For the inductive step, there are two cases to consider.

• •

If $V=W\cdot X$ with $W$ and $X$ smaller than $V$, there exists a $g_{2}\in{\mathcal{T}_{\Sigma}}$ such that e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g_{2} and g_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{X}}}_{\Sigma}f_{2}. By induction, there exists a $g\in{\mathcal{T}_{\Sigma}}$ such that f_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g with $g_{2}\lesssim g$. By Lemma 4.3, we find $f$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{X}}}_{\Sigma}f with $f_{2}\lesssim f$, and thus f_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f.

• •

If $V=W\parallel X$ with $W$ and $X$ smaller than $V$, there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}g^{\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{X}}}_{\Sigma}h^{\prime} and $f_{2}=\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. We can then choose $f=\gamma_{\Sigma}(f_{1}\cdot e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. It is now easy to show that f_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f with $f_{2}\lesssim f$.

The third claim is a direct consequence of the first two claims and Lemma 4.3. ∎

We can also construct traces that start in a parallel composition. One way is to construct traces that start in each operand and reach an accepting state; we obtain a trace in their parallel composition almost trivially. If one of the operands is accepting, we can also construct a single trace that starts in the other operand and obtain a trace with the same label starting in the parallel construction. In both cases, we describe the target of the new trace using $\lesssim$.

Lemma \thelemma.

Let $e_{1},e_{2}\in{\mathcal{T}_{\Sigma}}$. The following hold:

• •

If $f_{1},f_{2}\in F_{\Sigma}$ and $U,V\in\mathsf{Pom}_{\Sigma}^{+}$ are such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f_{2}, then there exists an $f\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U\parallel V}}}_{\Sigma}f with $1\lesssim f$.

• •

If $e_{2}\in F_{\Sigma}$ (respectively $e_{1}\in F_{\Sigma}$), and $f^{\prime}\in{\mathcal{T}_{\Sigma}}$ and $U\in\mathsf{Pom}_{\Sigma}^{+}$ are such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} (respectively e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime}), then there exists an $f\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f^{\prime}\lesssim f$.

Proof.

For the first claim, choose $f=\gamma_{\Sigma}(e_{1}\parallel e_{2},\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\})$. We then immediately find that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U\parallel V}}}_{\Sigma}f with $1\lesssim f$.

For the second claim, the proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$ and $f_{1}=\delta_{\Sigma}(e_{1},a)$. Choose $f=\delta_{\Sigma}(e_{1}\parallel e_{2},a)$. It is then easy to see that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\lesssim f$.

In the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, there exists a $g_{1}$ such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g_{1} and g_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f_{1}. By induction, we find $g\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g with $g_{1}\lesssim g$. By Lemma 4.3, we find $f\in{\mathcal{T}_{\Sigma}}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f and $f_{1}\lesssim f$. In total, we have that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\lesssim f$.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, and $f_{1}=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. We choose $f=\gamma_{\Sigma}(e_{1}\parallel e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. It is now easy to see that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\lesssim f$. ∎

Lastly, we present a trace construction lemma to obtain traces originating in expressions of the form $e^{*}$. The idea here is that, given a finite number of traces that originate in $e$, where all (but possibly one) have an accepting state as their target, we can construct a trace originating in $e^{*}$, with a concatenation of the labels of the input traces as its label.

Lemma \thelemma.

Let $e,f_{1},f_{2},\dots,f_{n}\in{\mathcal{T}_{\Sigma}}$ (with $n>0$) be such that $f_{1},f_{2},\dots,f_{n-1}\in F_{\Sigma}$. Also, let $U,U_{1},U_{2},\dots,U_{n}\in\mathsf{Pom}_{\Sigma}^{+}$ be such that $U=U_{1}\cdot U_{2}\cdots U_{n}$. If for all $i\leq n$ it holds that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i}, then there exists an $f\in{\mathcal{T}_{\Sigma}}$ such that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f, with $f_{n}\cdot e^{*}\lesssim f$.

Proof.

First, we show that the claim holds for $n=1$, i.e., if $e,f_{1}\in{\mathcal{T}_{\Sigma}}$ and $U\in\mathsf{Pom}_{\Sigma}^{+}$ are such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1}, then there exists an $f\in{\mathcal{T}_{\Sigma}}$ such that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f, with $f_{1}\cdot e^{*}\lesssim f$. The proof proceeds by induction on $U$. In the base, $U=a\in\Sigma$ and $f_{1}=\delta_{\Sigma}(e,a)$. We choose $f=\delta_{\Sigma}(e^{*},a)=\delta_{\Sigma}(e,a)\cdot e^{*}=f_{1}\cdot e^{*}$ to find that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\cdot e^{*}\lesssim f$.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, there exists a $g_{1}\in{\mathcal{T}_{\Sigma}}$ such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g_{1} and g_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f_{1}. By induction, we find $g\in{\mathcal{T}_{\Sigma}}$ such that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g with $g_{1}\cdot e^{*}\lesssim g$. By Lemma 4.3, we find $h\in{\mathcal{T}_{\Sigma}}$ such that g_{1}\cdot e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h, with $f_{1}\cdot e^{*}\lesssim h$. By Lemma 4.3, we find $f$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f with $h\lesssim f$. In total, we have that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\cdot e^{*}\lesssim f$.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime}, and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, and $f_{1}=\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. In this case, we choose $f=\gamma_{\Sigma}(e^{*},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$ to find that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\cdot e^{*}\lesssim f$.

We now inductively extend the claim to all $n>0$, using the proof above as our base. In the inductive step, we assume the claim holds for $n-1$, and try to prove it for $n$. Let $U^{\prime}=U_{1}\cdot U_{2}\cdots U_{n-1}$. By induction, we obtain $g\in{\mathcal{T}_{\Sigma}}$ such that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U^{\prime}}}}_{\Sigma}g with $f_{n-1}\cdot e^{*}\lesssim g$. Furthermore, by the previous observation, we find $h\in{\mathcal{T}_{\Sigma}}$ such that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{n}}}}_{\Sigma}h with $f_{n}\cdot e^{*}\lesssim h$. By Lemma 4.3 and the fact that $f_{n-1}\in F_{\Sigma}$, we find $d\in{\mathcal{T}_{\Sigma}}$ such that f_{n-1}\cdot e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{n}}}}_{\Sigma}d with $h\lesssim d$. By the fact that $f_{n-1}\cdot e^{*}\lesssim g$ and f_{n-1}\cdot e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{n}}}}_{\Sigma}d, we find $f\in{\mathcal{T}_{\Sigma}}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{n}}}}_{\Sigma}f with $d\lesssim f$. In total, we have that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{n}\cdot e^{*}\lesssim h\lesssim d\lesssim f$. ∎

4.4 Soundness for the syntactic PA

With trace deconstruction and construction lemmas in our toolbox, we are ready to show that the syntactic PA indeed captures series-rational languages.

First, note that $L_{\Sigma}$ can be seen as a function from ${\mathcal{T}_{\Sigma}}$ to $\mathsf{Pom}_{\Sigma}$, like \left\ldbrack-\right\rdbrack. To establish equality between $L_{\Sigma}$ and \left\ldbrack-\right\rdbrack, we first show that $L_{\Sigma}$ enjoys the same homomorphic equalities as those in the definition of the semantic map, i.e., that $L_{\Sigma}(e)$ can be expressed in terms of $L_{\Sigma}$ applied to subexpressions of $e$. The proofs of the equalities below follow a similar pattern: for the inclusion from left to right we use trace deconstruction lemmas to obtain traces for the component expressions, while for the inclusion from right to left we use trace construction lemmas to build traces for the composed expressions given the traces of the component expressions. We treat the case for the empty pomset separately almost everywhere.

Lemma \thelemma.

Let $e_{1},e_{2}\in{\mathcal{T}_{\Sigma}}$, and $a\in\Sigma$. The following equalities hold:

[TABLE]

Proof.

For (1), suppose that $U\in L_{\Sigma}(0)$. Then there exists an $f\in F_{\Sigma}$ such that 0\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{\Sigma}f. Since $0\not\in F_{\Sigma}$, we know that $f\neq 0$, and so 0\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f must hold. But then, by Lemma 4.2 we know that $f=0$, which is a contradiction. We conclude that $L_{\Sigma}(0)=\emptyset$.

For (2), suppose that $U\in L_{\Sigma}(1)$. Then there exists an $f\in F_{\Sigma}$ such that 1\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{\Sigma}f. Then either $f=1$ and $U=1$, or $U\in\mathsf{Pom}_{\Sigma}^{+}$ and 1\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f. The former case is possible (since $1\in F_{\Sigma}$), but in the latter case we find that $f=0$ by Lemma 4.2, and so $f\not\in F_{\Sigma}$ — a contradiction. In conclusion, we find that $U=1$, and thus $U\in\{1\}$. The other inclusion is easy: simply observe that 1\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{1}\mkern-14.0mu\rightarrow}}_{\Sigma}1 by definition of $\mathrel{\rightarrow\mkern-14.0mu}\rightarrow_{\Sigma}$, implying that $1\in L_{\Sigma}(1)$.

For (3), suppose that $U\in L_{\Sigma}(a)$. Then there exists an $f\in F_{\Sigma}$ such that a\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{\Sigma}f. Then either $f=a$ and $U=1$, or $U\in\mathsf{Pom}_{\Sigma}^{+}$ and a\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f. We can rule out the former case, as it implies that $f=a\in F_{\Sigma}$ — a contradiction. In the latter case, we find by Lemma 4.2 that either $U=a$ and $f=1$, or $f=0$. Since the latter again contradicts that $f\in F_{\Sigma}$, we find that $U=a$; we thus conclude that $U\in\{a\}$. The other inclusion is easy: simply observe that a\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{a}}}_{\Sigma}1 by definition of $\mathrel{\rightarrow}_{\Sigma}$, and thus a\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{a}\mkern-14.0mu\rightarrow}}_{\Sigma}1, implying that $a\in L_{\Sigma}(a)$.

For (4), suppose that $U\in L_{\Sigma}(e_{1}+e_{2})$. Then there exists an $f\in F_{\Sigma}$ such that e_{1}+e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{\Sigma}f. If $f=e_{1}+e_{2}$ and $U=1$, then either $e_{1}\in F_{\Sigma}$ or $e_{2}\in F_{\Sigma}$. In either case, it follows quite easily that $U\in L_{\Sigma}(e_{1})\cup L_{\Sigma}(e_{2})$. Otherwise, e_{1}+e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f. But then, by Lemma 4.2, we know that $f=f_{1}+f_{2}$, such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{2}. Since $f\in F_{\Sigma}$, either $f_{1}\in F_{\Sigma}$ or $f_{2}\in F_{\Sigma}$, and therefore $U\in L_{\Sigma}(e_{1})$ or $U\in L_{\Sigma}(e_{2})$; either way, $U\in L_{\Sigma}(e_{1})\cup L_{\Sigma}(e_{2})$.

To prove the other inclusion, suppose that $U\in L_{\Sigma}(e_{1})\cup L_{\Sigma}(e_{2})$. If $U\in L_{\Sigma}(e_{1})$, then there exists an $f_{1}\in F_{\Sigma}$ such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{\Sigma}f_{1}. If $U=1$ and $f_{1}=e_{1}$, then $e_{1}\in F_{\Sigma}$ and therefore $e_{1}+e_{2}\in F_{\Sigma}$; it follows that $U\in L_{\Sigma}(e_{1}+e_{2})$. Otherwise, e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1}, and so by Lemma 4.3 and the fact that $e_{1}\lesssim e_{1}+e_{2}$ we find $f\in{\mathcal{T}_{\Sigma}}$ such that e_{1}+e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{1}\lesssim f_{2}$. By Lemma 4.3, $f\in F_{\Sigma}$, and so it follows that $U\in L_{\Sigma}(e_{1}+e_{2})$. The case where $U\in L_{\Sigma}(e_{2})$ is similar.

For (5), suppose that $U\in L_{\Sigma}(e_{1}\cdot e_{2})$. Then there exists an $f\in F_{\Sigma}$ such that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{\Sigma}f. If $U=1$ and $f=e_{1}\cdot e_{2}$, then $e_{1}\cdot e_{2}\in F_{\Sigma}$, and thus $e_{1},e_{2}\in F_{\Sigma}$. Therefore $1\in L_{\Sigma}(e_{1})$ and $1\in L_{\Sigma}(e_{2})$, implying that $1=1\cdot 1\in L_{\Sigma}(e_{1})\cdot L_{\Sigma}(e_{2})$. Otherwise, e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f. Then, by Lemma 4.2, there exists an $f^{\prime}\in{\mathcal{T}_{\Sigma}}$ and a finite set $I$, as well as $I$-indexed families ${(f_{i}^{\prime})}_{i\in I}$ over $F_{\Sigma}$ and ${(f_{i})}_{i\in I}$ over ${\mathcal{T}_{\Sigma}}$ and ${(U_{i}^{\prime})}_{i\in I}$ over $\mathsf{Pom}_{\Sigma}$ and ${(U_{i})}_{i\in I}$ over ${\mathcal{T}_{\Sigma}}$, such that:

• •

$f\simeq f^{\prime}\cdot e_{2}+\sum_{i\in I}f_{i}$, e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime}

• •

for all $i\in I$, e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}^{\prime}}}}_{\Sigma}f_{i}^{\prime}, e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i} and $U=U_{i}^{\prime}\cdot U_{i}$.

Since $f\in F_{\Sigma}$, also $f^{\prime}\cdot e_{2}+\sum_{i\in I}f_{i}\in F_{\Sigma}$ by Lemma 4.1. This means that either $f^{\prime}\cdot e_{2}\in F_{\Sigma}$, or $f_{i}\in F_{\Sigma}$ for some $i\in I$. In the former case, $f^{\prime},e_{2}\in F_{\Sigma}$, and therefore $U\in L_{\Sigma}(e_{1})$ and $1\in L_{\Sigma}(e_{2})$, thus $U=U\cdot 1\in L_{\Sigma}(e_{1})\cdot L_{\Sigma}(e_{2})$. In the latter case, $U_{i}^{\prime}\in L_{\Sigma}(e_{1})$ and $U_{i}\in L_{\Sigma}(e_{2})$, thus $U=U_{i}^{\prime}\cdot U_{i}\in L_{\Sigma}(e_{1})\cdot L_{\Sigma}(e_{2})$.

To prove the other inclusion, suppose that $U\in L_{\Sigma}(e_{1})\cdot L_{\Sigma}(e_{2})$. Then $U=U_{1}\cdot U_{2}$, with $U_{1}\in L_{\Sigma}(e_{1})$ and $U_{2}\in L_{\Sigma}(e_{2})$. There are four cases to consider.

• •

If $U_{1}=1$ and $U_{2}=1$, then $e_{1},e_{2}\in F_{\Sigma}$, and therefore $e_{1}\cdot e_{2}\in F_{\Sigma}$. Thus $1\in L_{\Sigma}(e_{1}\cdot e_{2})$.

• •

If $U_{1}=1$ and $U_{2}\neq 1$, then $e_{1}\in F_{\Sigma}$ and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{2}}}}_{\Sigma}f_{2} for some $f_{2}\in F_{\Sigma}$. Then, by Lemma 4.3, e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{2}}}}_{\Sigma}f for some $f\in{\mathcal{T}_{\Sigma}}$ with $f_{2}\lesssim f$. By Lemma 4.3, $f\in F_{\Sigma}$, and thus $U=U_{2}\in L_{\Sigma}(e_{1}\cdot e_{2})$.

• •

If $U_{1}\neq 1$ and $U_{2}=1$, then e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{1}}}}_{\Sigma}f_{1} for some $f_{1}\in F_{\Sigma}$, and $e_{2}\in F_{\Sigma}$. Then, by Lemma 4.3, e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{1}}}}_{\Sigma}f for some $f\in{\mathcal{T}_{\Sigma}}$ with $f_{1}\cdot e_{2}\lesssim f$. Since $f_{1},e_{2}\in F_{\Sigma}$, also $f_{1}\cdot e_{2}\in F_{\Sigma}$, and thus by Lemma 4.3, $f\in F_{\Sigma}$. Therefore $U=U_{1}\in L_{\Sigma}(e_{1}\cdot e_{2})$.

• •

If $U_{1}\neq 1$ and $U_{2}\neq 1$, then e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{1}}}}_{\Sigma}f_{1} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{2}}}}_{\Sigma}f_{2} for some $f_{1},f_{2}\in F_{\Sigma}$. Then, by Lemma 4.3, we find that e_{1}\cdot e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{2}\lesssim f$. By Lemma 4.3, $f\in F_{\Sigma}$, and thus $U\in L_{\Sigma}(e_{1}\cdot e_{2})$.

For (6), suppose that $U\in L_{\Sigma}(e_{1}\parallel e_{2})$. Then there exists an $f\in F_{\Sigma}$ such that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{\Sigma}f. If $f=e_{1}\parallel e_{2}$ and $U=1$, then $e_{1},e_{2}\in F_{\Sigma}$, and thus $1\in L_{\Sigma}(e_{1})$ and $1\in L_{\Sigma}(e_{2})$. But then $1=1\parallel 1\in L_{\Sigma}(e_{1})\parallel L_{\Sigma}(e_{2})$. Otherwise, e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f for some $f\in F_{\Sigma}$. By Lemma 4.2, we obtain $f_{1},f_{2},f_{3}\in F_{\Sigma}$ such that

• •

$f\simeq f_{1}+f_{2}+f_{3}$

• •

either $f_{1}=0$, or $e_{2}\in F_{\Sigma}$ and e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1}

• •

either $f_{2}=0$, or $e_{1}\in F_{\Sigma}$ and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{2}

• •

either $f_{3}=0$, or $f_{3}=1$ and there exist $e_{1}^{\prime},e_{2}^{\prime}\in{\mathcal{T}_{\Sigma}}$ and $f_{1}^{\prime},f_{2}^{\prime}\in F_{\Sigma}$ and $U_{1},U_{2}\in\mathsf{Pom}_{\Sigma}^{+}$ such that $e_{1}\simeq e_{1}^{\prime}$ and $e_{2}\simeq e_{2}^{\prime}$ and $U=U_{1}\parallel U_{2}$ and e_{1}^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{1}}}}_{\Sigma}f_{1}^{\prime} and e_{2}^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{2}}}}_{\Sigma}f_{2}^{\prime}.

By Lemma 4.3, $f_{1}+f_{2}+f_{3}\in F_{\Sigma}$, and thus $f_{1}\in F_{\Sigma}$ or $f_{2}\in F_{\Sigma}$ or $f_{3}\in F_{\Sigma}$. In the first case, $U\in L_{\Sigma}(e_{1})$ and $1\in L_{\Sigma}(e_{2})$, and therefore $U=U\parallel 1\in L_{\Sigma}(e_{1})\parallel L_{\Sigma}(e_{2})$. In the second case, we similarly find that $U\in L_{\Sigma}(e_{1})\parallel L_{\Sigma}(e_{2})$. In the last case, we find by Lemma 4.1 and Lemma 4.1 $f_{1}^{\prime\prime},f_{2}^{\prime\prime}\in F_{\Sigma}$ such that e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{1}^{\prime\prime} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f_{2}^{\prime\prime}, and thus we have that $U=U_{1}\parallel U_{2}$ such that $U_{1}\in L_{\Sigma}(e_{1})$ and $U_{2}\in L_{\Sigma}(e_{2})$, therefore $U\in L_{\Sigma}(e_{1})\parallel L_{\Sigma}(e_{2})$.

To prove the other inclusion, suppose that $U\in L_{\Sigma}(e_{1})\parallel L_{\Sigma}(e_{2})$. Then $U=U_{1}\parallel U_{2}$. There are four cases to consider.

• •

If $U_{1}=1$ and $U_{2}=1$, then $e_{1},e_{2}\in F_{\Sigma}$, thus $e_{1}\parallel e_{2}\in F_{\Sigma}$. But then $U=1\in L_{\Sigma}(e_{1}\parallel e_{2})$.

• •

If $U_{1}=1$ and $U_{2}\neq 1$, then e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{2}}}}_{\Sigma}f_{2} for some $f_{2}\in F_{\Sigma}$. By Lemma 4.3, we find an $f\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{2}\lesssim f$. But then, by Lemma 4.3, $f\in F_{\Sigma}$, and thus $U\in L_{\Sigma}(e_{1}\parallel e_{2})$.

• •

If $U_{1}\neq 1$ and $U_{2}=1$, then we find that $U\in L_{\Sigma}(e_{1}\parallel e_{2})$ by an argument similar to the above case.

• •

If $U_{1}\neq 1$ and $U_{2}\neq 1$, then e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{1}}}}_{\Sigma}f_{1} and e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{2}}}}_{\Sigma}f_{2} for some $f_{1},f_{2}\in F_{\Sigma}$. By Lemma 4.3, we find an $f\in{\mathcal{T}_{\Sigma}}$ such that e_{1}\parallel e_{2}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $1\lesssim f$. But then, by Lemma 4.3, $f\in F_{\Sigma}$, and thus $U\in L_{\Sigma}(e_{1}\parallel e_{2})$.

For (7), suppose that $U\in L_{\Sigma}(e_{1}^{*})$. Then there exists an $f\in F_{\Sigma}$ such that e_{1}^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}\mkern-14.0mu\rightarrow}}_{\Sigma}f. If $f=e_{1}^{*}$ and $U=1$, then $1\in{L_{\Sigma}(e_{1})}^{*}$. Otherwise, e_{1}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f. By Lemma 4.2, we find a finite set $I$ and an $I$-indexed family of finite sets ${(J_{i})}_{i\in I}$ as well as $I$-indexed families ${(f_{i})}_{i\in I}$ over ${\mathcal{T}_{\Sigma}}$ and ${(U_{i})}_{i\in I}$ over $\mathsf{Pom}_{\Sigma}^{+}$, and for all $i\in I$ also $J_{i}$-indexed families ${(f_{i,j})}_{j\in J_{i}}$ over ${\mathcal{T}_{\Sigma}}$ and ${(U_{i,j})}_{j\in J_{i}}$ over $\mathsf{Pom}_{\Sigma}^{+}$, such that $f\simeq\sum_{i\in I}f_{i}\cdot e^{*}$, and for all $i\in I$

• •

e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i}

• •

for all $j\in J_{i}$ we have that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i,j}}}}_{\Sigma}f_{i,j}

• •

$U=U_{i}^{\prime}\cdot U_{i}$, where $U_{i}^{\prime}$ is some concatenation of all $U_{i,j}$ for all $j\in J_{i}$.

By Lemma 4.3, we know that $\sum_{i\in I}f_{i}\cdot e^{*}\in F_{\Sigma}$, and thus $f_{i}\cdot e^{*}\in F_{\Sigma}$ for some $i\in I$, meaning in particular that $f_{i}\in F_{\Sigma}$ for this $i\in I$. Now $U_{i,j}\in L_{\Sigma}(e)$ for all $j\in J$, and thus $U_{i}^{\prime}\in{L_{\Sigma}(e)}^{*}$. Since also $U_{i}\in L_{\Sigma}(e)$, we find that $U=U_{i}^{\prime}\cdot U_{i}\in{L_{\Sigma}(e)}^{*}\cdot L_{\Sigma}(e)\subseteq{L_{\Sigma}(e)}^{*}$.

To prove the other inclusion, suppose that $U\in{L_{\Sigma}(e)}^{*}$. Then $U\in{L_{\Sigma}(e)}^{n}$, i.e., $U=U_{1}\cdot U_{2}\cdots U_{n}$, such that for all $1\leq i\leq n$ we have $U_{i}\in L_{\Sigma}(e)$. Assume (without loss of generality) that $U_{i}\neq 1$ for all $1\leq i\leq n$. If $n=0$, then $U=1$ and we find that $U\in L_{\Sigma}(e^{*})$ immediately. Otherwise, there exist $f_{1},f_{2},\dots,f_{n}\in F_{\Sigma}$ such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{i}}}}_{\Sigma}f_{i}. By Lemma 4.3 we find $f\in{\mathcal{T}_{\Sigma}}$ such that e^{*}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f with $f_{n}\lesssim f$. But then $f\in F_{\Sigma}$ by Lemma 4.3, and thus $U\in L_{\Sigma}(e^{*})$. ∎

It is now easy to establish that the Brzozowski construction for the syntactic PA is sound with respect to the denotational semantics of series-rational expressions.

Theorem 4.1**.**

Let $e\in{\mathcal{T}_{\Sigma}}$. Then L_{\Sigma}(e)=\left\ldbrack e\right\rdbrack.

Proof.

The proof proceeds by induction on $e$. In the base, $e=0$, $e=1$ or $e=a$ for some $a\in\Sigma$. In all cases, L_{\Sigma}(e)=\left\ldbrack e\right\rdbrack by Lemma 4.4. For the inductive step, there are four cases to consider: either $e=e_{1}+e_{2}$, $e=e_{1}\cdot e_{2}$, $e=e_{1}\parallel e_{2}$ or $e=e_{1}^{*}$. In all cases, the claim follows from the induction hypothesis and the definition of \left\ldbrack-\right\rdbrack, combined with Lemma 4.4. ∎

4.5 Bounding the syntactic PA

Ideally, we would like to obtain a single PA with finitely many states that recognizes \left\ldbrack e\right\rdbrack for a given $e\in{\mathcal{T}_{\Sigma}}$. Unfortunately, the syntactic PA is not bounded, and thus Theorem 3.1 does not apply. For instance, the requirement that $\rho_{\Sigma}(e)$ be finite for $e\in{\mathcal{T}_{\Sigma}}$ fails; consider the family of distinct terms ${(e_{n})}_{n\in\mathbb{N}}$ defined by $e_{0}=1\cdot a^{*}$ and $e_{n+1}=0\cdot a^{*}+e_{n}$ for $n\in\mathbb{N}$; it is not hard to show that $e_{n}\in\rho_{\Sigma}(a^{*})$ for $n\in\mathbb{N}$, and thus conclude that $\rho_{\Sigma}(a^{*})$ is infinite. We remedy this problem by quotienting the state space of the syntactic PA by congruence.

In what follows, we write $[e]$ for the congruence class of $e\in{\mathcal{T}_{\Sigma}}$ modulo $\simeq$, i.e., the set of all $e^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that $e\simeq e^{\prime}$. We furthermore write ${\mathcal{Q}_{\Sigma}}$ for the set of all congruence classes of expressions in ${\mathcal{T}_{\Sigma}}$. We now leverage Lemma 4.1 to define a transition structure on ${\mathcal{Q}_{\Sigma}}$.

Definition \thedefinition.

We define $\delta_{\simeq}:{\mathcal{Q}_{\Sigma}}\times\Sigma\to{\mathcal{Q}_{\Sigma}}$ and $\gamma_{\simeq}:{\mathcal{Q}_{\Sigma}}\times\binom{{\mathcal{Q}_{\Sigma}}}{2}\to{\mathcal{Q}_{\Sigma}}$ as {mathpar} δ_≃([e], a) = [δΣ(e, a)] γ≃([e], {|[f], [g]|}) = {[0] f ≃0 or g ≃0[γΣ(e, {|g, h|})] otherwise

Furthermore, the set $F_{\simeq}$ is defined to be $\{[e]:e\in F_{\Sigma}\}$. The quotiented syntactic PA is the PA $A_{\simeq}=\left\langle{\mathcal{Q}_{\Sigma}},\delta_{\simeq},\gamma_{\simeq},F_{\simeq}\right\rangle$.

Note that, by virtue of Lemma 4.1 and Lemma 4.1, we have that $\delta_{\simeq}$ and $\gamma_{\simeq}$, as well as $F_{\simeq}$, are well-defined. As before, we abbreviate subscripts, for example by writing $\mathrel{\rightarrow}_{\simeq}$ rather than $\mathrel{\rightarrow}_{A_{\simeq}}$, and $L_{\simeq}$ rather than $L_{A_{\simeq}}$. Of course, we also want the quotiented syntactic PA to accept the same languages as the syntactic PA. To that end, we show that the trace relations of the syntactic PA and the quotiented syntactic PA correspond.

Lemma \thelemma.

Let $e,f\in{\mathcal{T}_{\Sigma}}$ and $U\in\mathsf{Pom}_{\Sigma}^{+}$. If e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f, then [e]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\simeq}[f]. If [e]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\simeq}[f], then there exists an $f\in{\mathcal{T}_{\Sigma}}$ with $f\simeq f^{\prime}$ and e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime}.

Proof.

Refer to Appendix A. ∎

Theorem 4.2**.**

Let $e\in{\mathcal{T}_{\Sigma}}$. Then $L_{\Sigma}(e)=L_{\simeq}([e])$.

Proof.

By definition, $e\in F_{\Sigma}$ if and only if $[e]\in F_{\simeq}$. It then follows that $1\in L_{\Sigma}(e)$ if and only if $1\in L_{\simeq}([e])$. The remaining cases are covered by Lemma 4.5. ∎

Corollary \thecorollary.

The state $[0]$ is the only state in the quotiented syntactic PA with an empty language.

Proof.

Let $[e]\in{\mathcal{Q}_{\Sigma}}$ be a state such that $L_{\simeq}([e])=\emptyset$. Then, by Theorem 4.2, we know that $L_{\Sigma}(e)=\emptyset$, and by Theorem 4.1, \left\ldbrack e\right\rdbrack=\emptyset. But then $e\simeq 0$ by Lemma 2.4, and thus $[e]=[0]$. ∎

We now show that the quotiented syntactic PA is bounded. First, we need the following.

Definition \thedefinition.

Let $e\in{\mathcal{T}_{\Sigma}}$. The parallel depth of $e$, denoted $0pt{e}$, is [math] when $e\simeq 0$, and otherwise: {mathpar} 0pt1 = 0 0pta = 1 0pte_1 + e_2 = max(0pte_1, 0pte_2)

0pte_1 ⋅e_2 = max(0pte_1, 0pte_2)0pte_1 ∥e_2 = max(0pte_1, 0pte_2) + 10pte_1^* = 0pte_1

It is easy to show that the parallel depth of an expression is also well-defined on the congruence classes of $\simeq$. This allows us to define a fork hierarchy on ${\mathcal{Q}_{\Sigma}}$.

Lemma \thelemma.

Let $e,e^{\prime}\in{\mathcal{T}_{\Sigma}}$ be such that $e\simeq e^{\prime}$. Then $0pt{e}=0pt{e^{\prime}}$.

Proof.

Refer to Appendix A. ∎

Definition \thedefinition.

The relation $\prec\ \subseteq{\mathcal{Q}_{\Sigma}}\times{\mathcal{Q}_{\Sigma}}$ is such that $[e]\prec[f]$ if and only if $0pt{e}<0pt{f}$.

Lemma \thelemma.

The quotiented syntactic PA is fork-acyclic, with fork hierarchy $\prec$.

Proof.

We need to show that $\prec$ satisfies the conditions of Definition 3.

For the first rule, we begin by showing that if $g,h,e\in{\mathcal{T}_{\Sigma}}$ such that $e,g,h\not\simeq 0$ and $\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$, then $0pt{g}<0pt{e}$. The proof proceeds by induction on $e$. In the base, $e=1$ or $e=a$; in both cases, $\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=0$ and so the claim holds vacuously. For the inductive step, there are four cases to consider.

• •

If $e=e_{1}+e_{2}$, then $\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})+\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$, thus $\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$ or $\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$. Therefore, by induction $0pt{g}<0pt{e_{1}}$ or $0pt{g}<0pt{e_{2}}$, and thus $0pt{g}<\max(0pt{e_{1}},0pt{e_{2}})=0pt{e}$.

• •

If $e=e_{1}\cdot e_{2}$, then $\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\cdot e_{2}+e_{1}\star\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$, thus $\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$ or $\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$. Therefore, by induction $0pt{g}<0pt{e_{1}}$ or $0pt{g}<0pt{e_{2}}$, and thus $0pt{g}<\max(0pt{e_{1}},0pt{e_{2}})=0pt{e}$.

• •

If $e=e_{1}\parallel e_{2}$, then $\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=[\{\mskip-4.0mu|g,h|\mskip-4.0mu\}=\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}]+e_{2}\star\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})+e_{1}\star\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$. If $[\{\mskip-4.0mu|g,h|\mskip-4.0mu\}=\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}]\not\simeq 0$, we know that $\{\mskip-4.0mu|g,h|\mskip-4.0mu\}=\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}$. Assume without loss of generality that $e_{1}=g$; then $0pt{g}=0pt{e_{1}}<\max(0pt{e_{1}},0pt{e_{2}})+1=0pt{e}$. If $\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$, then by induction $0pt{g}<0pt{e_{1}}<\max(0pt{e_{1}},0pt{e_{2}})+1$. The case where $\gamma_{\Sigma}(e_{2},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$ is similar.

• •

If $e=e_{1}^{*}$, then $\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})=\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\cdot e_{1}^{*}\not\simeq 0$ and therefore $\gamma_{\Sigma}(e_{1},\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$. But then $0pt{g}<0pt{e_{1}}=0pt{e}$ by induction.

To fully validate the first rule, suppose that $\{\mskip-4.0mu|[g],[h]|\mskip-4.0mu\}\in\pi_{\simeq}([e])$. Then $e,g,h\not\simeq 0$ and $\gamma_{\simeq}([e],\{\mskip-4.0mu|[g],[h]|\mskip-4.0mu\})\neq[0]$ and thus $\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})\not\simeq 0$. But then we find that $0pt{g}<0pt{e}$ by the above, and therefore $[g]\prec[e]$.

For the second rule, we first show that if $a\in\Sigma$ and $e\in{\mathcal{T}_{\Sigma}}$, then $0pt{\delta_{\Sigma}(e,a)}\leq 0pt{e}$. If $e\simeq 0$, then $0pt{\delta_{\Sigma}(e,a)}=0pt{\delta_{\Sigma}(0,a)}=0pt{0}=0\leq 0pt{0}=0pt{e}$. The proof of the remaining cases proceeds by induction on $e$. In the base, $e=1$ or $e=a$. In both cases, $0pt{\delta_{\Sigma}(e,a)}=0\leq 0pt{e}$.

For the inductive step, there are four cases to consider.

• •

If $e=e_{1}+e_{2}$, then we can derive

[TABLE]

• •

If $e=e_{1}\cdot e_{2}$, then we can derive

[TABLE]

• •

If $e=e_{1}\parallel e_{2}$, then we can derive

[TABLE]

• •

If $e=e_{1}^{*}$, then we can derive

[TABLE]

Thus, suppose that $[f]\prec\delta_{\simeq}([e],a)=[\delta_{\Sigma}(e,a)]$. Then $[f]\prec[e]$, since we can derive that $0pt{f}<0pt{\delta_{\Sigma}(e,a)}\leq 0pt{e}$.

For the third rule, one also first shows that for $e\in{\mathcal{T}_{\Sigma}}$ and $\phi\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ we have that $0pt{\gamma_{\Sigma}(e,\phi)}\leq 0pt{e}$. One can then extend this to show that if $[f]\prec\gamma_{\simeq}([e],\phi)$, also $[f]\prec[e]$ using the same technique as above. ∎

Finally, we investigate the reach and support of a state in the quotiented syntactic PA, using the deconstruction lemmas showed in Section 4.2, as well as Lemma 4.5.

Lemma \thelemma.

Let $e\in{\mathcal{T}_{\Sigma}}$. Then $\rho_{\simeq}([e])$ and $\pi_{\simeq}([e])$ are finite.

Proof.

We first claim that $R_{\Sigma}(e)$ is finite up to $\simeq$, i.e., that the set $\{[f]:f\in R_{\Sigma}(e)\}$ is finite. The proof of this claim proceeds by induction on $e$. In the base, there are three cases to consider.

• •

If $e=0$ and e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f, then $f=0$ by Lemma 4.2; it follows that $R_{\Sigma}(e)$ is finite.

• •

If $e=1$ and e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f, then $f=0$ by Lemma 4.2; it follows that $R_{\Sigma}(e)$ is finite.

• •

If $e=a$ for some $a\in\Sigma$, then $f=0$ or $f=1$ by Lemma 4.2. It follows that $R_{\Sigma}(e)$ is finite.

In all cases, we find that $R_{\Sigma}(e)$ is finite, and therefore finite up to $\simeq$.

For the inductive step, there are four cases to consider. In each case our strategy is to write an arbitrary element of $R_{\Sigma}(e)$ into a sum of a number of terms. If we can then show that there are only finitely many choices for each term up to $\simeq$, it follows that there are only finitely many such sums up to $\simeq$. Note that the number of terms does not matter, since repeated terms in a sum do not make a difference with respect to $\simeq$ by virtue of the idempotence rule.

• •

If $e=e_{1}+e_{2}$ and $f\in R_{\Sigma}(e)$, then by Lemma 4.2 there exist $f_{1}\in R_{\Sigma}(e_{1})$ and $f_{2}\in R_{\Sigma}(e_{2})$ such that $f\simeq f_{1}+f_{2}$. Since $R_{\Sigma}(e_{1})$ and $R_{\Sigma}(e_{2})$ are finite up to $\simeq$ by induction, it follows that $R_{\Sigma}(e)$ is finite up to $\simeq$.

• •

If $e=e_{1}\cdot e_{2}$ and $f\in R_{\Sigma}(e)$, then by Lemma 4.2 there exists an $f^{\prime}\in R_{\Sigma}(e_{1})\cup\{e_{1}\}$ and a finite set $I$ and an $I$-indexed set of terms ${(f_{i})}_{i\in I}\in R_{\Sigma}(e_{2})$ such that $f\simeq f^{\prime}\cdot e_{2}+\sum_{i\in I}f_{i}$. Since $R_{\Sigma}(e_{1})\cup\{e_{1}\}$ and $R_{\Sigma}(e_{2})$ are finite up to $\simeq$ by induction, it follows that $R_{\Sigma}(e)$ is finite up to $\simeq$.

• •

If $e=e_{1}\parallel e_{2}$ and $f\in R_{\Sigma}(e)$, then by Lemma 4.2 there exist $f_{1}\in R_{\Sigma}(e_{1})\cup\{0\}$, $f_{2}\in R_{\Sigma}(e_{2})\cup\{0\}$ and $f_{3}\in\{0,1\}$ such that $f\simeq f_{1}+f_{2}+f_{3}$. Since $R_{\Sigma}(e_{1})$ and $R_{\Sigma}(e_{2})$ are finite up to $\simeq$ by induction, it follows that $R_{\Sigma}(e)$ is finite up to $\simeq$.

• •

If $e=e_{1}^{*}$ and $f\in R_{\Sigma}(e)$, then by Lemma 4.2 there exists a finite set $I$ and an $I$-indexed family ${(f_{i})}_{i\in I}$ over $R_{\Sigma}(e_{1})$ such that $f\simeq\sum_{i\in I}f_{i}\cdot e^{*}$. Since $R_{\Sigma}(e_{1})$ is finite up to $\simeq$ by induction, it follows that $R_{\Sigma}(e)$ is finite up to $\simeq$.

Since $\rho_{\simeq}(e)\cup\{[0]\}=R_{\simeq}([e])\cup\{[e],[0]\}$ by Lemma 3 and Corollary 4.5, it suffices to show that $R_{\simeq}([e])$ is finite. This is an immediate consequence of Lemma 4.5 and the above.

We now treat the claim about $\pi_{\simeq}([e])$. First, we claim that there are finitely many $\phi\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ up to $\simeq$ such that $\gamma_{\Sigma}(e,\phi)\not\simeq 0$. This is shown by induction on $e$. In the base, $e=0$, $e=1$ or $e=a$; in all cases, we find that $\gamma_{\Sigma}(e,\phi)=0$ for $\phi\in\binom{{\mathcal{T}_{\Sigma}}}{2}$. For the inductive step, there are four cases; in each case, we apply Lemma 4.4.

• •

Suppose $e=e_{1}+e_{2}$. By induction, there are finitely many $\phi$ up to $\simeq$ such that $\gamma_{\Sigma}(e_{1},\phi)\not\simeq 0$ or $\gamma_{\Sigma}(e_{2},\phi)\not\simeq 0$. Thus, there are finitely many $\phi\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ up to $\simeq$ such that $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e_{1},\phi)+\gamma_{\Sigma}(e_{2},\phi)\not\simeq 0$.

• •

Suppose $e=e_{1}\cdot e_{2}$. By induction, there are finitely many $\phi$ up to $\simeq$ such that $\gamma_{\Sigma}(e_{1},\phi)\not\simeq 0$ or $\gamma_{\Sigma}(e_{2},\phi)\not\simeq 0$. Thus, there are finitely many $\phi\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ up to $\simeq$ such that $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e_{1},\phi)\cdot e_{2}+e_{1}\star\gamma_{\Sigma}(e_{2},\phi)\not\simeq 0$.

• •

Suppose $e=e_{1}\parallel e_{2}$. By induction, there are finitely many $\phi$ up to $\simeq$ such that $\gamma_{\Sigma}(e_{1},\phi)\not\simeq 0$ or $\gamma_{\Sigma}(e_{2},\phi)\not\simeq 0$. Furthermore, there is exactly one $\phi$ up to $\simeq$ such that $\phi\simeq\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}$. Thus, there are finitely many $\phi\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ up to $\simeq$ such that $\gamma_{\Sigma}(e,\phi)=[\phi\simeq\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}]+e_{2}\star\gamma_{\Sigma}(e_{1},\phi)+e_{1}\star\gamma_{\Sigma}(e_{2},\phi)\not\simeq 0$.

• •

Suppose $e=e_{1}^{*}$. By induction, there are finitely many $\phi$ up to $\simeq$ such that $\gamma_{\Sigma}(e_{1},\phi)\not\simeq 0$. Thus, there are finitely many $\phi\in\binom{{\mathcal{T}_{\Sigma}}}{2}$ up to $\simeq$ such that $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e_{1},\phi)\cdot e_{1}^{*}\not\simeq 0$.

The proof that that $\pi_{\simeq}([e])$ is finite, i.e., that there are finitely many $\phi\in\binom{{\mathcal{Q}_{\Sigma}}}{2}$ such that $\gamma_{\simeq}([e],\phi)\neq[0]$ is now an immediate consequence of the above. ∎

Theorem 4.3**.**

The quotiented syntactic PA is bounded.

Proof.

By Lemma 4.5, we know that $A_{\simeq}$ is fork-acyclic. Furthermore, $\prec$ is well-founded by construction: every term has finite depth. By Lemma 4.5, we know that $\rho_{\simeq}([e])$ and $\pi_{\simeq}([e])$ are finite for all $[e]\in{\mathcal{Q}_{\Sigma}}$. All requirements are now validated. ∎

The desired result then follows from the above, Lemma 3 and Theorem 3.1.

Corollary \thecorollary.

Let $e\in{\mathcal{T}_{\Sigma}}$. There exists a finite PA $A_{e}$ that accepts \left\ldbrack e\right\rdbrack.

Proof.

Consider the quotiented syntactic PA $A_{\simeq}$. By Theorem 4.2 and Theorem 4.1, we know that L_{\simeq}([e])=L_{\Sigma}(e)=\left\ldbrack e\right\rdbrack. By Theorem 4.3, $A_{\simeq}$ is bounded, and therefore (by Theorem 3.1) we can construct a finite and closed set $Q_{e}$ such that $[e]\in Q_{e}$. We now choose $A_{e}=A_{\simeq}\!\upharpoonright_{Q_{e}}$ and $q=[e]$ to find that L_{A_{e}}(q)=L_{\simeq}([e])=\left\ldbrack e\right\rdbrack by Lemma 3. ∎

5 Automata to expressions

To associate with every state $q$ in a bounded PA $A=\left\langle Q,\delta,\gamma,F\right\rangle$ a series-rational expression $e_{q}$ such that \left\ldbrack e_{q}\right\rdbrack=L_{A}(q), we modify the procedure for associating a rational expression with a state in a finite automaton described in [11]. The modification consists of adding parallel terms to the expression associated with $q$ whenever a fork in $q$ contributes to its language, i.e., whenever $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\pi_{A}(q)$.

In view of the special treatment of $1$ in the semantics of PAs, it is convenient to first define expressions $e_{q}^{+}$ with the property that \left\ldbrack e_{q}^{+}\right\rdbrack=L_{A}(q)-\{1\}; then we can define $e_{q}$ by $e_{q}=e_{q}^{+}+[q\in F]$. The definition of $e_{q}^{+}$ proceeds by induction on the well-founded partial order $\prec_{A}$ associated with a bounded PA. That is, when defining $e_{q}^{+}$ we assume the existence of expressions $e_{q^{\prime}}^{+}$ for all $q^{\prime}\in Q$ such that $q^{\prime}\prec_{A}q$.

First, however, we shall define auxiliary expressions $e^{Q^{\prime}}_{qq^{\prime}}$ for suitable choices of $Q^{\prime}\subseteq Q$ and of $q,q^{\prime}\in Q$. Intuitively, $e^{Q^{\prime}}_{qq^{\prime}}$ denotes the pomset language characterizing all paths from $q$ to $q^{\prime}$ with all intermediate states in $Q^{\prime}$; $e_{q}^{+}$ can then be defined as the summation of all $e^{\rho_{A}(q)}_{qq^{\prime}}$ with $q^{\prime}\in F\cap\rho_{A}(q)$.

Definition \thedefinition.

Let $Q^{\prime}$ be a finite subset of $Q$, and assume that for all $r\in Q$ such that $r\prec_{A}q$ for some $q\in Q^{\prime}$ there exists a series-rational expression $e_{r}^{+}\in{\mathcal{T}_{\Sigma}}$ such that \left\ldbrack e_{r}^{+}\right\rdbrack=L_{A}(q)-\{1\}. For all $Q^{\prime\prime}\subseteq Q^{\prime}$ and $q,q^{\prime}\in Q^{\prime}$, we define a series-rational expression $e^{Q^{\prime\prime}}_{qq^{\prime}}$ by induction on the size of $Q^{\prime\prime}$, as follows:

If $Q^{\prime\prime}=\emptyset$, then let $\widetilde{\Sigma}=\{a\in\Sigma:q^{\prime}=\delta(q,a)\}$, and let $\widetilde{Q}=\{\phi\in\pi_{A}(q):\gamma(q,\phi)=q^{\prime}\}$. We define

[TABLE] 2. 2.

Otherwise, we choose a $q^{\prime\prime}\in Q^{\prime\prime}$ and define

[TABLE]

Note that $e_{r}^{+}$ and $e_{s}^{+}$, appearing in the first clause of the definition of $e^{Q^{\prime\prime}}_{qq^{\prime}}$, exist by assumption, for by fork-acyclicity we have that $r,s\prec_{A}q\in Q^{\prime}$.

Theorem 5.1**.**

Let $Q^{\prime}$ be a finite subset of $Q$ and assume that for all $r\in Q$ such that $r\prec_{A}q$ for some $q\in Q^{\prime}$ there exists a series-rational expression $e_{r}^{+}\in{\mathcal{T}_{\Sigma}}$ with \left\ldbrack e_{r}^{+}\right\rdbrack=L_{A}(q)-\{1\}. For all $q,q^{\prime}\in Q^{\prime}$, for all $Q^{\prime\prime}\subseteq Q^{\prime}$, and for all $U\in\mathsf{Pom}_{\Sigma}^{+}$, we have that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime} according to some path that only visits states in $Q^{\prime\prime}$ if, and only if, U\in\left\ldbrack e^{Q^{\prime\prime}}_{qq^{\prime}}\right\rdbrack.

Proof.

We prove the implication from left to right with induction on the size of $Q^{\prime\prime}$.

Suppose that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime} according to some path through $A$ that only visits states in $Q^{\prime\prime}$. Then there exist $n\geq 1$, $q_{0},q_{n}\in Q$, $q_{1},\dots,q_{n-1}\in Q^{\prime\prime}$ and $U_{1},\dots,U_{n}\in\mathsf{Pom}_{\Sigma}^{+}$ such that $U=U_{1}\cdots U_{n}$ and

[TABLE]

Furthermore, for all $1\leq i\leq n$, either $U_{i}=a$ for some $a\in\Sigma$ and $q_{i}=\delta(q_{i-1},a)$, or $U_{i}=V_{i}\parallel W_{i}$ for some $V_{i},W_{i}\in\mathsf{Pom}_{\Sigma}^{+}$ and there are $r_{i},s_{i}\in Q$ and $r_{i}^{\prime},s_{i}^{\prime}\in F$ such that r_{i}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{i}}}}r_{i}^{\prime}, s_{i}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{i}}}}s_{i}^{\prime} and $q_{i}=\gamma(q_{i-1},\{\mskip-4.0mu|r_{i},s_{i}|\mskip-4.0mu\})$. We distinguish cases according to whether $n=1$ or $n>1$.

• •

If $n=1$, then we distinguish cases according to whether $U_{1}=a$ or $U_{1}=V_{1}\parallel W_{1}$. In the first case, we have that $q^{\prime}=\delta(q,a)$, so U=U_{1}=a\in\left\ldbrack e^{\emptyset}_{qq^{\prime}}\right\rdbrack\subseteq\left\ldbrack e^{Q^{\prime\prime}}_{qq^{\prime}}\right\rdbrack. In the second case, we have that there exist $r,s^{\prime}\in Q$ and $r^{\prime},s^{\prime}\in F$ such that $q^{\prime}=\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$, r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V_{1}}}}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W_{1}}}}s^{\prime}. Hence $V_{1}\in L_{A}(r)-\{1\}$ and $W_{1}\in L_{A}(s)-\{1\}$. Furthermore, by fork-acyclicity we have that $r,s\prec_{A}q$, so there exist series-rational expressions $e_{r}^{+},e_{s}^{+}\in{\mathcal{T}_{\Sigma}}$ such that \left\ldbrack e_{r}^{+}\right\rdbrack=L_{A}(r)-\{1\} and \left\ldbrack e_{s}^{+}\right\rdbrack=L_{A}(s)-\{1\}. It follows that V_{1}\in\left\ldbrack e_{r}^{+}\right\rdbrack and W_{1}\in\left\ldbrack e_{s}^{+}\right\rdbrack, and hence V_{1}\parallel W_{1}\in\left\ldbrack e_{r}^{+}\parallel e_{s}^{+}\right\rdbrack. We conclude that U=U_{1}=V_{1}\parallel W_{1}\in\left\ldbrack e^{\emptyset}_{qq^{\prime}}\right\rdbrack\subseteq\left\ldbrack e^{Q^{\prime\prime}}_{qq^{\prime}}\right\rdbrack.

• •

If $n>1$. Then, clearly, $Q^{\prime\prime}$ is non-empty; let $q^{\prime\prime}\in Q^{\prime\prime}$. Furthermore, let $I=\{0\leq i\leq n:q_{i}=q^{\prime\prime}\}$. If $I=\emptyset$, then by the induction hypothesis we have that U\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{qq^{\prime}}\right\rdbrack\subseteq\left\ldbrack e^{Q^{\prime\prime}}_{qq^{\prime}}\right\rdbrack.

Otherwise, suppose that $I\neq\emptyset$, say $I=\{i_{1},\dots,i_{k}\}$ with $i_{1}<\cdots<i_{k}$. Then, by the induction hypothesis, U_{i_{j}+1}\cdots U_{i_{j+1}}\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{q^{\prime\prime}q^{\prime\prime}}\right\rdbrack for all $1\leq j<k$. Moreover, also by the induction hypothesis, U_{0}\cdots U_{i_{1}}\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{qq^{\prime\prime}}\right\rdbrack and U_{i_{k}+1}\cdots U_{n}\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{q^{\prime\prime}q^{\prime}}\right\rdbrack. Hence,

[TABLE]

We prove the implication from right to left also with induction on the size of $Q^{\prime\prime}$. Suppose that U\in\left\ldbrack e^{Q^{\prime\prime}}_{qq^{\prime}}\right\rdbrack. If $Q^{\prime\prime}=\emptyset$, then, considering the structure of $e^{Q^{\prime\prime}}_{qq^{\prime}}$, there are two cases:

• •

If $U=a$ for some $a\in\Sigma$ such that $q^{\prime}=\delta(q,a)$, then, clearly, q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}q^{\prime}.

• •

If there exist $r,s\in Q$ and $V,W\in\mathsf{Pom}_{\Sigma}^{+}$ such that $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\pi_{A}(q)$, $q^{\prime}=\gamma(q,\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$, $U=V\parallel W$, V\in\left\ldbrack e_{r}^{+}\right\rdbrack, and W\in\left\ldbrack e_{s}^{+}\right\rdbrack, then (by the premise) there exist $r^{\prime},s^{\prime}\in F$ such that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}s^{\prime}. Hence, q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}q^{\prime}.

Otherwise, suppose that $Q^{\prime\prime}$ is non-empty, and let $q^{\prime\prime}\in Q^{\prime\prime}$. Then, again considering the structure of $e^{Q^{\prime\prime}}_{qq^{\prime}}$, there are two cases:

• •

If U\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{qq^{\prime}}\right\rdbrack, then by the induction hypothesis q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}q^{\prime}.

• •

If U\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{qq^{\prime\prime}}\cdot{(e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{q^{\prime\prime}q^{\prime\prime}})}^{*}\cdot e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{q^{\prime\prime}q^{\prime}}\right\rdbrack, then there exist $U^{\prime}$, $U_{1},\dots U_{n}$ ($n\geq 0$) and $U^{\prime\prime}$ such that $U=U^{\prime}\cdot U_{1}\cdots U_{n}\cdot U^{\prime\prime}$, U^{\prime}\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{qq^{\prime\prime}}\right\rdbrack, U_{i}\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{q^{\prime\prime}q^{\prime\prime}}\right\rdbrack for all $1\leq i\leq n$, and U^{\prime\prime}\in\left\ldbrack e^{Q^{\prime\prime}-\{q^{\prime\prime}\}}_{q^{\prime\prime}q^{\prime}}\right\rdbrack. By the induction hypothesis, it follows that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U^{\prime}}}}q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{1}}}}\cdots\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U_{n}}}}q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U^{\prime\prime}}}}q^{\prime}, according to a series of paths that only visit states in $Q^{\prime\prime}-\{q^{\prime\prime}\}$, with the intermediate states of these paths all $q^{\prime\prime}$. We thus conclude that q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}q^{\prime} according to some path that only visits states in $Q^{\prime\prime}$. ∎

Using the auxiliary expressions $e^{Q^{\prime\prime}}_{qq^{\prime}}$, we can now associate series-rational expressions $e_{q},e_{q}^{+}\in{\mathcal{T}_{\Sigma}}$ with every $q\in Q$, defining $e_{q}^{+}$ by $e_{q}^{+}=\sum_{q^{\prime}\in\rho_{A}(q)\cap F}e^{\rho_{A}(q)}_{qq^{\prime}}$ and $e_{q}=e_{q}^{+}+[q\in F]$. Note that $q\in\rho_{A}(q)$ and, by Lemma 3, for all $q^{\prime}\in Q$ such that $q^{\prime}\prec_{A}q^{\prime\prime}$ for some $q^{\prime\prime}\in\rho_{A}(q)$ we have $q^{\prime}\prec_{A}q$, and hence there exists, by induction, a series-rational expression $e_{q^{\prime}}\in{\mathcal{T}_{\Sigma}}$ such that \left\ldbrack e_{q^{\prime}}\right\rdbrack=L_{A}(q^{\prime}). So the expressions $e^{\rho_{A}(q)}_{qq^{\prime}}$ are, indeed, defined in Definition 5.

Corollary \thecorollary.

For every state $q\in Q$ we have \left\ldbrack e_{q}^{+}\right\rdbrack=L_{A}(q)-\{1\} and \left\ldbrack e_{q}\right\rdbrack=L_{A}(q).

6 Discussion

Another automaton formalism for pomsets, branching automata, was proposed by Lodaya and Weil [14, 15]. Branching automata define the states where parallelism can start (fork) or end (join) in two relations; pomset automata condense this information in a single function. Lodaya and Weil also provided a translation of series-parallel expressions to branching automata, based on Thompson’s construction [18], which relies on the fact that their automata encode transitions non-deterministically, i.e., as relations. Our Brzozowski-style [3] translation, in contrast, directly constructs transition functions from the expressions. Lastly, their translation of branching automata to series-parallel expressions is only sound for a semantically restricted class of automata, whereas our restriction is syntactic.

Jipsen and Moshier [8] provided an alternative formulation of the automata proposed by Lodaya and Weil, also called branching automata. Their method to encode parallelism in these branching automata is conceptually dual to pomset automata: branching automata distinguish based on the target states of traces to determine the join state, whereas pomset automata distinguish based on the origin states of traces. The translations of series-parallel expressions to branching automata and vice versa suffer from the same shortcomings as those by Lodaya and Weil, i.e., transition relations rather than functions and a semantic restriction on automata for the translation of automata to expressions.

Lodaya and Weil observed [15] that the behaviour of their automata corresponds to $1$-safe Petri nets. Since the behavior of their branching automata can be matched with our (bounded, fork-acyclic) pomset automata, we believe that $1$-safe Petri nets also correspond to our automata. We opted to treat semantics of series-rational expressions in terms of automata instead of Petri nets to find more opportunities to extend to a coalgebraic treatment. While the present paper does not reach this goal, we believe that our formulation in terms of states and transition functions offers some hope of getting there.

Prisacariu introduced Synchronous Kleene Algebra (SKA) [16], extending Kleene Algebra with a synchronous composition operator. SKA differs from our model in that it assumes that all basic actions are performed in unit time, and that actors responsible for individual actions never idle. In contrast, our (weak BKA-like) model makes no synchrony assumptions: expressions can be composed in parallel, and the relative timing of basic actions within those expressions is irrelevant for the semantics. Prisacariu axiomatized SKA and extended it to Synchronous Kleene Algebra with Tests (SKAT); others [2] proposed Brzozowski-style derivatives of SKA expressions and used them to test equivalence of SKA and SKAT terms.

7 Further work

We plan to extend our results to semantics of series-parallel expressions in terms of downward-closed pomset languages, i.e., sets of pomsets that are closed under Gischer’s subsumption order [4]. Such an extension would correspond to adding the weak exchange law (which relates sequential and parallel compositions), and thus yields an operational model for weak CKA. We conjecture that no change to the automaton model is necessary to accommodate this generalization, just like Struth and Laurence suspect that the downward-closed semantics of series-parallel expressions can be captured by their non-downward closed semantics.

Our series-rational expressions do not include the parallel analogue of the Kleene star (sometimes called “parallel star”, or “replication”). Future work could look into extending derivatives to include this operator, and relaxing fork-acyclicity to allow recovering expressions that include the parallel star from an automaton that satisfies this weaker restriction.

A classic result by Kozen [10] axiomatizes language equivalence of rational expressions using Kleene’s theorem [9] and the uniqueness of minimal finite automata; consequently, the free model for KA can also be characterized in terms of rational languages. It would be interesting to see if the same technique can be used (based on pomset automata) to show that the axioms of weak Bi-Kleene Algebra are a complete axiomatization of pomset language equivalence of series-rational expressions, and thus characterise the free weak Bi-Kleene Algebra (or even the free weak CKA) in terms of series-rational pomset languages. Although an such a result was recently published [13], it does not rely on an automaton model.

Brzozowski derivatives for classic rational expressions induce a coalgebra on rational expressions that corresponds to a finite automaton. We aim to study series-rational expressions coalgebraically. The first step would be to find the coalgebraic analogue of pomset automata such that language acceptance is characterized by the homomorphism into the final coalgebra. Ideally, such a view of pomset automata would give rise to a decision procedure for equivalence of series-rational expressions based on coalgebraic bisimulation-up-to [17].

Rational expressions can be extended with tests to reason about imperative programs equationally [12]. In the same vein, one can extend series-rational expressions with tests [7, 8] to reason about parallel imperative programs equationally. We are particularly interested in employing such an extension to extend the network specification language NetKAT [1] with primitives for concurrency so as to model and reason about concurrency within networks.

Appendix A Proofs of auxiliary lemmas

See 2.4

Proof.

The proof of the first claim proceeds by induction on the construction of $\simeq$. In the base, there are nine cases to consider.

• •

If $e=f$, then the claim follows immediately.

• •

If $e=f+0$, then \left\ldbrack e\right\rdbrack=\left\ldbrack f\right\rdbrack\cup\left\ldbrack 0\right\rdbrack=\left\ldbrack f\right\rdbrack\cup\emptyset=\left\ldbrack f\right\rdbrack.

• •

If $e=f+f$, then \left\ldbrack e\right\rdbrack=\left\ldbrack f\right\rdbrack\cup\left\ldbrack f\right\rdbrack=\left\ldbrack f\right\rdbrack.

• •

If $e=g_{1}+g_{2}$ and $f=g_{2}+g_{1}$, then \left\ldbrack e\right\rdbrack=\left\ldbrack g_{1}\right\rdbrack\cup\left\ldbrack g_{2}\right\rdbrack=\left\ldbrack g_{2}\right\rdbrack\cup\left\ldbrack g_{1}\right\rdbrack=\left\ldbrack f\right\rdbrack.

• •

If $e=g_{1}+(g_{2}+g_{3})$ and $f=(g_{1}+g_{2})+g_{3}$, then \left\ldbrack e\right\rdbrack=\left\ldbrack g_{1}\right\rdbrack\cup(\left\ldbrack g_{2}\right\rdbrack\cup\left\ldbrack g_{3}\right\rdbrack)=(\left\ldbrack g_{1}\right\rdbrack\cup\left\ldbrack g_{2}\right\rdbrack)\cup\left\ldbrack g_{3}\right\rdbrack=\left\ldbrack f\right\rdbrack.

• •

If $e=0\cdot e_{1}$ and $f=0$, then \left\ldbrack e\right\rdbrack=\left\ldbrack 0\right\rdbrack\cdot\left\ldbrack e_{1}\right\rdbrack=\emptyset=\left\ldbrack f\right\rdbrack.

• •

If $e=e_{1}\cdot 0$ and $f=0$, then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack\cdot\left\ldbrack 0\right\rdbrack=\emptyset=\left\ldbrack f\right\rdbrack.

• •

If $e=0\parallel e_{1}$ and $f=0$, then \left\ldbrack e\right\rdbrack=\left\ldbrack 0\right\rdbrack\parallel\left\ldbrack e_{1}\right\rdbrack=\emptyset=\left\ldbrack f\right\rdbrack.

• •

If $e=e_{1}\parallel 0$ and $f=0$, then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack\parallel\left\ldbrack 0\right\rdbrack=\emptyset=\left\ldbrack f\right\rdbrack.

For the inductive step, there are six cases to consider.

• •

If $e\simeq f$ because $e\simeq g$ and $g\simeq f$, then \left\ldbrack e\right\rdbrack=\left\ldbrack g\right\rdbrack and \left\ldbrack g\right\rdbrack=\left\ldbrack f\right\rdbrack by induction, thus \left\ldbrack e\right\rdbrack=\left\ldbrack f\right\rdbrack.

• •

If $e\simeq f$ because $f\simeq e$, then \left\ldbrack f\right\rdbrack=\left\ldbrack e\right\rdbrack by induction, and thus \left\ldbrack e\right\rdbrack=\left\ldbrack f\right\rdbrack.

• •

If $e\simeq f$ because $e=e_{1}+e_{2}$ and $f=f_{1}+f_{2}$ with $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then we know that \left\ldbrack e_{1}\right\rdbrack=\left\ldbrack f_{1}\right\rdbrack and \left\ldbrack e_{2}\right\rdbrack=\left\ldbrack f_{2}\right\rdbrack by induction. But then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack\cup\left\ldbrack e_{2}\right\rdbrack=\left\ldbrack f_{1}\right\rdbrack\cup\left\ldbrack f_{2}\right\rdbrack=\left\ldbrack f\right\rdbrack.

• •

If $e\simeq f$ because $e=e_{1}\cdot e_{2}$ and $f=f_{1}\cdot f_{2}$ with $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then we know that \left\ldbrack e_{1}\right\rdbrack=\left\ldbrack f_{1}\right\rdbrack and \left\ldbrack e_{2}\right\rdbrack=\left\ldbrack f_{2}\right\rdbrack by induction. But then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack\cdot\left\ldbrack e_{2}\right\rdbrack=\left\ldbrack f_{1}\right\rdbrack\cdot\left\ldbrack f_{2}\right\rdbrack=\left\ldbrack f\right\rdbrack.

• •

If $e\simeq f$ because $e=e_{1}\parallel e_{2}$ and $f=f_{1}\parallel f_{2}$ with $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then we know that \left\ldbrack e_{1}\right\rdbrack=\left\ldbrack f_{1}\right\rdbrack and \left\ldbrack e_{2}\right\rdbrack=\left\ldbrack f_{2}\right\rdbrack by induction. But then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack\parallel\left\ldbrack e_{2}\right\rdbrack=\left\ldbrack f_{1}\right\rdbrack\parallel\left\ldbrack f_{2}\right\rdbrack=\left\ldbrack f\right\rdbrack.

• •

If $e\simeq f$ because $e=e_{1}^{*}$ and $f=f_{1}^{*}$ with $e_{1}\simeq f_{1}$, then we know that \left\ldbrack e_{1}\right\rdbrack=\left\ldbrack f_{1}\right\rdbrack by induction. But then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack^{*}=\left\ldbrack f_{1}\right\rdbrack^{*}=\left\ldbrack f\right\rdbrack.

We now prove the second claim. For the direction from left to right, note that \left\ldbrack e\right\rdbrack=\left\ldbrack 0\right\rdbrack=\emptyset by Lemma 2.4. The direction from right to left proceeds by induction on $e$. In the base, $e=0$ and thus $e\simeq 0$ by reflexivity. For the inductive step, there are three cases to consider.

• •

If $e=e_{1}+e_{2}$, then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack\cup\left\ldbrack e_{2}\right\rdbrack=\emptyset, therefore \left\ldbrack e_{1}\right\rdbrack=\emptyset and \left\ldbrack e_{2}\right\rdbrack=\emptyset. But then, by induction, we have that $e_{1}\simeq 0$ and $e_{2}\simeq 0$. We then know that $e=e_{1}+e_{2}\simeq 0+0\simeq 0$.

• •

If $e=e_{1}\cdot e_{2}$, then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack\cdot\left\ldbrack e_{2}\right\rdbrack=\emptyset, therefore \left\ldbrack e_{1}\right\rdbrack=\emptyset or \left\ldbrack e_{2}\right\rdbrack=\emptyset. But then, by induction, we have that $e_{1}\simeq 0$ or $e_{2}\simeq 0$. In either case, it follows that $e=e_{1}\cdot e_{2}\simeq 0$.

• •

If $e=e_{1}\parallel e_{2}$, then \left\ldbrack e\right\rdbrack=\left\ldbrack e_{1}\right\rdbrack\parallel\left\ldbrack e_{2}\right\rdbrack=\emptyset, therefore \left\ldbrack e_{1}\right\rdbrack=\emptyset or \left\ldbrack e_{2}\right\rdbrack=\emptyset. But then, by induction, we have that $e_{1}\simeq 0$ or $e_{2}\simeq 0$. In either case, it follows that $e=e_{1}\parallel e_{2}\simeq 0$. ∎

See 3

Proof.

We write R_{A}(q)=\{q^{\prime}\in Q:\exists U\in\mathsf{Pom}_{\Sigma}^{+}.\ q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{A}q^{\prime}\}.

Suppose that $q^{\prime}\in R_{A}(q)\cup\{q,\bot\}$. If $q^{\prime}\in\{q,\bot\}$, then $q^{\prime}\in\rho_{A}(q)\cup\{\bot\}$ by definition. Otherwise, if $q^{\prime}\in R_{A}(q)$, then q\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}q^{\prime} for some $U\in\mathsf{Pom}_{\Sigma}^{+}$. We show, more generally, that if q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}q^{\prime} for some $q^{\prime\prime}\in\rho_{A}(q)\cup\{\bot\}$, then $q^{\prime}\in\rho_{A}(q)\cup\{\bot\}$, by induction on $U$. In the base, $U=a\in\Sigma$ and thus $q^{\prime\prime}=\delta(q^{\prime},a)$. But then $q^{\prime}\in\rho_{A}(q)\cup\{\bot\}$ immediately. For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$ with $V$ and $W$ smaller than $U$, then there exists an $r\in Q$ such that q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}r and r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}q^{\prime}. By induction, $r\in\rho_{A}(q)\cup\{\bot\}$, and again by induction $q^{\prime}\in\rho_{A}(q)\cup\{\bot\}$.

• •

If $U=V\parallel W$ with $V$ and $W$ smaller than $U$, then there exist $r,s\in Q$ and $r^{\prime},s^{\prime}\in F$ such that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}s^{\prime}, and $q^{\prime}=\gamma(q^{\prime\prime},\{\mskip-4.0mu|r,s|\mskip-4.0mu\})$. Note that, in this case, $r^{\prime},s^{\prime}\neq\bot$. If $q^{\prime}=\bot$, then $q^{\prime}\in\rho_{A}(q)\cup\{\bot\}$. Otherwise, $\{\mskip-4.0mu|r,s|\mskip-4.0mu\}\in\pi_{A}(q^{\prime\prime})$, and thus $q^{\prime}\in\rho_{A}(q)\cup\{\bot\}$.

For the second part of the claim, suppose that $\bot$ is the only state of $A$ with an empty language. Let $q^{\prime}\in\rho_{A}(q)\cup\{\bot\}$. If $q^{\prime}=\bot$, then the claim follows. For the case where $q^{\prime}\in\rho_{A}(q)$, we prove that $q^{\prime}\in R_{A}(q)\cup\{q,\bot\}$, by induction on the construction of $\rho_{A}(q)$. In the base, $q^{\prime}=q$, and thus we find that $q^{\prime}\in R_{A}(q)\cup\{q,\bot\}$ immediately.

For the inductive step, there are two cases to consider. For both cases, first note that if $q^{\prime\prime}\in R_{A}(q^{\prime})$ and $q^{\prime}\in R_{A}(q)$, then $q^{\prime\prime}\in R_{A}(q)$.

• •

Suppose $q^{\prime}=\delta(q^{\prime\prime},a)$ for some $q^{\prime\prime}\in\rho_{A}(q)$ and $a\in\Sigma$. By induction, we know that $q^{\prime\prime}\in R_{A}(q)\cup\{q,\bot\}$. If $q^{\prime\prime}=\bot$, then $q^{\prime}=\bot$ and the claim follows. Otherwise, note that $q^{\prime}\in R_{A}(q^{\prime\prime})$ by q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{a}}}_{A}q^{\prime}. If $q^{\prime\prime}=q$, then $q^{\prime}\in R_{A}(q)$ immediately. In the remaining case, $q^{\prime\prime}\in R_{A}(q)$, and thus $q^{\prime}\in R_{A}(q)$ by the observation above.

• •

Suppose $q^{\prime}=\gamma(q^{\prime\prime},\phi)$ for some $q^{\prime\prime}\in\rho_{A}(q)$ and $\phi\in\pi_{A}(q^{\prime\prime})$. By induction we know that $q^{\prime\prime}\in R_{A}(q)\cup\{q,\bot\}$. Since $\phi\in\pi_{A}(q^{\prime\prime})$, we know that $q^{\prime\prime}\neq\bot$ — for otherwise $q^{\prime}=\bot$ and thus $\phi\not\in\pi_{A}(q^{\prime\prime})$. Furthermore, if $\phi=\{\mskip-4.0mu|r,s|\mskip-4.0mu\}$ then $r,s\neq\bot$ and thus, since $\bot$ is the only state with an empty language, there exist $V,W\in\mathsf{Pom}_{\Sigma}^{+}$ as well as $r^{\prime},s^{\prime}\in F$ such that r\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{A}r^{\prime} and s\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{A}s^{\prime}; therefore, q^{\prime\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U\parallel V}}}_{A}q^{\prime} and thus $q^{\prime}\in R_{A}(q^{\prime\prime})$. If $q^{\prime\prime}=q$, then $q^{\prime}\in R_{A}(q)$ immediately. Otherwise, $q^{\prime\prime}\in R_{A}(q)$, and thus $q^{\prime}\in R_{A}(q)$ by the observation above. ∎

See 4.1

Proof.

The proof proceeds by induction on the construction of $\simeq$. In the base, there are nine cases to consider.

• •

Suppose that $e=f$, then the claim holds immediately.

• •

Suppose that $e=f+0$. If $e\in F_{\Sigma}$, then either $f\in F_{\Sigma}$ or $0\in F_{\Sigma}$. Since the latter does not hold, $f\in F_{\Sigma}$ follows. Also, if $f\in F_{\Sigma}$, then $e=f+0\in F_{\Sigma}$ immediately.

• •

Suppose that $e=f+f$. If $f+f\in F_{\Sigma}$, then $f\in F_{\Sigma}$ immediately; if $f\in F_{\Sigma}$, then also $f+f\in F_{\Sigma}$.

• •

Suppose that $e=g_{1}+g_{2}$ and $f=g_{2}+g_{1}$. If $g_{1}+g_{2}\in F_{\Sigma}$, then $g_{1}\in F_{\Sigma}$ or $g_{2}\in F_{\Sigma}$; in either case, $g_{2}+g_{1}\in F_{\Sigma}$. The claim in the other direction is proved similarly.

• •

Suppose that $e=g_{1}+(g_{2}+g_{3})$ and $f=(g_{1}+g_{2})+g_{3}$. If $e\in F_{\Sigma}$, then $g_{1}\in F_{\Sigma}$ or $g_{2}+g_{3}\in F_{\Sigma}$, and thus one of $g_{1},g_{2},g_{3}$ must be in $F_{\Sigma}$. But then $g_{1}+g_{2}$ or $g_{3}$ must be in $F_{\Sigma}$, and thus $f=(g_{1}+g_{2})+g_{3}\in F_{\Sigma}$. The proof in the other direction is similar.

• •

Suppose that $e=0\cdot e_{1}$ and $f=0$. Then $e,f\not\in F_{\Sigma}$ and thus the claim holds immediately.

• •

Suppose that $e=e_{1}\cdot 0$ and $f=0$. Then $e,f\not\in F_{\Sigma}$ and thus the claim holds immediately.

• •

Suppose that $e=e_{1}\parallel 0$ and $f=0$. Then $e,f\not\in F_{\Sigma}$ and thus the claim holds immediately.

• •

Suppose that $e=0\parallel e_{1}$ and $f=0$. Then $e,f\not\in F_{\Sigma}$ and thus the claim holds immediately.

For the inductive step, there are six cases to consider.

• •

Suppose that $e\simeq f$ because $f\simeq e$; the claim (in both directions) then follows from the induction hypothesis by symmetry of mutual implication.

• •

Suppose that $e\simeq f$ because $e\simeq g$ and $g\simeq f$; the claim (in both directions) then follows from the induction hypothesis by transitivity of implication.

• •

Suppose that $e\simeq f$ because $e=e_{1}+e_{2}$ and $f=f_{1}+f_{2}$, with $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$. If $e_{1}+e_{2}\in F_{\Sigma}$, either $e_{1}\in F_{\Sigma}$ or $e_{2}\in F_{\Sigma}$. But then (by induction) either $f_{1}\in F_{\Sigma}$ or $f_{2}\in F_{\Sigma}$, thus $f_{1}+f_{2}\in F_{\Sigma}$. The claim in the other direction is proved similarly.

• •

Suppose that $e\simeq f$ because $e=e_{1}\cdot e_{2}$ and $f=f_{1}\cdot f_{2}$, with $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$. If $e\in F_{\Sigma}$, then $e_{1},e_{2}\in F_{\Sigma}$. But then (by induction) $f_{1},f_{2}\in F_{\Sigma}$, thus $f_{1}\cdot f_{2}\in F_{\Sigma}$. The claim in the other direction is proved similarly.

• •

Suppose that $e\simeq f$ because $e=e_{1}\parallel e_{2}$ and $f=f_{1}\parallel f_{2}$ with $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$. If $e\in F_{\Sigma}$, then $e_{1},e_{2}\in F_{\Sigma}$. But then (by induction) $f_{1},f_{2}\in F_{\Sigma}$, thus $f_{1}\parallel f_{2}\in F_{\Sigma}$. The claim in the other direction is proved similarly.

• •

Suppose that $e\simeq f$ because $e=e_{1}^{*}$ and $f=f_{1}^{*}$ with $e_{1}\simeq f_{1}$. Then $e,f\in F_{\Sigma}$, and so the claim holds immediately in both directions. ∎

See 4.1

Proof.

The proof of the first claim proceeds by induction on the construction of $\simeq$. In the base, there are nine cases to consider.

• •

If $e=f$, then $\delta_{\Sigma}(e,a)=\delta_{\Sigma}(f,a)\simeq\delta_{\Sigma}(f,a)$.

• •

If $e=f+0$, then $\delta_{\Sigma}(e,a)=\delta_{\Sigma}(f,a)+\delta_{\Sigma}(0,a)=\delta_{\Sigma}(f,a)+0\simeq\delta_{\Sigma}(f,a)$.

• •

If $e=f+f$, then $\delta_{\Sigma}(e,a)=\delta_{\Sigma}(f,a)+\delta_{\Sigma}(f,a)\simeq\delta_{\Sigma}(f,a)$.

• •

If $e=g_{1}+g_{2}$ and $f=g_{2}+g_{1}$, then

[TABLE]

• •

If $e=g_{1}+(g_{2}+g_{3})$ and $f=(g_{1}+g_{2})+g_{3}$, then

[TABLE]

• •

If $e=0\cdot e_{1}$ and $f=0$, then $\delta_{\Sigma}(e,a)=\delta_{\Sigma}(0,a)\cdot e_{1}+0=0\cdot e_{1}+0\simeq 0=\delta_{\Sigma}(0,a)$.

• •

If $e=e_{1}\cdot 0$ and $f=0$, then $\delta_{\Sigma}(e,a)=\delta_{\Sigma}(e_{1},a)\cdot 0+e_{1}\star\delta_{\Sigma}(0,a)\simeq 0=\delta_{\Sigma}(0,a)$.

• •

If $e=e_{1}\parallel 0$ and $f=0$, then $\delta_{\Sigma}(e,a)=e_{1}\star\delta_{\Sigma}(0,a)+0\simeq 0=\delta_{\Sigma}(0,a)$.

• •

If $e=0\parallel e_{1}$ and $f=0$, then $\delta_{\Sigma}(e,a)=0+e_{2}\star\delta_{\Sigma}(0,a)\simeq 0=\delta_{\Sigma}(0,a)$.

For the inductive step, there are six cases to consider.

• •

If $e\simeq f$ because $f\simeq e$, then by induction we know that $\delta_{\Sigma}(f,a)\simeq\delta_{\Sigma}(e,a)$, thus $\delta_{\Sigma}(e,a)\simeq\delta_{\Sigma}(f,a)$.

• •

If $e\simeq f$ because $e\simeq g$ and $g\simeq f$, then by induction we know that $\delta_{\Sigma}(e,a)\simeq\delta_{\Sigma}(g,a)$ and $\delta_{\Sigma}(g,a)\simeq\delta_{\Sigma}(f,a)$ thus $\delta_{\Sigma}(e,a)\simeq\delta_{\Sigma}(f,a)$.

• •

If $e\simeq f$ because $e=e_{1}+e_{2}$ and $f=f_{1}+f_{2}$ such that $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then by induction we know that $\delta_{\Sigma}(e_{1},a)\simeq\delta_{\Sigma}(f_{1},a)$ and $\delta_{\Sigma}(e_{2},a)\simeq\delta_{\Sigma}(f_{2},a)$, and thus

[TABLE]

• •

If $e\simeq f$ because $e=e_{1}\cdot e_{2}$ and $f=f_{1}\cdot f_{2}$ such that $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then by induction we know that $\delta_{\Sigma}(e_{1},a)\simeq\delta_{\Sigma}(f_{1},a)$ and $\delta_{\Sigma}(e_{2},a)\simeq\delta_{\Sigma}(f_{2},a)$, and thus

[TABLE]

where we also apply Lemma 4.1.

• •

If $e\simeq f$ because $e=e_{1}\parallel e_{2}$ and $f=f_{1}\parallel f_{2}$ such that $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then by induction we know that $\delta_{\Sigma}(e_{1},a)\simeq\delta_{\Sigma}(f_{1},a)$ and $\delta_{\Sigma}(e_{2},a)\simeq\delta_{\Sigma}(f_{2},a)$, and thus

[TABLE]

where we also apply Lemma 4.1.

• •

If $e\simeq f$ because $e=e_{1}^{*}$ and $f=f_{1}^{*}$ such that $e_{1}\simeq f_{1}$, then by induction we know that $\delta_{\Sigma}(e_{1},a)\simeq\delta_{\Sigma}(f_{1},a)$, and thus $\delta_{\Sigma}(e,a)=\delta_{\Sigma}(e_{1},a)\cdot e_{1}^{*}\simeq\delta_{\Sigma}(f_{1},a)\cdot f_{1}^{*}=\delta_{\Sigma}(f,a)$.

The proof of the second claim also proceeds by induction on the construction of $\simeq$. In the base, there are nine cases to consider.

• •

If $e=f$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(f,\phi)\simeq\gamma_{\Sigma}(f,\phi)$.

• •

If $e=f+0$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(f,\phi)+\gamma_{\Sigma}(0,\phi)=\gamma_{\Sigma}(f,\phi)+0\simeq\gamma_{\Sigma}(f,\phi)$.

• •

If $e=f+f$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(f,\phi)+\gamma_{\Sigma}(f,\phi)\simeq\gamma_{\Sigma}(f,\phi)$.

• •

If $e=g_{1}+g_{2}$ and $f=g_{2}+g_{1}$, then

[TABLE]

• •

If $e=g_{1}+(g_{2}+g_{3})$ and $f=(g_{1}+g_{2})+g_{3}$, then

[TABLE]

• •

If $e=0\cdot e_{1}$ and $f=0$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(0,\phi)\cdot e_{1}+0=0\cdot e_{1}+0\simeq 0=\gamma_{\Sigma}(0,\phi)$.

• •

If $e=e_{1}\cdot 0$ and $f=0$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e_{1},\phi)\cdot 0+e_{1}\star\gamma_{\Sigma}(0,\phi)\simeq 0=\gamma_{\Sigma}(0,\phi)$.

• •

If $e=0\parallel e_{1}$ and $f=0$, then since $g,h\not\simeq 0$, in particular $\phi\not\simeq\{\mskip-4.0mu|e_{1},0|\mskip-4.0mu\}$. We then find that $\gamma_{\Sigma}(e,\phi)=0+e_{1}\star\gamma_{\Sigma}(0,\phi)+0\simeq 0=\gamma_{\Sigma}(0,\phi)$.

• •

If $e=e_{1}\parallel 0$ and $f=0$, then since $g,h\not\simeq 0$, in particular $\phi\not\simeq\{\mskip-4.0mu|0,e_{1}|\mskip-4.0mu\}$. We then find that $\gamma_{\Sigma}(e,\phi)=0+0+e_{1}\star\gamma_{\Sigma}(0,\phi)\simeq 0=\gamma_{\Sigma}(0,\phi)$.

For the inductive step, there are six cases to consider.

• •

If $e\simeq f$ because $f\simeq e$, then by induction we know that $\gamma_{\Sigma}(f,\phi)\simeq\gamma_{\Sigma}(e,\phi)$, thus $\gamma_{\Sigma}(e,\phi)\simeq\gamma_{\Sigma}(f,\phi)$.

• •

If $e\simeq f$ because $e\simeq g$ and $g\simeq f$, then by induction we know that $\gamma_{\Sigma}(e,\phi)\simeq\gamma_{\Sigma}(g,\phi)$ and $\gamma_{\Sigma}(g,\phi)\simeq\gamma_{\Sigma}(f,\phi)$, thus $\gamma_{\Sigma}(e,\phi)\simeq\gamma_{\Sigma}(f,\phi)$.

• •

If $e\simeq f$ because $e=e_{1}+e_{2}$ and $f=f_{1}+f_{2}$ such that $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then by induction we know that $\gamma_{\Sigma}(e_{1},\phi)\simeq\gamma_{\Sigma}(f_{1},\phi)$ and $\gamma_{\Sigma}(e_{2},\phi)\simeq\gamma_{\Sigma}(f_{2},\phi)$, and thus

[TABLE]

• •

If $e\simeq f$ because $e=e_{1}\cdot e_{2}$ and $f=f_{1}\cdot f_{2}$ such that $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then by induction we know that $\gamma_{\Sigma}(e_{1},\phi)\simeq\gamma_{\Sigma}(f_{1},\phi)$ and $\gamma_{\Sigma}(e_{2},\phi)\simeq\gamma_{\Sigma}(f_{2},\phi)$, and thus

[TABLE]

where we also apply Lemma 4.1.

• •

If $e\simeq f$ because $e=e_{1}\parallel e_{2}$ and $f=f_{1}\parallel f_{2}$ such that $e_{1}\simeq f_{1}$ and $e_{2}\simeq f_{2}$, then by induction we know that $\gamma_{\Sigma}(e_{1},\phi)\simeq\gamma_{\Sigma}(f_{1},\phi)$ and $\gamma_{\Sigma}(e_{2},\phi)\simeq\gamma_{\Sigma}(f_{2},\phi)$. Furthermore, $\phi\simeq\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}$ if and only if $\phi\simeq\{\mskip-4.0mu|f_{1},f_{2}|\mskip-4.0mu\}$, and thus

[TABLE]

where we also apply Lemma 4.1.

• •

If $e\simeq f$ because $e=e_{1}^{*}$ and $f=f_{1}^{*}$ such that $e_{1}\simeq f_{1}$, then by induction we know that $\gamma_{\Sigma}(e_{1},\phi)\simeq\gamma_{\Sigma}(f_{1},\phi)$, and thus $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e_{1},\phi)\cdot e_{1}^{*}\simeq\gamma_{\Sigma}(f_{1},\phi)\cdot f_{1}^{*}=\gamma_{\Sigma}(f,\phi)$.

The last claim is shown by induction on $e$. In the base, $e=0$, $e=1$ or $e=a$, and thus $\gamma_{\Sigma}(e,\phi)=0=\gamma_{\Sigma}(e,\psi)$. For the inductive step, there are four cases to consider.

• •

If $e=e_{1}+e_{2}$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e_{1},\phi)+\gamma_{\Sigma}(e_{2},\phi)=\gamma_{\Sigma}(e_{1},\psi)+\gamma_{\Sigma}(e_{2},\psi)=\gamma_{\Sigma}(e,\psi)$.

• •

If $e=e_{1}\cdot e_{2}$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e_{1},\phi)\cdot e_{2}+e_{1}\star\gamma_{\Sigma}(e_{2},\phi)=\gamma_{\Sigma}(e_{1},\psi)\cdot e_{2}+e_{1}\star\gamma_{\Sigma}(e_{2},\psi)=\gamma_{\Sigma}(e,\psi)$.

• •

If $e=e_{1}\parallel e_{2}$, then $\gamma_{\Sigma}(e,\phi)=[\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}\simeq\phi]+e_{2}\star\gamma_{\Sigma}(e_{1},\phi)+e_{1}\star\gamma_{\Sigma}(e_{2},\phi)=[\{\mskip-4.0mu|e_{1},e_{2}|\mskip-4.0mu\}\simeq\psi]+e_{2}\star\gamma_{\Sigma}(e_{1},\psi)+e_{1}\star\gamma_{\Sigma}(e_{2},\psi)$.

• •

If $e=e_{1}^{*}$, then $\gamma_{\Sigma}(e,\phi)=\gamma_{\Sigma}(e_{1},\phi)\cdot e_{1}^{*}=\gamma_{\Sigma}(e_{1},\psi)\cdot e_{1}^{*}=\gamma_{\Sigma}(e,\psi)$. ∎

See 4.5

Proof.

The proof for the first claim proceeds by induction on $U$. In the base, $U=a\in\Sigma$. If e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f, then $f=\delta_{\Sigma}(e,a)$. But then, since $\delta_{\simeq}([e],a)=[f]$ by definition of $\delta_{\simeq}$, we find that [e]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\simeq}[f].

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$, with $V$ and $W$ smaller than $U$, then there exists a $g\in{\mathcal{T}_{\Sigma}}$ such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g and g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}f. By induction we find that [e]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\simeq}[g] and [g]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\simeq}[f], and thus [e]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\simeq}[f].

• •

If $U=V\parallel W$, with $V$ and $W$ smaller than $U$, then there exist $g,h\in{\mathcal{T}_{\Sigma}}$ and $g^{\prime},h^{\prime}\in F_{\Sigma}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime}, and $f=\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$. Note that, by Lemma 4.2, $g,h\not\simeq 0$. By induction, we find [g]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\simeq}[g^{\prime}] and [h]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\simeq}[h^{\prime}], with $[g^{\prime}],[h^{\prime}]\in F_{\simeq}$. Since $\gamma_{\simeq}([e],\{\mskip-4.0mu|[g],[h]|\mskip-4.0mu\})=[\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})]=[f]$, we find that [e]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\simeq}[f].

The proof of the second claim also proceeds by induction on $U$. In the base, $U=a\in\Sigma$. If [e]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}[f], then $[f]=\delta_{\simeq}([e],a)$. We choose $f^{\prime}=\delta_{\Sigma}(e,a)$ to find that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f and $f\simeq f^{\prime}$ by Lemma 4.1.

For the inductive step, there are two cases to consider.

• •

If $U=V\cdot W$, with $V$ and $W$ smaller than $U$, then there exists a $g\in{\mathcal{T}_{\Sigma}}$ such that [e]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\simeq}[g] and [g]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\simeq}[f]. By induction, we find $g^{\prime},f^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime} and $g\simeq g^{\prime}$ as well as g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f^{\prime\prime} and $f\simeq f^{\prime\prime}$. By Lemma 4.1, we find $f^{\prime}\in{\mathcal{T}_{\Sigma}}$ such that g^{\prime}\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}f^{\prime} and $f^{\prime\prime}\simeq f$. In total, we have that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} with $f\simeq f^{\prime}$.

• •

If $U=V\parallel W$, with $V$ and $W$ smaller than $U$, then there exist $[g],[h]\in{\mathcal{Q}_{\Sigma}}$ and $[g^{\prime}],[h^{\prime}]\in F_{\simeq}$ such that [g]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\simeq}[g^{\prime}] and [h]\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\simeq}[h^{\prime}], and $[f]=\gamma_{\simeq}([e],\{\mskip-4.0mu|[g],[h]|\mskip-4.0mu\})$. By induction, we find that $h^{\prime\prime},g^{\prime\prime}\in{\mathcal{T}_{\Sigma}}$ such that g\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{V}}}_{\Sigma}g^{\prime\prime} and h\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{W}}}_{\Sigma}h^{\prime\prime}, with $g^{\prime}\simeq g^{\prime\prime}$ and $h^{\prime}\simeq h^{\prime\prime}$, with $g^{\prime\prime},h^{\prime\prime}\in F_{\Sigma}$ by Lemma 4.1. But then $g,h\not\simeq 0$ by Lemma 4.2. We can choose $f^{\prime}=\gamma_{\Sigma}(e,\{\mskip-4.0mu|g,h|\mskip-4.0mu\})$ to find that that e\mathrel{\raisebox{-3.0pt}{\xrightarrow[]{U}}}_{\Sigma}f^{\prime} and $f\simeq f^{\prime}$ by Lemma 4.1. ∎

See 4.5

Proof.

First, if $e\simeq 0\simeq e^{\prime}$, then $0pt{e}=0=0pt{e^{\prime}}$ by definition. The proof for the remaining cases proceeds by induction on the construction of $\simeq$. In the base, there are nine cases to consider.

• •

If $e=e^{\prime}$, then the claim holds immediately.

• •

If $e=e^{\prime}+0$, then $0pt{e}=\max(0pt{e^{\prime}},0pt{0})=0pt{e^{\prime}}$.

• •

If $e=e^{\prime}+e^{\prime}$, then $0pt{e}=\max(0pt{e^{\prime}},0pt{e^{\prime}})=0pt{e^{\prime}}$.

• •

If $e=e_{1}+e_{2}$ and $e^{\prime}=e_{2}+e_{1}$, then $0pt{e}=\max(0pt{e_{1}},0pt{e_{2}})=\max(0pt{e_{2}},0pt{e_{1}})=0pt{e^{\prime}}$.

• •

If $e=e_{1}+(e_{2}+e_{3})$ and $e^{\prime}=(e_{1}+e_{2})+e_{3}$, then $0pt{e}=\max(0pt{e_{1}},0pt{e_{2}},0pt{e_{3}})=0pt{e^{\prime}}$.

For the inductive step, there are six cases to consider.

• •

If $e\simeq e^{\prime}$ because $e^{\prime}\simeq e$, then $0pt{e^{\prime}}=0pt{e}$ by induction and so the claim follows.

• •

If $e\simeq e^{\prime}$ because $e\simeq e^{\prime\prime}\simeq e^{\prime}$, then $0pt{e}=0pt{e^{\prime\prime}}=0pt{e^{\prime}}$ by induction and so $0pt{e}=0pt{e^{\prime}}$.

• •

If $e\simeq e^{\prime}$ because $e=e_{1}+e_{2}$ and $e^{\prime}=e_{1}^{\prime}+e_{2}^{\prime}$ with $e_{1}\simeq e_{1}^{\prime}$ and $e_{2}\simeq e_{2}^{\prime}$, then $0pt{e_{1}}=0pt{e_{1}^{\prime}}$ and $0pt{e_{2}}=0pt{e_{2}^{\prime}}$ by induction, thus $0pt{e}=\max(0pt{e_{1}},0pt{e_{2}})=\max(0pt{e_{1}^{\prime}},0pt{e_{2}^{\prime}})=0pt{e^{\prime}}$.

• •

If $e\simeq e^{\prime}$ because $e=e_{1}\cdot e_{2}$ and $e^{\prime}=e_{1}^{\prime}\cdot e_{2}^{\prime}$ with $e_{1}\simeq e_{1}^{\prime}$ and $e_{2}\simeq e_{2}^{\prime}$, then $0pt{e_{1}}=0pt{e_{1}^{\prime}}$ and $0pt{e_{2}}=0pt{e_{2}^{\prime}}$ by induction, thus $0pt{e}=\max(0pt{e_{1}},0pt{e_{2}})=\max(0pt{e_{1}^{\prime}},0pt{e_{2}^{\prime}})=0pt{e^{\prime}}$.

• •

If $e\simeq e^{\prime}$ because $e=e_{1}\parallel e_{2}$ and $e^{\prime}=e_{1}^{\prime}\parallel e_{2}^{\prime}$ with $e_{1}\simeq e_{1}^{\prime}$ and $e_{2}\simeq e_{2}^{\prime}$, then $0pt{e_{1}}=0pt{e_{1}^{\prime}}$ and $0pt{e_{2}}=0pt{e_{2}^{\prime}}$ by induction, thus $0pt{e}=\max(0pt{e_{1}},0pt{e_{2}})+1=\max(0pt{e_{1}^{\prime}},0pt{e_{2}^{\prime}})+1=0pt{f}$.

• •

If $e\simeq e^{\prime}$ because $e=e_{1}^{*}$ and $e^{\prime}=e_{1}^{\prime*}$, then by induction $0pt{e}=0pt{e_{1}}=0pt{e_{1}^{\prime}}=0pt{e^{\prime}}$. ∎