# Kleene Theorems for Lasso Languages and $\omega$-Languages

Mike Cruchten
The University of Sheffield

###### Abstract

Automata operating on pairs of words were introduced as an alternative way of
capturing acceptance of regular $\omega$-languages. Families of DFAs and lasso
automata operating on such pairs followed, giving rise to minimisation
algorithms, a Myhill-Nerode theorem and language learning algorithms. Yet
Kleene theorems for such a well-established class are still missing. Here, we
introduce rational lasso languages and expressions, show a Kleene theorem for
lasso languages and explore the connection between rational lasso and
$\omega$-expressions, which yields a Kleene theorem for $\omega$-languages
with respect to saturated lasso automata. For one direction of the Kleene
theorems, we also provide a Brzozowski construction for lasso automata from
rational lasso expressions.

##  1 Introduction

Lassos occur naturally in the study of $\omega$-automata, where they manifest
themselves in nondeterministic Büchi automata as paths consisting of a prefix
leading from the initial state to some state $q$, and a period which leads
from $q$ back to itself, traversing some accepting state infinitely often. The
existence of such paths for non-empty non-deterministic Büchi automata is
necessary, in that every such automaton where some accepting state is
reachable must admit an accepting run in the shape of a lasso. On the level of
words, these infinite paths correspond to infinite words of the shape
$uv^{\omega}$, which are called ultimately periodic words. These words play an
important role, as regular $\omega$-languages are completely characterised by
them in the sense that two regular $\omega$-languages are equal if and only if
they contain the same ultimately periodic words. By representing an ultimately
periodic word $uv^{\omega}$ as a string $u\$v$, Calbrix, Nivat and Podelski
show that for any regular $\omega$-language $L$, the set $L_{\$}=\\{u\$v\mid
uv^{\omega}\in L\\}$ is regular and can be accepted by a finite deterministic
automaton (DFA) using an alphabet extended by the symbol $\$$ [4].
Additionally, Calbrix et al. give conditions under which a regular language
$U$ over the extended alphabet is equal to $L_{\$}$ for some regular
$\omega$-language $L$. Their work shows that certain DFAs over an extended
alphabet, called $L_{\$}$-automata, act as acceptors of regular
$\omega$-languages. These $L_{\$}$-automata are deterministic and their
acceptance condition makes no longer use of infinite paths. The results came
with the hope of improving existing algorithms for deciding emptiness and
language inclusion of regular $\omega$-languages, which are prominently used
in software verification and model checking.

Angluin and Fisman use $(u,v)$ (instead of $u\$v$) as a representation of
$uv^{\omega}$, and introduce families of DFAs (FDFAs) operating on such pairs
[2]. They combine the work by Calbrix et al. on $L_{\$}$-automata and also
work done by Maler and Staiger [9] on syntactic congruences to produce
different variations of FDFAs, the periodic and syntactic FDFA. They
additionally define a recurrent FDFA and investigate the differences in size
for the various FDFAs. From these automata, they devise language learning
algorithms to learn regular $\omega$-languages and show that this can be done
in polynomial time in the size of the FDFA. Moreover, in [1], they investigate
the complexity of certain operations and decision procedures on FDFAs,
including deciding emptiness and language inclusion, and the performance of
Boolean operations. They show that these can all be performed in non-
deterministic logarithmic space, validating the hopes of Calbrix et al.

An equivalent automaton to the FDFA is the lasso automaton defined by Ciancia
and Venema [5]. Lasso automata also operate on pairs $(u,v)$ which they call
lassos. We follow this convention and call pairs $(u,v)$ representing
ultimately periodic words lassos. In [5], Ciancia et al. give a Myhill-Nerode
theorem and show that lasso automata can be minimised using partition
refinement. Alternatively, minimisation can also be obtained from a double
reverse powerset construction à la Brzozowski [6].

Although automata operating on lassos, such as $L_{\$}$-automata, FDFAs and
lasso automata, are well-established in many regards, they still lack a Kleene
theorem. Our main goal is to establish a Kleene theorem for lasso languages,
that is sets of lassos, with respect to lasso automata, and to show how
rational lasso and $\omega$-expressions relate. This paves a way towards a
Kleene theorem for $\omega$-languages with respect to saturated lasso automata
(Definition 2.7).

rational lasso lang.regular lasso lang.rational $\omega$-lang.regular
$\omega$-lang.5.74.145.4,5.6[4]6.156.16[4] Figure 1: Diagram showing our main
contributions as dashed arrows.

Our contributions are indicated as dashed arrows in Figure 1. We define
rational lasso languages as those lasso languages that can be obtained from
rational languages using rational lasso operations. Our first contribution is
a Kleene theorem for lasso languages: we show that a lasso language is
rational if and only if it is accepted by a finite lasso automaton (Theorem
5.7). For one direction, we provide a Brzozowski construction, which turns a
rational lasso expression into a finite lasso automaton accepting the
corresponding rational lasso language (Theorem 4.14). For the converse
direction, we show how to dissect a finite lasso automaton into several DFAs
and prove that the lasso language accepted by the lasso automaton can be
obtained from the rational languages corresponding to the DFAs by using the
rational lasso operations (Proposition 5.4 and Corollary 5.6), following ideas
from [4].

Secondly, we study the relationship between rational lasso and
$\omega$-expressions. We introduce a novel notion of rational lasso expression
representing a rational $\omega$-expression (Definition 6.2). Intuitively, it
expresses that the language semantics of either expression completely
determines that of the other. We show that, for any given rational
$\omega$-expression, we can construct a representing rational lasso expression
in a syntactic manner provided we have access to two additional operations on
rational expressions (cf. Proposition 6.15).

These two contributions, together with a result of [4], allow us to re-
establish Kleene’s theorem for $\omega$-languages with respect to saturated
lasso automata. Given a rational $\omega$-language, we can turn it into a
rational lasso expression (Proposition 6.15) and apply our Brzozowski
construction (Theorem 4.14) to obtain the desired finite saturated lasso
automaton, hence every rational $\omega$-language is regular (Theorem 6.16).
The converse direction is given by [4], showing that every $\omega$-language
accepted by a finite saturated lasso automaton is rational.

### Organisation of the paper.

Section 2 consists of the preliminaries. In Section 3 we introduce rational
lasso expressions and languages together with an algebra. Section 4 is devoted
to a Brzozowski construction for lasso automata. Section 5 shows how to obtain
expressions from automata, and Section 6 investigates the connection between
rational lasso and $\omega$-expressions.

##  2 Preliminaries

Throughout this article, $\Sigma$ denotes a finite alphabet. The free monoid
$(\Sigma^{\ast},\cdot,\varepsilon)$ over $\Sigma$ is formed by finite words,
written $u,v,w$, with concatenation $u\cdot v=uv$ and the empty word
$\varepsilon$. We write $\Sigma^{\omega}$ for the set of infinite words and
$\Sigma^{\text{up}}$ for the set of ultimately periodic words, that is, those
of the form $uv^{\omega}$ with $v\not=\varepsilon$. A _lasso_ is a pair
$(u,v)\in\Sigma^{\ast}\times\Sigma^{+}$, with $u$ the _spoke_ and $v$ the
_loop_. We write $\Sigma^{\ast+}$ for the set $\Sigma^{\ast}\times\Sigma^{+}$
and think of the lasso $(u,v)$ as a representative for $uv^{\omega}$.

We write $U,V,W$ for languages of words and $L,K$ for languages of infinite
words ($\omega$-languages) or of lassos, depending on context. As is standard,
the rational languages are those obtained from $\emptyset$, $\\{a\\}\
(a\in\Sigma)$ and $\\{\varepsilon\\}$ using the rational operations of
language concatenation, union and Kleene star. Similarly, the rational
$\omega$-languages are those which can be written as a finite union
$\bigcup_{i\in I}U_{i}\cdot V_{i}^{\omega}$ where the $U_{i}$ and $V_{i}$ are
rational languages, $\cdot$ denotes the concatenation between a language and
an $\omega$-language, and $(-)^{\omega}$ denotes $\omega$-iteration. A
language is regular if it is accepted by a DFA and an $\omega$-language is
regular if it is accepted by a finite nondeterministic Büchi automaton. For an
$\omega$-language $L$, $\text{UP}(L)=L\cap\Sigma^{\text{up}}$ is its
_ultimately periodic fragment_. The set Exp of rational expressions is given
by the grammar:

$\displaystyle t$ $\displaystyle::=0\mid 1\mid a\in\Sigma\mid t\cdot t\mid
t+t\mid t^{\ast}.$

We reserve the symbols $t,r,s$ for rational expressions. To each rational
expression we associate a rational language through the semantics map
$\llbracket-\rrbracket:\text{Exp}\to 2^{\Sigma^{\ast}}$ which is the unique
map satisfying:

$\displaystyle\llbracket 0\rrbracket$ $\displaystyle=\emptyset$
$\displaystyle\llbracket 1\rrbracket$ $\displaystyle=\\{\varepsilon\\}$
$\displaystyle\llbracket a\rrbracket$ $\displaystyle=\\{a\\}$
$\displaystyle\llbracket t\cdot r\rrbracket$ $\displaystyle=\llbracket
t\rrbracket\cdot\llbracket r\rrbracket$ $\displaystyle\llbracket
t+r\rrbracket$ $\displaystyle=\llbracket t\rrbracket\cup\llbracket
r\rrbracket$ $\displaystyle\llbracket t^{\ast}\rrbracket$
$\displaystyle=\llbracket t\rrbracket^{\ast}$

We write $N$ for the set of all rational expressions which have the _empty
word property_ , that is those $t\in\text{Exp}$ such that
$\varepsilon\in\llbracket t\rrbracket$. The sets $\text{Exp}_{\omega}$ of
$\omega$-rational expressions are given by the grammar:

$\displaystyle T$ $\displaystyle::=0_{\omega}\mid T+_{\omega}T\mid
t\cdot_{\omega}T\mid r^{\omega},$

where $t,r\in\text{Exp}$ and $r\not\in N$. We drop the subscript
$(-)_{\omega}$ whenever this does not lead to confusion, thus simply writing
$0,+$ and $\cdot$. The symbol $T$ ($T_{1},T_{2},\ldots$) is reserved for
rational $\omega$-expressions. Similarly to the rational expressions, we
associate to each rational $\omega$-expression a rational $\omega$-language
through the semantics map
$\llbracket-\rrbracket_{\omega}:\text{Exp}_{\omega}\to 2^{\Sigma^{\omega}}$
uniquely determined by

$\displaystyle\llbracket 0_{\omega}\rrbracket_{\omega}$
$\displaystyle=\emptyset$ $\displaystyle\llbracket
T_{1}+_{\omega}T_{2}\rrbracket_{\omega}$ $\displaystyle=\llbracket
T_{1}\rrbracket_{\omega}\cup\llbracket T_{2}\rrbracket_{\omega}$
$\displaystyle\llbracket t\cdot_{\omega}T\rrbracket_{\omega}$
$\displaystyle=\llbracket t\rrbracket\cdot\llbracket T\rrbracket_{\omega}$
$\displaystyle\llbracket r^{\omega}\rrbracket_{\omega}$
$\displaystyle=\llbracket r\rrbracket^{\omega}.$

The following definition introduces a rewrite system on lassos. The rewrite
system alongside some of its properties (which are stated below) can be found
in [6].

###### Definition 2.1.

We define the following rewrite rules on $\Sigma^{\ast+}$:

$\prftree[r]{(\gamma_{1})}{a\in\Sigma}{(ua,va)}{(u,av)}\quad\quad\quad\quad\prftree[r]{(\gamma_{2})}{(u,v^{k})}{(k>1)}{(u,v)}$

We write $(u,v)\to_{\gamma_{i}}(u^{\prime},v^{\prime})$ if $(u,v)$ rewrites to
$(u^{\prime},v^{\prime})$ in one step under $\gamma_{i}$ and say that $(u,v)$
_$\gamma_{i}$ -reduces_ to $(u^{\prime},v^{\prime})$ (or that
$(u^{\prime},v^{\prime})$ _$\gamma_{i}$ -expands_ to $(u,v)$). We let
${\to_{\gamma}}={\to_{\gamma_{1}}}\cup{\to_{\gamma_{2}}}$, denote by
$\sim_{\gamma}$ the least equivalence relation including $\to_{\gamma}$ and
say that two lassos are _$\gamma$ -equivalent_ if they are
$\sim_{\gamma}$-related.

###### Proposition 2.2.

The relation $\to_{\gamma}$ is confluent and strongly normalising.

It follows from this proposition that every lasso $(u,v)$ has a unique _normal
form_. As an example, take the lasso $(aba,baba)$ which is a representative
for $(ab)^{\omega}$. We show the different reductions which lead to the normal
form $(\varepsilon,ab)$ below.

$(\varepsilon,ab)$$(\varepsilon,abab)$$(a,ba)$$(a,baba)$$(ab,ab)$$(ab,abab)$$(aba,ba)$$(aba,baba)$$\gamma_{2}$$\gamma_{1}$$\gamma_{2}$$\gamma_{1}$$\gamma_{1}$$\gamma_{2}$$\gamma_{1}$$\gamma_{1}$$\gamma_{2}$$\gamma_{1}$

This picture suggests that if $(u,v)\to_{\gamma}(u^{\prime},v^{\prime})$, then
$uv^{\omega}=u^{\prime}v^{\prime\omega}$, that is, reduction preserves the
ultimately periodic word which is represented. In fact, the other direction
also holds as shown by the next proposition.

###### Proposition 2.3 (Lasso Representation Lemma).

Let $(u,v),(u^{\prime},v^{\prime})\in\Sigma^{\ast+}$. Then

$(u,v)\sim_{\gamma}(u^{\prime},v^{\prime})\iff
uv^{\omega}=u^{\prime}v^{\prime\omega}.$

One consequence of this proposition, is that two lassos reduce to the same
normal form if and only if they are a representative of the same ultimately
periodic word.

###### Definition 2.4 ([5]).

A _lasso automaton_ is a structure
$\mathcal{A}=(X,Y,\overline{x},\delta_{1},\delta_{2},\delta_{3},F)$ where
$\delta_{1}\colon X\to X^{\Sigma}$, $\delta_{2}\colon X\to Y^{\Sigma}$,
$\delta_{3}\colon Y\to Y^{\Sigma}$ and $F\subseteq Y$. We call $X$ and $Y$ the
sets of _spoke_ and _loop states_. The maps $\delta_{1},\delta_{2}$ and
$\delta_{3}$ are called the _spoke_ , _switch_ and _loop transition maps_ of
$\mathcal{A}$. The set $F$ denotes the _accepting states_ and $\overline{x}\in
X$ is the _initial state_ of $\mathcal{A}$.

We do not consider nondeterministic lasso automata in this text. For
convenience, we assume that $X$ and $Y$ are disjoint and define the map
$(\delta_{2}\mathop{:}\delta_{3}):X\uplus Y\to Y^{\Sigma}$ which is equal to
$\delta_{2}$ on $X$ and equal to $\delta_{3}$ on $Y$. The maps
$\delta_{1},(\delta_{2}\mathop{:}\delta_{3})$ and $\delta_{3}$ can be extended
from symbols to finite words in the usual way.

###### Definition 2.5 ([5]).

A lasso $(u,v)\in\Sigma^{\ast+}$ is _accepted_ by $\mathcal{A}$, if
$(\delta_{2}\mathop{:}\delta_{3})(\delta_{1}(\overline{x},u),v)\in F$. The set
of all lassos accepted by $\mathcal{A}$ is denoted $L_{\circ}(\mathcal{A})$. A
lasso language $L$ is _regular_ if it is accepted by a finite lasso automaton.

