# Separation for dot-depth two

Thomas Place  LaBRI, Université de Bordeaux, Institut Universitaire de France
<EMAIL_ADDRESS>and  Marc Zeitoun  LaBRI, Université de Bordeaux<EMAIL_ADDRESS>
###### Abstract.

The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free
languages of finite words. By a theorem of McNaughton and Papert, these are
also the first-order definable languages. The dot-depth rose to prominence
following the work of Thomas, who proved an exact correspondence with the
quantifier alternation hierarchy of first-order logic: each level in the dot-
depth hierarchy consists of all languages that can be defined with a
prescribed number of quantifier blocks. One of the most famous open problems
in automata theory is to settle whether the membership problem is decidable
for each level: is it possible to decide whether an input regular language
belongs to this level?

Despite a significant research effort, membership by itself has only been
solved for low levels. A recent breakthrough was achieved by replacing
membership with a more general problem: _separation_. Given two input
languages, one has to decide whether there exists a third language in the
investigated level containing the first language and disjoint from the second.
The motivation for looking at separation is threefold: (1) while more
difficult, it is more rewarding, as solving it requires a better
understanding; (2) being more general, it provides a more convenient
framework, and (3) all recent membership algorithms are actually reductions to
separation for lower levels.

We present a separation algorithm for dot-depth two. A key point is that while
dot-depth two is our most prominent application, our theorem is more general.
We consider a family of hierarchies, which includes the dot-depth:
concatenation hierarchies. They are built through a generic construction
process: one first chooses an initial class, the basis, which serves as the
lowest level in the hierarchy. Then, further levels are built by applying
generic operations. Our main theorem states that for any concatenation
hierarchy whose basis consists of finitely many languages, separation is
decidable for level one. In the special case of the dot-depth, this can be
lifted to level two using previously known results.

###### Key words and phrases:

Words, regular languages, concatenation hierarchies, first-order logic,
quantifier alternation, membership, separation

###### 1991 Mathematics Subject Classification:

F.4.1,F.4.3

Supported by the Agence Nationale de la Recherche, DeLTA project
(ANR-16-CE40-0007).

##  1\. Introduction

Concatenation hierarchies. Many fundamental problems about regular languages
raised in the 70s [Pin17b] led to considerable advances, not only in automata
theory but also in logic and algebra, thanks to the discovery of deep
connections between these areas. Even if some of these questions are now well
understood, a few others remain wide open, despite a wealth of research work
spanning several decades. This is the case for the fascinating dot-depth
problem [Pin17a], which has two elementary formulations: a language-theoretic
one and a logical one. The language-theoretic one is the older of the two. It
takes its roots in a theorem of Schützenberger [Sch65] (see also [DKRH16,
DG08]), which gives an algorithm to decide whether a regular language is star-
free, _i.e._ , can be expressed using union, complement and concatenation, but
without the Kleene star operator. This celebrated result was highly
influential for three reasons:

  * •

First, Schützenberger precisely formalized the objective of “understanding the
expressive power of a formalism” through a decision problem called
_membership_ , which asks whether an input regular language belongs to the
class under study.

  * •

Next, he developed a methodology for tackling it, which he applied to
membership for the class of star-free languages.

  * •

Finally, McNaughton and Papert [MP71] established that star-free languages are
exactly the first-order definable ones.

This work highlighted the robustness of the notion of regularity, underlining
the ties between automata theory and logic, and revealing new links with
algebra. It also established membership as the reference problem for
investigating classes of languages.

Schützenberger’s theorem led Brzozowski and Cohen to define the dot-depth
hierarchy [BC71], an infinite classification [BK78] of all star-free languages
counting the number of alternations between concatenations and complements
needed to define them. This definition is a particular instance of a generic
construction process, which was formalized later and named _concatenation
hierarchies_. Any such hierarchy has a single parameter: a “level $0$ class”
(its _basis_). Then, one uses two operations, polynomial and Boolean closure,
to build two kinds of classes: half levels 1/2, 3/2, 5/2…and full levels 1, 2,
3…Given a class of languages $\mathcal{C}$, its _polynomial closure_
${Pol\/}(\mathcal{C})$ is the least class of languages containing
$\mathcal{C}$ and closed under union and marked concatenation ($K,L\mapsto
KaL$, where $a$ is a letter). Its _Boolean closure_ ${Bool\/}(\mathcal{C})$ is
the least class containing $\mathcal{C}$ and closed under union and
complement. For any full level $n$, the next half and full levels are built as
follows:

  * •

Level $n+\frac{1}{2}$ is the polynomial closure of level $n$.

  * •

Level $n+1$ is the Boolean closure of level $n+\frac{1}{2}$.

Thus, a concatenation hierarchy is fully determined by its basis. Here, we are
interested in hierarchies with a _finite_ basis, _i.e._ , consisting of a
finite number of regular languages.

The most prominent hierarchies of this kind in the literature are the dot-
depth itself, as well as the Straubing-Thérien hierarchy [Str81, Thé81]. They
acquired this status when it was discovered [Tho82, PP86] that each of them
coincides with the quantifier alternation hierarchy within an appropriate
variant of first-order logic. These two variants have the same overall
expressiveness but slightly different signatures (which impacts the properties
that one can define at a given level of their quantifier alternation
hierarchies).

These correspondences motivated a research program to solve membership for all
levels of both hierarchies, thus also characterizing the alternation
hierarchies of first-order logic. However, progress has been slow. Until
recently, the classes that were solved for both variants are only level 1/2
[Arf87, PW97], level 1 [Sim75, Kna83] and level 3/2 [Arf87, PW97, GS00]. See
[DGK08] for a survey. Following these results, membership for level 2 remained
open for a long time and was named the “dot-depth 2 problem”.

Separation. Recently [PZ19, Pla18], solutions were found for levels 2, 5/2 and
7/2. The key ingredient is a new problem stronger than membership:
_separation_. Rather than asking whether an input language belongs to the
class $\mathcal{C}$ under investigation, the $\mathcal{C}$-separation problem
takes as input _two_ languages, and asks whether there exists a third one
_from $\mathcal{C}$_ containing the first and disjoint from the second. While
the interest in separation is recent, it has quickly replaced membership as
the central question. A first practical reason is that separation proved
itself to be a key ingredient in obtaining all recent membership results. See
[PZ15, PZ18b] for an overview. A striking example is provided by a crucial
theorem of [PZ19]. It establishes a generic reduction from
${Pol\/}(\mathcal{C})$-separation to $\mathcal{C}$-membership which holds for
any class $\mathcal{C}$. Combined with a separation algorithm for level 3/2
and a little extra work, this yields a membership algorithm for level 5/2.

However, the main reason is deeper. The primary motivation for considering
such problems is to thoroughly understand the classes under investigation. In
this respect, while harder, separation is also far more rewarding than
membership. On one hand, a membership algorithm for a class $\mathcal{C}$ only
applies to languages of $\mathcal{C}$: it can detect them and build a
description witnessing membership. On the other hand, a separation algorithm
for $\mathcal{C}$ is universal: it applies to _any_ language. Indeed, one may
view separation as an approximation problem: given an input pair
$(L_{1},L_{2})$ one wants to over-approximate $L_{1}$ by a language in
$\mathcal{C}$, and $L_{2}$ serves to specify what a satisfying approximation
is. This is why we look at separation: it yields a more robust understanding
of the classes than membership.

The state of the art for separation is the following: it was shown to be
decidable for levels 1/2, 1, 3/2 and 5/2 in the Straubing-Thérien hierarchy
[CMM13, PvRZ13, PZ19, Pla18]. These results can be lifted to dot-depth using a
generic transfer theorem [PZ20]. Notice the gap between levels 3/2 and 5/2: no
algorithm is known for level 2. This is explained by the fact that obtaining
separation algorithms presents very different challenges for half levels and
for full levels. Indeed, it turns out that most separation algorithms rely
heavily on closure under marked concatenation, which holds for half levels by
definition, but not for full levels.

Contributions. Our main result is a separation algorithm for level 2 in the
Straubing-Thérien hierarchy. Furthermore, by the aforementioned transfer
theorem [PZ20], this can be lifted to separation for dot-depth 2. A crucial
point is that this separation result is actually an instance of a generic
theorem, which applies to any _finite_ class $\mathcal{C}$ satisfying a few
standard properties (namely closure under Boolean operations and quotients).
It states that for such a class $\mathcal{C}$, the class
${Bool\/}({Pol\/}(\mathcal{C}))$ has decidable separation. This has two
important consequences:

  * •

In _any_ hierarchy whose basis is such a class, level 1 has decidable
separation.

  * •

In the specific case of the Straubing-Thérien hierarchy, this extends to level
2, since it is also level 1 of another finitely based concatenation hierarchy
[PS85].

This generic result complements other recent results in a natural way. It has
been shown in [Pla18] that ${Pol\/}(\mathcal{C})$\- and
${Pol\/}({Bool\/}({Pol\/}(\mathcal{C})))$-separation are decidable for any
finite class $\mathcal{C}$ satisfying the aforementioned hypotheses. Combined
with our results, this implies that for finitely based concatenation
hierarchies, separation is decidable for all levels up to 3/2.

Our proof argument exploits a theorem of [Pla18] about the simpler class
${Pol\/}(\mathcal{C})$. However, the techniques that we use here are very
different from the ones used in [Pla18], which rely heavily on the fact that
${Pol\/}(\mathcal{C})$ and ${Pol\/}({Bool\/}({Pol\/}(\mathcal{C})))$ are
closed under concatenation (again, this is not the case for
${Bool\/}({Pol\/}(\mathcal{C}))$).

Being generic, our approach yields separation algorithms for a whole family of
classes. Moreover, it serves to pinpoint the key hypotheses which are critical
in order to solve separation for dot-depth 2. Let us also stress that we
obtain new direct proofs that separation is decidable for level 1 in both the
dot-depth and Straubing-Thérien hierarchies. This is of particular interest
for dot-depth 1 since the previous solution was indirect, as it relied on a
transfer result from [PZ20].

Finally, a key point is that all our results are stated and proved using a
general framework that was recently introduced in [PZ18a]. It is designed to
handle the separation problem and to present the solutions in an elegant
manner. In fact, this framework considers a third decision problem, which is
even more general than separation: _covering_. Given a class $\mathcal{C}$,
the $\mathcal{C}$-covering problem takes two objects as input, a single
regular language $L$ and a finite set of regular languages $\mathbf{L}$. It
asks whether there exists a $\mathcal{C}$-cover of $L$ (_i.e._ , a finite set
of languages in $\mathcal{C}$ whose union includes $L$) such that no language
in this $\mathcal{C}$-cover intersects all languages in $\mathbf{L}$. It is
simple to show that separation is the special case of covering when the set
$\mathbf{L}$ is a singleton. Our main theorem actually states that
${Bool\/}({Pol\/}(\mathcal{C}))$-covering is decidable for any finite class
$\mathcal{C}$ satisfying mild hypotheses.

Organization. The paper is organized as follows. Section 2 gives preliminary
definitions. In Section 3, we introduce concatenation hierarchies and state
our generic theorem: ${Bool\/}({Pol\/}(\mathcal{C}))$-covering is decidable
for every finite quotient-closed Boolean algebra $\mathcal{C}$. The remainder
of the paper is devoted to presenting the algorithm. In Section 4, we recall
the framework which was designed in [PZ18a] to handle the covering problem. We
use this framework in Section 5 to formulate our algorithm for
${Bool\/}({Pol\/}(\mathcal{C}))$-covering. The remaining sections are devoted
to proving that this algorithm is correct.

This is the journal version of [PZ17]. The main result (_i.e._ , that
${Bool\/}({Pol\/}(\mathcal{C}))$-separation is decidable for every finite
quotient-closed Boolean algebra $\mathcal{C}$) has been generalized to
${Bool\/}({Pol\/}(\mathcal{C}))$-covering. Moreover, both its presentation and
its proof have been completely reworked. Our results are now formulated using
the general framework introduced in [PZ18a], designed to handle separation and
covering problems.

##  2\. Preliminaries

In this preliminary section, we provide standard definitions for the basic
objects investigated in the paper. Moreover, we present the separation and
covering problems.

###  2.1. Words, languages and classes

For the whole paper, we fix an arbitrary finite alphabet $A$. Recall that
$A^{*}$ denotes the set of all words over $A$, including the empty word
$\varepsilon$. We let $A^{+}=A^{*}\setminus\\{\varepsilon\\}$. If $u,v\in
A^{*}$ are words, we write $u\cdot v$ or $uv$ the word obtained by
concatenating $u$ and $v$.

A subset of $A^{*}$ is called a _language_. We shall denote the singleton
language $\\{u\\}$ by $u$. It is standard to generalize the concatenation
operation to languages: given $K,L\subseteq A^{*}$, we write $KL$ for the
language $KL=\\{uv\mid u\in K\text{ and }v\in L\\}$. Moreover, we shall also
consider _marked concatenation_ , which is less standard. Given $K,L\subseteq
A^{*}$, a marked concatenation of $K$ with $L$ is a language of the form $KaL$
for some letter $a\in A$.

A _class of languages_ $\mathcal{C}$ is simply a set of languages. In the
paper, we work with robust classes which satisfy standard closure properties:

  * •

A _lattice_ is a class $\mathcal{C}$ closed under finite union and finite
intersection, and such that $\emptyset\in\mathcal{C}$ and
$A^{*}\in\mathcal{C}$.

  * •

A _Boolean algebra_ is a lattice closed under complement.

  * •

Finally, a class $\mathcal{C}$ is _quotient-closed_ when for all
$L\in\mathcal{C}$ and all $w\in A^{*}$, the following two languages belong to
$\mathcal{C}$:

$w^{-1}L\stackrel{{\scriptstyle\text{def}}}{{=}}\\{u\in A^{*}\mid wu\in
L\\}\quad\text{and}\quad
Lw^{-1}\stackrel{{\scriptstyle\text{def}}}{{=}}\\{u\in A^{*}\mid uw\in L\\}.$

All classes considered in the paper will be (at least) quotient-closed
lattices. Moreover, they are all included in the class of _regular languages_.
These are the languages that can be equivalently defined by monadic second-
order logic, finite automata or finite monoids. Let us briefly recall the
definition based on monoids, which we shall use.

A _monoid_ is a set $M$ equipped with an associative multiplication (usually
denoted by “$\cdot$”) which has a neutral element (usually denoted by
“$1_{M}$”). Recall that an _idempotent_ within a semigroup $S$ is an element
$e\in S$ such that $ee=e$. Observe that $A^{*}$ is a monoid when equipped with
word concatenation as the multiplication (the neutral element is
$\varepsilon$). Hence, given a monoid $M$, we may consider morphisms
$\alpha:A^{*}\rightarrow M$. Given such a morphism, we say that a language
$L\subseteq A^{*}$ is _recognized_ by $\alpha$ when there exists $F\subseteq
M$ such that $L=\alpha^{-1}(F)$. It is well-known that the regular languages
are exactly those which can be recognized by a morphism
$\alpha:A^{*}\rightarrow M$, where $M$ is a finite monoid.

######  Remark 2.1.

Whenever we consider a morphism $\alpha:A^{*}\to M$ in the paper, the monoid
$M$ will be finite. For the sake of avoiding clutter, this will be implicit
from now on.

###  2.2. Separation and covering

In this paper, we investigate specific classes of languages which are part of
concatenation hierarchies (introduced in Section 3). We do so by relying on
two decision problems: separation and covering. The former is standard while
the latter was introduced in [PZ18a]. Both of them are parametrized by an
arbitrary class of languages $\mathcal{C}$. Let us start with the definition
of separation.

Separation. Given three languages $K,L_{1},L_{2}$, we say that $K$ _separates_
$L_{1}$ from $L_{2}$ if $L_{1}\subseteq K\text{ and }L_{2}\cap K=\emptyset$.
Given a class of languages $\mathcal{C}$, we say that $L_{1}$ is
_$\mathcal{C}$ -separable_ from $L_{2}$ if some language in $\mathcal{C}$
separates $L_{1}$ from $L_{2}$. Observe that when $\mathcal{C}$ is not closed
under complement, the definition is not symmetrical: $L_{1}$ could be
$\mathcal{C}$-separable from $L_{2}$ while $L_{2}$ is not
$\mathcal{C}$-separable from $L_{1}$. The separation problem associated to a
given class $\mathcal{C}$ is as follows:

INPUT: | Two regular languages $L_{1}$ and $L_{2}$.
---|---
OUTPUT: | Is $L_{1}$ $\mathcal{C}$-separable from $L_{2}$?

Separation is meant to be used as a mathematical tool in order to investigate
classes of languages. Intuitively, obtaining a $\mathcal{C}$-separation
algorithm requires a solid understanding of $\mathcal{C}$.

######  Remark 2.2.

The $\mathcal{C}$-separation problem generalizes another classical decision
problem: $\mathcal{C}$-membership, which asks whether a single regular
language $L$ belongs to $\mathcal{C}$. Indeed, $L\in\mathcal{C}$ if and only
if $L$ is $\mathcal{C}$-separable from $A^{*}\setminus L$.

Covering. Our second problem is more general and was introduced in [PZ18a].
Given a language $L$, a _cover of $L$_ is a _finite_ set of languages
$\mathbf{K}$ such that:

$L\subseteq\bigcup_{K\in\mathbf{K}}K.$

We speak of _universal cover_ to mean a cover of $A^{*}$. Moreover, if
$\mathcal{C}$ is a class, a $\mathcal{C}$-cover of $L$ is a cover $\mathbf{K}$
of $L$ such that all $K\in\mathbf{K}$ belong to $\mathcal{C}$.

Covering takes as input a language $L_{1}$ and a _finite set of languages_
$\mathbf{L}_{2}$. A _separating cover_ for the pair $(L_{1},\mathbf{L}_{2})$
is a cover $\mathbf{K}$ of $L_{1}$ such that for every $K\in\mathbf{K}$, there
exists $L\in\mathbf{L}_{2}$ which satisfies $K\cap L=\emptyset$. Finally,
given a class $\mathcal{C}$, we say that the pair $(L_{1},\mathbf{L}_{2})$ is
$\mathcal{C}$-coverable when there exists a separating $\mathcal{C}$-cover.
The $\mathcal{C}$-covering problem is now defined as follows:

INPUT: | A regular language $L_{1}$ and a finite set of regular languages $\mathbf{L}_{2}$.
---|---
OUTPUT: | Is $(L_{1},\mathbf{L}_{2})$ $\mathcal{C}$-coverable?

Note that in the covering problem, we are interested in the existence of
covers which are _separating_ (but notice that we do not keep this precision
in the name of the problem itself, to lighten the terminology). It is
straightforward to prove that covering generalizes separation (provided that
the class $\mathcal{C}$ is a lattice), as stated in the following lemma (see
Theorem 3.5 in [PZ18a] for the proof).

######  Lemma 2.3.

Let $\mathcal{C}$ be a lattice and $L_{1},L_{2}$ be two languages. Then
$L_{1}$ is $\mathcal{C}$-separable from $L_{2}$, if and only if
$(L_{1},\\{L_{2}\\})$ is $\mathcal{C}$-coverable.

