Department of Software Science, Tallinn University of Technology,
Estoniahendrik@cs.ioc.eehttps://orcid.org/0000-0002-1967-4297 School of
Computer Science, Reykjavik University, Iceland and Department of Software
Science, Tallinn University of
Technologytarmo@ru.ishttps://orcid.org/0000-0002-1297-0579 Hendrik Maarand and
Tarmo UustaluTheory of computation Regular languages Theory of computation
Concurrency This is an extended version of the conference paper [14]. Hendrik
Maarand: supported by the ERDF funded Estonian national CoE project EXCITE
(2014-2020.4.01.15-0018). Both authors: supported by the Estonian Ministry of
Education and Research institutional grant no. IUT33-13.

###### Acknowledgements.

We thank Pierre-Louis Curien, Jacques Sakarovitch, Simon Doherty, Georg Struth
and Ralf Hinze for inspiring discussions, and our anonymous reviewers for the
exceptionally thorough and constructive feedback they gave us.Wan Fokkink and
Rob van Glabbeek 2 30th International Conference on Concurrency Theory (CONCUR
2019) CONCUR 2019 CONCUR 2019 August 27–30, 2019 Amsterdam, the Netherlands
140 36

# Reordering Derivatives of Trace Closures of Regular Languages (Full Version)

Hendrik Maarand  Tarmo Uustalu

###### Abstract

We provide syntactic derivative-like operations, defined by recursion on
regular expressions, in the styles of both Brzozowski and Antimirov, for trace
closures of regular languages. Just as the Brzozowski and Antimirov derivative
operations for regular languages, these syntactic reordering derivative
operations yield deterministic and nondeterministic automata respectively. But
trace closures of regular languages are in general not regular, hence these
automata cannot generally be finite. Still, as we show, for star-connected
expressions, the Antimirov and Brzozowski automata, suitably quotiented, are
finite. We also define a refined version of the Antimirov reordering
derivative operation where parts-of-derivatives (states of the automaton) are
nonempty lists of regular expressions rather than single regular expressions.
We define the uniform scattering rank of a language and show that, for a
regexp whose language has finite uniform scattering rank, the truncation of
the (generally infinite) refined Antimirov automaton, obtained by removing
long states, is finite without any quotienting, but still accepts the trace
closure. We also show that star-connected languages have finite uniform
scattering rank.

###### keywords:

Mazurkiewicz traces, trace closure, regular languages, finite automata,
language derivatives, scattering rank, star-connected expressions

###### category:

##  1 Introduction

Traces were introduced to concurrency theory by Mazurkiewicz [15, 16] as an
alternative to words. A word can be seen as a linear order that is labelled
with letters of the alphabet. Intuitively, the main idea of traces is that the
linear order, corresponding to sequentiality, is replaced with a partial
order. Sets of words (or word languages) can be used to describe the behaviour
of concurrent systems. Similarly, sets of traces (or trace languages) can also
be used for this purpose. The difference is that descriptions in terms of
traces do not distinguish between different linear extensions (words) of the
same partial order (trace)—they are considered equivalent. Different linear
extensions of the same partial order can be seen as different observations of
the same behaviour.

Given a word language $L$ and a letter $a$, the derivative of $L$ along $a$ is
the language consisting of all the words $v$ such that $av$ belongs to $L$. An
essential difference between words and traces is that a nonempty word (a
linear order) has its first letter as the unique minimal element, but a
nonempty trace (a partial order) may have several minimal elements. A trace
from a trace language can be derived along any of its minimal letters.
Clearly, a minimal letter of a trace need not be the first letter of a word
representing this trace.

It is well-known that the derivative of a regular word language along a letter
is again regular. Brzozowski [7] showed that a regexp for it can be computed
from a regexp for the given language, and Antimirov [3] then further optimized
this result. We show that these syntactic derivative operations generalize to
trace closures (i.e., closures under equivalence) of regular word languages in
the form of syntactic _reordering derivative_ operations.

The syntactic derivative operations for regular word languages provide ways to
construct automata from a regexp. The Brzozowski derivative operation is a
function on regexps while the Antimirov derivative operation is a relation.
Accordingly, they yield deterministic and nondeterministic automata. The set
of Brzozowski derivatives of a regexp (modulo appropriate equations) and the
set of Antimirov parts-of-derivatives are finite, hence so are the resulting
automata. Our generalizations to trace closures of regular languages similarly
give deterministic and nondeterministic automata, but these cannot be finite
in general. Still, as we show, for a star-connected expression, the Antimirov
and Brzozowski automata, suitably quotiented, are finite. We also develop a
finer version of the Antimirov reordering derivative, where parts-of-
derivatives are nonempty lists of regexps rather than single regexps, and we
show that the set of expressions that can appear in these lists for a given
initial regexp is finite. We introduce a new notion of _uniform scattering
rank_ of a language (a variant of Hashiguchi’s scattering rank [9]) and show
that, for a regexp whose language has finite uniform rank, a truncation of the
refined reordering Antimirov automaton accepts its trace closure despite the
removed states, and is finite, without any quotienting.

This is an extension of the conference paper [14] with proofs of the most
important propositions and background material on classical language
derivatives and trace closures of regular languages.

##  2 Preliminaries on Word Languages

An _alphabet_ $\Sigma$ is a finite set (of _letters_). A _word_ over $\Sigma$
is a finite sequence of letters. The set $\Sigma^{*}$ of all words over
$\Sigma$ is the free monoid on $\Sigma$ with the empty word $\varepsilon$ as
the unit and concatenation of words (denoted by ${\cdot}$ that can be omitted)
as the multiplication. By $\pi_{X}(u)$ we mean the projection of a word $u$ to
a subalphabet $X\subseteq\Sigma$, i.e., $\pi_{X}(u)$ discards from $u$ all
letters which are not in $X$. We write $|u|$ for the length of a word $u$ and
also $|X|$ for the size of a subalphabet $X$. By $|u|_{a}$ we mean
$|\pi_{a}(u)|$, i.e., the number of occurrences of $a$ in $u$. By $\Sigma(u)$
we denote the set of letters that appear in $u$.

A _(word) language_ is a subset of $\Sigma^{*}$. The empty word and
concatenation of words lift to word languages via
$\mathbf{1}=_{\mathrm{df}}\\{\varepsilon\\}$ and $L\cdot
L^{\prime}=_{\mathrm{df}}\\{uv\mid u\in L\wedge v\in L^{\prime}\\}$.

###  2.1 Regular Languages

The set $\mathsf{RE}$ of _regular expressions_ (in short, _regexps_) over
$\Sigma$ is given by the grammar $E,F::=a\mid 0\mid E+F\mid 1\mid EF\mid
E^{*}$ where $a$ ranges over $\Sigma$.

The _word-language semantics_ of regular expressions is given by a function
$\llbracket\\_\rrbracket:\mathsf{RE}\to\mathcal{P}\Sigma^{*}$ defined
recursively by

$\small\begin{array}[]{rcl@{\qquad}rcl}\llbracket
a\rrbracket&=_{\mathrm{df}}&\\{a\\}&\llbracket
1\rrbracket&=_{\mathrm{df}}&\mathbf{1}\\\ \llbracket
0\rrbracket&=_{\mathrm{df}}&\emptyset&\llbracket
EF\rrbracket&=_{\mathrm{df}}&\llbracket E\rrbracket\cdot\llbracket
F\rrbracket\\\ \llbracket E+F\rrbracket&=_{\mathrm{df}}&\llbracket
E\rrbracket\cup\llbracket F\rrbracket&\llbracket
E^{*}\rrbracket&=_{\mathrm{df}}&\mu X.\,\mathbf{1}\cup\llbracket
E\rrbracket\cdot X\end{array}$

A word language $L$ is said to be _regular_ (or _rational_) if $L=\llbracket
E\rrbracket$ for some regexp $E$. Kleene algebras are defined by an equational
theory. It was shown by Kozen [13] that the set $\\{\llbracket E\rrbracket\mid
E\in\mathsf{RE}\\}$ of all regular languages together with the language
operations $\emptyset$, $\cup$, $\mathbf{1}$, ${\cdot}$, $(\\_)^{*}$ is the
free Kleene algebra on $\Sigma$. An important property for us is that $E\doteq
F$ iff $\llbracket E\rrbracket=\llbracket F\rrbracket$ where $\doteq$ refers
to valid equations in the Kleene algebra theory.

Kleene’s theorem [11] says that a word language is rational iff it is
_recognizable_ , i.e., accepted by a finite deterministic automaton
(acceptance by a finite nondeterministic automaton is an equivalent condition
because of determinizability [20]).

###  2.2 Derivatives of a Language

A word language $L$ is said to be _nullable_ $L{\downarrow}$, if
$\varepsilon\in L$. The _derivative_ (or _left quotient_)111We use the word
‘derivative’ both for languages and expressions, reserving the word ‘quotient’
for quotients of sets by equivalence relations. of $L$ along a word $u$ is
defined by $D_{u}L=_{\mathrm{df}}\\{v\mid uv\in L\\}$. For any $L$, we have
$D_{\varepsilon}L=L$ as well as $D_{uv}L=D_{v}(D_{u}L)$ for any
$u,v\in\Sigma^{*}$, i.e., the operation
$D:\mathcal{P}\Sigma^{*}\times\Sigma^{*}\to\mathcal{P}\Sigma^{*}$ is a right
action of $\Sigma^{*}$ on $\mathcal{P}\Sigma^{*}$. We also have
$L=\\{\varepsilon\mid L{\downarrow}\\}\cup\bigcup\\{\\{a\\}\cdot D_{a}L\mid
a\in\Sigma\\}$, and for any $u\in\Sigma^{*}$, we have $u\in L$ iff
$(D_{u}L){\downarrow}$.

Derivatives of regular languages are regular. A remarkable fact is that they
can be computed syntactically, on the level of regular expressions. There are
two constructions for this, due to Brzozowski [7] and Antimirov [3]. We review
these in the next two subsections. The Brzozowski and Antimirov derivative
operations yield deterministic resp. nondeterministic automata accepting the
language of a regular expression $E$. The Antimirov automaton is finite. The
Brzozowski automaton becomes finite when quotiented by associativity,
commutativity and idempotence for $+$. Identified up to the Kleene algebra
theory, the states of the Brzozowski automaton correspond to the derivatives
of the language $\llbracket E\rrbracket$. Regular languages can be
characterized as languages with finitely many derivatives.

###  2.3 Brzozowski Derivative

Nullability and derivative are semantic notions, defined about languages.
However, Brzozowski [7] noticed that for regular languages, one can compute
nullability and the derivatives syntactically, on the level of regular
expressions.

######  Definition 2.1.

The _syntactic nullability_ and the _Brzozowski derivative_ of a regexp are
given by functions ${{\downarrow}}:\mathsf{RE}\to\mathbb{B}$,
$D:\mathsf{RE}\times\Sigma\to\mathsf{RE}$ and
$D:\mathsf{RE}\times\Sigma^{*}\to RE$ defined recursively by

$\begin{array}[]{rclrcl}b{\downarrow}&=_{\mathrm{df}}&\mathsf{ff}&D_{a}b&=_{\mathrm{df}}&\mathsf{if\leavevmode\nobreak\
}a=b\mathsf{\leavevmode\nobreak\ then\leavevmode\nobreak\
}1\mathsf{\leavevmode\nobreak\ else\leavevmode\nobreak\ }0\\\
0{\downarrow}&=_{\mathrm{df}}&\mathsf{ff}&D_{a}0&=_{\mathrm{df}}&0\\\
(E+F){\downarrow}&=_{\mathrm{df}}&E{\downarrow}\vee
F{\downarrow}&D_{a}(E+F)&=_{\mathrm{df}}&D_{a}E+D_{a}F\\\
1{\downarrow}&=_{\mathrm{df}}&\mathsf{tt}&D_{a}1&=_{\mathrm{df}}&0\\\
(EF){\downarrow}&=_{\mathrm{df}}&E{\downarrow}\wedge
F{\downarrow}&D_{a}(EF)&=_{\mathrm{df}}&\mathsf{if\leavevmode\nobreak\
}E{\downarrow}\mathsf{\leavevmode\nobreak\ then\leavevmode\nobreak\
}(D_{a}E)F+D_{a}F\mathsf{\leavevmode\nobreak\ else\leavevmode\nobreak\
}(D_{a}E)F\\\
(E^{*}){\downarrow}&=_{\mathrm{df}}&\mathsf{tt}&D_{a}(E^{*})&=_{\mathrm{df}}&(D_{a}E)E^{*}\\\\[8.61108pt]
&&&D_{\varepsilon}E&=_{\mathrm{df}}&E\\\
&&&D_{ua}E&=_{\mathrm{df}}&D_{a}(D_{u}E)\end{array}$

######  Proposition 2.2.

For any $E$,

  1. 1.

$\llbracket E\rrbracket{\downarrow}=E{\downarrow}$;

  2. 2.

for any $a\in\Sigma$, $D_{a}\llbracket E\rrbracket=\llbracket
D_{a}E\rrbracket$;

  3. 3.

for any $u\in\Sigma^{*}$, $D_{u}\llbracket E\rrbracket=\llbracket
D_{u}E\rrbracket$.

######  Corollary 2.3.

For any $E$,

  1. 1.

$\llbracket E\rrbracket=\\{\varepsilon\mid
E{\downarrow}\\}\cup\bigcup\\{\\{a\\}\cdot\llbracket D_{a}E\rrbracket\mid
a\in\Sigma\\}$;

  2. 2.

for any $a\in\Sigma$, $v\in\Sigma^{*}$, $av\in\llbracket E\rrbracket$ iff
$v\in\llbracket D_{a}E\rrbracket$;

  3. 3.

for any $u,v\in\Sigma^{*}$, $uv\in\llbracket E\rrbracket$ iff $v\in\llbracket
D_{u}E\rrbracket$;

  4. 4.

for any $u\in\Sigma^{*}$, $u\in\llbracket E\rrbracket$ iff
$(D_{u}E){\downarrow}$.

The Brzozowski derivative operation gives a method for turning a regular
expression into a deterministic automaton. For a regexp $E$, the set of states
is $Q^{E}=\\{D_{u}E\mid u\in\Sigma^{*}\\}$, the initial state is
$q^{E}_{0}=E$, the final states are $F^{E}=\\{E^{\prime}\in Q^{E}\mid
E^{\prime}{\downarrow}\\}$ and the transition function $\delta^{E}$ is defined
by $D$ restricted to $Q^{E}$.

This automaton is generally not finite, but its quotient by a suitable
syntactically defined equivalence relation on the state set is finite, as we
will see in the next subsection.

###  2.4 Antimirov Derivative

Antimirov [3] optimized Brzozowski’s construction essentially constructing a
nondeterministic finite automaton (NFA) instead of a DFA, with a smaller
number of states and, crucially, without having to identify states up to
equations.

Antimirov’s syntactic derivative operation is a multivalued function, in other
words, a relation. Antimirov spoke of “partial derivatives” or “linear
factors”, we prefer to use the term “parts-of-derivatives”.

######  Definition 2.4.

The _Antimirov parts-of-derivatives_ of a regular expression along a letter or
a word are given the relations
${\to}\subseteq\mathsf{RE}\times\Sigma\times\mathsf{RE}$ and
${\to^{*}}\subseteq\mathsf{RE}\times\Sigma^{*}\times\mathsf{RE}$ defined
inductively by

$\small\begin{array}[]{l}a\to(a,1)\quad
E+F\to(a,E^{\prime})E\to(a,E^{\prime})\quad
E+F\to(a,F^{\prime})F\to(a,F^{\prime})\\\\[7.74997pt]
EF\to(a,E^{\prime}F)E\to(a,E^{\prime})\quad
EF\to(a,F^{\prime})\lx@proof@logical@and E{\downarrow}F\to(a,F^{\prime})\quad
E^{*}\to(a,E^{\prime}E^{*})E\to(a,E^{\prime})\\\\[7.74997pt]
E\to^{*}(\varepsilon,E)\quad
E\to^{*}(ua,E^{\prime\prime})\lx@proof@logical@and
E\to^{*}(u,E^{\prime})E^{\prime}\to(a,E^{\prime\prime})\end{array}$

The Antimirov parts-of-derivatives compute the semantic derivative
collectively.222If we took languages to be multisets of words (i.e.,
introduced the notion of a word occurring in a language some number of times )
and adopted the obvious multisets-of-words semantics of regular expressions,
the Antimirov parts-of-derivatives would compute regular expressions for a
partition of the semantic derivative. In the sets-of-words semantics, however,
overlaps are possible, so we do not get a partition.

######  Proposition 2.5.

For any $E$,

  1. 1.

for any $a\in\Sigma$, $D_{a}\llbracket E\rrbracket=\bigcup\\{\llbracket
E^{\prime}\rrbracket\mid E\to(a,E^{\prime})\\}$;

  2. 2.

for any $u\in\Sigma^{*}$, $D_{u}\llbracket E\rrbracket=\bigcup\\{\llbracket
E^{\prime}\rrbracket\mid E\to^{*}(u,E^{\prime})\\}$.

######  Corollary 2.6.

For any $E$,

  1. 1.

$av\in\llbracket E\rrbracket=\\{u\mid\exists
E^{\prime}.\,E\to(a,E^{\prime})\wedge v\in\llbracket E^{\prime}\rrbracket\\}$.

  2. 2.

$uv\in\llbracket E\rrbracket=\\{u\mid\exists
E^{\prime}.\,E\to^{*}(u,E^{\prime})\wedge v\in\llbracket
E^{\prime}\rrbracket\\}$.

  3. 3.

$u\in\llbracket E\rrbracket=\\{u\mid\exists
E^{\prime}.\,E\to^{*}(u,E^{\prime})\wedge E^{\prime}{\downarrow}\\}$.

The parts-of-derivatives of a regexp $E$ induce a nondeterministic automaton.
The state set is $Q^{E}=_{\mathrm{df}}\\{E^{\prime}\mid\exists
u\in\Sigma^{*}.\,E\to^{*}(u,E^{\prime})\\}$. The set of initial states is
$I^{E}=_{\mathrm{df}}\\{E\\}$. The set of final states is
$F^{E}=_{\mathrm{df}}\\{E^{\prime}\in Q^{E}\mid E^{\prime}{\downarrow}\\}$.
Finally, the transition relation is defined by
$E^{\prime}\to^{E}(a,E^{\prime\prime})=_{\mathrm{df}}E^{\prime}\to(a,E^{\prime\prime})$
for $E^{\prime},E^{\prime\prime}\in Q^{E}$.

The state set $Q^{E}$ is shown finite by proving it to be a subset of another
set that is straightforwardly seen to be finite.

######  Definition 2.7.

For any $E$, we define a set $E^{\to^{*}}$ of regexps recursively by

$\begin{array}[]{rcl}E^{\to^{*}}&=_{\mathrm{df}}&\\{E\\}\cup
E^{\to^{+}}\\\\[8.61108pt] a^{\to^{+}}&=_{\mathrm{df}}&\\{1\\}\\\
0^{\to^{+}}&=_{\mathrm{df}}&\emptyset\\\
(E+F)^{\to^{+}}&=_{\mathrm{df}}&E^{\to^{+}}\cup F^{\to^{+}}\\\
1^{\to^{+}}&=_{\mathrm{df}}&\emptyset\\\
(EF)^{\to^{+}}&=_{\mathrm{df}}&E^{\to^{+}}\cdot\\{F\\}\cup F^{\to^{+}}\\\
(E^{*})^{\to^{+}}&=_{\mathrm{df}}&E^{\to^{+}}\cdot\\{E^{*}\\}\end{array}$

######  Proposition 2.8.

For any $E$,

  1. 1.