$0$start$1$$2$$3$$4$$b$$a$$b$$a$$a,b$$b$$a$$b$$a$$b$$a$$a,b$ Figure 2: A lasso
automaton accepting $\\{(a^{k},ba^{j})\mid k,j\in\mathbb{N}\\}$.

###### Example 2.6.

Figure 2 depicts a lasso automaton. The spoke states are labelled $0$ and $1$.
The states $2,3$ and $4$ are loop states. Spoke transitions are drawn as solid
arrows, switch transitions as dotted arrows and loop transitions as dashed
arrows. The initial state is indicated by the ‘start’ arrow and accepting
states are drawn as double circles. We give an example run for the lasso
$(aaa,baa)$. Reading this lasso from the initial state leads to the state

$(\delta_{2}\mathop{:}\delta_{3})(\delta_{1}(0,aaa),baa)=\delta_{3}(\delta_{2}(\delta_{1}(0,aaa),b),aa)=\delta_{3}(\delta_{2}(0,b),aa)=\delta_{3}(2,aa)=2.$

Hence $(aaa,baa)$ is accepted by the lasso automaton. The regular lasso
language it accepts is $\\{(a^{k},ba^{j})\mid k,j\in\mathbb{N}\\}$.

In [5], the authors define an $\Omega$-automaton as a lasso automaton with
special structural properties. We give an alternative definition of these
automata using saturation.

###### Definition 2.7.

A lasso automaton $\mathcal{A}$ is _saturated_ if for any two
$\gamma$-equivalent lassos
$(u_{1},v_{1}),(u_{2},v_{2})\in\Sigma^{\ast+}:(u_{1},v_{1})\in
L_{\circ}(\mathcal{A})\iff(u_{2},v_{2})\in L_{\circ}(\mathcal{A})$. An
_$\Omega$ -automaton_ is a saturated lasso automaton.

Finite $\Omega$-automata act as acceptors of regular $\omega$-languages. A
finite $\Omega$-automaton $\mathcal{A}$ accepts the regular $\omega$-language
$L$ if $L_{\circ}(\mathcal{A})=\\{(u,v)\mid uv^{\omega}\in L\\}$ [5]. Note
that $L_{\circ}(\mathcal{A})$ is always $\sim_{\gamma}$-saturated (that is, a
partition of $\sim_{\gamma}$ equivalence classes) for an $\Omega$-automaton
$\mathcal{A}$, and that $\\{(u,v)\mid uv^{\omega}\in L\\}=\\{(u,v)\mid
uv^{\omega}\in K\\}$ implies $L=K$ for regular $\omega$-languages $K,L$ [4].
The _regular $\omega$-language accepted by a finite $\Omega$-automaton
$\mathcal{A}$_ is denoted $L_{\omega}(\mathcal{A})$.

start$a,b$$a,b$$a$$b$$a$$b$ Figure 3: A saturated lasso automaton
($\Omega$-automaton).

###### Example 2.8.

The lasso automaton shown in Figure 3 is saturated. It accepts the regular
lasso language $\\{(u,a^{k})\mid u\in\Sigma^{\ast},k\geq 1\\}$ and the regular
$\omega$-language $\\{ua^{\omega}\mid u\in\Sigma^{\ast}\\}$. The automaton
from Example 2.6 (c.f. Figure 2) is not saturated as it accepts the lasso
$(\varepsilon,b)$ but it does not accept $(b,b)$ although these two lassos are
$\gamma$-equivalent.

##  3 Rational Lasso Expressions

In this section we introduce rational lasso expressions, languages and an
algebra for these, which we show to be sound. A lasso language is _rational_
if it is obtained from rational languages using the operations

$U^{\circ}=\\{(\varepsilon,u)\mid u\in U\\},\qquad U\cdot K=\\{(uv,w)\mid u\in
U,(v,w)\in K\\},\qquad K_{1}\cup K_{2},$

where $U$ is a rational language and $K,K_{1},K_{2}$ are rational lasso
languages.

From here on, we assume RA to be an arbitrary but fixed algebra of rational
expressions of signature $(0,1,+,\cdot,^{\ast})$ (for instance KA, the theory
of Kleene Algebra [8]). We write $\vdash_{\mathbf{RA}}t=r$ if $t=r$ is
deducible in RA. As it is always clear from context, we drop the subscript and
just write $\vdash t=r$, sometimes even dropping the turnstyle altogether. We
write $t\leq r$ for $\vdash t+r=r$, as the $+$-reduct of an RA-algebra is a
join-semilattice. Finally, for a formula $\varphi$, the _Iverson bracket_ of
$\varphi$ is defined as

$[\varphi]=\begin{cases}1&\text{if }\varphi\text{ is true},\\\
0&\text{otherwise}.\end{cases}$

###### Definition 3.1.

Let $t,r\in\text{Exp}$ with $r\not\in N$. The set $\text{Exp}_{\circ}$ of
_rational lasso expressions_ is defined by the grammar

$\rho,\sigma::=0_{\circ}\mid t\cdot_{\circ}\rho\mid\rho+_{\circ}\sigma\mid
r^{\circ}.$

Whenever it is clear from context, we drop the subscript $(-)_{\circ}$, simply
writing $0,+$ and $\cdot$. We associate a rational lasso language to each
rational lasso expression using the operations defined at the start of this
section.

###### Definition 3.2.

The _language semantics for rational lasso expressions_
$\llbracket-\rrbracket_{\circ}:\text{Exp}_{\circ}\to 2^{\Sigma^{\ast+}}$ is
given by

$\llbracket 0\rrbracket_{\circ}=\emptyset,\qquad\llbracket
t\cdot\rho\rrbracket_{\circ}=\llbracket
t\rrbracket\cdot\llbracket\rho\rrbracket_{\circ},\qquad\llbracket\rho+\sigma\rrbracket_{\circ}=\llbracket\rho\rrbracket_{\circ}\cup\llbracket\sigma\rrbracket_{\circ},\qquad\llbracket
r^{\circ}\rrbracket_{\circ}=\llbracket r\rrbracket^{\circ}.$

By definition, the lasso language semantics $\llbracket-\rrbracket_{\circ}$
extends the language semantics of rational expressions
$\llbracket-\rrbracket$.

start$b$$a$$a,b$$a$$b$$b$$a$$a,b$$a,b$$a,b$$a,b$ Figure 4: A finite lasso
automaton accepting $\llbracket b(a^{\ast}b^{\circ})\rrbracket_{\circ}$.

###### Example 3.3.

Let $\Sigma=\\{a,b\\}$ and consider the rational lasso expression
$b(a^{\ast}b^{\circ})$. We compute its language semantics recursively:

$\llbracket b(a^{\ast}b^{\circ})\rrbracket_{\circ}=\llbracket
b\rrbracket(\llbracket a^{\ast}\rrbracket\llbracket
b^{\circ}\rrbracket_{\circ})=\\{b\\}(\\{a^{k}\mid k\geq
0\\}\\{(\varepsilon,b)\\})=\\{b\\}\\{(a^{k},b)\mid k\geq
0\\}=\\{(ba^{k},b)\mid k\geq 0\\}.$

The rational lasso language obtained is also regular as it is accepted by the
finite lasso automaton in Figure 4.

Next, we introduce a theory to reason about regular lasso expressions. This
theory is sound with respect to the lasso language semantics, which we require
for the construction of a Brzozowski lasso automaton.

###### Definition 3.4.

The _two-sorted theory LA of lasso algebras_ extends the theory RA by the
following axioms:

$\displaystyle 1\cdot\rho$ $\displaystyle=\rho$ $\displaystyle 0\cdot\rho$
$\displaystyle=0$ $\displaystyle\rho+\sigma$ $\displaystyle=\sigma+\rho$
$\displaystyle(t+r)\cdot\rho$ $\displaystyle=t\cdot\rho+r\cdot\rho$
$\displaystyle 0^{\circ}$ $\displaystyle=0$ $\displaystyle(\rho+\sigma)+\tau$
$\displaystyle=\rho+(\sigma+\tau)$ $\displaystyle t\cdot(\rho+\sigma)$
$\displaystyle=t\cdot\rho+t\cdot\sigma$ $\displaystyle 0+\rho$
$\displaystyle=\rho$ $\displaystyle\rho+\rho$ $\displaystyle=\rho$
$\displaystyle t\cdot(r\cdot\rho)$ $\displaystyle=(t\cdot r)\cdot\rho$
$\displaystyle t\cdot 0$ $\displaystyle=0$ $\displaystyle(t+r)^{\circ}$
$\displaystyle=t^{\circ}+r^{\circ}\ (t,r\not\in N)$

with $t,r\in\text{Exp}$ and $\rho,\sigma,\tau\in\text{Exp}_{\circ}$. The
axioms together with the laws for equality and the substitution of provably
equivalent rational and rational lasso expressions gives us the deductive
system $\mathbf{LA}$. We write $\vdash_{\mathbf{LA}}\rho=\sigma$ when the
equation $\rho=\sigma$ is deducible in LA. Whenever it is clear from context,
we drop the turnstile $\vdash_{\mathbf{LA}}$.

The next proposition shows that the theory of lasso algebras is sound with
respect to the language semantics for rational lasso expressions. We make no
claim about its completeness.

###### Proposition 3.5 (Soundness).

Let $\rho,\sigma\in\text{Exp}_{\circ}$. Then
$\vdash_{\mathbf{LA}}\rho=\sigma\implies\llbracket\rho\rrbracket_{\circ}=\llbracket\sigma\rrbracket_{\circ}$.

The verification of the laws in Definition 3.4 is routine. It relies on the
following properties of the rational lasso operations. For rational languages
$U,V$ and rational lasso languages $K,L$, we have

  1. 1.

$U\cdot(V\cdot L)=(U\cdot V)\cdot L$,

  2. 2.

$(U\cup V)\cdot L=(U\cdot L)\cup(V\cdot L)$,

  3. 3.

$U\cdot(K\cup L)=U\cdot K\cup U\cdot L$,

  4. 4.

$(U\cup V)^{\circ}=U^{\circ}\cup V^{\circ}$.

###### Remark 3.6.

We briefly highlight the differences between lasso and Wagner algebras ([10]).
A Wagner algebra is a two-sorted algebra similar to the lasso algebra but with
an operation $(-)^{\omega}$ instead of $(-)^{\circ}$. They are used to reason
about rational $\omega$-expressions and Wagner showed completeness of his
axiomatisation with respect to the language semantics for rational
$\omega$-expressions. Wagner’s axiomatisation looks very similar to that of a
lasso algebra. However, the unary operations $(-)^{\circ}$ and $(-)^{\omega}$
satisfy different laws, the ones for $(-)^{\omega}$ being

$(t\cdot r)^{\omega}=t\cdot(r\cdot t)^{\omega}\qquad\text{ and }\qquad
t^{\omega}=(t^{+})^{\omega}.$

Other than this, there are two more subtle differences that can be pointed
out:

  1. 1.

from the $(-)^{\omega}$-axioms, one can deduce that $0^{\omega}=0$, which is
not the case for lasso algebras (i.e. we need the axiom $0^{\circ}=0$),

  2. 2.

Wagner has an additional derivation rule which allows to solve equations of a
particular type, such a rule is not given for lasso algebras.

Analogously to the situation for rational and rational $\omega$-expressions,
each rational lasso expression is provably equivalent to a rational lasso
expression of the form $\sum_{i=1}^{n}t_{i}\cdot r_{i}^{\circ}$. Such a form
is called a _disjunctive form_ , but note that a disjunctive form is not
unique.

###### Proposition 3.7.

Let $\rho\in\text{Exp}_{\circ}$. Then there exists $n\in\mathbb{N}$ and
$t_{1},\ldots,t_{n},r_{1},\ldots,r_{n}\in\text{Exp}$ with $r_{i}\not\in N$ for
all $1\leq i\leq n$ such that

$\vdash_{\mathbf{LA}}\rho=\sum_{i=1}^{n}t_{i}\cdot r_{i}^{\circ}.$

###### Proof.

We show this by structural induction on rational lasso expressions. For $0$ we
have that $0=0\cdot 0^{\circ}$. For $t^{\circ}$ we have $t^{\circ}=1\cdot
t^{\circ}$. For $r\cdot\rho$, we know by the induction hypothesis that we can
find a finite number of pairs $(t_{i},r_{i})$ such that
$\rho=\sum_{i}(t_{i},r_{i})$. It follows that

$r\cdot\rho=r\cdot\sum_{i}t_{i}\cdot r_{i}^{\circ}=\sum_{i}r\cdot(t_{i}\cdot
r_{i}^{\circ})=\sum_{i}(r\cdot t_{i})\cdot r_{i}^{\circ}.$

Finally, for $\rho+\sigma$ we can find two finite sets
$\\{(t_{i},r_{i})\\}_{i\in I},\\{(t_{j},r_{j})\\}_{j\in J}$ with
$\rho=\sum_{i}(t_{i},r_{i})$ and $\sigma=\sum_{j}(t_{j},r_{j})$, then clearly
$\rho+\sigma=\sum_{k\in I\cup J}(t_{k},r_{k})$ as required. ∎

We often write $(t,r)$ instead of $t\cdot r^{\circ}$, which accentuates the
distinction between the ‘finite’ and ‘infinite’ part more. It also allows for
a more direct correspondence to the language semantics as

$\llbracket(t,r)\rrbracket_{\circ}=\\{(u,v)\in\Sigma^{\ast+}\mid
u\in\llbracket t\rrbracket,v\in\llbracket r\rrbracket\\}.$

##  4 Rational Lasso Languages are Regular

In this section we explore a construction for lasso automata from rational
lasso expressions. Given a rational lasso expression $\rho$, our aim is to
build a finite lasso automaton $\mathcal{A}$ which accepts
$\llbracket\rho\rrbracket_{\circ}$. This shows one direction of Kleene’s
Theorem, namely that every rational lasso language is regular.

We start the section by going over the standard Brzozowski construction for
deterministic finite automata ([3]). The rest of the section generalises this
construction to finite lasso automata. For this we first define Brzozowski
derivatives for the spoke and switch transitions. We then show some results on
how they interact with the theory of lasso algebras and prove a fundamental
theorem. This allows us to define a Brzozowski lasso automaton whose spoke
states are rational lasso expressions with the property that the language
accepted from an initial state $\rho\in\text{Exp}_{\circ}$ is
$\llbracket\rho\rrbracket_{\circ}$. Finally, we introduce a suitable
equivalence relation to quotient our automaton which guarantees that our final
lasso automaton has only finitely many reachable states from any equivalence
class of rational lasso expressions.

If we consider a word $a_{1}\ldots a_{n}$, then after reading $a_{1}$ what
remains is $a_{2}\ldots a_{n}$. This is called a left-quotient and forms the
basic idea behind the Brzozowski derivative. The idea can be taken to the
level of sets where we start with a language $U$ and wonder what remains if we
tried to read an $a$ from all the words in $U$, again this is a left quotient
often written $a^{-1}U=\\{u\mid au\in U\\}$. The Brzozowski derivative tries
to capture this notion of a left-quotient syntactically.

The next set of definitions and results are well-known ([3]). The definition
of the Brzozowski derivative makes use of the Iverson bracket introduced in
Section 3.

###### Definition 4.1.

The _Brzozowski derivative_ $d:\text{Exp}\to\text{Exp}^{\Sigma}$ is defined
recursively on rational expressions.