In the paper, we shall not work with covering directly. Instead, we use a
framework introduced in [PZ18a], which is designed to formulate and handle
these problems. We recall it in Section 4.

###  2.3. Finite lattices

In the paper, we work with classes built from an arbitrary finite lattice
(_i.e._ , one that contains finitely many languages) using generic two
operations: polynomial closure and Boolean closure (see Section 3). Here, we
present standard results about such classes.

Canonical preorder relations. Consider a finite lattice $\mathcal{C}$. It is
classical to associate a _canonical preorder relation over $A^{*}$_ to
$\mathcal{C}$. Given $w,w^{\prime}\in A^{*}$, we write
$w\leqslant_{\mathcal{C}}w^{\prime}$ if and only if the following holds:

$\text{For all $L\in\mathcal{C}$,}\quad w\in L\ \Rightarrow\ w^{\prime}\in L.$

It is immediate from the definition that $\leqslant_{\mathcal{C}}$ is
transitive and reflexive, making it a preorder.

######  Example 2.4.

Consider the class $\mathcal{C}$ consisting of all unions of intersections of
languages of the form $A^{*}aA^{*}$, for $a\in A$. By definition, this class
is a finite lattice. The assiciated preorder $\leqslant_{\mathcal{C}}$ is
defined by $w\leqslant_{\mathcal{C}}w^{\prime}$ if and only if every letter
occurring in $w$ also occurs in $w^{\prime}$.

We shall use several results about the relation $\leqslant_{\mathcal{C}}$. We
omit the proofs which are simple and available in [Pla18].

The first lemma is where we use the hypothesis that $\mathcal{C}$ is finite.
We say that a language $L\subseteq A^{*}$ is an _upper set_ (for
$\leqslant_{\mathcal{C}}$) when for any two words $u,v\in A^{*}$, if $u\in L$
and $u\leqslant_{\mathcal{C}}v$, then $v\in L$. Furthermore, given $u\in
A^{*}$, we let ${\mathord{\uparrow}_{\mathcal{C}}\,u}\subseteq A^{*}$ be the
least upper set containing $u$: ${\mathord{\uparrow}_{\mathcal{C}}\,u}=\\{v\in
A^{*}\mid u\leqslant_{\mathcal{C}}v\\}$.

######  Lemma 2.5.

Let $\mathcal{C}$ be a finite lattice. Then, for any $L\subseteq A^{*}$, we
have $L\in\mathcal{C}$ if and only if $L$ is an upper set for
$\leqslant_{\mathcal{C}}$. In particular, $\leqslant_{\mathcal{C}}$ has
finitely many upper sets.

Let us complete these definitions with a few additional useful results. First,
as we observed for and in Example 2.7, when the finite lattice $\mathcal{C}$
is actually a Boolean algebra, it turns out that $\leqslant_{\mathcal{C}}$ is
an equivalence relation, which we shall denote by $\sim_{\mathcal{C}}$.

######  Lemma 2.6.

Let $\mathcal{C}$ be a finite Boolean algebra. Then, for any alphabet $A$, the
canonical preorder $\leqslant_{\mathcal{C}}$ is an equivalence relation
$\sim_{\mathcal{C}}$ which admits the following direct definition:

$\text{$w\sim_{\mathcal{C}}w^{\prime}$ if and only if for all
$L\in\mathcal{C}$,\quad$w\in L\ \Leftrightarrow\ w^{\prime}\in L$}.$

Thus, for any $L\subseteq A^{*}$, we have $L\in\mathcal{C}$ if and only if $L$
is a union of $\sim_{\mathcal{C}}$-classes. In particular,
$\sim_{\mathcal{C}}$ has finite index.

######  Example 2.7.

Consider the class and of all Boolean combinations of languages $A^{*}aA^{*}$,
for $a\in A$ (“ and ” stands for “alphabet testable”: $L\in\and$ if and only
if membership of a word $w$ in $L$ depends only on the letters occurring in
$w$). Clearly, and is a finite Boolean algebra—it is the Boolean closure of
the class from Example 2.4 (see Section 3.1 for the definition of Boolean
closure). In that case, $\leqslant_{\and}$ is an equivalence relation
$\sim_{\and}$: $w\sim_{\and}w^{\prime}$ if and only if $w$ and $w^{\prime}$
have the same alphabet (_i.e._ , contain the same set of letters).

Another important and useful property is that when $\mathcal{C}$ is quotient-
closed, the canonical preorder $\leqslant_{\mathcal{C}}$ is compatible with
word concatenation.

######  Lemma 2.8.

A finite lattice $\mathcal{C}$ is quotient-closed if and only if its
associated canonical preorder $\leqslant_{\mathcal{C}}$ is compatible with
word concatenation. That is, for any words $u,v,u^{\prime},v^{\prime}$,

$u\leqslant_{\mathcal{C}}u^{\prime}\quad\text{and}\quad
v\leqslant_{\mathcal{C}}v^{\prime}\quad\Rightarrow\quad
uv\leqslant_{\mathcal{C}}u^{\prime}v^{\prime}.$

$\mathcal{C}$-compatible morphisms. We use these notions to define special
monoid morphisms. We fix a finite quotient-closed Boolean algebra
$\mathcal{C}$ for the definition.

By Lemma 2.6, $\sim_{\mathcal{C}}$ has finite index and the languages in
$\mathcal{C}$ are exactly the unions of $\sim_{\mathcal{C}}$-classes.
Moreover, since $\mathcal{C}$ is quotient-closed, we know from Lemma 2.8 that
$\sim_{\mathcal{C}}$ is a congruence for word concatenation. It follows that
the quotient set ${A^{*}}/{\sim_{\mathcal{C}}}$ is a finite monoid and the map
$w\mapsto[w]_{\mathcal{C}}$ is a morphism from $A^{*}$ to
${A^{*}}/{\sim_{\mathcal{C}}}$. Consider an arbitrary morphism
$\alpha:A^{*}\to M$. We say that $\alpha$ is _$\mathcal{C}$ -compatible_ when,
for every $s\in M$, there exists a $\sim_{\mathcal{C}}$-class denoted by
$[s]_{\mathcal{C}}$ such that $\alpha^{-1}(s)\subseteq[s]_{\mathcal{C}}$. In
other words, $[w]_{\mathcal{C}}=[s]_{\mathcal{C}}$ for every $w\in A^{*}$ such
that $\alpha(w)=s$.

######  Remark 2.9.

Given $s\in M$, the $\sim_{\mathcal{C}}$-class $[s]_{\mathcal{C}}$ is
determined by $\alpha$ when $\alpha^{-1}(s)\neq\emptyset$
($[s]_{\mathcal{C}}=[w]_{\mathcal{C}}$ for any $w\in\alpha^{-1}(s)$). If
$\alpha^{-1}(s)=\emptyset$, we may choose any $\sim_{\mathcal{C}}$-class as
$[s]_{\mathcal{C}}$. When we consider a $\mathcal{C}$-compatible morphism, we
implicitly assume that the map $s\mapsto[s]_{\mathcal{C}}$ is fixed.

We prove that we may assume without loss of generality that all our morphisms
are $\mathcal{C}$-compatible: any regular language $L$ is recognized by a
$\mathcal{C}$-compatible morphism which recognizes $L$.

######  Lemma 2.10.

Let $\mathcal{C}$ be a finite quotient-closed Boolean algebra. Given a regular
language $L\subseteq A^{*}$, one may compute a $\mathcal{C}$-compatible
morphism $\alpha:A^{*}\to M$ recognizing $L$.

###### Proof.

Since $L$ is regular, we may compute a finite monoid $N$ and a morphism
$\beta:A^{*}\to N$ (not necessarily $\mathcal{C}$-compatible) recognizing $L$.
Since we know that the quotient set ${A^{*}}/{\sim_{\mathcal{C}}}$ is a finite
monoid, the Cartesian product $M=N\times({A^{*}}/{\sim_{\mathcal{C}}})$ is a
finite monoid for the componentwise multiplication. It now suffices to define
the morphism $\alpha:A^{*}\to M$ by $\alpha(w)=(\beta(w),[w]_{\mathcal{C}})$
for any $w\in A^{*}$. Clearly, $\alpha$ is a morphism which recognizes $L$ and
one may verify that it is $\mathcal{C}$-compatible. ∎

##  3\. Closure operations and main theorem

In this section, we define the family of classes that we investigate in the
paper and present a few results about them. Then, we state our main theorem
and discuss its consequences.

###  3.1. Closure operations

Consider a class $\mathcal{C}$. The _Boolean closure_ of $\mathcal{C}$,
denoted by ${Bool\/}(\mathcal{C})$, is defined as the least Boolean algebra
containing $\mathcal{C}$. The next lemma follows from the definitions (this
amounts to verifying that quotients commute with Boolean operations, _e.g._ ,
that for all languages $K,L\subseteq A^{*}$ and for all words $w$, we have
$w^{-1}(K\cup L)=w^{-1}K\cup w^{-1}L$ and $w^{-1}(A^{*}\setminus
L)=A^{*}\setminus(w^{-1}L)$, and symmetrically for the other quotient
operation).

######  Lemma 3.1.

Let $\mathcal{C}$ be a quotient-closed lattice. Then ${Bool\/}(\mathcal{C})$
is a quotient-closed Boolean algebra.

The second operation that we shall consider is slightly more involved. Given a
class $\mathcal{C}$, the _polynomial closure_ of $\mathcal{C}$, denoted by
${Pol\/}(\mathcal{C})$, is the least class containing $\mathcal{C}$ which is
closed under both union and marked concatenation:

$\text{for all $K,L\in{Pol\/}(\mathcal{C})$ and $a\in A$},\quad K\cup
L\in{Pol\/}(\mathcal{C})\text{ and }KaL\in{Pol\/}(\mathcal{C}).$

While this is not obvious from the definition, when the input class
$\mathcal{C}$ is a quotient-closed lattice, its polynomial closure
${Pol\/}(\mathcal{C})$ is a quotient-closed lattice as well. The difficulty is
to establish that ${Pol\/}(\mathcal{C})$ is closed under intersection. This
was originally proved by Arfi [Arf87], assuming additionally that
$\mathcal{C}$ is closed under complement. The result was then strengthened in
[Pin13, PZ18b].

######  Theorem 3.2 (Arfi [Arf87]).

Let $\mathcal{C}$ be a quotient-closed lattice. Then, ${Pol\/}(\mathcal{C})$
is a quotient-closed lattice closed under concatenation and marked
concatenation.

In the paper, we consider classes of the form ${Bool\/}({Pol\/}(\mathcal{C}))$
built by applying polynomial closure and Boolean closure successively to some
arbitrary quotient-closed Boolean algebra $\mathcal{C}$. For the sake of
avoiding clutter, we shall write ${BPol\/}(\mathcal{C})$ for
${Bool\/}({Pol\/}(\mathcal{C}))$. Note that by Lemma 3.1 and Theorem 3.2, we
have the following corollary.

######  Corollary 3.3.

Let $\mathcal{C}$ be a quotient-closed lattice. Then, ${BPol\/}(\mathcal{C})$
is a quotient-closed Boolean algebra.

A key remark is that in general, classes built with Boolean closure (such as
${BPol\/}(\mathcal{C})$) are _not_ closed under concatenation. This contrasts
with polynomial closure in which closure under (marked) concatenation holds by
definition. This is an issue, as most of our techniques designed for handling
separation and covering rely heavily on concatenation. We cope with this
problem by using the following weak concatenation principle, which holds for
any class that is the Boolean closure of another class which is itself closed
under concatenation.

######  Lemma 3.4.

Let $\mathcal{D}$ be a lattice closed under concatenation. Consider
$L,L^{\prime}\in\mathcal{D}$ and let $\mathbf{K},\mathbf{K}^{\prime}$ be
${Bool\/}(\mathcal{D})$-covers of $L$ and $L^{\prime}$ respectively. There
exists a ${Bool\/}(\mathcal{D})$-cover $\mathbf{H}$ of $LL^{\prime}$ such that
for every $H\in\mathbf{H}$, we have $H\subseteq KK^{\prime}$ for some
$K\in\mathbf{K}$ and $K^{\prime}\in\mathbf{K}^{\prime}$.

###### Proof.

Every language in $\mathbf{K}\cup\mathbf{K}^{\prime}$ is a Boolean combination
of languages in $\mathcal{D}$ and $L,L^{\prime}\in\mathcal{D}$. Therefore,
there exists a finite lattice $\mathcal{C}\subseteq\mathcal{D}$ satisfying the
two following properties:

  1. (1)

$L,L^{\prime}\in\mathcal{C}$ and,

  2. (2)

every language $K\in\mathbf{K}\cup\mathbf{K}^{\prime}$ belongs to
${Bool\/}(\mathcal{C})$.

We define $\mathcal{F}$ as the least lattice such that
$HH^{\prime}\in\mathcal{F}$ for every $H,H^{\prime}\in\mathcal{C}$. We know
that $\mathcal{C}$ is finite, $\mathcal{C}\subseteq\mathcal{D}$ and
$\mathcal{D}$ is a lattice closed under concatenation. Thus, $\mathcal{F}$ is
a finite lattice such that $\mathcal{F}\subseteq\mathcal{D}$. It follows that
${Bool\/}(\mathcal{F})$ is a finite Boolean algebra such that
${Bool\/}(\mathcal{F})\subseteq{Bool\/}(\mathcal{D})$.

Consider the canonical equivalence $\sim_{{Bool\/}(\mathcal{F})}$ associated
to ${Bool\/}(\mathcal{F})$ (it relates words that belong to the same languages
of ${Bool\/}(\mathcal{F})$, see Section 2). Since
$L,L^{\prime}\in\mathcal{C}$, it is immediate by definition of $\mathcal{F}$
that we have $LL^{\prime}\in\mathcal{F}\subseteq{Bool\/}(\mathcal{F})$.
Therefore, Lemma 2.6 implies that $LL^{\prime}$ is a union of
$\sim_{{Bool\/}(\mathcal{F})}$-classes. We let $\mathbf{H}$ be the set
consisting of all these $\sim_{{Bool\/}(\mathcal{F})}$-classes. By definition,
$\mathbf{H}$ is a ${Bool\/}(\mathcal{F})$-cover of $LL^{\prime}$ and therefore
a ${Bool\/}(\mathcal{D})$-cover as well since
${Bool\/}(\mathcal{F})\subseteq{Bool\/}(\mathcal{D})$. It remains to prove
that for every $H\in\mathbf{H}$, we have $H\subseteq KK^{\prime}$ for some
$K\in\mathbf{K}$ and $K^{\prime}\in\mathbf{K}^{\prime}$. We fix
$H\in\mathbf{H}$ for the proof. We use the following fact.

######  Fact 3.5.

Consider a finite language $G\subseteq H$. Then, there exists $K\in\mathbf{K}$
and $K^{\prime}\in\mathbf{K}^{\prime}$ such that $G\subseteq KK^{\prime}$.

Let us first admit Fact 3.5 and apply it to finish the main proof. For every
$n\in{\rm Nature}$, we let $G_{n}\subseteq H$ be the finite language
containing all words of length at most $n$ in $H$. Clearly, we have,

$H=\bigcup_{n\in{\rm Nature}}G_{n}\quad\text{and}\quad G_{n}\subseteq
G_{n+1}\text{ for all $n\in{\rm Nature}$}.$

For every $n\in{\rm Nature}$, Fact 3.5 yields $K_{n}\in\mathbf{K}$ and
$K_{n}^{\prime}\in\mathbf{K}^{\prime}$ such that $G_{n}\subseteq
K_{n}K_{n}^{\prime}$. Since $\mathbf{K}$ and $\mathbf{K}^{\prime}$ are finite
sets, there exist $K\in\mathbf{K}$ and $K^{\prime}\in\mathbf{K}^{\prime}$ such
that $K_{n}=K$ and $K^{\prime}_{n}=K^{\prime}$ for infinitely many $n$. Since
$G_{n}\subseteq G_{n+1}$ for all $n$, it follows that $G_{n}\subseteq
KK^{\prime}$ for every $n\in{\rm Nature}$. Finally, since $H=\bigcup_{n\in{\rm
Nature}}G_{n}$, this implies $H\subseteq KK^{\prime}$, finishing the proof.

It remains to prove Fact 3.5. Consider a finite language $G\subseteq H$ and
let $G=\\{w_{1},\dots,w_{n}\\}$. We exhibit $K\in\mathbf{K}$ and
$K^{\prime}\in\mathbf{K}^{\prime}$ such that $G\subseteq KK^{\prime}$.

By definition, $H$ is a $\sim_{{Bool\/}(\mathcal{F})}$-class included in
$LL^{\prime}$. This implies that $w_{1},\dots,w_{n}\in LL^{\prime}$ and
$w_{1}\sim_{{Bool\/}(\mathcal{F})}\cdots\sim_{{Bool\/}(\mathcal{F})}w_{n}$.
Using these equivalences, we first prove the following claim which involves
the canonical preorder $\leqslant_{\mathcal{C}}$ associated to the finite
lattice $\mathcal{C}$.

######  Claim.

For every $u,v\in A^{*}$ such that $w_{n}=uv$, there exist
$u_{1},\dots,u_{n},v_{1},\dots,v_{n}\in A^{*}$ such that $w_{i}=u_{i}v_{i}$
for every $i\leq n$,
$u\leqslant_{\mathcal{C}}u_{1}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}u_{n}$
and
$v\leqslant_{\mathcal{C}}v_{1}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}v_{n}$.

###### Proof.

We prove the existence of $u_{1},v_{1}\in A^{*}$ such that $w_{1}=u_{1}v_{1}$,
$u\leqslant_{\mathcal{C}}u_{1}$ and $v\leqslant_{\mathcal{C}}v_{1}$ using the
hypothesis that $w_{n}=uv$ and $w_{n}\sim_{{Bool\/}(\mathcal{F})}w_{1}$. One
may then iterate the argument to build $u_{2},\dots,u_{n}\in A^{*}$ and
$v_{2},\dots,v_{n}\in A^{*}$ since
$w_{1}\sim_{{Bool\/}(\mathcal{F})}\cdots\sim_{{Bool\/}(\mathcal{F})}w_{n}$.

Consider the languages $U={\mathord{\uparrow}_{\mathcal{C}}\,u}$ and
$V={\mathord{\uparrow}_{\mathcal{C}}\,v}$ (the upper sets of $u$ and $v$ for
$\leqslant_{\mathcal{C}}$). By Lemma 2.5, we have $U,V\in\mathcal{C}$.
Therefore, we have $UV\in\mathcal{F}$ by definition of $\mathcal{F}$. Clearly,
$w_{n}=uv\in UV$. Therefore, $w_{n}\sim_{{Bool\/}(\mathcal{F})}w_{1}$ implies
that $w_{1}\in UV$. This yields a decomposition $w_{1}=u_{1}v_{1}$ with
$u_{1}\in U$ and $v_{1}\in V$. By definition of $U,V$, this implies
$u\leqslant_{\mathcal{C}}u_{1}$ and $v\leqslant_{\mathcal{C}}v_{1}$, finishing
the proof. ∎