$E^{\to^{*}}$ is finite, in fact, of cardinality linear in the size of $E$;

  2. 2.

$Q^{E}\subseteq E^{\to^{*}}$.

######  Proof 2.9.

Both parts by induction on $E$.

######  Corollary 2.10.

For any $E$, the Antimirov automaton is finite.

We note that the Antimirov automaton, constructed as above, while canonical,
is generally not trim: every state is reachable, but not every state is
generally coreachable (i.e., not every state needs to have a path to some
final state). A state $E^{\prime}$ is not coreachable if and only if
$\llbracket E^{\prime}\rrbracket=\emptyset$. This is the case precisely when
$E^{\prime}$ equals $0$ in the theory of idempotence of $+$ and the left and
right zero laws of $0$ wrt. $\cdot$. The Antimirov automaton is trimmed by
removing the states that are not coreachable.

Now we can also show that a suitable quotient of the Brzozowski automaton is
finite.

For this we prove a syntactic version of Proposition 2.5 relating the
Brzozowski derivative and the Antimirov parts-of-derivatives.

######  Proposition 2.11.

For any $E$,

  1. 1.

for any $a\in\Sigma$, $D_{a}E\doteq\sum\\{E^{\prime}\mid
E\to(a,E^{\prime})\\}$;

  2. 2.

for any $u\in\Sigma^{*}$, $D_{u}E\doteq\sum\\{E^{\prime}\mid
E\to^{*}(u,E^{\prime})\\}$.

(using the semilattice equations for $0,+$, that $0$ is left zero, and
distributivity of $\cdot$ over $+$ from the right).

######  Corollary 2.12.

For any $E$, the Brzozowski automaton, suitably quotiented, is finite.

######  Proof 2.13.

Just notice that the powerset of a finite set is finite too.

This quotient does not give the minimal deterministic automaton (given by
semantic derivatives of $\llbracket E\rrbracket$). The minimal deterministic
automaton is obtained from the Brzozowski automaton by quotienting it by the
full Kleene algebra theory.

##  3 Trace Closures of Regular Languages

###  3.1 Trace Closure of a Word Language

An _independence alphabet_ is an alphabet $\Sigma$ together with an
irreflexive and symmetric relation $I\subseteq\Sigma\times\Sigma$ called the
_independence_ relation. The complement $D$ of $I$, which is reflexive and
symmetric, is called _dependence_. We extend independence to words by saying
that two words $u$ and $v$ are independent, $uIv$, if $aIb$ for all $a,b$ such
that $a\in\Sigma(u)$ and $b\in\Sigma(v)$.

Let $\sim^{I}\subseteq\Sigma^{*}\times\Sigma^{*}$ be the least congruence
relation on the free monoid $\Sigma^{*}$ such that $aIb$ implies
$ab\sim^{I}ba$ for all $a,b\in\Sigma$. If $uIv$, then $uv\sim^{I}vu$.

A _(Mazurkiewicz) trace_ is an equivalence class of words wrt. $\sim^{I}$. The
equivalence class of a word $w$ is denoted by $[w]^{I}$.

A word $a_{1}\ldots a_{n}$ where $a_{i}\in\Sigma$ yields a directed node-
labelled acyclic graph as follows. Take the vertex set to be
$V=_{\mathrm{df}}\\{1,\ldots,n\\}$ and label vertex $i$ with $a_{i}$. Take the
edge set to be $E=_{\mathrm{df}}\\{(i,j)\mid i<j\wedge a_{i}Da_{j}\\}$. This
graph $(V,E)$ for a word $w$ is called the _dependence graph_ of $w$ and is
denoted by $\langle w\rangle_{D}$. If $w\sim^{I}z$, then the dependence graphs
of $w$ and $z$ are isomorphic, i.e., traces can be identified with dependence
graphs up to isomorphism.

The set $\Sigma^{*}/{\sim^{I}}$ of all traces is the free partially
commutative monoid on $(\Sigma,I)$. If $I=\emptyset$, then
$\Sigma^{*}/{\sim^{I}}\cong\Sigma^{*}$, the set of words, i.e., we recover the
free monoid. If $I=\\{(a,b)\mid a\neq b\\}$, then
$\Sigma^{*}/{\sim^{I}}\cong\mathcal{M}_{\mathrm{f}}(\Sigma)$, the set of
finite multisets over $\Sigma$, i.e., the free commutative monoid.

A _trace language_ is a subset of $\Sigma^{*}/{\sim^{I}}$. Trace languages are
in bijection with word languages that are _(trace) closed_ in the sense that,
if $z\in L$ and $w\sim^{I}z$, then also $w\in L$. If $T$ is a trace language,
then its flattening $L=_{\mathrm{df}}\bigcup T$ is a closed word language. On
the other hand, the trace language corresponding to a closed word language $L$
is $T=_{\mathrm{df}}\\{t\in\Sigma^{*}/{\sim^{I}}\mid\exists z\in t.\,z\in
L\\}=\\{t\in\Sigma^{*}/{\sim^{I}}\mid\forall z\in t.\,z\in L\\}$.

Given a general (not necessarily closed) word language $L$, we define its
_(trace) closure_ $[L]^{I}$ as the least closed word language that contains
$L$. Clearly $[L]^{I}=\\{w\in\Sigma^{*}\mid\exists z\in L.\,w\sim^{I}z\\}$ and
also $[L]^{I}=\bigcup\\{t\in\Sigma^{*}/{\sim^{I}}\mid\exists z\in t.\,z\in
L\\}$. For any $L$, we have $[[L]^{I}]^{I}=[L]^{I}$, so $[\\_]^{I}$ is a
closure operator. Note also that $L$ is closed iff $[L]^{I}=L$.

As seen in Section 2.2, the derivative of a word language is the set of all
suffixes for a prefix. We now look at what the prefixes and suffixes of a word
as a representative of a trace should be. For a word $vuv^{\prime}$ such that
$vIu$, we can consider $u$ to be its prefix, up to reordering, and
$vv^{\prime}$ to be the suffix. This is because an equivalent word
$uvv^{\prime}$ strictly has $u$ as a prefix and $vv^{\prime}$ as the suffix.
Similarly, we may also want to consider $u^{\prime}$ to be a prefix of
$vuv^{\prime}$ when $u^{\prime}\sim^{I}u$ since
$u^{\prime}vv^{\prime}\sim^{I}uvv^{\prime}\sim^{I}vuv^{\prime}$. Note that if
$a$ is such a prefix of $z$, then, by irreflexivity of $I$, this $a$ is the
first $a$ of $z$. In general, when $u$ is a prefix of $z$, then the letter
occurrences in $u$ uniquely map to letter occurrences in $z$. We scale these
ideas to allow $u$ to be scattered in $z$ as $z=v_{0}u_{1}v_{1}\ldots
u_{n}v_{n}$ in either the sense that $u=u_{1}\ldots u_{n}$ or
$u\sim^{I}u_{1}\ldots u_{n}$. We also define degree-bounded versions of
scattering that become relevant in Section 5.

######  Definition 3.1.

For all
$u_{1},\ldots,u_{n}\in\Sigma^{+},v_{0}\in\Sigma^{*},v_{1}\ldots,v_{n-1}\in\Sigma^{+},v_{n}\in\Sigma^{*},z\in\Sigma^{*}$,
$u_{1},\ldots,u_{n}\lhd z\rhd
v_{0},\ldots,v_{n}=_{\mathrm{df}}z=v_{0}u_{1}v_{1}\ldots
u_{n}v_{n}\wedge\forall i.\,\forall j<i.\,v_{j}Iu_{i}$.

######  Definition 3.2.

For all $u,v,z\in\Sigma^{*}$,

  1. 1.

$u\lhd z\rhd v=_{\mathrm{df}}\exists
n\in\mathbb{N},u_{1},\ldots,u_{n},v_{0},\ldots,v_{n}.\,u=u_{1}\ldots
u_{n}\wedge v=v_{0}\ldots v_{n}\wedge\\\ \hskip
14.22636ptu_{1},\ldots,u_{n}\lhd z\rhd v_{0},\ldots,v_{n}$;

  2. 2.

$u\mathrel{{\sim}{\lhd}}z\rhd v=_{\mathrm{df}}\exists
u^{\prime}.\,u\sim^{I}u^{\prime}\wedge u^{\prime}\lhd z\rhd v$;

  3. 3.

$u\mathrel{{\sim}{\lhd}}z\mathrel{{\rhd}{\sim}}v=_{\mathrm{df}}\exists
u^{\prime},v^{\prime}.\,u\sim^{I}u^{\prime}\wedge u^{\prime}\lhd z\rhd
v^{\prime}\wedge v^{\prime}\sim^{I}v$.

In all three cases, we talk about $u$ being a prefix and $v$ being a suffix of
$z$, up to reordering, or $uv$ being _scattered_ in $z$ with _degree_ $n$.

######  Lemma 3.3.

For any $u,v,z\in\Sigma^{*}$,

  1. 1.

$u\lhd z\rhd
v\iff\exists!n\in\mathbb{N},u_{1},\ldots,u_{n},v_{0},\ldots,v_{n}.\,u=u_{1}\ldots
u_{n}\wedge v=v_{0}\ldots v_{n}\wedge\\\ \hskip
14.22636ptu_{1},\ldots,u_{n}\lhd z\rhd v_{0},\ldots,v_{n}$;

  2. 2.

$u\mathrel{{\sim}{\lhd}}z\rhd
v\iff\exists!u^{\prime}.\,u\sim^{I}u^{\prime}\wedge u^{\prime}\lhd z\rhd v$;

  3. 3.

$u\mathrel{{\sim}{\lhd}}z\mathrel{{\rhd}{\sim}}v\iff\exists!u^{\prime},v^{\prime}.\,u\sim^{I}u^{\prime}\wedge
u^{\prime}\lhd z\rhd v^{\prime}\wedge v^{\prime}\sim^{I}v$.

######  Definition 3.4.

For all $u,v,z\in\Sigma^{*}$ and $N\in\mathbb{N}$,

  1. 1.

$u\lhd_{N}z\rhd v=_{\mathrm{df}}\exists n\leq
N,u_{1},\ldots,u_{n},v_{0},\ldots,v_{n}.\,u_{1},\ldots,u_{n}\lhd z\rhd
v_{0},\ldots,v_{n}$;

  2. 2.

(and $u\mathrel{{\sim}{\lhd}}_{N}z\rhd v$ and
$u\mathrel{{\sim}{\lhd}}_{N}z\mathrel{{\rhd}{\sim}}v$ are defined
analogously).

######  Example 3.5.

Let $\Sigma=_{\mathrm{df}}\\{a,b,c\\}$ and $aIb$ and $aIc$. Take
$z=_{\mathrm{df}}aabcba$. We have $ab\lhd z\rhd acba$ since $a,b\lhd
z\rhd\varepsilon,a,cba$. We can visualize this by underlining the subwords of
$u=_{\mathrm{df}}ab$ in $z=\varepsilon\underline{a}a\underline{b}cba$. This
scattering is valid because $\varepsilon Ia$, $\varepsilon Ib$ and $aIb$:
recall that Def. 3.1 requires all underlined subwords $u_{i}$ to be
independent with all non-underlined subwords $v_{i}$ to their left in $z$.
Similarly we have $aa,a\lhd z\rhd\varepsilon,bcb,\varepsilon$ because
$z=\varepsilon\underline{aa}bcb\underline{a}\varepsilon$, $\varepsilon Iaa$,
$\varepsilon Ia$ and $bcbIa$. Note that neither
$aa\underline{b}cb\underline{a}\varepsilon$ nor
$aabc\underline{ba}\varepsilon$ satisfies the conditions about independence
and thus there is no $v$ such that $ba\lhd z\rhd v$. We do have
$ba\mathrel{{\sim}{\lhd}}z\rhd acba$ though, since $ba\sim^{I}ab$ and $a,b\lhd
z\rhd\varepsilon,a,cba$.

######  Proposition 3.6.

For all $u,v,z\in\Sigma^{*},uv\sim^{I}z\iff
u\mathrel{{\sim}{\lhd}}z\mathrel{{\rhd}{\sim}}v$.

###  3.2 Trace-Closing Semantics of Regular Expressions

We now define a nonstandard word-language semantics of regexps that directly
interprets $E$ as the trace closure $[\llbracket E\rrbracket]^{I}$ of its
standard regular word-language denotation of $\llbracket E\rrbracket$.

We have $[\\{a\\}]^{I}=\\{a\\}$, $[\emptyset]^{I}=\emptyset$, $[L\cup
L^{\prime}]^{I}=[L]^{I}\cup[L^{\prime}]^{I}$ and
$[\mathbf{1}]^{I}=\mathbf{1}$. But for general $I$, we do not have $[L\cdot
L^{\prime}]^{I}=[L]^{I}\cdot[L^{\prime}]^{I}$. For example, for
$\Sigma=_{\mathrm{df}}\\{a,b\\}$ and $aIb$, we have $[\\{a\\}]^{I}=\\{a\\}$,
$[\\{b\\}]^{I}=\\{b\\}$ whereas
$[\\{ab\\}]^{I}=\\{ab,ba\\}\neq\\{ab\\}=[\\{a\\}]^{I}\cdot[\\{b\\}]^{I}$.
Hence we need a different concatenation operation.

######  Definition 3.7.

  1. 1.

The $I$-_reordering concatenation of words_
$\cdot^{I}:\Sigma^{*}\times\Sigma^{*}\to\mathcal{P}\Sigma^{*}$ is defined by

$\begin{array}[]{rcl}\varepsilon\cdot^{I}v&=_{\mathrm{df}}&\\{v\\}\\\
u\cdot^{I}\varepsilon&=_{\mathrm{df}}&\\{u\\}\\\
au\cdot^{I}bv&=_{\mathrm{df}}&\\{a\\}\cdot(u\cdot^{I}bv)\cup\\{b\mid
auIb\\}\cdot(au\cdot^{I}v)\\\\[8.61108pt] \end{array}$

  2. 2.

The lifting of $I$-reordering concatenation to _languages_ is defined by

$L\cdot^{I}L^{\prime}=_{\mathrm{df}}\bigcup\\{u\cdot^{I}v\mid u\in L\wedge
v\in L^{\prime}\\}$

Note that $\\{b\mid auIb\\}$ acts as a test: it is either $\emptyset$ or
$\\{b\\}$.

######  Example 3.8.

Let $\Sigma=_{\mathrm{df}}\\{a,b\\}$ and $aIb$. Then
$a\cdot^{I}b=\\{ab,ba\\}$, $aa\cdot^{I}b=\\{aab,aba,baa\\}$,
$a\cdot^{I}bb=\\{abb,bab,bba\\}$ and $ab\cdot^{I}ba=\\{abba\\}$. The last
example shows that although $I$-reordering concatenation is defined quite
similarly to shuffle, it is different.

######  Proposition 3.9.

For any $u,v,z\in\Sigma^{*}$, $z\in u\cdot^{I}v\iff u\lhd z\rhd v$.

######  Proposition 3.10.

For any languages $L$ and $L^{\prime}$, $[L\cdot
L^{\prime}]^{I}=[L]^{I}\cdot^{I}[L^{\prime}]^{I}$.

Evidently, if $I=\emptyset$, then reordering concatenation is just ordinary
concatenation: $u\cdot^{\emptyset}v=\\{uv\\}$. For $I=\Sigma\times\Sigma$,
which is forbidden in independence alphabets, as $I$ is required to be
irreflexive, it is shuffle:
$u\cdot^{\Sigma\times\Sigma}v=u\mathrel{{\sqcup}{\sqcup}}v$. For general $I$,
it has properties similar to concatenation. In particular, we have

$\begin{array}[]{rcl@{\quad}rcl}\mathbf{1}\cdot^{I}L&=&L&\emptyset\cdot^{I}L&=&\emptyset\\\
L\cdot^{I}\mathbf{1}&=&L&(L_{1}\cup L_{2})\cdot^{I}L&=&L_{1}\cdot^{I}L\cup
L_{2}\cdot^{I}L\\\
(L\cdot^{I}L^{\prime})\cdot^{I}L^{\prime\prime}&=&L\cdot^{I}(L^{\prime}\cdot^{I}L^{\prime\prime})&(L_{1}\mathrel{{\sqcup}{\sqcup}}L_{2})\cdot^{I}(L_{1}^{\prime}\mathrel{{\sqcup}{\sqcup}}L_{2}^{\prime})&\subseteq&(L_{1}\cdot^{I}L_{1}^{\prime})\mathrel{{\sqcup}{\sqcup}}(L_{2}\cdot^{I}L_{2}^{\prime})\end{array}$

but also other equations of the concurrent Kleene algebra theory introduced in
[10].

We are ready to introduce the closing semantics of regular expressions.

######  Definition 3.11.

The _trace-closing semantics_
$\llbracket\\_\rrbracket^{I}:\mathsf{RE}\to\mathcal{P}\Sigma^{*}$ of regular
expressions is defined recursively by

$\small\begin{array}[]{rcl@{\qquad}rcl}\llbracket
a\rrbracket^{I}&=_{\mathrm{df}}&\\{a\\}&\llbracket
1\rrbracket^{I}&=_{\mathrm{df}}&\mathbf{1}\\\ \llbracket
0\rrbracket^{I}&=_{\mathrm{df}}&\emptyset&\llbracket
EF\rrbracket^{I}&=_{\mathrm{df}}&\llbracket E\rrbracket^{I}\cdot^{I}\llbracket
F\rrbracket^{I}\\\ \llbracket E+F\rrbracket^{I}&=_{\mathrm{df}}&\llbracket
E\rrbracket^{I}\cup\llbracket F\rrbracket^{I}&\llbracket
E^{*}\rrbracket^{I}&=_{\mathrm{df}}&\mu X.\,\mathbf{1}\cup\llbracket
E\rrbracket^{I}\cdot^{I}X\end{array}$

Compared to the standard semantics of regular expressions, the difference is
in the handling of the $EF$ case (and consequently also the $E^{*}$ case) due
to the cross-commutation that happens in concatenation of traces and must be
accounted for by ${\cdot^{I}}$.

With $I=\emptyset$, we fall back to the standard interpretation of regular
expressions: $\llbracket E\rrbracket^{\emptyset}=\llbracket E\rrbracket$. For
$I$ a general independence relation, we obtain the desired property that the
semantics delivers the trace closure of the language of the regexp.

######  Proposition 3.12.

For any $E$, $\llbracket E\rrbracket^{I}$ is trace closed; moreover,
$\llbracket E\rrbracket^{I}=[\llbracket E\rrbracket]^{I}$.

###  3.3 Properties of Trace Closures of Regular Languages

Trace closures of regular languages are theoretically interesting due to their
intricate properties and have therefore been studied in a number of works,
e.g., [4, 18, 2, 21, 9, 12]. For a thorough survey, see Ochmański’s handbook
chapter [19].

The most important property for us is that the trace closure of a regular
language is not necessarily regular.

######  Proposition 3.13.

There exists a regular language $L$ such that $[L]^{I}$ is not regular.

######  Proof 3.14.

Consider $\Sigma=_{\mathrm{df}}\\{a,b\\}$, $aIb$. Let
$L=_{\mathrm{df}}\llbracket(ab)^{*}\rrbracket$. The language
$[L]^{I}=\\{u\mid|u|_{a}=|u|_{b}\\}$ is not regular.

The class of trace closures of regular languages over an independence alphabet
behaves quite differently from the class of regular languages over an
alphabet. Here are some results demonstrating this.

######  Theorem 3.15 (Bertoni et al. [5], Aalbersberg and Welzl [2],
Sakarovitch [21]).

(cf. [19, Thm. 6.2.5]) The class of trace closures of regular languages over
$(\Sigma,I)$ is closed under complement iff $I$ is quasi-transitive (i.e., its
reflexive closure is transitive).

