Completeness Theorems for Pomset Languages and Concurrent Kleene Algebras

TL;DR

This paper establishes completeness theorems for pomset languages using bi-Kleene algebra operations, connecting their equational theory to regular and commutative-regular languages, and explores properties of rational pomset languages and ideals.

Contribution

It proves that all valid equations over pomset languages are derivable from known algebraic theories and characterizes the structure of rational pomset languages and their ideals.

Findings

Valid universal equalities follow from regular and commutative-regular language theories.

Rational pomset languages are closed under Boolean operations.

Equivalence of ideal languages is provable from Kleene and exchange axioms.

Abstract

Pomsets constitute one of the most basic models of concurrency. A pomset is a generalisation of a word over an alphabet in that letters may be partially ordered. A term $t$ using the bi-Kleene operations $0,1, +, \cdot\, ,^*, \parallel, ^{(*)}$ defines a language $ \mathopen{[\![ } t \mathclose{]\!] } $ of pomsets in a natural way. We prove that every valid universal equality over pomset languages using these operations is a consequence of the equational theory of regular languages (in which parallel multiplication and iteration are undefined) plus that of the commutative-regular languages (in which sequential multiplication and iteration are undefined). We also show that the class of $\textit{rational}$ pomset languages (that is, those languages generated from singleton pomsets using the bi-Kleene operations) is closed under all Boolean operations. An $ \textit{ideal}$ of a pomset $p$ is a pomset using the letters of $p$, but having an ordering at least as strict as $p$. A bi-Kleene term $t$ thus defines the set $ \textbf{Id} (\mathopen{[\![ } t \mathclose{]\!] }) $ of ideals of pomsets in $ \mathopen{[\![ } t \mathclose{]\!] } $. We prove that if $t$ does not contain commutative iteration $^{(*)}$ (in our terminology, $t$ is bw-rational) then $\textbf{Id} (\mathopen{[\![ } t \mathclose{]\!] }) \cap \textbf{Pom}_{sp}$, where $ \textbf{Pom}_{sp}$ is the set of pomsets generated from singleton pomsets using sequential and parallel multiplication ($ \cdot$ and $ \parallel$) is defined by a bw-rational term, and if two such terms $t,t'$ define the same ideal language, then $t'=t$ is provable from the Kleene axioms for $0,1, +, \cdot\, ,^*$ plus the commutative idempotent semiring axioms for $0,1, +, \parallel$ plus the exchange law $ (u \parallel v)\cdot ( x \parallel y) \le v \cdot y \parallel u \cdot x $.

Equations

$$(u\parallel v)\cdot (x\parallel y)\le v\cdot y\parallel u\cdot x$$

$$t\le t^{\prime }\stackrel{\text{defn}}{⟺}t+t^{\prime }=t^{\prime }.$$

$$x+x=x,x(y+z)=xy+xz,(y+z)x=yx+yz,$$

$$1+x{x}^{\ast }=1+x^{\ast }x=x^{\ast },$$

$$xy\le y\Rightarrow x^{\ast }y\le y,yx\le y\Rightarrow y{x}^{\ast }\le y,$$

$$S^{(0)}=1,S^{(1)}=S,S^{(2)}=S\parallel S,S^{(3)}=S\parallel S\parallel S,\dots$$