Since $w_{n}\in LL^{\prime}$, it admits at least one decomposition $w_{n}=uv$
with $u\in L$ and $v\in L^{\prime}$. Therefore, we may apply the claim: there
exist $u_{1,1},\dots,u_{n,1},v_{1,1},\dots,v_{n,1}\in A^{*}$ such that
$w_{i}=u_{i,1}v_{i,1}$ for every $i\leq n$,
$u\leqslant_{\mathcal{C}}u_{1,1}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}u_{n,1}$
and
$v\leqslant_{\mathcal{C}}v_{1,1}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}v_{n,1}$.
Since $w_{n}=u_{n,1}v_{n,1}$, one can repeat the argument any number of times,
say $m$, to obtain words $u_{i,j},v_{i,j}$ for $1\leqslant i\leqslant n$ and
$1\leqslant j\leqslant m$, such that for all such $i,j$, we have
$w_{i}=u_{i,j}v_{i,j}$, and:

$\displaystyle u$
$\displaystyle\leqslant_{\mathcal{C}}u_{1,1}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}u_{n,1}\qquad\text{and}\qquad$
$\displaystyle v$
$\displaystyle\leqslant_{\mathcal{C}}v_{1,1}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}v_{n,1},$
$\displaystyle u_{n,1}$
$\displaystyle\leqslant_{\mathcal{C}}u_{1,2}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}u_{n,2}\qquad\text{and}\qquad$
$\displaystyle v_{n,1}$
$\displaystyle\leqslant_{\mathcal{C}}v_{1,2}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}v_{n,2},$
$\displaystyle\ \cdots\qquad$ $\displaystyle u_{n,m-1}$
$\displaystyle\leqslant_{\mathcal{C}}u_{1,m}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}u_{n,m}\quad\
\,\text{and}\qquad$ $\displaystyle v_{n,m-1}$
$\displaystyle\leqslant_{\mathcal{C}}v_{1,m}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}v_{n,m}.$

Moreover, since $w_{1}$ is a finite word, it admits finitely many
decompositions $w_{1}=u_{1}v_{1}$ with $u_{1},v_{1}\in A^{*}$. Therefore, the
pigeonhole principle yields two integers $j<k$ such that $u_{1,j}=u_{1,k}$
(and therefore $v_{1,j}=v_{1,k}$), which gives words
$u_{1},\dots,u_{n},v_{1},\dots,v_{n}\in A^{*}$ such that $w_{i}=u_{i}v_{i}$
for every $i\leq n$ and,

$u\leqslant_{\mathcal{C}}u_{1}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}u_{n}\leqslant_{\mathcal{C}}u_{1}\qquad
v\leqslant_{\mathcal{C}}v_{1}\leqslant_{\mathcal{C}}\cdots\leqslant_{\mathcal{C}}v_{n}\leqslant_{\mathcal{C}}v_{1}.$

Since $u\in L$, $v\in L^{\prime}$ and $L,L^{\prime}\in\mathcal{C}$ by
definition of $\mathcal{C}$, we get that $u_{1}\in L$ and $v_{1}\in
L^{\prime}$ by definition of $\leqslant_{\mathcal{C}}$. Therefore, since
$\mathbf{K}$ and $\mathbf{K}^{\prime}$ are covers of $L$ and $L^{\prime}$
respectively, there exist $K\in\mathbf{K}$ and
$K^{\prime}\in\mathbf{K}^{\prime}$ such that $u_{1}\in K$ and $v_{1}\in
K^{\prime}$.

Moreover, one may verify from the definitions that for every $x,y\in A^{*}$,
$x\leqslant_{\mathcal{C}}y$ and $y\leqslant_{\mathcal{C}}x$ imply that
$x\sim_{{Bool\/}(\mathcal{C})}y$. Therefore, the above implies that,

$u_{1}\sim_{{Bool\/}(\mathcal{C})}\cdots\sim_{{Bool\/}(\mathcal{C})}u_{n}\qquad
v_{1}\sim_{{Bool\/}(\mathcal{C})}\cdots\sim_{{Bool\/}(\mathcal{C})}v_{n}.$

Therefore, since $K,K^{\prime}\in{Bool\/}(\mathcal{C})$ by definition of
$\mathcal{C}$, it is immediate that $u_{1},\dots,u_{n}\in K$ and
$v_{1},\dots,v_{n}\in K^{\prime}$. Altogether, we obtain that
$G=\\{u_{1}v_{1},\dots,u_{n}v_{n}\\}\subseteq KK^{\prime}$, finishing the
proof. ∎

Finally, we shall need the following variant of Lemma 3.4, which considers
marked concatenation instead of standard concatenation. The proof is identical
to the one of Lemma 3.4 and left to the reader.

######  Lemma 3.6.

Let $\mathcal{D}$ be a lattice closed under marked concatenation. Consider
$L,L^{\prime}\in\mathcal{D}$ and $a\in A$, and let
$\mathbf{K},\mathbf{K}^{\prime}$ be ${Bool\/}(\mathcal{D})$-covers of $L$ and
$L^{\prime}$ respectively. There exists a ${Bool\/}(\mathcal{D})$-cover
$\mathbf{H}$ of $LaL^{\prime}$ such that for every $H\in\mathbf{H}$, we have
$H\subseteq KaK^{\prime}$ for some $K\in\mathbf{K}$ and
$K^{\prime}\in\mathbf{K}^{\prime}$.

###  3.2. Main theorem

We may now state the main theorem of the paper: whenever $\mathcal{C}$ is a
_finite_ quotient-closed Boolean algebra, ${BPol\/}(\mathcal{C})$-separation
and ${BPol\/}(\mathcal{C})$-covering are both decidable.

######  Theorem 3.7.

Let $\mathcal{C}$ be a finite quotient-closed Boolean algebra. Then,
separation and covering are decidable for ${BPol\/}(\mathcal{C})$.

Before we detail the applications of Theorem 3.7, let us make an important
observation. This result completes an earlier one presented in [Pla18] which
applies to classes of the form ${Pol\/}(\mathcal{C})$ and
${Pol\/}({BPol\/}(\mathcal{C}))$ (when $\mathcal{C}$ is a finite quotient-
closed Boolean algebra). Let us recall this result.

######  Theorem 3.8 ([Pla18]).

Let $\mathcal{C}$ be a finite quotient-closed Boolean algebra. Then,
separation and covering are decidable for ${Pol\/}(\mathcal{C})$ and
${Pol\/}({BPol\/}(\mathcal{C}))$.

An important point is that while ${BPol\/}(\mathcal{C})$ is an intermediary
class between ${Pol\/}(\mathcal{C})$ and ${Pol\/}({BPol\/}(\mathcal{C}))$, the
proof of Theorem 3.7 involves ideas which are very different from those used
in [Pla18] to prove Theorem 3.8. This is not surprising and we already
mentioned the reason above: unlike ${Pol\/}(\mathcal{C})$ and
${Pol\/}({BPol\/}(\mathcal{C}))$, the class ${BPol\/}(\mathcal{C})$ is not
closed under concatenation in general. This difference is significant since
most of the techniques we have for handling covering rely heavily on
concatenation. In practice, this means that Boolean closure is harder to
handle than polynomial closure, at least with such techniques.

However, we do reuse a result of [Pla18] to prove Theorem 3.7. More precisely,
it turns out that the arguments for handling ${BPol\/}(\mathcal{C})$ (in this
paper) and ${Pol\/}({BPol\/}(\mathcal{C}))$ (in [Pla18]) both exploit the same
subresult for the simpler class ${Pol\/}(\mathcal{C})$ (albeit in very
different ways). This subresult is stronger than the decidability of
${Pol\/}(\mathcal{C})$-covering and is proved in [Pla18]. We recall it in
Section 7. However, it is important to keep in mind that from this preliminary
result for ${Pol\/}(\mathcal{C})$, the arguments for ${BPol\/}(\mathcal{C})$
and ${Pol\/}({BPol\/}(\mathcal{C}))$ build in orthogonal directions.

######  Remark 3.9.

This discussion might seem surprising. Indeed, by definition,
${Pol\/}({BPol\/}(\mathcal{C}))$ is built from ${BPol\/}(\mathcal{C})$ using
polynomial closure. Hence, intuition suggests that one needs some knowledge
about the latter to handle the former. However, this is not the case as
Boolean closure can be bypassed in the definition of
${Pol\/}({BPol\/}(\mathcal{C}))$. Specifically, one may prove that
${Pol\/}({BPol\/}(\mathcal{C}))={Pol\/}({co\/}\textup{-}{\it
Pol\/}(\mathcal{C}))$ where ${co\/}\textup{-}{\it Pol\/}(\mathcal{C})$ is the
class containing all complements of languages in ${Pol\/}(\mathcal{C})$. This
is exactly how the class ${Pol\/}({BPol\/}(\mathcal{C}))$ is handled in
[Pla18].

The remaining sections of the paper are devoted to proving Theorem 3.7. We
rely on a framework which was designed in [PZ18a] for the specific purpose of
handling the covering problem. We recall it in Section 4. The algorithm for
${BPol\/}(\mathcal{C})$-covering is presented in Section 5. The remaining
sections are then devoted to the correction proof of this algorithm. However,
let us first conclude the current section by detailing the important
applications of Theorem 3.7.

###  3.3. Applications of the main theorem

Classes of the form ${BPol\/}(\mathcal{C})$ are important: they are involved
in natural hierarchies of classes of languages, called _concatenation
hierarchies_. Let us briefly recall what they are (we refer the reader to
[PZ18b] for a detailed presentation). A particular concatenation hierarchy
depends on a single parameter: an arbitrary quotient-closed Boolean algebra of
regular languages $\mathcal{C}$, called its _basis_. Once the basis is chosen,
the construction is uniform. Languages are classified into levels of two
kinds: full levels (denoted by 0, 1, 2,…) and half levels (denoted by 1/2,
3/2, 5/2,…):

  * •

Level $0$ is the basis (_i.e._ , our parameter class $\mathcal{C}$).

  * •

Each _half level_ $n+\frac{1}{2}$, for $n\in{\rm Nature}$, is the _polynomial
closure_ of the previous full level, _i.e._ , of level $n$.

  * •

Each _full level_ $n+1$, for $n\in{\rm Nature}$, is the _Boolean closure_ of
the previous half level, _i.e._ , of level $n+\frac{1}{2}$.

The generic process is depicted in the following figure.

$0$$\frac{1}{2}$$1$$\frac{3}{2}$$2$$\frac{5}{2}$$Pol$$Bool$$Pol$$Bool$$Pol$

Hence, a reformulation of Theorem 3.7 is that for any concatenation hierarchy
whose basis is _finite_ , separation is decidable for level one. There are two
prominent examples of finitely based hierarchies:

  * •

The _Straubing-Thérien_ hierarchy [Str81, Thé81], whose basis is the class
$\\{\emptyset,A^{*}\\}$.

  * •

The _dot-depth_ hierarchy of Brzozowski and Cohen [BC71], whose basis is the
class $\\{\emptyset,\\{\varepsilon\\},A^{+},A^{*}\\}$.

Consequently, Theorem 3.7 implies that separation and covering are decidable
for level one in these two hierarchies. These are not new results. By
definition, level one in the Straubing-Thérien hierarchy is exactly the class
of _piecewise testable languages_. For this class, separation has been solved
in [CMM13, PvRZ13] and covering has been solved in [PZ18a]. For dot-depth one,
the decidability of covering and separation was originally obtained
indirectly. Indeed, it is known [PZ20] that separation and covering for any
level in the dot-depth hierarchy reduce to the same problem for the
corresponding level in the Straubing-Thérien hierarchy. Therefore, while the
decidability of separation and covering for dot-depth one is not a new result,
an advantage of Theorem 3.7 is that we obtain a new _direct_ proof of this
result.

However, these are not the main applications of Theorem 3.7. It turns out that
the theorem also applies to level two in the Straubing-Thérien hierarchy.
Indeed, it is known that this level is also level one in another finitely
based concatenation hierarchy. More precisely, recall the class and presented
in Example 2.7: it consists of all Boolean combinations of languages
$A^{*}aA^{*}$, for some $a\in A$. It is straightforward to verify that and is
a finite quotient-closed Boolean algebra. The following theorem was shown in
[PS85] (see also [PZ18a] for a recent proof).

######  Theorem 3.10 ([PS85]).

Level two in the Straubing-Thérien hierarchy is exactly the class
${BPol\/}(\and)$.

In view of Theorem 3.10, we obtain the following immediate corollary of
Theorem 3.7.

######  Corollary 3.11.

Separation and covering are decidable for level two in the Straubing-Thérien
hierarchy.

Finally, this result may be lifted to dot-depth two using again the generic
transfer theorem proved in [PZ20]. Hence, we obtain the following additional
corollary.

######  Corollary 3.12.

Separation and covering are decidable for dot-depth two.

######  Remark 3.13.

Logical characterizations of these two hierarchies are known (see [Tho82] for
the dot-depth hierarchy and [PP86] for the Straubing-Thérien hierarchy). Each
of them corresponds to a quantifier alternation hierarchy within a particular
variant of first-order logic over words. The two variants differ by the set of
predicates which are allowed in sentence (they have the same overall
expressive power, but this changes the levels in their respective quantifier
alternation hierarchies). We refer the reader to [PZ18b] for details and a
recent proof of these results.

In particular, level two in the Straubing-Thérien hierarchy corresponds to a
logic denoted by $\mathcal{B}\Sigma_{2}(<)$ and dot-depth two corresponds to
another logic denoted by $\mathcal{B}\Sigma_{2}(<,+1)$. Hence, our results
also imply that covering and separation are decidable for these two logics.

##  4\. Framework: rating maps and optimal covers

In this section, we present the framework which we use to formulate our
covering algorithm for ${BPol\/}(\mathcal{C})$ (when $\mathcal{C}$ is a finite
quotient-closed Boolean algebra) announced in Theorem 3.7. The framework
itself was designed and applied to several specific classes in [PZ18a].
Moreover, it was also used in [Pla18] to formulate algorithms for
${Pol\/}(\mathcal{C})$\- and ${Pol\/}({BPol\/}(\mathcal{C}))$-covering. Here,
we recall the part of this framework that we shall actually need in the paper.
We refer the reader to [PZ18a] for a complete and detailed presentation.

Consider a lattice $\mathcal{D}$. In $\mathcal{D}$-covering, the input is a
pair $(L,\mathbf{L})$ where $L$ is a regular language and $\mathbf{L}$ a
finite set of regular languages: we have to decide whether there exists a
$\mathcal{D}$-cover of $L$ which is separating for $\mathbf{L}$. The main idea
in the framework of [PZ18a] is to replace the set $\mathbf{L}$ by a (more
general) algebraic object called _rating map_. Intuitively, rating maps are
designed to measure the quality of $\mathcal{D}$-covers. Given a rating map
$\rho$ and a language $L$, we use $\rho$ to rank the existing
$\mathcal{D}$-covers of $L$. This leads to the definition of “optimal”
$\mathcal{D}$-cover of $L$. We are then able to reformulate
$\mathcal{D}$-covering with these notions. Instead of deciding whether
$(L,\mathbf{L})$ is $\mathcal{D}$-coverable, we compute an optimal
$\mathcal{D}$-cover for $L$ for a rating map $\rho$ that we build from
$\mathbf{L}$. An advantage of this approach is that it yields elegant
formulations for the covering algorithms which are formulated with it. We
refer the reader to [PZ18a] and [Pla18] for examples (in addition to
${BPol\/}(\mathcal{C})$ which is presented in this paper). Another important
motivation for using this framework is that in order to handle
${BPol\/}(\mathcal{C})$, we require a result for the simpler class
${Pol\/}(\mathcal{C})$ which is stronger than the decidability of covering
(this result is proved in [Pla18]). The framework of [PZ18a] is designed to
formulate this result.

We start by defining rating maps. Then, we explain how they are used to
measure the quality of a cover and define optimal covers. Finally, we connect
these notions to the covering problem. Let us point out that several
statements presented here are without proof. We refer the reader to [PZ18a]
for these proofs.

###  4.1. Rating maps

Rating maps involve commutative and idempotent monoids. We shall write such
monoids $(R,+)$: we call the binary operation “$+$” _addition_ and denote the
neutral element by $0_{R}$. Being idempotent means that for all $r\in R$, we
have $r+r=r$. Observe that for every commutative and idempotent monoid
$(R,+)$, we may define a canonical ordering $\leq$ over $R$:

$\text{For all }r,s\in R,\quad r\leq s\text{ when }r+s=s.$

It is straightforward to verify that $\leq$ is a partial order which is
compatible with addition. Moreover, we have the following fact which is
immediate from the definitions.

######  Fact 4.1.

Let $(R,+)$ and $(Q,+)$ be two commutative and idempotent monoids. Moreover,
let $\gamma:(R,+)\to(Q,+)$ be a morphism. Then, $\gamma$ is increasing: for
every $s,t\in R$ such that $s\leq t$, we have $\gamma(s)\leq\gamma(t)$.

######  Example 4.2.

For any set $E$, it is immediate that $(2^{E},\cup)$ is an idempotent and
commutative monoid. The neutral element is $\emptyset$. Moreover, the
canonical ordering is set inclusion.

When manipulating the subsets of a commutative and idempotent monoid $(R,+)$
we shall often need to apply a _downset operation_. Given $S\subseteq R$, we
write $\mathord{\downarrow_{R}}S$ for the set,

$\mathord{\downarrow_{R}}S=\\{r\in R\mid r\leq s\text{ for some $s\in S$}\\}.$

We extend this notation to Cartesian products of arbitrary sets with $R$.
Given some set $X$ and a subset $S\subseteq X\times R$, we write
$\mathord{\downarrow_{R}}S$ for the set,

$\mathord{\downarrow_{R}}S=\\{(x,r)\in X\times R\mid\text{there exists $q\in
R$ such that $r\leq q$ and $(x,q)\in S$}\\}.$

We may now define rating maps. A _rating map_ is a morphism
$\rho:(2^{A^{*}},\cup)\to(R,+)$ where $(R,+)$ is a _finite_ idempotent and
commutative monoid called the _rating set of $\rho$_. That is, $\rho$ is a map
from $2^{A^{*}}$ to $R$ satisfying the following properties:

  1. (1)

$\rho(\emptyset)=0_{R}$.

  2. (2)

For all $K_{1},K_{2}\subseteq A^{*}$, $\rho(K_{1}\cup
K_{2})=\rho(K_{1})+\rho(K_{2})$.

For the sake of improved readability, when applying a rating map $\rho$ to a
singleton set $K=\\{w\\}$, we shall write $\rho(w)$ for $\rho(\\{w\\})$.
Additionally, we write $\rho_{*}:A^{*}\to R$ for the restriction of $\rho$ to
$A^{*}$: for every $w\in A^{*}$, we have $\rho_{*}(w)=\rho(w)$ (this notation
allows us to write $\rho_{*}^{-1}(r)\subseteq A^{*}$ for the language of all
words $w\in A^{*}$ such that $\rho(w)=r$).

Most of the statements involved in our framework make sense for arbitrary
rating maps. However, we shall often have to work with special rating maps
which satisfy additional properties. We present them now.

Nice rating maps. A rating map $\rho:2^{A^{*}}\to R$ is nice when, for every
language $K\subseteq A^{*}$, there exist finitely many words
$w_{1},\dots,w_{n}\in K$ such that $\rho(K)=\rho(w_{1})+\cdots+\rho(w_{k})$.