######  Theorem 3.16 (Bertoni et al. [4], Aalbersberg and Welzl [2] (“if”
part); Aalbersberg and Hoogeboom [1]).

(cf. [19, Thm. 6.2.5]) The problem of whether the trace closures of two
regular languages over $(\Sigma,I)$ are equal is decidable iff $I$ is quasi-
transitive.

######  Theorem 3.17 (Sakarovitch [22]).

(cf. [19, Thm. 6.2.7]) The problem of whether the trace closure of the
language of a regexp over $(\Sigma,I)$ is regular is decidable iff $I$ is
quasi-transitive.

A closed language is regular iff the corresponding trace language is accepted
by a finite asynchronous (a.k.a. Zielonka) automaton [24, 25]. In Section 4.4,
we will see further characterizations of regular closed languages based on
star-connected expressions.

###  3.4 Rational and Recognizable Languages of Monoids

Trace languages are a special case of languages of monoids.

A subset $T$ of a monoid $M$ is called an $M$-language.

An $M$-language $T$ is called _rational_ if $T=\llbracket E\rrbracket^{M}$ for
some regular expression $E$ over $M$. Here
$\llbracket\\_\rrbracket^{M}:\mathsf{RE}(M)\to\mathcal{P}M$ interprets any
element $m$ of $M$ as $\\{m\\}$, the $0,+$ constructors of regular expressions
by $\emptyset$ and $\cup$, the $1,{\cdot}$ constructors as mandated by the
monoid structure, and $(\\_)^{*}$ as the appropriate least fixpoint.

An $M$-language $T$ is called _recognizable_ if there is a deterministic
finite $M$-automaton accepting $T$. An deterministic $M$-automaton is given by
a state set $Q$, an initial state $q_{0}\in Q$, a set of final states
$F\subseteq Q$, and a right action $\delta$ of $M$ on $Q$. An element $m\in M$
is accepted by the automaton if $\delta_{m}q_{0}\in F$.

Kleene’s celebrated theorem says that, for languages of free monoids on finite
sets (i.e., word languages over finite alphabets), rationality and
recognizability are equivalent conditions (and we can thus just speak about
regularity). For a general monoid, however, the two notions are different.

######  Theorem 3.18 (Kleene [11]).

Let $M$ be the free monoid $\Sigma^{*}$ on a finite set $\Sigma$. An
$M$-language $T$ is rational iff $T$ is recognizable.

######  Theorem 3.19 (McKnight [17]).

Let $M$ be finitely generated. If an $M$-language $T$ is recognizable, then
$T$ is rational.

Given a monoid $M$ and a congruence $\equiv$ on $M$, the set $M/{\equiv}$ is a
monoid too. We view $M/{\equiv}$-languages as sets of equivalence classes wrt.
$\equiv$.

######  Proposition 3.20.

Given a monoid $M$ and a congruence $\equiv$ on it.

  1. 1.

The $M/{\equiv}$-language $\llbracket E\rrbracket^{M/{\equiv}}$ of a regular
expression $E$ is expressible via its $M$-language $\llbracket
E\rrbracket^{M}$ by $\llbracket E\rrbracket^{M/{\equiv}}=\\{t\in
M/{\equiv}\mid\exists u\in t.\,u\in\llbracket E\rrbracket^{M}\\}$.

  2. 2.

A $M/{\equiv}$-language $T$ is recognizable iff its flattening $\bigcup T$
into an $M$-language is recognizable.

For the monoid $\Sigma^{*}/{\sim^{I}}$ of traces, which is the free partially
commutative monoid, the classes of rational and recognizable languages are
different, the class of rational languages is a proper subclass of that of
recognizable languages. In view of Proposition 3.20, a trace language $T$ is
rational iff $T=\\{t\in\Sigma^{*}/{\sim^{I}}\mid\exists u\in t.\,u\in L\\}$
or, equivalently, $\bigcup T=[L]^{I}$ for some regular word language $L$ (in
the alternative terminology of Aalbersberg and Welzl [2], such a trace
language $T$ is called _existentially regular_), and recognizable iff $\bigcup
T=L$ for some regular word language $L$ (such a trace language is called
_consistently regular_).

The question of when a rational trace language is recognizable is nontrivial.
We have just seen that, reformulated in terms of word languages, it becomes:
given a regular language $L$, when is its trace closure $[L]^{I}$ regular?

##  4 Reordering Derivatives

We are now ready to generalize the Brzozowski and Antimirov constructions for
trace closures of regular languages. To this end, we switch to what we call
reordering derivatives.

###  4.1 Reordering Derivative of a Language

Let $(\Sigma,I)$ be a fixed independence alphabet. We generalize the concepts
of (semantic) nullability and derivative of a language to concepts of
reorderable part and reordering derivative.

######  Definition 4.1.

We define the _$I$ -reorderable part_ of a language $L$ wrt. a word $u$ by
$R^{I}_{u}L=_{\mathrm{df}}\\{v\in L\mid vIu\\}$ and the _$I$ -reordering
derivative_ along $u$ by $D^{I}_{u}L=_{\mathrm{df}}\\{v\mid\exists z\in
L.\,u\mathrel{{\sim}{\lhd}}z\rhd v\\}$.

By Prop. 3.9, we can equivalently say that $D^{I}_{u}L=\\{v\mid\exists z\in
L.\,z\in[u]^{I}\cdot^{I}v\\}$. For a single-letter word $a$, we get
$D^{I}_{a}L=\\{v_{l}v_{r}\mid v_{l}av_{r}\in L\wedge
v_{l}Ia\\}=\\{v\mid\exists z\in L.\,z\in a\cdot^{I}v\\}$. That is, we require
some reordering of $u$ (resp. $a$) to be a prefix, up to reordering, of some
word $z$ in $L$ with $v$ as the corresponding strict suffix. (In other words,
for the sake of precision and emphasis, we allow reordering of letters within
$u$ and across $u$ and $v$, but not within $v$.)

######  Example 4.2.

Let $\Sigma=_{\mathrm{df}}\\{a,b,c\\}$ and $aIb$. Take
$L=_{\mathrm{df}}\\{\varepsilon,a,b,ca,aa,bbb,babca,abbaba\\}$. We have
$R^{I}_{a}L=R^{I}_{aa}L=\\{\varepsilon,b,bbb\\}$,
$D^{I}_{a}L=\\{\varepsilon,a,bbca,bbaba\\}$ and
$D^{I}_{aa}L=\\{\varepsilon,bbba\\}$.

In the special case $I=\emptyset$, we have $R^{\emptyset}_{\varepsilon}L=L$,
$R^{\emptyset}_{u}L=\\{\varepsilon\mid L{\downarrow}\\}$ for any
$u\neq\varepsilon$, and $D^{\emptyset}_{u}L=D_{u}L$. In the general case, the
reorderable part and reordering derivative enjoy the following properties.

######  Lemma 4.3.

For every $L$, $L^{\prime}$, for any $u\in\Sigma^{*}$, if $L\subseteq
L^{\prime}$, then $R^{I}_{u}L\subseteq R^{I}_{u}L^{\prime}$ and
$D^{I}_{u}L\subseteq D^{I}_{u}L^{\prime}$.

######  Lemma 4.4.

For every $L$,

  1. 1.

$R^{I}_{\varepsilon}L=L$; for every $u,v\in\Sigma^{*}$,
$R^{I}_{v}(R^{I}_{u}L)=R^{I}_{uv}L$;

  2. 2.

for every $u,u^{\prime}\in\Sigma^{*}$,
$R^{I}_{\Sigma(u)}L=R^{I}_{\Sigma(u^{\prime})}L$.

We extend $R^{I}$ to subsets of $\Sigma$: by $R^{I}_{X}L$, we mean
$R^{I}_{u}L$ where $u$ is any enumeration of $X$.

######  Lemma 4.5.

For every $L$,

  1. 1.

$D^{I}_{\varepsilon}L=L$; for any $u,v\in\Sigma^{*}$,
$D^{I}_{v}(D^{I}_{u}L)=D^{I}_{uv}L$;

  2. 2.

for any $u,u^{\prime}\in\Sigma^{*}$ such that $u\sim^{I}u^{\prime}$, we have
$D^{I}_{u}L=D^{I}_{u^{\prime}}L$.

######  Proposition 4.6.

For every $L$,

  1. 1.

for any $u\in\Sigma^{*}$, $D_{u}([L]^{I})=[D^{I}_{u}L]^{I}$;
if $L$ is closed (i.e., $[L]^{I}=L$), then, for any $u\in\Sigma^{*}$,
$D^{I}_{u}L$ is closed and $D_{u}L=D^{I}_{u}L$;

  2. 2.

for any $u,v\in\Sigma^{*}$, $uv\in[L]^{I}$ iff $v\in[D^{I}_{u}L]^{I}$;

  3. 3.

for any $u\in\Sigma^{*}$, $u\in[L]^{I}$ iff $(D^{I}_{u}L){\downarrow}$;

  4. 4.

$[L]^{I}=\\{\varepsilon\mid
L{\downarrow}\\}\cup\bigcup_{a\in\Sigma}\\{a\\}\cdot[D^{I}_{a}L]^{I}$.

######  Example 4.7.

Let $\Sigma=_{\mathrm{df}}\\{a,b\\}$ and $aIb$. Take $L$ to be the regular
language $\llbracket(ab)^{*}\rrbracket$. We have already noted that the
language $[L]^{I}=\\{u\mid|u|_{a}=|u|_{b}\\}$ is not regular. For any
$n\in\mathbb{N}$, $D^{I}_{b^{n}}L=\\{a^{n}\\}\cdot L=\llbracket
a^{n}(ab)^{*}\rrbracket$ whereas
$D_{b^{n}}([L]^{I})=\\{a^{n}\\}\cdot^{I}[L]^{I}=\\{u\mid|u|_{a}=|u|_{b}+n\\}$.
We can see that $[L]^{I}$ has infinitely many derivatives, none of which are
regular, and $L$ has infinitely many reordering derivatives, all regular.

###  4.2 Brzozowski Reordering Derivative

The reorderable parts and reordering derivatives of regular languages turn out
to be regular. We now show that they can be computed syntactically,
generalizing the classical syntactic nullability and Brzozowski derivative
operations [7].

######  Definition 4.8.

The _$I$ -reorderable part_ and the _Brzozowski $I$-reordering derivative_ of
a regexp are given by functions
$R^{I},D^{I}:\mathsf{RE}\times\Sigma\to\mathsf{RE}$ and
$R^{I},D^{I}:\mathsf{RE}\times\Sigma^{*}\to\mathsf{RE}$ defined recursively by

$\small\begin{array}[]{rcl@{\qquad}rcl}R^{I}_{a}b&=_{\mathrm{df}}&\mathsf{if\leavevmode\nobreak\
}aIb\mathsf{\leavevmode\nobreak\ then\leavevmode\nobreak\
}b\mathsf{\leavevmode\nobreak\ else\leavevmode\nobreak\
}0&D^{I}_{a}b&=_{\mathrm{df}}&\mathsf{if\leavevmode\nobreak\
}a=b\mathsf{\leavevmode\nobreak\ then\leavevmode\nobreak\
}1\mathsf{\leavevmode\nobreak\ else\leavevmode\nobreak\ }0\\\
R^{I}_{a}0&=_{\mathrm{df}}&0&D^{I}_{a}0&=_{\mathrm{df}}&0\\\
R^{I}_{a}(E+F)&=_{\mathrm{df}}&R^{I}_{a}E+R^{I}_{a}F&D^{I}_{a}(E+F)&=_{\mathrm{df}}&D^{I}_{a}E+D^{I}_{a}F\\\
R^{I}_{a}1&=_{\mathrm{df}}&1&D^{I}_{a}1&=_{\mathrm{df}}&0\\\
R^{I}_{a}(EF)&=_{\mathrm{df}}&(R^{I}_{a}E)(R^{I}_{a}F)&D^{I}_{a}(EF)&=_{\mathrm{df}}&(D^{I}_{a}E)F+(R^{I}_{a}E)(D^{I}_{a}F)\\\
R^{I}_{a}(E^{*})&=_{\mathrm{df}}&(R^{I}_{a}E)^{*}&D^{I}_{a}(E^{*})&=_{\mathrm{df}}&(R^{I}_{a}E)^{*}(D^{I}_{a}E)E^{*}\\\\[7.74997pt]
R^{I}_{\varepsilon}E&=_{\mathrm{df}}&E&D^{I}_{\varepsilon}E&=_{\mathrm{df}}&E\\\
R^{I}_{ua}E&=_{\mathrm{df}}&R^{I}_{a}(R^{I}_{u}E)&D^{I}_{ua}E&=_{\mathrm{df}}&D^{I}_{a}(D^{I}_{u}E)\end{array}$

The regexp $R_{u}E$ is nothing but $E$ with all occurrences of letters
dependent with $u$ replaced with $0$. The definition of $D$ is more
interesting. Compared to the classical Brzozowski derivative, the nullability
condition $E{\downarrow}$ in the $EF$ case has been replaced with
concatenation with the reorderable part $R^{I}_{a}E$, and the $E^{*}$ case has
also been adjusted.

The functions $R$ and $D$ on regexps compute their semantic counterparts on
the corresponding regular languages.

######  Proposition 4.9.

For any $E$,

  1. 1.

for any $a\in\Sigma$, $R^{I}_{a}\llbracket E\rrbracket=\llbracket
R^{I}_{a}E\rrbracket$ and $D^{I}_{a}\llbracket E\rrbracket=\llbracket
D^{I}_{a}E\rrbracket$;

  2. 2.

for any $u\in\Sigma^{*}$, $R^{I}_{u}\llbracket E\rrbracket=\llbracket
R^{I}_{u}E\rrbracket$ and $D^{I}_{u}\llbracket E\rrbracket=\llbracket
D^{I}_{u}E\rrbracket$.

######  Proposition 4.10.

For any $E$,

  1. 1.

for any $a\in\Sigma$, $v\in\Sigma^{*}$, $av\in\llbracket E\rrbracket^{I}\iff
v\in\llbracket D^{I}_{a}E\rrbracket^{I}$;

  2. 2.

for any $u,v\in\Sigma^{*}$, $uv\in\llbracket E\rrbracket^{I}\iff
v\in\llbracket D^{I}_{u}E\rrbracket^{I}$;

  3. 3.

for any $u\in\Sigma^{*}$, $u\in\llbracket
E\rrbracket^{I}\iff(D^{I}_{u}E){\downarrow}$.

######  Example 4.11.

Let $\Sigma=_{\mathrm{df}}\\{a,b\\}$, $aIb$ and $E=_{\mathrm{df}}aa+ab+b$.

$\begin{array}[]{rcl}\small D^{I}_{b}E&=&D^{I}_{b}aa+D^{I}_{b}ab+D^{I}_{b}b\\\
&=&((D^{I}_{b}a)a+(R^{I}_{b}a)(D^{I}_{b}a))+((D^{I}_{b}a)b+(R^{I}_{b}a)(D^{I}_{b}b))+D^{I}_{b}b\\\
&=&(0a+a0)+(0b+a1)+1\doteq a+1\\\\[8.61108pt]
D^{I}_{b}(E^{*})&=&(R^{I}_{b}E)^{*}(D^{I}_{b}E)E^{*}\\\
&=&(aa+a0+0)^{*}((0a+a0)+(0b+a1)+1)E^{*}\doteq(aa)^{*}(a+1)E^{*}\\\\[8.61108pt]
D^{I}_{bb}(E^{*})&\doteq&D^{I}_{b}((aa)^{*}(a+1)E^{*})\doteq(aa)^{*}(a+1)(aa)^{*}(a+1)E^{*}\end{array}$

As with the classical Brzozowski derivative, we can use the reordering
Brzozowski derivative to construct deterministic automata. For a regexp $E$,
take $Q^{E}=_{\mathrm{df}}\\{D^{I}_{u}E\mid u\in\Sigma^{*}\\}$,
$q^{E}_{0}=_{\mathrm{df}}E$, $F^{E}=_{\mathrm{df}}\\{E^{\prime}\in Q^{E}\mid
E^{\prime}{\downarrow}\\}$,
$\delta^{E}_{a}E^{\prime}=_{\mathrm{df}}D^{I}_{a}E^{\prime}$ for
$E^{\prime}\in Q^{E}$. By Prop. 4.10, this automaton accepts the closure
$\llbracket E\rrbracket^{I}$. But even quotiented by the full Kleene algebra
theory, the quotient of $Q^{E}$ is not necessarily finite, i.e., we may be
able to construct infinitely many different languages by taking reordering
derivatives. For the regexp from Example 4.7, we have
$D^{I}_{b^{n}}((ab)^{*})\doteq a^{n}(ab)^{*}$, so it has infinitely many
Brzozowski reordering derivatives even up to the Kleene algebra theory. This
is only to be expected, as the closure $\llbracket(ab)^{*}\rrbracket^{I}$ is
not regular and cannot possibly have an accepting finite automaton.

###  4.3 Antimirov Reordering Derivative

Like the classical Brzozowski derivative that was optimized by Antimirov [3],
the Brzozowski reordering derivative construction can be optimized by
switching from functions on regexps to multivalued functions or relations.

######  Definition 4.12.

The _Antimirov $I$-reordering parts-of-derivatives_ of a regexp along a letter
and a word are relations
${\to^{I}}\subseteq\mathsf{RE}\times\Sigma\times\mathsf{RE}$ and
${\to^{I*}}\subseteq\mathsf{RE}\times\Sigma^{*}\times\mathsf{RE}$ defined
inductively by

$\small\begin{array}[]{l}a\to^{I}(a,1)\quad
E+F\to^{I}(a,E^{\prime})E\to^{I}(a,E^{\prime})\quad
E+F\to^{I}(a,F^{\prime})F\to^{I}(a,F^{\prime})\\\\[7.74997pt]
EF\to^{I}(a,E^{\prime}F)E\to^{I}(a,E^{\prime})\quad
EF\to^{I}(a,(R^{I}_{a}E)F^{\prime})F\to^{I}(a,F^{\prime})\quad
E^{*}\to^{I}(a,(R^{I}_{a}E)^{*}E^{\prime}E^{*})E\to^{I}(a,E^{\prime})\\\\[7.74997pt]
E\to^{I*}(\varepsilon,E)\quad
E\to^{I*}(ua,E^{\prime\prime})\lx@proof@logical@and
E\to^{I*}(u,E^{\prime})E^{\prime}\to^{I}(a,E^{\prime\prime})\end{array}$

Here $R^{I}$ is defined as before. Similarly to the Brzozowski reordering
derivative from the previous subsection, the condition $E{\downarrow}$ in the
second $EF$ rule has has been replaced with concatenation with $R^{I}_{a}E$,
and the $E^{*}$ rule has been adjusted.

Collectively, the Antimirov reordering parts-of-derivatives of a regexp $E$
compute the semantic reordering derivative of the language $\llbracket
E\rrbracket$.

######  Proposition 4.13.

For any $E$,

  1. 1.

for any $a\in\Sigma$, $D^{I}_{a}\llbracket E\rrbracket=\bigcup\\{\llbracket
E^{\prime}\rrbracket\mid E\to^{I}(a,E^{\prime})\\}$;

  2. 2.

for any $u\in\Sigma^{*}$, $D^{I}_{u}\llbracket
E\rrbracket=\bigcup\\{\llbracket E^{\prime}\rrbracket\mid
E\to^{I*}(u,E^{\prime})\\}$.

######  Proposition 4.14.

For any $E$,

  1. 1.