$$\{\begin{array}{ll}\text{sequential}& \text{if }p=q_1{q}_2\\ \text{parallel}& \text{if }p=q_1\parallel q_2\end{array}$$

$$\mathrm{Para}={\cup }_{i\ge 2}{\mathrm{Para}}_i$$

$$S=\{X\subseteq V|x\in X\wedge y\in V-X\Rightarrow \neg (x\le y\vee y\le x)\}.$$

$$[[\kappa (t)]]=\bigcup _{p\in [[t]]}[[\kappa (p)]]$$

$$[[\kappa (t)]]=[[\kappa (t_1{t}_2)]]=[[\kappa (t_1)\kappa (t_2)]]=[[\kappa (t_1)]][[\kappa (t_2)]]$$

$$(\bigcup _{p_1\in [[t_1]]}[[\kappa (p_1)]])(\bigcup _{p_2\in [[t_2]]}[[\kappa (p_2)]])=\bigcup _{p_1\in [[t_1]],p_2\in [[t_2]]}[[\kappa (p_1{p}_2)]]$$

$$[[\kappa (t)]]$$

$$\displaystyle=\bigcup_{n\geq 0}\Big{(}\big{(}\bigcup_{p_{1}\in\mathopen{[\![}s\mathclose{]\!]}}\mathopen{[\![}\kappa(p_{1})\mathclose{]\!]}\big{)}\ldots\big{(}\bigcup_{p_{n}\in\mathopen{[\![}s\mathclose{]\!]}}\mathopen{[\![}\kappa(p_{n})\mathclose{]\!]}\big{)}\Big{)}$$

$$=\bigcup _{n\ge 0}\bigcup _{\text{ each }{p}_i\in [[s]]}[[\kappa (p_1)]]\dots [[\kappa (p_n)]]=\bigcup _{n\ge 0}\bigcup _{q\in [[s{]]}^n}[[\kappa (q)]]$$

$$=\bigcup _{q\in [[s^{\ast }]]}[[\kappa (q)]],$$

$$\mathrm{depth}(p)=ma{x}_{i\le m}\mathrm{depth}(p_i)+1.$$

$$\mathrm{depth}(p)=ma{x}_{i\le n}\mathrm{depth}(q_i)+1.$$

$$u^{!}=u^{\ast }{u}^2,u^{(!)}=u^{(\ast )}\parallel u^{(2)}.$$

$$u+0=0+u\to u,u0=0u\to 0,0^{\ast }\to 1,$$

$$u^{\ast }=u^{!}+1+u,u^{(\ast )}=u^{(!)}+1+u,$$

$$u1=1u\to u,(u+1{)}^{!}=(1+u{)}^{!}\to u^{!}+1+u,$$

$$t{=}_{bi-KA}{t}^{\prime }+t^{\prime \prime }+t^{\prime \prime \prime }.$$

$$[[u\parallel v]]\cap {\mathrm{Para}}_i=\bigcup _{j+k=i}[[u]]\cap {\mathrm{Para}}_j\parallel [[v]]\cap {\mathrm{Para}}_k$$

$$depth(u\parallel v)\le \mathrm{depth}(u)+\mathrm{depth}(v)+1,$$

$$[[u^{(!)}]]\cap {\mathrm{Para}}_i=\bigcup _{j\le i}\bigcup _{2\le k_1+\cdots +k_j=i}[[u]]\cap {\mathrm{Para}}_{k_1}\parallel \cdots \parallel [[u]]\cap {\mathrm{Para}}_{k_j}$$

$$\mathrm{depth}(u^{(!)})\le \mathrm{depth}(u)+1$$

$$[[t_1]]=[[t_2]]⟺([[t_1]]-[[t_2]])\cup ([[t_2]]-[[t_1]])=\varnothing$$

$$[[t_i]]=\bigcup _{i\in N}[[s_N]],$$

$$\nu :T_{bi-KA}(L_U)\to T_{bi-KA}(\Sigma )$$

$$p\notin [[s]]\Rightarrow [[\nu (p)]]\cap [[\nu (s)]]=\varnothing$$

$$[[s]]\cap [[s^{\prime }]]=\varnothing \Rightarrow [[\nu (s)]]\cap [[\nu (s^{\prime })]]=\varnothing$$

$$\mathrm{depth}(\sum _{x\in {\cup }_{t\in T}{U}_t}x)<\mathrm{depth}(\sum _{x\in T}x)$$

Full text

An ideal of a pomset $p$ is a pomset using the letters of $p$, but having an ordering at least as strict as $p$. A bi-Kleene term $t$ thus defines the set $\operatorname{\textbf{{Id}}}(\mathopen{[\![}t\mathclose{]\!]})$ of ideals of pomsets in $\mathopen{[\![}t\mathclose{]\!]}$. We prove that if $t$ does not contain commutative iteration (∗) (in our terminology, $t$ is bw-rational) then $\operatorname{\textbf{{Id}}}(\mathopen{[\![}t\mathclose{]\!]})\cap\operatorname{\textbf{{Pom}}}_{sp}$, where $\operatorname{\textbf{{Pom}}}_{sp}$ is the set of pomsets generated from singleton pomsets using sequential and parallel multiplication ($\cdot$ and $\parallel$) is defined by a bw-rational term, and if two such terms $t,t^{\prime}$ define the same ideal language, then $t^{\prime}=t$ is provable from the Kleene axioms for $0,1,+,\cdot\,,^{*}$ plus the commutative idempotent semiring axioms for $0,1,+,\parallel$ plus the exchange law $(u\parallel v)\cdot(x\parallel y)\leq v\cdot y\parallel u\cdot x$.

1 Introduction

Pomsets may be regarded as a generalisation of both words over an alphabet and commutative words over an alphabet as studied by Conway [1, Chapter 11]. Words of the former kind are generated using sequential multiplication $(\cdot)$, whereas commutative words are generated using parallel multiplication $(\parallel)$. Both operations are defined on the set of pomsets. Pomsets have been widely used to model the behaviour of concurrent systems [2, 3, 4, 5, 6].

A pomset over an alphabet $\Sigma$ is defined by a finite labelled partially ordered set; that is, a finite partially ordered set (or poset) $V$ on which a labelling function into $\Sigma$ is defined. Since the focus is on the labelling rather than the elements of $V$, isomorphic labelled posets are regarded as defining the same pomset. For pomsets $p_{1},p_{2}$ defined by posets $V_{1},V_{2}$, the sequential and parallel products $p_{1}\cdot p_{2}$ and $p_{1}\parallel p_{2}$ are defined, respectively, by placing the elements of $V_{1}$ below those of $V_{2}$, and placing the elements of $V_{1}$ and $V_{2}$ side by side.

Given any monoid $(M,\cdot,1)$, the operation $\cdot$ can be extended pointwise to the power set $2^{M}$ of $M$, and if the regular operations $0,1,+,\cdot,^{*}$ are defined in the usual way for $2^{M}$ (in particular, $P^{*}=\cup_{i\geq 0}P^{i}$), then the algebra thus defined is an example of a Kleene algebra (Definition 1). Since the set of pomsets over an alphabet $\Sigma$ is a monoid with respect to the operations $\cdot,1$ and a commutative monoid with respect to $\parallel,1$, the class of languages (sets) of pomsets over $\Sigma$ is thus a bi-Kleene algebra with respect to the bi-Kleene operations $0,1,+,\cdot,^{*}\parallel,^{(*)}$, where parallel iteration (∗) is defined analogously to ∗, but using parallel multiplication. A pomset language is rational if is defined by a bi-Kleene term over an alphabet $\Sigma$. This is a simplification of the phrase series-parallel-rational used by Lodaya and Weil [7, 8]. If $t$ is a bi-Kleene term, then we use $\mathopen{[\![}t\mathclose{]\!]}$ to denote the language that it defines.

In this paper we prove the following theorems, for bi-Kleene terms $t,t^{\prime}$ over an alphabet $\Sigma$;

• •

The language $\mathopen{[\![}t\mathclose{]\!]}-\mathopen{[\![}t^{\prime}\mathclose{]\!]}$ is rational.

• •

It is decidable whether $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$ holds.

• •

If $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$ holds, then $t=t^{\prime}$ holds in every bi-Kleene algebra. Equivalently, the algebra of pomset languages generated by the bi-Kleene operations from the singleton pomsets with label in $\Sigma$ is the free bi-Kleene algebra with basis $\Sigma$.

This latter theorem is, in effect, a strengthening of Gischer [9, Theorem 4.3], in which neither of the two Kleene stars ${}^{*},\,^{(*)}$ was considered. Bi-Kleene algebras have been proposed as tools for the verification of concurrent programs [10]. Our completeness and decidability results can make reasoning about such programs simpler and less problematic.

1.1 New theorems for pomset ideals and bw-rational operations

Given a pomset $p$, an ideal of $p$ is a pomset that may be represented using the same vertex set as $p$, with the same labelling, but whose partial ordering is at least as strict as that for $p$. We write $\operatorname{\textbf{{Id}}}(L)$ for a pomset language $L$ to denote the set of ideals of elements of $L$. The function $\operatorname{\textbf{{Id}}}$ was first defined by Grabowski [11], who associated pomset ideals (that is, pomset languages closed under $\operatorname{\textbf{{Id}}}$) with a reachability condition between markings of a Petri net.

The class of pomset ideals over $\Sigma$ is a Kleene algebra with respect to the Kleene operations, but is not a Kleene algebra with respect to the commutative Kleene operations $0,1,+,\parallel,^{(*)}$, since $L\parallel L^{\prime}$ is not an ideal if $L,L^{\prime}\nsubseteq\{1\}$, but it can be made into a bi-Kleene algebra if $\parallel$ is interpreted as $(L,L^{\prime})\mapsto\operatorname{\textbf{{Id}}}(L\parallel L^{\prime})$ and parallel iteration (∗) is defined analogously. Additionally, the class of pomset ideals satisfies the exchange law:

[TABLE]

where we use the abbreviation

[TABLE]

We have failed to prove an analogous result for ideals to the freeness theorem given for pomset languages above, but by abandoning the parallel iteration operation (∗) we have the following partial results. We will refer to $0,1,+,\cdot,^{*}\parallel$ as bw-rational operations (‘bw’ meaning bounded width) and we call algebras over the bw-rational operations that satisfy both the Kleene axioms for $0,1,+,\cdot,^{*}$ and the idempotent commutative semiring axioms for $0,1,+,\parallel$ bw-rational algebras and refer to a term in the bw-rational operations as a bw-rational term. We say that a pomset is series-parallel if it is generated from the set of singleton pomsets using only sequential and parallel multiplication, and use $\operatorname{\textbf{{Pom}}}_{sp}$ to denote the set of series-parallel pomsets. With these definitions, we prove for bw-rational terms $t,t^{\prime}$ over an alphabet $\Sigma$ that

• •

the language $\operatorname{\textbf{{Id}}}(\mathopen{[\![}t\mathclose{]\!]})\cap\operatorname{\textbf{{Pom}}}_{sp}$ is representable by a bw-rational term, and

• •

suppose that $\operatorname{\textbf{{Id}}}(\mathopen{[\![}t\mathclose{]\!]})=\operatorname{\textbf{{Id}}}(\mathopen{[\![}t^{\prime}\mathclose{]\!]})$, or equivalently $\operatorname{\textbf{{Id}}}(\mathopen{[\![}t\mathclose{]\!]})\cap\operatorname{\textbf{{Pom}}}_{sp}=\operatorname{\textbf{{Id}}}(\mathopen{[\![}t^{\prime}\mathclose{]\!]})\cap\operatorname{\textbf{{Pom}}}_{sp}$. Then $t=t^{\prime}$ is a consequence of the bw-rational axioms plus the exchange law (1). Hence the algebra of pomset ideals generated by the bi-Kleene operations from the singleton pomsets with labels in $\Sigma$ is the free algebra with basis $\Sigma$ with respect to the class of bw-rational algebras satisfying the exchange law.

This freeness result is, in effect, a generalisation of Gischer [9, Theorem 5.9], which gave the analogous result for idempotent bi-semirings, in which the Kleene star ∗ was not considered.

1.2 Organisation of the paper

In Section 2, we give most of the basic definitions and results that will be used throughout the paper. In Section 3, we prove our first main theorem for rational pomset languages; in particular, we show that if $L,L^{\prime}$ are rational languages, then so is $L\setminus L^{\prime}$. We also show that a bi-Kleene term defining $L\setminus L^{\prime}$ can be computed from terms defining $L$ and $L^{\prime}$. In Section 4, we prove our second main theorem; that if two bi-Kleene terms define the same rational language, then they define the same element of every bi-Kleene algebra. In Section 8, we give further definitions for pomset ideals. We also prove that the set of pomset ideals defines a bi-Kleene algebra, provided that the operations $\parallel,\,^{(*)}$ are suitably modified. Section 5.1 gives a summary of the method of proof of our remaining theorems, which occupies Sections 6–8. In Section 9 we give our conclusions.

2 Kleene algebra and pomset definitions

Definition 1** (bi-Kleene algebras and bw-rational algebras)**

A monoid, as usual, is an algebra with an associative binary operation $\cdot$ and identity $1$. A bimonoid is an algebra with operations $\cdot,\parallel,1$ that is a monoid with respect to $\cdot,1$ and a commutative monoid with respect to $\parallel,1$.

A Kleene algebra is an algebra $K$ with constants $0,1$, a binary addition operation $+$, a multiplication operation $\cdot$ (usually omitted) and a unary iteration operation ∗, such that the following hold; $(K,1,\cdot)$ is a monoid, $(K,0,+)$ is a commutative monoid and also, for all $x,y,z\in K$,

[TABLE]

where (2) is assumed. The identities (5) are normally called the induction axioms. The identities in (3) together with the preceding conditions amount to stating that $K$ is an idempotent semiring, or dioid. We say that $K$ is a commutative Kleene algebra if $\cdot$ is commutative.

A bi-Kleene algebra is an algebra with operations $0,1,+,\cdot,^{*},\parallel,^{(*)}$ that is a Kleene algebra with respect to $0,1,+,\cdot,^{*}$ and a commutative Kleene algebra with respect to $0,1,+,\parallel,^{(*)}$, with $\parallel$ and (∗) playing the role of $\cdot$ and ∗ respectively in the Kleene axioms given above. For the purposes of this paper, we need to define bw-rational algebras, which have operations $0,1,+,\cdot,^{*},\parallel,$ and satisfy only the conditions on the definition of a bi-Kleene algebra given above that do not mention (∗); thus, a bw-rational algebra is a Kleene algebra with respect to $0,1,+,\cdot,^{*}$ and is a commutative idempotent semiring with respect to the operations $0,1,+,\parallel$; that is, it satisfies (3) with $\cdot$ replaced by $\parallel$ and is a commutative monoid with respect to $1,\parallel$.

Given a set $\Sigma$, we use $T_{Reg}(\Sigma)$, $T_{ComReg}(\Sigma)$, $T_{bimonoid}(\Sigma)$, $T_{bi-KA}(\Sigma)$, and $T_{bw-Rat}(\Sigma)$ to denote the sets of terms generated from $\Sigma$ using, respectively, the regular operations $0,1,+,\cdot,^{*}$, the commutative-regular operations $0,1,+,\parallel,^{(*)}$, the bimonoid operations $1,\cdot,\parallel$, the bi-Kleene operations $0,1,+,\cdot,^{*},\parallel,^{(*)}$ and the bw-rational operations $0,1,+,\cdot,^{*},\parallel$.

An important class of naturally arising Kleene algebras is given by Proposition 2.

Proposition 2** (Kleene algebras defined on power sets of monoids)**

Let

$(M,1,\cdot)$ be a monoid. Then $(2^{M},0,1,+,\cdot,^{*})$, with [math] defining $\emptyset$, $1$ defining $\{1\}$, $+$ defining union, $\cdot$ given by pointwise multiplication and $S^{*}\overset{\text{defn}}{=}\cup_{i\geq 0}S^{i}$, is a Kleene algebra.

*Proof. * Straightforward. ∎

Definition 3** (commutative words)**

A commutative word over an alphabet $\Sigma$ is a multiset over $\Sigma$; that is, a function from $\Sigma$ into the set of non-negative integers. A commuting word may be represented by a word $\sigma_{1}\parallel\cdots\parallel\sigma_{m}$ with each $\sigma_{i}\in\Sigma$, with two such words representing the same commutative word if and only if for each $\sigma\in\Sigma$, they contain the same number of occurrences of $\sigma$. Thus the set of commutative words forms a commutative monoid with $\parallel$ as multiplication and the empty word $1$ as identity.

It follows from Proposition 2 that the set of languages of strings over an alphabet $\Sigma$ is a Kleene algebra, and the set of languages of commutative words over $\Sigma$ is a commutative Kleene algebra with respect to the commutative-regular operations $0,1,+,\parallel,^{(*)}$, when these are interpreted as given in the Proposition; in particular, $S^{(*)}=\cup_{i\geq 0}S^{(i)}$, where we define

[TABLE]

Definition 4** (pomsets and the $\operatorname{supp}$ function)**

A labelled partial order is a $3$-tuple $(V,\leq,\mu)$, where $V$ is a set of vertices, $\leq$ is a partial ordering on the set $V$ and $\mu:V\to\Sigma$ for an alphabet $\Sigma$ is a labelling function. Two labelled partial orders $(V,\leq,\mu)$ and $(V^{\prime},\leq^{\prime},\mu^{\prime})$ are isomorphic if there is a bijection $\tau:V\to V^{\prime}$ that preserves ordering and labelling; that is, for $v,w\in V$, $v\leq w\iff\tau(v)\leq^{\prime}\tau(w)$ and $\mu(v)=\mu^{\prime}(\tau(v))$ holds. A pomset is an isomorphism class of finite labelled partial orders, and a set of pomsets is usually called a language. We write $\operatorname{\textbf{{Pom}}}(\Sigma)$ to denote the set of all pomsets with labels in an alphabet $\Sigma$. If $p$ is a pomset, then $\operatorname{supp}(p)$ is the set of labels occurring in $p$, and if $L$ is a pomset language, then we define $\operatorname{supp}(L)=\cup_{p\in L}\operatorname{supp}(p)$.

Observe that a pomset whose ordering $\leq$ is total is simply a word, in the usual sense, over its labelling alphabet $\Sigma$. Thus the word $\sigma$ of length one for $\sigma\in\Sigma$ is the pomset with a single vertex having label $\sigma$. On the other hand, a pomset over $\Sigma$ whose order relation is empty is, in effect, a commutative word $\sigma_{1}\parallel\ldots\parallel\sigma_{m}$ with each $\sigma_{i}\in\Sigma$.

Definition 5** (sequential and parallel multiplication of pomsets)**

For pomsets $p_{1},p_{2}$ represented by the $3$-tuples $(V_{1},\leq_{1},\mu_{1})$ and $(V_{2},\leq_{2},\mu_{2})$ respectively, their sequential product $p_{1}\cdot p_{2}$ and parallel product $p_{1}\parallel p_{2}$ are given as follows; these definitions can easily be shown to be well-defined; that is, independent of the choice of representative $3$-tuple of each pomset $p_{i}$.

• •

$p_{1}\cdot p_{2}$ (usually written simply $p_{1}p_{2}$) is represented by the $3$-tuple $(V_{1}\cup V_{2},\ll,\mu)$, where the function $\mu$ agrees with each function $\mu_{i}$ on the set $V_{i}$ and $v\ll w$ holds if and only if either both vertices $v,w$ lie in one set $V_{i}$ for $i\in\{1,2\}$ and $v\leq_{i}w$ holds, or $v\in V_{1}$ and $w\in V_{2}$.

• •

the pomset $p_{1}\parallel p_{2}$ is represented by the $3$-tuple $(V_{1}\cup V_{2},\prec,\eta)$, where the function $\eta$ agrees with each function $\mu_{i}$ on the set $V_{i}$ and $v\prec w$ holds if and only if both vertices $v,w$ lie in one set $V_{i}$ for $i\in\{1,2\}$.

2.1 The bi-Kleene algebra of pomset languages

It follows from Proposition 2 that the set of pomset languages over $\Sigma$ is a bi-Kleene algebra when equipped with the constant operations $0,1$, the operations $+,\,\cdot,\,\parallel$ of arity two and the operations ∗ and (∗) of arity one, with interpretations as given in the Proposition; in particular, $1$ denotes the singleton containing the empty pomset, also denoted by $1$, whose vertex set is empty, the sequential and parallel products of pomset languages are defined from those of pomsets by pointwise extension, and for a pomset language $P$, we define $P^{*}=\bigcup_{i\geq 0}P^{i}$ and $P^{(*)}=\bigcup_{i\geq 0}P^{(i)}$, where $P^{(i)}$ is defined as indicated in (6).

2.2 Series-parallel pomsets and rational pomset languages

For an alphabet $\Sigma$ and $\sigma\in\Sigma$, we use $\sigma$ to refer to the pomset having only one vertex with label $\sigma$, and for any $t\in T_{bi-KA}(\Sigma)$, we write $\mathopen{[\![}t\mathclose{]\!]}$ to denote the pomset language defined by $t$, with operations interpreted as above. Thus if $t\in T_{Reg}(\Sigma)$ then $\mathopen{[\![}t\mathclose{]\!]}$ is regular; by analogy, if $t\in T_{ComReg}(\Sigma)$ then we say that $\mathopen{[\![}t\mathclose{]\!]}$ is commutative-regular. If a pomset $p$ satisfies $\{p\}=\mathopen{[\![}t\mathclose{]\!]}$ for $t\in T_{bimonoid}(\Sigma)$, then we say that $p$ is a series-parallel pomset. We write $\operatorname{\textbf{{Pom}}}_{sp}$ and $\operatorname{\textbf{{Pom}}}_{sp}(\Sigma)$ to denote, respectively, the set of all series-parallel pomsets and the set of all series-parallel pomsets with labels in $\Sigma$. Fig. 1 gives an example of a pomset that does not lie in $\operatorname{\textbf{{Pom}}}_{sp}$.

We say that a pomset language $L$ is rational if $L=\mathopen{[\![}t\mathclose{]\!]}$ for $t\in T_{bi-KA}(\Sigma)$; if $t\in T_{bw-Rat}(\Sigma)$, we say that $L$ is bw-rational. The following freeness results for the algebras of regular and commutative-regular languages have been proved.

Theorem 6

Let $\Sigma$ be an alphabet. If $t,t^{\prime}\in T_{Reg}(\Sigma)$ and $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$ holds, then $t=t^{\prime}$ holds in every Kleene algebra. If instead, $t,t^{\prime}\in T_{ComReg}(\Sigma)$ and $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$ holds, then $t=t^{\prime}$ holds in every commutative Kleene algebra.

*Proof. * The assertion for regular languages was proved by Kozen [12]. For commutative-regular languages, the result is implicit in the work of Conway [1, chap.11]. ∎

Definition 7** (parallel and sequential pomset languages)**

A pomset $p$ is

[TABLE]

for pomsets $q_{1},q_{2}$ with each $q_{i}\not=1$ in each case. A pomset language $L$ is sequential if every element of $L$ is sequential and non-sequential if none of its elements are sequential; we define a language to be parallel analogously. We define $\operatorname{\textbf{{Seq}}}$ and $\operatorname{\textbf{{Para}}}$ to be the language of all sequential and parallel pomsets respectively. Further, for any $i\geq 1$ we define the language $\operatorname{\textbf{{Para}}}_{i}=\{q_{1}\parallel\cdots\parallel q_{i}|\,\text{each }q_{i}\not=1\text{ and not parallel}\}$. Thus

[TABLE]

holds.

2.3 The bi-Kleene algebra of rational pomset languages is free with respect to bi-Kleene algebras defined by power sets of bimonoids

Lemma 8 shows that a pomset cannot be both sequential and parallel, and hence a sequential pomset language and a parallel pomset language do not intersect.

Lemma 8

Let $p_{1},p_{2},q_{1},q_{2}$ be pomsets and suppose that each $p_{i}\not=1,q_{j}\not=1$. Then $p_{1}\parallel p_{2}\not=q_{1}q_{2}$ holds.

*Proof. * Suppose that $p_{1}\parallel p_{2}=q_{1}q_{2}$ holds, and let $(Z,\leq)$ be a poset defining $q_{1}q_{2}$. Thus $Z$ can be partitioned non-trivially as $Z=V_{1}\uplus V_{2}=W_{1}\uplus U_{2}$, where $x_{1}\leq x_{2}$ if each $x_{i}\in V_{i}$ and $y_{1},y_{2}$ are incomparable with respect to $\leq$ if each $y_{i}\in W_{i}$. Suppose $W_{1}\subseteq V_{2}$; then $W_{2}\supseteq V_{1}$, giving a contradiction since the sets $V_{i},W_{i}$ are non-empty and so $W_{1}\cap V_{2},\,W_{2}\cap V_{1}\not=\emptyset$. Thus $W_{1}\nsubseteq V_{2}$ and so $W_{1}\cap V_{1}\not=\emptyset$. Similarly $W_{2}\cap V_{2}\not=\emptyset$ also holds, again giving a contradiction. Thus the conclusion follows. ∎

Lemma 9** (uniqueness of pomset decomposition)**

**

1. (1)

Let $p_{1}\parallel\cdots\cdots\parallel p_{m}=q_{1}\parallel\cdots\cdots\parallel q_{n}$ be a pomset and assume that no pomset $p_{i}$ or $q_{j}$ is parallel. Then $m=n$ and there is a permutation $\theta$ on $\{1,\ldots,m\}$ such that each $p_{i}=q_{\theta(i)}$. 2. (2)

Let $p_{1}\ldots\ldots p_{m}=q_{1}\ldots\ldots q_{n}$ be a pomset and assume that no pomset $p_{i}$ or $q_{j}$ is sequential. Then $m=n$ and each $p_{i}=q_{i}$.

*Proof. * (2) is proved in Gischer [9, Lemma 3.2]. (1) is proved as follows. Let $(V,\leq)$ be a poset defining $p_{1}\parallel\ldots\ldots\parallel p_{m}$. We may assume that $V\not=\emptyset$ since otherwise the conclusion is obvious. We may define the partition $V=V_{1}\uplus\ldots\uplus V_{m}$, where each pomset $p_{i}$ is defined by $V_{i}\not=\emptyset$ and the restriction of $\leq$ to $V_{i}$. Similarly, $V=W_{1}\uplus\ldots\uplus W_{n}$, where each pomset $q_{i}$ is defined by $W_{i}\not=\emptyset$ and the restriction of $\leq$ to $W_{i}$. Define the collection

[TABLE]

Clearly $X,Y\in S\Rightarrow X\cap Y\in S$ holds. Owing to the indecomposability conditions on $p_{i}$ and $q_{j}$, the sets $V_{i},W_{j}$ are minimal non-empty elements of $S$ and so $V_{i}\cap W_{j}\not=\emptyset\Rightarrow V_{i}=W_{j}$ holds, proving the result. ∎

Corollary 10 states that the pomset language defined by $T_{bimonoid}(\Sigma)$ is the free bimonoid over $\Sigma$.

Corollary 10

Let $\Sigma$ be an alphabet, let $M$ be a bimonoid and let $\kappa:T_{bimonoid}(\Sigma)\to M$ be a homomorphism of the bimonoid operations. Let $t,t^{\prime}\in T_{bimonoid}(\Sigma)$ with $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$. Then $\kappa(t)=\kappa(t^{\prime})$ holds.

*Proof. * Using Theorem 8 and Lemma 9 it follows by induction on the structure of $t$ that $t=t^{\prime}$ holds in any bimonoid, and hence in $M$. ∎

Our main result of the subsection follows.

Lemma 11

Let $\Sigma$ be an alphabet, let $M$ be a bimonoid and let $\kappa:T_{bi-KA}(\Sigma)\to 2^{M}$ be a homomorphism of the bi-Kleene operations. Suppose we extend $\kappa$ to $\operatorname{\textbf{{Pom}}}_{sp}(\Sigma)$ by defining $\kappa(p)=\kappa(t)$ for any $t\in T_{bimonoid}(\Sigma)$ with $\mathopen{[\![}t\mathclose{]\!]}=\{p\}$ (well-defined by Corollary 10). Let $t\in T_{bi-KA}(\Sigma)$. Then

[TABLE]

holds. In particular, $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}\Rightarrow\kappa(t)=\kappa(t^{\prime})$ holds, and hence $\kappa$ defines a bi-Kleene homomorphism from \big{\{}\mathopen{[\![}t\mathclose{]\!]}\big{|}\,t\in T_{bi-KA}(\Sigma)\big{\}} into $2^{M}$.