Observe that in this case, $\rho$ is characterized by the canonical map
$\rho_{*}:A^{*}\to R$. Indeed, for every language $K$, we may consider the sum
of all elements $\rho(w)$ for $w\in K$: while it may be infinite, it boils
down to a finite one since $R$ is commutative and idempotent. The hypothesis
that $\rho$ is nice implies that $\rho(K)$ is equal to this sum.

Multiplicative rating maps. A rating map $\rho:2^{A^{*}}\to R$ is
multiplicative when its rating set $R$ has more structure: it needs to be an
_idempotent semiring_. Moreover, $\rho$ has to satisfy an additional property
connecting this structure to language concatenation. Namely, it has to be a
morphism of semirings.

A _semiring_ is a tuple $(R,+,\cdot)$ where $R$ is a set and “$+$” and
“$\cdot$” are two binary operations called addition and multiplication, such
that the following axioms are satisfied:

  * •

$(R,+)$ is a commutative monoid (the neutral element is denoted by $0_{R}$).

  * •

$(R,\cdot)$ is a monoid (the neutral element is denoted by $1_{R}$).

  * •

Multiplication distributes over addition: $r\cdot(s+t)=(r\cdot s)+(r\cdot t)$
and $(r+s)\cdot t=(r\cdot t)+(s\cdot t)$ for every $r,s,t\in R$.

  * •

The neutral element of $(R,+)$ is a zero for $(R,\cdot)$: $0_{R}\cdot r=r\cdot
0_{R}=0_{R}$ for every $r\in R$.

We say that a semiring $R$ is _idempotent_ when $r+r=r$ for every $r\in R$,
_i.e._ , when the additive monoid $(R,+)$ is idempotent (on the other hand,
there is no additional constraint on the multiplicative monoid $(R,\cdot)$).

######  Example 4.3.

A key example of infinite idempotent semiring is the set $2^{A^{*}}$ of all
languages over $A$. Union is the addition (with $\emptyset$ as neutral
element) and concatenation is the multiplication (with $\\{\varepsilon\\}$ as
neutral element).

Clearly, any finite idempotent semiring $(R,+,\cdot)$ is in particular a
rating set: $(R,+)$ is an idempotent and commutative monoid. In particular,
one may verify that the canonical ordering “$\leq$” on $R$, is compatible with
multiplication as well.

We may now define multiplicative rating maps: as expected they are semiring
morphisms. Let $\rho:2^{A^{*}}\to R$ be a rating map. By definition, this
means that the rating set $(R,+)$ is a finite idempotent commutative monoid
and that $\rho$ is a monoid morphism from $(2^{A^{*}},\cup)$ to $(R,+)$. We
say that $\rho$ is multiplicative when the rating set $R$ is equipped with a
second binary operation “$\cdot$” such that $(R,+,\cdot)$ is an idempotent
semiring and $\rho$ is also a monoid morphism from $(2^{A^{*}},\cdot)$ to
$(R,\cdot)$. In other words, the two following additional axioms hold:

  1. (3)

$\rho(\varepsilon)=1_{R}$.

  2. (4)

For all $K_{1},K_{2}\subseteq A^{*}$, we have
$\rho(K_{1}K_{2})=\rho(K_{1})\cdot\rho(K_{2})$.

######  Remark 4.4.

An important point is that the rating maps which are both nice and
multiplicative are finitely representable. As we explained above, a nice
rating map $\rho:2^{A^{*}}\to R$ is characterized by the canonical map
$\rho_{*}:A^{*}\to R$. Moreover, when $\rho$ is multiplicative as well,
$\rho_{*}$ is finitely representable: it is a morphism into a finite monoid.
Thus, we may consider algorithms taking nice multiplicative rating maps as
input. Let us point out that the rating maps which are not nice and
multiplicative remain important. We often deal with them in our proofs.

###  4.2. Imprints and optimal covers

We now explain how we use rating maps to measure the quality of covers. This
involves an additional notion: “imprints”. Consider a rating map
$\rho:2^{A^{*}}\to R$. For any finite set of languages $\mathbf{K}$, the
$\rho$-imprint of $\mathbf{K}$ (denoted by
$\mathcal{I}[\rho](\mathbf{K})\subseteq R$) is the following set:

$\begin{array}[]{lll}\mathcal{I}[\rho](\mathbf{K})&=&\mathord{\downarrow_{R}}\\{\rho(K)\mid
K\in\mathbf{K}\\}\subseteq R\\\ &=&\\{r\in R\mid\text{there exists
$K\in\mathbf{K}$ such that $r\leq\rho(K)$}\\}.\end{array}$

When using this notion, we shall have some language $L\subseteq A^{*}$ in
hand: our goal is to find the “best possible” cover $\mathbf{K}$ of $L$.
Intuitively, $\rho$-imprints measure the “quality” of candidate covers
$\mathbf{K}$ (the smaller the $\rho$-imprint, the better the quality).

This leads to the notion of optimality. Let $\mathcal{D}$ be an arbitrary
lattice. Given a language $L$, an _optimal $\mathcal{D}$-cover of $L$ for
$\rho$_ is a $\mathcal{D}$-cover of $L$ which has the smallest possible
$\rho$-imprint (with respect to inclusion). That is, $\mathbf{K}$ is an
optimal $\mathcal{D}$-cover of $L$ for $\rho$ if and only if,

$\mathcal{I}[\rho](\mathbf{K})\subseteq\mathcal{I}[\rho](\mathbf{K}^{\prime})\quad\text{for
every $\mathcal{D}$-cover $\mathbf{K}^{\prime}$ of $L$}$

Furthermore, in the special case when $L=A^{*}$, we speak of optimal
_universal_ $\mathcal{D}$-cover for $\rho$.

In general, given an arbitrary language $L$, there are infinitely many optimal
$\mathcal{D}$-covers of $L$ for $\rho$. However, there always exists at least
one (this requires the hypothesis that $\mathcal{D}$ is a lattice, see Lemma
4.15 in [PZ18a] for the proof).

######  Lemma 4.5.

Let $\mathcal{D}$ be a lattice. Then, for any rating map $\rho:2^{A^{*}}\to R$
and any language $L\subseteq A^{*}$, there exists an optimal
$\mathcal{D}$-cover of $L$ for $\rho$.

It is important to note that the proof of Lemma 4.5 is non-constructive: given
$L$ and $\rho:2^{A^{*}}\to R$, computing an actual optimal $\mathcal{D}$-cover
of $L$ for $\rho$ is a difficult problem in general. As seen below, getting
such algorithm (in the special case when $\rho$ is nice and multiplicative)
yields a procedure for $\mathcal{D}$-covering. Before we can establish this
connection precisely, we require a key observation about optimal
$\mathcal{D}$-covers.

Optimal imprints. By definition, given a language $L$, all optimal
$\mathcal{D}$-covers of $L$ for $\rho$ have the same $\rho$-imprint. Hence,
this unique $\rho$-imprint is a _canonical_ object for $\mathcal{D}$, $L$ and
$\rho$. We call it the _$\mathcal{D}$ -optimal $\rho$-imprint on $L$_ and we
denote it by $\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]$:

$\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]=\mathcal{I}[\rho](\mathbf{K})\subseteq
R\quad\text{for every optimal $\mathcal{D}$-cover $\mathbf{K}$ of $L$ for
$\rho$}.$

Additionally, in the particular case when $L=A^{*}$, we shall speak of
_$\mathcal{D}$ -optimal universal $\rho$-imprint_ and write
$\mathcal{I}_{\mathcal{D}}\left[\rho\right]$ for
$\mathcal{I}_{\mathcal{D}}\left[A^{*},\rho\right]$.

We complete these definitions with a few properties of optimal imprints. We
start with a straightforward fact which compares the optimal imprints on
languages which are comparable with inclusion. The proof is available in
[PZ18a, Fact 4.17].

######  Fact 4.6.

Consider a rating map $\rho:2^{A^{*}}\to R$ and a lattice $\mathcal{D}$. Let
$H,L$ be two languages such that $H\subseteq L$. Then,
$\mathcal{I}_{\mathcal{D}}\left[H,\rho\right]\subseteq\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]$.

More precisely, the following fact connects optimal imprints with union of
languages.

######  Fact 4.7.

Let $\rho:2^{A^{*}}\to R$ be a rating map and consider two languages $H,L$.
Then, for every lattice $\mathcal{D}$, we have
$\mathcal{I}_{\mathcal{D}}\left[H\cup
L,\rho\right]=\mathcal{I}_{\mathcal{D}}\left[H,\rho\right]\cup\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]$.

###### Proof.

We already know that
$\mathcal{I}_{\mathcal{D}}\left[H,\rho\right]\subseteq\mathcal{I}_{\mathcal{D}}\left[H\cup
L,\rho\right]$ and
$\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]\subseteq\mathcal{I}_{\mathcal{D}}\left[H\cup
L,\rho\right]$ by Fact 4.6. Therefore, the inclusion
$\mathcal{I}_{\mathcal{D}}\left[H,\rho\right]\cup\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]\subseteq\mathcal{I}_{\mathcal{D}}\left[H\cup
L,\rho\right]$ is immediate. We prove the converse one. Let
$r\in\mathcal{I}_{\mathcal{D}}\left[H\cup L,\rho\right]$. We let
$\mathbf{K}_{H}$ and $\mathbf{K}_{L}$ be optimal $\mathcal{D}$-covers of $H$
and $L$ respectively (for $\rho$). Clearly, $\mathbf{K}_{H}\cup\mathbf{K}_{L}$
is a cover $H\cup L$. Therefore, $r\in\mathcal{I}_{\mathcal{D}}\left[H\cup
L,\rho\right]$ implies that
$r\in\mathcal{I}[\rho](\mathbf{K}_{H}\cup\mathbf{K}_{L})$. Hence, there exists
$K\in\mathbf{K}_{H}\cup\mathbf{K}_{L}$ such that $r\leq\rho(K)$. Then, either
$K\in\mathbf{K}_{H}$ which implies
$r\in\mathcal{I}[\rho](\mathbf{K}_{H})=\mathcal{I}_{\mathcal{D}}\left[H,\rho\right]$
or $K\in\mathbf{K}_{L}$ which implies
$r\in\mathcal{I}[\rho](\mathbf{K}_{L})=\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]$.
Altogether, we get
$r\in\mathcal{I}_{\mathcal{D}}\left[H,\rho\right]\cup\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]$,
finishing the proof. ∎

###  4.3. Connection with the covering problem

Finally, we explain how rating maps are used for handling the covering
problem.

Given a lattice $\mathcal{D}$, it turns out that the $\mathcal{D}$-covering
problem reduces to another problem whose input is a nice multiplicative rating
map. Let us point out that _two_ reductions of this kind are presented in
[PZ18a]. The first one is simpler but restricted to classes $\mathcal{D}$
which are Boolean algebras. On the other hand, the second one applies to all
lattices but requires working with more involved objects.

In the paper, we investigate classes of the form ${BPol\/}(\mathcal{C})$ which
are Boolean algebras. Hence, we shall mostly work with the first variant whose
statement is as follows (we refer the reader to [PZ18a] for the proof).

######  Proposition 4.8 ([PZ18a]).

Let $\mathcal{D}$ be a Boolean algebra. Assume that there exists an algorithm
for the following computational problem:

Input: |  A nice multiplicative rating map $\rho:2^{A^{*}}\to R$.
---|---
Output: |  Compute the $\mathcal{D}$-optimal universal $\rho$-imprint, $\mathcal{I}_{\mathcal{D}}\left[\rho\right]$.

Then, $\mathcal{D}$-covering is decidable.

Additionally, we shall need in Section 6 to apply a theorem of [Pla18] for
classes of the form ${Pol\/}(\mathcal{C})$ (which are lattices but not Boolean
algebras) as a sub-result. Thus, we also recall the terminology associated to
the generalized reduction which holds for arbitrary lattices, since we need it
to state this theorem.

When working with an arbitrary lattice, one needs to consider slightly more
involved objects. Given a lattice $\mathcal{D}$, a map $\alpha:A^{*}\to M$
into a finite set $M$ (in practice, $\alpha$ will be a monoid morphism but
this is not required for the definition) and a rating map $\rho:2^{A^{*}}\to
R$, we write $\mathcal{P}_{\mathcal{D}}^{\alpha}[\rho]$ for the following set,

$\mathcal{P}_{\mathcal{D}}^{\alpha}[\rho]=\\{(s,r)\in M\times R\mid
r\in\mathcal{I}_{\mathcal{D}}\left[\alpha^{-1}(s),\rho\right]\\}\subseteq
M\times R$

We call $\mathcal{P}_{\mathcal{D}}^{\alpha}[\rho]$ the _$\alpha$ -pointed
$\mathcal{D}$-optimal $\rho$-imprint_. Clearly, it encodes all sets
$\mathcal{I}_{\mathcal{D}}\left[\alpha^{-1}(s),\rho\right]$ for $s\in M$. The
following statement is [Pla18, Proposition 5.18].

######  Proposition 4.9.

Consider a lattice $\mathcal{D}$ and some finite quotient-closed Boolean
algebra $\mathcal{C}$. Assume that there exists an algorithm for the following
computational problem:

Input: |  A $\mathcal{C}$-compatible morphism $\alpha:A^{*}\to M$ and
---|---
|  a nice multiplicative rating map $\rho:2^{A^{*}}\to R$.
Output: |  Compute the $\alpha$-pointed $\mathcal{D}$-optimal $\rho$-imprint, $\mathcal{P}_{\mathcal{D}}^{\alpha}[\rho]$.

Then, $\mathcal{D}$-covering is decidable.

##  5\. Characterization of ${BPol\/}(\mathcal{C})$-optimal imprints

We present a generic characterization of ${BPol\/}(\mathcal{C})$-optimal
imprints which holds when $\mathcal{C}$ is a finite quotient-closed Boolean
algebra. For the sake of avoiding clutter, we assume that the finite quotient-
closed Boolean algebra $\mathcal{C}$ is fixed for the whole section.

Given a _nice_ multiplicative rating map $\rho:2^{A^{*}}\to R$, we want to
characterize the set
$\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[\rho\right]\subseteq R$. An
important point is that we do not work directly with this set. Instead, we
characterize the family of all sets
$\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[D,\rho\right]\subseteq R$ where
$D\subseteq A^{*}$ is a $\sim_{\mathcal{C}}$-class. Note that this family of
sets record more information than just the set
$\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[\rho\right]$. Indeed, by Fact 4.7,
we have,

$\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[\rho\right]=\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[A^{*},\rho\right]=\bigcup_{D\in{A^{*}}/{\sim_{\mathcal{C}}}}\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[D,\rho\right].$

For the sake of convenience, we shall encode this family as a set of pairs in
$({A^{*}}/{\sim_{\mathcal{C}}})\times R$. Given a multiplicative rating map
$\rho:2^{A^{*}}\to R$, we define:

$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]=\\{(D,r)\in({A^{*}}/{\sim_{\mathcal{C}}})\times
R\mid r\in\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[D,\rho\right]\\}.$

When $\rho$ is nice, we characterize
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$ as the _greatest_
subset of $R$ satisfying specific properties. From the statement, it is
straightforward to obtain a greatest fixpoint procedure for computing
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$ from $\rho$. In
turns, this allows to compute
$\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[\rho\right]$ using the above
equality. By Proposition 4.8, this yields an algorithm for
${BPol\/}(\mathcal{C})$-covering, thus proving our main result: Theorem 3.7.

######  Remark 5.1.

This characterization is rather unique among the results that have been
obtained for other classes in [PZ18a] and [Pla18]. Typically, optimal imprints
are characterized as least subsets, not greatest ones.

######  Notation.

In our statements, we shall frequently manipulate subsets of
$({A^{*}}/{\sim_{\mathcal{C}}})\times R$. When doing so, the following
notation will be convenient. Given
$S\subseteq({A^{*}}/{\sim_{\mathcal{C}}})\times R$ and
$D\in{A^{*}}/{\sim_{\mathcal{C}}}$, we write,

$S(D)=\\{r\in R\mid(D,r)\in S\\}$

In particular, observe that
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho](D)=\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[D,\rho\right]$
by definition.

Given a multiplicative rating map $\rho:2^{A^{*}}\to R$, we define a notion of
${BPol\/}(\mathcal{C})$-saturated subset of
$({A^{*}}/{\sim_{\mathcal{C}}})\times R$ (for $\rho$). Our theorem then states
that when $\rho$ is nice, the greatest such subset is exactly
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$.

######  Remark 5.2.

The definition of ${BPol\/}(\mathcal{C})$-saturated sets makes sense
regardless of whether $\rho$ is nice. However, we need this hypothesis for the
greatest one to be $\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$.

The definition is based on an intermediary notion. With every set
$S\subseteq({A^{*}}/{\sim_{\mathcal{C}}})\times R$, we associate another set
$\mathcal{R}^{\rho}_{S}\subseteq({A^{*}}/{\sim_{\mathcal{C}}})\times R\times
2^{R}$. For the definition, we need to recall a few properties. Given a word
$w\in A^{*}$, we denote its $\sim_{\mathcal{C}}$ class by $[w]_{\mathcal{C}}$.
Moreover, since $\mathcal{C}$ is closed under quotients, Lemma 2.8 yields that
the equivalence $\sim_{\mathcal{C}}$ is a congruence. We denote by
“$\mathbin{\scriptscriptstyle\bullet}$” the multiplication of
$\sim_{\mathcal{C}}$-classes in the monoid ${A^{*}}/{\sim_{\mathcal{C}}}$.
Additionally, since $R$ is a semiring, $2^{R}$ is one as well for union as
addition and the natural multiplication lifted from the one of $R$ (for
$U,V\in 2^{R}$, $UV=\\{qr\mid q\in U\text{ and }r\in V\\}$).

We may now present our definition. Consider a set
$S\subseteq({A^{*}}/{\sim_{\mathcal{C}}})\times R$. We define
$\mathcal{R}^{\rho}_{S}$ as the least subset of
$({A^{*}}/{\sim_{\mathcal{C}}})\times R\times 2^{R}$ (with respect to
inclusion) which satisfies the following properties:

  * •

Trivial elements. For every $w\in A^{*}$, we have
$([w]_{\mathcal{C}},\rho(w),\\{\rho(w)\\})\in\mathcal{R}^{\rho}_{S}$.

  * •

Extended downset. For every $(C,q,U)\in\mathcal{R}^{\rho}_{S}$ and
$V\subseteq\mathord{\downarrow_{R}}U$, we have
$(C,q,V)\in\mathcal{R}^{\rho}_{S}$.

  * •

Multiplication. For every $(C,q,U),(D,r,V)\in\mathcal{R}^{\rho}_{S}$, we have
$(C\mathbin{\scriptscriptstyle\bullet}D,qr,UV)\in\mathcal{R}^{\rho}_{S}$.

  * •

$S$-restricted closure. For every triple of idempotents
$(E,f,F)\in\mathcal{R}^{\rho}_{S}$, we have
$(E,f,F\cdot S(E)\cdot F)\in\mathcal{R}^{\rho}_{S}$.