$\displaystyle d(0,a)$ $\displaystyle=0$ $\displaystyle d(t+r,a)$
$\displaystyle=d(t,a)+d(r,a)$ $\displaystyle d(b,a)$ $\displaystyle=[b=a]$
$\displaystyle d(1,a)$ $\displaystyle=0$ $\displaystyle d(t\cdot r,a)$
$\displaystyle=d(t,a)\cdot r+[t\in N]\cdot d(r,a)$ $\displaystyle
d(t^{\ast},a)$ $\displaystyle=d(t,a)\cdot t^{\ast}$

The next propositions show that the Brzozowski derivative does indeed capture
a left-quotient syntactically. Firstly, if two rational languages $U$ and $V$
are equal, so should be their quotients $a^{-1}U=a^{-1}V$ for all
$a\in\Sigma$. Secondly, we expect that $a(a^{-1}U)\subseteq U$ for all
$a\in\Sigma$, and moreover, that $U=\bigcup_{a\in\Sigma}a(a^{-1}U)$.

###### Proposition 4.2.

The Brzozowski derivative preserves provable equality of terms.

$\forall t,r\in\text{Exp}:\ \vdash_{\mathbf{RA}}t=r\implies\left(\forall
a\in\Sigma:\ \vdash_{\mathbf{RA}}d(t,a)=d(r,a)\right).$

###### Proposition 4.3 (Fundamental Theorem).

If $t\in\text{Exp}$. Then

$\vdash t=[t\in N]+\sum_{a\in\Sigma}a\cdot d(t,a).$

The Brzozowski derivative together with the set $N$ of expressions having the
empty word property allows us to define the _deterministic Brzozowski
automaton_ $\mathcal{B}=(\text{Exp},d,N)$. We do not settle on an initial
state, but join it later depending on which language we would like the
Brzozowski automaton to accept. In fact, the next proposition shows that if we
choose $t\in\text{Exp}$ as initial state, then the Brzozowski automaton is
going to accept the language $\llbracket t\rrbracket$.

###### Proposition 4.4.

For all $t\in\text{Exp}$ we have $L(\mathcal{B},t)=\llbracket t\rrbracket$.

Unfortunately, the Brzozowski automaton is not necessarily a DFA. If we choose
$t\in\text{Exp}$ as initial state, it could happen that there are infinitely
many reachable states. To solve this we introduce an equivalence relation by
which we can quotient the Brzozowski automaton. We define
$\sim_{B}\subseteq\text{Exp}^{2}$ to be the least equivalence relation
satisfying:

$\displaystyle 1\cdot t$ $\displaystyle\sim_{B}t$ $\displaystyle 0\cdot t$
$\displaystyle\sim_{B}0$ $\displaystyle t$ $\displaystyle\sim_{B}t+t$
$\displaystyle t+r$ $\displaystyle\sim_{B}r+t$ $\displaystyle(t+r)+g$
$\displaystyle\sim_{B}t+(r+g).$

We write $\sim$ whenever this does not lead to confusion. Now we can quotient
the state space, but this also means that we have to modify the Brzozowski
derivative and our set of accepting states. This is done by defining the
derivative of an equivalence class to be the equivalence class of the
derivative, and to make an equivalence class accepting if one of its members
has the empty word property. The next lemma shows that this is well-defined.

###### Lemma 4.5.

The equivalence relation $\sim$ is compatible with the Brzozowski derivative
$d$ and with the predicate $N$, i.e. if $t,r\in\text{Exp}$ and $t\sim r$, then

  1. 1.

$t\in N\iff r\in N$ and

  2. 2.

$\forall a\in\Sigma:d(t,a)\sim d(r,a)$.

We let $\widehat{d}:{\text{Exp}/_{\sim}}\to(\text{Exp}/_{\sim})^{\Sigma}$ be
the map given by $\widehat{d}([t]_{\sim},a)=[d(t,a)]_{\sim}$ and define the
predicate $\widehat{N}\subseteq(\text{Exp}/_{\sim})^{2}$ by
$[t]_{\sim}\in\widehat{N}\iff t\in N$.

###### Corollary 4.6.

The derivative $\widehat{d}$ and the predicate $\widehat{N}$ are well-defined.

This concludes the construction of the quotiented automaton
$\widehat{\mathcal{B}}=(\text{Exp}/{\sim},\widehat{d},\widehat{N})$. The next
result shows that if we choose $[t]_{\sim}$ as initial state, then we obtain a
DFA which accepts $\llbracket t\rrbracket$.

###### Theorem 4.7.

For all $t\in\text{Exp}$, $L(\widehat{\mathcal{B}},[t]_{\sim})=\llbracket
t\rrbracket$ and the set of states reachable from $[t]_{\sim}$ is finite.

The next example shows that with minimal effort and using the Brzozowski
construction, we can quickly come up with a lasso automaton for a simple
rational lasso expression.

###### Example 4.8.

Let $\rho=(b(ab)^{\ast},ab^{\ast})$. Then
$(u,v)\in\llbracket\rho\rrbracket_{\circ}$ if and only if $u\in\llbracket
b(ab)^{\ast}\rrbracket$ and $v\in\llbracket ab^{\ast}\rrbracket$. So the idea
is to build one DFA for $b(ab)^{\ast}$ and one DFA for $ab^{\ast}$, which
correspond to the spoke and loop part of the lasso automaton, and then link
them. The construction of the DFAs is done using Brzozowski derivatives, which
yields the following DFAs:

$b(ab)^{\ast}$start$(ab)^{\ast}$$0$$0$$b^{\ast}$$ab^{\ast}$start$b$$a$$a$$b$$a,b$$a,b$$a$$b$$b$$a$

Note that we are allowed to transition from the first to the second DFA
immediately after we have read $u$, that is, when we have reached an accepting
state in the spoke DFA. In order to determine where to switch to, we think of
our spoke state as the initial state of the loop DFA. From any other state in
the spoke DFA (i.e. the non-accepting ones), attempting to transition just
leads to a dead state. In the final lasso automaton the initial state of the
second DFA is omitted as it is not reachable.

$b(ab)^{\ast}$start$(ab)^{\ast}$$0$$0$$b^{\ast}$$b$$a$$a,b$$a$$b$$b$$a$$a,b$$a,b$$a,b$$a$$b$

We turn this intuition into a formal construction, first defining the
derivatives and showing some of their properties, and then proving that the
lasso automaton we obtain accepts the desired language.

###### Definition 4.9.

Define the _spoke_ and _switch Brzozowski derivatives_
$d_{1}\colon\text{Exp}_{\circ}\to\text{Exp}_{\circ}^{\Sigma}$ and
$d_{2}\colon\text{Exp}_{\circ}\to\text{Exp}^{\Sigma}$ recursively on the
structure of rational lasso expressions as

$\displaystyle d_{1}(0,a)$ $\displaystyle=0$ $\displaystyle d_{2}(0,a)$
$\displaystyle=0$ $\displaystyle d_{1}(t^{\circ},a)$ $\displaystyle=0$
$\displaystyle d_{2}(t^{\circ},a)$ $\displaystyle=d(t,a)$ $\displaystyle
d_{1}(\rho+\sigma,a)$ $\displaystyle=d_{1}(\rho,a)+d_{1}(\sigma,a)$
$\displaystyle d_{2}(\rho+\sigma,a)$
$\displaystyle=d_{2}(\rho,a)+d_{2}(\sigma,a)$ $\displaystyle
d_{1}(r\cdot\rho,a)$ $\displaystyle=d(r,a)\cdot\rho+[r\in N]\cdot
d_{1}(\rho,a)$ $\displaystyle d_{2}(r\cdot\rho,a)$ $\displaystyle=[r\in
N]\cdot d_{2}(\rho,a)$

Analogously to the situation with the classical Brzozowski construction, we
can show that the additional derivatives preserve provable equality of terms.

###### Proposition 4.10.

Let $\rho,\sigma\in\text{Exp}_{\circ}$ with $\vdash_{\mathbf{LA}}\rho=\sigma$.
Then for all $a\in\Sigma$:

  1. 1.

$\vdash_{\mathbf{RA}}d_{2}(\rho,a)=d_{2}(\sigma,a)$ and

  2. 2.

$\vdash_{\mathbf{LA}}d_{1}(\rho,a)=d_{1}(\sigma,a)$.

###### Proof.

We need to check all the relevant equations from our theory and make sure that
it works for substitution. We only treat some of the equations from the theory
as this involves simple manipulations of equations. The checks for
substitution are readily verified and hence omitted.

For both derivatives we show the claim for the equations
$t\cdot(r\cdot\rho)=(t\cdot r)\cdot\rho$ and
$(t+r)^{\circ}=t^{\circ}+r^{\circ}$. When treating the first equation, we need
this additional fact:

$\vdash[t\in N]\cdot[r\in N]=[t\cdot r\in N].$

We start with the derivative $d_{1}$ and check the first equation:

$\displaystyle d_{1}(t\cdot(r\cdot\rho),a)$
$\displaystyle=d(t,a)\cdot(r\cdot\rho)+[t\in N]\cdot d_{1}(r\cdot\rho,a)$
$\displaystyle(\text{defn. $d_{1}$})$
$\displaystyle=d(t,a)\cdot(r\cdot\rho)+[t\in N]\cdot(d(r,a)\cdot\rho$
$\displaystyle\qquad+[r\in N]\cdot d_{1}(\rho,a))$ $\displaystyle(\text{defn.
$d_{1}$})$ $\displaystyle=d(t,a)\cdot(r\cdot\rho)+[t\in
N]\cdot(d(r,a)\cdot\rho)$ $\displaystyle\qquad+[t\in N]\cdot([r\in N]\cdot
d_{1}(\rho,a))$ $\displaystyle(\text{dist.})$ $\displaystyle=(d(t,a)\cdot
r)\cdot\rho+([t\in N]\cdot d(r,a))\cdot\rho$ $\displaystyle\qquad+([t\in
N]\cdot[r\in N])\cdot d_{1}(\rho,a)$ $\displaystyle(\text{mixed assoc.})$
$\displaystyle=\left(d(t,a)\cdot r+[t\in N]\cdot d(r,a)\right)\cdot\rho$
$\displaystyle\qquad+[t\cdot r\in N]\cdot d_{1}(\rho,a)$
$\displaystyle(\text{dist. \& fact})$ $\displaystyle=d(t\cdot
r,a)\cdot\rho+[t\cdot r\in N]\cdot d_{1}(\rho,a)$ $\displaystyle(\text{defn.
$d$})$ $\displaystyle=d_{1}((t\cdot r)\cdot\rho,a)$ $\displaystyle(\text{defn.
$d_{1}$})$

For the other equation we get

$d_{1}((t+r)^{\circ},a)=0=0+0=d_{1}(t^{\circ},a)+d_{1}(r^{\circ},a)=d_{1}(t^{\circ}+r^{\circ},a),$

using the definition of $d_{1}$ and $\vdash_{\mathbf{LA}}0+0=0$.

Next we turn to $d_{2}$. Again, for the first equation we have

$\displaystyle d_{2}(t\cdot(r\cdot\rho),a)$ $\displaystyle=[t\in N]\cdot
d_{2}(r\cdot\rho,a)$ $\displaystyle(\text{defn. $d_{2}$})$
$\displaystyle=[t\in N]\cdot\left([r\in N]\cdot d_{2}(\rho,a)\right)$
$\displaystyle(\text{defn. $d_{2}$})$ $\displaystyle=\left([t\in N]\cdot[r\in
N]\right)\cdot d_{2}(\rho,a)$ $\displaystyle(\text{mixed assoc.})$
$\displaystyle=[t\cdot r\in N]\cdot d_{2}(\rho,a)$
$\displaystyle(\text{fact})$ $\displaystyle=d_{2}((t\cdot r)\cdot\rho,a).$
$\displaystyle(\text{defn. $d_{2}$})$

Finally, for the second equation we obtain

$\displaystyle d_{2}((t+r)^{\circ},a)$ $\displaystyle=d(t+r,a)$
$\displaystyle(\text{defn. $d_{2}$})$ $\displaystyle=d(t,a)+d(r,a)$
$\displaystyle(\text{defn. $d$})$
$\displaystyle=d_{2}(t^{\circ},a)+d_{2}(r^{\circ},a)$
$\displaystyle(\text{defn. $d_{2}$})$
$\displaystyle=d_{2}(t^{\circ}+r^{\circ},a).$ $\displaystyle(\text{defn.
$d_{2}$})$

The other proofs are similar. ∎

Next we show a fundamental theorem. The two-sorted nature of lasso automata
becomes clearly visible with a rational lasso expression being decomposed in
terms of the two derivatives $d_{1}$ and $d_{2}$.

###### Proposition 4.11 (Fundamental Theorem).

Let $\rho\in\text{Exp}_{\circ}$. Then

$\vdash_{\mathbf{LA}}\rho=\left(\sum_{a\in\Sigma}a\cdot
d_{1}(\rho,a)\right)+\left(\sum_{a\in\Sigma}a\cdot
d_{2}(\rho,a)\right)^{\circ}.$

###### Proof.

We proceed by structural induction on rational lasso expressions. For the case
where $\rho=0$ we apply the definition of $d_{1}$ and $d_{2}$, and use the
fact that $0$ is an absorbing element.

$\sum_{a\in\Sigma}a\cdot d_{1}(0,a)+\left(\sum_{a\in\Sigma}a\cdot
d_{2}(0,a)\right)^{\circ}=\sum_{a}a\cdot 0+\left(\sum_{a}a\cdot
0\right)^{\circ}=0$

For the case $\rho=t^{0}$, we apply the definition of the derivatives, use the
fact that $0$ is an absorbing element, and use the Fundamental Theorem
(Proposition 4.3) for rational expressions with the fact that $t\not\in N$.

$\sum_{a\in\Sigma}a\cdot d_{1}(t^{\circ},a)+\left(\sum_{a\in\Sigma}a\cdot
d_{2}(t^{\circ},a)\right)^{\circ}=\sum_{a}a\cdot 0+\left(\sum_{a}a\cdot
d(t,a)\right)^{\circ}=t^{\circ}$

For the case of $\rho+\sigma$, we make use of the induction hypothesis,
distributivity, associativity, commutativity and the fact that $(-)^{\circ}$
distributes over sums.

$\displaystyle\phantom{km}\sum_{a\in\Sigma}a\cdot
d_{1}(\rho+\sigma,a)+\left(\sum_{a\in\Sigma}a\cdot
d_{2}(\rho+\sigma,a)\right)^{\circ}$ $\displaystyle=\sum_{a}a\cdot
d_{1}(\rho,a)+\sum_{a}a\cdot d_{1}(\sigma,a)+\left(\sum_{a}a\cdot
d_{2}(\rho,a)+\sum_{a}a\cdot d_{2}(\sigma,a)\right)^{\circ}$
$\displaystyle=\sum_{a}a\cdot d_{1}(\rho,a)+\sum_{a}a\cdot
d_{1}(\sigma,a)+\left(\sum_{a}a\cdot
d_{2}(\rho,a)\right)^{\circ}+\left(\sum_{a}a\cdot
d_{2}(\sigma,a)\right)^{\circ}$ $\displaystyle=\sum_{a}a\cdot
d_{1}(\rho,a)+\left(\sum_{a}a\cdot d_{2}(\rho,a)\right)^{\circ}+\sum_{a}a\cdot
d_{1}(\sigma,a)+\left(\sum_{a}a\cdot d_{2}(\sigma,a)\right)^{\circ}$
$\displaystyle=\rho+\sigma$

Finally, for the case $r\cdot\rho$ we use the Fundamental Theorem for rational
expressions (Proposition 4.3) on $r$, make use of the induction hypothesis,
distributivity, associativity, commutativity and the additional facts