*Proof. * The displayed equation follows by induction on the structure of $t$. If $t\in\Sigma\cup\{0,1\}$ then the equality is obvious, and the case where $t=t_{1}+t_{2}$ is straightforward. We now consider the remaining cases.

• •

Suppose that $t=t_{1}t_{2}$. Then

[TABLE]

follows, using the inductive hypothesis for each $t_{i}$ at the fourth equality.

• •

Suppose that $t=s^{*}$. Then

[TABLE]

using the inductive hypothesis at the second equality.

The cases where $t=t_{1}\parallel t_{2}$ or $t=s^{(*)}$ are similar to those above, hence the conclusion holds. ∎

Lemma 11 has analogues for $T_{Reg}(\Sigma)$ and monoids, and $T_{ComReg}(\Sigma)$ and commutative monoids, and these have similar proofs.

2.4 Depth of a series-parallel pomset

In order to prove our main theorems, we need to find a quasi-partial order on bi-Kleene terms in such a way that a parallel term is preceded by its sequential subterms and ground subterms (and the analogous statement with sequential and parallel interchanged also holds) and this ordering is determined by the language that a term defines. Therefore, we first define the depth of a pomset, and then extend this definition to bi-Kleene terms.

Definition 12** (depth of a series-parallel pomset)**

Let $p\in\operatorname{\textbf{{Pom}}}_{sp}$. Then we define $\operatorname{depth}(p)\in\mathbb{N}$ recursively as follows.

• •

If $p$ is a singleton pomset or $p=1$, then $\operatorname{depth}(p)=0$.

• •

If $p=p_{1}\parallel\ldots\ldots\parallel p_{m}$ for $m\geq 2$ and each $p_{i}$ is a singleton pomset or is sequential, then

[TABLE]

• •

If $p=q_{1}\ldots\ldots q_{n}$ for $n\geq 2$ and each $q_{i}$ is a singleton pomset or is sequential, then

[TABLE]

Owing to Lemma 9 and Lemma 8, this is a valid definition.

Definition 13** (width of a pomset)**

The width of a pomset $p$, $\operatorname{width}(p)$, is the maximal cardinality of any set of wholly unordered vertices in a representation of $p$. If $L$ is a pomset language then $\operatorname{width}(L)$ is the maximum width of any pomset in $L$, if this is defined, in which case we say that $L$ has bounded width; otherwise we define $\operatorname{width}(L)=\infty$. We also define $\operatorname{width}(t)=\operatorname{width}(\mathopen{[\![}t\mathclose{]\!]})$ for a bi-Kleene term $t$.

Observe that if $t\in T_{bi-KA}(\Sigma)$ and $\mathopen{[\![}t\mathclose{]\!]}$ has bounded width, then $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$ for some $t^{\prime}\in T_{bw-Rat}(\Sigma)$, since any subterm $s^{(*)}$ of $t$ can be replaced by the term $\sum_{i=0}^{\operatorname{width}(t)}s^{(i)}$, thus eliminating occurences of (∗) from $t$. Conversely, every term in $T_{bw-Rat}(\Sigma)$ defines a language of bounded width. This justifies our bw-rational terminology.

2.5 Standardising terms using the bi-Kleene axioms

In this subsection we will show that the parallel and sequential subsets of a rational language are rational, and definable by terms that can be computed. There is a difficulty, however, with the usual Kleene operations in that the way to partition a rational language into its parallel, sequential and other pomsets is not clearly indicated by the highest-level operation that defines it; for example, a language $\mathopen{[\![}t^{*}\mathclose{]\!]}$ may contain both parallel and sequential pomsets. Therefore we consider new unary operations !, (!) that will not be used outside this subsection. They are defined by

[TABLE]

Definition 14 gives the relations between terms with which our main theorems will be expressed.

Definition 14** (The $=_{bi-KA}$ and $=_{bw-Rat}$relations)**

Let $\Sigma$ be an alphabet and let $t,t^{\prime}\in T_{bi-KA}(\Sigma)$. We say that $t=_{bi-KA}t^{\prime}$ if $t=t^{\prime}$ holds in every bi-Kleene algebra. If $t,t^{\prime}\in T_{bw-Rat}(\Sigma)$, then we say $t=_{bw-Rat}t^{\prime}$ if $t=t^{\prime}$ holds in every bw-rational algebra. We also define the partial orderings $\leq_{bi-KA}$ and $\leq_{bw-Rat}$ by analogy with (2).

Proposition 15 shows the use of defining the new operations given in (7).

Proposition 15

Let $\Sigma$ be an alphabet and let $t$ be a term over $\Sigma$ with operations in $\{+,\cdot,^{!},\parallel,^{(!)}\}$. We extend the definition of the language $\mathopen{[\![}t\mathclose{]\!]}$ by interpreting ${}^{!},^{(!)}$ as given in (7). Then $1\notin\mathopen{[\![}t\mathclose{]\!]}$; also, if the term $t=uv$ or $t=u^{!}$, then $\mathopen{[\![}t\mathclose{]\!]}$ is a sequential language, and an analogous assertion holds for the operations $\parallel,\,^{(!)}$.

*Proof. * The proof that $1\notin\mathopen{[\![}t\mathclose{]\!]}$ follows by induction on the structure of $t$; in particular, it follows from (7) that $1\notin\mathopen{[\![}r\mathclose{]\!]}\Rightarrow 1\notin\mathopen{[\![}r^{!}\mathclose{]\!]},$ and analogously for $r^{(!)}$, if $r$ has operations in $\{+,\cdot,\parallel,^{!},^{(!)}\}$. The remaining assertions follow by applying this result to $u$ and $v$. ∎

Proposition 16

Let $\Sigma$ be an alphabet and let $t\in T_{bi-KA}(\Sigma)$. Suppose the relation $=_{bi-KA}$ is extended to terms containing the unary operations ${}^{!},^{(!)}$ by assuming the substitutions indicated by (7). Then there is a term $t^{\prime}$ with operations in $\{0,1,+,\cdot,\parallel,^{!},^{(!)}\}$ satisfying $t=_{bi-KA}t^{\prime}$ such that either $t^{\prime}=0$ or [math] does not occur in $t^{\prime}$ and $1$ does not occur in the argument of any operation except possibly $+$ in $t^{\prime}$.

*Proof. * By using the Kleene-valid substitutions

[TABLE]

and their parallel analogues, we may assume that either $t=0$ or [math] does not occur in $t$. We now eliminate the iteration operations ${}^{*},^{(*)}$ from $t$ by replacing them with new unary operations !, (!) respectively using the following identities;

[TABLE]

which follow from (7) plus the Kleene axioms. If $t\not=0$, then by using the distributive laws and the substitutions

[TABLE]

which follow from the Kleene axioms plus (7), and their parallel analogues, we can ensure that $1$ does not occur in the resulting term in the argument of any operation except possibly $+$, thus proving the result. ∎

We are now able to show that a rational language can be expressed as a sum of terms representing its sequential, parallel and remaining pomsets.

Lemma 17

Let $\Sigma$ be an alphabet and let $t\in T_{bi-KA}(\Sigma)$. Then the pomset languages $\mathopen{[\![}t\mathclose{]\!]}\cap\operatorname{\textbf{{Para}}}_{i}$ for each $i\geq 1$ are rational and definable by terms that are computable from $t$; and there exist terms $t^{\prime},t^{\prime\prime},t^{\prime\prime\prime}\in T_{bi-KA}(\Sigma)$ that that are computable from $t$ and define pomset languages $\mathopen{[\![}t\mathclose{]\!]}\cap\operatorname{\textbf{{Seq}}}$, $\mathopen{[\![}t\mathclose{]\!]}\cap\operatorname{\textbf{{Para}}}$ and $\mathopen{[\![}t\mathclose{]\!]}\cap(\Sigma\cup\{1\})$ and satisfy

[TABLE]

Furthermore, $\operatorname{depth}(t)<\infty$.

*Proof. * By Proposition 16, we may assume that either $t=0$ or $1$ does not occur in $t$ in the argument of any operation except possibly $+$, and $t$ has operations lying in $\{1,+,\cdot,\parallel,^{!},^{(!)}\}$. We prove the results (apart from the computability assertions, which follow immediately) for the set of terms $t$ satisfying these conditions by induction on the structure of $t$, and we can then reinstate the operations ${}^{*},^{(*)}$ in $t^{\prime},t^{\prime\prime},t^{\prime\prime\prime}$ using (7).

If $t\in\Sigma\cup\{0,1\}$ then the results are immediate. If $t=t_{1}+t_{2}$ then the results follow from the inductive hypothesis applied to each $t_{j}$.

If $t=u\parallel v$ then by Proposition 15 the term $t$ is parallel and so $L=L\cap\operatorname{\textbf{{Para}}}$ holds; also,

[TABLE]

and

[TABLE]

proving the rationality assertion for the languages $\mathopen{[\![}t\mathclose{]\!]}\cap\operatorname{\textbf{{Para}}}_{i}$ and the depth assertion for $t$ by the inductive hypothesis. The case $t=uv$ is analogous.

If instead $t=u^{(!)}$ then again by Proposition 15, $t$ is parallel and so $L=L\cap\operatorname{\textbf{{Para}}}$ holds; also,

[TABLE]

and

[TABLE]

proving the rationality assertion for the languages $\mathopen{[\![}t\mathclose{]\!]}\cap\operatorname{\textbf{{Para}}}_{i}$ and the depth assertion for $t$ by the inductive hypothesis. The case $t=u^{!}$ is analogous. ∎

Proposition 18 will be an essential tool for proving assertions on bi-Kleene terms by induction on the depth of their languages.

Proposition 18

*Let $\Sigma$ be an alphabet and let $t\in T_{bi-KA}(\Sigma)$. If $t$ is parallel, then $t=_{bi-KA}c(u_{1},\ldots,u_{m})$ for a commutative-regular term $c$ and terms $u_{i}\in T_{bi-KA}(\Sigma)$ defining non-empty languages that are either sequential or lie in $\Sigma$, and satisfy

$\operatorname{depth}(u_{i})<\operatorname{depth}(t)$, with $c$ and each $u_{i}$ being computable from $t$.*

*Proof. * By Proposition 16, we may assume that either $t=0$, or $t$ contains only the operations $1,+,\cdot,^{!},\parallel,^{(!)}$, with $1$ not occurring in the argument of any operation in $t$ except possibly $+$. If $t=0$ then the conclusion is obvious, so we assume the latter case. Since $t$ is parallel, this implies that $1$ does not occur at all in $t$. Thus $t$ has the form $c(u_{1},\ldots,u_{m})$ for a term $c$ with operations in $\{+,\parallel,^{(!)}\}$ and terms $u_{i}$ that either lie in $\Sigma$ or have the form $uv$ or $u^{!}$ and are hence sequential by Proposition 15, and define non-empty languages. For each $j\leq m$, let $p_{j}$ be a pomset in $\mathopen{[\![}u_{j}\mathclose{]\!]}$ of maximal depth. We may assume that each $u_{i}$ actually occurs in $t$. Let $i\leq m$. Thus for an alphabet $\{\sigma_{1},\ldots,\sigma_{m}\}$, the language $\mathopen{[\![}c(\sigma_{1},\ldots,\sigma_{m})\mathclose{]\!]}$ contains a parallel word $w$ of width $\geq 2$ in which $\sigma_{i}$ occurs, and so the pomset language $\mathopen{[\![}t\mathclose{]\!]}$ contains $w(\sigma_{j}\setminus p_{j}|\,j\leq m)$, whose depth is greater than that of $u_{i}$, proving the depth assertion. By reinstating ∗ and (∗) in each $u_{i}$ and (∗) in $c$ using (7), we get the result required. ∎