We are ready to define the ${BPol\/}(\mathcal{C})$-saturated subsets of
$({A^{*}}/{\sim_{\mathcal{C}}})\times R$. Consider a set
$S\subseteq({A^{*}}/{\sim_{\mathcal{C}}})\times R$. We say that $S$ is
_${BPol\/}(\mathcal{C})$ -saturated for $\rho$_ if the following property
holds:

$\begin{array}[]{c}\text{for every $(D,r)\in S$, there exist
$r_{1},\dots,r_{k}\in R$ such that,}\\\ \text{$r\leq r_{1}+\cdots+r_{k}$ and
$(D,r_{i},\\{r_{1}+\cdots+r_{k}\\})\in\mathcal{R}^{\rho}_{S}$ for every $i\leq
k$}\end{array}$ (1)

We now state our characterization of ${BPol\/}(\mathcal{C})$-optimal imprints
in the following theorem.

######  Theorem 5.3.

Let $\rho:2^{A^{*}}\to R$ be a nice multiplicative rating map. Then,
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$ is the greatest
${BPol\/}(\mathcal{C})$-saturated subset of
$({A^{*}}/{\sim_{\mathcal{C}}})\times R$ for $\rho$.

Given as input a nice multiplicative rating map $\rho:2^{A^{*}}\to R$, Theorem
5.3 yields an algorithm to compute
$\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[\rho\right]$. Indeed, computing the
greatest ${BPol\/}(\mathcal{C})$-saturated subset of
$({A^{*}}/{\sim_{\mathcal{C}}})\times R$ is achieved with a greatest fixpoint
algorithm. One starts from the set $S_{0}=({A^{*}}/{\sim_{\mathcal{C}}})\times
R$ and computes a sequence $S_{0}\supseteq S_{1}\supseteq
S_{2}\supseteq\cdots$ of subsets. For every $n\in{\rm Nature}$, $S_{n+1}$ is
the set of all pairs $(D,r)\in S_{n}$ satisfying (1) for $S=S_{n}$. That is,

$\begin{array}[]{c}\text{there exist $r_{1},\dots,r_{k}\in R$ such that,}\\\
\text{$r\leq r_{1}+\cdots+r_{k}$ and
$(D,r_{i},\\{r_{1}+\cdots+r_{k}\\})\in\mathcal{R}^{\rho}_{S_{n}}$ for every
$i\leq k$}\end{array}$

Clearly, $S_{n+1}\subseteq S_{n}$ for every $n\in{\rm Nature}$. Therefore, the
computation eventually reaches a fixpoint which is the greatest
${BPol\/}(\mathcal{C})$-saturated subset of
$({A^{*}}/{\sim_{\mathcal{C}}})\times R$ by definition. Let us point out that
the computation of $S_{n+1}$ from $S_{n}$ involves computing
$\mathcal{R}^{\rho}_{S_{n}}$, which is achieved with a least fixpoint
procedure by definition.

Altogether, it follows that Theorem 5.3 yields an algorithm for computing
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$ (and therefore,
$\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[\rho\right]$ as well by Fact 4.7)
which alternates between a greatest fixpoint and a least fixpoint.

######  Remark 5.4.

The hypothesis that $\rho$ is nice in Theorem 5.3 is mandatory: the result
fails otherwise. This is actually apparent on the definition of
${BPol\/}(\mathcal{C})$-saturated sets. One may verify from the definition of
$\mathcal{R}^{\rho}_{S}$ that for every triple
$(D,q,U)\in\mathcal{R}^{\rho}_{S}$, there exists a word $w\in A^{*}$ such that
$D=[w]_{\mathcal{C}}$ and $q=\rho(w)$. Therefore, it follows from (1) that for
every $(D,r)\in({A^{*}}/{\sim_{\mathcal{C}}})\times R$ belonging to a
${BPol\/}(\mathcal{C})$-saturated subset, its second component $r$ must
satisfy $r\leq\rho(w_{1})+\cdots+\rho(w_{k})$ for some words
$w_{1},\dots,w_{k}\in A^{*}$. Intuitively, this means that
${BPol\/}(\mathcal{C})$-saturated subsets only depend on the image of
singletons. Therefore, using the notion only makes sense when $\rho$ is
characterized by these images: this is exactly the definition of nice rating
maps.

This might seem to be a minor observation. Indeed, by Proposition 4.8, being
able to compute $\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[\rho\right]$ from a
nice multiplicative rating map suffices to meet our goal: getting an algorithm
for ${BPol\/}(\mathcal{C})$-covering. Actually, it does not even make sense to
speak of an algorithm which takes arbitrary multiplicative rating maps as
input since we are not able to finitely represent them. However, from a
theoretical point of view, the fact that we only manage to get a description
of $\mathcal{I}_{{BPol\/}(\mathcal{C})}\left[\rho\right]$ when $\rho$ is nice
is significant. In the proof of Theorem 5.3, we use a theorem of [Pla18] as a
subresult. Specifically, this theorem is a characterization of
${Pol\/}(\mathcal{C})$-optimal pointed imprints: given a
$\mathcal{C}$-compatible morphism $\alpha:A^{*}\to M$ and a multiplicative
rating map $\tau:2^{A^{*}}\to Q$, it describes the set
$\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\tau]$. A key point is that this
characterization does not require $\tau$ to be nice. This is crucial: in the
proof of Theorem 5.3, we consider auxiliary rating maps (built from $\rho$)
which need not be nice. Altogether, this means that we are able to handle
${Pol\/}(\mathcal{C})$ for all multiplicative rating maps and this is crucial
in order to handle ${BPol\/}(\mathcal{C})$ but we are only able to do so for
_nice_ multiplicative rating maps (the situation is similar for
${Pol\/}({BPol\/}(\mathcal{C}))$ as shown in [Pla18]). This explains why the
results presented in this paper and in [Pla18] cannot be lifted to higher
levels in concatenation hierarchies (at least not in a straightforward
manner).

We turn to the proof of Theorem 5.3. It spans the remaining four sections of
the paper. Given a nice multiplicative rating map $\rho:2^{A^{*}}\to R$, we
have to show that $\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$ is
the greatest ${BPol\/}(\mathcal{C})$-saturated subset of
$({A^{*}}/{\sim_{\mathcal{C}}})\times R$ for $\rho$. The main argument
involves two directions which are proved independently. They correspond to
soundness and completeness of the greatest fixpoint algorithm computing
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$.

  * •

The soundness argument shows that
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$ contains every
${BPol\/}(\mathcal{C})$-saturated subset (this implies that the greatest
fixpoint procedure only computes elements of
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$). We present it in
Section 8.

  * •

The completeness argument shows that
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$ itself is
${BPol\/}(\mathcal{C})$-saturated (this implies that the greatest fixpoint
procedure computes all elements of
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$). We present it in
Section 9.

When put together, these two results yield as desired that
$\mathcal{P}_{{BPol\/}(\mathcal{C})}^{\mathcal{C}}[\rho]$ is the greatest
${BPol\/}(\mathcal{C})$-saturated subset of $R$, proving Theorem 5.3.

However, before presenting the main argument, we require some additional
material about rating maps. For both directions, we shall introduce auxiliary
rating maps (built from $\rho$) and apply a characterization of
${Pol\/}(\mathcal{C})$-optimal imprints to them (taken from [Pla18]). These
auxiliary rating maps are built using generic constructions which are not
specific to Theorem 5.3. We present them in Section 6. Then, we recall the
theorem characterizing ${Pol\/}(\mathcal{C})$-optimal imprints from [Pla18] in
Section 7 (actually, we slightly generalize it, since we shall apply it for
rating maps that are more general than the ones considered in [Pla18]).

##  6\. Nesting of rating maps

In this section, we present two generic constructions. Each of them builds a
new rating map out of an already existing one and a lattice $\mathcal{D}$. The
constructions are new: they do not appear in [PZ18a] (however, one of them
generalizes and streamlines a technical construction used in [Pla18]).

######  Remark 6.1.

As announced, we shall later rely on these constructions in the proof of
Theorem 5.3 (we use them in the special cases when $\mathcal{D}$ is either
${Pol\/}(\mathcal{C})$ or ${BPol\/}(\mathcal{C})$). However, this section is
independent from Theorem 5.3: all definitions are presented in a general
context.

We first present the constructions and then investigate the properties of the
output rating maps they produce.

###  6.1. Definition

We present two constructions. The first one involves two objects: a lattice
$\mathcal{D}$ and a rating map $\rho:2^{A^{*}}\to R$. We build a new rating
map $\xi_{\mathcal{D}}[\rho]$ whose rating set is $(2^{R},\cup)$, and which
associates to a language its optimal $\mathcal{D}$-optimal $\rho$-imprint.

$\begin{array}[]{llll}\xi_{\mathcal{D}}[\rho]:&(2^{A^{*}},\cup)&\to&(2^{R},\cup)\\\
&K&\mapsto&\mathcal{I}_{\mathcal{D}}\left[K,\rho\right]\end{array}$

The fact that $\xi_{\mathcal{D}}[\rho]$ is indeed a rating map is shown below
in Proposition 6.2. The second construction involves an additional object: a
map $\alpha:A^{*}\to M$ where $M$ is some arbitrary finite set (in practice,
$\alpha$ will be a monoid morphism, but this is not required for the
definition). We build a new rating map $\zeta_{\mathcal{D}}^{\alpha}[\rho]$
with rating set $(2^{M\times R},\cup)$:

$\begin{array}[]{llll}\zeta_{\mathcal{D}}^{\alpha}[\rho]:&(2^{A^{*}},\cup)&\to&(2^{M\times
R},\cup)\\\ &K&\mapsto&\\{(s,r)\mid
r\in\mathcal{I}_{\mathcal{D}}\left[\alpha^{-1}(s)\cap
K,\rho\right]\\}.\end{array}$

Let us prove that these two maps are indeed rating maps. We state this result
in the following proposition.

######  Proposition 6.2.

Consider a lattice $\mathcal{D}$, a map $\alpha:A^{*}\to M$ into a finite set
$M$ and a rating map $\rho:2^{A^{*}}\to R$. Then, $\xi_{\mathcal{D}}[\rho]$
and $\zeta_{\mathcal{D}}^{\alpha}[\rho]$ are rating maps.

###### Proof.

We start with $\xi_{\mathcal{D}}[\rho]$. It is immediate that
$\xi_{\mathcal{D}}[\rho](\emptyset)=\mathcal{I}_{\mathcal{D}}\left[\emptyset,\rho\right]=\emptyset$.
Moreover, we obtain from Fact 4.7 that for every $H,L\subseteq A^{*}$,

$\xi_{\mathcal{D}}[\rho](H\cup L)=\mathcal{I}_{\mathcal{D}}\left[H\cup
L,\rho\right]=\mathcal{I}_{\mathcal{D}}\left[H,\rho\right]\cup\mathcal{I}_{\mathcal{D}}\left[L,\rho\right]=\xi_{\mathcal{D}}[\rho](H)\cup\xi_{\mathcal{D}}[\rho](L).$

We conclude that $\xi_{\mathcal{D}}[\rho]$ is indeed a rating map. We turn to
$\zeta_{\mathcal{D}}^{\alpha}[\rho]$. Clearly,

$\zeta_{\mathcal{D}}^{\alpha}[\rho](\emptyset)=\\{(s,r)\mid
r\in\mathcal{I}_{\mathcal{D}}\left[\emptyset,\rho\right]\\}=\\{(s,r)\mid
r\in\emptyset\\}=\emptyset.$

Moreover, given $H,L\subseteq A^{*}$,

$\zeta_{\mathcal{D}}^{\alpha}[\rho](H\cup L)=\\{(s,r)\mid
r\in\mathcal{I}_{\mathcal{D}}\left[\alpha^{-1}(s)\cap(H\cup
L),\rho\right]\\}.$

By Fact 4.7, this yields,

$\zeta_{\mathcal{D}}^{\alpha}[\rho](H\cup L)=\\{(s,r)\mid
r\in\mathcal{I}_{\mathcal{D}}\left[\alpha^{-1}(s)\cap
H,\rho\right]\cup\mathcal{I}_{\mathcal{D}}\left[\alpha^{-1}(s)\cap
L,\rho\right]\\}$

This exactly says that $\zeta_{\mathcal{D}}^{\alpha}[\rho](H\cup
L)=\zeta_{\mathcal{D}}^{\alpha}[\rho](H)\cup\zeta_{\mathcal{D}}^{\alpha}[\rho](L)$,
finishing the proof that $\zeta_{\mathcal{D}}^{\alpha}[\rho]$ is a rating map.
∎

A crucial observation is that the rating maps $\xi_{\mathcal{D}}[\rho]$ and
$\zeta_{\mathcal{D}}^{\alpha}[\rho]$ are not nice in general, even when the
original rating map $\rho$ is. Let us present a counter-example.

######  Example 6.3.

Let $\mathcal{D}$ be the Boolean algebra consisting of all languages which are
either finite or co-finite (_i.e._ , their complement is finite). Moreover,
let $T=\\{0,1\\}$ and $R=2^{T}$. We define a nice rating map
$\rho:2^{A^{*}}\to R$ as follows (actually, it is simple to verify from the
definition that $\rho$ is also multiplicative). Since we are defining a nice
rating map, it suffices to specify the evaluation of words: for any $w\in
A^{*}$, we let $\rho(w)=\\{0\\}$ if $w$ has even length and $\rho(w)=\\{1\\}$
if $w$ has odd length. We show that the rating map
$\xi_{\mathcal{D}}[\rho]:2^{A^{*}}\to 2^{R}$ is not nice.

By definition,
$\xi_{\mathcal{D}}[\rho](A^{*})=\mathcal{I}_{\mathcal{D}}\left[A^{*},\rho\right]$.
Recall that $\mathcal{D}$ contains only finite and co-finite languages.
Moreover, covers may only contain finitely many languages. Hence, it is
immediate that if $\mathbf{K}$ is an optimal $\mathcal{D}$-cover of $A^{*}$
for $\rho$, then there exists $K\in\mathbf{K}$ containing a word of even
length and a word of odd length. Therefore $\rho(K)=\\{0,1\\}$ by definition
of $\rho$, whence
$\xi_{\mathcal{D}}[\rho](A^{*})=\mathcal{I}[\rho](\mathbf{K})=\\{\\{0,1\\},\\{0\\},\\{1\\},\emptyset\\}=R$.

Now observe that for any $w\in A^{*}$, $\\{w\\}\in\mathcal{D}$ by definition
(it is a finite language). Hence, $\\{\\{w\\}\\}$ is a $\mathcal{D}$-cover of
$\\{w\\}$ and since
$\xi_{\mathcal{D}}[\rho](w)=\mathcal{I}_{\mathcal{D}}\left[\\{w\\},\rho\right]$,
we know that $\xi_{\mathcal{D}}[\rho](w)=\\{\\{0\\},\emptyset\\}$ if $w$ has
even length and $\xi_{\mathcal{D}}[\rho](w)=\\{\\{1\\},\emptyset\\}$ if $w$
has odd length. Altogether, we obtain that,

$\bigcup_{w\in
A^{*}}\xi_{\mathcal{D}}[\rho](w)=\\{\\{0\\},\\{1\\},\emptyset\\}\neq\xi_{\mathcal{D}}[\rho](A^{*})$

We conclude that $\xi_{\mathcal{D}}[\rho]$ is not nice.

Another important question is whether $\xi_{\mathcal{D}}[\rho]$ and
$\zeta_{\mathcal{D}}^{\alpha}[\rho]$ are multiplicative. The remainder of the
section is devoted to discussing this point.

###  6.2. Multiplication

If $\alpha:A^{*}\to M$ is a morphism into a finite monoid and
$\rho:2^{A^{*}}\to R$ is a multiplicative rating map, $(M,\cdot)$ is a monoid
and $(R,+,\cdot)$ is an idempotent semiring. We may lift the multiplication of
$R$ to $2^{R}$ in the natural way: given $U,V\in 2^{R}$, we let $UV=\\{qr\mid
q\in U\text{ and }r\in V\\}$. One may verify that $(2^{R},\cup,\cdot)$ is an
idempotent semiring. Similarly, we may lift the componentwise multiplication
on $M\times R$ to $2^{M\times R}$ and $(2^{M\times R},\cup,\cdot)$ is an
idempotent semiring. Whenever we consider semiring structures for $2^{R}$ and
$2^{M\times R}$, these are the additions and multiplications that we shall
use.

Unfortunately, even though $2^{R}$ and $2^{M\times R}$ are semirings, neither
$\xi_{\mathcal{D}}[\rho]:2^{A^{*}}\to 2^{R}$ nor
$\zeta_{\mathcal{D}}^{\alpha}[\rho]:2^{A^{*}}\to 2^{M\times R}$ are
multiplicative: they are not monoid morphisms for multiplication. However, it
turns out that they behave almost as multiplicative rating maps when the class
$\mathcal{D}$ satisfies appropriate properties related to closure under
concatenation. We formalize this with a new notion: quasi-multiplicative
rating maps.

Quasi-multiplicative rating maps. Let $\rho:(2^{A^{*}},\cup)\to(R,+)$ be a
rating map whose rating set is equipped with a multiplication “$\cdot$” such
that $(R,+,\cdot)$ is a semiring (however, $\rho$ is not required to be
multiplicative for this multiplication). Finally, let $\mu_{\rho}$ be an
endomorphism of the additive monoid $(R,+)$ (_i.e._ ,
$\mu_{\rho}(0_{R})=0_{R}$ and for all $r,s\in R$,
$\mu_{\rho}(r+s)=\mu_{\rho}(r)+\mu_{\rho}(s)$). We say that $\rho$ is _quasi-
multiplicative for $\mu_{\rho}$_ when the following axioms are satisfied:

  1. (1)

For every $q,r,s\in R$, $\mu_{\rho}(q\mu_{\rho}(r)s)=\mu_{\rho}(qrs)$.

  2. (2)

For every $K_{1},K_{2}\subseteq A^{*}$, we have
$\rho(K_{1}K_{2})=\mu_{\rho}(\rho(K_{1})\cdot\rho(K_{2}))$.

For the sake of improved readability, we often abuse terminology and simply
say that “the rating map $\rho$ is quasi-multiplicative”, assuming implicitly
that the endomorphism $\mu_{\rho}$ is defined and fixed. Note however that
this is slightly ambiguous as there might be several endomorphisms of $(R,+)$
satisfying the above axioms for the same rating map $\rho$.

######  Remark 6.4.

Since $\mu_{\rho}$ is an endomorphism of $(R,+)$, it preserves the canonical
order on $R$. Given $q,r\in R$ such that $q\leq r$, we have
$\mu_{\rho}(q)\leq\mu_{\rho}(r)$. Indeed, by definition, $q\leq r$ means that
$q+r=r$. Therefore, since $\mu_{\rho}$ is a morphism,
$\mu_{\rho}(q)+\mu_{\rho}(r)=\mu_{\rho}(r)$ which means that
$\mu_{\rho}(q)\leq\mu_{\rho}(r)$. We use this property implicitly in proofs.

######  Remark 6.5.