$\vdash t\cdot[r\in N]=[r\in N]\cdot t\qquad\text{ and
}\qquad\vdash_{\mathbf{LA}}([r\in N]\cdot t)^{\circ}=[r\in N]\cdot t^{\circ}.$

This yields:

$\displaystyle\phantom{km}\sum_{a\in\Sigma}a\cdot
d_{1}(r\cdot\rho,a)+\left(\sum_{a\in\Sigma}a\cdot
d_{2}(r\cdot\rho,a)\right)^{\circ}$
$\displaystyle=\sum_{a}a\cdot(d(r,a)\cdot\rho+[r\in N]\cdot
d_{1}(\rho,a))+\left(\sum_{a}a\cdot[r\in N]\cdot d_{2}(\rho,a)\right)^{\circ}$
$\displaystyle=\sum_{a}a\cdot(d(r,a)\cdot\rho)+\sum_{a}a\cdot\left([r\in
N]\cdot d_{1}(\rho,a)\right)+\left(\sum_{a\in\Sigma}a\cdot[r\in N]\cdot
d_{2}(\rho,a)\right)^{\circ}$ $\displaystyle=\sum_{a}(a\cdot
d(r,a))\cdot\rho+[r\in N]\cdot\sum_{a}a\cdot d_{1}(\rho,a)+[r\in
N]\cdot\left(\sum_{a\in\Sigma}a\cdot d_{2}(\rho,a)\right)^{\circ}$
$\displaystyle=\left(\sum_{a}a\cdot d(r,a)\right)\cdot\rho+[r\in
N]\cdot\left(\sum_{a}a\cdot d_{1}(\rho,a)+\left(\sum_{a\in\Sigma}a\cdot
d_{2}(\rho,a)\right)^{\circ}\right)$ $\displaystyle=\left(\sum_{a}a\cdot
d(r,a)\right)\cdot\rho+[r\in N]\cdot\rho$
$\displaystyle=\left(\left(\sum_{a}a\cdot d(r,a)\right)+[r\in
N]\right)\cdot\rho$ $\displaystyle=r\cdot\rho\qed$

We call the lasso automaton
$\mathcal{C}=(\text{Exp}_{\circ},\text{Exp},d_{1},d_{2},d,N)$ the _Brzozowski
lasso automaton_. The loop states together with the Brzozowski derivative and
the accepting states forms the standard Brzozowski automaton $\mathcal{B}$, so
we can think of $\mathcal{C}$ as extending $\mathcal{B}$. Moreover, if we set
the initial state to be $\rho\in\text{Exp}_{\circ}$, then the lasso language
accepted by $\mathcal{C}$ is $\llbracket\rho\rrbracket_{\circ}$.

###### Proposition 4.12.

If $\rho\in\text{Exp}_{\circ}$, then
$L_{\circ}(\mathcal{C},\rho)=\llbracket\rho\rrbracket_{\circ}$.

###### Proof.

We proceed by induction on the length of the spoke word. For the base case
assume the spoke word to be the empty word, i.e. consider the lasso
$(\varepsilon,au)$. By using the Fundamental Theorem (Proposition 4.11) and
Soundness (Proposition 3.5) we get

$(\varepsilon,au)\in\llbracket\rho\rrbracket_{\circ}\iff(\varepsilon,au)\in\left\llbracket\sum_{a}a\cdot
d_{1}(\rho,a)+\left(\sum_{a}a\cdot
d_{2}(\rho,a)\right)^{\circ}\right\rrbracket_{\circ}.$

It follows that $au\in\left\llbracket a\cdot d_{2}(\rho,a)\right\rrbracket$
which is equivalent to $\varepsilon\in\llbracket
d(d_{2}(\rho,a),u)\rrbracket$, and in turn to $d(d_{2}(\rho,a),u)\in N$. By
the definition of acceptance this is the same as $(\varepsilon,au)\in
L_{\circ}(\mathcal{C},\rho)$. This establishes the base case. For the
induction step consider the lasso $(au,v)$. Again by using the Fundamental
Theorem and Soundness we get that

$(au,v)\in\llbracket\rho\rrbracket_{\circ}\iff(au,v)\in\left\llbracket\sum_{a}a\cdot
d_{1}(\rho,a)+\left(\sum_{a}a\cdot
d_{2}(\rho,a)\right)^{\circ}\right\rrbracket_{\circ}.$

By the definition of the semantics map this is the same as
$(au,v)\in\left\llbracket a\cdot d_{1}(\rho,a)\right\rrbracket_{\circ}$ which
in turn is equivalent to $(u,v)\in\left\llbracket
d_{1}(\rho,a)\right\rrbracket_{\circ}$. Using the induction hypothesis we get
$(u,v)\in L_{\circ}(\mathcal{C},d_{1}(\rho,a))$ which is equivalent to
$(au,v)\in L_{\circ}(\mathcal{C},\rho)$. ∎

The Brzozowski lasso automaton is not necessarily finite. The easiest fix to
this is to assume that our rational lasso expressions are disjunctive forms
(c.f. Proposition 3.7). To accommodate this assumption with regards to our
Brzozowski lasso automaton, we slightly adapt the definition of $d_{1}$ so
that $d_{1}(\rho,a)$ is again a disjunctive form for $a\in\Sigma$. This is
done by defining

$d_{1}(t\cdot s^{\circ},a):=d(t,a)\cdot s^{\circ}.$

It is important to point out that this does not jeopardise our earlier result
(Proposition 4.12). Indeed without this change we would have

$d_{1}(t\cdot s^{\circ},a)=d(t,a)\cdot s^{\circ}+[t\in N]\cdot
d(s^{\circ},a)=d(t,a)\cdot s^{\circ}+[t\in N]\cdot 0,$

which is provably equivalent to $d(t,a)\cdot s^{\circ}$. We ignore this
technicality in pursuit of a cleaner presentation.

It should also be remarked, that with these changes $d_{1}$ only acts on the
spoke expressions (where it acts just like a normal Brzozowski derivative),
$d_{2}$ acts on the loop expression to give a rational expression (provided
that the spoke expression has the empty word property) and finally $d$ acts on
the obtained rational expression. In this sense, we are really constructing
two DAs using Brzozowski derivatives and linking them appropriately with
$d_{2}$, as in Example 4.8.

In the remainder of this section, we quotient our Brzozowski lasso automaton
by a suitable equivalence relation which respects the derivatives, and such
that for any rational lasso expression, its set of successors is finite. Using
our assumption that rational lasso expressions are in a disjunctive form, the
definition makes use of the equivalence relation $\sim_{B}$ which we
introduced earlier as the least equivalence relation satisfying

$\displaystyle 1\cdot t$ $\displaystyle\sim_{B}t$ $\displaystyle 0\cdot t$
$\displaystyle\sim_{B}0$ $\displaystyle t$ $\displaystyle\sim_{B}t+t$
$\displaystyle t+r$ $\displaystyle\sim_{B}r+t$ $\displaystyle(t+r)+g$
$\displaystyle\sim_{B}t+(r+g).$

Using the equivalence relation $\sim_{B}$, we define
${\sim_{C}}\subseteq\text{Exp}_{\circ}^{2}$ to be the least equivalence
relation such that

$\sum_{i=1}^{n}t_{i}\cdot
r_{i}^{\circ}\sim_{C}\sum_{i=1}^{n}t^{\prime}_{i}\cdot(r^{\prime}_{i})^{\circ}\iff\forall\
1\leq i\leq n:t_{i}\sim_{B}t^{\prime}_{i}\text{ and }r_{i}=r^{\prime}_{i}.$

As with the standard Brzozowski derivative, we define our derivatives $d_{1}$
and $d_{2}$ now on equivalence classes and then show that this is well-
defined. Let $\widehat{d_{1}}$ and $\widehat{d_{2}}$ be the following maps:

$\displaystyle\widehat{d_{1}}:\text{Exp}_{\circ}/{\sim_{C}}$
$\displaystyle\longrightarrow(\text{Exp}_{\circ}/{\sim_{C}})^{\Sigma}$
$\displaystyle\widehat{d_{2}}:\text{Exp}_{\circ}/{\sim_{C}}$
$\displaystyle\longrightarrow(\text{Exp}/{\sim_{B}})^{\Sigma}$
$\displaystyle[\rho]_{\sim_{C}}$ $\displaystyle\longmapsto\lambda
a\in\Sigma.[d_{1}(\rho,a)]_{\sim_{C}}$ $\displaystyle\qquad[\rho]_{\sim_{C}}$
$\displaystyle\longmapsto\lambda a\in\Sigma.[d_{2}(\rho,a)]_{\sim_{B}}$

###### Proposition 4.13.

The maps $\widehat{d_{1}}$ and $\widehat{d_{2}}$ are well defined.

###### Proof.

Let $\sum_{i=1}^{n}t_{i}\cdot
s_{i}^{\circ}\sim_{C}\sum_{i=1}^{n}t^{\prime}_{i}\cdot(s^{\prime}_{i})^{\circ}$.
We have to show that their $d_{1}$ derivatives are in the same $\sim_{C}$
equivalence class, and that their $d_{2}$ derivatives are in the same
$\sim_{B}$ equivalence class. We start by taking their $d_{1}$ derivatives
with respect to some $a\in\Sigma$:

$d_{1}\left(\sum_{i=1}^{n}t_{i}\cdot
s_{i}^{\circ},a\right)=\sum_{i=1}^{n}d(t_{i},a)\cdot s_{i}^{\circ}\qquad\text{
and }\qquad
d_{1}\left(\sum_{i=1}^{n}t^{\prime}_{i}\cdot(s^{\prime}_{i})^{\circ},a\right)=\sum_{i=1}^{n}d(t^{\prime}_{i},a)\cdot(s^{\prime}_{i})^{\circ}.$

By our assumption and the definition of $\sim_{C}$, it follows that
$t_{i}\sim_{B}t^{\prime}_{i}$. Hence $d(t_{i},a)\sim_{B}d(t^{\prime}_{i},a)$
by Lemma 4.5. Furthermore, we also have $s_{i}=s^{\prime}_{i}$ and so

$d_{1}\left(\sum_{i=1}^{n}t_{i}\cdot
s_{i}^{\circ},a\right)\sim_{C}d_{1}\left(\sum_{i=1}^{n}t_{i}\cdot
s_{i}^{\circ},a\right),$

that is their $d_{1}$ derivatives are in the same $\sim_{C}$ equivalence
class. Next, we take the $d_{2}$ derivatives with respect to some
$a\in\Sigma$:

$d_{2}\left(\sum_{i=1}^{n}t_{i}\cdot
s_{i}^{\circ},a\right)=\sum_{i=1}[t_{i}\in N]\cdot d(s_{i},a)\qquad\text{ and
}\qquad
d_{2}\left(\sum_{i=1}^{n}t^{\prime}_{i}\cdot(s^{\prime}_{i})^{\circ},a\right)=\sum_{i=1}[t^{\prime}_{i}\in
N]\cdot d(s^{\prime}_{i},a).$

Again, by our assumption $t_{i}\sim_{B}t^{\prime}_{i}$ so that $[t_{i}\in
N]=[t^{\prime}_{i}\in N]$ by Lemma 4.5. Moreover,
$d(s_{i},a)=d(s^{\prime}_{i},a)$ follows from $s_{i}=s_{i}^{\prime}$, hence

$d_{2}\left(\sum_{i=1}^{n}t_{i}\cdot
s_{i}^{\circ},a\right)=d_{2}\left(\sum_{i=1}^{n}t_{i}^{\prime}\cdot(s_{i}^{\prime})^{\circ},a\right)$

and so their $d_{2}$ derivatives are in particular related by $\sim_{B}$. ∎

We obtain the lasso automaton
$\widehat{\mathcal{C}}=(\text{Exp}_{\circ}/{\sim_{C}},\text{Exp}/{\sim_{B}},\widehat{d_{1}},\widehat{d_{2}},\widehat{d},\widehat{N})$
by quotienting the lasso automaton $\mathcal{C}$ by $(\sim_{C},\sim_{B})$.

###### Theorem 4.14.

For all $\rho\in\text{Exp}_{\circ}$, where $\rho$ is a disjunctive form,
$L_{\circ}(\widehat{\mathcal{C}},[\rho]_{\sim_{C}})=\llbracket\rho\rrbracket_{\circ}$
and the set of states reachable from $[\rho]_{\sim_{C}}$ is finite.

###### Proof.

The claim that
$L_{\circ}(\widehat{\mathcal{C}},[\rho]_{\sim_{C}})=\llbracket\rho\rrbracket_{\circ}$
follows as $\sim_{C}$ is a congruence compatible with the structure of the
Brzozowski automaton, hence the map sending a state to its equivalence class
preserves the accepted language.

The fact that there are only finitely many reachable states from
$[\rho]_{\sim_{C}}$ follows from the definition of $\sim_{C}$. More precisely,
we defined it in terms of $\sim_{B}$ for which we already know that taking
Brzozowski derivatives leads to finitely many reachable states. The fact that
$\sim_{C}$ is given by equality on expressions underneath $(-)^{\circ}$ means
that they do not contribute anything. ∎

The following corollary is immediate.

###### Corollary 4.15.

Every rational lasso language is regular.

##  5 Regular Lasso Languages are Rational

The previous section gives us one direction of Kleene’s theorem for lasso
languages. We obtain the other direction by slightly modifying a result by
Calbrix et al., which is interesting in its own right as it gives insights
into the connection between $\Omega$-automata and nondeterministic Büchi
automata [4].

Calbrix et al. show how to build the rational $\omega$-language accepted by an
$\Omega$-automaton $\mathcal{A}$ from some rational languages defined on the
basis of $\mathcal{A}$ [4]. This shows that every regular $\omega$-language is
rational.

We first recall the results (Lemma 5.1 and Theorem 5.2) by [4] and then
continue with a similar result for lasso languages which shows that every
regular lasso language is rational. We begin with a technical lemma.

###### Lemma 5.1 ([4, Lemma 5]).

Let $U,V$ be regular languages such that $\varepsilon\not\in V$, $UV^{\ast}=U$
and $V^{+}=V$. Then for all $uv^{\omega}\in UV^{\omega}$, there exist
$u^{\prime}\in U$ and $v^{\prime}\in V$ such that
$uv^{\omega}=u^{\prime}v^{\prime\omega}$.

This fact is a simple application of the pigeonhole principle. Given an
ultimately periodic word $uv^{\omega}\in UV^{\omega}$, we can find
$u^{\prime}\in U$ and $v_{1},\ldots,v_{n},v_{n+1},\ldots,v_{n+m}\in V$ such
that $uv^{\omega}=u^{\prime}v_{1}\ldots v_{n}(v_{n+1}\ldots v_{n+m})^{\omega}$
using the pigeonhole principle. As $UV^{\ast}=U$ and $V^{+}=V$ it follows that
$u^{\prime}v_{1}\ldots v_{n}\in U$ and $v_{n+1}\ldots v_{n+m}\in V$. Hence the
lemma states that for suitable $U$ and $V$, if $uv^{\omega}$ is an arbitrary
ultimately periodic word in $UV^{\omega}$, we may instead use an identical
ultimately periodic word $u^{\prime}v^{\prime\omega}\in UV^{\omega}$ which on
top also satisfies the property that $u^{\prime}\in U$ and $v^{\prime}\in V$.
Calbrix et al. use this lemma to show Theorem 5.2 and we use it later in
Section 6 to prove Proposition 6.9.

###### Theorem 5.2 ([4]).