2.6 Regular and commutative-regular languages are closed under boolean operations

Theorem 19 recalls the fact that our first main theorem is known to hold for the subclasses of regular and commutative-regular languages.

Theorem 19

Let $\Sigma$ be an alphabet and let $t_{1},t_{2}\in T_{Reg}(\Sigma)$, or alternatively $t_{1},t_{2}\in T_{ComReg}(\Sigma)$. Then there exists a term $s\in T_{Reg}(\Sigma)$ or $T_{ComReg}$, respectively, such that $\mathopen{[\![}s\mathclose{]\!]}=\mathopen{[\![}t_{1}\mathclose{]\!]}-\mathopen{[\![}t_{2}\mathclose{]\!]}$. Furthermore, $s$ can be computed from $t_{1}$ and $t_{2}$.

*Proof. * If each term $t_{i}$ is regular, then the conclusion is a well-known theorem for regular languages. If each term $t_{i}$ is commutative-regular, then it follows from Conway [1, Chapter 11], the computability result being an implicit consequence of his method of proof. ∎

Corollary 20

Let $\Sigma$ be an alphabet and let $t_{1},t_{2}$ be both regular or both commutative-regular terms over $\Sigma$. Then it is decidable whether $\mathopen{[\![}t_{1}\mathclose{]\!]}=\mathopen{[\![}t_{2}\mathclose{]\!]}$ holds.

*Proof. * This follows since

[TABLE]

holds, and it is clearly possible to decide whether an element of $T_{bi-KA}(\Sigma)$ defines the empty language. ∎

Corollary 21

Let $\Sigma$ be an alphabet and let $T$ be a finite set of elements of $T_{bi-KA}(\Sigma)$ that are either all regular or all commutative-regular. Then there exists a finite set $U$ of terms, pairs of which define disjoint languages, and such that for each $t\in T$, there exists $V_{t}\subseteq U$ such that $\mathopen{[\![}t\mathclose{]\!]}=\bigcup_{x\in V_{t}}\mathopen{[\![}x\mathclose{]\!]}$ holds. Furthermore, the set $U$ can be computed from $T$, as can the subset $V_{t}$ from $T$ and $t$.

*Proof. * Write $T=\{t_{1},\ldots,t_{n}\}$. By Theorem 19, for each $N\subseteq\{1,\ldots,n\}$, we may define a term $s_{N}$ satisfying $\mathopen{[\![}s_{N}\mathclose{]\!]}=\bigcup_{i\in N}\mathopen{[\![}t_{i}\mathclose{]\!]}-\bigcup_{i\notin N}\mathopen{[\![}t_{i}\mathclose{]\!]}$, and $M\not=N\Rightarrow\mathopen{[\![}s_{M}\mathclose{]\!]}\cap\mathopen{[\![}s_{N}\mathclose{]\!]}=\emptyset$ holds. Clearly

[TABLE]

thus proving the Corollary, since from Theorem 19, the terms $s_{N}$ can clearly be computed from $T$. ∎

3 Closure of rational pomset languages under Boolean operations

In this section we prove our first main theorem.

3.1 The label set $L_{U}$ and function $\nu$

For the remainder of this section, and in Section 4, Definition 22 will be assumed.

Definition 22** (associating a label with a term, the function $\nu$)**

For any term $u$, we assume a label $l_{u}$, where distinct terms define distinct labels, and for any set $U$ of terms over an alphabet $\Sigma$, we define $L_{U}=\{l_{u}|\,u\in U\}$. We also define the homomorphism

[TABLE]

given by $\nu(l_{u})=u$. Further, for any $p\in\operatorname{\textbf{{Pom}}}_{sp}(L_{U})$, we define $\nu(p)=\nu(t)$, where $t\in T_{bimonoid}(L_{U})$ satisfies $\mathopen{[\![}t\mathclose{]\!]}=\{p\}$ (well-defined by Corollary 10).

Note: the assertions of Proposition 18, Lemma 23 and Corollary 24, and Lemma 28 in Section 4 have their counterparts with references to sequential and parallel multiplication interchanged, and these have analogous proofs.

Lemma 23

Let $\Sigma$ be an alphabet and let $U$ be a set of elements of $T_{bi-KA}(\Sigma)$ such that every element of $U$ either lies in $\Sigma$ or is sequential. Assume that distinct terms in $U$ define disjoint languages. Let $p$ be a parallel product of elements of $L_{U}$ and let $s\in T_{ComReg}(L_{U})$. Then

[TABLE]

holds.

*Proof. * Order the terms $s$, firstly by the total number of occurrences of $+$ and (∗), and secondly by the number of occurrences of $\parallel$. Assume that $p\notin\mathopen{[\![}s\mathclose{]\!]}$ holds. We prove $\mathopen{[\![}\nu(p)\mathclose{]\!]}\cap\mathopen{[\![}\nu(s)\mathclose{]\!]}=\emptyset$ by induction using this ordering.

• •

Suppose that $s\in L_{U}$. If the commutative word $p\notin L_{U}\cup\{1\}$, then we may write $p=q\parallel q^{\prime}$ for $q,q^{\prime}\not=1$ and hence $\nu(p)=\nu(q)\parallel\nu(q^{\prime})$ is a parallel term, whereas no elements of $\mathopen{[\![}\nu(s)\mathclose{]\!]}$ are parallel, proving $\mathopen{[\![}\nu(p)\mathclose{]\!]}\cap\mathopen{[\![}\nu(s)\mathclose{]\!]}=\emptyset$. On the other hand, if $p\in L_{U}$ or $p=1$, then $\mathopen{[\![}\nu(p)\mathclose{]\!]}\cap\mathopen{[\![}\nu(s)\mathclose{]\!]}=\emptyset$ follows, respectively, from the disjointness assumption on the elements of $U$ or the fact that $1\notin\mathopen{[\![}u\mathclose{]\!]}$ for all $u\in U$.

• •

Suppose $s=s_{1}+s_{2}$. The conclusion follows by the inductive hypothesis applied to each term $s_{i}$.

• •

Suppose $s=s_{1}\parallel s_{2}$. Write $p=l_{u_{1}}\parallel\ldots\parallel l_{u_{m}}$ with each $u_{i}\in U$. Assume the conclusion is false for $s$; thus there are pomsets $q_{i}\in\mathopen{[\![}\nu(s_{i})\mathclose{]\!]}$ such that $q_{1}\parallel q_{2}\in\mathopen{[\![}\nu(p)\mathclose{]\!]}\cap\mathopen{[\![}\nu(s)\mathclose{]\!]}$. Since every element of every set $\mathopen{[\![}u_{i}\mathclose{]\!]}$ is not parallel and not $1$, after rearrangement of the labels $l_{u_{i}}$ we may write $q_{1}=v_{1}\parallel\ldots\parallel v_{n}$ and $q_{2}=v_{n+1}\parallel\ldots\parallel v_{m}$ with each pomset $v_{i}\in\mathopen{[\![}u_{i}\mathclose{]\!]}$. Thus $l_{u_{1}}\parallel\ldots\parallel l_{u_{n}}\in\mathopen{[\![}s_{1}\mathclose{]\!]}$ and $l_{u_{n+1}}\parallel\ldots\parallel l_{u_{m}}\in\mathopen{[\![}s_{2}\mathclose{]\!]}$ by the inductive hypothesis, and so $p\in\mathopen{[\![}s_{1}\parallel s_{2}\mathclose{]\!]}$, giving a contradiction.

• •

Suppose $s=r^{(*)}$. Thus for every $n\geq 0$, $\mathopen{[\![}p\mathclose{]\!]}\cap\mathopen{[\![}\underbrace{r\parallel\ldots\parallel r}_{n\text{ terms}}\mathclose{]\!]}=\emptyset$ holds, and from the minimality condition on $s$, $\mathopen{[\![}\nu(p)\mathclose{]\!]}\cap\mathopen{[\![}\nu(\underbrace{r\parallel\ldots\parallel r}_{n\text{ terms}})\mathclose{]\!]}=\emptyset$ follows. Since $\mathopen{[\![}\nu(s)\mathclose{]\!]}=\cup_{n\geq 0}\mathopen{[\![}\nu(\underbrace{r\parallel\ldots\parallel r}_{n\text{ terms}})\mathclose{]\!]}$, this leads to a contradiction. ∎

Corollary 24 extends Lemma 23 by replacing $p$ by an arbitrary commutative-regular term.

Corollary 24

Let $\Sigma$ be an alphabet and let $U$ be a set of elements of $T_{bi-KA}(\Sigma)$ such that every element of $U$ either lies in $\Sigma$ or is sequential. Assume that distinct terms in $U$ define disjoint languages. Let $s,s^{\prime}\in T_{ComReg}(L_{U})$. Then

[TABLE]

holds.

*Proof. * If $\mathopen{[\![}\nu(s)\mathclose{]\!]}$ and $\mathopen{[\![}\nu(s^{\prime})\mathclose{]\!]}$ are not disjoint, then from the commutative-regular analogue of Lemma 11, there exists a commutative word $w$ such that $w\in\mathopen{[\![}s\mathclose{]\!]}$ and $\mathopen{[\![}\nu(w)\mathclose{]\!]}\subseteq\mathopen{[\![}\nu(s)\mathclose{]\!]}$ and $\mathopen{[\![}\nu(w)\mathclose{]\!]}$ intersects with $\mathopen{[\![}\nu(s^{\prime})\mathclose{]\!]}$, and so from Lemma 23, $w\in\mathopen{[\![}s^{\prime}\mathclose{]\!]}$ also follows. ∎

Lemma 25

Let $\Sigma$ be an alphabet and let $T$ be a finite set of elements of $T_{bi-KA}(\Sigma)$. Then there exists a finite set $U$ of elements of $T_{bi-KA}(\Sigma)$ defining non-empty pairwise disjoint languages, such that for each $t\in T$, there exists $U_{t}\subseteq U$ such that $\mathopen{[\![}t\mathclose{]\!]}=\bigcup_{x\in U_{t}}\mathopen{[\![}x\mathclose{]\!]}$ holds. Furthermore, the set $U$ can be computed from $T$ and any subset $U_{t}$ can be computed from $T$ and $t$.

*Proof. * We will prove the computability assertion separately; first we prove the preceding claims in the Lemma by induction on $\operatorname{depth}(\sum_{x\in T}x)$. If $T\subseteq\Sigma\cup\{1\}$ then the conclusion is obvious, and so using Lemma 17, we need only consider the case that each term in $T$ is parallel; the case that each term in $T$ is sequential is analogous.

By Proposition 18, for each $t\in T$ there exists a finite set $U_{t}$ of terms that all either lie in $\Sigma$ or are sequential and a commutative-regular term $s_{t}$ over $L_{U_{t}}$ such that $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}\nu(s_{t})\mathclose{]\!]}$ and for each $u\in U_{t}$, $\operatorname{depth}(u)<\operatorname{depth}(t)$, and hence

[TABLE]

holds.

From applying the inductive hypothesis to $\cup_{t\in T}U_{t}$ there is a set $V$ of terms over $\Sigma$ defining non-empty pairwise disjoint pomset languages, and such that for each $u\in\cup_{t\in T}U_{t}$, there exists $V_{u}\subseteq V$ such that

[TABLE]

holds.

For each $t\in T$, let $s_{t}^{\prime}$ be obtained from $s_{t}$ by replacing every letter $l_{u}$ by the sum $\sum_{x\in V_{u}}l_{x}$. Thus $\mathopen{[\![}\nu(s_{t}^{\prime})\mathclose{]\!]}=\mathopen{[\![}\nu(s_{t})\mathclose{]\!]}=\mathopen{[\![}t\mathclose{]\!]}$ holds by Theorem 6. By Corollary 21 applied to the terms $s_{t}^{\prime}$, there is a set $C$ of commutative-regular terms defining non-empty pairwise disjoint languages and such that for each $t\in T$, there are terms $c_{1},\ldots,\ldots,c_{n}\in C$ satisfying $\mathopen{[\![}s_{t}^{\prime}\mathclose{]\!]}=\mathopen{[\![}c_{1}+\ldots\ldots+c_{n}\mathclose{]\!]}$ and again from Theorem 6,

[TABLE]

holds. From Corollary 24, the terms in $\nu(C)$ also satisfy the required disjointness property and hence satisfy the conclusion of the Lemma for $U$.

We now consider the computability assertion. We define a recursive algorithm $\mathcal{A}$ that on input $T$ computes the sets $U$ and $U_{t}$ for each $t\in T$ satisfying the conditions required. We may assume that each term in $T$ defines a non-empty pomset language. $\mathcal{A}$ is defined precisely as indicated by our proof above. We prove by induction on $\operatorname{depth}(\sum_{x\in T}x)$ that $\mathcal{A}$ terminates with the correct outputs. We define the partition $T=T_{para}\uplus T_{seq}\uplus T_{\Sigma}$, where $T_{para}$ contains all elements of $T$ that are parallel, $T_{seq}$ contains all elements of $T$ that are sequential, and $T_{\Sigma}\subseteq\Sigma\cup\{1\}$ contains all remaining elements of $T$. The term sets $U_{t}$ and terms $s_{t}$ can be computed from each $t\in T_{para}$, by Lemma 18. $\mathcal{A}$ obtains the sets $V$ and $V_{u}$ for each $u\in\cup_{t\in T_{para}}U_{t}$ by calling itself with input $\cup_{t\in T_{para}}U_{t}$; by the inductive hypothesis and (11), $\mathcal{A}$ terminates and returns the correct values. Thus the terms $s_{t}^{\prime}$ can also be computed, and so the set $C$ and the appropriate set of elements $\{c_{1},\ldots,c_{n}\}$ for each term $t$ can be computed by Corollary 21. The function $\nu$ is clearly computable and thus $\mathcal{A}$ returns the correct term sets for $T_{para}$. The correct output for $T_{seq}$ is computed analogously. ∎