for any $a\in\Sigma$, $v\in\Sigma^{*}$, $av\in\llbracket
E\rrbracket^{I}\iff\exists E^{\prime}.\,E\to^{I}(a,E^{\prime})\wedge
v\in\llbracket E^{\prime}\rrbracket^{I}$;

  2. 2.

for any $u,v\in\Sigma^{*}$, $uv\in\llbracket E\rrbracket^{I}\iff\exists
E^{\prime}.\,E\to^{I*}(u,E^{\prime})\wedge v\in\llbracket
E^{\prime}\rrbracket^{I}$;

  3. 3.

for any $u\in\Sigma^{*}$, $u\in\llbracket E\rrbracket^{I}\iff\exists
E^{\prime}.\,E\to^{I*}(u,E^{\prime})\wedge E^{\prime}{\downarrow}$.

######  Example 4.15.

Let us revisit Example 4.11. The Antimirov reordering parts-of-derivatives of
$E$ along $b$ are $a1$ and $1$:

$\small\begin{array}[]{l}aa+ab+b\to^{I}(b,a1)ab+b\to^{I}(b,a1)ab\to^{I}(b,a1)b\to^{I}(b,1)\qquad
aa+ab+b\to^{I}(b,1)ab+b\to^{I}(b,1)b\to^{I}(b,1)\end{array}$

The Antimirov reordering parts-of-derivatives of $E^{*}$ along $b$ are
therefore $E_{b}^{*}(a1)E^{*}$ and $E_{b}^{*}1E^{*}$ where
$E_{b}=_{\mathrm{df}}R^{I}_{b}E=aa+a0+0$. Recall that, for the Brzozowski
reordering derivative, we computed $D^{I}_{b}E=(0a+a0)+(0b+a1)+1$ and
$D^{I}_{b}E^{*}=E_{b}^{*}((0a+a0)+(0b+a1)+1)E^{*}$.

Like the classical Antimirov construction, the Antimirov reordering parts-of-
derivatives of a regexp $E$ give a nondeterministic automaton by
$Q^{E}=_{\mathrm{df}}\\{E^{\prime}\mid\exists
u\in\Sigma^{*}.\,E\to^{I*}(u,E^{\prime})\\}$, $I^{E}=_{\mathrm{df}}\\{E\\}$,
$F^{E}=_{\mathrm{df}}\\{E^{\prime}\in Q^{E}\mid E^{\prime}{\downarrow}\\}$,
$E^{\prime}\to^{E}(a,E^{\prime\prime})=_{\mathrm{df}}E^{\prime}\to^{I}(a,E^{\prime\prime})$
for $E^{\prime},E^{\prime\prime}\in Q^{E}$. This automaton accepts $\llbracket
E\rrbracket^{I}$ by Prop. 4.14, but is generally infinite, also if quotiented
by the full Kleene algebra theory. Revisiting Example 4.7 again, $(ab)^{*}$
must have infinitely many Antimirov reordering parts-of-derivatives modulo the
Kleene algebra theory since $\llbracket(ab)^{*}\rrbracket^{I}$ is not regular
and cannot have a finite accepting nondeterministic automaton. Specifically,
it has $(a0)^{*}((a1)\ldots((a0)^{*}((a1)(ab)^{*}))\ldots)\doteq
a^{n}(ab)^{*}$ as its single reordering part-of-derivative along $b^{n}$.

However, if quotienting the Antimirov automaton for $E$ by some sound theory
(a theory weaker than the Kleene algebra theory) makes it finite, then the
Brzozowski automaton can also be quotiented to become finite.

######  Proposition 4.16.

For any $E$,

  1. 1.

for any $a\in\Sigma$, $D^{I}_{a}E\doteq\sum\\{E^{\prime}\mid
E\to^{I}(a,E^{\prime})\\}$;

  2. 2.

for any $u\in\Sigma^{*}$, $D^{I}_{u}E\doteq\sum\\{E^{\prime}\mid
E\to^{I*}(u,E^{\prime})\\}$

(using the semilattice equations for $0,+$, that $0$ is zero, and
distributivity of $\cdot$ over $+$).

######  Corollary 4.17.

If some quotient of the Antimirov automaton for $E$ (accepting $\llbracket
E\rrbracket^{I}$) is finite, then also some quotient of the Brzozowski
automaton is finite.

###  4.4 Star-Connected Expressions

Star-connected expressions are important as they characterize regular closed
languages. A corollary of that is a further characterization of such languages
in terms of a “concurrent” semantics of regexps that interprets Kleene star
nonstandardly as “concurrent star”.

######  Definition 4.18.

A word $w\in\Sigma^{*}$ is connected if its dependence graph $\langle
w\rangle_{D}$ is connected. A language $L\subseteq\Sigma^{*}$ is connected if
every word $w\in L$ is connected.

######  Definition 4.19.

  1. 1.

_Star-connected expressions_ are a subset of the set of all regexps defined
inductively by: $0$, $1$ and $a\in\Sigma$ are star-connected. If $E$ and $F$
are star-connected, then so are $E+F$ and $EF$. If $E$ is star-connected and
$\llbracket E\rrbracket$ is connected, then $E^{*}$ is star-connected.

  2. 2.

A language $L$ is said to be _star-connected_ if $L=\llbracket E\rrbracket$
for some star-connected regexp.

Ochmański [18] proved that a closed language is regular iff it is the closure
of a star-connected language. This means that, for any regexp $E$, the
language $\llbracket E\rrbracket^{I}$ is regular iff there exists a star-
connected expression $E^{\prime}$ such that $\llbracket
E\rrbracket^{I}=\llbracket E^{\prime}\rrbracket^{I}$. It is important to
realize that generally $E\neq E^{\prime}$ and also $\llbracket
E\rrbracket\neq\llbracket E^{\prime}\rrbracket$. Ochmański’s proof was as
follows.

For a linear order $\leq$ on $\Sigma$, a word $z$ is a _lexicographic normal
form_ if $\forall w\in[z]^{I}.\,z\leq_{\mathrm{lex}}w$ where
$\leq_{\mathrm{lex}}$ is the lexicographic order on $\Sigma^{*}$ induced by
$\leq$. We write $\mathrm{Lex}^{I}$ for the set of all lexicographic normal
forms.

######  Lemma 4.20.

(cf. [19, Props. 6.3.4, 6.3.10])

  1. 1.

$\mathrm{Lex}^{I}$ is regular.

  2. 2.

For any regular expression $E$, if $\llbracket
E\rrbracket\subseteq\mathrm{Lex}^{I}$, then $E$ is star-connected.

######  Theorem 4.21 (Ochmański [18]).

(cf. [19, Thm. 6.3.13]) For any closed language $L$, the following are
equivalent:

  1. 1.

$L$ is regular;

  2. 2.

$L\cap\mathrm{Lex}^{I}$ is regular;

  3. 3.

$L$ is star-connected.

######  Proof 4.22.

(1) $\Rightarrow$ (2) is a consequence of Lemma 4.20(1) as the intersection of
regular languages is regular. (2) $\Longrightarrow$ (3) follows from Lemma
4.20(2). For (3) $\Longrightarrow$ (1), Ochmański employed Hachiguchi’s notion
of rank of a language and Hachiguchi’s lemma, which we will study in Def. 5.1
and Prop. 5.2 below, and proved that, if $L$ is closed and connected, then
$L^{*}$ has rank.

The nonstandard _concurrent-star trace-language semantics_ of regular
expressions
$\llbracket\\_\rrbracket^{\mathrm{con}}:\mathsf{RE}(\Sigma)\to\mathcal{P}\Sigma^{*}$
is like $\llbracket\\_\rrbracket$ except that the star constructor is
interpreted nonstandardly as the _concurrent star_ operation. Informally, the
concurrent star of a language iterates not the given language but the language
of connected components of its words.

The concurrent star of a connected language coincides with its Kleene star.
The idea of this nonstandard semantics is to make non-star-connected regular
expressions harmless, so as to obtain the following replacement for Kleene’s
theorem.

######  Theorem 4.23 (Ochmański [18]).

(cf. [19, Thm. 6.3.16]) A closed langugage $L$ is regular iff $L=[\llbracket
E\rrbracket^{\mathrm{con}}]^{I}$ for some regexp $E$.

###  4.5 Automaton Finiteness for Star-Connected Expressions

We now show that the set of Antimirov reordering parts-of-derivatives of a
star-connected expression is finite modulo suitable equations.

######  Lemma 4.24.

If a language $L$ is connected, then for any $u\in\Sigma^{+}$,
$R^{I}_{u}(D^{I}_{u}L)\subseteq\mathbf{1}$.

######  Proof 4.25.

Because $L$ is connected, if $w\in D^{I}_{u}L$, then $aDb$ for some $a\in u$
and $b\in w$. For such $w$ to also be in $R^{I}_{u}(D^{I}_{u}L)$, we also need
that $wIu$. This is only possible if $w=\varepsilon$.

######  Lemma 4.26.

For any $E$, if $\llbracket E\rrbracket\subseteq\mathbf{1}$, then either
$E\doteq 0$ or $E\doteq 1$ (using the equations involving $0$ and $1$ only
(e.g., $0+1\doteq 1$ and $0^{*}\doteq 1$ etc.) and that $0$ is zero).

######  Lemma 4.27.

For any $E$, $E^{\prime}$ and $u\in\Sigma^{+}$, if $\llbracket E\rrbracket$ is
connected and $E\to^{I*}(u,E^{\prime})$, then $R^{I}_{u}E^{\prime}\doteq 0$ or
$R^{I}_{u}E^{\prime}\doteq 1$ (using the equations involving $0$ and $1$ only
and that $0$ is zero).

######  Proof 4.28.

From $E\to^{I*}(u,E^{\prime})$ by Proposition 4.13, $\llbracket
E^{\prime}\rrbracket\subseteq D^{I}_{u}\llbracket E\rrbracket$. Hence by Lemma
4.24, we get $\llbracket R^{I}_{u}E^{\prime}\rrbracket=R^{I}_{u}\llbracket
E^{\prime}\rrbracket\subseteq R^{I}_{u}(D^{I}_{u}\llbracket
E\rrbracket)\subseteq\mathbf{1}$. By Lemma 4.26, $R^{I}_{u}E^{\prime}\doteq 0$
or $R^{I}_{u}E^{\prime}\doteq 1$.

######  Lemma 4.29.

For any $E$, $E^{\prime}$ and $u\in\Sigma^{*}$, if
$E^{*}\to^{I*}(u,E^{\prime})$, then there exist $n\in\mathbb{N}$,
$E_{1},\ldots,E_{n}$, $\emptyset\subset X_{0},\ldots,X_{n-1}\subseteq\Sigma$
and $u_{1},\ldots,u_{n}\in\Sigma^{+}$ such that

$E^{\prime}\doteq(R^{I}_{X_{0}}E)^{*}(R^{I}_{X_{1}}E_{1})(R^{I}_{X_{1}}E)^{*}\ldots(R^{I}_{X_{n-1}}E_{n-1})(R^{I}_{X_{n-1}}E)^{*}E_{n}E^{*}$

where $X_{i-1}\supseteq X_{i}\cup\Sigma(u_{i})$ and $E\to^{I*}(u_{i},E_{i})$
for all $i$ (using only associativity of $\cdot$).

######  Lemma 4.30.

For any $E$, $E^{\prime}$ and $u\in\Sigma^{*}$, if $\llbracket E\rrbracket$ is
connected, $E^{*}\to^{I*}(u,E^{\prime})$ and, for the development of
$E^{\prime}$ from the previous lemma, we have $X_{i-1}=X_{i}$ for some $i$,
then $R^{I}_{X_{i}}E_{i}\doteq 0$ or $R^{I}_{X_{i}}E_{i}\doteq 1$ (using the
equations involving $0$ and $1$ only, that $0$ is zero).

######  Proof 4.31.

We have $\Sigma(u_{i})\subseteq X_{i-1}=X_{i}$. From $E\to^{I*}(u_{i},E_{i})$,
by Lemma 4.27 either $R^{I}_{u_{i}}E_{i}\doteq 0$ or $R^{I}_{u_{i}}E_{i}\doteq
1$. Therefore also $R^{I}_{X_{i}}E_{i}\doteq 0$ or $R^{I}_{X_{i}}E_{i}\doteq
1$.

######  Lemma 4.32.

For any $E$, $E^{\prime}$ and $u\in\Sigma^{*}$, if $\llbracket E\rrbracket$ is
connected and $E^{*}\to^{I*}(u,E^{\prime})$, then there exist $n\leq|\Sigma|$,
$E_{1},\ldots,E_{n}$ and $\emptyset\subset
X_{0},\ldots,X_{n-1}\subseteq\Sigma$ such that

$E^{\prime}\doteq(R^{I}_{X_{0}}E)^{*}(R^{I}_{X_{1}}E_{1})(R^{I}_{X_{1}}E)^{*}\ldots(R^{I}_{X_{n-1}}E_{n-1})(R^{I}_{X_{n-1}}E)^{*}E_{n}E^{*}$

and $X_{i-1}\supset X_{i}$ for all $i$ (using, in addition to the equations
mentioned in the lemmata above, unitality of $1$ and the equation $F^{*}\cdot
F^{*}\doteq F^{*}$).

######  Proof 4.33.

From Lemmata 4.29, 4.30 noting that at most $|\Sigma|-1$ of the inclusions
$X_{i-1}\supseteq X_{i}$ can be proper.

######  Definition 4.34.

We define functions
$(\\_)^{\to+},(\\_)^{\to*}:\mathsf{RE}\to\mathcal{P}\mathsf{RE}$ by

$\small\begin{array}[]{rcl}a^{\to+}&=_{\mathrm{df}}&\\{1\\}\\\
0^{\to+}&=_{\mathrm{df}}&\emptyset\\\
(E+F)^{\to+}&=_{\mathrm{df}}&E^{\to+}\cup F^{\to+}\\\
1^{\to+}&=_{\mathrm{df}}&\emptyset\\\
(EF)^{\to+}&=_{\mathrm{df}}&E^{\to+}\cdot\\{F\\}\cup\bigcup\\{R^{I}_{X}(E^{\to*})\cdot
F^{\to+}\mid\emptyset\subset X\subseteq\Sigma\\}\\\
(E^{*})^{\to+}&=_{\mathrm{df}}&\\{(R^{I}_{X_{0}}E)^{*}(R^{I}_{X_{1}}E_{1})\ldots(R^{I}_{X_{n-1}}E_{n-1})(R^{I}_{X_{n-1}}E)^{*}E_{n}E^{*}\mid\\\
&&\hskip 14.22636ptn>0,\emptyset\subset X_{i}\subseteq\Sigma,X_{i-1}\supseteq
X_{i},E_{i}\in E^{\to+}\\}\\\\[7.74997pt] E^{\to*}&=_{\mathrm{df}}&\\{E\\}\cup
E^{\to+}\end{array}$

######  Proposition 4.35.

For any $E$, $E^{\prime}$ and $u\in\Sigma^{*}$, if $E\to^{I*}(u,E^{\prime})$,
then there exists $E^{\prime\prime}$ such that $E^{\prime}\doteq
E^{\prime\prime}$ and $E^{\prime\prime}\in E^{\to*}$ (using only the equations
mentioned in the above lemmata).

######  Proposition 4.36.

If $E$ is star-connected, then a suitable sound quotient of the state set
$\\{E^{\prime}\mid\exists u\in\Sigma^{*}.\ E\to^{I*}(u,E^{\prime})\\}$ of the
Antimirov automaton for $E$ (accepting $\llbracket E\rrbracket^{I}$) is
finite.

######  Proof 4.37.

By Lemma 4.32, for a star-connected expression $E$, we only need to consider
$n\leq|\Sigma|$ in the definition of $(E^{*})^{\to+}$ for Proposition 4.35 to
hold. This restriction makes the set $E^{\to*}$ finite.

##  5 Uniform Scattering Rank of a Language

We proceed to defining the notion of uniform scattering rank of a language and
show that star-connected expressions define languages with uniform scattering
rank.

###  5.1 Scattering Rank vs. Uniform Scattering Rank

The notion of scattering rank of a language (a.k.a. distribution rank,
$k$-block testability) was introduced by Hashiguchi [9].

######  Definition 5.1.

A language $L$ has _( $I$-scattering) rank_ at most $N$ if
$\forall u,v.\,uv\in[L]^{I}\Longrightarrow\exists z\in
L.\,u\mathrel{{\sim}{\lhd}}_{N}z\mathrel{{\rhd}{\sim}}v$.

We say that $L$ has rank if it has rank at most $N$ for some $N\in\mathbb{N}$.
If it does, then, for the least such $N$, we say that $L$ has rank $N$.

The only languages with rank 0 are $\emptyset$ and $\mathbf{1}$. If a
nontrivial language $L$ is closed, it has rank 1: for any $uv\in[L]^{I}$, we
have also have $uv\in L$ and $u\lhd uv\rhd\varepsilon,v$.

Having rank is a sufficient condition for regularity of the trace closure of a
regular language. But it is not a necessary condition.

######  Proposition 5.2 (Hashiguchi [9]).

(cf. [19, Prop. 6.3.2]) If a regular language $L$ has rank, then $[L]^{I}$ is
regular.

######  Proposition 5.3.

There exist regular languages $L$ such that $[L]^{I}$ is regular but $L$ is
without a rank.

######  Proof 5.4.

Consider $\Sigma=_{\mathrm{df}}\\{a,b\\}$, $aIb$. The regular language
$L=_{\mathrm{df}}\llbracket(ab)^{*}(a^{*}+b^{*})\rrbracket$ is without a rank,
since, for any $n$, we have $(ab)^{n}\in L$ and $a^{n}b^{n}\in[L]^{I}$ while
the smallest $N$ such that
$a^{n}\mathrel{{\sim}{\lhd}}_{N}(ab)^{n}\mathrel{{\rhd}{\sim}}b^{n}$ is $n$.
Nonetheless, $[L]^{I}=\Sigma^{*}=\llbracket(a+b)^{*}\rrbracket$ is regular.

We wanted to show that a truncation of the refined Antimirov automaton (which
we define in Section 6) is finite for regexps whose language has rank. But it
turns out, as we shall see, that rank does not quite work for this. For this
reason, we introduce a stronger notion that we call uniform scattering rank.

######  Definition 5.5.

A language $L$ has _uniform ( $I$-scattering) rank_ at most $N$ if
$\forall w\in[L]^{I}.\ \exists z\in L.\ \forall u,v.\,w=uv\Longrightarrow
u\mathrel{{\sim}{\lhd}}_{N}z\mathrel{{\rhd}{\sim}}v$.

The difference between the two definitions is that, in the uniform case, the
choice of $z$ depends only on $w$ whereas, in the non-uniform case, it depends
on the particular split of $w$ as $w=uv$, i.e., for every such split of $w$ we
may choose a different $z$.

######  Lemma 5.6.

If $L$ has uniform rank at most $N$, then $L$ has rank at most $N$.

The converse of the above lemma does not hold—there are languages with uniform
rank greater than rank. Furthermore, there are languages that have rank but no
uniform rank.

######  Proposition 5.7.

Let $\Sigma=_{\mathrm{df}}\\{a,b,c\\}$, $aIb$ and
$E=_{\mathrm{df}}a^{*}b^{*}c(ab)^{*}(a^{*}+b^{*})+(ab)^{*}(a^{*}+b^{*})ca^{*}b^{*}$.

  1. 1.

The language $\llbracket E\rrbracket$ has rank 2.

  2. 2.

The language $\llbracket E\rrbracket$ has no uniform rank.

######  Proof 5.8.