Let $\mathcal{A}=(X,Y,\overline{x},\delta_{1},\delta_{2},\delta_{3},F)$ be a
finite $\Omega$-automaton. For $x\in X$ and $y\in F$ we abbreviate

$\displaystyle S_{x}$
$\displaystyle=\\{u\in\Sigma^{\ast}\mid\delta_{1}(\overline{x},u)=x\\},$
$\displaystyle R_{x,y}$
$\displaystyle=\\{u\in\Sigma^{+}\mid\delta_{1}(x,u)=x\text{ and
}(\delta_{2}:\delta_{3})(x,u)=\delta_{3}(y,u)=y\\}.$

Then

$L_{\omega}(\mathcal{A})=\bigcup_{x\in X}\bigcup_{y\in F}S_{x}\cdot
R_{x,y}^{\omega}.$

The rational language $S_{x}$ consists of all words that lead from the initial
state $\overline{x}$ to $x$. As $R_{x,y}$ contains those words which at the
same time bring us from $x$ back to $x$ via $\delta_{1}$, from $x$ to $y$ via
$(\delta_{2}\mathop{:}\delta_{3})$ and from $y$ back to itself via
$\delta_{3}$, concatenating infinitely many such words traces paths which
intersect a final state infinitely often. Hence a saturated lasso automaton
can be seen as a nondeterministic Büchi automaton [5, Remark 21].

###### Corollary 5.3.

Every regular $\omega$-language is rational: for every finite
$\Omega$-automaton $\mathcal{A}$, one can construct a rational
$\omega$-expression $T$ such that $L_{\omega}(\mathcal{A})=\llbracket
T\rrbracket_{\omega}$.

###### Proof.

The languages $S_{x}$ and $R_{x,y}$ constructed in Theorem 5.2 are regular and
hence also rational. Therefore, we can find matching rational expressions
which allow us to define a suitable rational $\omega$-expression. ∎

In order to obtain a similar result for lasso languages, we slightly modify
the definition of $R_{x,y}$ from Theorem 5.2. This shows that every regular
lasso language is rational.

###### Proposition 5.4.

Let $\mathcal{A}=(X,Y,\overline{x},\delta_{1},\delta_{2},\delta_{3},F)$ be a
finite lasso automaton. For $x\in X$ and $y\in F$, let $S_{x}$ be defined as
in Theorem 5.2 and let

$R_{x,y}=\\{u\in\Sigma^{+}\mid(\delta_{2}\mathop{:}\delta_{3})(x,u)=y\\}.$

Then

$L_{\circ}(\mathcal{A})=\bigcup_{x\in X}\bigcup_{y\in F}S_{x}\cdot
R_{x,y}^{\circ}.$

###### Proof.

If $(u,v)\in L_{\circ}(\mathcal{A})$, then
$(\delta_{2}\mathop{:}\delta_{3})(\delta_{1}(\overline{x},u),v)\in F$. If we
choose $x=\delta_{1}(\overline{x},u)$ and
$y=(\delta_{2}\mathop{:}\delta_{3})(x,v)\in F$, then $(u,v)\in S_{x}\cdot
R_{x,y}^{\circ}$.

For the other inclusion, let $(u,v)\in S_{x}\cdot R_{x,y}^{\circ}$ for some
$x\in X$ and $y\in F$. By definition, we have $x=\delta_{1}(\overline{x},u)$
and $y=(\delta_{2}\mathop{:}\delta_{3})(x,v)$. Hence
$(\delta_{2}\mathop{:}\delta_{3})(\delta_{1}(\overline{x},u),v)\in F$ and
$(u,v)\in L_{\circ}(\mathcal{A})$. ∎

###### Example 5.5.

In this example we extract a rational lasso expression from the lasso
automaton in Example 4.8 reproduced below:

$0$start$1$$2$$4$$3$$b$$a$$a,b$$a$$b$$b$$a$$a,b$$a,b$$a,b$$a$$b$

Instead of using rational languages, we immediately use corresponding rational
expressions for the sake of simplicity. For each spoke state in $\\{0,1,2\\}$
we compute $S_{x}$, giving

$S_{0}=(ba)^{\ast},\qquad S_{1}=b(ab)^{\ast},\qquad
S_{2}=(ba)^{\ast}a(a+b)^{\ast}+b(ab)^{\ast}b(a+b)^{\ast}.$

Next, we compute $R_{x,y}$, which results in

$R_{0,3}=0,\qquad R_{1,3}=ab^{\ast},\qquad R_{2,3}=0.$

So the language accepted by the lasso automaton (which we call $\mathcal{A}$)
is:

$L_{\circ}(\mathcal{A})=(ba)^{\ast}0^{\circ}+b(ab)^{\ast}(ab^{\ast})^{\circ}+\left[(ba)^{\ast}a(a+b)^{\ast}+b(ab)^{\ast}b(a+b)^{\ast}\right]0^{\circ}.$

Note that this is provably equivalent to $b(ab)^{\ast}(ab^{\ast})^{\circ}$
which is exactly what we started out with.

###### Corollary 5.6.

Every regular lasso language is rational: for each finite lasso automaton
$\mathcal{A}$, one can construct a rational lasso expression $\rho$ such that
$L_{\circ}(\mathcal{A})=\llbracket\rho\rrbracket_{\circ}$.

###### Proof.

The proof is analogous to that of Corollary 5.3. ∎

###### Theorem 5.7.

A lasso language is regular if and only if it is rational.

###### Proof.

This theorem follows immediately from Corollary 4.15 and Corollary 5.6. ∎

##  6 Rational $\omega$\- and Lasso Expressions

Additionally to the concepts already introduced in the preliminaries, we make
use of the following definitions and terminology throughout this section. As
$\sim_{\gamma}$ is an equivalence relation, we obtain a canonical map
$\varphi:\Sigma^{\ast+}\to\Sigma^{\ast+}/{\sim_{\gamma}}$ which sends a lasso
$(u,v)$ to its $\gamma$-equivalence class $[(u,v)]_{\gamma}$. A subset
$L\subseteq\Sigma^{\ast+}$ is called _$\sim_{\gamma}$ -saturated_ (or simply
_saturated_) if $L=\varphi^{-1}(K)$ for some
$K\subseteq\Sigma^{\ast+}/{\sim_{\gamma}}$. From the fact that
$(u,v)\sim_{\gamma}(u^{\prime},v^{\prime})\iff
uv^{\omega}=u^{\prime}v^{\prime\omega}$ it follows that
$\Sigma^{\ast+}/{\sim_{\gamma}}$ is isomorphic to $\Sigma^{\text{up}}$ through
the map $[(u,v)]_{\gamma}\mapsto uv^{\omega}$. We therefore make no
distinction between $\Sigma^{\ast+}/{\sim_{\gamma}}$ and $\Sigma^{\text{up}}$,
nor between $[(u,v)]_{\gamma}$ and $uv^{\omega}$.

In the first part of the section, we present some basic results on saturation
and show that a lasso language is saturated if and only if it is closed under
$\gamma$-expansion and $\gamma$-reduction. Of particular interest are those
rational lasso languages whose semantics is saturated, as the image of such a
language under $\varphi$ corresponds precisely to the ultimately periodic
fragment of a rational $\omega$-language. We lift this relationship between
languages to that of expressions by saying that a rational lasso expression
$\tau$ represents a rational $\omega$-expression $T$, if
$\llbracket\tau\rrbracket_{\circ}$ is saturated and its image under $\varphi$
is the ultimately periodic fragment of $\llbracket T\rrbracket_{\omega}$. The
question we then try to answer is, given $T$, can we syntactically build
$\tau$? We show that this is indeed possible under the assumption that we have
two additional operations on rational expressions. Our approach consists of
first introducing a weaker notion, that of weak representability, which drops
the saturation requirement. From $T$ we then construct in a first step a weak
representation $\tau$ whose semantics is not saturated but is only closed
under $\gamma$-expansion. This first construction makes use of the sequential
splitting relation, which to each rational expression $t$ associates a finite
set of pairs of rational expressions called splits, intuitively corresponding
to all the ways words in the semantics of $t$ can be split into two. We
subsequently modify our weak representation $\tau$ to obtain a rational lasso
expression which is also closed under $\gamma$-reduction and hence saturated.
This part of the construction makes use of two additional operations on
rational expressions, intersection and root, which both preserve rationality.

The use of the sequential splitting relation and the rational operations
intersection and root has to do with the fact that we have to capture the
rewrite rules $\gamma_{1}$ and $\gamma_{2}$ on the level of expressions, that
is syntactically.

The next lemma introduces several equivalent definitions of saturation using
the canonical map $\varphi$ which we described above. The most interesting for
our purposes is the last one, which describes saturation in terms of the
rewrite rules $\to_{\gamma_{1}}$ and $\to_{\gamma_{2}}$.

###### Lemma 6.1.

Let $L\subseteq\Sigma^{\ast+}$. The following are equivalent definitions of
$\sim_{\gamma}$-saturation:

  1. 1.

$L=\varphi^{-1}(K)$ for some $K\subseteq\Sigma^{\ast+}/{\sim_{\gamma}}$.

  2. 2.

$L$ is the union of $\sim_{\gamma}$-equivalence classes.

  3. 3.

$L=\varphi^{-1}(\varphi(L))$.

  4. 4.

Let

$\displaystyle L^{\uparrow}$
$\displaystyle=\\{(u^{\prime},v^{\prime})\in\Sigma^{\ast+}\mid\exists
i\in\\{1,2\\},\exists(u,v)\in
L:(u^{\prime},v^{\prime})\to_{\gamma_{i}}(u,v)\\},$ $\displaystyle
L^{\downarrow}$
$\displaystyle=\\{(u^{\prime},v^{\prime})\in\Sigma^{\ast+}\mid\exists
i\in\\{1,2\\},\exists(u,v)\in
L:(u,v)\to_{\gamma_{i}}(u^{\prime},v^{\prime})\\}.$

Then $L$ is saturated if and only if $L=L^{\uparrow}=L^{\downarrow}$.

###### Proof.

Of these four, the first three definitions are standard. The last definition
of saturation states that if $L$ is closed under $\gamma$-expansion
($L=L^{\uparrow}$) and under $\gamma$-reduction $L=L^{\downarrow}$, then $L$
is saturated. To see why this is the case assume that
$L=L^{\uparrow}=L^{\downarrow}$, let $(u,v)\in L$ and
$(u^{\prime},v^{\prime})\sim_{\gamma}(u,v)$. If we show that
$(u^{\prime},v^{\prime})\in L$ it follows immediately that $L$ is a union of
equivalence classes. From $(u,v)\sim_{\gamma}(u^{\prime},v^{\prime})$ it
follows that the two lassos reduce to the same normal form
$(u^{\prime\prime},v^{\prime\prime})$. As $L$ is closed under
$\gamma$-reduction and $(u,v)\to_{\gamma}(u^{\prime\prime},v^{\prime\prime})$,
$(u^{\prime\prime},v^{\prime\prime})\in L$. Next as $L$ is also closed under
$\gamma$-expansion and
$(u^{\prime},v^{\prime})\to_{\gamma}(u^{\prime\prime},v^{\prime\prime})$,
$(u^{\prime},v^{\prime})\in L$ as required. Hence $L$ is saturated. ∎

We remind again that we make no distinction between
$\Sigma^{\ast+}/{\sim_{\gamma}}$ and $\Sigma^{\text{up}}$ as they are
isomorphic so that we are treating $\varphi$ as though its type was
$\varphi:\Sigma^{\ast+}\to\Sigma^{\text{up}}$.

###### Definition 6.2.

For a rational lasso expression $\tau\in\text{Exp}_{\circ}$ and a rational
$\omega$-expression $T\in\text{Exp}_{\omega}$,

  1. 1.

$\tau$ _weakly represents_ $T$ if
$\varphi\left(\llbracket\tau\rrbracket_{\circ}\right)=\text{UP}(\llbracket
T\rrbracket_{\omega})$,

  2. 2.

$\tau$ _represents_ $T$ if
$\llbracket\tau\rrbracket_{\circ}=\varphi^{-1}\left(\text{UP}(\llbracket
T\rrbracket_{\omega})\right)$.

###### Example 6.3.

Let $T=(a+b)^{\ast}a^{\omega}$. Then $((a+b)^{\ast},a)$ constitutes a weak
representation but not a representation of $T$. This is seen from the
following facts:

  1. 1.

$\varphi\left(\llbracket((a+b)^{\ast},a)\rrbracket_{\circ}\right)=\varphi(\\{(u,a)\mid
u\in\Sigma^{\ast}\\})=\\{ua^{\omega}\mid
u\in\Sigma^{\ast}\\}=\text{UP}(\llbracket T\rrbracket_{\omega})$,

  2. 2.

$\varphi(\varepsilon,aa)=a^{\omega}\in\text{UP}(\llbracket
T\rrbracket_{\omega})$ but
$(\varepsilon,aa)\not\in\llbracket((a+b)^{\ast},a)\rrbracket_{\circ}$.

###### Remark 6.4.

If $\tau$ represents $T$ it also weakly represents $T$ as $\varphi$ is
surjective, i.e. $\varphi\circ\varphi^{-1}=\text{id}$. Conversely, if $\tau$
weakly represents $T$, then it represents $T$ if and only if
$\llbracket\tau\rrbracket_{\circ}=\varphi^{-1}(\varphi(\llbracket\tau\rrbracket_{\circ}))$,
that is if and only if $\llbracket\tau\rrbracket_{\circ}$ is
$\sim_{\gamma}$-saturated. In the previous example, $((a+b)^{\ast},a^{+})$ is
a weak representation of $T$ and moreover its semantics is
$\sim_{\gamma}$-saturated, hence it is a representation of $T$.

As discussed at the start of the section, we proceed by first constructing a
weak representation whose semantics is closed under $\gamma$-expansion. This
means we want to syntactically mimic the following directions of rules
$\gamma_{1}$ and $\gamma_{2}$ :

$\displaystyle(u,vw)$ $\displaystyle\to(uv,wv)$ $\displaystyle(u,v)$
$\displaystyle\to(u,v^{k})\quad(k\geq 1)$

For the first expansion, given a lasso $(u,v)$ we may split $v$ into two words
$v_{1}$ and $v_{2}$ and obtain the new lasso $(uv_{1},v_{2}v_{1})$. For the
second one, given a lasso $(u,v)$ we may choose arbitrary $k\geq 1$ and obtain
the new lasso $(u,v^{k})$. To mimic the first expansion, we need to be able to
split rational expressions into two rational expressions. Then given a
rational lasso expression $(t,r)$ (recall that we use $(t,r)$ to mean $t\cdot
r^{\circ}$), we can split $r$ into two rational expressions $r_{1}$ and
$r_{2}$ and obtain a new rational lasso expression $(tr_{1},r_{2}r_{1})$. For
the second expansion, we can use the Kleene plus to go from $(t,r)$ to
$(t,r^{+})$, taking care of the arbitrary $k\geq 1$.

Hence, in order to close the semantics under $\gamma$-expansion, whenever we
add a term $(t,r)$, we also want to add $(tr_{1},r_{2}r_{1})$ for all possible
splits of $r$, and additionally, we also want to apply the Kleene plus. We now
formally define the sequential splitting relation and show some of its
properties which are needed to show that our first construction yields a weak
representation.

###### Definition 6.5 ([7]).

Let $\nabla:\text{Exp}\to 2^{\text{Exp}\times\text{Exp}}$ be defined
recursively:

$\displaystyle\nabla(0)$ $\displaystyle=\emptyset$ $\displaystyle\nabla(1)$
$\displaystyle=\\{(1,1)\\}$ $\displaystyle\nabla(a)$
$\displaystyle=\\{(1,a),(a,1)\\}$
$\nabla(t+r)=\nabla(t)\cup\nabla(r)\qquad\qquad\qquad\nabla(t^{\ast})=\\{(t^{\ast}\cdot
t_{0},t_{1}\cdot
t^{\ast})\mid(t_{0},t_{1})\in\nabla(t)\\}\cup\\{(1,1),(t^{\ast}\cdot t,1)\\}$

test

$\nabla(t\cdot r)=\\{(t_{0},t_{1}\cdot
r)\mid(t_{0},t_{1})\in\nabla(t)\\}\cup\\{(t\cdot
r_{0},r_{1})\mid(r_{0},r_{1})\in\nabla(r)\\}$

We write $\nabla_{t}$ for $\nabla(t)$ and call $\nabla_{t}$ the _sequential
splitting relation of $t$_.

The following lemma establishes some properties of the splitting relation, of
which points $1.$ and $2.$ are taken from [7].

###### Lemma 6.6.

Let $t\in\text{Exp}$. The sequential splitting relation $\nabla_{t}$
satisfies:

  1. 1.

$|\nabla_{t}|$ is finite and $\forall(t_{0},t_{1})\in\nabla_{t}\colon
t_{0}\cdot t_{1}\leq t$,

  2. 2.

if $u\cdot v\in\llbracket t\rrbracket$, then there is a split
$(t_{0},t_{1})\in\nabla_{t}$ such that $u\in\llbracket t_{0}\rrbracket$ and
$v\in\llbracket t_{1}\rrbracket$,

  3. 3.

if $(t_{0},t_{1})\in\nabla_{t}$ and $(r_{0},r_{1})\in\nabla_{t_{1}}$, then
there exists $(s_{0},s_{1})\in\nabla_{t}$ such that $t_{0}\cdot r_{0}\leq
s_{0}$ and $r_{1}\leq s_{1}$.

###### Proof.

The first two items follow by [7], so we only focus on the third item, which
we show by structural induction on rational expressions. For $t=0$,
$\nabla_{0}=\emptyset$ and so it trivially holds. For $t=1$,
$\nabla_{1}=\\{(1,1)\\}$ and so there is only one choice for $(t_{0},t_{1})$
and $(r_{0},r_{1})$, namely the pair $(1,1)$. As $1\cdot 1\leq 1$ and $1\leq
1$, we are done. For $t=a$, there are three cases. First, let
$(t_{0},t_{1})=(a,1)$, then $(r_{0},r_{1})=(1,1)$ and we have $a\cdot 1\leq a$
and $1\leq 1$. For the other two cases, let $(t_{0},t_{1})=(1,a)$. If
$(r_{0},r_{1})=(1,a)$, then we are done as $1\cdot 1\leq 1$ and $a\leq a$. On
the other hand, for $(r_{0},r_{1})=(a,1)$ we have $1\cdot a\leq a$ and $1\leq
1$. This covers all the base cases.

For the induction steps, we start with $t\cdot r$. There are two cases two
consider, the first split can either be $(t_{0},t_{1}\cdot r)$ or $(t\cdot
r_{0},r_{1})$. For the case $(t_{0},t_{1}\cdot r)$, there are again two
subcases, namely the splits $(t_{10},t_{11}\cdot r)$ and $(t_{1}\cdot
r_{0},r_{1})$ in $\nabla_{t_{1}\cdot r}$. For the first subcase, we know that
$(t_{10},t_{11})\in\nabla_{t_{1}}$, so by the induction hypothesis, there
exists a split $(s_{0},s_{1})\in\nabla_{t}$ such that $t_{0}\cdot t_{10}\leq
s_{0}$ and $t_{11}\leq s_{1}$. It follows that $(s_{0},s_{1}\cdot
r)\in\nabla_{t\cdot r}$ is a suitable candidate as $t_{0}\cdot t_{10}\leq
s_{0}$ and $t_{11}\cdot r\leq s_{1}\cdot r$. For the second subcase, we have
$(r_{0},r_{1})\in\nabla_{r}$, hence $(t\cdot r_{0},r_{1})\in\nabla_{t\cdot r}$
works as $t_{0}\cdot t_{1}\cdot r_{0}\leq t\cdot r_{0}$ and $r_{1}\leq r_{1}$.
Finally, for the case $(t\cdot r_{0},r_{1})$, let
$(r_{10},r_{11})\in\nabla_{r_{1}}$. Then, by the induction hypothesis, there
exists a split $(s_{0},s_{1})\in\nabla_{r}$ with $r_{0}\cdot r_{10}\leq s_{0}$
and $r_{11}\leq s_{1}$. Our candidate is $(t\cdot s_{0},s_{1})$ which works as
$t\cdot r_{0}\cdot r_{10}\leq t\cdot s_{0}$ and $r_{11}\leq s_{1}$.

The next induction step is $t_{0}+t_{1}$. Let
$(t,t^{\prime})\in\nabla_{t_{0}+t_{1}}$, then
$(t,t^{\prime})\in\nabla_{t_{i}}$ for some $i\in\\{0,1\\}$. Next, take
$(r_{0},r_{1})\in\nabla_{t^{\prime}}$. By the induction hypothesis we find
$(s_{0},s_{1})\in\nabla_{t_{i}}$ such that $t\cdot r_{0}\leq s_{0}$ and
$r_{1}\leq s_{1}$. As $(s_{0},s_{1})\in\nabla_{t_{i}}$, we also have
$(s_{0},s_{1})\in\nabla_{t_{0}+t_{1}}$. Choosing $(s_{0},s_{1})$ suffices to
satisfy the claim.

For the last case, we consider the expression $t^{\ast}$. If we consider
$(1,1)\in\nabla_{t^{\ast}}$, then this is taken care of by one of the previous
points. A similar argument also suffices for $(t^{\ast}\cdot
t,1)\in\nabla_{t^{\ast}}$. For the other case, let $(t^{\ast}\cdot
t_{0},t_{1}\cdot t^{\ast})\in\nabla_{t^{\ast}}$ where
$(t_{0},t_{1})\in\nabla_{t}$. There are four cases, as the splits in
$\nabla_{t_{1}\cdot t^{\ast}}$ are either of the form $(t_{1}\cdot 1,1)$,
$(t_{1}\cdot t^{\ast}\cdot t,1)$, $(t_{1}\cdot t^{\ast}\cdot r_{0},r_{1}\cdot
t^{\ast})$ (with $(r_{0},r_{1})\in\nabla_{t}$) or $(t_{10},t_{11}\cdot
t^{\ast})$ (with $(t_{10},t_{11})\in\nabla_{t_{1}}$). For the first case,
consider $(t^{\ast}\cdot t,1)\in\nabla_{t^{\ast}}$. Then $t^{\ast}\cdot
t_{0}\cdot t_{1}\cdot 1\leq t^{\ast}\cdot t$ and $1\leq 1$ as required. For
the second case consider again $(t^{\ast}\cdot t,1)\in\nabla_{t^{\ast}}$ for
which we have $t^{\ast}\cdot t_{0}\cdot t_{1}\cdot t^{\ast}\cdot t\leq
t^{\ast}\cdot t$ and $1\leq 1$ satisfying the requirement. For the third case
we choose the split $(t^{\ast}\cdot r_{0},r_{1}\cdot
t^{\ast})\in\nabla_{t^{\ast}}$ as $t^{\ast}\cdot t_{0}\cdot t_{1}\cdot
t^{\ast}\cdot r_{0}\leq t^{\ast}\cdot r_{0}$ and $r_{1}\cdot t^{\ast}\leq
r_{1}\cdot t^{\ast}$. Finally, for the last case we find by the induction
hypothesis a split $(r_{0},r_{1})\in\nabla_{t}$ with $t_{0}\cdot t_{10}\leq
r_{0}$ and $t_{11}\leq r_{1}$ for which we then have $t^{\ast}\cdot t_{0}\cdot
t_{10}\leq t^{\ast}\cdot r_{0}$ and $t_{11}\cdot t^{\ast}\leq r_{1}\cdot
t^{\ast}$ with $(t^{\ast}\cdot r_{0},r_{1}\cdot t^{\ast})\in\nabla_{t^{\ast}}$
as desired. ∎

###### Example 6.7.

For this example we explore the sequential splitting relation of a simple
rational expression and briefly touch on the different properties outlined in
Lemma 6.6. Let $t=b(a+b^{\ast})$. Then

$\nabla_{t}=\\{(1,b(a+b^{\ast})),(b,1(a+b^{\ast})),(b1,a),(ba,1),(bb^{\ast}1,bb^{\ast}),(bb^{\ast}b,1b^{\ast}),(b1,1)\\}.$

If we choose a word in $\llbracket t\rrbracket$, say $bb\cdot b$, then we can
find a corresponding split, in this case $(bb^{\ast}b,1b^{\ast})$ for example.
Moreover, if we choose any split in $\nabla_{t}$, say
$(bb^{\ast}b,1b^{\ast})$, and take any split in $\nabla_{1b^{\ast}}$, say
$(1b^{\ast}1,bb^{\ast})$, then we can find a split
$(t_{0},t_{1})\in\nabla_{t}$ such that $bb^{\ast}b1b^{\ast}1\leq t_{0}$ and
$bb^{\ast}\leq t_{1}$, namely $(bb^{\ast}1,bb^{\ast})$.

With the sequential splitting relation at hand, we define the map $h$ which
takes a rational $\omega$-expression and returns a rational lasso expression
which is weakly representing. The definition of $h$ makes use of the
sequential splitting relation and the Kleene plus in the definition of
$h(t^{\omega})$. Instead of just mapping $t^{\omega}$ to $(1,t)$ (i.e.
$t^{\circ}$), we go over every possible way of splitting $t$ into $t_{0}$ and
$t_{1}$ and make sure to add $(t_{0},t_{1}t_{0})$. Additionally, we also
incorporate the Kleene plus, which appears as a Kleene star in the definition.

###### Definition 6.8.

Let $h:\text{Exp}_{\omega}\to\text{Exp}_{\circ}$ be defined as

$\displaystyle h(0)$ $\displaystyle=0$ $\displaystyle h(t^{\omega})$
$\displaystyle=\sum_{(t_{0},t_{1})\in\nabla_{t}}(t^{\ast}\cdot
t_{0},t_{1}\cdot t^{\ast}\cdot t_{0})$ $\displaystyle h(T_{1}+T_{2})$
$\displaystyle=h(T_{1})+h(T_{2})$ $\displaystyle h(t\cdot T)$
$\displaystyle=t\cdot h(T)$

Rational lasso expressions can only contain finite sums, so it is crucial in
the definition of $h(t^{\omega})$ that $|\nabla_{t}|$ is finite (Lemma 6.6).
The next steps are to show that $h(T)$ weakly represents $T$ and that its
semantics is closed under $\gamma$-expansion. The proof that $h(T)$ weakly
represents $T$ relies on Lemma 5.1 from Section 5.

###### Proposition 6.9.

Let $T\in\text{Exp}_{\omega}$. Then $h(T)$ weakly represents $T$.

###### Proof.

This is shown by structural induction on rational $\omega$-expressions. The
case $T=0$ is trivial. For $T=t^{\omega}$, let first
$uv^{\omega}\in\text{UP}(\llbracket T\rrbracket_{\omega})$. Then

$uv^{\omega}\in\llbracket t\rrbracket^{\ast}(\llbracket
t\rrbracket^{+})^{\omega}$

and by Lemma 5.1 there exist $u^{\prime},v^{\prime}$ with
$uv^{\omega}=u^{\prime}v^{\prime\omega}$, $u^{\prime}\in\llbracket
t\rrbracket^{\ast}$ and $v^{\prime}\in\llbracket t\rrbracket^{+}$. As
$v^{\prime}\in\llbracket t\rrbracket^{+}$ we can find $v_{1}\in\llbracket
t\rrbracket$ and $w\in\llbracket t\rrbracket^{\ast}$ with $v^{\prime}=v_{1}w$.
Now $v_{1}=\varepsilon\cdot v_{1}$ gives rise to a split
$(t_{0},t_{1})\in\nabla_{t}$ with $\varepsilon\in\llbracket t_{0}\rrbracket$
and $v_{1}\in\llbracket t_{1}\rrbracket$. It is quickly verified that

$(u^{\prime},v^{\prime})=(u^{\prime}\cdot\varepsilon,v_{1}\cdot
w\cdot\varepsilon)\in\llbracket(t^{\ast}t_{0},t_{1}t^{\ast}t_{0})\rrbracket_{\circ}\subseteq\llbracket
h(t^{\omega})\rrbracket_{\circ}.$

Hence $uv^{\omega}=u^{\prime}v^{\prime\omega}\in f[\llbracket
h(t^{\omega})\rrbracket_{\circ}]$. For the other direction, let
$(u,v)\in\llbracket h(t^{\omega})\rrbracket_{\circ}$. Then there exists a
split $(t_{0},t_{1})\in\nabla_{t}$ with $u\in\llbracket
t^{\ast}t_{0}\rrbracket$ and $v\in\llbracket t_{1}t^{\ast}t_{0}\rrbracket$.
Now

$\llbracket t^{\ast}t_{0}\rrbracket\cdot(\llbracket
t_{1}t^{\ast}t_{0}\rrbracket)^{\omega}=\llbracket
t^{\ast}t_{0}t_{1}\rrbracket\cdot(\llbracket
t^{\ast}t_{0}t_{1}\rrbracket)^{\omega}\subseteq\llbracket
t^{\omega}\rrbracket_{\omega},$

hence $f(u,v)=uv^{\omega}\in\llbracket t^{\omega}\rrbracket_{\omega}$.

For the induction steps, we first consider the case $T_{1}+T_{2}$. For the
right to left inclusion, let $uv^{\omega}\in\llbracket
T_{1}+T_{2}\rrbracket_{\omega}$. Then $uv^{\omega}\in\llbracket
T_{i}\rrbracket_{\omega}$ for $i\in\\{1,2\\}$. By the induction hypothesis,
there exists some $(u^{\prime},v^{\prime})\in\llbracket
h(T_{i})\rrbracket_{\circ}$ with $(u,v)\sim_{\gamma}(u^{\prime},v^{\prime})$.
Then

$(u^{\prime},v^{\prime})\in\llbracket h(T_{1})\rrbracket\cup\llbracket
h(T_{2})\rrbracket_{\circ}=\llbracket
h(T_{1})+h(T_{2})\rrbracket_{\circ}=\llbracket
h(T_{1}+T_{2})\rrbracket_{\circ}$

as required. For the other inclusion, let $(u,v)\in\llbracket
h(T_{1}+T_{2})\rrbracket_{\circ}$, then $(u,v)\in\llbracket
h(T_{i})\rrbracket_{\circ}$ for some $i\in\\{1,2\\}$. By the induction
hypothesis, $uv^{\omega}\in\llbracket
T_{i}\rrbracket_{\omega}\subseteq\llbracket T_{1}+T_{2}\rrbracket_{\omega}$.

The last case is that of $t\cdot T$. For the right to left inclusion, take
$u_{0}u_{1}v^{\omega}\in\llbracket t\cdot T\rrbracket_{\omega}$ where
$u_{0}\in\llbracket t\rrbracket$ and $u_{1}v^{\omega}\in\llbracket
T\rrbracket_{\omega}$. By the induction hypothesis, there exists
$(u^{\prime},v^{\prime})\in\llbracket h(T)\rrbracket_{\circ}$ such that
$uv^{\omega}=u^{\prime}v^{\prime\omega}$. It follows that