Our first main Theorem now follows.

Theorem 26

Let $\Sigma$ be an alphabet and let $t_{1},t_{2}\in T_{bi-KA}(\Sigma)$. Then there exist elements of $T_{bi-KA}(\Sigma)$ defining the sets $\mathopen{[\![}t_{1}\mathclose{]\!]}\cup\mathopen{[\![}t_{2}\mathclose{]\!]}$, $\mathopen{[\![}t_{1}\mathclose{]\!]}\cap\mathopen{[\![}t_{2}\mathclose{]\!]}$ and $\mathopen{[\![}t_{1}\mathclose{]\!]}-\mathopen{[\![}t_{2}\mathclose{]\!]}$, which can be computed from $t_{1}$ and $t_{2}$.

*Proof. * The case $\mathopen{[\![}t_{1}\mathclose{]\!]}\cup\mathopen{[\![}t_{2}\mathclose{]\!]}$ is trivial, and since $\mathopen{[\![}t_{1}\mathclose{]\!]}\cap\mathopen{[\![}t_{2}\mathclose{]\!]}=\mathopen{[\![}t_{1}+t_{2}\mathclose{]\!]}-(\mathopen{[\![}t_{1}\mathclose{]\!]}-\mathopen{[\![}t_{2}\mathclose{]\!]})-(\mathopen{[\![}t_{2}\mathclose{]\!]}-\mathopen{[\![}t_{1}\mathclose{]\!]})$ holds, it suffices to prove the existence of an element $s\in T_{bi-KA}(\Sigma)$ such that $\mathopen{[\![}s\mathclose{]\!]}=\mathopen{[\![}t_{1}\mathclose{]\!]}-\mathopen{[\![}t_{2}\mathclose{]\!]}$ holds. This follows from Lemma 25 with $T=\{t_{1},t_{2}\}$ in that Lemma. ∎

We now give our bi-Kleene term decidability result.

Theorem 27

Let $\Sigma$ be an alphabet and let $t,t^{\prime}\in T_{bi-KA}(\Sigma)$. Then it is decidable whether $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$ holds.

*Proof. * This follows from Theorem 26, similarly to the proof of Corollary 20.

4 Equality between bi-Kleene terms defining pomset languages is a consequence of the bi-Kleene axioms

In this section we use Lemma 25 to prove our second main theorem. We first show that under stricter hypotheses, the converse implication to that given in Corollary 24 holds.

Lemma 28

Let $\Sigma$ be an alphabet and let $U$ be a set of elements of $T_{bi-KA}(\Sigma)$ such that every element of $U$ either lies in $\Sigma$ or is sequential and defines a non-empty language. Assume that pairs of terms in $U$ define disjoint languages. Let $s,t$ be commutative-regular terms over $L_{U}$. Then

[TABLE]

holds.

*Proof. * Suppose that $\mathopen{[\![}s\mathclose{]\!]}\not=\mathopen{[\![}t\mathclose{]\!]}$ holds. Then there exists a pomset $p\in\mathopen{[\![}s\mathclose{]\!]}-\mathopen{[\![}t\mathclose{]\!]}$ ($s,t$ may need to be interchanged). Let $\tilde{p}\in T_{bimonoid}(\Sigma)$ satisfy $\mathopen{[\![}\tilde{p}\mathclose{]\!]}=\{p\}$. Thus $\mathopen{[\![}s+\tilde{p}\mathclose{]\!]}=\mathopen{[\![}s\mathclose{]\!]}$ and so $\mathopen{[\![}\nu(s)\mathclose{]\!]}+\mathopen{[\![}\nu(p)\mathclose{]\!]}=\mathopen{[\![}\nu(s)+\nu(\tilde{p})\mathclose{]\!]}=\mathopen{[\![}\nu(s)\mathclose{]\!]}$ by Lemma 11, whereas $\mathopen{[\![}\nu(p)\mathclose{]\!]}\cap\mathopen{[\![}\nu(t)\mathclose{]\!]}=\emptyset$ by the commutative-regular analogue of Lemma 11. Since each element of $U$ defines a non-empty language, $\mathopen{[\![}\nu({p})\mathclose{]\!]}\not=\emptyset$ and so $\mathopen{[\![}\nu(s)\mathclose{]\!]}\not=\mathopen{[\![}\nu(t)\mathclose{]\!]}$ follows. ∎

Our second main theorem follows.

Theorem 29

Let $\Sigma$ be an alphabet and let $t,t^{\prime}\in T_{bi-KA}(\Sigma)$. Assume $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$; then $t=_{bi-KA}t^{\prime}$ holds.

*Proof. * We prove the Theorem by induction on $\operatorname{depth}(t)=\operatorname{depth}(t^{\prime})$. If $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}\subseteq\{1\}\cup\Sigma$, then $t=_{bi-KA}t^{\prime}$ is obvious. By Lemma 17, we may assume that $t,t^{\prime}$ are both parallel; the case that they are both sequential is analogous.

By Proposition 18, there exists a finite set $U$ of terms that all either lie in $\Sigma$ or are sequential and define non-empty languages, and commutative-regular terms $s,s^{\prime}$ over $L_{U}$ such that

[TABLE]

By Lemma 25, there is a finite subset $V$ of $T_{bi-KA}(\Sigma)$, pairs of which define disjoint languages, and such that for each $u\in U$ there exists $V_{u}\subseteq V$ satisfying

[TABLE]

For each $u\in U$, let $w_{u}$ be a sum of the labels $l_{x}$ for each $x\in V_{u}$. Hence by Theorem 6 and (13),

[TABLE]

holds. Let the terms $r,r^{\prime}$ be obtained from $s,s^{\prime}$ respectively by replacing each occurrence of any $l_{u}\in L_{U}$ by $w_{u}$. Thus $\nu(r)$ is obtained from $\nu(s)$ by replacing each subterm $u\in U$ by $\nu(w_{u})$, and similarly for $\nu(r^{\prime})$ and $\nu(s^{\prime})$. By Proposition 18 and (14), for each $u\in U$

[TABLE]

follows, and so from the inductive hypothesis, $\nu(w_{u})=_{bi-KA}u$ follows from (14). Since $=_{bi-KA}$ is preserved by congruence,

[TABLE]

holds using (12). Since $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$ holds, $\mathopen{[\![}\nu(r)\mathclose{]\!]}=\mathopen{[\![}\nu(r^{\prime})\mathclose{]\!]}$ follows from (15). From Lemma 28, $r=_{bi-KA}r^{\prime}$ follows from Theorem 6 since the terms $r,r^{\prime}$ are commutative-regular, and so $\nu(r)=_{bi-KA}\nu(r^{\prime})$ holds since $=_{bi-KA}$ is preserved by substitution. Hence $t=_{bi-KA}t^{\prime}$ follows from (15), thus concluding the proof. ∎

Theorem 29 has an analogue for bw-rational algebras.

Theorem 30

Let $\Sigma$ be an alphabet and let $t,t^{\prime}\in T_{bw-Rat}(\Sigma)$. Assume $\mathopen{[\![}t\mathclose{]\!]}=\mathopen{[\![}t^{\prime}\mathclose{]\!]}$; then $t=_{bw-Rat}t^{\prime}$ holds.

*Proof. * This has a similar proof to that of Theorem 29. The proof relies on the fact that the proofs of Theorem 29 and its contributing lemmas and propositions can be adapted for bw-rational algebras by ignoring the cases in their proofs that consider the parallel iteration operation (∗). In the case of Theorem 6, the relevant result is that the algebra of commutative-word languages generated by an alphabet $\Sigma$ and the operations $0,1,+,\parallel$ is the free idempotent commutative semiring with basis $\Sigma$, and this is straightforward to prove. ∎

5 The bi-Kleene algebra of pomset ideals

We now move on to considering pomset ideals. We first give a criterion for elements of $\operatorname{\textbf{{Pom}}}$ to lie in $\operatorname{\textbf{{Pom}}}_{sp}$.

Definition 31** (N-free pomsets)**

A pomset defined by vertex set $V$ with partial order $\leq$ is N-free if $V$ does not contain a 4-element subset $\{v_{1},\ldots,v_{4}\}$ with $v_{1}\leq v_{2}$ and $v_{3}\leq v_{2},\;v_{3}\leq v_{4}$, and such that $\leq$ when restricted to $\{v_{1},\ldots,v_{4}\}$ does not contain any other pairs.

Theorem 32

A pomset is series-parallel if and only if it is N-free.

*Proof. * Gischer [9, Theorem 3.1]. ∎

Definition 33** (ideals of a pomset)**

Let $p$ be a pomset. An ideal of $p$ is a pomset that may be represented using the same vertex set as $p$, with the same labelling, but whose partial ordering is at least as strict as that for $p$. Let $L$ be a language of pomsets. Then $\operatorname{\textbf{{Id}}}(L)$ is the language of pomsets that are ideals of pomsets lying in $L$. We say that $L$ is a (pomset) ideal if $\operatorname{\textbf{{Id}}}(L)=L$ holds. We also define $\operatorname{\textbf{{Id}}}_{sp}(L)=\operatorname{\textbf{{Id}}}(L)\cap\operatorname{\textbf{{Pom}}}_{sp}$. If $\operatorname{\textbf{{Id}}}_{sp}(L)=L$ then we say that $L$ is an sp-ideal. The functions $\operatorname{\textbf{{Id}}}$ and $\operatorname{\textbf{{Id}}}_{sp}$ are closure operators on the sets $2^{\operatorname{\textbf{{Pom}}}(\Sigma)}$ and $2^{\operatorname{\textbf{{Pom}}}_{sp}(\Sigma)}$ respectively [13, chap.1].

In order to to study the sp-ideal of a parallel product $p\parallel q$ of pomsets, we introduce the function $\odot$. The use of this operation will be demonstrated by the identity (19).

Definition 34** (the $\odot$ binary function on pomset languages)**

Let $p_{1},p_{2}$ be pomsets defined with disjoint vertex sets $V_{1},V_{2}$. Then we define the set $p_{2}\odot p_{2}$ to be the set of all pomsets $q\in\operatorname{\textbf{{Pom}}}_{sp}$ whose vertex set is $V_{1}\cup V_{2}$ and such that $q$ retains the vertex labelling and ordering of each $p_{i}$ within $V_{i}$. We extend the domain of $\odot$ pointwise to pairs of pomset languages. Clearly $\odot$ is associative and commutative.

Lemma 35

The following hold for pomset languages $L,L^{\prime},L_{j}$ for $j$ in an indexing set $S$.

[TABLE]

[TABLE]

[TABLE]

Furthermore, if $L,L^{\prime},L_{j}\subseteq\operatorname{\textbf{{Pom}}}_{sp}$ then the same equalities with $\operatorname{\textbf{{Id}}}$ replaced by $\operatorname{\textbf{{Id}}}_{sp}$ also hold; in addition,

[TABLE]

*Proof. * (16) and its $\operatorname{\textbf{{Id}}}_{sp}$ counterpart follow immediately from the definition of an ideal. (17) for $\operatorname{\textbf{{Id}}}$ is straightforward. To prove $\operatorname{\textbf{{Id}}}_{sp}(LL^{\prime})\subseteq\operatorname{\textbf{{Id}}}_{sp}(L)\operatorname{\textbf{{Id}}}_{sp}(L^{\prime})$, observe that any element of $\operatorname{\textbf{{Id}}}(LL^{\prime})$ has the form $pp^{\prime}$ with $p\in\operatorname{\textbf{{Id}}}(L)$, $p^{\prime}\in\operatorname{\textbf{{Id}}}(L^{\prime})$. If in addition $pp^{\prime}\in\operatorname{\textbf{{Pom}}}_{sp}$, then $pp^{\prime}$ is N-free by Theorem 32, hence $p,p^{\prime}$ are also N-free and again by this Theorem, $p,\,p^{\prime}\in\operatorname{\textbf{{Pom}}}_{sp}$ hold. The other inclusion is obvious, and hence $\operatorname{\textbf{{Id}}}_{sp}(L^{i})=(\operatorname{\textbf{{Id}}}_{sp}(L))^{i}$ for each $i\geq 0$ follows by induction on $i$. Thus $\operatorname{\textbf{{Id}}}_{sp}(L^{*})=(\operatorname{\textbf{{Id}}}_{sp}(L))^{*}$ follows from this and (16) for $\operatorname{\textbf{{Id}}}_{sp}$, thus proving both versions of (17). (18) follows immediately from the definition of a (sp-)ideal and their closure properties.

We prove (19) as follows. Suppose a pomset $r\in\operatorname{\textbf{{Id}}}_{sp}(L\parallel L^{\prime})$. Thus $r$ is representable by a labelled partial order $(V\cup V^{\prime}\leq,\mu)$ for pomsets $q,q^{\prime}$ defined by disjoint vertex sets $V,V^{\prime}$ that are ideals of pomsets lying in $L,L^{\prime}$ respectively. By Theorem 32 applied to $r$, the pomsets $q,q^{\prime}$ are N-free; hence again by this Theorem, $q,q^{\prime}\,\in\operatorname{\textbf{{Id}}}_{sp}(L)$, $\operatorname{\textbf{{Id}}}_{sp}(L^{\prime})$ respectively. Thus $r\in\operatorname{\textbf{{Id}}}_{sp}(L)\odot\operatorname{\textbf{{Id}}}_{sp}(L^{\prime})$. We have shown that $\operatorname{\textbf{{Id}}}_{sp}(L\parallel L^{\prime})\subseteq\operatorname{\textbf{{Id}}}_{sp}(L)\odot\operatorname{\textbf{{Id}}}_{sp}(L^{\prime})$, and clearly equality holds. ∎

The set of pomset ideals is not a sub-bi-Kleene algebra of the set of pomset languages, since if the commutative Kleene operations are defined as given by Proposition 2, then the parallel product of two pomset ideals is not usually an ideal; an analogous statement holds for sp-ideals. However, by taking the ideal closure, or sp-ideal closure, respectively, of the pomset languages defined in the usual way by $\parallel$ and (∗), we obtain bi-Kleene algebras of pomset ideals and sp-pomset ideals.