Note that $c$ behaves like a separator—although $a$ and $b$ are independent,
neither $a$ nor $b$ commutes with $c$. It can be seen that words in
$\llbracket E\rrbracket^{I}$ are of the form $w_{l}cw_{r}$ where $w_{l}$ and
$w_{r}$ consist of some number of $a$’s and $b$’s, i.e., $\llbracket
E\rrbracket^{I}=\llbracket(a+b)^{*}c(a+b)^{*}\rrbracket$.

  1. 1.

Let $uv\in\llbracket E\rrbracket^{I}$. We have to find $u_{1},u_{2}$ and
$v_{0},v_{1},v_{2}$ so that $u_{1}u_{2}\sim^{I}u$, $v_{0}v_{1}v_{2}\sim^{I}v$,
$v_{0}Iu_{1}$, $v_{0}v_{1}Iu_{2}$ and $v_{0}u_{1}v_{1}u_{2}v_{2}\in\llbracket
E\rrbracket$. There are two cases to consider: either $c$ is in the suffix $v$
or it is in the prefix $u$.

     * •

Case $c\in v$: We have that $u$ consists of only $a$’s and $b$’s. Let
$x,y\in\Sigma^{*}$ be such that $v=xcy$. Set $u_{1}=_{\mathrm{df}}\pi_{a}(u)$,
$u_{2}=_{\mathrm{df}}\pi_{b}(u)$, $v_{0}=_{\mathrm{df}}\varepsilon$ and
$v_{1}=_{\mathrm{df}}\pi_{a}(x)$. Let $k=_{\mathrm{df}}|y|_{a}$,
$l=_{\mathrm{df}}|y|_{b}$ and $m=_{\mathrm{df}}\min(k,l)$. Set
$v_{2}=_{\mathrm{df}}\pi_{b}(x)c(ab)^{m}a^{k-m}b^{l-m}$. We have that
$u_{1}u_{2}=\pi_{a}(u)\pi_{b}(u)\sim^{I}u$. Since
$\pi_{a}(x)\pi_{b}(x)\sim^{I}x$ and $(ab)^{m}a^{k-m}b^{l-m}\sim^{I}y$, we also
have
$v_{0}v_{1}v_{2}=\varepsilon\pi_{a}(x)\pi_{b}(x)c(ab)^{m}a^{k-m}b^{l-m}\sim^{I}xcy=v$.
Also, $\varepsilon I\pi_{a}(u)$ and $\varepsilon\pi_{a}(x)I\pi_{b}(u)$.
Finally,
$v_{0}u_{1}v_{1}u_{2}v_{2}=\varepsilon\pi_{a}(u)\pi_{a}(x)\pi_{b}(u)\pi_{b}(x)c(ab)^{m}a^{k-m}b^{l-m}\in\llbracket
a^{*}b^{*}c(ab)^{*}(a^{*}+b^{*})\rrbracket$.

     * •

Case $c\in u$: Similar to the previous case. Let $x$ and $y$ be such that
$u=xcy$. Let $k=_{\mathrm{df}}|x|_{a}$, $l=_{\mathrm{df}}|x|_{b}$ and
$m=_{\mathrm{df}}\min(k,l)$. Set
$u_{1}=_{\mathrm{df}}(ab)^{m}a^{k-m}b^{l-m}c\pi_{a}(y)$,
$u_{2}=_{\mathrm{df}}\pi_{b}(y)$, $v_{0}=_{\mathrm{df}}\varepsilon$,
$v_{1}=_{\mathrm{df}}\pi_{a}(v)$ and $v_{2}=_{\mathrm{df}}\pi_{b}(v)$. In this
case we have
$v_{0}u_{1}v_{1}u_{2}v_{2}\in\llbracket(ab)^{*}(a^{*}+b^{*})ca^{*}b^{*}\rrbracket$.

  2. 2.

Assume that $\llbracket E\rrbracket$ has uniform rank at most $N$. Take
$w=_{\mathrm{df}}a^{N+1}b^{N+1}ca^{N+1}b^{N+1}\in\llbracket E\rrbracket^{I}$.
By our assumption, there is $z\in\llbracket E\rrbracket$ such that, for all
$u$ and $v$, if $w=uv$, then
$u\mathrel{{\sim}{\lhd}}_{N}z\mathrel{{\rhd}{\sim}}v$.

Take $u=_{\mathrm{df}}a^{N+1}$ and $v=_{\mathrm{df}}b^{N+1}ca^{N+1}b^{N+1}$.
Thus, for some $n\leq N$, $z=v_{0}u_{1}v_{1}\ldots u_{n}v_{n}$ and
$u=a^{N+1}\sim^{I}u_{1}\ldots u_{n}$. Since we have $N+1$ letters $a$ to
divide into $n\leq N$ words, at least one $u_{i}$ must consist of more than
one $a$ and thus $z$ must contain two consecutive $a$’s that are before $c$.

Take $u^{\prime}=_{\mathrm{df}}a^{N+1}b^{N+1}ca^{N+1}$ and
$v^{\prime}=_{\mathrm{df}}b^{N+1}$. Again, for some $n\leq N$,
$z=v^{\prime}_{0}u^{\prime}_{1}v^{\prime}_{1}\ldots
u^{\prime}_{n}v^{\prime}_{n}$ and
$v^{\prime}=b^{N+1}\sim^{I}v^{\prime}_{0}\ldots v^{\prime}_{n}$. Note that $c$
must be in one of the $u^{\prime}_{i}$’s and thus for all $j<i$ it must be
that $v^{\prime}_{j}=\varepsilon$. Hence $v^{\prime}_{0}=\varepsilon$ and we
have $N+1$ letters $b$ to divide into $n\leq N$ words and thus at least one
$v^{\prime}_{i}$ consists of more than one $b$. This means that $z$ must
contain two consecutive $b$’s that are after $c$.

The only words in $\llbracket E\rrbracket$ equivalent to $w$ are
$a^{N+1}b^{N+1}c(ab)^{N+1}$ and $(ab)^{N+1}ca^{N+1}b^{N+1}$. Neither of these
has at least two consecutive $a$’s before $c$ as well as at least two
consecutive $b$’s after $c$, so neither qualifies as $z$. Contradiction.

###  5.2 Star-Connected Languages Have Uniform Rank

Klunder et al. [12] established that star-connectedness is a sufficient
condition for a regular language to have rank, although not a necessary one.

######  Proposition 5.9 (Klunder et al. [12]).

Any star-connected language has rank.

######  Proof 5.10.

The language $\\{a\\}$ has rank $1$. The languages $\emptyset$ and
$\mathbf{1}$ have rank $0$. If two languages $L_{1}$ and $L_{2}$ have ranks at
most $N_{1}$ resp. $N_{2}$, then $L_{1}\cup L_{2}$ has rank at most
$\max(N_{1},N_{2})$ and $L_{1}\cdot L_{2}$ has rank at most $N_{1}+N_{2}$. If
a general language $L$ has rank at most $N$, then $L^{*}$ need not have rank.
For example, for $\Sigma=_{\mathrm{df}}\\{a,b\\}$, $aIb$, the language
$\\{ab\\}$ has rank 1, but $\\{ab\\}^{*}$ is without rank. But if $L$ is also
connected, then $L^{*}$ turns out to have rank at most $(N+1)\cdot|\Sigma|$.
The claim follows by induction on the given star-connected expression.

######  Proposition 5.11.

There exist regular languages with rank (and also with uniform rank) that are
not star-connected.

######  Proof 5.12.

Consider $\Sigma=_{\mathrm{df}}\\{a,b\\}$, $aIb$. The language
$L=_{\mathrm{df}}\llbracket(aa+ab+ba+bb)^{*}\rrbracket$ has rank 1, in fact
even uniform rank 1, because it is closed. The regular expression
$(aa+ab+ba+bb)^{*}$ is clearly not star-connected, since the language
$\llbracket aa+ab+ba+bb\rrbracket$ contains disconnected words $ab$ and $ba$.
But a more involved pumping argument also shows that $L$ is not star-
connected, i.e., that there is no star-connected expression $E$ such that
$L=\llbracket E\rrbracket$.

We will now show that star-connected languages also have uniform rank, by
refining Klunder et al.’s proof of Proposition 5.9, especially the case of the
Kleene star.

Let us analyze the case $L^{*}$ where $L$ is a connected language. When
$w\in[L^{*}]^{I}$, then there exists $z\in L$ such that $w\sim^{I}z$. This
further means that there exist $n\in N$ and $z_{1},\ldots,z_{n}\in L$ such
that $z=z_{1}\ldots z_{n}$ where we can require that all $z_{i}$ are nonempty.
Since $L$ is connected, each $z_{i}$ is also connected. If $w=uv$, then there
exist $u_{1},\ldots,u_{n}$ and $v_{1},\ldots,v_{n}$ such that
$u\sim^{I}u_{1}\ldots u_{n}$, $v\sim^{I}v_{1}\ldots v_{n}$ and, for every $i$,
$z_{i}\sim^{I}u_{i}v_{i}$ and, for every $j<i$, $v_{j}Iu_{i}$. In other words,
$u_{i}$ is the part of $z_{i}$ that belongs to $u$ and $v_{i}$ is the part
that belongs to $v$. In particular, if $u_{i}=\varepsilon$ (or
$z_{i}\sim^{I}v_{i}$), then all letters of $z_{i}$ belong to the suffix $v$,
and similarly if $v_{i}=\varepsilon$ (or $z_{i}\sim^{I}u_{i}$), then all
letters of $z_{i}$ belong to the prefix $u$. An important observation for us
is that not more than $|\Sigma|$ of the $z_{i}$ can be two-colored in the
sense that both $u_{i}\neq\varepsilon$ and $v_{i}\neq\varepsilon$.

######  Lemma 5.13.

Let $w,u,v,z_{1},\ldots,z_{n}$ be words such that $w=uv$,
$w\sim^{I}z_{1}\ldots z_{n}$ and each $z_{i}$ is nonempty and connected. Let
$u_{1},\ldots,u_{n},v_{1},\ldots,v_{n}$ be words such that
$u\sim^{I}u_{1}\ldots u_{n}$, $v\sim^{I}v_{1}\ldots v_{n}$, for all $i$,
$z_{i}\sim^{I}u_{i}v_{i}$, and, for all $j<i$, $v_{j}Iu_{i}$. For at most
$|\Sigma|$ of the words $z_{i}$, it can be that both $u_{i}\neq\varepsilon$
and $v_{i}\neq\varepsilon$.

######  Proof 5.14.

If, for some $i$, we have that $u_{i}\neq\varepsilon$ and
$v_{i}\neq\varepsilon$, then, since $z_{i}\sim^{I}u_{i}v_{i}$ is connected,
there must exist letters $a$ and $b$ such that $a\in u_{i}$, $b\in v_{i}$ and
$aDb$. Since $v_{i}Iu_{i+1}\ldots u_{n}$, we have $a\not\in u_{i+1}\ldots
u_{n}$. This means that, if there are $k$ words $z_{i}$ such that
$u_{i}\neq\varepsilon$ and $v_{i}\neq\varepsilon$, then these words together
must contain at least $k$ distinct letters.

Should it happen for some $i$ that $z_{i}$ and $z_{i+1}$ are completely from
the prefix $u$ (in the sense that $v_{i}=v_{i+1}=\varepsilon$, i.e.,
$z_{i}\sim^{I}u_{i}$ and $z_{i+1}\sim^{I}u_{i+1}$), then $z_{i}$ and $z_{i+1}$
belong to the same block of $u$ in the scattering
$u\mathrel{{\sim}{\lhd}}z\mathrel{{\rhd}{\sim}}v$, which can potentially help
keeping the uniform rank of $L^{*}$ low. The same holds for $z_{i}$ and
$z_{i+1}$ that are completely from the suffix $v$: they belong to the same
block of $v$. Having words $z_{i}$ that are completely from $u$ interspersed
with other types of words $z_{i}$ (for example, having all odd-numbered
$z_{i}$ completely from $u$ and all even-numbered are completely from $v$), in
contrast, is not helpful. It could thus be useful to be able to choose $z$,
$n$ and $z_{1}\ldots,z_{n}$ in such a way that as many as possible of the
$z_{i}$ that are completely from $u$ are adjacent in $z$ for all splits of $w$
of as $w=uv$.

For example, take $\Sigma=_{\mathrm{df}}\\{a,b\\}$, $aIb$ and
$L=_{\mathrm{df}}\Sigma=\llbracket a+b\rrbracket$. For
$w=_{\mathrm{df}}a^{m}b^{m}\in[L^{*}]^{I}$, we could build $z=a^{m}b^{m}\in
L^{*}$ from $n=_{\mathrm{df}}2m$, $z_{i}=_{\mathrm{df}}a$ for $1\leq i\leq m$
and $z_{i}=_{\mathrm{df}}b$ for $m+1\leq i\leq 2m$. Another option is to
construct $z=(ab)^{m}$ from $n=_{\mathrm{df}}2m$, $z_{2i-1}=_{\mathrm{df}}a$
and $z_{2i}=_{\mathrm{df}}b$ for $1\leq i\leq m$. In the first case, the
letters from $u$ stay together in $z$ for all prefixes $u$ of $w$ (as $w=z$).
In the second case, they can be interleaved with the letters from $v$ (in the
most extreme case $u=_{\mathrm{df}}a^{m}$ and $v=_{\mathrm{df}}b^{m}$, the
words $u$ and $v$ get scattered into $m$ resp. $m+1$ blocks in $z$). Note
that, when $z_{i}\sim^{I}v_{i}$ and $z_{i+1}\sim^{I}u_{i+1}$, then
$z_{i}Iz_{i+1}$. The next lemma says that, for given $z$, $n$,
$z_{1},\ldots,z_{n}$, the sequence of words $z_{1},\ldots,z_{n}$ can be
permuted into $z^{\prime}_{1},\ldots,z^{\prime}_{n}$ with $z_{1}\ldots
z_{n}\sim^{I}z^{\prime}_{1}\ldots z^{\prime}_{n}$ so that, if $z^{\prime}_{i}$
is completely from $u$, then $z^{\prime}_{i-1}$ is not completely from $v$. As
$z_{i}\in L$ for all $i$, it is of course the case that
$z^{\prime}=_{\mathrm{df}}z^{\prime}_{1}\ldots z^{\prime}_{n}\in L^{*}$, so
$z^{\prime}$ is as good a witness of $w\in[L^{*}]^{I}$ as $z$.

######  Lemma 5.15.

Let $w,u,v,z_{1},\ldots,z_{n}$ be words such that $w=uv$,
$w\sim^{I}z_{1}\ldots z_{n}$, and each $z_{i}$ is nonempty and connected.
There exists a permutation
$\sigma^{\prime}=z^{\prime}_{1},\ldots,z^{\prime}_{n}$ of
$\sigma=_{\mathrm{df}}z_{1},\ldots,z_{n}$ with the following properties:

  1. 1.

$z_{1}\ldots z_{n}\sim^{I}z^{\prime}_{1}\ldots z^{\prime}_{n}$;

  2. 2.

for any $u^{\prime},v^{\prime}$ such that $u=u^{\prime}v^{\prime}$, and for
any $u_{1},\ldots,u_{n},v_{1},\ldots v_{n}$ such that
$u^{\prime}\sim^{I}u_{1}\ldots u_{n}$, $v^{\prime}v\sim^{I}v_{1}\ldots v_{n}$,
for all $i$, $z^{\prime}_{i}\sim^{I}u_{i}v_{i}$, and, for all $j<i$,
$v_{j}Iu_{i}$, we have: if $v_{i}=\varepsilon$, then $u_{i-1}\neq\varepsilon$
unless $i=1$.

######  Proof 5.16.

By induction on $u$.

  * •

Case $\varepsilon$: The identical permutation
$\sigma^{\prime}=_{\mathrm{df}}\sigma$ has property 1 trivially. It also
enjoys property 2 since $\varepsilon=u^{\prime}v^{\prime}$ implies
$u^{\prime}=v^{\prime}=\varepsilon$, and, for all $i$, we have
$z_{i}\sim^{I}u_{i}v_{i}$, $z_{i}\neq\varepsilon$, $u_{i}=\varepsilon$ and
hence $v_{i}\neq\varepsilon$.

  * •

Case $ua$: By induction hypothesis, we have a permutation
$\sigma^{\prime}=z^{\prime}_{1},\ldots,z^{\prime}_{n}$ of $\sigma$ which has
property 1 and and also has property 2 for all prefixes $u^{\prime}$ of $w$ up
to $u$. Now consider the case where $u^{\prime}=_{\mathrm{df}}ua$ and
$v^{\prime}=_{\mathrm{df}}\varepsilon$. This particular $a$ is in one of the
$z^{\prime}_{i}$, say $z^{\prime}_{m}$. The only difference with the case
$u^{\prime}=_{\mathrm{df}}u$ and $v^{\prime}=_{\mathrm{df}}a$ is that this $a$
is now in the $u^{\prime}$ part of $z^{\prime}_{m}$ and no longer in the
$v^{\prime}v$ part. Let us also note that every nonempty $u_{i}$ has remained
nonempty.

If $v_{m}\neq\varepsilon$, then the empty $v_{i}$ are exactly the same as in
the case $u^{\prime}=_{\mathrm{df}}u$. Hence $\sigma^{\prime}$ has property 2
also for the prefix $u^{\prime}=_{\mathrm{df}}ua$.

If $v_{m}=\varepsilon$, but $m=1$ or $u_{m-1}\neq\varepsilon$, then
$\sigma^{\prime}$ has property 2 also for the prefix
$u^{\prime}=_{\mathrm{df}}ua$.

In the critical case $v_{m}=\varepsilon$, $m\neq 1$ and $u_{m-1}=\varepsilon$,
we construct a new permutation
$\sigma^{\prime\prime}=_{\mathrm{df}}z^{\prime\prime}_{1},\ldots,z^{\prime\prime}_{n}$
from $\sigma^{\prime}$ by moving the words
$z^{\prime}_{m},\ldots,z^{\prime}_{l}$ (where $l$ is the largest such that
$v_{m}\ldots v_{l}=\varepsilon$) in front of of
$z^{\prime}_{k},\ldots,z^{\prime}_{m-1}$ (where $k$ is the smallest such that
$u_{k}\ldots u_{m-1}=\varepsilon$). Moving all these words rather than just
$z_{m}$ alone ensures that the new permutation $\sigma^{\prime\prime}$ has
property 2 also for all prefixes $u^{\prime}$ up to $u^{\prime}=u$ and not
just only for the prefix $u^{\prime}=ua$. The new permutation
$\sigma^{\prime\prime}$ also has property 1: indeed, we have $z_{1}\ldots
z_{n}\sim^{I}z^{\prime}_{1}\ldots
z^{\prime}_{n}\sim^{I}z^{\prime\prime}_{1}\ldots z^{\prime\prime}_{n}$ as
$z^{\prime}_{k}\ldots z^{\prime}_{m-1}\sim^{I}v_{k}\ldots
v_{m-1}\leavevmode\nobreak\ I\leavevmode\nobreak\ u_{m}\ldots
u_{l}\sim^{I}z^{\prime}_{m}\ldots z^{\prime}_{l}$.

######  Proposition 5.17.

If $E$ is star-connected, then the language $\llbracket E\rrbracket$ has
uniform rank.

######  Proof 5.18.

By induction on $E$. We only look at the case $E^{*}$.

  * •

Case $E^{*}$: From the assumption we have that $E$ is star-connected and
$\llbracket E\rrbracket$ is connected. By induction hypothesis $\llbracket
E\rrbracket$ has uniform rank at most $N$ for some $N\in\mathbb{N}$. We show
that $\llbracket E^{*}\rrbracket$ has uniform rank at most $(|\Sigma|+1)N$.