$(u_{0}u^{\prime},v^{\prime})\in\llbracket t\cdot
h(T)\rrbracket_{\circ}=\llbracket h(t\cdot T)\rrbracket_{\circ}$

and moreover, $u_{0}u^{\prime}v^{\prime\omega}=u_{0}u_{1}v^{\omega}$ and we
are done. For the other inclusion, let $(u_{0}u_{1},v)\in\llbracket h(t\cdot
T)\rrbracket_{\circ}$, where $u_{0}\in\llbracket t\rrbracket$ and
$(u_{1},v)\in\llbracket h(T)\rrbracket_{\circ}$. By the induction hypothesis,
$u_{1}v^{\omega}\in\llbracket T\rrbracket_{\omega}$ and so
$u_{0}u_{1}v^{\omega}\in\llbracket t\cdot T\rrbracket_{\omega}$ which
concludes the proof. ∎

Showing that the semantics of $h(T)$ is closed under $\gamma$-expansion relies
crucially on some of the properties of the sequential splitting relation, in
particular on Lemma 6.6.3.

###### Proposition 6.10.

Let $T\in\text{Exp}_{\omega}$. Then $\llbracket h(T)\rrbracket_{\circ}$ is
closed under $\gamma$-expansion.

###### Proof.

We proceed by structural induction on rational $\omega$-expressions. The first
base case $T=0$ is trivial as $\llbracket h(0)\rrbracket_{\circ}=\emptyset$.
For the second, $T=t^{\omega}$. We show that $\llbracket
h(t^{\omega})\rrbracket_{\circ}$ is closed under $\gamma_{1}$\- and
$\gamma_{2}$-expansion. The result then follows as these commute. For
$\gamma_{1}$-expansion, let $(ua,va)\to_{\gamma_{1}}(u,av)$ and
$(u,av)\in\llbracket h(t^{\omega})\rrbracket_{\circ}$. Then there exists a
split $(t_{0},t_{1})\in\nabla_{t}$ such that $u\in\llbracket t^{\ast}\cdot
t_{0}\rrbracket$ and $av\in\llbracket t_{1}\cdot t^{\ast}\cdot
t_{0}\rrbracket$. Hence we can find $v_{1},\ldots,v_{k}\in\Sigma^{\ast}$ with
$v_{1}\in\llbracket t_{1}\rrbracket$, $v_{2},\ldots,v_{k-1}\in\llbracket
t^{\ast}\rrbracket$, $v_{k}\in\llbracket t_{0}\rrbracket$ and
$v_{1}v_{2}\ldots v_{k}=av$.

We need to distinguish three subcases:

  1. 1.

If $v_{1}\not=\varepsilon$, then $v_{1}=av_{1}^{\prime}$ and this induces a
split $(r_{0},r_{1})\in\nabla_{t_{1}}$, where $a\in\llbracket r_{0}\rrbracket$
and $v_{1}^{\prime}\in\llbracket r_{1}\rrbracket$. By Lemma 6.6.3, there
exists a split $(s_{0},s_{1})\in\nabla_{t}$ such that $t_{0}\cdot r_{0}\leq
s_{0}$ and $r_{1}\leq s_{1}$. We now have that

$ua\in\llbracket t^{\ast}\cdot t_{0}\cdot r_{0}\rrbracket\subseteq\llbracket
t^{\ast}\cdot s_{0}\rrbracket\qquad\text{ and }\qquad va\in\llbracket
r_{1}\cdot t^{\ast}\cdot t_{0}\cdot r_{0}\rrbracket\subseteq\llbracket
s_{1}\cdot t^{\ast}\cdot s_{0}\rrbracket.$

Hence $(ua,va)\in\llbracket h(t^{\omega})\rrbracket_{\circ}$.

  2. 2.

If $v_{1}=\varepsilon$ and $k=2$, we have that $v_{2}=av$, and hence a split
$(r_{0},r_{1})\in\nabla_{t_{0}}$ where $a\in\llbracket r_{0}\rrbracket$ and
$v\in\llbracket r_{1}\rrbracket$. Moreover, as $v_{1}=\varepsilon$, it follows
that $1\leq t_{1}$ and so $t_{0}=t_{0}\cdot 1\leq t_{0}\cdot t_{1}\leq t$.
Thus

$ua\in\llbracket t^{\ast}\cdot t_{0}\cdot r_{0}\rrbracket\subseteq\llbracket
t^{\ast}\cdot e\cdot r_{0}\rrbracket\subseteq\llbracket t^{\ast}\cdot
r_{0}\rrbracket\qquad\text{ and }\qquad va\in\llbracket r_{1}\cdot
r_{0}\rrbracket\subseteq\llbracket r_{1}\cdot t^{\ast}\cdot r_{0}\rrbracket.$

Hence $(ua,va)\in\llbracket h(t^{\omega})\rrbracket_{\circ}$.

  3. 3.

If $v_{1}=\varepsilon$ and $k>2$, then $v_{2}=av_{2}^{\prime}$ as
$\varepsilon\not\in\llbracket t\rrbracket$. This gives rise to a split
$(r_{0},r_{1})\in\nabla_{t}$ with $a\in\llbracket r_{0}\rrbracket$ and
$v_{2}^{\prime}\in\llbracket r_{1}\rrbracket$. As in the previous case, we
have $t_{0}\leq t$ as $v_{1}=\varepsilon$. This gives us that

$\displaystyle ua$ $\displaystyle\in\llbracket t^{\ast}\cdot t_{0}\cdot
r_{0}\rrbracket\subseteq\llbracket t^{\ast}\cdot t\cdot
r_{0}\rrbracket\subseteq\llbracket t^{\ast}\cdot r_{0}\rrbracket,$
$\displaystyle va$ $\displaystyle\in\llbracket r_{1}\cdot t^{\ast}\cdot
t_{0}\cdot r_{0}\rrbracket\subseteq\llbracket r_{1}\cdot t^{\ast}\cdot t\cdot
r_{0}\rrbracket\subseteq\llbracket r_{1}\cdot t^{\ast}\cdot r_{0}\rrbracket.$

So $(ua,va)\in\llbracket h(t^{\omega})\rrbracket_{\circ}$.

For $\gamma_{2}$-expansion, let $(u,v^{k})\to_{\gamma_{2}}(u,v)$ ($k\geq 1$)
and $(u,v)\in\llbracket h(t^{\omega})\rrbracket_{\circ}$. So there exists a
split $(t_{0},t_{1})\in\nabla_{t}$ with $u\in\llbracket t^{\ast}\cdot
t_{0}\rrbracket$ and $v\in\llbracket t_{1}\cdot t^{\ast}\cdot
t_{0}\rrbracket$. It suffices to show that $v^{k}\in\llbracket t_{1}\cdot
t^{\ast}\cdot t_{0}\rrbracket$. We have

$v^{k}\in\llbracket t_{1}\cdot t^{\ast}\cdot
t_{0}\rrbracket^{k}=\llbracket(t_{1}\cdot t^{\ast}\cdot
t_{0})^{k}\rrbracket\subseteq\llbracket t_{1}\cdot t^{\ast}\cdot
t_{0}\rrbracket,$

where the last step holds because

$(t_{1}\cdot t^{\ast}\cdot t_{0})\cdot(t_{1}\cdot t^{\ast}\cdot
t_{0})=t_{1}\cdot t^{\ast}\cdot(t_{0}\cdot t_{1})\cdot t^{\ast}\cdot t_{0}\leq
t_{1}\cdot t^{\ast}\cdot t\cdot t^{\ast}\cdot t_{1}\leq t_{1}\cdot
t^{\ast}\cdot t_{0},$

as $t_{0}\cdot t_{1}\leq t$. This concludes the base cases.

For the first induction step, let $T=T_{1}+T_{2}$. Let
$(u,v)\to_{\gamma}(u^{\prime},v^{\prime})$ and
$(u^{\prime},v^{\prime})\in\llbracket h(T_{1}+T_{2})\rrbracket_{\circ}$. As
$\llbracket h(T_{1}+T_{2})\rrbracket_{\circ}=\llbracket
h(T_{1})\rrbracket\cup\llbracket h(T_{2})\rrbracket_{\circ}$,
$(u^{\prime},v^{\prime})\in\llbracket h(T_{i})\rrbracket_{\circ}$ for
$i\in\\{1,2\\}$. By the induction hypothesis, $(u,v)\in\llbracket
h(T_{i})\rrbracket_{\circ}$ and so $(u,v)\in\llbracket
h(T_{1}+T_{2})\rrbracket_{\circ}$.

For the remaining induction step, let $T=t\cdot T^{\prime}$. We treat the case
of $\gamma_{1}$\- and $\gamma_{2}$-expansion separately. For
$\gamma_{1}$-expansion, let $(ua,va)\to_{\gamma_{1}}(u,av)$ and
$(u,av)\in\llbracket h(t\cdot T^{\prime})\rrbracket_{\circ}$. As $\llbracket
h(t\cdot T^{\prime})\rrbracket_{\circ}=\llbracket t\rrbracket\cdot\llbracket
h(T^{\prime})\rrbracket_{\circ}$ there exist $u_{0},u_{1}\in\Sigma^{\ast}$
such that $u_{0}u_{1}=u$, $u_{0}\in\llbracket t\rrbracket$ and
$(u_{1},av)\in\llbracket h(T^{\prime})\rrbracket_{\circ}$. By the induction
hypothesis, $(u_{1}a,va)\in\llbracket h(T^{\prime})\rrbracket_{\circ}$, and

$(ua,va)=(u_{0}u_{1}a,va)\in\llbracket t\rrbracket\cdot\llbracket
h(T^{\prime})\rrbracket_{\circ}=\llbracket h(t\cdot
T^{\prime})\rrbracket_{\circ}.$

Finally, for $\gamma_{2}$-expansion, let $(u,v^{k})\to_{\gamma_{2}}(u,v)$
($k\geq 1$) and $(u,v)\in\llbracket h(t\cdot T^{\prime})\rrbracket_{\circ}$.
So there exist $u_{0},u_{1}$ with $u_{0}\in\llbracket t\rrbracket$,
$(u_{1},v)\in\llbracket h(T^{\prime})\rrbracket_{\circ}$ and $u_{0}u_{1}=u$.
By the induction hypothesis, $(u_{1},v^{k})\in\llbracket
h(T^{\prime})\rrbracket_{\circ}$ and so
$(u,v^{k})=(u_{0}u_{1},v^{k})\in\llbracket h(t\cdot
T^{\prime})\rrbracket_{\circ}$. ∎

Our next goal is to take the weak representation, of which we know that its
semantics is closed under $\gamma$-expansion, and from it construct a new
rational lasso expression, whose semantics is also closed under
$\gamma$-reduction. So now we want to mimic the other directions of
$\gamma_{1}$ and $\gamma_{2}$, namely:

$\displaystyle(uv,wv)$ $\displaystyle\to(u,vw)$ $\displaystyle(u,v^{k})$
$\displaystyle\to(u,v)\quad(k\geq 1)$

For the first reduction, given a lasso $(u,v)$, if we split $u$ and $v$ into
words $u_{1},u_{2},v_{1}$ and $v_{2}$, and if $u_{2}$ happens to be equal to
$v_{2}$, we may reduce to the lasso $(u_{1},u_{2}v_{1})$ (or equivalently
$(u_{1},v_{2}v_{1})$). For the other reduction, if we have a lasso $(u,v)$ and
it happens to be the case that $v=w^{k}$ for some $k\geq 1$, then we may
reduce to the new lasso $(u,w)$. On the level of expressions, if we start with
$(t,r)$ and split both $t$ and $r$ into $t_{0},t_{1},r_{0},r_{1}$ and it so
happens that $t_{1}\cap r_{1}\not=\emptyset$, then we may form the new
rational lasso expression $(t_{0},(t_{1}\cap r_{1})r_{0})$. For the other
reduction, we make use of the root operation, defined on a rational language
$U$ as $\sqrt{U}=\\{u\in\Sigma^{+}\mid\exists k\geq 1:u^{k}\in U\\}$. This
then allows us to go from $(t,r)$ to $(t,\sqrt{r})$, taking care of the
reduction. The next definition combines the ideas of using sequential splits,
the root operation and the intersection. We point out that we assume the input
to be a disjunctive form.

###### Definition 6.11.

Let $\tau=\sum_{i=1}^{n}t_{i}\cdot r_{i}^{\circ}\in\text{Exp}_{\circ}$. We
define the map $\Gamma$ as

$\Gamma(\tau)=\sum_{i=1}^{n}\sum_{\begin{subarray}{c}(t^{\prime}_{0},t^{\prime}_{1})\in\nabla_{t}\\\
(s^{\prime}_{0},s^{\prime}_{1})\in\nabla_{s}\end{subarray}}t^{\prime}_{0}\cdot\left(\sqrt{(t^{\prime}_{1}\cap
s^{\prime}_{1})\cdot s^{\prime}_{0}}\right)^{\circ}.$

We follow up with a proposition which relates the semantics of the rational
lasso expression $\tau$ to that of $\Gamma(\tau)$. From this we can derive a
couple of corollaries which prove useful later on in showing that if the
semantics of $\tau$ is closed under $\gamma$-expansion, then that of
$\Gamma(\tau)$ is saturated. The intuition behind the proposition is gained by
looking at the shape of the lassos on either side of the if and only if.
Specifically, for the lasso $(u,v)$ on the left-hand side, any lasso which is
$\gamma$-equivalent to it has to be of the shape as shown on the right-hand
side.

###### Proposition 6.12.

Let $\tau=\Sigma_{i=1}^{n}t_{i}\cdot r_{i}^{\circ}\in\text{Exp}_{\circ}$. Then

$(u,v)\in\llbracket\Gamma(\tau)\rrbracket_{\circ}\iff\exists k_{1},k_{2}\geq
0,\exists
v_{1},v_{2}\in\Sigma^{\ast}:v=v_{1}v_{2}\land(uv^{k_{1}}v_{1},v_{2}v^{k_{2}+k_{1}}v_{1})\in\llbracket\tau\rrbracket_{\circ}.$

###### Proof.

This is shown by using the various definitions of $\Gamma$, the root
operation, the intersection and the semantics of expressions.

$\displaystyle(u,v)\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$
$\displaystyle\iff\exists
i,\exists(t^{\prime}_{0},t^{\prime}_{1})\in\nabla_{t_{i}},\exists(s^{\prime}_{0},s^{\prime}_{1})\in\nabla_{s_{i}}:(u,v)\in\left\llbracket
t^{\prime}_{0}\cdot\left(\sqrt{(t^{\prime}_{1}\cap s^{\prime}_{1})\cdot
s^{\prime}_{0}}\right)^{\circ}\right\rrbracket_{\circ}$
$\displaystyle\iff\exists
i,\exists(t^{\prime}_{0},t^{\prime}_{1})\in\nabla_{t_{i}},\exists(s^{\prime}_{0},s^{\prime}_{1})\in\nabla_{s_{i}},\exists
k\geq 1:u\in\llbracket
t^{\prime}_{0}\rrbracket,v^{k}\in\llbracket(t^{\prime}_{1}\cap
s^{\prime}_{1})\cdot s^{\prime}_{0}\rrbracket$ $\displaystyle\iff\exists
i,\exists(t^{\prime}_{0},t^{\prime}_{1})\in\nabla_{t_{i}},\exists(s^{\prime}_{0},s^{\prime}_{1})\in\nabla_{s_{i}},\exists
k_{1},k_{2}\geq 0,\exists v_{1},v_{2}\in\Sigma^{\ast}:$
$\displaystyle\qquad\qquad v_{1}v_{2}=v,u\in\llbracket
t^{\prime}_{0}\rrbracket,v^{k_{1}}v_{1}\in\llbracket t^{\prime}_{1}\cap
s^{\prime}_{1}\rrbracket,v_{2}v^{k_{2}}\in\llbracket s^{\prime}_{0}\rrbracket$
$\displaystyle\iff\exists i,\exists k_{1},k_{2}\geq 0,\exists
v_{1},v_{2}\in\Sigma^{\ast}:v_{1}v_{2}=v,uv^{k_{1}}v_{1}\in\llbracket
t_{i}\rrbracket,v_{2}v^{k_{2}+k_{1}}v_{1}\in\llbracket s_{i}\rrbracket$
$\displaystyle\iff\exists k_{1},k_{2}\geq 0,\exists
v_{1},v_{2}\in\Sigma^{\ast}:v_{1}v_{2}=v,(uv^{k_{1}}v_{1},v_{2}v^{k_{2}+k_{1}}v_{1})\in\llbracket\tau\rrbracket_{\circ}.\qed$