Theorem 36** (bi-Kleene algebras of pomset ideals and sp-ideals)**

Let $\Sigma$ be an alphabet. Then $\operatorname{\textbf{{Id}}}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$ is a bi-Kleene algebra provided that the Kleene operations $0,1,+,\cdot,^{*}$ are interpreted as indicated in Proposition 2 and the commutative Kleene operations $\parallel,\,^{(*)}$ are interpreted as

[TABLE]

respectively.

Furthermore, the set $\operatorname{\textbf{{Id}}}_{sp}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$ of sp-ideals with labels in $\Sigma$ is a bi-Kleene algebra provided that the Kleene operations $0,1,+,\cdot,^{*}$ are interpreted as indicated in Proposition 2, and the commutative Kleene operations $\parallel,\,^{(*)}$ are interpreted as

[TABLE]

respectively.

Lastly, the function

[TABLE]

defined by

[TABLE]

is an injective bi-Kleene homomorphism.

*Proof. * We first consider $\operatorname{\textbf{{Id}}}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$. Since this set is closed under the Kleene operations $0,1,+,\cdot,^{*}$, it is a Kleene subalgebra of $2^{\operatorname{\textbf{{Pom}}}(\Sigma)}$. Thus it remains to prove the validity of the bi-Kleene axioms mentioning $\parallel$ and (∗). Associativity of $\parallel$ follows since for $I^{\prime},I^{\prime\prime},I^{\prime\prime\prime}\in\operatorname{\textbf{{Id}}}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$,

[TABLE]

by (18) in Lemma 35. The remaining axioms involving only $0,1,+,\parallel$ are clear. The identities in (4) for $\parallel,^{(*)}$ follow since for $I\in\operatorname{\textbf{{Id}}}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$,

[TABLE]

The induction axiom $s\parallel t\leq t\Rightarrow s^{(*)}\parallel t\leq t$ follows since for $I,J\in\operatorname{\textbf{{Id}}}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$

[TABLE]

The corresponding result for $\operatorname{\textbf{{Id}}}_{sp}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$ is proved analogously. We now show that the function given by (22) is a bi-Kleene homomorphism. For the Kleene operation $+$ this follows from (16). For $\parallel$, observe that $\operatorname{\textbf{{Id}}}(\operatorname{\textbf{{Id}}}_{sp}(I\parallel I^{\prime}))=\operatorname{\textbf{{Id}}}(I\parallel I^{\prime})=\operatorname{\textbf{{Id}}}(\operatorname{\textbf{{Id}}}(I)\parallel\operatorname{\textbf{{Id}}}(I^{\prime}))$ using (18), and the case of (∗) then follows from (16). The cases of $\cdot$ and ∗ are given by (17). To show injectivity, observe that there is a partial inverse function

[TABLE]

since if $I\in\operatorname{\textbf{{Id}}}_{sp}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$ then $\operatorname{\textbf{{Id}}}_{sp}(\operatorname{\textbf{{Id}}}(I))=\operatorname{\textbf{{Id}}}(I)\cap\operatorname{\textbf{{Pom}}}_{sp}(\Sigma)=\operatorname{\textbf{{Id}}}_{sp}(I)=I$ holds. ∎

Restricting the homomorphism from $\operatorname{\textbf{{Id}}}_{sp}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$ to $\operatorname{\textbf{{Id}}}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$ given by (22) to the subalgebra of $\operatorname{\textbf{{Id}}}_{sp}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$ generated by the set of singleton pomsets \big{\{}\{\sigma\}\big{|}\,\sigma\in\Sigma\big{\}} gives an isomorphism onto the subalgebra of $\operatorname{\textbf{{Id}}}(2^{\operatorname{\textbf{{Pom}}}(\Sigma)})$ generated by this set.

Theorem 37

Let $\Sigma$ be an alphabet. Then the bi-Kleene algebras

[TABLE]

with the operations $\parallel,^{(*)}$ interpreted as given in (21) and (20) respectively, and the Kleene operations $0,1,+,\cdot,^{*}$ interpreted as given in Proposition 2, are isomorphic; an isomorphism is given by

[TABLE]

*Proof. * Immediate from Theorem 36. ∎

Proposition 38

The classes of pomset ideals and sp-ideals, with the operation $\parallel$ interpreted as in (20) and (21) respectively, satisfy the exchange law (1).

*Proof. * We consider the class of pomset ideals; the proof for the case of sp-ideals is analogous, with $\operatorname{\textbf{{Id}}}$ replaced by $\operatorname{\textbf{{Id}}}_{sp}$. Let $u,v,x,y\in\operatorname{\textbf{{Id}}}(2^{\operatorname{\textbf{{Pom}}}})$ and suppose $p_{u}\in u$ and similarly for $p_{v},p_{x},p_{y}$. Then the pomset $(p_{u}\parallel p_{v})\cdot(p_{x}\parallel p_{y})\in\operatorname{\textbf{{Id}}}(p_{v}\cdot p_{y}\parallel p_{u}\cdot p_{x})$ holds, and hence

[TABLE]

follows. Applying $\operatorname{\textbf{{Id}}}$ to the left side by using (17) gives $\operatorname{\textbf{{Id}}}(u\parallel v)\cdot\operatorname{\textbf{{Id}}}(x\parallel y)\subseteq\operatorname{\textbf{{Id}}}(v\cdot y\parallel u\cdot x)$ and thus (1) holds. ∎

Definition 39** (The $=_{EX}$ relation)**

Let $t,t^{\prime}\in T_{bw-Rat}(\Sigma)$ for an alphabet $\Sigma$. We say that $t=_{EX}t^{\prime}$ if $t=t^{\prime}$ holds in every bw-rational algebra in which the exchange law (1) also holds. We also define the partial ordering $\leq_{EX}$ by analogy with (2).

In view of Theorem 30, we will broaden the use of the relations $\leq_{EX}$ and $=_{EX}$. Clearly $\leq_{bw-Rat}\,\subseteq\,\leq_{EX}$ holds, and we exploit this by allowing bw-rational pomset languages to occur in the arguments of $\leq_{EX}$ and $=_{EX}$; for example, $L=_{EX}t^{\prime}$ for term $t^{\prime}$ and language $L$ if $t=_{EX}t^{\prime}$ holds for at least one (and hence every) term $t\in T_{bw-Rat}(\Sigma)$ satisfying $L=\mathopen{[\![}t\mathclose{]\!]}$.

5.1 Summary of proof of our main theorems on pomset ideals

The reader is advised to study the proof of Theorem 50, our last main theorem, in order to have an insight into the purpose of the lemmas and theorems preceding it. This proof is straightforward if it is assumed that for any bw-rational term $t$, the language $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})$ is bw-rational and satisfies $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})\leq_{EX}t$. This is precisely the content of Theorem 49, which is proved by induction on the structure of $t$. The only non-trivial case in this proof is that where $t$ is a parallel product; $t=r_{1}\parallel r_{2}$, which implies $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})=\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}r_{1}\mathclose{]\!]})\odot\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}r_{2}\mathclose{]\!]})$ by (19) in Lemma 35. Thus it is necessary to prove Theorem 49 for the special case that $\mathopen{[\![}t\mathclose{]\!]}$ is a $\odot$-product of two bw-rational ideal languages. This is implied by Lemma 48, which states that for bw-rational terms $r_{1},r_{2}$, $\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}\leq_{EX}r_{1}\parallel r_{2}$ holds. Its proof is by induction on the sum of the widths of $r_{1}$ and $r_{2}$ and entails proving that for each $k\geq 1$, \big{(}\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}\big{)}\cap\operatorname{\textbf{{Para}}}_{k}\leq r_{1}\parallel r_{2} holds. The cases $k\geq 2$ can be inferred from the case $k=1$ using the inductive hypothesis and Corollary 45. The case $k=1$ follows from Corollary 43, which shows that for bw-rational terms $L_{1},L_{2}$, the language $(L_{1}\odot L_{2})\cap\operatorname{\textbf{{Seq}}}$ is definable by a regular term with $\odot$-product languages substituted for its ground terms.

6 Two automata-theoretic lemmas

In order to prove our main theorems, we need the following automata-theoretic results.

Lemma 40

Let $\Gamma$ be a finite alphabet and let $L$ be a regular language over $\Gamma$. Let $\approx$ be a congruence of finite index of the monoid $(\Gamma^{*},1,\cdot)$ and assume that $L$ is a union of some of the $\approx$-congruence classes. Define a finite set $\Delta$ and a function $\theta:\Delta\to\Gamma^{*}/\approx$. Define the set

[TABLE]

Then $V$ is a regular language over $\Delta$.

*Proof. * We define a deterministic finite state automaton $B$ as follows. $B$ has state set $\Gamma^{*}/\approx$. Its initial state is the $\approx$-class containing $1$, and its final states are those whose union is $L$. For each $\delta\in\Delta$, $B$ has a binary transition relation $\underset{\delta}{\leadsto}$ on $\Gamma^{*}/\approx$ as follows; for $S\in\Gamma^{*}/\approx$, we define $S\underset{\delta}{\leadsto}S^{\prime}$, where $S\theta(\delta)\subseteq S^{\prime}$. Since $\approx$ is a congruence, the class $S^{\prime}$ exists and is uniquely determined by $S$ and $\delta$.

Let $S_{0}$ be the initial state of $B$, so $1\in S_{0}$. Given $\delta_{1},\ldots,\delta_{b}\in\Delta$ for $b\geq 0$, there are states $S_{1},\ldots,S_{b}$ of $B$ such that $S_{0}\underset{\delta_{1}}{\leadsto}S_{1}\underset{\delta_{2}}{\leadsto}\ldots\underset{\delta_{b}}{\leadsto}S_{b}$ holds. Thus $S_{b}\subseteq L\iff S_{0}\,\theta(\delta_{1})\ldots\theta(\delta_{b})\subseteq L\iff\theta(\delta_{1})\ldots\theta(\delta_{b})\subseteq L\iff\delta_{1}\ldots\delta_{b}\in V$, proving that $B$ accepts $V$. ∎

Lemma 41

Let $\Gamma$ be a finite alphabet and let $L_{1},L_{2}$ be regular languages over $\Gamma$. Let $\approx$ be a congruence of finite index of the monoid $(\Gamma^{*},1,\cdot)$ and assume that each $L_{i}$ is a union of some of the $\approx$-congruence classes. Define a finite set $\Delta$ and a function $\theta:\Delta\to\Gamma^{*}/\approx$, and define the language

[TABLE]

over $\Delta\times\Delta$. Then $U$ is regular.

*Proof. * For each $j=1,2$, let $V_{j}$ be the language defined as $U$ is, but satisfying only the condition $\theta(\delta_{i1})\ldots\theta(\delta_{ib})\subseteq L_{i}$ for $i=j$. Thus $U=V_{1}\cap V_{2}$. It suffices thus to prove that each $V_{j}$ is regular, and this follows from Lemma 40, since regularity is preserved by substitution. ∎

7 Expressing the sequential sublanguage of a $\odot$-product as a regular function of ‘smaller’ non-sequential sublanguages of $\odot$-products

Our main result in this section is Corollary 43, which is an essential intermediate result for proving that the $\odot$ operation preserves bw-rationality, as indicated in Section 5.1.

Lemma 42

Let $\Sigma$ be an alphabet and let $C_{1},\ldots,C_{m}\in\operatorname{\textbf{{Pom}}}_{sp}(\Sigma)$ be non-sequential and let $\{\gamma_{1},\ldots,\gamma_{m}\}$ be an alphabet and for $i=1,2$ let

[TABLE]

Let $\Delta$ be a set and let $\approx$ be a congruence on the monoid $(\{\gamma_{1},\ldots,\gamma_{m}\}^{*},1,\cdot)$ such that each language $L_{i}$ is a union of $\approx$-classes. Let $\phi$ be a function from $\Delta$ onto $\{\gamma_{1},\ldots,\gamma_{m}\}^{*}/\approx$. Define the language

[TABLE]

over the alphabet $\Delta\times\Delta$, and write

[TABLE]

where for each $\delta\in\Delta$, we write $\phi(\delta)(C_{1},\ldots,C_{m})$ to denote the language $\phi(\delta)$ with each letter $\gamma_{i}$ replaced by the language $C_{i}$. Then

[TABLE]

holds.

*Proof. * Let p\in\big{(}L_{1}(C_{1},\ldots,C_{m})\odot L_{2}(C_{1},\ldots,C_{m})\big{)}\cap\operatorname{\textbf{{Seq}}}. We will show that $p\in\tilde{U}$. We have

[TABLE]

for $b\geq 2$ and each $p_{j}\in\operatorname{\textbf{{Para}}}\cup\Sigma$ and there are pomsets

[TABLE]

such that

[TABLE]

Clearly each $q_{i}=r_{i1}\ldots r_{ia_{i}}$ for some $a_{i}\geq 0$, where each pomset $r_{ij}\in\cup_{k=1}^{m}C_{k}$ and is hence non-sequential. Hence the vertices in any pomset $r_{ij}$ all lie in one of the pomsets $p_{l}$ and since their ordering in each $q_{i}$ is preserved in $p$, for any $j<j^{\prime}$ the vertices in $r_{ij}$ and $r_{ij^{\prime}}$ lie in $p_{l}$ and $p_{l^{\prime}}$ respectively for some $l\leq l^{\prime}$. Hence by gathering together adjacent pomsets $r_{ij}$ whose vertices lie in the same pomset $p_{l}$, we may write

[TABLE]

where each $w_{ij}$ is a sequence of pomsets all lying in $\cup_{k=1}^{m}C_{k}$ and the vertices in $w_{ij}$ occur in the pomset $p_{j}$. Thus each

[TABLE]

holds.

Clearly each language

[TABLE]

and so each $w_{i1}\ldots w_{ib}=q_{i}\in v_{i}(C_{1},\ldots,C_{m})$ for words $v_{i}=v_{i}(\gamma_{1},\ldots,\gamma_{m})\in{L}_{i}$. Since the pomsets in the language $\cup_{k=1}^{m}C_{k}$ are non-sequential, by Part (2) of Lemma 9 there are words $v_{ij}=v_{ij}(\gamma_{1},\ldots,\gamma_{m})$ such that $v_{i}=v_{i1}\ldots v_{ib}$ and $w_{ij}\in v_{ij}(C_{1},\ldots,C_{m})$ holds. Hence