Let $w\in\llbracket E^{*}\rrbracket^{I}$. Then there exist unique $n$ and
$w_{1},\ldots,w_{n}$ such that $w\in w_{1}\cdot^{I}\ldots\cdot^{I}w_{n}$,
$w_{i}\in\llbracket E\rrbracket^{I}$, and we can also require that
$w_{i}\neq\varepsilon$. By $\llbracket E\rrbracket$ having uniform rank at
most $N$, for every $i$, there exists a nonempty word $z_{i}\in\llbracket
E\rrbracket$ such that, for any split of $w_{i}$ as $u_{i}v_{i}$, we have
$u_{i}\mathrel{{\sim}{\lhd}}_{N}z_{i}\mathrel{{\rhd}{\sim}}v_{i}$. By
connectedness of $\llbracket E\rrbracket$, all $z_{i}$ are connected.

We take $z^{\circ}=_{\mathrm{df}}z^{\circ}_{1}\ldots z^{\circ}_{n}$ where
$\sigma^{\circ}=_{\mathrm{df}}z^{\circ}_{1},\ldots,z^{\circ}_{n}$ is the
permutation of $\sigma=z_{1},\ldots,z_{n}$ obtained by Lemma 5.15 for
$u=_{\mathrm{df}}w$ and $v=_{\mathrm{df}}\varepsilon$, i.e., for the specific
split of $w$ as $w\varepsilon$. By Lemma 5.15(1), we have
$w\sim^{I}w_{1}\ldots w_{n}\sim^{I}z_{1}\ldots
z_{n}\sim^{I}z^{\circ}_{1}\ldots z^{\circ}_{n}=z^{\circ}$. We let
$w^{\circ}_{1},\ldots,w^{\circ}_{n}$ be the corresponding permutation of
$w_{1},\ldots,w_{n}$, so we also have $w\sim^{I}w^{\circ}_{0}\ldots
w^{\circ}_{n}$ and $w^{\circ}_{i}\sim^{I}z^{\circ}_{i}$ for all $i$.

We will now show that, for any split of $w$ as $w=uv$, we have
$u\mathrel{{\sim}{\lhd}}_{(|\Sigma|+1)N}z^{\circ}\mathrel{{\rhd}{\sim}}v$.

Let $w=uv$ be any split of $w$. There exist unique
$u_{1},\ldots,u_{n},v_{1},\ldots v_{n}$ such $u\sim^{I}u_{1}\ldots u_{n}$,
$v\sim^{I}v_{1}\ldots v_{n}$, for all $i$, $w^{\circ}_{i}=u_{i}v_{i}$, and for
all $j<i$, $v_{j}Iu_{i}$. They give us $u_{1}\ldots u_{n}\lhd z^{\circ}\rhd
v_{1}\ldots v_{n}$ and thus
$u\mathrel{{\sim}{\lhd}}z^{\circ}\mathrel{{\rhd}{\sim}}v$. By Lemma 5.15(2)
for $u^{\prime}=_{\mathrm{df}}u$, $v^{\prime}=_{\mathrm{df}}\varepsilon$, we
have that $v_{i}=\varepsilon$ implies $u_{i-1}\neq\varepsilon$ unless $i=1$.
By Lemma 5.13, there can be at most $|\Sigma|$ words $z^{\circ}_{i}$ such that
both $u_{i}\neq\varepsilon$ and $v_{i}\neq\varepsilon$.

Each of these two-colored $z^{\circ}_{i}$ contributes at most $N$ to the
degree of $u\mathrel{{\sim}{\lhd}}z^{\circ}\mathrel{{\rhd}{\sim}}v$, so
altogether they contribute at most $|\Sigma|N$.

Between any two-colored $z^{\circ}_{i}$ and also before the first and after
the last one of them, there are some $z^{\circ}_{i}$ completely from $u$
followed by some $z^{\circ}_{i}$ completely from $v$. Each such sequence
contributes at most 1 to the degree of
$u\mathrel{{\sim}{\lhd}}z^{\circ}\mathrel{{\rhd}{\sim}}v$. If there are less
than $|\Sigma|$ two-colored words, these sequences thus contribute altogether
at most $|\Sigma|$ to the degree. If there are exactly $|\Sigma|$ two-colored
words $z^{\circ}_{i}$, then the $z^{\circ}_{i}$ after the last of them are all
completely from $v$, so their sequence belongs to the last $v$-block generated
by the last two-colored $z^{\circ}_{i}$ and thus contributes 0. Again
altogether these sequences contribute at most $|\Sigma|$.

Altogether the degree of $u\lhd z^{\circ}\rhd v$ is thus at most
$(|\Sigma|+1)N$.

##  6 Antimirov Reordering Derivative and Uniform Rank

We have seen that the reordering language derivative $D^{I}_{u}L$ allows $u$
to be scattered in a word $z\in L$ as $u_{1},\ldots,u_{n}\lhd z\rhd
v_{0},\ldots,v_{n}$ where $u\sim^{I}u_{1}\ldots u_{n}$. We will now consider a
version of the Antimirov reordering derivative operation that delivers lists
of regexps for the possible $v_{0},\ldots,v_{n}$ rather than just single
regexps for their concatenations $v_{0}\ldots v_{n}$.

###  6.1 Refined Antimirov Reordering Derivative

The refined reordering parts-of-derivative of a regexp $E$ along a letter $a$
are pairs of regexps $E_{l},E_{r}$. For any word $w=av\in\llbracket
E\rrbracket^{I}$, there must be an equivalent word $z=v_{l}av_{r}\in\llbracket
E\rrbracket$. Instead of describing the words $v_{l}v_{r}$ obtainable by
removing a minimal occurrence of $a$ in a word $z\in\llbracket E\rrbracket$,
the refined parts-of-derivative describe the subwords $v_{l},v_{r}$ that were
to the left and right of this $a$ in $z$: it must be the case that
$v_{l}\in\llbracket E_{l}\rrbracket$ and $v_{r}\in\llbracket E_{r}\rrbracket$
for one of the pairs $E_{l},E_{r}$. For a longer word $u$, the refined
reordering derivative operation gives lists of regexps $E_{0},\ldots,E_{n}$
fixing what the lists of subwords $v_{0},\ldots,v_{n}$ can be in words
$z=v_{0}u_{1}v_{1}\ldots u_{n}v_{n}\in\llbracket E\rrbracket$ equivalent to a
given word $w=uv\in\llbracket E\rrbracket^{I}$.

######  Definition 6.1.

The _(unbounded and bounded) refined Antimirov $I$-reordering_ parts-of-
derivatives of a regexp along a letter and a word are given by relations
${\to^{I}}\subseteq\mathsf{RE}\times\Sigma\times\mathsf{RE}\times\mathsf{RE}$,
${\Rightarrow^{I}}\subseteq\mathsf{RE}^{+}\times\Sigma\times\mathsf{RE}^{+}$,
${\to^{I*}}\subseteq\mathsf{RE}\times\Sigma^{*}\times\mathsf{RE}^{+}$,
${\Rightarrow^{I}_{N}}\subseteq\mathsf{RE}^{+\leq
N+1}\times\Sigma\times\mathsf{RE}^{+\leq N+1}$, and
${\to^{I*}_{N}}\subseteq\mathsf{RE}\times\Sigma^{*}\times\mathsf{RE}^{+\leq
N+1}$ defined inductively by

$\small\begin{array}[]{l}a\to^{I}(a;1,1)\quad
E+F\to^{I}(a;E_{l},E_{r})E\to^{I}(a;E_{l},E_{r})\quad
E+F\to^{I}(a;F_{l},F_{r})F\to^{I}(a;F_{l},F_{r})\\\\[7.74997pt]
EF\to^{I}(a;E_{l},E_{r}F)E\to^{I}(a;E_{l},E_{r})\quad
EF\to^{I}(a;(R^{I}_{a}E)F_{l},F_{r})F\to^{I}(a;F_{l},F_{r})\quad
E^{*}\to^{I}(a;(R^{I}_{a}E)^{*}E_{l},E_{r}E^{*})E\to^{I}(a;E_{l},E_{r})\end{array}$
$\small\begin{array}[]{l}\Gamma,E,\Delta\Rightarrow^{I}_{N}(a;R^{I}_{a}\Gamma,E_{l},E_{r},\Delta)\lx@proof@logical@and
E\to^{I}(a;E_{l},E_{r})|\Gamma,\Delta|<N\quad\Gamma,E,\Delta\Rightarrow^{I}_{N}(a;R^{I}_{a}\Gamma,E_{r},\Delta)\lx@proof@logical@and
E\to^{I}(a;E_{l},E_{r})E_{l}{\downarrow}|\Gamma|>0\\\\[7.74997pt]
\Gamma,E,\Delta\Rightarrow^{I}_{N}(a;R^{I}_{a}\Gamma,E_{l},\Delta)\lx@proof@logical@and
E\to^{I}(a;E_{l},E_{r})E_{r}{\downarrow}|\Delta|>0\quad\Gamma,E,\Delta\Rightarrow^{I}_{N}(a;R^{I}_{a}\Gamma,\Delta)\lx@proof@logical@and
E\to^{I}(a;E_{l},E_{r})E_{l}{\downarrow}E_{r}{\downarrow}|\Gamma|>0|\Delta|>0\end{array}$
$\small\begin{array}[]{l}E\to^{I*}_{N}(\varepsilon;E)\quad
E\to^{I*}_{N}(ua;\Gamma^{\prime})\lx@proof@logical@and
E\to^{I*}_{N}(u;\Gamma)\Gamma\Rightarrow^{I}_{N}(a;\Gamma^{\prime})\par\end{array}$

By $\mathsf{RE}^{+\leq N+1}$ we mean nonempty lists of regexps of length at
most $N+1$. The relations $\Rightarrow^{I}$ and $\to^{I*}$ are defined exactly
as $\Rightarrow_{N}^{I}$ and $\to_{N}^{I*}$ but with the condition
$|\Gamma,\Delta|<N$ of the first rule of $\Rightarrow_{N}^{I}$ dropped. The
operation $R^{I}_{a}$ is extended to lists of regexps in the obvious way.

We have several rules for deriving a list of regexps along $a$. If $E$ is
split into $E_{l},E_{r}$ and neither of them is nullable, then, in the
$N$-bounded case, we require that the given list is shorter than $N+1$ since
the new list will be longer by 1. If one of $E_{l},E_{r}$ is nullable, not the
first resp. last in the list and we choose to drop it, then the new list will
be of the same length. If both are nullable, not the first resp. last and we
opt to drop both, then the new list will be shorter by 1. They must be
droppable under these conditions to handle the situation when a word $z$ has
been split as $v_{0}u_{1}v_{1}\ldots u_{k}v_{k}u_{k+1}\ldots u_{n}v_{n}$ and
$v_{k}$ is further being split as $v_{l}av_{r}$ while $v_{l}$ or $v_{r}$ is
empty. If $k\neq 0$ and $v_{l}$ is empty, we must join $u_{k}$ and $a$ into
$u_{k}a$. If $k\neq n$ and $v_{r}$ is empty, we must join $a$ and $u_{k+1}$
into $au_{k+1}$. If $k$ is neither $0$ nor $n$ and both $v_{l}$ and $v_{r}$
are empty, we must join all three of $u_{k}$, $a$ and $u_{k+1}$ into
$u_{k}au_{k+1}$. The length of the new list of regexps is always at least 2.

######  Proposition 6.2.

For any $E$,

  1. 1.

for any $a\in\Sigma,v_{l},v_{r}\in\Sigma^{*}$,

$v_{l}Ia\wedge v_{l}av_{r}\in\llbracket E\rrbracket\iff\exists
E_{l},E_{r}.\,E\to^{I}(a;E_{l},E_{r})\wedge v_{l}\in\llbracket
E_{l}\rrbracket\wedge v_{r}\in\llbracket E_{r}\rrbracket;$

  2. 2.

for any
$u\in\Sigma^{*},n\in\mathbb{N},v_{0}\in\Sigma^{*},v_{1},\ldots,v_{n-1}\in\Sigma^{+},v_{n}\in\Sigma^{*}$,

$\begin{array}[]{l}\exists z\in\llbracket
E\rrbracket,u_{1},\ldots,u_{n}\in\Sigma^{+}.\,u\sim^{I}u_{1}\ldots u_{n}\wedge
u_{1},\ldots,u_{n}\lhd z\rhd v_{0},\ldots,v_{n}\\\ \iff\\\ \exists
E_{0},\ldots,E_{n}.\,E\to^{I*}(u;E_{0},\ldots,E_{n})\wedge\forall j.\
v_{j}\in\llbracket E_{j}\rrbracket.\end{array}$

######  Proof 6.3.

  1. 1.

$\Longrightarrow$: By induction on $E$.

     * •

Case $a^{\prime}$ where $a^{\prime}\neq a$: $v_{l}av_{r}\in\llbracket
a^{\prime}\rrbracket=\\{a^{\prime}\\}$ is impossible.

     * •

Case $a$: Suppose $v_{l}av_{r}\in\llbracket a\rrbracket=\\{a\\}$. Then
$v_{l}=v_{r}=\varepsilon$. We have $a\to^{I}(a;1,1)$ and
$\varepsilon\in\llbracket 1\rrbracket$ as required.

     * •

Case $0$: $v_{l}av_{r}\in\llbracket 0\rrbracket=\emptyset$ is impossible.

     * •

Case $E_{1}+E_{2}$: Suppose $v_{l}av_{r}\in\llbracket
E_{1}+E_{2}\rrbracket=\llbracket E_{1}\rrbracket\cup\llbracket
E_{2}\rrbracket$ and $v_{l}Ia$. Then $v_{l}av_{r}\in\llbracket
E_{i}\rrbracket$ for one of two possible $i$. By IH for $E_{i},a,v_{l},v_{r}$,
there are $E_{l}$, $E_{r}$ such that $E_{i}\to^{I}(a;E_{l},E_{r})$,
$v_{l}\in\llbracket E_{l}\rrbracket$, $v_{r}\in\llbracket E_{r}\rrbracket$ and
we also obtain $E_{1}+E_{2}\to^{I}(a;E_{l},E_{r})$.

     * •

Case $1$: $v_{l}av_{r}\in\llbracket 1\rrbracket=\mathbf{1}$ is impossible.

     * •

Case $EF$: Suppose $v_{l}av_{r}\in\llbracket EF\rrbracket=\llbracket
E\rrbracket\cdot\llbracket F\rrbracket$ and $v_{l}Ia$. Then $v_{l}av_{r}=xy$
for some $x\in\llbracket E\rrbracket$ and $y\in\llbracket F\rrbracket$. Either
(i) there exists $v^{\prime}$ such that $x=v_{l}av^{\prime}$ and
$v_{r}=v^{\prime}y$ or (ii) there exists $v^{\prime}$ such that
$y=v^{\prime}av_{r}$ and $v_{l}=xv^{\prime}$.

If (i), then, by IH for $E,a,v_{l},v^{\prime}$, there are $E_{l},E_{r}$ such
that $E\to^{I}(a;E_{l},E_{r})$, $v_{l}\in\llbracket E_{l}\rrbracket$,
$v^{\prime}\in\llbracket E_{r}\rrbracket$. We then also have
$EF\to^{I}(a;E_{l},E_{r}F)$ and $v_{r}=v^{\prime}y\in\llbracket
E_{r}F\rrbracket$.

If (ii), then $xIa$ and $v^{\prime}Ia$, so $x\in\llbracket
R^{I}_{a}E\rrbracket$ and, by IH for $F,a,v^{\prime},v_{r}$, there are
$F_{l},F_{r}$ such that $F\to^{I}(a;F_{l},F_{r})$, $v^{\prime}\in\llbracket
F_{l}\rrbracket$, $v_{r}\in\llbracket F_{r}\rrbracket$. We then also have
$EF\to^{I}(a;(R^{I}_{a}E)F_{l},F_{r})$ and
$v_{l}=xv^{\prime}\in\llbracket(R^{I}_{a}E)F_{l}\rrbracket$.

     * •

Case $E^{*}$: Suppose $v_{l}av_{r}\in\llbracket E^{*}\rrbracket$ and
$v_{l}Ia$. Then $v_{l}=xv^{\prime}_{l}$, $v_{r}=v^{\prime}_{r}y$ for some
$x,y\in\llbracket E^{*}\rrbracket$ and $v^{\prime}_{l},v^{\prime}_{r}$ such
that $v^{\prime}_{l}av^{\prime}_{r}\in\llbracket E\rrbracket$. We have $xIa$,
$v^{\prime}_{l}Ia$. Hence $x\in\llbracket R^{I}_{a}E^{*}\rrbracket$ and, by IH
for $E,a,v^{\prime}_{l},v^{\prime}_{r}$, we get that there are $E_{l}$,
$E_{r}$ such that $E\to^{I}(a;E_{l},E_{r})$ and $v^{\prime}_{l}\in\llbracket
E_{l}\rrbracket$, $v^{\prime}_{r}\in\llbracket E_{r}\rrbracket$. We also
obtain $v_{l}=xv^{\prime}_{l}\in\llbracket(R^{I}_{a}E^{*})E_{l}\rrbracket$ and
$v_{r}=v^{\prime}_{r}y\in\llbracket E_{r}E^{*}\rrbracket$.

$\Longleftarrow$: By induction on the derivation of $E\to^{I}(a;E_{l},E_{r})$.

     * •

Case $a\to^{I}(a;1,1)$ as an axiom: Suppose $v_{l},v_{r}\in\llbracket
1\rrbracket=\mathbf{1}$. Then $v_{l}=v_{r}=\varepsilon$ and we have
$\varepsilon a\varepsilon=a\in\llbracket a\rrbracket$ as required.

     * •

Case $E_{1}+E_{2}\to^{I}(a;E_{l},E_{r})$ inferred from
$E_{i}\to^{I}(a;E_{l},E_{r})$ where $i$ is 1 or 2: Suppose $v_{l}\in\llbracket
E_{l}\rrbracket$, $v_{r}\in\llbracket E_{r}\rrbracket$. We can then apply IH
to the subderivation, $v_{l},v_{r}$ and obtain that $v_{l}Ia$ and
$v_{l}av_{r}\in\llbracket E_{i}\rrbracket$, which gives us also that
$v_{l}av_{r}\in\llbracket E_{1}\rrbracket\cup\llbracket
E_{2}\rrbracket=\llbracket E_{1}+E_{2}\rrbracket$.

     * •

Case $EF\to^{I}(a;E_{l},E_{r}F)$ inferred from $E\to^{I}(a;E_{l},E_{r})$:
Suppose $v_{l}\in\llbracket E_{l}\rrbracket$, $v_{r}\in\llbracket
E_{r}F\rrbracket=\llbracket E_{r}\rrbracket\cdot\llbracket F\rrbracket$. Then
$v_{r}=xy$ for some $x\in\llbracket E_{r}\rrbracket$ and $y\in\llbracket
F\rrbracket$. We can then apply IH to the subderivation, $v_{l},x$ and obtain
that $v_{l}Ia$ and $v_{l}ax\in\llbracket E\rrbracket$. As $v_{r}=xy$, we
obtain $v_{l}av_{r}=(v_{l}ax)y\in\llbracket E\rrbracket\cdot\llbracket
F\rrbracket=\llbracket EF\rrbracket$.

     * •

Case $EF\to^{I}(a,(R_{a}E)F_{l},F_{r})$ inferred from
$F\to^{I}(a;F_{l},F_{r})$: Suppose
$v_{l}\in\linebreak\llbracket(R_{a}E)F_{l}\rrbracket=R_{a}\llbracket
E\rrbracket\cdot\llbracket F_{l}\rrbracket$, $v_{r}\in\llbracket
F_{r}\rrbracket$. Then $v_{l}=xy$ for some $x\in R_{a}\llbracket E\rrbracket$
and $y\in\llbracket F_{l}\rrbracket$, which also gives us $xIa$ and
$x\in\llbracket E\rrbracket$. We can then apply IH to the subderivation,
$y,v_{r}$ and obtain that $yIa$ and $yav_{r}\in\llbracket F\rrbracket$. As
$v_{l}=xy$, we get $v_{l}Ia$ and $v_{l}av_{r}=x(yav_{r})\in\llbracket
E\rrbracket\cdot\llbracket F\rrbracket=\llbracket EF\rrbracket$.

     * •