###### Corollary 6.13.

Let $\tau\in\text{Exp}_{\circ}$. Then

  1. 1.

$\forall(u,v)\in\llbracket\Gamma(\tau)\rrbracket_{\circ},\exists(u^{\prime},v^{\prime})\in\llbracket\tau\rrbracket_{\circ}\colon(u^{\prime},v^{\prime})\to^{\ast}_{\gamma}(u,v)$,

  2. 2.

$\\{uv^{\omega}\mid(u,v)\in\llbracket\tau\rrbracket_{\circ}\\}=\\{uv^{\omega}\mid(u,v)\in\llbracket\Gamma(\tau)\rrbracket_{\circ}\\}$
and

  3. 3.

$\llbracket\tau\rrbracket_{\circ}\subseteq\llbracket\Gamma(\tau)\rrbracket_{\circ}$.

###### Proof.

In Proposition 6.12 we have
$(uv^{k_{1}}v_{1},v_{2}v^{k_{2}+k_{1}}v_{1})\to^{\ast}_{\gamma}(u,v)$, hence
$(1)$ follows. Moreover, this shows that for each lasso in
$\llbracket\tau\rrbracket_{\circ}$ there exists a $\gamma$-equivalent one in
$\llbracket\Gamma(\tau)\rrbracket_{\circ}$ and vice-versa, hence taking direct
images via $f$ on both sides yields the same set, giving us $(2)$. Finally,
for $(u,v)\in\llbracket\tau\rrbracket_{\circ}$. Choose $k_{1}=k_{2}=0$,
$v_{1}=\varepsilon$ and $v_{2}=v$, so
$(u,v)=(uv^{k_{1}}v_{1},v_{2}v^{k_{2}+k_{1}}v_{1})\in\llbracket\tau\rrbracket_{\circ}$.
By Proposition 6.12,
$(u,v)=(u,v_{1}v_{2})\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$ establishing
$(3)$. ∎

For technical reasons, we require an additional lemma before we can conclude
that for a given rational $\omega$-expression $T$, $\Gamma(h(T))$ is a
representation of $T$. More concretely, given an arbitrary rational lasso
expression $\tau$, it is not the case that the semantics of $\Gamma(\tau)$ is
closed under $\gamma$-reduction. As a counterexample, consider the rational
lasso expression $(aaa,a)$. Then $\Gamma(aaa,a)=(aa,a)+(aaa,a)$ whose
semantics is not closed under $\gamma$-reduction (it misses both
$(\varepsilon,a)$ and $(a,a)$). The reason for this is that the intersection
operation has a limit to how much it can shift underneath the $(-)^{\circ}$.
In the example with $(aaa,a)$, one could apply $\Gamma$ several times, and
indeed after a few consecutive applications we obtain a rational lasso
expression whose semantics is closed under $\gamma$-reduction. Luckily, if one
starts out with a rational lasso expression whose semantics is already closed
under $\gamma$-expansion, then this is no longer a problem and applying
$\Gamma$ yields a rational lasso expression whose semantics is also closed
under $\gamma$-reduction.

###### Lemma 6.14.

Let $\tau\in\text{Exp}_{\circ}$. If $\llbracket\tau\rrbracket_{\circ}$ is
closed under $\gamma$-expansion, then
$\llbracket\Gamma(\tau)\rrbracket_{\circ}$ is $\sim_{\gamma}$-saturated.

###### Proof.

By Lemma 6.1, $\llbracket\Gamma(\tau)\rrbracket_{\circ}$ is
$\sim_{\gamma}$-saturated if it is closed under both $\gamma$-reduction and
$\gamma$-expansion so this is what we show.

We begin by showing that $\llbracket\Gamma(\tau)\rrbracket_{\circ}$ is closed
under $\gamma$-reduction. We split the proof into two cases, one for each type
of reduction. For $\gamma_{1}$-reduction we look at
$(ua,va)\to_{\gamma_{1}}(u,av)$. Suppose
$(ua,va)\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$, we want to show that
$(u,av)\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$. By Proposition 6.12, we
find $k_{1},k_{2},v_{1},v_{2}$ such that

$va=v_{1}v_{2}\qquad\text{ and
}\qquad(ua(va)^{k_{1}}v_{1},v_{2}(va)^{k_{2}+k_{1}}v_{1})\in\llbracket\tau\rrbracket_{\circ}.$

We proceed by case analysis on $v_{2}$. If $v_{2}=\varepsilon$, then
$v_{1}=va$ and

$(ua(va)^{k_{1}}va,(va)^{k_{2}+k_{1}}va)\in\llbracket\tau\rrbracket_{\circ}.$

As $\llbracket\tau\rrbracket_{\circ}$ is closed under $\gamma$-expansion, we
also have that

$(u(av)^{k_{1}+1}a,v(av)^{(2\cdot
k_{2}+k_{1})+(k_{1}+1)}a)=(ua(va)^{k_{1}}va,((va)^{k_{2}+k_{1}}va)^{2})\in\llbracket\tau\rrbracket_{\circ}.$

Using Proposition 6.12, we obtain
$(u,av)\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$. If
$v_{2}\not=\varepsilon$, we find $v_{2}^{\prime}$ with
$v_{2}=v_{2}^{\prime}a$. Then

$(u(av)^{k_{1}}av_{1},v_{2}^{\prime}(av)^{k_{2}+k_{1}}av_{1})=(ua(va)^{k_{1}}v_{1},v_{2}(va)^{k_{2}+k_{1}}v_{1})\in\llbracket\tau\rrbracket_{\circ}.$

Hence, by Proposition 6.12 and as $v_{1}v_{2}^{\prime}=v$ we again have
$(u,av)\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$.

For $\gamma_{2}$-reduction we look at $(u,v^{k})\to_{\gamma_{2}}(u,v)$ where
$k\geq 1$. Assume that $(u,v^{k})\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$.
So by Proposition 6.12 there are $k_{1},k_{2},v_{1},v_{2}$ with

$v^{k}=v_{1}v_{2}\qquad\text{ and
}\qquad(u(v^{k})^{k_{1}}v_{1},v_{2}(v^{k})^{k_{2}+k_{1}}v_{1})\in\llbracket\tau\rrbracket_{\circ}.$

As $v_{1}v_{2}=v^{k}$ we can find some $w_{1},w_{2}$ and $\ell_{1},\ell_{2}$
with $v^{\ell_{1}}w_{1}=v_{1}$ and $w_{2}v^{\ell_{2}}=v_{2}$. It follows that

$(uv^{k\cdot
k_{1}+\ell_{1}}w_{1},w_{2}v^{\ell_{2}+k\cdot(k_{2}+k_{1})+\ell_{1}}w_{1})=(u(v^{k})^{k_{1}}v^{\ell_{1}}w_{1},w_{2}v^{\ell_{2}}(v^{k})^{k_{2}+k_{1}}v^{\ell_{1}}w_{1})\in\llbracket\tau\rrbracket_{\circ}.$

Hence, by Proposition 6.12,
$(u,v)=(u,w_{1}w_{2})\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$. So
$\llbracket\Gamma(\tau)\rrbracket_{\circ}$ is closed under $\gamma$-reduction.

Next we show that $\llbracket\Gamma(\tau)\rrbracket_{\circ}$ is closed under
$\gamma$-expansion. Let $(u,v)\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$ and
$(u_{1},v_{1})\to_{\gamma}(u,v)$. We want to show that
$(u_{1},v_{1})\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$. By Corollary
6.13.1 there exists some $(u_{2},v_{2})\in\llbracket\tau\rrbracket_{\circ}$
with $(u_{2},v_{2})\to^{\ast}_{\gamma}(u,v)$. As
$(u_{1},v_{1})\sim_{\gamma}(u_{2},v_{2})$, there exists a lasso
$(u_{3},v_{3})$ such that $(u_{3},v_{3})\to^{\ast}_{\gamma}(u_{1},v_{1})$ and
$(u_{3},v_{3})\to^{\ast}_{\gamma}(u_{2},v_{2})$. As
$\llbracket\tau\rrbracket_{\circ}$ is closed under $\gamma$-expansion,
$(u_{3},v_{3})\in\llbracket\tau\rrbracket_{\circ}$. It follows by Corollary
6.13.3 that $(u_{3},v_{3})\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$.
Finally, as we have already shown that
$\llbracket\Gamma(\tau)\rrbracket_{\circ}$ is closed under $\gamma$-reduction
and as $(u_{3},v_{3})\to^{\ast}_{\gamma}(u_{1},v_{1})$, we obtain that
$(u_{1},v_{1})\in\llbracket\Gamma(\tau)\rrbracket_{\circ}$. ∎

###### Proposition 6.15.

Let $T\in\text{Exp}_{\omega}$. Then $\Gamma(h(T))$ represents $T$.

###### Proof.

By Proposition 6.9, $h(T)$ weakly represents $T$, i.e. $\text{UP}(\llbracket
T\rrbracket_{\omega})=\\{uv^{\omega}\mid(u,v)\in\llbracket
h(T)\rrbracket_{\circ}\\}$. It follows from Corollary 6.13.2 that
$\Gamma(h(T))$ also weakly represents $T$, as

$\text{UP}(\llbracket
T\rrbracket_{\omega})=\\{uv^{\omega}\mid(u,v)\in\llbracket
h(T)\rrbracket_{\circ}\\}=\\{uv^{\omega}\mid(u,v)\in\llbracket\Gamma(h(T))\rrbracket_{\circ}\\}.$

Furthermore, as $\llbracket h(T)\rrbracket_{\circ}$ is closed under
$\gamma$-expansion (Proposition 6.10),
$\llbracket\Gamma(h(T))\rrbracket_{\circ}$ is $\sim_{\gamma}$-saturated
(Proposition 6.14). Hence, by Remark 6.4 $\Gamma(h(T))$ represents $T$. ∎

The previous proposition together with the Brzozowski construction for lasso
automata give us the main result of this section. This establishes the
remaining arrow in Figure 1 from the introduction.

###### Theorem 6.16.

Every rational $\omega$-language is accepted by a finite $\Omega$-automaton.

###### Proof.

Let $L$ be a rational $\omega$-language and $T\in\text{Exp}_{\omega}$ a
rational $\omega$-expression denoting it. Then the lasso automaton
$(\widehat{\mathcal{C}},[\Gamma(h(T))]_{\sim_{C}})$ is a finite
$\Omega$-automaton with

$L_{\omega}(\widehat{\mathcal{C}},[\Gamma(h(T))]_{\sim_{C}})=\llbracket
T\rrbracket_{\omega}=L.\qed$

##  7 Conclusion

We have introduced rational lasso expressions and languages and shown a Kleene
Theorem for lasso languages and $\omega$-languages. In order to obtain these
results we gave a Brzozowski construction for lasso automata. Moreover, we
introduced the notion of representation and showed how to construct a
representing rational lasso expression from a rational $\omega$-expression. As
a consequence, we obtained a new construction for converting rational
$\omega$-expressions to $\Omega$-automata.

Our results motivate some interesting directions for future work. In [2],
Angluin et al. introduce syntactic and recurring FDFAs and show that they can
be up to exponentially smaller than periodic FDFAs. This raises the question
whether from a given rational $\omega$-expression, we can construct a rational
lasso expression such that the Brzozowski construction yields a syntactic or
recurring FDFA. These FDFAs operate using different congruences and it might
be of interest to see how the structure of rational lasso expressions interact
with them. As one of the applications is language learning, it is also worth
investigating the complexity of our constructions. The state complexity of the
root and intersection operation are known. We remark that the languages of
which we compute the root are always transitive and we wonder if the state
complexity of the root operation improves when restricting to transitive
languages. Moreover, as Calbrix et al. devised $L_{\$}$ in the hopes of
improving algorithms for model checking and verification, it would be of
interest to establish a more direct link between lasso automata and logics
such as linear temporal logic. This naturally leads on to a comparison between
the more traditionally used $\omega$-automata, such as nondeterministic Büchi
automata, and $\Omega$-automata.

Another line of work is to show completeness of the lasso algebra we
introduced in Section 3, and to look more closely at the links between lasso
and Wagner algebras.

### Acknowledgements.

This article is the result of the author’s Master’s thesis which was written
under the supervision of Tobias Kappé and Yde Venema. The author would like to
thank Yde Venema for suggesting this topic and also both Tobias Kappé and Yde
Venema for valuable discussions. Furthermore, the author would like to thank
Harsh Beohar and Georg Struth for valuable discussions and for reading earlier
drafts of this paper.

## References

  * [1] Dana Angluin, Udi Boker, and Dana Fisman.  Families of DFAs as acceptors of omega-regular languages.  In Piotr Faliszewski, Anca Muscholl, and Rolf Niedermeier, editors, 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, August 22-26, 2016 - Kraków, Poland, volume 58 of LIPIcs, pages 11:1–11:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [2] Dana Angluin and Dana Fisman.  Learning regular omega languages.  Theor. Comput. Sci., 650:57–72, 2016.
  * [3] Janusz A. Brzozowski.  Derivatives of regular expressions.  J. ACM, 11(4):481–494, 1964.
  * [4] Hugues Calbrix, Maurice Nivat, and Andreas Podelski.  Ultimately periodic words of rational $\omega$-languages.  In Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings, volume 802 of Lecture Notes in Computer Science, pages 554–566. Springer, 1993.
  * [5] Vincenzo Ciancia and Yde Venema.  Omega-automata: A coalgebraic perspective on regular omega-languages.  In Markus Roggenbach and Ana Sokolova, editors, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO), volume 139 of LIPIcs, pages 5:1–5:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [6] Mike Cruchten.  Topics in $\Omega$-automata – A journey through lassos, algebra, coalgebra and expressions.  Master’s thesis, The University of Amsterdam, June 2022.
  * [7] Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi.  Concurrent Kleene algebra: Free model and completeness.  In Amal Ahmed, editor, Proceedtings of the 27th European Symposium on Programming, ESOP 2018, volume 10801 of Lecture Notes in Computer Science, pages 856–882. Springer, 2018.
  * [8] Dexter Kozen.  A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events.  Inf. Comput., 110(2):366–390, 1994.
  * [9] Oded Maler and Ludwig Staiger.  On syntactic congruences for omega-languages.  Theor. Comput. Sci., 183(1):93–112, 1997.
  * [10] Klaus W. Wagner.  Eine Axiomatisierung der Theorie der regulären Folgenmengen.  J. Inf. Process. Cybern., 12(7):337–354, 1976.