[TABLE]

holds.

Since $\phi$ is onto, we may suppose each $v_{ij}\in\phi(\delta_{ij})$ for $\delta_{ij}\in\Delta$. Then each $w_{ij}\in\phi(\delta_{ij})(C_{1},\ldots,C_{m})$ and so

[TABLE]

holds. Also, $\phi(\delta_{i1})\ldots\phi(\delta_{ib})\subseteq W_{i}$ for some $\approx$-class $W_{i}$, since $\approx$ is a congruence. From (25), $L_{i}\cap W_{i}\neq\emptyset$ holds, and so $\phi(\delta_{i1})\ldots\phi(\delta_{ib})\subseteq L_{i}$ follows since each $L_{i}$ is a union of $\approx$-classes. Hence $p\in\tilde{U}$ follows from (24) and (26). Thus we have proved \big{(}L_{1}(C_{1},\ldots,C_{m})\odot L_{2}(C_{1},\ldots,C_{m})\big{)}\cap\operatorname{\textbf{{Seq}}}\subseteq\tilde{U}.

Conversely, suppose that $p\in\tilde{U}$ holds. Then there exist $b\geq 2$ and elements $\delta_{ij}\in\Delta$ such that

[TABLE]

and so there exist words $v_{ij}=v_{ij}(\gamma_{1},\ldots,\gamma_{m})\in\phi(\delta_{ij})$ such that each

[TABLE]

and hence there exist pomsets

[TABLE]

such that each p_{j}\in\big{(}w_{1j}\odot w_{2j}\big{)}\cap(\operatorname{\textbf{{Para}}}\cup\Sigma). Thus

[TABLE]

where for each $i=1,2$, clearly $v_{i1}\ldots v_{ib}\in{L}_{i}(\gamma_{1},\ldots,\gamma_{m})$ and thus

[TABLE]

holds. Thus p\in\big{(}L_{1}(C_{1},\ldots,C_{m})\odot L_{2}(C_{1},\ldots,C_{m})\big{)}\cap\operatorname{\textbf{{Seq}}} follows, as required. ∎

The main result of this section follows.

Corollary 43

Let $\Sigma$ be an alphabet and let terms $c_{1},\ldots,c_{m}\in T_{bw-Rat}(\Sigma)$ be non-sequential with each $\mathopen{[\![}c_{j}\mathclose{]\!]}=C_{j}$ and let

[TABLE]

be regular terms over an alphabet $\{\gamma_{1},\ldots,\gamma_{m}\}$. Let $\Delta$ be a finite set and let $\approx$ be a congruence of finite index on the monoid $(\{\gamma_{1},\ldots,\gamma_{m}\}^{*},1,\cdot)$ such that each language $\mathopen{[\![}t_{i}\mathclose{]\!]}$ is a union of $\approx$-classes. Let $\phi$ be a function from $\Delta$ onto $\{\gamma_{1},\ldots,\gamma_{m}\}^{*}/\approx$. Then there is a regular term $u$ over the alphabet $\Delta\times\Delta$ such that

[TABLE]

holds and for each word $(\delta_{11},\delta_{21})\ldots(\delta_{1b},\delta_{2b})\in\mathopen{[\![}u\mathclose{]\!]}$ and $i=1,2$,

[TABLE]

Also, for each $(\epsilon_{1},\epsilon_{2})\in\operatorname{supp}(u)$ and $i=1,2$,

[TABLE]

holds.

*Proof. *

By Lemma 41, there is a term $u\in T_{Reg}(\Delta\times\Delta)$ such that

[TABLE]

and so (27) holds by Lemma 42, with $\mathopen{[\![}t_{i}\mathclose{]\!]}$ in the role of the languages $L_{i}$, and (28) holds from the definition of $u$.

To prove (29), let $(\epsilon_{1},\epsilon_{2})\in\operatorname{supp}(u)$. Thus there is a word

$(\delta_{11},\delta_{21})\ldots(\delta_{1b},\delta_{2b})\in\mathopen{[\![}u\mathclose{]\!]}$ in which $(\epsilon_{1},\epsilon_{2})$ occurs and so there exists $b^{\prime}\leq b$ such that for each $j=1,2$, $\,{\epsilon_{j}}=\delta_{jb^{\prime}}$ holds and so from (28),

[TABLE]

holds. Since the elements of $\phi(\Delta)$ are non-empty sublanguages of $\{\gamma_{1},\ldots,\gamma_{m}\}^{*}$, each pomset language $\phi(\delta_{jk})(C_{1},\ldots,C_{m})$ is also non-empty and so

[TABLE]

holds. Thus (29) follows from (30). ∎

Lemma 44 relates the $\odot$-product of two languages defined as parallel products to $\odot$-products of their respective parallel components.

Lemma 44

Let $L_{1},L_{2}$ be bounded-width languages of sp-pomsets over an alphabet $\Sigma$, where each

[TABLE]

for $m_{i}\geq 1$ and pomset languages $S_{ij}$ satisfying $S_{ij}\subseteq\operatorname{\textbf{{Seq}}}\cup\Sigma$. Let $k\geq 1$. Then the following holds; the language $(L_{1}\odot L_{2})\cap\operatorname{\textbf{{Para}}}_{k}$ is the union of all languages of the form $M_{1}\parallel\cdots\parallel M_{k}$, where each language

[TABLE]

where for each $i\in\{1,2\}$, sets $T_{i1},\ldots,T_{ik}$ partition the set $\{1,\ldots,m_{i}\}$, and such that for each $j\leq k$, the set $T_{1j}\cup T_{2j}\not=\emptyset$. If additionally $k\geq 2$ holds then

[TABLE]

holds for each $j\leq k$.

*Proof. * Observe first that each metaterm $S_{ij}$ occurs exactly once in both the expressions $L_{1}\odot L_{2}$ and $M_{1}\parallel\cdots\parallel M_{k}$ under the conditions on the sets $T_{ij}$ given in the Lemma. Additionally, if any ordering occurs in a pomset in $M_{1}\parallel\cdots\parallel M_{k}$ between vertices in a pomset in $S_{ij}$ and in $S_{i^{\prime}j^{\prime}}$, then either $i=i^{\prime}\wedge j=j^{\prime}$ or $i\not=i^{\prime}$ holds, and hence the same ordering can occur in $L_{1}\odot L_{2}$. Thus any pomset in a language $M_{1}\parallel\cdots\parallel M_{k}$ under the given conditions lies in $(L_{1}\odot L_{2})\cap\operatorname{\textbf{{Para}}}_{k}$.

Conversely, let $p\in(L_{1}\odot L_{2})\cap\operatorname{\textbf{{Para}}}_{k}$. Thus each language $S_{ab}$ contains a pomset $q_{ab}$ such that the vertex set of $p$ is the pairwise disjoint union of all the vertex sets of the pomsets $q_{ab}$, with the same labelling and the same vertex ordering within each $q_{ab}$.

Write $p=p_{1}\parallel\ldots\parallel p_{k}$, with each $p_{j}\in\operatorname{\textbf{{Seq}}}\cup\Sigma$. Given any $j\leq k$ and $i\in\{1,2\}$, let $T_{ij}$ be the set of elements of $\{1,\ldots,m_{i}\}$ such that $p_{j}$ contains at least one vertex from $q_{ib}$ if and only if $b\in T_{ij}$. Since each $q_{ib}\notin\operatorname{\textbf{{Para}}}$, and its ordering is preserved in $p$, all vertices in $q_{ib}$ occur in $p_{j}$ if $b\in T_{ij}$. Hence $j\not=j^{\prime}\Rightarrow T_{ij}\cap T_{ij^{\prime}}=\emptyset$ follows, and since the vertices of every pomset $q_{ib}$ must occur in some $p_{j}$, $\{1,\ldots,m_{i}\}=\cup_{j=1}^{k}T_{ij}$ holds, proving the partitioning property of the sets $T_{ij}$ asserted by the Lemma.

Since the ordering of the vertices in $\parallel_{b\leq m_{i}}q_{ib}$ and hence in $\parallel_{b\in T_{ij}}q_{ib}$ is preserved in $p$, and each $p_{j}\in\operatorname{\textbf{{Seq}}}\cup\Sigma$, it follows that $p_{j}\in M_{j}$, with $M_{j}$ defined as in the statement of the Lemma using the sets $T_{ij}$. The assertion that $T_{1j}\cup T_{2j}\not=\emptyset$ holds follows since $p\in\operatorname{\textbf{{Para}}}_{k}$ and each $M_{j}\not=\{1\}$.

The width property asserted by the Lemma holds if $k\geq 2$ since for each $j\leq k$ and $i\in\{1,2\}$, $T_{ij}\subseteq\{1,\ldots,m_{i}\}$ and so

[TABLE]

holds, with strict inequality for at least one $i\in\{1,2\}$, since given any $j,j^{\prime}\leq k$ with $j^{\prime}\not=j$, $T_{ij^{\prime}}\not=\emptyset$ holds for at least one element $i\in\{1,2\}$, and so for every $b\in T_{ij^{\prime}}=T_{ij^{\prime}}-T_{ij}$, the term $S_{ib^{\prime}}$ occurs in the middle term but not on the left side of the above inequality, and $S_{ib^{\prime}}\ni q_{ib}\not=\{1\}$. Thus we have proved the Lemma. ∎

Corollary 45 gives an inductive step in the proof of Theorem 48, our third main theorem.

Corollary 45

Let $L_{1},L_{2}$ be bw-rational languages of sp-pomsets over an alphabet $\Sigma$, and assume that for any bw-rational languages $L_{1}^{\prime},L_{2}^{\prime}$ satisfying $\sum_{i=1}^{2}\operatorname{width}(L_{i}^{\prime})<\sum_{i=1}^{2}\operatorname{width}(L_{i})$, the language $(L_{1}^{\prime}\odot L_{2}^{\prime})\cap(\operatorname{\textbf{{Seq}}}\cup\Sigma)$ is bw-rational and satisfies

[TABLE]

Let $k\geq 2$. Then $(L_{1}\odot L_{2})\cap\operatorname{\textbf{{Para}}}_{k}$ is bw-rational and

[TABLE]

holds.

*Proof. * Using the distributive law for $\parallel$, we may assume that each $L_{i}=S_{i1}\parallel\cdots\parallel S_{im_{i}}$ for $m_{i}\geq 1$ and bw-rational pomset languages $S_{ij}$ satisfying $S_{ij}\subseteq\operatorname{\textbf{{Seq}}}\cup\Sigma$.

We first prove that $M_{1}\parallel\cdots\parallel M_{k}\leq_{EX}L_{1}\parallel L_{2}$ holds, where the languages $M_{j}$ are as defined using sets $T_{ij}$ as in Lemma 44; in particular, $\cup_{j=1}^{k}T_{ij}=\{1,\ldots,m_{i}\}$ for each $i\in\{1,2\}$. From the conclusion of that Lemma and the extra hypotheses assumed here, each language $M_{j}$ is bw-rational and

[TABLE]

holds. Thus

[TABLE]

holds. Thus the Corollary follows since there are finitely many ways of defining collections of sets $T_{ij}$ satisfying the conditions given in Lemma 44 and so by that Lemma, $L_{1}\odot L_{2}\cap\operatorname{\textbf{{Para}}}_{k}$ is a finite union of bw-rational languages $R$ satisfying $R\leq_{EX}L_{1}\parallel L_{2}$. ∎

8 The main theorems for sp-ideals of rational languages

We now show that $\odot$ preserves bw-rationality of pomset languages, and defines a language that is $=_{EX}$-equivalent to the parallel product of the languages. We first need an automata-theoretic lemma.

Lemma 46

Let $\Gamma$ be a finite alphabet, and let $S$ be a finite set of regular languages over $\Gamma$. Then there exists a congruence $\approx$ of finite index of the monoid $(\Gamma^{*},1,\cdot)$ such that each language $L\in S$ is the union of a subcollection of $\approx$-equivalence classes.

*Proof. * Since the conjunction of two congruences of finite index is itself a congruence of finite index, we may assume that $S$ is a singleton, $S=\{L\}$. Let $A$ be a deterministic finite state automaton accepting the language $L$. We assume $A$ has state set $Q$ and a binary transition relation $\underset{w}{\leadsto}\,\subseteq Q\times Q$ for each $w\in\Gamma^{*}$. For any function $\theta:Q\to Q$, let

[TABLE]

For any $w\in\Gamma^{*}$, there is a function $\theta:Q\to Q$ such that for any $q\in Q$, there exists a state $\theta(q)$ satisfying $q\underset{w}{\leadsto}\theta(q)$, and so $w\in K_{\theta}$; furthermore, if any $w\in K_{\theta}\cap K_{\theta^{\prime}}$, then for each $q\in Q$ both $q\underset{w}{\leadsto}\theta(q)$ and $q\underset{w}{\leadsto}\theta^{\prime}(q)$ hold. Since $A$ is deterministic, $\theta(q)=\theta^{\prime}(q)$ follows and so $\theta=\theta^{\prime}$. Thus the sets $K_{\theta}$ partition $\Gamma^{*}$ and are clearly regular, and for each $\theta,\theta^{\prime}:Q\to Q$, there exists $\theta^{\prime\prime}$ satisfying $K_{\theta}K_{\theta^{\prime}}\subseteq K_{\theta^{\prime\prime}}$. Clearly $L$ is the union of a collection of languages $K_{\theta}$; since there are finitely many functions from $Q$ into $Q$, the Lemma follows. ∎

Lemma 47 will be used with Corollary 43 to transform a ‘regular over parallel’ term given by $u$ in the statement of this Corollary into a sum of parallel terms in Theorem 48, which shows that $\odot$ preserves bw-rationality.

Lemma 47

Let $\{\gamma_{1},\ldots,\gamma_{m}\}$ be an alphabet and let terms $d_{1},\ldots,d_{k}\in T_{Reg}(\gamma_{1},\ldots,\gamma_{m})$ be such that the languages $\mathopen{[\![}d_{1}\mathclose{]\!]},\ldots,\mathopen{[\![}d_{k}\mathclose{]\!]}$ partition $\{\gamma_{1},\ldots,\gamma_{m}\}^{*}$ and for each $i,i^{\prime}\leq k$ there is a term $d_{j}$ satisfying $\mathopen{[\![}d_{i}d_{i^{\prime}}\mathclose{]\!]}\subseteq\mathopen{[\![}d_{j}\mathclose{]\!]}$.