Case $E^{*}\to^{I}(a;(R_{a}E^{*})E_{l},E_{r}E^{*})$ inferred from
$E\to^{I}(a;E_{l},E_{r})$: Suppose
$v_{l}\in\llbracket(R_{a}E^{*})E_{l}\rrbracket=R_{a}\llbracket
E^{*}\rrbracket\cdot\llbracket E_{l}\rrbracket$, $v_{r}\in\llbracket
E_{r}E^{*}\rrbracket=\llbracket E_{r}\rrbracket\cdot\llbracket
E^{*}\rrbracket$. Then $v_{l}=xy$ for some $x\in R_{a}\llbracket
E^{*}\rrbracket$ and $y\in\llbracket E_{l}\rrbracket$, which also gives us
$xIa$ and $x\in\llbracket E^{*}\rrbracket$, and $v_{r}=zw$ for some
$z\in\llbracket E_{r}\rrbracket$ and $w\in\llbracket E^{*}\rrbracket$. We can
then apply IH to the subderivation, $y,z$ and obtain that $yIa$ and
$yaz\in\llbracket E\rrbracket$. As $v_{l}=xy$ and $v_{r}=zw$, we get that
$v_{l}Ia$ and $v_{l}av_{r}=x(yaz)w\in\llbracket E^{*}\rrbracket\cdot\llbracket
E\rrbracket\cdot\llbracket E^{*}\rrbracket\subseteq\llbracket
E^{*}\rrbracket$.

  2. 2.

$\Longrightarrow$: For any $E$ by induction on $u$.

     * •

Case $\varepsilon$: Suppose $\varepsilon\sim^{I}u_{1}\ldots u_{n}$ and
$z=v_{0}u_{1}v_{1}\ldots u_{n}v_{n}\in\llbracket E\rrbracket$. Then
necessarily $n=0$, which means that we actually have $v_{0}\in\llbracket
E\rrbracket$. We also have $E\to^{I^{*}}(\varepsilon;E)$ as required.

     * •

Case $ua$: Suppose $ua\sim^{I}u_{1}\ldots u_{n}$ and $\forall i.\forall
j<i.\,v_{j}Iu_{i}$ and $z=v_{0}u_{1}v_{1}\ldots u_{n}v_{n}\in\llbracket
E\rrbracket$. It must be that $n>0$ and there must exist $k$ and
$u_{l},u_{r}\in\Sigma^{*}$ such that $u_{k}=u_{l}au_{r}$, $v_{j}Ia$ for all
$j<k$, $aIu_{r}$, $aIu_{i}$ for all $i>k$ and $u\sim^{I}u_{1}\ldots
u_{k-1}u_{l}u_{r}u_{k+1}\ldots u_{n}$.

       * –

If $u_{l}=u_{r}=\varepsilon$, then, as $v_{k-1}av_{k}Iu_{i}$ for all $i>k$, we
are entitled to apply IH to $u$, $n-1$,
$v_{0},v_{1},\ldots,v_{k-2},v_{k-1}av_{k},v_{k+1},\ldots,v_{n}$, $z$,
$u_{1},\ldots,u_{k-1},u_{k+1},\ldots,u_{n}$. We get $E_{0},\ldots,E_{k-2}$,
$E^{\prime}$, $E_{k+1}$, …$E_{n}$ such that
$E\to^{I*}(u;E_{0},\ldots,E_{k-2},E^{\prime},E_{k+1},\ldots,E_{n})$ and
$v_{j}\in\llbracket E_{j}\rrbracket$ for all $j<k-1$,
$v_{k-1}av_{k}\in\llbracket E^{\prime}\rrbracket$, $v_{j}\in\llbracket
E_{j}\rrbracket$ for all $j>k$. As $v_{k-1}Ia$, we can apply 1\. to
$E^{\prime}$, $a$, $v_{k-1}$, $v_{k}$ and get $E_{k-1},E_{k}$ such that
$E^{\prime}\to^{I}(a;E_{k-1},E_{k})$, $v_{k-1}\in\llbracket E_{k-1}\rrbracket$
and $v_{k}\in\llbracket E_{k}\rrbracket$. This allows us to infer
$E\to^{I*}(ua;R^{I}_{a}E_{0},\ldots,R^{I}_{a}E_{k-2},E_{k-1},E_{k},E_{k+1},\ldots,E_{n})$.
As $v_{j}Ia$ also for all $j<k-1$, we in fact also have $v_{j}\in\llbracket
R^{I}_{a}E_{j}\rrbracket$ for all $j<k-1$.

       * –

If $u_{l}\neq\varepsilon$, $u_{r}=\varepsilon$, we note that $av_{k}Iu_{i}$
for all $i>k$ and apply IH to $u$, $n$, $v_{0}$, $v_{1},\ldots,v_{k-1}$,
$av_{k},v_{k+1},\ldots,v_{n}$, $z$,
$u_{1},\ldots,u_{k-1},u_{l},u_{k+1},\ldots,u_{n}$. We get
$E_{0},\ldots,E_{k-1}$, $E^{\prime}$, $E_{k+1},\ldots E_{n}$ such that
$E\to^{I*}(u;E_{0},\ldots,E_{k-1},E^{\prime},E_{k+1},\ldots,E_{n})$ and
$v_{j}\in\llbracket E_{j}\rrbracket$ for all $j<k$, $av_{k}\in\llbracket
E^{\prime}\rrbracket$, $v_{j}\in\llbracket E_{j}\rrbracket$ for all $j>k$. As
$\varepsilon Ia$, we can apply 1\. to $E^{\prime}$, $a$, $\varepsilon$,
$v_{k}$ and get $E^{\prime\prime},E_{k}$ such that
$E^{\prime}\to^{I}(a;E^{\prime\prime},E_{k})$, $\varepsilon\in\llbracket
E^{\prime\prime}\rrbracket$, $v_{k}\in\llbracket E_{k}\rrbracket$. As
$\varepsilon\in\llbracket E^{\prime\prime}\rrbracket$ tells us that
$E^{\prime\prime}{\downarrow}$, we can infer
$E\to^{I*}(ua;R^{I}_{a}E_{0},\ldots,R^{I}_{a}E_{k-1},E_{k},E_{k+1},\ldots,E_{n})$.
As $v_{j}Ia$ also for all $j<k$, we in fact also have $v_{j}\in\llbracket
R^{I}_{a}E_{j}\rrbracket$ for all $j<k$.

       * –

The cases $u_{l}=\varepsilon$, $u_{r}\neq\varepsilon$ and
$u_{l}\neq\varepsilon$, $u_{r}\neq\varepsilon$ are handled similarly to the
previous case.

$\Longleftarrow$: By induction on the derivation of
$E\to^{I*}(u;E_{0},\ldots,E_{n})$.

     * •

Case $E\to^{I*}(\varepsilon;E)$ as an axiom: Suppose that $v_{0}\in\llbracket
E\rrbracket$. We have $\varepsilon\sim\varepsilon$ as well as
$z=v_{0}\in\llbracket E\rrbracket$ directly.

     * •

Case
$E\to^{I*}(ua;R^{I}_{a}E_{0},\ldots,R^{I}_{a}E_{k-1},E_{l},E_{r},E_{k+1},\ldots,E_{n})$
inferred from subderivations $E\to^{I*}(u;E_{0},\ldots,E_{n})$ and
$E_{k}\to^{I}(a;E_{l},E_{r})$: Suppose that $v_{0}\in\llbracket
R^{I}_{a}E_{0}\rrbracket$, …, $v_{k-1}\in\llbracket
R^{I}_{a}E_{k-1}\rrbracket$, $v_{l}\in\llbracket E_{l}\rrbracket$,
$v_{r}\in\llbracket E_{r}\rrbracket$, $v_{k+1}\in\llbracket
E_{k+1}\rrbracket$, …, $v_{n}\in\llbracket E_{n}\rrbracket$, which gives us
$v_{0}Ia$, …, $v_{k-1}Ia$, $v_{0}\in\llbracket E_{0}\rrbracket$, …,
$v_{k-1}\in\llbracket E_{k-1}\rrbracket$. Applying (1.$\Longleftarrow$) to
$E_{k}$, $a$, $v_{l}$, $v_{r}$, we learn that $v_{l}Ia$ and
$v_{l}av_{r}\in\llbracket E_{k}\rrbracket$. Applying IH to the subderivation,
$v_{0},\ldots,v_{k-1}$, $v_{l}av_{r}$, $v_{k+1},\ldots,v_{n}$, we obtain
$z,u_{1},\ldots,u_{n}\in\Sigma^{+}$ such that $u\sim^{I}u_{1}\ldots u_{n}$,
$\forall i.\,\forall j<i.\ v_{j}Iu_{i}$, $\forall i>k.\,v_{l}av_{r}Iu_{i}$ and
$z=v_{0}u_{1}v_{1}\ldots v_{k-1}u_{k}(v_{l}av_{r})u_{k+1}v_{k+1}\ldots
u_{n}v_{n}\in\llbracket E\rrbracket$. Clearly $ua\sim^{I}u_{1}\ldots
u_{k}au_{k+1}\ldots u_{n}$ and $z=v_{0}u_{1}v_{1}\ldots
v_{k-1}u_{k}v_{l}av_{r}u_{k+1}v_{k+1}\ldots u_{n}v_{n}\in\llbracket
E\rrbracket$.

     * •

Case
$E\to^{I*}(ua;R^{I}_{a}E_{0},\ldots,R^{I}_{a}E_{k-1},E_{r},E_{k+1},\ldots,E_{n})$
inferred from subderivations $E\to^{I*}(u;E_{0},\ldots,E_{n})$ and
$E_{k}\to^{I}(a;E_{l},E_{r})$ and $E_{l}{\downarrow}$ whereby $k\neq 0$:
Suppose that $v_{0}\in\llbracket R^{I}_{a}E_{0}\rrbracket$, …,
$v_{k-1}\in\llbracket R^{I}_{a}E_{k-1}\rrbracket$, $v_{r}\in\llbracket
E_{r}\rrbracket$, $v_{k+1}\in\llbracket E_{k+1}\rrbracket$, …,
$v_{n}\in\llbracket E_{n}\rrbracket$, which gives us $v_{0}Ia$, …,
$v_{k-1}Ia$, $v_{0}\in\llbracket E_{0}\rrbracket$, …, $v_{k-1}\in\llbracket
E_{k-1}\rrbracket$. Applying (1.$\Longleftarrow$) to $E$, $a$, $\varepsilon$,
$v_{r}$, we learn that $av_{r}\in\llbracket E_{k}\rrbracket$. Applying IH to
the subderivation, $v_{0},\ldots,v_{k-1}$, $av_{r}$, $v_{k+1},\ldots,v_{n}$,
we obtain $z,u_{1},\ldots,u_{n}\in\Sigma^{+}$ such that $u\sim^{I}u_{1}\ldots
u_{n}$, $\forall i.\,\forall j<i.\ v_{j}Iu_{i}$, $\forall i>k.\,av_{r}Iu_{i}$
and $z=v_{0}u_{1}v_{1}\ldots v_{k-1}u_{k}(av_{r})u_{k+1}v_{k+1}\ldots
u_{n}v_{n}\in\llbracket E\rrbracket$. Now clearly
$ua\sim^{I}u_{1}\ldots(u_{k}a)u_{k+1}\ldots u_{n}$ and
$z=v_{0}u_{1}v_{1}\ldots v_{k-1}(u_{k}a)v_{r}u_{k+1}v_{k+1}\ldots
u_{n}v_{n}\in\llbracket E\rrbracket$.

     * •

The two remaining cases are treated similarly to the previous case.

######  Proposition 6.4.

For any $E$,

  1. 1.

for any $a\in\Sigma,v\in\Sigma^{*}$, the following are equivalent:

    1. (a)

$av\in\llbracket E\rrbracket^{I}$;

    2. (b)

$\exists v_{l},v_{r}\in\Sigma^{*}.\,v\sim^{I}v_{l}v_{r}\wedge v_{l}Ia\wedge
v_{l}av_{r}\in\llbracket E\rrbracket$;

    3. (c)

$\exists v_{l},v_{r}\in\Sigma^{*}.\,\\\ \hskip
14.22636ptv\sim^{I}v_{l}v_{r}\wedge\exists
E_{l},E_{r}.\,E\to^{I}(a;E_{l},E_{r})\wedge v_{l}\in\llbracket
E_{l}\rrbracket\wedge v_{r}\in\llbracket E_{r}\rrbracket$;

    4. (d)

$\exists v_{l},v_{r}\in\Sigma^{*}.\,\\\ \hskip 14.22636ptv\in
v_{l}\cdot^{I}v_{r}\wedge\exists E_{l},E_{r}.\,E\to^{I}(a;E_{l},E_{r})\wedge
v_{l}\in\llbracket E_{l}\rrbracket^{I}\wedge v_{r}\in\llbracket
E_{r}\rrbracket^{I}$.

  2. 2.

for any $u,v\in\Sigma^{*}$, the following are equivalent:

    1. (a)

$uv\in\llbracket E\rrbracket^{I}$;

    2. (b)

$\exists z\in\llbracket E\rrbracket.\
u\mathrel{{\sim}{\lhd}}z\mathrel{{\rhd}{\sim}}v$;

    3. (c)

$\exists
n\in\mathbb{N},v_{0}\in\Sigma^{*},v_{1},\ldots,v_{n-1}\in\Sigma^{+},v_{n}\in\Sigma^{*}.\,v\sim^{I}v_{0}v_{1}\ldots
v_{n}\wedge\\\ \hskip 14.22636pt\exists
E_{0},\ldots,E_{n}.\,E\to^{I*}(u;E_{0},\ldots,E_{n})\wedge\forall
j.\,v_{j}\in\llbracket E_{j}\rrbracket$;

    4. (d)

$\exists
n\in\mathbb{N},v_{0}\in\Sigma^{*},v_{1},\ldots,v_{n-1}\in\Sigma^{+},v_{n}\in\Sigma^{*}.\,v\in
v_{0}\cdot^{I}v_{1}\cdot^{I}\ldots\cdot^{I}v_{n}\wedge\\\ \hskip
14.22636pt\exists
E_{0},\ldots,E_{n}.\,E\to^{I*}(u;E_{0},\ldots,E_{n})\wedge\forall
j.\,v_{j}\in\llbracket E_{j}\rrbracket^{I}$.

  3. 3.

for any $u\in\Sigma^{*}$,
$u\in\llbracket E\rrbracket^{I}\iff(u=\varepsilon\wedge
E{\downarrow})\vee(u\neq\varepsilon\wedge\exists
E_{0},E_{1}.\,E\to^{I*}(u;E_{0},E_{1})\wedge E_{0}{\downarrow}\wedge
E_{1}{\downarrow})$.

######  Proof 6.5.

  1. 1.

(a) $\iff$ (b) follows from Proposition 3.6. (b) $\iff$ (c) follows from
Proposition 6.2(1). (c) $\iff$ (d) follows from Proposition 3.10.

  2. 2.

(a) $\iff$ (b) follows from Proposition 3.6. (b) $\iff$ (c) follows from
Proposition 6.2(2). (c) $\iff$ (d) follows from Proposition 3.10.

  3. 3.

From (2) for $E,u,\varepsilon$.

######  Proposition 6.6.

For any $E$, $N\in\mathbb{N}$, $u\in\Sigma^{*}$, $z\in\llbracket E\rrbracket$,

$\begin{array}[]{l}(\forall
u^{\prime},u^{\prime\prime}.\,u=u^{\prime}u^{\prime\prime}\Longrightarrow\exists
v.\,u^{\prime}\mathrel{{\sim}{\lhd}}_{N}z\rhd v)\\\ \Longrightarrow\\\ \exists
E_{0},\ldots,E_{n}.\,E\to^{I*}_{N}(u;E_{0},\ldots,E_{n})\wedge\forall j.\
v_{j}\in\llbracket E_{j}\rrbracket\\\ \quad\textrm{for the
unique\leavevmode\nobreak\ }n,v_{0},\ldots,v_{n}\textrm{\leavevmode\nobreak\
such that\leavevmode\nobreak\ }u\mathrel{{\sim}{\lhd}}z\rhd
v_{0},\ldots,v_{n}\end{array}$

######  Proof 6.7.

By replaying the proof of Proposition 6.2(2.$\Longrightarrow$). In the fourth
subcase ($u_{l}\neq\varepsilon$, $u_{r}\neq\varepsilon$) of the case $ua$ of
induction, IH for $u^{\prime}=u$, $u^{\prime\prime}=a$ is needed.

######  Corollary 6.8.

For any $E$ such that $\llbracket E\rrbracket$ has uniform rank at most $N$,

  1. 1.

for any $u,v\in\Sigma^{*}$, the following are equivalent:

    1. (a)

$uv\in\llbracket E\rrbracket^{I}$;

    2. (b)

$\exists z\in\llbracket E\rrbracket.\ \forall
u^{\prime},u^{\prime\prime}.\,u=u^{\prime}u^{\prime\prime}\Longrightarrow
u^{\prime}\mathrel{{\sim}{\lhd}}_{N}z\mathrel{{\rhd}{\sim}}u^{\prime\prime}v$;

    3. (c)

$\exists n\leq
N,v_{0}\in\Sigma^{*},v_{1},\ldots,v_{n-1}\in\Sigma^{+},v_{n}\in\Sigma^{*}.\,v\sim^{I}v_{0}v_{1}\ldots
v_{n}\wedge\\\ \hskip 14.22636pt\exists
E_{0},\ldots,E_{n}.\,E\to^{I*}_{N}(u;E_{0},\ldots,E_{n})\wedge\forall
j.\,v_{j}\in\llbracket E_{j}\rrbracket$;

    4. (d)

$\exists n\leq
N,v_{0}\in\Sigma^{*},v_{1},\ldots,v_{n-1}\in\Sigma^{+},v_{n}\in\Sigma^{*}.\,v\in
v_{0}\cdot^{I}v_{1}\cdot^{I}\ldots\cdot^{I}v_{n}\wedge\\\ \hskip
14.22636pt\exists
E_{0},\ldots,E_{n}.\,E\to^{I*}_{N}(u;E_{0},\ldots,E_{n})\wedge\forall
j.\,v_{j}\in\llbracket E_{j}\rrbracket^{I}$.

  2. 2.

for any $u\in\Sigma^{*}$,
$u\in\llbracket E\rrbracket^{I}\iff(u=\varepsilon\wedge
E{\downarrow})\vee(u\neq\varepsilon\wedge\exists
E_{0},E_{1}.\,E\to^{I*}_{N}(u;E_{0},E_{1})\wedge E_{0}{\downarrow}\wedge
E_{1}{\downarrow})$.

######  Proof 6.9 (Proof of 1).

(a) $\Longrightarrow$ (b) is from $E$ having uniform rank at most $N$. (b)
$\Longrightarrow$ (c) follows from Proposition 6.6. (c) $\Longrightarrow$ (d)
and (d) $\Longrightarrow$ (a) are those from Proposition 6.4.

######  Example 6.10.

We go back to Example 4.11. Recall that $E=_{\mathrm{df}}aa+ab+b$ and
$E_{b}=_{\mathrm{df}}R^{I}_{b}E=aa+a0+0$. Here is one of the refined
reordering parts-of-derivatives of $E^{*}$ along $bb$.