Clearly, a true multiplicative rating map is always quasi-multiplicative.
Indeed, in this case, it suffices to choose $\mu_{\rho}$ as the identity;
$\mu_{\rho}(r)=r$ for all $r\in R$.

We have the following useful fact about quasi-multiplicative rating maps.

######  Fact 6.6.

Let $\rho:2^{A^{*}}\to R$ be a quasi-multiplicative rating map. For every
language $H\subseteq A^{*}$, we have $\rho(H)=\mu_{\rho}(\rho(H))$.

###### Proof.

Axiom 2 in the definition yields
$\rho(H)=\mu_{\rho}(\rho(H)\cdot\rho(\varepsilon))$. Thus, Axiom 1 yields
$\mu_{\rho}(\rho(H))=\mu_{\rho}(\mu_{\rho}(\rho(H)\cdot\rho(\varepsilon)))=\mu_{\rho}(\rho(H)\cdot\rho(\varepsilon))=\rho(H)$.
This concludes the proof. ∎

Additionally, we shall need the following lemma which is a straightforward
adaptation of a result proved in [PZ18a, Lemma 5.8] to quasi-multiplicative
rating maps.

######  Lemma 6.7.

Let $\mathcal{C}$ be a quotient-closed lattice and $\rho:2^{A^{*}}\to R$ be a
quasi-multiplicative rating map. For every $H,L\subseteq A^{*}$,
$q\in\mathcal{I}_{\mathcal{C}}\left[H,\rho\right]$ and
$r\in\mathcal{I}_{\mathcal{C}}\left[L,\rho\right]$, we have
$\mu_{\rho}(qr)\in\mathcal{I}_{\mathcal{C}}\left[HL,\rho\right]$.

###### Proof.

Let $q\in\mathcal{I}_{\mathcal{C}}\left[H,\rho\right]$ and
$r\in\mathcal{I}_{\mathcal{C}}\left[L,\rho\right]$. By definition, it suffices
to prove that for every $\mathcal{C}$-cover $\mathbf{K}$ of $HL$, we have
$\mu_{\rho}(qr)\in\mathcal{I}[\rho](\mathbf{K})$. Let $\mathbf{K}$ be a
$\mathcal{C}$-cover of $HL$, we have to find $K\in\mathbf{K}$ such that
$\mu_{\rho}(qr)\leq\rho(K)$. We use the following claim which is based on the
Myhill-Nerode theorem.

######  Claim.

There exists a language $G\in\mathcal{C}$ which satisfies the following two
properties:

  1. (1)

For all $u\in H$, there exists $K\in\mathbf{K}$ such that $G\subseteq
u^{-1}K$.

  2. (2)

$r\leq\rho(G)$

###### Proof of the claim.

For every $u\in H$, we let $\mathbf{Q}_{u}=\\{u^{-1}K\mid K\in\mathbf{K}\\}$.
Clearly, $\mathbf{Q}_{u}$ is a $\mathcal{C}$-cover of $L$ since $\mathbf{K}$
is a cover of $HL$ and $\mathcal{C}$ is closed under quotients. Moreover, we
know by hypothesis on $\mathcal{C}$ that all languages in $\mathbf{K}$ are
regular. Therefore, it follows from the Myhill-Nerode theorem that they have
finitely many quotients. Thus, while there might be infinitely many words
$u\in H$, there are only finitely many distinct sets $\mathbf{Q}_{u}$. It
follows that we may use finitely many intersections to build a
$\mathcal{C}$-cover $\mathbf{Q}$ of $L$ such that for every $Q\in\mathbf{Q}$
and every $u\in H$, there exists $K\in\mathbf{K}$ satisfying $Q\subseteq
u^{-1}K$. This means that all $Q\in\mathbf{Q}$ satisfy the first item in the
claim, we now pick one which satisfies the second one as well.

Since $r\in\mathcal{I}_{\mathcal{C}}\left[L,\rho\right]$, and $\mathbf{Q}$ is
a $\mathcal{C}$-cover of $L$, we have $r\in\mathcal{I}[\rho](\mathbf{Q})$.
Thus, we get $G\in\mathbf{Q}$ such that $r\leq\rho(G)$ by definition. This
concludes the proof of the claim. ∎

We may now finish the proof of Lemma 6.7. Let $G\in\mathcal{C}$ be as defined
in the claim and consider the following set:

$\mathbf{G}=\left\\{\bigcap_{v\in G}Kv^{-1}\mid K\in\mathbf{K}\right\\}.$

Observe that all languages in $\mathbf{G}$ belong to $\mathcal{C}$. Indeed, by
hypothesis on $\mathcal{C}$, every $K\in\mathbf{K}$ is regular. Thus, it has
finitely many right quotients by the Myhill-Nerode theorem and the language
$\bigcap_{v\in H}Kv^{-1}$ is the intersection of finitely many quotients of
languages in $\mathcal{C}$. By closure under intersection and quotients, it
follows that $\bigcap_{v\in G}Kv^{-1}\in\mathcal{C}$. Moreover, $\mathbf{G}$
is a $\mathcal{C}$-cover of $H$. Indeed, given $u\in H$, we have
$K\in\mathbf{K}$ such that $G\subseteq u^{-1}K$ by the first assertion in the
claim. Hence, for every $v\in G$, we have $u\in Kv^{-1}$ and we obtain that
$u\in\bigcap_{v\in G}Kv^{-1}$, which is an element of $\mathbf{G}$.

Therefore, since $q\in\mathcal{I}_{\mathcal{C}}\left[H,\rho\right]$ by
hypothesis, we have $q\in\mathcal{I}[\rho](\mathbf{G})$ and we obtain
$G^{\prime}\in\mathbf{G}$ such that $q\leq\rho(G^{\prime})$. Hence, since
$r\leq\rho(G)$ by the second item in the claim, we have
$qr\leq\rho(G^{\prime})\cdot\rho(G)$. Since $\rho$ is quasi-multiplicative
over $\mathcal{C}$ and $G,G^{\prime}\in\mathcal{C}$, it follows from Axiom 2
in the definition of quasi-multiplicative rating maps that,

$\rho(G^{\prime}G)=\mu_{\rho}(\rho(G^{\prime})\cdot\rho(G))$

Moreover, since $\mu_{\rho}$ is an endomorphism of $(R,+)$ and
$qr\leq\rho(G^{\prime})\cdot\rho(G)$, we have by Fact 4.1:

$\mu_{\rho}(qr)\leq\mu_{\rho}(\rho(G^{\prime})\cdot\rho(G))$

Altogether, we get $\mu_{\rho}(qr)\leq\rho(G^{\prime}G)$. Finally, observe
that $G^{\prime}G\subseteq K$ for some $K\in\mathbf{K}$. Indeed, if $w\in
G^{\prime}G$, we have $w=uv$ with $u\in G^{\prime}$ and $v\in G$. Moreover,
$G^{\prime}=\bigcap_{v\in G}Kv^{-1}$ for some $K\in\mathbf{K}$ by definition
of $\mathbf{G}$. Hence, $u\in Kv^{-1}$ which yields $w=uv\in K$. Altogether,
we get that $\mu_{\rho}(qr)\leq\rho(G^{\prime}G)\leq\rho(K)$, which concludes
the proof. ∎

We now prove that when $\mathcal{D}$ is a quotient-closed lattice closed under
concatenation, the rating map $\zeta_{\mathcal{D}}^{\alpha}[\rho]$ is quasi-
multiplicative provided that $\alpha$ is a morphism and $\rho$ is already
quasi-multiplicative (actually, this is also true for
$\xi_{\mathcal{D}}[\rho]$ but we do not need this result). This result is
tailored to the situation in which we shall later use
$\zeta_{\mathcal{D}}^{\alpha}[\rho]$: $\mathcal{D}={Pol\/}(\mathcal{C})$.

######  Lemma 6.8.

Let $\mathcal{D}$ be a quotient-closed lattice closed under concatenation,
$\alpha:A^{*}\to M$ be a morphism and $\rho:2^{A^{*}}\to R$ be a quasi-
multiplicative rating map. Then, $\zeta_{\mathcal{D}}^{\alpha}[\rho]$ is
quasi-multiplicative for the following associated endomorphism
$\mu_{\zeta_{\mathcal{D}}^{\alpha}[\rho]}$ of $(2^{M\times R},\cup)$:

$\mu_{\zeta_{\mathcal{D}}^{\alpha}[\rho]}(T)=\mathord{\downarrow_{R}}\\{(s,\mu_{\rho}(r))\mid(s,r)\in
T\\}\quad\text{for every $T\in 2^{M\times R}$}.$

###### Proof.

We already know from Proposition 6.2 that $\zeta_{\mathcal{D}}^{\alpha}[\rho]$
is a rating map. Hence, we have to prove that the axioms of quasi-
multiplicative rating maps hold for the endomorphism
$\mu_{\zeta_{\mathcal{D}}^{\alpha}[\rho]}$ of $(2^{M\times R},\cup)$ described
in the lemma (it is clear from the definition that this is indeed an
endomorphism). For the sake of avoiding clutter, we write $\mu$ for
$\mu_{\zeta_{\mathcal{D}}^{\alpha}[\rho]}$.

We start with the first axiom. Consider $T,U,V\in 2^{M\times R}$. We have to
show that $\mu(T\mu(U)V)=\mu(TUV)$. Assume first that $(s,r)\in\mu(T\mu(U)V)$.
By definition of $\mu$, this yields $(s_{1},r_{1})\in T$,
$(s_{2},r_{2})\in\mu(U)$ and $(s_{3},r_{3})\in V$ such that
$s=s_{1}s_{2}s_{3}$ and $r\leq\mu_{\rho}(r_{1}r_{2}r_{3})$. Since
$(s_{2},r_{2})\in\mu(U)$, we have $(s_{2},r^{\prime}_{2})\in U$ such that
$r_{2}\leq\mu_{\rho}(r^{\prime}_{2})$. It follows that $r_{1}r_{2}r_{3}\leq
r_{1}\mu_{\rho}(r^{\prime}_{2})r_{2}$ and since $\mu_{\rho}$ is an
endomorphism of $(R,+)$, we obtain,

$r\leq\mu_{\rho}(r_{1}r_{2}r_{3})\leq\mu_{\rho}(r_{1}\mu_{\rho}(r^{\prime}_{2})r_{2}).$

Since $\rho$ is quasi-multiplicative, the first axiom in the definition yields
that
$\mu_{\rho}(r_{1}\mu_{\rho}(r^{\prime}_{2})r_{2})=\mu_{\rho}(r_{1}r^{\prime}_{2}r_{3})$
and we get $r\leq\mu_{\rho}(r_{1}r^{\prime}_{2}r_{3})$. Since
$(s_{1},r_{1})\in T$, $(s_{2},r^{\prime}_{2})\in U$ and $(s_{3},r_{3})\in V$.
This yields $(s,r)=(s_{1}s_{2}s_{3},r)\in\mu(TUV)$.

Conversely, assume that $(s,r)\in\mu(TUV)$. By definition of $\mu$, we get
$(s_{1},r_{1})\in T$, $(s_{2},r_{2})\in U$ and $(s_{3},r_{3})\in V$ such that
$s=s_{1}s_{2}s_{3}$ and $r\leq\mu_{\rho}(r_{1}r_{2}r_{3})$. The first axiom in
the definition of quasi-multiplicative rating maps yields that
$\mu_{\rho}(r_{1}\mu_{\rho}(r_{2})r_{2})=\mu_{\rho}(r_{1}r_{2}r_{3})$.
Therefore, $r\leq\mu_{\rho}(r_{1}\mu_{\rho}(r_{2})r_{3})$. Moreover, since
$(s_{2},r_{2})\in U$, it is immediate that
$(s_{2},\mu_{\rho}(r_{2}))\in\mu(U)$ by definition of $\mu$. Altogether, this
implies that $(s,r)\in\mu(T\mu(U)V)$.

It remains to establish that $\zeta_{\mathcal{D}}^{\alpha}[\rho]$ fulfills the
Axiom 2. Let $K_{1},K_{2}\subseteq A^{*}$. We show that,

$\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1}K_{2})=\mu(\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1})\cdot\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{2})).$
(2)

We start with the right to left inclusion. Consider
$(s,r)\in\mu\big{(}\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1})\cdot\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{2})\big{)}$.
By definition of $\mu$ we have
$(s_{1},r_{1})\in\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1})$ and
$(s_{2},r_{2})\in\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{2})$ such that
$s=s_{1}s_{2}$ and $r\leq\mu_{\rho}(r_{1}r_{2})$. By definition of
$\zeta_{\mathcal{D}}^{\alpha}[\rho]$, this means that
$r_{1}\in\mathcal{I}_{\mathcal{D}}\left[K_{1}\cap\alpha^{-1}(s_{1}),\rho\right]$
and
$r_{2}\in\mathcal{I}_{\mathcal{D}}\left[K_{2}\cap\alpha^{-1}(s_{2}),\rho\right]$.
Since $\mathcal{D}$ is a quotient-closed lattice, Lemma 6.7 yields that:

$\mu_{\rho}(r_{1}r_{2})\in\mathcal{I}_{\mathcal{D}}\left[(K_{1}\cap\alpha^{-1}(s_{1}))\cdot(K_{2}\cap\alpha^{-1}(s_{2})),\rho\right].$

Observe that
$(K_{1}\cap\alpha^{-1}(s_{1}))\cdot(K_{2}\cap\alpha^{-1}(s_{2}))\subseteq
K_{1}K_{2}\cap\alpha^{-1}(s_{1})\alpha^{-1}(s_{2})$. Moreover, since $\alpha$
is a morphism, it is clear that
$\alpha^{-1}(s_{1})\alpha^{-1}(s_{2})\subseteq\alpha^{-1}(s_{1}s_{2})=\alpha^{-1}(s)$.
Altogether, this means that we have
$(K_{1}\cap\alpha^{-1}(s_{1}))\cdot(K_{2}\cap\alpha^{-1}(s_{2}))\subseteq
K_{1}K_{2}\cap\alpha^{-1}(s)$. Thus, Fact 4.6 yields
$\mu_{\rho}(r_{1}r_{2})\in\mathcal{I}_{\mathcal{D}}\left[K_{1}K_{2}\cap\alpha^{-1}(s),\rho\right]$.
Since $r\leq\mu_{\rho}(r_{1}r_{2})$, this implies
$r\in\mathcal{I}_{\mathcal{D}}\left[K_{1}K_{2}\cap\alpha^{-1}(s),\rho\right]$,
which exactly says that
$(s,r)\in\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1}K_{2})$, concluding the proof
for the left to right inclusion.

We turn to the converse inclusion. This is where we need $\mathcal{D}$ to be
closed under concatenation. Let
$(s,r)\in\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1}K_{2})$. We show that
$(s,r)\in\mu\big{(}\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1})\cdot\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{2})\big{)}$.
By definition, we have
$r\in\mathcal{I}_{\mathcal{D}}\left[K_{1}K_{2}\cap\alpha^{-1}(s),\rho\right]$.
For every $t\in M$ and $i\in\\{1,2\\}$, we define $\mathbf{H}_{i,t}$ as an
optimal $\mathcal{D}$-cover of $K_{i}\cap\alpha^{-1}(t)$. Consider the
following finite set of languages $\mathbf{H}$,

$\mathbf{H}=\\{H_{1}H_{2}\mid\text{there exist $s_{1},s_{2}\in M$ such that
$s_{1}s_{2}=s$, $H_{1}\in\mathbf{H}_{1,s_{1}}$ and
$H_{2}\in\mathbf{H}_{2,s_{2}}$}\\}.$

We prove that $\mathbf{H}$ is a $\mathcal{D}$-cover of
$K_{1}K_{2}\cap\alpha^{-1}(s)$. Clearly all languages in $\mathbf{H}$ belong
to $\mathcal{D}$ since $\mathcal{D}$ is closed under concatenation by Theorem
3.2. Let us show that $\mathbf{H}$ is a cover of
$K_{1}K_{2}\cap\alpha^{-1}(s)$. Consider $w\in K_{1}K_{2}\cap\alpha^{-1}(s)$,
we exhibit $H\in\mathbf{H}$ such that $w\in H$. Since $w\in K_{1}K_{2}$, we
have $w=w_{1}w_{2}$ with $w_{1}\in K_{1}$ and $w_{2}\in K_{2}$. Let
$s_{1}=\alpha(w_{1})$ and $s_{2}=\alpha(w_{2})$. Altogether, this means that
$w_{1}\in K_{1}\cap\alpha^{-1}(s_{1})$ and $w_{2}\in
K_{2}\cap\alpha^{-1}(s_{2})$. Therefore, we have
$H_{1}\in\mathbf{H}_{1,s_{1}}$ and $H_{2}\in\mathbf{H}_{2,s_{2}}$ such that
$w_{1}\in H_{1}$ and $w_{2}\in H_{2}$. This yields $w\in H_{1}H_{2}$. Finally,
$s_{1}s_{2}=\alpha(w)=s$ which yields that $H_{1}H_{2}\in\mathbf{H}$ by
definition.

We may now finish the argument and show that
$(s,r)\in\mu(\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1})\cdot\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{2}))$.
Recall that
$r\in\mathcal{I}_{\mathcal{D}}\left[K_{1}K_{2}\cap\alpha^{-1}(s),\rho\right]$.
Thus, since $\mathbf{H}$ is a $\mathcal{D}$-cover of
$K_{1}K_{2}\cap\alpha^{-1}(s)$, we have $r\in\mathcal{I}[\rho](\mathbf{H})$.
It follows that there exists $H\in\mathbf{H}$ such that $r\leq\rho(H)$. By
definition of $\mathbf{H}$, we have $H=H_{1}H_{2}$ with
$H_{1}\in\mathbf{H}_{1,s_{1}}$ and $H_{2}\in\mathbf{H}_{2,s_{2}}$ where
$s_{1},s_{2}\in M$ satisfy $s_{1}s_{2}=s$. Let $r_{1}=\rho(H_{1})$ and
$r_{2}=\rho(H_{2})$. Since $\mathbf{H}_{1,s_{1}}$ and $\mathbf{H}_{2,s_{2}}$
are optimal $\mathcal{D}$-covers of $K_{1}\cap\alpha^{-1}(s_{1})$ and
$K_{2}\cap\alpha^{-1}(s_{2})$ respectively, we have
$r_{1}\in\mathcal{I}_{\mathcal{D}}\left[K_{1}\cap\alpha^{-1}(s_{1}),\rho\right]$
and
$r_{2}\in\mathcal{I}_{\mathcal{D}}\left[K_{2}\cap\alpha^{-1}(s_{2}),\rho\right]$.
It follows that $(s_{1},r_{1})\in\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1})$
and $(s_{2},r_{2})\in\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{2})$. Consequently,
$(s,r_{1}r_{2})=(s_{1}s_{2},r_{1}r_{2})\in\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1})\cdot\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{2})$.
Finally, by hypothesis and since $\rho$ is quasi-multiplicative, we have,

$r\leq\rho(H)=\rho(H_{1}H_{2})=\mu_{\rho}(\rho(H_{1})\cdot\rho(H_{2}))=\mu_{\rho}(r_{1}r_{2}).$

By definition of $\mu$, this
yields$(s,r)\in\mu(\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{1})\cdot\zeta_{\mathcal{D}}^{\alpha}[\rho](K_{2}))$,
concluding the proof. ∎