Let $\Delta$ be a set and let $\phi:\Delta\to\{d_{1},\ldots,d_{k}\}$ be a bijection. Then for any term $u\in T_{Reg}(\Delta\times\Delta)$, there is a set $\Lambda\subseteq\Delta\times\Delta$ such that

[TABLE]

holds and for each element $(\epsilon_{1},\epsilon_{2})\in\Lambda$, there is a word $(\delta_{11},\delta_{21})\ldots(\delta_{1b},\delta_{2b})\in\mathopen{[\![}u\mathclose{]\!]}$ such that $\mathopen{[\![}\phi(\delta_{i1})\ldots\phi(\delta_{ib})\mathclose{]\!]}\subseteq\mathopen{[\![}\phi(\epsilon_{i})\mathclose{]\!]}$ for each $i\in\{1,2\}$, where if $b=0$ the product $\mathopen{[\![}\phi(\delta_{i1})\ldots\phi(\delta_{ib})\mathclose{]\!]}$ is defined to be the language $\{1\}$.

*Proof. * This follows by induction on the structure of $u$. For convenience, since $\phi$ is a bijection we may define $1_{\Delta}\in\Delta$ to be the element satisfying $1\in\mathopen{[\![}\phi(1_{\Delta})\mathclose{]\!]}$, and for any regular term $x$ over the alphabet $\Delta\times\Delta$ we define $\bar{x}=x((\delta,\delta^{\prime})\setminus\phi(\delta)\parallel\phi(\delta^{\prime})|\;\delta,\delta^{\prime}\in\Delta)$. If $u$ is [math] or an element of $\Delta\times\Delta$ then $\Lambda$ is as follows;

[TABLE]

and the conclusion of the Lemma is immediate. If $u=1$, we define $\Lambda=\{(1_{\Delta},1_{\Delta})\}$; for then by Theorem 30, $\bar{u}=1\leq_{bw-Rat}\phi(1_{\Delta})\parallel\phi(1_{\Delta})$ and $\{1\}\subseteq\mathopen{[\![}\phi(1_{\Delta})\mathclose{]\!]}$ hold, as required by the Lemma. If $u$ is a sum of terms, then the result follows from the inductive hypothesis applied to each of these terms.

There remain two cases, in both of which it is convenient to define multiplication on the set $\Delta$ as follows, using the fact that $\phi$ is a bijection; if $\phi(\delta)\phi(\delta^{\prime})\subseteq\phi(\delta^{\prime\prime})$, then $\delta\delta^{\prime}=\delta^{\prime\prime}$ holds. Clearly this definition turns $\Delta$ into a monoid, with $1_{\Delta}$ as the identity element. Furthermore, for any $\delta_{1},\ldots,\delta_{r},\in\Delta$,

[TABLE]

follows by induction on $r$. Thus the condition $\mathopen{[\![}\phi(\delta_{i1})\ldots\phi(\delta_{ib})\mathclose{]\!]}\subseteq\mathopen{[\![}\phi(\epsilon_{i})\mathclose{]\!]}$ in the statement of the Lemma is equivalent to $\delta_{i1}\ldots\delta_{ib}=\epsilon_{i}$, where if $b=0$ this states that $1_{\Delta}=\epsilon_{i}$.

• •

Suppose $u=u_{1}u_{2}$. By the inductive hypothesis, for each $i\in\{1,2\}$, there are sets $\Lambda_{i}\subseteq\Delta\times\Delta$ such that

[TABLE]

Define the set

[TABLE]

From the exchange law and the fact that by Theorem 30, $\phi(\delta)\phi(\delta^{\prime})\leq_{bw-Rat}\phi(\delta\delta^{\prime})$ always holds,

[TABLE]

holds. In addition, if $\lambda\in\Upsilon$, say $\lambda=(\epsilon_{11}\epsilon_{21},\epsilon_{12}\epsilon_{22})$ with each $(\epsilon_{i1},\epsilon_{i2})\in\Lambda_{i}$, by the inductive hypothesis there is a word $w_{i}=(\delta_{i11},\delta_{i21})\ldots(\delta_{i1b_{i}},\delta_{i2b_{i}})\in\mathopen{[\![}u_{i}\mathclose{]\!]}$ such that $\delta_{ij1}\ldots\delta_{ijb_{i}}=\epsilon_{ij}$ for each $i,j\in\{1,2\}$. Thus the word $w_{1}w_{2}\in\mathopen{[\![}u\mathclose{]\!]}$, and the product of all the $j$th components of the letters of $w_{1}w_{2}$ is $\delta_{1j1}\ldots\delta_{1jb_{1}}\delta_{2j1}\ldots\delta_{2jb_{2}}=\epsilon_{1j}\epsilon_{2j}$, proving the result.

• •

Suppose $u=t^{*}$. By the inductive hypothesis, there is a set $\Lambda\subseteq\Delta\times\Delta$ such that

[TABLE]

Define the set

[TABLE]

(note that $(1_{\Delta},1_{\Delta})\in\Psi$). For each $(\epsilon_{1},\epsilon_{2})\in\Lambda$,

[TABLE]

follows from the exchange law and Theorem 30 and the fact that $(\delta_{1},\delta_{2})\in\Psi\Rightarrow(\epsilon_{1}\delta_{1},\epsilon_{2}\delta_{2})\in\Psi$ always holds, and hence

[TABLE]

using the induction axiom of Kleene algebra. In addition, if $\lambda\in\Psi$, then

[TABLE]

for some $b\geq 0$, and each $(\delta_{j1},\delta_{j2})\in\Lambda$; and by the inductive hypothesis, for each $j\leq b$ and $i\in\{1,2\}$ there is a word $w_{j}\in\mathopen{[\![}t\mathclose{]\!]}$ such that the product of all the $i$th components of the letters of $w_{j}$ is $\delta_{ji}$. Clearly the word $w=w_{1}\ldots w_{b}\in\mathopen{[\![}u\mathclose{]\!]}$, and the product of all the $i$th components of the letters of $w$ is $\delta_{1i}\ldots\delta_{bi}$, completing the proof. ∎

Theorem 48** ($\odot$ preserves bw-rationality)**

Let $r_{1},r_{2}$ be bw-rational terms over an alphabet. Then the language $\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}$ is bw-rational and satisfies $\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}=_{EX}r_{1}\parallel r_{2}$.

*Proof. * Assume that each term $r_{i}\in T_{bw-Rat}(\Sigma)$ for an alphabet $\Sigma$. We will first prove that

[TABLE]

by induction on $\sum_{i=1}^{2}\operatorname{width}(r_{i})$. We will do this as follows. Clearly $\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}\subseteq\Sigma\cup\{1\}\cup\operatorname{\textbf{{Seq}}}\cup\,\cup_{k=1}^{\operatorname{width}(\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]})}\operatorname{\textbf{{Para}}}_{k}$. For any $k\geq 2$, it follows from Corollary 45 and the inductive hypothesis that the language $\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}\cap\operatorname{\textbf{{Para}}}_{k}$ is bw-rational and satisfies $\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}\cap\operatorname{\textbf{{Para}}}_{k}\,\leq_{EX}r_{1}\parallel r_{2}$. The same assertion with $\operatorname{\textbf{{Para}}}_{k}$ replaced by $\Sigma\cup\{1\}$ obviously holds. Thus it suffices to prove that $\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}\cap\operatorname{\textbf{{Seq}}}$ is bw-rational and

[TABLE]

holds. This will be proved using Corollary 43.

By Lemma 17 and Proposition 18 and its sequential counterpart, and by ignoring the cases in their proofs that refer to parallel iteration (∗), there are regular terms $t_{i}=t_{i}(\gamma_{1},\ldots,\gamma_{m})$ over an alphabet $\Gamma=\{\gamma_{1},\ldots,\gamma_{m}\}$ satisfying $r_{i}=_{bw-Rat}t_{i}(c_{1},\ldots,c_{m})$ for non-sequential terms $c_{1},\ldots,c_{m}$. By Lemma 46, there exists a congruence $\approx$ of finite index of the monoid $(\Gamma^{*},1,\cdot)$ such that each language $\mathopen{[\![}t_{i}\mathclose{]\!]}$ is the union of a subcollection of $\approx$-equivalence classes. Define the languages $C_{j}=\mathopen{[\![}c_{j}\mathclose{]\!]}$ for each $j\leq m$.

Let $\Delta$ be a set such that there is a bijection $\phi$ from $\Delta$ to the set of $\approx$-equivalence classes. Then by Corollary 43, there is a regular term $u$ with $\operatorname{supp}(u)\subseteq\Delta\times\Delta$ such that (27) holds, and for each word $(\delta_{11},\delta_{21})\ldots(\delta_{1b},\delta_{2b})\in\mathopen{[\![}u\mathclose{]\!]}$ and $i=1,2$, (28) holds.

Let $(\delta_{1},\delta_{2})\in\operatorname{supp}(u)$. Then by (29), \operatorname{width}\big{(}\phi(\delta_{i})(C_{1},\ldots,C_{m})\big{)}\leq\operatorname{width}(r_{i}) holds for each $i=1,2$. Hence by the inductive hypothesis, we can apply Corollary 45 to the languages $\phi(\delta_{i})(C_{1},\ldots,C_{m})$, and so for each $k\geq 2$,

[TABLE]

holds. In addition, the same statement with $\operatorname{\textbf{{Para}}}_{k}$ replaced by $\Sigma$ is clearly true. Thus by taking the union of the languages \phi(\delta_{1})(C_{1},\ldots,C_{m})\odot\phi(\delta_{2})(C_{1},\ldots,C_{m})\big{)}\cap\operatorname{\textbf{{Para}}}_{k} for each

k\in\{2,\ldots,\operatorname{width}\big{(}\phi(\delta_{1})(C_{1},\ldots,C_{m})\odot\phi(\delta_{2})(C_{1},\ldots,C_{m})\big{)}\} and also the language

$\phi(\delta_{1})(C_{1},\ldots,C_{m})\odot\phi(\delta_{2})(C_{1},\ldots,C_{m})\,\cap\Sigma$ it follows that

[TABLE]

holds. Hence by (27), the language $\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}\,\cap\,\operatorname{\textbf{{Seq}}}$ is bw-rational and

[TABLE]

holds. By Lemma 47, there exists a set $\Lambda\subseteq\Delta\times\Delta$ such that

[TABLE]

and for each $(\epsilon_{1},\epsilon_{2})\in\Lambda$, there is a word $(\delta_{11},\delta_{21})\ldots(\delta_{1b},\delta_{2b})\in\mathopen{[\![}u\mathclose{]\!]}$ such that

[TABLE]

for each $i\in\{1,2\}$, where if $b=0$ the product $\phi(\delta_{i1})\ldots\phi(\delta_{ib})$ is defined to be the language $\{1\}$; and since each language $\mathopen{[\![}{t}_{i}\mathclose{]\!]}$ is a union of $\approx$-equivalence classes, $\phi(\epsilon_{i})\subseteq\mathopen{[\![}{t}_{i}\mathclose{]\!]}$ follows from (28) and so by Theorem 30,

[TABLE]

and so (32) follows from (33) and (34) with the languages $C_{j}$ substituted for $\gamma_{j}$.

Hence we have proved (31). Since $\,\mathopen{[\![}r_{1}\mathclose{]\!]}\odot\mathopen{[\![}r_{2}\mathclose{]\!]}\supseteq\mathopen{[\![}r_{1}\parallel r_{2}\mathclose{]\!]}$ clearly holds, by Theorem 30 we can replace $\leq_{EX}$ by $=_{EX}$ in (31). ∎

Our main theorems concerning pomset ideals follow.

Theorem 49** ($\operatorname{\textbf{{Id}}}_{sp}$ preserves bw-rationality of pomset languages)**

*Let $t$ be a bw-rational pomset term. Then $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})$ is bw-rational and

$\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})\leq_{EX}t$ holds.*

*Proof. * The result follows by induction on the structure of $t$. If $t\in\{0,1\}$ or $t$ is a letter, then the result is immediate. If $t=u+v$ then the result follows since $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})=\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}u\mathclose{]\!]})+\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}v\mathclose{]\!]})$. If $t=u^{*}$ then the result follows since $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})=(\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}u\mathclose{]\!]}))^{*}$. If $t=uv$ then the result follows since $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})=\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}u\mathclose{]\!]})\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}v\mathclose{]\!]})$. Lastly if $t=r_{1}\parallel r_{2}$ then the result follows from Theorem 48 since $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}t\mathclose{]\!]})=\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}r_{1}\mathclose{]\!]})\odot\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}r_{2}\mathclose{]\!]})$ by (19) in Lemma 35. ∎

Theorem 50** (free bw-rational algebras with exchange law given as ideals)**

Let $\Sigma$ be an alphabet and let $a,b\in T_{bw-Rat}$. Suppose that $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}a\mathclose{]\!]})=\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}b\mathclose{]\!]})$ holds. Then $a=_{EX}b$ holds. Thus the isomorphic bw-rational algebras

[TABLE]

with $\parallel$ interpreted as in (21) and (20) respectively, are both freely generated in the class of bw-rational algebras satisfying (1) by the elements $\{\sigma\}$ for $\sigma\in\Sigma$.

*Proof. * By Theorem 49, the languages $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}a\mathclose{]\!]})$ and $\operatorname{\textbf{{Id}}}_{sp}(\mathopen{[\![}b\mathclose{]\!]})$ are bw-rational, and so we have

[TABLE]

where the first two relations follow from Theorem 30 and the last relation follows from Theorem 49. Interchanging $a$ and $b$ in this argument gives $a=_{EX}b$. The freeness assertion then follows from Theorem 37. ∎

9 Conclusions

We have proved, in this paper, that the class of pomset languages is closed under all Boolean operations, and that every identity that is valid for all pomset languages is a consequence of the set of valid regular and commutative-regular identities. We have also shown that the problem of establishing whether two pomset terms define the same language is decidable. The complexity of this is not clear however. It is known that decidability of equivalence of two regular terms is PSPACE-complete [14, 15], and can be shown that the analogous problem for commutative-regular terms lies in PSPACE, hence it is possible that generalising to pomset terms does not increase the bound beyond PSPACE. On the other hand, this problem may be EXPTIME-complete or EXPSPACE-complete. This is worth investigating further.