$\begin{array}[]{l}\small
E^{*}\to^{I*}_{2}(bb;E_{b}^{*}(a1),1(E_{b}^{*}(a1)),1E^{*})\lx@proof@logical@and
E^{*}\to^{I*}_{2}(b;E_{b}^{*}(a1),1E^{*})\lx@proof@logical@and
E^{*}\to^{I*}_{2}(\varepsilon;E^{*})E^{*}\Rightarrow^{I}_{2}(b;E_{b}^{*}(a1),1E^{*})\lx@proof@logical@and
E^{*}\to^{I}(b;E^{*}_{b}(a1),1E^{*})aa+ab+b\to^{I}(b;a1,1)ab+b\to^{I}(b;a1,1)ab\to^{I}(b;a1,1)b\to^{I}(b;1,1)0<2E_{b}^{*}(a1),1E^{*}\Rightarrow^{I}_{2}(b;E_{b}^{*}(a1),1(E_{b}^{*}(a1)),1E^{*})\lx@proof@logical@and
1E^{*}\to^{I}(b;1(E^{*}_{b}(a1)),1E^{*})E^{*}\to^{I}(b;E^{*}_{b}(a1),1E^{*})aa+ab+b\to^{I}(b;a1,1)ab+b\to^{I}(b;a1,1)ab\to^{I}(b;a1,1)b\to^{I}(b;1,1)1<2\end{array}$

In this example, we chose $N=_{\mathrm{df}}2$. The regexp
$1(E_{b}^{*}(a1))\doteq(aa)^{*}a$ is not nullable, so we could not have
dropped it. From here we cannot continue by deriving along a third $b$ by
again taking it from the summand $ab$ of $E$ in $1E^{*}$, as this would
produce another nondroppable $1(E_{b}^{*}(a1))$ and make the list too long
(longer than 3). For example, we are not allowed to establish
$w=_{\mathrm{df}}bbbaaa\in\llbracket E^{*}\rrbracket^{I}$ (by deriving $E^{*}$
along $w$ and checking if we can arrive at $E_{0},E_{1}$ with both
$E_{0},E_{1}$ nullable), mandated by $z=_{\mathrm{df}}ababab\in\llbracket
E^{*}\rrbracket$, but we are allowed to do so because of
$z^{\prime}=_{\mathrm{df}}bbabaa\in\llbracket E^{*}\rrbracket$. The word $z$
is not useful since among the splits of $w$ as $w=uv$ there is
$u=_{\mathrm{df}}bbb$, $v=_{\mathrm{df}}aaa$, which splits $z$ as
$u\mathrel{{\sim}{\lhd}}z\mathrel{{\rhd}{\sim}}v$ scattering $u$ into 3 blocks
as $z=a\underline{b}a\underline{b}a\underline{b}$ (we underline the letters
from $u$); the full sequence of these corresponding splits of $z$ is $ababab$,
$a\underline{b}abab$, $a\underline{b}a\underline{b}ab$,
$a\underline{b}a\underline{b}a\underline{b}$,
$\underline{ab}a\underline{b}a\underline{b}$,
$\underline{abab}a\underline{b}$, $\underline{ababab}$. The word $z^{\prime}$,
on the contrary, is fine because, for every split of $w$ as $w=uv$, there are
at most two blocks of letters from $u$ in $z^{\prime}$: $bbabaa$,
$\underline{b}babaa$, $\underline{bb}abaa$, $\underline{bb}a\underline{b}aa$,
$\underline{bbab}aa$, $\underline{bbaba}a$, $\underline{bbabaa}$. The choice
$N=2$ suffices for accepting all of $\llbracket E^{*}\rrbracket^{I}$, since
$\llbracket E^{*}\rrbracket$ happens to have uniform rank 2.

The refined Antimirov reordering parts-of-derivatives of a regexp $E$ give a
nondeterministic automaton by $Q^{E}=_{\mathrm{df}}\\{\Gamma\mid\exists
u\in\Sigma^{*}.\,E\to^{I*}(u;\Gamma)\\}$, $I^{E}=_{\mathrm{df}}\\{E\\}$,
$F^{E}=_{\mathrm{df}}\\{E\mid E{\downarrow}\\}\cup\\{E_{0},E_{1}\in Q^{E}\mid
E_{0}{\downarrow}\wedge E_{1}{\downarrow}\\}$,
$\Gamma\to^{E}(a;\Gamma^{\prime})=_{\mathrm{df}}\Gamma\Rightarrow^{I}(a;\Gamma^{\prime})$
for $\Gamma,\Gamma^{\prime}\in Q^{E}$. By Prop. 6.4, this automaton accepts
$\llbracket E\rrbracket^{I}$. It is generally not finite as $Q^{E}$ can
contain states $\Gamma$ of any length.

Given $N\in\mathbb{N}$, another automaton is obtained by restricting $Q^{E}$,
$F^{E}$ and $\to^{E}$ to $Q^{E}_{N}=_{\mathrm{df}}\\{\Gamma\mid\exists
u\in\Sigma^{*}.\,E\to^{I*}_{N}(u;\Gamma)\\}$,
$F^{E}_{N}=_{\mathrm{df}}\\{E\mid E{\downarrow}\\}\cup\\{E_{0},E_{1}\in
Q^{E}_{N}\mid E_{0}{\downarrow}\wedge E_{1}{\downarrow}\\}$,
$\Gamma\to^{E}_{N}(a;\Gamma^{\prime})=_{\mathrm{df}}\Gamma\Rightarrow^{I}_{N}(a;\Gamma^{\prime})$
for $\Gamma,\Gamma^{\prime}\in Q^{E}_{N}$. By Cor. 6.8, if $\llbracket
E\rrbracket$ has uniform rank at most $N$, then this smaller automaton accepts
$\llbracket E\rrbracket^{I}$ despite the truncation. If $\llbracket
E\rrbracket$ does not have uniform rank or we choose $N$ smaller than the
uniform rank, then the $N$-truncated automaton recognizes a proper subset of
$\llbracket E\rrbracket^{I}$. Prop. 5.7 gives an example of this: however we
choose $N$, the $N$-truncated automaton fails to accept the word
$a^{n}b^{n}ca^{n}b^{n}$ for $n>N$. This happens because $\llbracket
E\rrbracket$ does not have uniform rank (and that it has rank 2 does not
help).

###  6.2 Automaton Finiteness for Regular Expressions with Uniform Rank

Is the $N$-truncated Antimirov automaton finite? The states $\Gamma$ of
$Q^{E}_{N}$ are all of length at most $N+1$, so there is hope. The automaton
will be finite if we can find a finite set containing all the individual
regexps $E^{\prime}$ appearing in the states $\Gamma$. We now define such a
set $E^{\to*}$.

######  Definition 6.11.

We define functions
$(\\_)^{\rightsquigarrow+},\mathbf{R},(\\_)^{\to+},(\\_)^{\to*}:\mathsf{RE}\to\mathcal{P}\mathsf{RE}$
by

$\small\begin{array}[]{rcl@{\hspace*{3cm}}rcl}a^{\rightsquigarrow+}&=_{\mathrm{df}}&\\{1\\}\hfil\hskip
85.35826pt&(E+F)^{\rightsquigarrow+}&=_{\mathrm{df}}&E^{\rightsquigarrow+}\cup
F^{\rightsquigarrow+}\\\
0^{\rightsquigarrow+}&=_{\mathrm{df}}&\emptyset\hfil\hskip
85.35826pt&1^{\rightsquigarrow+}&=_{\mathrm{df}}&\emptyset\\\\[3.87498pt]
(EF)^{\rightsquigarrow+}&=_{\mathrm{df}}&\lx@intercol
E^{\rightsquigarrow+}\cup F^{\rightsquigarrow+}\cup
E^{\rightsquigarrow+}\cdot\\{F\\}\cup\\{E\\}\cdot F^{\rightsquigarrow+}\cup
E^{\rightsquigarrow+}\cdot F^{\rightsquigarrow+}\hfil\lx@intercol\\\
(E^{*})^{\rightsquigarrow+}&=_{\mathrm{df}}&\lx@intercol
E^{\rightsquigarrow+}\cup\\{E^{*}\\}\cdot E^{\rightsquigarrow+}\cup
E^{\rightsquigarrow+}\cdot\\{E^{*}\\}\cup
E^{\rightsquigarrow+}\cdot(\\{E^{*}\\}\cdot E^{\rightsquigarrow+})\cup\
(E^{\rightsquigarrow+}\cdot\\{E^{*}\\})\cdot
E^{\rightsquigarrow+}\hfil\lx@intercol\end{array}$
$\small\begin{array}[]{rcl}\mathbf{R}E&=_{\mathrm{df}}&\\{R^{I}_{X}E\mid
X\subseteq\Sigma\\}\\\
E^{\to+}&=_{\mathrm{df}}&\mathbf{R}(E^{\rightsquigarrow+})\\\
E^{\to*}&=_{\mathrm{df}}&\\{E\\}\cup E^{\to+}\end{array}$

######  Proposition 6.12.

  1. 1.

For any $E$, the set $E^{\to*}$ is finite.

  2. 2.

For any $E$ and $X$, we have $(R^{I}_{X}E)^{\to*}\subseteq
R^{I}_{X}(E^{\to*})$.

  3. 3.

For any $E$, $a$ and $E_{l},E_{r}$, if $E\to^{I}(a;E_{l},E_{r})$, then
$E_{l}\in R^{I}_{a}(E^{\rightsquigarrow+})$ and $E_{r}\in
E^{\rightsquigarrow+}$.

  4. 4.

For any $E,E^{\prime},X,a,E^{\prime}_{l},E^{\prime}_{r}$, if $E^{\prime}\in
R^{I}_{X}(E^{\rightsquigarrow+})$ and
$E^{\prime}\to^{I}(a;E^{\prime}_{l},E^{\prime}_{r})$,
then $E^{\prime}_{l}\in R^{I}_{Xa}(E^{\rightsquigarrow+})$ and
$E^{\prime}_{r}\in R^{I}_{X}(E^{\rightsquigarrow+})$.

  5. 5.

For any $E$, $u$ and $E_{0},\ldots,E_{n}$, if
$E\to^{I*}(u;E_{0},\ldots,E_{n})$, then $\forall j.\,E_{j}\in E^{\to*}$.

######  Proposition 6.13.

For every $E$ and $N$, the state set $\\{\Gamma\mid\exists
u\in\Sigma^{*}.\,E\to^{I*}_{N}(u;\Gamma)\\}$ of the $N$-truncated refined
Antimirov automaton for $E$ (accepting $\llbracket E\rrbracket^{I}$ if
$\llbracket E\rrbracket$ has uniform rank at most $N$) is finite.

##  7 Related Work

Syntactic derivative constructions for regular expressions extended with
constructors for (versions of) the shuffle operation have been considered, for
example, by Sulzmann and Thiemann [23] for the Brzozowski derivative and by
Broda et al. [6] for the Antimirov derivative. This is relevant to our
derivatives since $L\cdot^{I}L^{\prime}$ is by definition a language between
$L\cdot L^{\prime}$ and $L\mathrel{{\sqcup}{\sqcup}}L^{\prime}$. Thus our
Brzozowski and Antimirov reordering derivatives of $EF$ must be between the
classical Brzozowski and Antimirov derivatives of $EF$ and
$E\mathrel{{\sqcup}{\sqcup}}F$.

##  8 Conclusion and Future Work

We have shown that the Brzozowski and Antimirov derivative operations
generalize to trace closures of regular languages in the form of reordering
derivative operations. The sets of Brzozowski resp. Antimirov reordering
(parts-of-)derivatives of a regexp are generally infinite, so the
deterministic and nondeterministic automata that they give, accepting the
trace closure, are generally infinite. Still, if the regexp is star-connected,
their appropriate quotients are finite. Also, the set of $N$-bounded refined
Antimirov reordering parts-of-derivatives is finite without quotienting, and
we showed that, if the language of the regexp has uniform rank at most $N$,
the $N$-truncated refined Antimirov automaton accepts the trace closure. We
also proved that star-connected expressions define languages with finite
uniform rank.

In summary, we have established the following picture.

$E$ star-connectedProp. 4.36Prop. 5.17Klunder et al. [12]Quot of Antim for
$\llbracket E\rrbracket^{I}$ finiteKleene$\llbracket E\rrbracket$ has uniform
rankProp. 6.13triv.Refined Antim for $\llbracket E\rrbracket^{I}$
finiteKleene$\llbracket E\rrbracket$ has rankHashiguchi [9]$\llbracket
E\rrbracket^{I}$ regularOchmański [18]$\llbracket E\rrbracket^{I}=\llbracket
E^{\prime}\rrbracket^{I}$ for some star-conn $E^{\prime}$

Our intended application of reordering derivatives is operational semantics in
the context of relaxed memory (where, e.g., shadow writes, i.e., writes from
local buffers to shared memory, can be reorderable with other actions). For
sequential composition $EF$ it is usually required that, to execute any action
from $F$, execution of $E$ must have completed. In the jargon of derivatives,
this is to say that for an action from $F$ to become executable, what is left
of $E$ has to have become nullable (i.e., one can consider the execution of
$E$ completed). With reordering derivatives, we can execute an action from $F$
successfully even when what is left of $E$ is not nullable. It suffices that
some sequence of actions to complete the residual of $E$ is reorderable with
the selected action of $F$.

In the definitions of the derivative operations we only use $I$ in one
direction, i.e., we do not make use of its symmetry. It would be interesting
to see if our results can be generalized to the setting of semi-commutations
[8] and which changes are required for that.

## References

  * [1] IJsbrand Jan Aalbersberg and Hendrik Jan Hoogeboom.  Characterizations of the decidability of some problems for regular trace languages.  Math. Syst. Theory, 22(1):1–19, 1989.  doi:10.1007/BF02088289.
  * [2] IJsbrand Jan Aalbersberg and Emo Welzl.  Trace languages defined by regular string languages.  Theor. Inf. Appl., 20(2):103–119, 1986.  doi:10.1051/ita/1986200201031.
  * [3] Valentin M. Antimirov.  Partial derivatives of regular expressions and finite automaton constructions.  Theor. Comput. Sci., 155(2):291–319, 1996.  doi:10.1016/0304-3975(95)00182-4.
  * [4] Alberto Bertoni, Giancarlo Mauri, and Nicoletta Sabadini.  Equivalence and membership problems for regular trace languages.  In Mogens Nielsen and Erik Meineche Schmidt, editors, Automata, Languages and Programming: 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings, volume 140 of Lecture Notes in Computer Science, pages 61–71. Springer, 1982.  doi:10.1007/BFb0012757.
  * [5] Alberto Bertoni, Giancarlo Mauri, and Nicoletta Sabadini.  Unambiguous regular trace languages.  In Janos Demetrovics, Gyula Katona, and Arto Salomaa, editors, Algebra, Combinatorics, and Logic in Computer Science, volume 42 of Collquia Mathematica Societas János Bolyai, pages 113–123. North-Holland, 1986.
  * [6] Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.  Partial derivative automaton for regular expressions with shuffle.  In Jeffrey Shallit and Alexander Okhotin, editors, Descriptional Complexity of Formal Systems: 17th International Workshop, DCFS 2015, Waterloo, ON, Canada, June 25-27, 2015, Proceedings, volume 9118 of Lecture Notes in Computer Science, pages 21–32. Springer, 2015.  doi:10.1007/978-3-319-19225-3_2.
  * [7] Janusz A. Brzozowski.  Derivatives of regular expressions.  J. ACM, 11(4):481–494, 1964.  doi:10.1145/321239.321249.
  * [8] Mireille Clerbout and Michel Latteux.  Semi-commutations.  Inf. Comput., 73(1):59–74, 1987.  doi:10.1016/0890-5401(87)90040-X.
  * [9] Kosaburo Hashiguchi.  Recognizable closures and submonoids of free partially commutative monoids.  Theor. Comput. Sci., 86(2):233–241, 1991.  doi:10.1016/0304-3975(91)90019-X.
  * [10] Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman.  Concurrent Kleene algebra and its foundations.  J. Log. Algebr. Program., 80(6):266–296, 2011.  doi:10.1016/j.jlap.2011.04.005.
  * [11] Stephen C. Kleene.  Representation of events in nerve sets and finite automata.  In Claude E. Shannon and John McCarthy, editors, Automata Studies, volume 34 of Annals of Mathematics Studies, pages 3–42. Princeton University Press, 1956.
  * [12] Barbara Klunder, Edward Ochmański, and Krystyna Stawikowska.  On star-connected flat languages.  Fund. Inf., 67(1–3):93–105, 2005.  URL: http://content.iospress.com/articles/fundamenta-informaticae/fi67-1-3-08.
  * [13] Dexter Kozen.  A completeness theorem for Kleene algebras and the algebra of regular events.  Inf. Comput., 110(2):366–390, 1994.  doi:10.1006/inco.1994.1037.
  * [14] Hendrik Maarand and Tarmo Uustalu.  Reordering derivatives of trace closures of regular languages.  In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27–30, 2019, Amsterdam, The Netherlands, volume 140 of Leibniz International Proceedings in Informatics, pages 40:1–40:16. Dagstuhl Publishing, 2019.  doi:10.4230/lipics.concur.2019.40.
  * [15] Antoni Mazurkiewicz.  Concurrent program schemes and their interpretations.  DAIMI Rep. PB-78, University of Aarhus, 1978.  doi:10.7146/dpb.v6i78.7691.
  * [16] Antoni Mazurkiewicz.  Introduction to trace theory.  In Volker Diekert, editor, The Book of Traces, pages 3–41. World Scientific, 1995.  doi:10.1142/9789814261456_0001.
  * [17] J. D. McKnight.  Kleene quotient theorems.  Pac. J. Math., 14(4):1343–1352, 1964.  doi:10.2140/pjm.1964.14.1343.
  * [18] Edward Ochmański.  Regular behaviour of concurrent systems.  Bull. EATCS, 27:56–67, 1985.
  * [19] Edward Ochmański.  Recognizable trace languages.  In Volker Diekert, editor, The Book of Traces, pages 167–204. World Scientific, 1995.  doi:10.1142/9789814261456_0006.
  * [20] Michael O. Rabin and Dana S. Scott.  Finite automata and their decision problems.  IBM J. Res. Devel., 3(2):114–125, 1959.  doi:10.1147/rd.32.0114.
  * [21] Jacques Sakarovitch.  On regular trace languages.  Theor. Comput. Sci., 52:59–75, 1987.  doi:10.1016/0304-3975(87)90080-6.
  * [22] Jacques Sakarovitch.  The "last" decision problem for rational trace languages.  In Imre Simon, editor, LATIN ’92, 1st Latin American Symposium on Theoretical Informatics, São Paulo, Brazil, April 6-10, 1992, Proceedings, volume 583 of Lecture Notes in Computer Science, pages 460–473. Springer, 1992.  doi:10.1007/BFb0023848.
  * [23] Martin Sulzmann and Peter Thiemann.  Derivatives for regular shuffle expressions.  In Adrian-Horia Dediu, Enrico Formenti, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications: 9th International Conference, LATA 2015, Nice, France, March 2-6, 2015, Proceedings, volume 8977 of Lecture Notes in Computer Science, pages 275–286. Springer, 2015.  doi:10.1007/978-3-319-15579-1_21.
  * [24] Wiesław Zielonka.  Notes on finite asynchronous automata.  Theor. Inf. Appl., 21(2):99–135, 1987.  doi:10.1051/ita/1987210200991.
  * [25] Wiesław Zielonka.  Asynchronous automata.  In Volker Diekert, editor, The Book of Traces, pages 205–247. World Scientific, 1995.  doi:10.1142/9789814261456_0007.