We present a second result for rating maps of the form
$\xi_{{Bool\/}(\mathcal{D})}[\rho]:2^{A^{*}}\to 2^{R}$. As expected, we shall
consider the case $\mathcal{D}={Pol\/}(\mathcal{C})$. In that case, we are not
able to prove that $\xi_{\mathcal{D}}[\rho]$ is quasi-multiplicative (the
issue being that ${Bool\/}(\mathcal{D})$ is _not_ closed under concatenation
in general). We deal with this problem using two separate results. First, we
show that when $\mathcal{D}$ is a quotient-closed lattice of regular languages
_closed under concatenation_ , while $\xi_{{Bool\/}(\mathcal{D})}[\rho]$ might
not be quasi-multiplicative itself, it coincides with a quasi-multiplicative
rating map over languages in $\mathcal{D}$. Note that this result is where we
use the weak concatenation principle that we presented for Boolean closure in
Lemma 3.4.

######  Lemma 6.9.

Let $\mathcal{D}$ be a quotient-closed lattice closed under concatenation and
$\rho:2^{A^{*}}\to R$ a multiplicative rating map. There exists a rating map
$\tau:2^{A^{*}}\to 2^{R}$ which satisfies the two following conditions:

  1. (1)

$\tau$ is quasi-multiplicative for the endomorphism
$\mu_{\tau}:U\mapsto\mathord{\downarrow_{R}}U$ of $(2^{R},\cup)$, and,

  2. (2)

for every $K\in\mathcal{D}$, we have
$\tau(K)=\xi_{{Bool\/}(\mathcal{D})}[\rho](K)$.

###### Proof.

We first define $\tau:2^{A^{*}}\to 2^{R}$. For every $K\subseteq A^{*}$, we
let,

$\tau(K)=\bigcap_{\\{L\in\mathcal{D}\mid K\subseteq
L\\}}\xi_{{Bool\/}(\mathcal{D})}[\rho](L)$

It is immediate by definition that when $K\in\mathcal{D}$, we have
$\tau(K)=\xi_{{Bool\/}(\mathcal{D})}[\rho](K)$. We have to verify that $\tau$
is a quasi-multiplicative rating map. We need the following fact.

######  Fact 6.10.

For all $K\subseteq A^{*}$, there exists $L\in\mathcal{D}$ such that
$K\subseteq L$ and $\tau(K)=\xi_{{Bool\/}(\mathcal{D})}[\rho](L)$.

###### Proof.

Since $2^{R}$ is finite, there are finitely many languages
$L_{1},\dots,L_{n}\in\mathcal{D}$ such that $K\subseteq L_{i}$ for every
$i\leq n$ and
$\tau(K)=\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{1})\cap\cdots\cap\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{n})$.
Since $\mathcal{D}$ is a lattice by hypothesis, we have $L=L_{1}\cap\cdots\cap
L_{n}\in\mathcal{D}$. Clearly, $K\subseteq L$ which implies
$\tau(K)\subseteq\xi_{{Bool\/}(\mathcal{D})}[\rho](L)$ by definition of
$\tau$. Finally, since $L\subseteq L_{i}$ for every $i$, we obtain that
$\xi_{{Bool\/}(\mathcal{D})}[\rho](L)\subseteq\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{1})\cap\cdots\cap\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{n})=\tau(K)$.
Altogether, we conclude that $\tau(K)=\xi_{{Bool\/}(\mathcal{D})}[\rho](L)$. ∎

Let us first prove that $\tau$ is a rating map. Clearly,
$\tau(\emptyset)=\xi_{{Bool\/}(\mathcal{D})}[\rho](\emptyset)=\emptyset$. Let
$K_{1},K_{2}\subseteq A^{*}$, we prove that $\tau(K_{1}\cup
K_{2})=\tau(K_{1})\cup\tau(K_{2})$. Clearly, every $H\in\mathcal{D}$
containing $K_{1}\cup K_{2}$ contains $K_{1}$ and $K_{2}$ as well. Thus,
$\tau(K_{1})\cup\tau(K_{2})\subseteq\tau(K_{1}\cup K_{2})$ by definition of
$\tau$. For the converse inclusion, Fact 6.10 yields
$L_{1},L_{2}\in\mathcal{D}$ such that $K_{i}\subseteq L_{i}$ and
$\tau(K_{i})=\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{i})$ for $i=1,2$. Since
$\xi_{{Bool\/}(\mathcal{D})}[\rho]$ is a rating map by Proposition 6.2, we get
$\tau(K_{1})\cup\tau(K_{2})=\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{1}\cup
L_{2})$. Since $K_{1}\cup K_{2}\subseteq L_{1}\cup L_{2}$, the definition of
$\tau$ then yields $\tau(K_{1}\cup K_{2})\subseteq\tau(K_{1})\cup\tau(K_{2})$.

It remains to prove that $\tau$ is quasi-multiplicative for the endomorphism
$\mu_{\tau}:U\mapsto\mathord{\downarrow_{R}}U$ of $(2^{R},\cup)$. Axiom 1 is
immediate: for every $T,U,V\in 2^{R}$, we have
$\mathord{\downarrow_{R}}(T(\mathord{\downarrow_{R}}U)V)=\mathord{\downarrow_{R}}(TUV)$.

We turn to Axiom 2. For $K_{1},K_{2}\subseteq A^{*}$, we prove that
$\tau(K_{1}K_{2})=\mathord{\downarrow_{R}}(\tau(K_{1})\cdot\tau(K_{2}))$. We
start with the right to left inclusion. Let
$r\in\mathord{\downarrow_{R}}(\tau(K_{1})\cdot\tau(K_{2}))$. We show that
$r\in\tau(K_{1}K_{2})$. By definition, this boils down to proving that
$r\in\xi_{{Bool\/}(\mathcal{D})}[\rho](H)$ for every $H\in\mathcal{D}$ such
that $K_{1}K_{2}\subseteq H$. We fix $H$ for the proof. Consider the two
following languages,

$U_{1}=\bigcap_{v\in K_{2}}Hv^{-1}\quad\text{and}\quad U_{2}=\bigcap_{u\in
U_{1}}u^{-1}H.$

Since $\mathcal{D}$ is a quotient-closed lattice of regular languages and
$H\in\mathcal{D}$, we have $U_{1},U_{2}\in\mathcal{D}$ (recall that a regular
language has finitely many quotients by the Myhill-Nerode theorem). Since
$K_{1}K_{2}\subseteq H$, one may verify that $K_{i}\subseteq U_{i}$ for
$i=1,2$. This yields
$\tau(K_{i})\subseteq\xi_{{Bool\/}(\mathcal{D})}[\rho](U_{i})$ by definition
of $\tau$. Therefore, since we have
$r\in\mathord{\downarrow_{R}}(\tau(K_{1})\cdot\tau(K_{2}))$, we obtain
$r_{i}\in\xi_{{Bool\/}(\mathcal{D})}[\rho](U_{i})$ (_i.e._
$r_{i}\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[U_{i},\rho\right]$) for
$i=1,2$ such that $r\leq r_{1}r_{2}$. By Lemma 3.1, ${Bool\/}(\mathcal{D})$ is
a quotient-closed Boolean algebra. Thus, since $\rho$ is a multiplicative
rating map, Lemma 6.7 yields
$r_{1}r_{2}\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[U_{1}U_{2},\rho\right]$.
Since $r\leq r_{1}r_{2}$, we obtain
$r\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[U_{1}U_{2},\rho\right]$ by
definition of imprints. Finally, we have $U_{1}U_{2}\subseteq H$ by definition
of $U_{2}$. Hence, Fact 4.6 yields
$r\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[H,\rho\right]=\xi_{{Bool\/}(\mathcal{D})}[\rho](H)$.

We turn to the converse inclusion. Let $r\in\tau(K_{1}K_{2})$. We show that
$r\in\mathord{\downarrow_{R}}(\tau(K_{1})\cdot\tau(K_{2}))$. For $i=1,2$, Fact
6.10 yields $L_{i}\in\mathcal{D}$ such that $K_{i}\subseteq L_{i}$ and
$\tau(K_{i})=\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{i})$. We let
$\mathbf{H}_{i}$ as an optimal ${Bool\/}(\mathcal{D})$-cover (for $\rho$) of
$L_{i}$. By definition,
$\mathcal{I}[\rho](\mathbf{H}_{i})=\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{i})=\tau(K_{i})$.
Since $L_{1},L_{2}\in\mathcal{D}$, we may apply Lemma 3.4 to build a
${Bool\/}(\mathcal{D})$-cover $\mathbf{H}$ of $L_{1}L_{2}$ such that for every
$H\in\mathbf{H}$, there exist $H_{1}\in\mathbf{H}_{1}$ and
$H_{2}\in\mathbf{H}_{2}$ such that $H\subseteq H_{1}H_{2}$. By hypothesis
$r\in\tau(K_{1}K_{2})$. Moreover, we have $K_{1}K_{2}\subseteq L_{1}L_{2}$ and
$L_{1}L_{2}\in\mathcal{D}$ since $\mathcal{D}$ is closed under concatenation.
Thus, $r\in\xi_{{Bool\/}(\mathcal{D})}[\rho](L_{1}L_{2})$ by definition of
$\tau$. It follows that
$r\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[L_{1}L_{2},\rho\right]$ and
since $\mathbf{H}$ is a ${Bool\/}(\mathcal{D})$-cover of $L_{1}L_{2}$, we get
$H\in\mathbf{H}$ such that $r\leq\rho(H)$. By definition of $\mathbf{H}$,
there exist $H_{1}\in\mathbf{H}_{1}$ and $H_{2}\in\mathbf{H}_{2}$ such that
$H\subseteq H_{1}H_{2}$. This implies that $r\leq\rho(H_{1})\cdot\rho(H_{2})$.
Finally, $\rho(H_{i})\in\tau(K_{i})$ for $i=1,2$ by definition of
$\mathbf{H}_{i}$. Thus, we get
$r\in\mathord{\downarrow_{R}}(\tau(K_{1})\cdot\tau(K_{2}))$ which concludes
the proof. ∎

We complete Lemma 6.9 with another statement which requires that $\mathcal{D}$
is closed under _marked_ concatenation (this will be the case in practice
since we apply these results for $\mathcal{D}={Pol\/}(\mathcal{C})$). In this
case as well, we use our weak concatenation principle for classes of the form
${Bool\/}(\mathcal{D})$. Specifically, we apply the variant for marked
concatenation (_i.e._ Lemma 3.6).

######  Lemma 6.11.

Let $\mathcal{D}$ be a quotient-closed lattice closed under marked
concatenation and $\rho:2^{A^{*}}\to R$ a multiplicative rating map. For every
$K_{1},K_{2}\in\mathcal{D}$ and $a\in A$, we have,

$\xi_{{Bool\/}(\mathcal{D})}[\rho](K_{1}aK_{2})=\mathord{\downarrow_{R}}(\xi_{{Bool\/}(\mathcal{D})}[\rho](K_{1})\cdot\\{\rho(a)\\}\cdot\xi_{{Bool\/}(\mathcal{D})}[\rho](K_{2}))$

###### Proof.

For the sake of avoiding clutter, we write $\xi$ for
$\xi_{{Bool\/}(\mathcal{D})}[\rho]$. We start with the right to left
inclusion. Let
$r\in\mathord{\downarrow_{R}}(\xi(K_{1})\cdot\\{\rho(a)\\}\cdot\xi(K_{2}))$.
We show that $r\in\xi(K_{1}aK_{2})$. By definition, we have
$r_{i}\in\xi(K_{i})$ for $i=1,2$ such that $r\leq r_{1}\rho(a)r_{2}$. We have
$r_{i}\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[K_{i},\rho\right]$ by
definition of $\xi=\xi_{{Bool\/}(\mathcal{D})}[\rho]$. Clearly, we also have
$\rho(a)\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[\\{a\\},\rho\right]$. By
Lemma 3.1, ${Bool\/}(\mathcal{D})$ is a quotient-closed Boolean algebra. Thus,
since $\rho$ is a multiplicative rating map, Lemma 6.7 yields
$r_{1}\rho(a)r_{2}\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[K_{1}aK_{2},\rho\right]$.
Since $r\leq r_{1}\rho(a)r_{2}$, we get
$r\in\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[K_{1}aK_{2},\rho\right]$. By
definition, this exactly says that $r\in\xi(K_{1}aK_{2})$. We turn to the
converse inclusion.

Let $r\in\xi(K_{1}aK_{2})$. We show that
$r\in\mathord{\downarrow_{R}}(\xi(K_{1})\cdot\\{\rho(a)\\}\cdot\xi(K_{2}))$.
For $i=1,2$, we let $\mathbf{H}_{i}$ as an optimal
${Bool\/}(\mathcal{D})$-cover (for $\rho$) of $K_{i}$ for $i=1,2$. By
definition, we have $\mathcal{I}[\rho](\mathbf{H}_{i})=\xi(K_{i})$. Since
$K_{1},K_{2}\in\mathcal{D}$, we may apply Lemma 3.6 to build a
${Bool\/}(\mathcal{D})$-cover $\mathbf{H}$ of $K_{1}aK_{2}$ such that for
every $H\in\mathbf{H}$, there exist $H_{1}\in\mathbf{H}_{1}$ and
$H_{2}\in\mathbf{H}_{2}$ such that $H\subseteq H_{1}aH_{2}$. By hypothesis,
$r\in\xi(K_{1}aK_{2})=\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[K_{1}aK_{2},\rho\right]$.
Therefore, since $\mathbf{H}$ is a ${Bool\/}(\mathcal{D})$-cover of
$K_{1}aK_{2}$, we have $r\leq\rho(H)$ for some $H\in\mathbf{H}$. The
definition of $\mathbf{H}$ then yields $H_{1}\in\mathbf{H}_{1}$ and
$H_{2}\in\mathbf{H}_{2}$ such that $H\subseteq H_{1}aH_{2}$. This implies that
$r\leq\rho(H_{1})\cdot\rho(a)\cdot\rho(H_{2})$. Finally,
$\rho(H_{i})\in\xi(K_{i})$ for $i=1,2$ by definition of $\mathbf{H}_{i}$. This
yields
$r\in\mathord{\downarrow_{R}}(\xi(K_{1})\cdot\\{\rho(a)\\}\cdot\xi(K_{2}))$
which concludes the proof. ∎

##  7\. Characterization of ${Pol\/}(\mathcal{C})$-optimal imprints

In this section, we recall the theorem of [Pla18] for classes of the form
${Pol\/}(\mathcal{C})$ (when $\mathcal{C}$ is a finite quotient-closed Boolean
algebra). It states a characterization of ${Pol\/}(\mathcal{C})$-optimal
imprints: for a $\mathcal{C}$-compatible morphism $\alpha:A^{*}\to M$ and a
multiplicative rating map $\rho:2^{A^{*}}\to R$,
$\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\rho]$ is characterized as the
least subset of $M\times R$ satisfying specific properties. When used in the
special case when $\rho$ is nice, one obtains a least fixpoint procedure for
computing $\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\rho]$ from $\alpha$
and $\rho$. By Proposition 4.9, this yields an algorithm for solving
${Pol\/}(\mathcal{C})$-covering. However, deciding
${Pol\/}(\mathcal{C})$-covering is not our motivation here: we need this
characterization in order to use it as a subresult when proving Theorem 5.3.

Unfortunately, there are technical complications. When we apply the
characterization as a subresult, we shall do so for rating maps which are not
multiplicative, only quasi-multiplicative (as expected, we build them using
the constructions presented in Section 6). This case is not covered by the
statement of [Pla18], which only deals with (true) multiplicative rating maps.
Consequently, we have to generalize this statement. We avoid redoing the whole
proof, by obtaining the generalized statement as a corollary of the original
one from [Pla18]. Additionally, we take this opportunity to slightly tweak the
original statement in order to better accommodate our use of the theorem in
Sections 8 and 9.

We first present the theorem and then focus on its proof. We fix an arbitrary
finite quotient-closed Boolean algebra $\mathcal{C}$ for the presentation.

###  7.1. Statement

Consider a $\mathcal{C}$-compatible morphism $\alpha:A^{*}\to M$ and a rating
map $\rho:2^{A^{*}}\to R$ which is quasi-multiplicative (there is no other
constraint on $\rho$, in particular, it need not be nice). Recall that since
$\alpha$ is $\mathcal{C}$-compatible, we know that for every $s\in M$,
$[s]_{\mathcal{C}}$ is well-defined as a $\sim_{\mathcal{C}}$-class containing
$\alpha^{-1}(s)$. We say that a subset $S\subseteq M\times R$ is
_${Pol\/}(\mathcal{C})$ -saturated_ (for $\alpha$ and $\rho$) when it
satisfies the following properties:

  1. (1)

_Trivial elements:_ For every $w\in A^{*}$, $(\alpha(w),\rho(w))\in S$.

  2. (2)

_Downset:_ We have $S=\mathord{\downarrow_{R}}S$.

  3. (3)

_Multiplication_ : For every $(s_{1},r_{1}),(s_{2},r_{2})\in S$, we have
$(s_{1}s_{2},r_{1}r_{2})\in S$.

  4. (4)

_${Pol\/}(\mathcal{C})$ -closure_: For every pair of (multiplicative)
idempotents $(e,f)\in S$, we have:

$(e,f\cdot\rho([e]_{\mathcal{C}})\cdot f)\in S.$

We prove the following statement as a corollary of [Pla18, Theorem 6.5].

######  Theorem 7.1.

Consider a $\mathcal{C}$-compatible morphism $\alpha:A^{*}\to M$ and a quasi-
multiplicative rating map $\rho:2^{A^{*}}\to R$. Moreover, let $S$ be the
least ${Pol\/}(\mathcal{C})$-saturated subset of $M\times R$. Then,

$\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\rho]=\mathord{\downarrow_{R}}\big{\\{}(s,\mu_{\rho}(r))\mid(s,r)\in
S\big{\\}}.$

Recall that a (true) multiplicative rating map $\rho:2^{A^{*}}\to R$ is also
quasi-multiplicative for the endomorphism $\mu_{\rho}$ defined as the identity
on $R$ (see Remark 6.5). Thus, in this case, Theorem 7.1 yields that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\rho]=\mathord{\downarrow_{R}}S=S$
where $S$ is the least ${Pol\/}(\mathcal{C})$-saturated subset of $M\times R$.
This is the original statement of [Pla18]. When $\rho$ is a nice
multiplicative rating map, it is clear that one may compute the least
${Pol\/}(\mathcal{C})$-saturated subset of $M\times R$ with a least fixpoint
algorithm. Therefore, we get an algorithm for ${Pol\/}(\mathcal{C})$-covering
by Proposition 4.9.

######  Remark 7.2.

There is a difference between Theorem 7.1 for ${Pol\/}(\mathcal{C})$ and
Theorem 5.3 for ${BPol\/}(\mathcal{C})$: the latter is restricted to nice
rating maps while this is not the case for the former. As explained in Remark
5.4, while it is easy to miss, this difference is crucial.

###  7.2. Proof of Theorem 7.1

We fix a $\mathcal{C}$-compatible morphism $\alpha:A^{*}\to M$ and a quasi-
multiplicative rating map $\rho:2^{A^{*}}\to R$. Since $\rho$ is quasi-
multiplicative, we have a semiring structure $(R,+,\cdot)$ on $R$ and an
endomorphism $\mu_{\rho}$ of $(R,+)$ satisfying the appropriate axioms.
Finally, we let $S$ as the least ${Pol\/}(\mathcal{C})$-saturated subset of
$M\times R$ for $\alpha$ and $\rho$. We show that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\rho]=\mathord{\downarrow_{R}}\big{\\{}(s,\mu_{\rho}(r))\mid(s,r)\in
S\big{\\}}$.

We first prove that the surjective restriction of $\rho$ is a _true_
multiplicative rating map (for a new multiplication on the rating set which is
distinct from “$\cdot$”). This allows us to apply the theorem of [Pla18].

We define a new multiplication on $R$ that we denote by “$\odot$”. For every
$q,r\in R$, we define $q\odot r=\mu_{\rho}(qr)$. It is immediate from Axiom 1
in the definition of quasi-multiplicative rating maps that “$\odot$” is
associative. Moreover, since $\mu_{\rho}$ is an endomorphism of $(R,+)$, one
may verify that “$\odot$” distributes over addition and that the element
$0_{R}$ is a zero for “$\odot$”. Yet, note that $(R,+,\odot)$ need not be a
semiring: “$\odot$” might not have a neutral element.

Axiom 2 in the definition of quasi-multiplicative rating maps solves this
issue. It implies that for $K_{1},K_{2}\subseteq A^{*}$, we have
$\rho(K_{1}K_{2})=\rho(K_{1})\odot\rho(K_{2})$. Thus, the rating map $\rho$ is
a semigroup morphism from $(2^{A^{*}},\cdot)$ to $(R,\cdot)$. Let
$Q=\rho(2^{A^{*}})\subseteq R$ and let $\tau:2^{A^{*}}\to Q$ be the surjective
restriction of $\rho$. It follows that $(Q,+,\odot)$ is an idempotent semiring
(the neutral element is $\rho(\varepsilon)=\tau(\varepsilon)\in Q$) and
$\tau:(2^{A^{*}},\cup,\cdot)\to(Q,+,\odot)$ is a semiring morphism, _i.e._ a
multiplicative rating map. Additionally, since we defined $\tau$ as the
surjective restriction of $\rho$, it is immediate that,

$\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\rho]=\mathord{\downarrow_{R}}\left(\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\tau]\right)$

Moreover, since $\tau$ is a true multiplicative rating map, we may apply the
theorem of [Pla18]. Let $T$ be the least ${Pol\/}(\mathcal{C})$-saturated of
$M\times Q$ for $\alpha$ and $\tau$. We obtain from [Pla18, Theorem 6.5] that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\tau]=T$. Hence, it now suffices
to prove that,

$\mathord{\downarrow_{R}}T=\mathord{\downarrow_{R}}\\{(s,\mu_{\rho}(r))\mid(s,r)\in
S\\}.$ (3)

Indeed, this clearly implies
$\mathcal{P}_{{Pol\/}(\mathcal{C})}^{\alpha}[\rho]=\mathord{\downarrow_{R}}\big{\\{}(s,\mu_{\rho}(r))\mid(s,r)\in
S\big{\\}}$ which concludes the proof of Theorem 7.1.

######  Remark 7.3.

We are dealing with two strongly connected ${Pol\/}(\mathcal{C})$-saturated
sets. Namely, $S\subseteq M\times R$ and $T\subseteq M\times Q\subseteq
M\times R$. However, there is a subtle difference between the two. By
definition, $S$ is ${Pol\/}(\mathcal{C})$-saturated for $\alpha$ and $\rho$.
This notion depends on the original multiplication “$\cdot$” of $R$. On the
other hand, $T$ is ${Pol\/}(\mathcal{C})$-saturated for $\alpha$ and $\tau$.
By definition of $\tau$, this notion depends on the new multiplication
“$\odot$” of $Q$.

It now remains to prove (3). We handle the two inclusions separately. First,
we show that
$\mathord{\downarrow_{R}}T\subseteq\mathord{\downarrow_{R}}\\{(s,\mu_{\rho}(r))\mid(s,r)\in
S\\}$. This boils down to proving that for every $(s,q)\in T$, we have $r\in
R$ such that $(s,r)\in S$ and $q\leq\mu_{\rho}(r)$. By definition, $T$ is the
least ${Pol\/}(\mathcal{C})$-saturated subset of $M\times Q$ for $\alpha$ and
$\tau$. Therefore, every pair $(s,q)\in T$ is built from trivial elements
using downset, multiplication and ${Pol\/}(\mathcal{C})$-closure (here, the
multiplication is “$\odot$” on $Q$, see Remark 7.3). We proceed by induction
on this construction.

If $(s,q)$ is a trivial element, we have $w\in A^{*}$ such that $s=\alpha(w)$
and $q=\tau(w)=\rho(w)$. We have $(s,q)\in S$ since $S$ is
${Pol\/}(\mathcal{C})$-saturated for $\alpha$ and $\rho$. Moreover,
$q=\mu_{\rho}(q)$ by Fact 6.6 since $q=\rho(w)$ which concludes this case. We
turn to downset: we have $q^{\prime}\in R$ such that $(s,q^{\prime})\in T$ and
$q\leq q^{\prime}$. Induction yields $r\in R$ such that $(s,r)\in S$ and
$q^{\prime}\leq\mu_{\rho}(r)$. Thus, $q\leq\mu_{\rho}(r)$ which concludes this
case. We turn to multiplication. In that case, we have
$(s_{1},q_{1}),(s_{2},q_{2})\in T$ such that $s=s_{1}s_{2}$ and $q=q_{1}\odot
q_{2}$. For $i=1,2$, induction yields $r_{i}\in R$ such that $(s_{i},r_{i})\in
S$ and $q_{i}\leq\mu_{\rho}(r_{i})$. Since $S$ is
${Pol\/}(\mathcal{C})$-saturated for $\alpha$ and $\rho$, we obtain
$(s,r_{1}r_{2})\in S$. Moreover, Axiom 1 in the definition of quasi-
multiplicative rating maps yields,

$q=q_{1}\odot
q_{2}=\mu_{\rho}(q_{1}q_{2})\leq\mu_{\rho}(\mu_{\rho}(r_{1})\mu_{\rho}(r_{2}))=\mu_{\rho}(r_{1}r_{2})$

This concludes the proof for this case. It remains to handle
${Pol\/}(\mathcal{C})$-closure. In that case, we have a pair of idempotents
$(e,f)\in T$ such that $s=e$ and $q=f\odot\tau([e]_{\mathcal{C}})\odot f$
(here, $f$ is an idempotent of $(R,\odot)$ since $T$ is
${Pol\/}(\mathcal{C})$-saturated for $\alpha$ and $\tau$). Induction yields
$r\in R$ such that $(e,r)\in S$ and $f\leq\mu_{\rho}(r)$. Since $(R,\cdot)$ is
a finite monoid, there exists a number $p\geq 1$ such that $r^{p}$ is an
idempotent of $(R,\cdot)$. Since $S$ is ${Pol\/}(\mathcal{C})$-saturated for
$\alpha$ and $\rho$, we obtain from closure under multiplication that
$(e,r^{p})\in S$. Together with ${Pol\/}(\mathcal{C})$-closure, this yields
$(e,r^{p}\rho([e]_{\mathcal{C}})r^{p})\in S$. Since $f\leq\mu_{\rho}(r)$ and
$f$ is an idempotent of $(R,\odot)$, we obtain,

$f\odot\tau([e]_{\mathcal{C}})\odot f=f\odot\rho([e]_{\mathcal{C}})\odot
f\leq\mu_{\rho}(r^{p}\rho([e]_{\mathcal{C}})r^{p})$

This concludes the proof for the inclusion
$\mathord{\downarrow_{R}}T\subseteq\mathord{\downarrow_{R}}\\{(s,\mu_{\rho}(r))\mid(s,r)\in
S\\}$ in (3).

We turn to the converse inclusion:
$\mathord{\downarrow_{R}}\\{(s,\mu_{\rho}(r))\mid(s,r)\in
S\\}\subseteq\mathord{\downarrow_{R}}T$. It suffices to show that for every
$(s,r)\in S$, we have $(s,\mu_{\rho}(r))\in\mathord{\downarrow_{R}}T$. By
definition, $S$ is the least ${Pol\/}(\mathcal{C})$-saturated subset of
$M\times R$ for $\alpha$ and $\rho$. Hence, every pair $(s,r)\in S$ is built
from trivial elements using downset, multiplication and
${Pol\/}(\mathcal{C})$-closure (here, the multiplication is “$\cdot$” on $R$,
see Remark 7.3). We proceed by induction on this construction.

If $(s,r)$ is a trivial element, we have $w\in A^{*}$ such that $s=\alpha(w)$
and $r=\rho(w)=\tau(w)$. By Fact 6.6, we have $\mu_{\rho}(r)=\rho(w)$. Thus,
$(s,\mu_{\rho}(r))\in T\subseteq\mathord{\downarrow_{R}}T$ since $T$ is
${Pol\/}(\mathcal{C})$-saturated for $\alpha$ and $\tau$. We turn to downset:
we have $r^{\prime}\in R$ such that $(s,r^{\prime})\in T$ and $r\leq
r^{\prime}$. Induction yields
$(s,\mu_{\rho}(r^{\prime}))\in\mathord{\downarrow_{R}}T$. Thus, since
$\mu_{\rho}(r)\leq\mu_{\rho}(r^{\prime})$, we get
$(s,\mu_{\rho}(r))\in\mathord{\downarrow_{R}}\mathord{\downarrow_{R}}T=\mathord{\downarrow_{R}}T$
as desired. We turn to multiplication. In that case, we have
$(s_{1},r_{1}),(s_{2},r_{2})\in S$ such that $s=s_{1}s_{2}$ and
$r=r_{1}r_{2}$. By induction, we obtain that
$(s_{i},\mu_{\rho}(r_{i}))\in\mathord{\downarrow_{R}}T$ for $i=1,2$. This
yields $q_{1},q_{2}\in Q$ such that $(s_{i},q_{i})\in T$ and
$\mu_{\rho}(r_{i})\leq q_{i}$ for $i=1,2$. Since $T$ is
${Pol\/}(\mathcal{C})$-saturated for $\alpha$ and $\tau$, it follows that
$(s,q_{1}\odot q_{2})\in T$ by closure under multiplication. Moreover,

$\mu_{\rho}(r)=\mu_{\rho}(r_{1}r_{2})=\mu_{\rho}(\mu_{\rho}(r_{1})\mu_{\rho}(r_{2}))\leq\mu_{\rho}(q_{1}q_{2})=q_{1}\odot
q_{2}$

Altogether, we obtain $(s,\mu_{\rho}(r))\in\mathord{\downarrow_{R}}T$ as
desired. It remains to handle ${Pol\/}(\mathcal{C})$-closure. We have a pair
of multiplicative idempotents $(e,f)\in S$ such that $s=e$ and
$r=f\cdot\rho([e]_{\mathcal{C}})\cdot f$ (here, $f$ is an idempotent of
$(R,\cdot)$ since $S$ is ${Pol\/}(\mathcal{C})$-saturated for $\alpha$ and
$\rho$). By induction, we have
$(e,\mu_{\rho}(f))\in\mathord{\downarrow_{R}}T$. Thus, we obtain $q\in Q$ such
that $(e,q)\in T$ and $\mu_{\rho}(f)\leq q$. Since $(R,\odot)$ is a finite
semigroup, there exists a number $p\geq 1$ such the multiplication of $p$
copies of $q$ with “$\odot$” is an idempotent of $(R,\odot)$. We write $g\in
R$ for this idempotent. Since $T$ is ${Pol\/}(\mathcal{C})$-saturated for
$\alpha$ and $\tau$, we obtain from closure under multiplication that
$(e,g)\in T$. Together with ${Pol\/}(\mathcal{C})$-closure, this yields
$(e,g\odot\tau([e]_{\mathcal{C}})\odot g)\in T$. Since $\mu_{\rho}(f)\leq q$
and $f$ is an idempotent of $(R,\cdot)$, one may verify that,

$\mu_{\rho}(f\cdot\rho([e]_{\mathcal{C}})\cdot
f)=\mu_{\rho}(f\cdot\tau([e]_{\mathcal{C}})\cdot f)\leq
g\odot\tau([e]_{\mathcal{C}})\odot g$

Altogether, we obtain
$(s,\mu_{\rho}(r))=(e,\mu_{\rho}(f\cdot\rho([e]_{\mathcal{C}})\cdot
f))\in\mathord{\downarrow_{R}}T$ as desired. This concludes the proof.

##  8\. Soundness in Theorem 5.3

We may now start the proof of Theorem 5.3. In this section, we establish that
the statement is sound. The proof is divided in two parts. First, we present a
preliminary result, which applies to the Boolean closure operation in general,
_i.e._ , to classes of the form ${Bool\/}(\mathcal{D})$ when $\mathcal{D}$ is
an arbitrary lattice. Then, we apply this preliminary result in the special
case when $\mathcal{D}={Pol\/}(\mathcal{C})$ (for $\mathcal{C}$ a finite
quotient-closed Boolean algebra) to establish the soundness direction in
Theorem 5.3.

###  8.1. Preliminary result

We first introduce terminology that we need to state our result. We fix a
lattice $\mathcal{D}$. Moreover, we let $\rho:2^{A^{*}}\to R$ be a rating map.

Using induction, we define a rating map $\tau_{n}:2^{A^{*}}\to Q_{n}$ for
every $n\in{\rm Nature}$. When $n=0$, the rating set $Q_{0}$ is $(2^{R},\cup)$
and $\tau_{0}$ is defined as follows,

$\begin{array}[]{llll}\tau_{0}:&(2^{A^{*}},\cup)&\to&(2^{R},\cup)\\\
&K&\mapsto&\\{\rho(w)\mid w\in K\\}.\end{array}$

It is immediate by definition that $\tau_{0}$ is indeed a rating map (_i.e._ ,
a monoid morphism).

Assume now that $n\geq 1$ and that $\tau_{n-1}:2^{A^{*}}\to Q_{n-1}$ is
defined. Recall that $\rho_{*}:A^{*}\to R$ denotes the canonical map
associated to the rating map $\rho$. We define $\tau_{n}$ as:

$\tau_{n}=\zeta_{\mathcal{D}}^{\rho_{*}}[\tau_{n-1}].$

By Proposition 6.2, $\tau_{n}$ is indeed a rating map. By definition, this
means that for all $n\geq 1$, the rating set $Q_{n}$ of $\tau_{n}$ is

$Q_{n}=(2^{R\times Q_{n-1}},\cup).$

We complete this definition with maps $f_{n}:Q_{n}\to 2^{R}$ for $n\in{\rm
Nature}$, defined by induction on $n$.

  * •

For $n=0$, let $T\in Q_{0}=2^{R}$. We define:

$f_{0}(T)=\mathord{\downarrow_{R}}\\{r_{1}+\cdots+r_{k}\mid
r_{1},\dots,r_{k}\in T\\}.$

  * •

For $n\geq 1$, let $T\in Q_{n}=2^{R\times Q_{n-1}}$. We define:

$f_{n}(T)={\mathord{\downarrow_{R}}}\left\\{r_{1}+\cdots+r_{k}\mid\begin{array}[]{c}\text{there
exist $(r_{1},T_{1}),\dots,(r_{k},T_{k})\in T$ such that}\\\
\text{$r_{1}+\cdots+r_{k}\in f_{n-1}(T_{i})$ for every $i\leq
k$}\end{array}\right\\}.$

The following fact is immediate from the definition.

######  Fact 8.1.

For every $n\in{\rm Nature}$ and $U,U^{\prime}\in Q_{n}$ such that $U\subseteq
U^{\prime}$, we have $f_{n}(U)\subseteq f_{n}(U^{\prime})$.

We may now state the preliminary result that we shall use in our soundness
direction of Theorem 5.3.

######  Proposition 8.2.

Consider a language $L\in\mathcal{D}$. Then, the following inclusion holds:

$\bigcap_{n\in{\rm
Nature}}f_{n}(\tau_{n}(L))\subseteq\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[L,\rho\right].$

###### Proof.

The proof is based on the following more involved statement which is proved by
induction on $n\in{\rm Nature}$.

######  Lemma 8.3.

Let $n\in{\rm Nature}$ and
$L,K_{0},\dots,K_{n},H_{0},\dots,H_{n}\in\mathcal{D}$ such that
$\\{K_{i}\setminus H_{i}\mid i\leq n\\}$ is a cover of $L$. Then, for every
$s\in f_{2n}(\tau_{2n}(L))$, there exists $j\leq n$ such that
$s\leq\rho(K_{j}\setminus H_{j})$.

Before proving the lemma, let us use it to prove the first property described
in Proposition 8.2. Let $L\in\mathcal{D}$ be a language. We write $S$ for the
set,

$S=\bigcap_{n\in{\rm Nature}}f_{n}(\tau_{n}(L)).$

We show that
$S\subseteq\mathcal{I}_{{Bool\/}(\mathcal{D})}\left[L,\rho\right]$. First, we
prove the following fact which describes a special optimal
${Bool\/}(\mathcal{D})$-cover of $L$ for $\rho$.

######  Fact 8.4.

There exist $n\in{\rm Nature}$ and
$K_{0},\dots,K_{n},H_{0},\dots,H_{n}\in\mathcal{D}$ such that
$\\{K_{i}\setminus H_{i}\mid i\leq n\\}$ is an optimal
${Bool\/}(\mathcal{D})$-cover of $L$ for $\rho$.

###### Proof.

Let $\mathbf{H}$ be an arbitrary optimal ${Bool\/}(\mathcal{D})$-cover of $L$
for $\rho$. Each $V\in\mathbf{H}$ is the Boolean combination of languages in
$\mathcal{D}$. We put it in disjunctive normal form. Each disjunct is an
intersection languages belonging to $\mathcal{D}$, or whose complement belongs
to $\mathcal{D}$. Since $\mathcal{D}$ is lattice, both $\mathcal{D}$ and the
complement class ${co\/}\textup{-}\mathcal{D}$ are closed under intersection.
Therefore, each disjunct in the disjunctive normal form of $V$ is actually of
the form $K\setminus H$, where $K,H$ both belong to $\mathcal{D}$. We let
$\mathbf{K}$ as the set of all languages $K\setminus H$ which are a disjunct
in the disjunctive normal form of some $V\in\mathbf{H}$. Clearly, $\mathbf{K}$
remains a ${Bool\/}(\mathcal{D})$-cover of $L$ since $\mathbf{H}$ was one.
Moreover, it is immediate that
$\mathcal{I}[\rho](\mathbf{K})\subseteq\mathcal{I}[\rho](\mathbf{H})$ since
every language in $\mathbf{K}$ is included in a language of $\mathbf{H}$.
Hence, $\mathbf{K}$ remains an optimal ${Bool\/}(\mathcal{D})$-cover of $L$
for $\rho$ since $\mathbf{H}$ was one. ∎