BRICS RS-03-28 Ésik & Larsen: Regular Languages Definable by Lindström Quantifiers BRICS

Basic Research in Computer Science

Regular Languages Definable by Lindström Quantifiers

Zoltán Ésik Kim G. Larsen BRICS Report Series RS-03-28 ISSN 0909-0878 August 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Zoltán Ésik & Kim G. Larsen.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/03/28/

Regular Languages Definable by Lindström Quantifiers^{∗}

Zoltán Ésik^{†} Dept. of Computer Science

University of Szeged

P.O.B. 652 6701 Szeged, Hungary

ze@inf.u-szeged.hu

Kim G. Larsen Dept. of Computer Science Aalborg University Fredrik Bajers Vej 7E 9220 Aalborg, Denmark kgl@cs.auc.dk

August 19, 2003

Abstract

In our main result, we establish a formal connection between Lindström quantifiers with respect to regular languages and the double semidirect product of finite monoids with a distinguished set of generators. We use this correspondence to characterize the expressive power of Lindström quantifiers associated with a class of regular languages.

1 Introduction

By the classic result of Büchi [6], Elgot [12] and Trakhtenbrot [40], the regular languages are exactly those definable by the sentences of a certain monadic second-order logic over words. Moreover, Mc Naughton and Papert [22] proved that the first-order sentences of this logic define an important subclass of the regular languages, namely the star-free languages. By Schützenberger’s theorem [29], the star-free languages are exactly those that can be recognized by the aperiodics, i.e., by those finite monoids containing no nontrivial groups.

∗Research supported by BRICS (Basic Research in Computer Science), Aalborg, Denmark. A preliminary version of this paper appeared as RS 02 20, BRICS Report Series, 2002.

†Supported in part by a grant from the National Foundation of Hungary for Scientific Research and by the Japan Society for the Promotion of Science.

Because of the limited expressive power of first-order logic on words, and in the search for characterizations of other important subclasses of regular languages in terms of formal logic, Straubing, Therien and Thomas [34, 35] studied generalized, or modular quantifiers ∃^{(m,r)}, where m ≥ 2 and r = 0, …, m − 1, with the following meaning: A word u satisfies a sentence ∃^{(m,r)}x.φ iff the number of assignments of positions in u to the variable x satisfying φ is congruent to r modulo m. They proved that a language is definable in the logic involving, in addition to first-order quantifiers, the above modular quantifiers iff its syntactic monoid is finite and solvable, i.e., it contains only solvable groups. This class of regular languages first arose in [30, 36]. And if no first-order quantifiers are allowed, then a language is definable iff its syntactic monoid is a finite solvable group. In fact, Straubing, Therien and Thomas also studied the more general setting when the moduli of the generalized quantifiers in the logic are restricted to a finite set of (prime) numbers. See also Straubing, Therien [33] for a more recent account, and Baziramwabo, McKenzie, Therien [4] for a corresponding extension of linear temporal logic with modular counting.

In order to express regular languages having non-solvable syntactic monoids, Barrington, Immerman and Straubing [3] associated a family of quantifiers with each finite group containing a quantifier corresponding to each group element. When the group is cyclic of order m, the associated quantifiers are essentially the modular quantifiers ∃^{(m,r)}. They showed that a language is definable in first-order logic enriched with group quantifiers corresponding to the members of a subclass G of the finite groups iff the language is regular (so that its syntactic monoid is finite), and every simple group that divides the syntactic monoid of the language divides a group in G. (See, e.g., [11] for a definition of when a group divides a group or a monoid.) Moreover, if only group quantifiers are allowed, then a language is definable iff in addition to the above conditions its syntactic monoid is a group. When G is empty, by Schützenberger’s theorem one obtains the Mc Naughton–Papert characterization of first-order definable languages. The theorem of Barrington, Immerman and Straubing easily extends to quantifiers associated with finite monoids.

The quantifiers associated with finite monoids and groups, and thus the modular quantifiers, are all special cases of (simple) Lindström quantifiers associated with (regular) languages, defined in [7]. (For more general treatments of Lindström quantifiers the reader is referred to Lindström [19] and Ebbinghaus and Flum [10], Chapter 12. See also the generalized quantifiers of Immerman [16] and the LNCS volume Väänänen [41].) By the results of Barrington, Immerman, Straubing [3], extended to monoids, it follows that when the Lindström quantifiers are associated with regular languages, then only regular languages can be defined. Moreover, when G is a class of finite groups (or monoids), and L_{G} is the class of regular languages that can be recognized by the members of the class G, then a language L is definable in first-order logic enriched with Lindström quantifiers associated with the languages in L_{G} iff L is regular and every simple group divisor of the syntactic monoid of L divides a group (or monoid) in G.

Our initial motivation for studying regular Lindström quantifiers was the question of characterizing those classes L of regular languages which are expressively complete in the sense that every regular language is definable by a sentence possibly involving, in addition to ordinary quantifiers, Lindström quantifiers with respect to the languages in L. By the classic theorem of Büchi, Elgot, and Trakhtenbrot, first-order logic, enriched with Lindström quantifiers with respect to the languages in an expressively complete class L, has the same expressive power as monadic second-order logic. Moreover, by the above-mentioned results of Barrington, Immerman and Straubing, a necessary condition of the expressive completeness of a class L of regular languages is that L be group-complete, i.e., every finite (non-abelian simple) group be a divisor of the syntactic monoid of a language in L. We will show that this condition, together with a condition involving the existence of certain cycles in the syntactic monoids of the languages in L, which is roughly equivalent to the expressibility of all of the one-letter languages (a^{n})^{∗}, n ≥ 2, is necessary and sufficient as long as L satisfies certain natural assumptions. On the other hand, we show that neither condition is sufficient by itself. But when L is closed with respect to taking quotients and admits padding, then L is expressively complete iff it is group-complete and at least one of the one-letter languages (a^{n})^{∗}, n ≥ 2 is definable.

Formal logic in connection with words and languages has several general techniques such as model theoretic games and deep algebraic techniques developed in the theory of finite semigroups and automata. A general account of these methods is given in Straubing [31]. In particular, the semidirect product and the wreath product, and their symmetric versions, the double semidirect product^{1} and the block product, defined by Rhodes and Tilson [28] (or the triple product of Eilenberg [11]), and the Krohn-Rhodes theorem [17] have been the fundamental tools for several of the aforementioned results. The same holds for our investigation. In our main technical result, Theorem 9.5, we make a bridge between Lindström quantifiers and the double semidirect product, or the block product. Particular instances of this correspondence appear in above cited works, see e.g. the proofs of lemmas VI.1.2, VI.1.4, VII.2.2. and VII.2.3 in Straubing [31]. In fact, we will make use of a version of the double semidirect product and the block product that concerns finite monoids with a distinguished set of generators.

For the connection between circuit complexity and generalized quantifiers, we refer to Barrington, Immerman, Straubing [3], Barrington, Compton, Straubing, Therien [2], and the last two chapters of Straubing [31]. For second-order Lindström quantifiers and the relation of Lindström quantifiers to leaf language definability, see Burtschick, Vollmer [7], Peichl, Vollmer [23], Galota, Vollmer [15]. For results regarding the connection between the semidirect product and the expressive power of temporal logics, see Cohen, Perrin, Pin [8], Therien, Wilke [37] and Baziramwabo, McKenzie, Therien [4]. The last paragraph of the paper McKenzie, Schwentick, Therien, Vollmer [20] contains an indication of the possibility of handling nested monoidal quantifiers in the logical framework by series connections of 2-way automata. The texts Pin [25], Straubing [31] and Thomas [38, 39] are excellent surveys of the subject.

The paper is organized as follows. In Section 2, we associate a Lindström quantifier with any language and in Section 3, we establish some simple properties of Lindsröm quantifiers. In Section 4, we relate Lindsröm quantifiers to literal varieties of languages. Section 5 is devoted to mg-pairs, that is monoids equipped with a distinguished set of generators, and Section 6 to relativization. In Sectionr̃efsec-double, we define the operations of double semidirect product and block product on mg-pairs. Section 8 is devoted to varieties of finite mg-pairs. We extend the double semidirect product and the block product to varieties. In Section 9, we establish a formal connection between Lindsröm quantifiers and the double semidirect product (block product, respectively) on varieties. In Section 10, we review the Krohn-Rhodes theorem and establish some of its consequences. In Section 11, we apply the results of Section 9 and 10 to provide additional characterizations of the expressive power of several concrete classes of Lindström quantifiers.

1The double semidirect product is called the bilateral semidirect product in [31].

We have tried to make the paper accessible not only for the experts but also for a larger audience.

2 Lindström quantifiers, defined

For each alphabet (i.e., finite nonempty set) Σ, the formulas over Σ are defined as follows. We assume that a fixed countable set of variables is given, and that each alphabet comes with a linear order defined on the letters of the alphabet.

• For each a ∈ Σ and each variable x, P_{a}(x) is an (atomic) formula. Moreover, when x, y are variables, x < y is an (atomic) formula.

• For all formulas φ and ψ, both φ ∨ ψ and ¬φ are formulas. Moreover, false is a formula.

• Suppose that K ⊆ Δ^{∗}, where Δ = {b_{1}, …, b_{m}}, m ≥ 1 is some alphabet, ordered as shown. Then for all variables x and formulas φ_{b_{i}}, b_{i} ∈ Δ, i < m,

Q_{K}x.⟨φ_{b_{1}}, …, φ_{b_{m−1}}⟩  (1)

is a formula.

We say that the variable x is bound in (1). The set of free variables of a formula is defined in the standard way. We identify any two formulas that differ only in the bound variables. Thus, we may assume that the bound variables of a formula are pairwise different, and different from any free variable. A formula with no free variables is called a sentence. The result of the substitution of a variable y for a (free) variable x in a formula φ, denoted φ[y/x], is defined in the standard way.

Suppose that u is a word in Σ^{∗} of length n, say u = u_{1} … u_{n}, where the u_{i} are letters. Moreover, suppose that φ is a formula over Σ whose free variables are contained in the finite set V. Given a function λ : V → [n], where [n] = {1, …, n}, we say that (u, λ) satisfies φ, in notation (u, λ) ⊧ φ, if

• φ is of the form P_{a}(x) and u_{λ(x)} = a; or φ is of the form x < y and λ(x) < λ(y), or

• φ is of the form φ_{1} ∨ φ_{2} and (u, λ) ⊧ φ_{1} or (u, λ) ⊧ φ_{2}; or φ is of the form ¬ψ and it is not the case that (u, λ) ⊧ ψ, or

• φ is of the form (1) and the characteristic word [7] \overline{u} = \overline{u}_{1} … \overline{u}_{n} determined by (u, λ) and the formula belongs to K, where for each i ∈ [n], \overline{u}_{i} is the least b_{j}, j < m such that we have (u, κ) ⊧ φ_{b_{j}} for the function κ : V ∪ {x} → [n] with κ(y) = λ(y), for all y ∈ V, and κ(x) = i.^{2} When no such b_{j} exists, we define \overline{u}_{i} = b_{m}. In particular, when u = ϵ is the empty word and V = ∅, then (u, λ) satisfies the formula (1) iff ϵ ∈ K.

For all pairs (u, λ), relation (u, λ) ⊧ false does not hold.

We will rely on the following lemma whose proof is standard.

Lemma 2.1 Suppose that φ is a formula over Σ and X and Y both contain the free variables of φ. Then for any word u = u_{1} … u_{n} ∈ Σ^{∗} and functions κ : X → [n] and λ : Y → [n] that agree on all free variables of φ, (u, κ) ⊧ φ iff (u, λ) ⊧ φ.

Suppose that φ, ψ are formulas over Σ whose free variables are in X. We say that φ and ψ are equivalent if for all words u = u_{1} … u_{n} ∈ Σ^{∗} and functions λ : X → [n], (u, λ) ⊧ φ iff (u, λ) ⊧ ψ.

Some notational conventions. In the sequel, in addition to the boolean connectives ∨ and ¬, we will also use the connectives ∧ (conjunction), → (implication) and ↔ (equivalence). These are treated as abbreviations. We use true to denote ¬false. Moreover, we write x ≤ y for ¬(y < x), x = y for (x ≤ y) ∧ (y ≤ x), etc. In quantified formulas (1), we may assume that the subformulas φ_{b_{i}} are pairwise inconsistent, i.e., no pair (u, λ) satisfies two or more φ_{b_{i}}. Then, we may define φ_{b_{m}} as ¬(⋁_{i<m} φ_{b_{i}}) and write (1) as Q_{K}x.⟨φ_{b_{i}}⟩_{b_{i}∈Δ}. Note that the ordering on Δ becomes irrelevant. Below, when writing Q_{K}x.⟨φ_{b_{i}}⟩_{b_{i}∈Δ}, we will always assume that the φ_{b_{i}} form a deterministic family, i.e., the formulas φ_{b_{i}} are pairwise inconsistent and for any appropriate (u, λ) there is some b_{i} with (u, λ) ⊧ φ_{b_{i}}. When φ_{b}, b ∈ Δ are formulas over Σ with free variables in V, a determinization of the family φ_{b}, b ∈ Δ is a family φ′_{b}, b ∈ Δ, where, given the linear order b_{1} < … < b_{n} of Δ, it holds that φ′_{b_{i}} = φ_{b_{i}} ∧ (⋀_{j<i} ¬φ_{b_{j}}), for all i < n, and φ_{b_{n}} = ⋀_{j<n} ¬φ_{b_{j}}. When φ is a sentence and V is empty, we will write u ⊧ φ whenever (u, λ) ⊧ φ for all, or for some λ : V → [n].

2When the φ_{b_{j}} contain no free variables other than x, then the function u ↦ \overline{u} is called a translation in [18] and [20].

When writing a word u in the form u = u_{1} … u_{n}, we usually assume that the u_{i} are letters, so that u is a word of length n. By a class of languages. or language class L we mean a set L(Σ^{∗}) of languages L ⊆ Σ^{∗}, for each alphabet Σ. A class of regular languages contains only regular languages. When L is a class of languages, we let Lin(L) denote the logic whose formulas are those defined above with the restriction that Lindström quantification (1) is restricted to languages K ∈ L. We also denote by Lin(L) the collection of formulas of this logic.

Example 2.2

• Suppose that K ⊆ {b_{1}, b_{2}}^{∗} is the language K_{∃} = b_{2}^{∗}b_{1}(b_{1} + b_{2})^{∗}, where we assume b_{1} < b_{2}. Then (u, λ) ⊧ Q_{K}x.⟨φ⟩ iff there is an extension κ : V ∪ {x} → [n] of λ : V → [n] such that (u, κ) ⊧ φ. Thus, the Lindtrsöm quantifier corresponding to K_{∃} is the ordinary existential quantifier. When K ⊆ {b_{1}, b_{2}}^{∗} is the language K_{∀} = b_{1}^{∗}, the corresponding Lindström quantifier is the ordinary universal quantifier.

• Suppose that M is a set of integers > 1. Let C_{M} consist of all languages C_{m}^{r} ⊆ {b_{1}, b_{2}}^{∗}, m ∈ M, r = 0, …, m − 1, where C_{m}^{r} is the set of all words u in {b_{1}, b_{2}}^{∗} such that the number of b_{1}s in u is congruent to r modulo m. Then, assuming the order b_{1} < b_{2}, Q_{C_{m}^{r}} is the “modular quantifier” ∃^{(m,r)} of Straubing, Therien and Thomas [35] and Straubing [31]. (Note that it is sufficient to allow modular quantifiers with respect to prime moduli as in [31, 35].)

• Let L_{m}^{r}, where m ≥ 1 and 0 ≤ r < m, denote the language (b_{1}^{m})^{∗}b_{1}^{r}, considered as a subset of {b_{1}}^{∗}. Then for every alphabet Σ, Q_{L_{m}^{r}}x.⟨⟩ is a sentence over Σ, and for every word u ∈ Σ^{∗}, u ⊧ Q_{L_{m}}x.⟨⟩ iff the length of u is congruent to r mod m.

• In [2], Barrington, Compton, Straubing and Therien studied the extension of firstorder logic with unary modular counting predicates x ≡ r mod m, where x is a variable, m ≥ 1 and r ∈ [m].^{3} We show that this extension can be handled by Lindström quantifiers. For every m, r as above, let K_{m}^{r} denote the two-letter language (b_{2}^{m})^{∗}b_{2}^{r−1}b_{1}(b_{1} + b_{2})^{∗}, where we assume that b_{1} < b_{2}. If u is word of length n and λ : V → [n], where V contains x, then (u, λ) satisfies Q_{K}y.⟨y = x⟩ iff

3In fact, the remainder r is taken between 0 and m − 1 in [2]. xλ is congruent to r modulo m. Conversely, Lindsröm quantification with respect to the language K_{m}^{r} is expressible by the corresponding modular counting predicate and first-order quantification. In fact, Q_{K_{m}^{r}}x.⟨φ⟩ is expressible as

∃x[(x ≡ r mod m) ∧ φ ∧ ∀y(y < x → ¬φ[y/x])].

• One can express temporal modalities by Lindström quantifiers. Recall from Pnueli [26], Cohen, Perrin, Pin [8] that the formulas of propositional linear temporal logic over an alphabet Σ are generated from atomic propositions p_{a}, a ∈ Σ, by the boolean connectives ∨ and ¬, and the next and until modalities denoted X and U. For more details and the definition of semantics we refer to [26, 8]. Let K_{X} denote the two-letter language (b_{1} + b_{2})b_{1}(b_{1} + b_{2})^{∗}, and let K_{U} denote the threeletter language b_{2}^{∗}b_{1}(b_{1} + b_{2} + b_{3})^{∗}, where we assume the orderings b_{1} < b_{2} and b_{1} < b_{2} < b_{3}, respectively. Using these notations, we can translate each formula φ of propositional temporal logic over Σ into a sentence τ(φ) involving ordinary quantifiers and Lindström quantifiers with respect to the languages K_{X} and K_{U}. We define:

1. τ(p_{a}) = ∃x.((∀y.x ≤ y) ∧ P_{a}(x)), for all a ∈ Σ.

2. τ(φ ∨ ψ) = τ(φ) ∨ τ(ψ) and τ(¬φ) = ¬τ(φ).

3. τ(Xφ) = Q_{K_{X}}x.⟨τ(φ)[≥ x]⟩, if ϵ |̸= φ, and τ(Xφ) = ψ ∨ Q_{K_{X}}x.⟨τ(φ)[≥ x]⟩, if ϵ ⊧ φ, where ψ is a sentence only satisfied by the one-letter words.

4. τ(φUψ) = Q_{K_{U}}x.⟨τ(ψ)[≥ x], τ(φ)[≥ x]⟩.

(Here, τ(φ)[≥ x] denotes a relativization of the formula τ(φ). See Straubing [31].) Then, for each word u ∈ Σ^{∗} and temporal logic formula φ, it holds that u ⊧ φ iff u ⊧ τ(φ).

Given a sentence φ in Lin(L) over the alphabet Σ, we let L_{φ} ⊆ Σ^{∗} denote the language defined by φ:

L_{φ} = {u ∈ Σ^{∗} : u ⊧ φ}.

We write Lin(L) to denote the class of all languages definable by the sentences of the logic Lin(L). Moreover, we define FO(L) = Lin(L ∪ {K_{∃}}) and FO(L) = Lin(L ∪ {K_{∃}}) = Lin(L ∪ {K_{∀}}). Thus, FO = FO(∅) is just ordinary first-order logic and FO = FO(∅) is the class of first-order definable languages of [22, 31].

Example 2.3

• When L = ∅, or when L(Σ^{∗}) = {∅, Σ^{∗}}, for each Σ, then for each alphabet Σ, Lin(L) consists of just the languages ∅ and Σ^{∗}.

• Suppose that for a one-letter alphabet {a}, L consists of the language {ϵ}, and L(Σ^{∗}) = ∅, for all other alphabets Σ. Then for each Σ, L′ = Lin(L) consists of the languages ∅, {ϵ}, Σ^{+} = Σ^{∗} − {ϵ} and Σ^{∗}. Moreover, Lin(L′) = L′.

• Let L consist of all finite languages. Then Lin(L) is the class of all finite or co-finite languages.

• Let L consist of the languages C_{m}^{r} defined in Example 2.2, where m ≥ 1 and 0 ≤ r < m. Then, as shown in Straubing, Therien, Thomas [35], Lin(L) (FO(L), respectively) is the class of all regular languages whose syntactic monoid is a solvable group (monoid, respectively). See also Section 11.

• More generally, when M denotes a set of integers ≥ 1 and C_{M} = {C_{m}^{r} : m ∈ M, 0 ≤ r < m} as above, then Lin(C_{M}) consists of those regular languages L whose syntactic monoid is a solvable group of order n such that any prime divisor of n divides an integer in M. Moreover, FO(C_{M}) consists of those regular languages L such that every subgroup of the syntactic monoid of L has this property. See Straubing, Therien, Thomas [35].

• Let K denote the collection of all languages K_{m}^{r} defined above. Then a language L belongs to FO(K) iff its syntactic monoid is quasi-aperiodic, cf. Barrington, Compton, Straubing, Therien [2] and Straubing [31]. Moreover, FO(K) = FO({K_{m}^{1} : m ≥ 1}). More generally, when M is a subset of the positive integers and K_{M} = {K_{m}^{r} : m ∈ M, r ∈ [m]}, then a characterization of the language class FO(K_{M}) is given in Ésik, Ito [14].

Some of our results will also take into account the quantification depth qd(φ) of a formula φ, defined as the maximum number of nested quantifiers in φ. For a language class L and integer n ≥ 0, we let Lin_{n}(L) (FO_{n}(L), respectively) denote the collection of all Lin(L) formulas (FO(L) formulas, respectively) whose quantification depth does not exceed n. Moreover, we denote by Lin_{n}(L) (FO_{n}(L), respectively) the class of all languages definable by sentences in Lin_{n}(L) (FO_{n}(L), respectively). Note that Lin(L) = ⋃_{n≥0} Lin_{n}(L) and FO(L) = ⋃_{n≥0} FO_{n}(L). Moreover, for every n ≥ 0, each family φ_{b}, b ∈ Δ of Lin_{n}(L) formulas has a determinization φ′_{b}, b ∈ Δ consisting of formulas in Lin_{n}(L), and similarly for families of FO_{n}(L) formulas.

For technical reasons, we also associate a language with formulas φ over Σ containing free variables. We follow the definitions in [31]. Let V denote a finite set of variables containing all of the free variables of φ. A V -structure over Σ is a word u = u_{1} … u_{n} in (Σ×P (V))^{∗}, where P (V) denotes the power set of V, such that each variable in V appears exactly once in the right hand component of a letter u_{i} = (a_{i}, X_{i}). Thus, the sets X_{i} are pairwise disjoint and their union is V. Note that the empty word ϵ is a V -structure iff V = ∅. Moreover, each letter a ∈ Σ may be identified with the pair (a, ∅). Given the V -structure u, the left hand components a_{i} determine a word v = a_{1} … a_{n} in Σ^{∗}, and the right hand components determine a function λ : V → [n], defined by λ(x) = i iff x ∈ X_{i}. Suppose that φ is a formula over Σ with free variables in V. We say that u satisfies φ, denoted u ⊧ φ, if (v, λ) ⊧ φ. The language L_{φ} defined by φ consists of all V -structures u over Σ with u ⊧ φ.

3 Elementary properties of Lindström quantification

In this section we establish some basic properties of Lindström quantification.

Proposition 3.1 For each class L of languages, it holds that L ⊆ Lin_{1}(L). Moreover, when L ⊆ L′, then Lin_{n}(L) ⊆ Lin_{n}(L′), for all n ≥ 0, so that Lin(L) ⊆ Lin(L′).

Proof. Given K ⊆ Δ^{∗} in L, where Δ = {b_{1}, …, b_{k}}, the language defined by the sentence Q_{K}x.⟨P_{b_{i}}(x)⟩_{b_{i}∈Δ} is K. The second claim is obvious. □

Lemma 3.2 Suppose that φ_{b}, b ∈ B is a deterministic family of formulas over A with free variables in {x} ∪ Y, and ψ is a formula over B whose free variables are in {x} ∪ Z, where Y and Z are disjoint. Then the formula ψ′ over the alphabet A with free variables in {x} ∪ Y ∪ Z that results from ψ by replacing each subformula of the form P_{b}(ξ), where ξ is any (free or bound) variable, by the formula φ_{b}[ξ/x], is well-defined. Let (a_{1}, Y_{1}) … (a_{n}, Y_{n}) be an Y -structure over A and for each j ∈ [n], let b_{j} ∈ B with

(a_{1}, Y_{1}) … (a_{j}, {x} ∪ Y_{j}) … (a_{n}, Y_{n}) ⊧ φ_{b_{j}}.  (2)

Suppose that Z_{1}, …, Z_{n} are disjoint subsets of Z whose union is Z, so that (b_{1}, Z_{1}) … (b_{n}, Z_{n}) is a Z-structure over B. Then for each i ∈ [n],

(a_{1}, Y_{1} ∪ Z_{1}) … (a_{i}, {x} ∪ Y_{i} ∪ Z_{i}) … (a_{n}, Y_{n} ∪ Z_{n}) ⊧ ψ′  (3)

iff

(b_{1}, Z_{1}) … (b_{i}, {x} ∪ Z_{i}) … (b_{n}, Z_{n}) ⊧ ψ.  (4)

Proof. We prove this claim by induction on the structure of ψ. The basis case can be divided into four subcases. Let i denote an integer in [n].

Case ψ = false. In this case our claim is obvious.

Case ψ = P_{b}(x), for some b ∈ B. Then ψ′ = φ_{b}. Thus, using (2) and Lemma 2.1, we have that (3) holds iff

(a_{1}, Y_{1}) … (a_{i}, {x_{i}} ∪ Y_{i}) … (a_{n}, Y_{n}) ⊧ φ_{b}

iff b = b_{i} iff (4) holds.

Case ψ = P_{b}(z), for some b ∈ B and z ∈ Z. Then ψ′ = φ_{b}[z/x]. Thus, using (2) and Lemma 2.1 again, (3) holds iff

∃j ∈ [n] z ∈ Z_{j} ∧ (a_{1}, Y_{1}) … (a_{j}, {z} ∪ Y_{j}) … (a_{n}, Y_{n}) ⊧ φ_{b}[z/x]

iff ∃j ∈ [n] z ∈ Z_{j} ∧ b = b_{j} iff (4) holds.

Case ψ = z_{1} < z_{2}, where z_{1}, z_{2} ∈ {x} ∪ Z. In this case ψ′ = ψ and (3) holds iff

(a_{1}, Z_{1}) … (a_{i}, {x} ∪ Z_{i}) … (a_{n}, Z_{n}) ⊧ z_{1} < z_{2}

iff

(b_{1}, Z_{1}) … (b_{i}, {x} ∪ Z_{i}) … (b_{n}, Z_{n}) ⊧ z_{1} < z_{2},

i.e., when (4) holds.

The induction step can be divided into three subcases.

Case ψ = ψ_{1} ∨ ψ_{2}, for some ψ_{1} and ψ_{2}. Then ψ′ = ψ′_{1} ∨ ψ′_{2}, where for j = 1, 2, ψ′_{j} is the formula that results from ψ_{j} by replacing each subformula of the form P_{b}(ξ) with φ_{b}[ξ/x]. Since by the induction hypothesis

(a_{1}, Y_{1} ∪ Z_{1}) … (a_{i}, {x} ∪ Y_{i} ∪ Z_{i}) … (a_{n}, Y_{n} ∪ Z_{n}) ⊧ ψ′_{j}

iff

(b_{1}, Z_{1}) … (b_{i}, {x} ∪ Z_{i}) … (b_{n}, Z_{n}) ⊧ ψ_{j},

for j = 1, 2, it follows that (3) holds iff (4) holds.

Case ψ = ¬ψ_{1}, for some ψ_{1}. This case is analogous to the previous one.

Case ψ = Q_{L}z_{0}.⟨τ_{d}⟩_{d∈D} for some τ_{d}, d ∈ D, where each τ_{d} is a formula over B in the free variables {x} ∪ Z ∪ {z_{0}}. Now ψ′ is Q_{L}z_{0}.⟨τ′_{d}⟩_{d∈D}, where each τ′_{d} is obtained from τ_{d} by replacing each subformula of the form P_{b}(ξ) with φ_{b}[ξ/x]. By the induction hypothesis, each τ′_{d} is well-defined. To prove that ψ′ is also well-defined, we have to show that the family τ′_{d}, d ∈ D, is deterministic, given that τ_{d}, d ∈ D is a deterministic family. But by the induction hypothesis,

(a_{1}, Y_{1} ∪ Z′_{1}) … (a_{j}, Y_{j} ∪ Z′_{j} ∪ {z_{0}}) … (a_{n}, Y_{n} ∪ Z′_{n}) ⊧ τ′_{d}

iff

(b_{1}, Z′_{1}) … (b_{j}, Z′_{j} ∪ {z_{0}}) … (b_{n}, Z′_{n}) ⊧ τ_{d},

for each d ∈ D and j ∈ [n], where Z′_{k} = Z_{k} if k ≠ i and Z′_{k} = Z_{k} ∪ {x} if k = i. Since τ_{d}, d ∈ D is deterministic, it follows that τ′_{d}, d ∈ D is also deterministic. Moreover, the characteristic word determined by the structure (a_{1}, Y_{1} ∪ Z_{1}) … (a_{i}, {x} ∪ Y_{i} ∪ Z_{i}) … (a_{n}, Y_{n} ∪ Z_{n}) and ψ′ is the same as that determined by (b_{1}, Z_{1}) … (b_{i}, {x} ∪ Z_{i}) … (b_{n}, Z_{n}) and ψ. It follows that (3) holds iff (4) does. □

Note the following special case of Lemma 3.2.

Corollary 3.3 Suppose that φ_{b}, b ∈ B is a deterministic family of formulas over A with free variables in {x} ∪ Y and ψ is formula over B with no free variable other than x. Let ψ′ denote the formula over the alphabet A with free variables in {x} ∪ Y that results from ψ by replacing each subformula of the form P_{b}(ξ), where ξ is any (free or bound) variable by the formula φ_{b}[ξ/x]. Let (a_{1}, Y_{1}) … (a_{n}, Y_{n}) be an Y -structure over A and for each j ∈ [n], let b_{j} ∈ B with

(a_{1}, Y_{1}) … (a_{j}, {x} ∪ Y_{j}) … (a_{n}, Y_{n}) ⊧ φ_{b_{j}}.

Then for each i ∈ [n],

(a_{1}, Y_{1}) … (a_{i}, {x} ∪ Y_{i}) … (a_{n}, Y_{n}) ⊧ ψ′

iff

b_{1} … (b_{i}, {x}) … b_{n} ⊧ ψ.

Lemma 3.4 Let φ = Q_{K}x.⟨φ_{b}⟩_{b∈B} be a formula over A with free variables in Y, and let ψ = Q_{L}x.⟨ψ_{c}⟩_{c∈C} be a sentence over B with L_{ψ} = K. For each c ∈ C, let ψ′_{c} denote the formula that results from ψ_{c} by replacing each subformula of the form P_{b}(ξ), where ξ is a free or bound variable, by the formula φ_{b}[ξ/x]. Then the formula φ′ = Q_{L}x.⟨ψ′_{c}⟩_{c∈C} of quantification depth less than or equal to qd(ψ) + qd(φ) − 1 is equivalent to φ, i.e., for all Y -structures (a_{1}, Y_{1}) … (a_{n}, Y_{n}) over A,

(a_{1}, Y_{1}) … (a_{n}, Y_{n}) ⊧ φ ⇔ (a_{1}, Y_{1}) … (a_{n}, Y_{n}) ⊧ φ′.  (5)

Proof. First note that by Lemma 3.2, φ′ and each ψ′_{c} is well-defined, moreover, ψ′_{c}, c ∈ C is a deterministic family. Let (a_{1}, Y_{1}) … (a_{n}, Y_{n}) denote an Y -structure over A. For each i ∈ [n], let b_{i} be the unique letter in B with

(a_{1}, Y_{1}) … (a_{i}, {x} ∪ Y_{i}) … (a_{n}, Y_{n}) ⊧ φ_{b_{i}}.

Moreover, let c_{i} ∈ C with

b_{1} … (b_{i}, {x}) … b_{n} ⊧ ψ_{c_{i}}.

We have

(a_{1}, Y_{1}) … (a_{n}, Y_{n}) ⊧ φ ⇔ b_{1} … b_{n} ∈ K
⇔ b_{1} … b_{n} ⊧ ψ
⇔ c_{1} … c_{n} ∈ L.

But by Corollary 3.3,

b_{1} … (b_{i}, {x}) … b_{n} ⊧ ψ_{c} ⇔ (a_{1}, Y_{1}) … (a_{i}, {x} ∪ Y_{i}) … (a_{n}, Y_{n}) ⊧ ψ′_{c},

for each i ∈ [n] and c ∈ C. Thus

(a_{1}, Y_{1}) … (a_{n}, Y_{n}) ⊧ φ′ ⇔ c_{1} … c_{n} ∈ L,

proving (5). □

Theorem 3.5 For any class L of languages, Lin(Lin(L)) ⊆ Lin(L). Moreover, Lin_{n}(Lin_{1}(L)) ⊆ Lin_{n}(L), for all n ≥ 0.

Proof. Given a formula φ in Lin(Lin(L)) over some alphabet A, we show by induction on the structure of φ how to construct an equivalent formula τ(φ) in Lin(L). If φ is in Lin(Lin_{1}(L)), we will also have qd(τ(φ)) ≤ qd(φ). When φ is an atomic formula or false, we define τ(φ) to be the same formula. When φ is φ_{1} ∨ φ_{2} or ¬φ_{1}, we define τ(φ) to be τ(φ_{1}) ∨ τ(φ_{2}) or ¬(τ(φ_{1})), respectively. Assume finally that φ is Q_{K}x.⟨φ_{b}⟩_{b∈B}, where each φ_{b} is a formula over A in Lin(Lin(L)) with free variables in {x} ∪ Y and K is a language in Lin(L) over the alphabet B. Now K is a boolean combination of languages K_{1}, …, K_{m} definable by Lin(L) sentences of the form Q_{L_{i}}x.⟨ψ_{c}^{i}⟩_{c∈C_{i}}, i ∈ [m]. Thus, φ is equivalent to a boolean combination of the formulas Q_{K_{i}}x.⟨φ_{b}⟩_{b∈B}, i ∈ [m], and by the induction hypothesis and Lemma 3.4, each Q_{K_{i}}x.⟨φ_{b}⟩_{b∈B} is equivalent to some formula ψ_{i} of Lin(L) obtained from Q_{L_{i}}x.⟨ψ_{c}^{i}⟩_{c∈C_{i}} by replacing each occurrence of P_{b}(ξ), where ξ is any variable, by φ_{b}[ξ/x]. Thus, when the quantification depth of Q_{L_{i}}x.⟨ψ_{c}^{i}⟩_{c∈C_{i}} is 1, so that the ψ_{c}^{i} contain no quantifiers, then qd(ψ_{i}) is at most the quantification depth of Q_{K_{i}}x.⟨φ_{b}⟩_{b∈B}. It follows that φ is equivalent to a boolean combination τ(φ) of the formulas ψ_{i}, i ∈ [m]. Moreover, when K ∈ Lin_{1}(L), then qd(φ) ≤ qd(τ(φ)). □

Corollary 3.6 Each of the assignments L ↦ Lin(L) and L ↦ Lin_{1}(L) defines a closure operator on language classes.

Corollary 3.7 The assignment L ↦ FO(L) defines a closure operator.

Corollary 3.8 For any language classes L, L′, we have Lin(L) ⊆ Lin(L′) iff for each formula of Lin(L) there is an equivalent formula of Lin(L′).

Proof. The sufficiency part of the claim is obvious. Suppose now that Lin(L) ⊆ Lin(L′). Then any formula φ of Lin(L) that possibly contains free variables is also a formula of Lin(Lin(L′)). Thus, since by the above proof of Theorem 3.5 every formula of Lin(Lin(L′)) is equivalent to a formula of Lin(L′), there is a Lin(L′) formula equivalent to φ. □

By the same argument, we have:

Corollary 3.9 For any language classes L, L′, we have Lin_{1}(L) ⊆ Lin_{1}(L′) iff for each formula φ of Lin(L) there is an equivalent formula φ′ of Lin(L′) with qd(φ′) ≤ qd(φ).

Corollary 3.10 For any class L of languages, Lin(L) = FO(L) iff K_{∃} ∈ Lin(L).

Of course, K_{∃} ∈ Lin(L) iff K_{∀} ∈ Lin(L).

Remark 3.11 When L is a regular language, one can use any finite automaton accepting L to express the Lindström quantifier Q_{L} in monadic second-order logic [31] and then use the theorem of Büchi [6], Elgot [12] and Trakhtenbrot [40] to establish that if each φ_{b_{i}} defines a regular language (of (V ∪ {x})-structures), then the formula (1) defines a regular language (of V -structures). Thus, for any class L of regular languages, Lin(L) contains only regular languages. This fact may also be seen as an instance of a general property of Lindström quantifiers, cf. Exercise 12.1.1 in [10]. Moreover, this fact also follows from Theorem 9.5 below. See also Barrington, Immerman, Straubing [3], Lautemann, McKenzie, Schwentick [18], and Theorem 9.5.

Remark 3.12 All of the results of this section remain valid if instead of the predicate < the language contains the successor predicate y = x + 1, or any other numerical predicate like the predicates x ≡ r mod m, where m ≥ 2 and r ∈ [m]. In fact, Corollary 3.6 formulates a very general property of Lindström quantification that we have not been able to locate in the literature.

4 Literal varieties

We say that a class L of languages is closed with respect to the boolean operations if for each alphabet Σ, L(Σ^{∗}) contains ∅ and Σ^{∗} and forms a boolean algebra. Moreover, we say that L is closed with respect to inverse literal (homo)morphisms if for all alphabets Σ, Δ and letter preserving homomorphisms h : Σ^{∗} → Δ^{∗} (i.e., such that h(Σ) ⊆ Δ), and for all languages L ∈ L(Δ^{∗}),

h^{−1}(L) = {u ∈ Σ^{∗} : h(u) ∈ L}

is in L(Σ^{∗}).

Suppose that L is a class of languages. We call L a literal prevariety if it is closed with respect to the boolean operations and inverse literal homomorphisms. A literal variety is also closed with respect to left and right quotients. Thus, if L, L_{1}, L_{2} ⊆ Σ^{∗} are in a literal variety L and v ∈ Σ^{∗}, then L_{1} ∪ L_{2}, Σ^{∗} − L and the left and right quotients v^{−1}L, Lv^{−1} are also in L, where

v^{−1}L = {u ∈ Σ^{∗} : vu ∈ L}
Lv^{−1} = {u ∈ Σ^{∗} : uv ∈ L}.

Moreover, if h is a literal morphism Σ^{∗} → Δ^{∗} and L ⊆ Δ^{∗} is in L, then h^{−1}(L) is also in L. Note that every literal variety contains, for each finite alphabet Σ, the language Σ^{∗} and the empty language. A literal (pre)variety of regular languages is a literal (pre)variety L such that every language in L is regular. Each class L of (regular) languages is contained in a least literal prevariety L′ and in a least literal variety L′′ of (regular) languages, respectively called the literal prevariety and the literal variety generated by L. Clearly, L′ ⊆ L′′. It is not difficult to see that a language belongs to L′ iff it is an inverse image under a literal morphism of a boolean combination of languages in L. Moreover, a language belongs to L′′ iff it is an inverse image under a literal morphism of a boolean combination of quotients of languages in L. Thus, L′ = L′′ iff each quotient of a language in L belongs to L′.

Literal varieties of regular languages are a generalization of the ∗-varieties of Eilenberg [11] and Pin [24] that are closed with respect to arbitrary inverse homomorphisms. Recently, Straubing [32] has defined the notion of Cvarieties, where C is a category of morphisms between free monoids. Literal varieties of regular languages may be seen as that special case corresponding to the category C of literal morphisms.

Proposition 4.1 For any language class L and integer n ≥ 0, Lin_{n}(L) is a literal prevariety. Thus, Lin(L) is also a literal prevariety.

Proof. It is obvious that for each n, Lin_{n}(L) is closed with respect to the boolean operations. To prove that Lin_{n}(L) is closed with respect to inverse literal homomorphisms, suppose that L ⊆ Δ^{∗} is in Lin_{n}(L) and h is a literal homomorphism Σ^{∗} → Δ^{∗}. We want to show h^{−1}(L) ∈ Lin_{n}(L). For any finite set V of variables, extend h to a literal homomorphism (Σ×P (V))^{∗} → (Δ × P (V))^{∗} by defining

h((u_{1}, V_{1}) … (u_{m}, V_{m})) = (h(u_{1}), V_{1}) … (h(u_{m}), V_{m}),

for all (u_{1}, V_{1}) … (u_{m}, V_{m}) ∈ (Σ × P (V))^{∗}. Then, for each formula φ in Lin(L) over Δ with free variables in V, let τ(φ) denote the formula obtained from φ by replacing each atomic subformula P_{b}(x), where x is a variable and b ∈ Δ, by the disjunction of all formulas P_{a}(x) with h(a) = b. When b is not in the range of h, we replace P_{b}(x) by the formula false. Note that qd(τ(φ)) = qd(φ) and τ(φ) ∈ Lin(L). It follows by a straightforward induction argument that for all V -structures u over Σ,

u ⊧ τ(φ) ⇔ h(u) ⊧ φ.

In particular, when φ is a sentence in Lin_{n}(L) defining L, we obtain L_{τ(φ)} = h^{−1}(L) and τ(φ) ∈ Lin_{n}(L), proving our claim. □

By Corollary 3.6, Lin_{1} is a closure operator on language classes. The following result gives a precise description of this closure operator.

Proposition 4.2 For each language class L, Lin_{1}(L) is the literal prevariety generated by L.

Proof. Let L′ denote the literal prevariety generated by L. We already know from Proposition 3.1 and Proposition 4.1 that Lin_{1}(L) is a literal prevariety containing L, so that L′ ⊆ Lin_{1}(L). Suppose now that L ⊆ Σ^{∗} is defined by a sentence φ_{K} = Q_{K}x.⟨φ_{b}⟩_{b∈Δ} in Lin(L) of quantification depth 1, so that each φ_{b} is quantifier-free and contains at most the variable x. It is easy to see that each φ_{b} is equivalent to a formula ψ_{b} which is a (possibly empty) disjunction of atomic formulas P_{a}(x), a ∈ Σ. Moreover, since the family φ_{b}, b ∈ Δ is deterministic, for each letter a ∈ Σ there is a unique b ∈ Δ such that P_{a}(x) appears as a subformula of ψ_{b}. Now let h : Σ^{∗} → Δ^{∗} denote the homomorphism that maps each letter a ∈ Σ to the corresponding b. Then L = h^{−1}(K), so that L ∈ L′. Since each sentence in Lin(L) is equivalent to a boolean combination of sentences φ_{K} and since literal prevarieties are closed with respect to the boolean operations, it follows now that Lin_{1}(L) ⊆ L′.

□

¿From Theorem 3.5 and Proposition 4.2 we immediately have:

Corollary 4.3 For each language class L and integer n ≥ 0, Lin_{n}(L′) = Lin_{n}(L), where L′ is the literal prevariety generated by L. Thus, Lin(L′) = Lin(L).

We say that quotients are expressible in Lin(L) if for each L ∈ L(Δ^{∗}) and v ∈ Δ^{∗}, and for any formulas φ = Q_{v^{−1}L}x.⟨φ_{b}⟩_{b∈Δ^{∗}} and φ′ = Q_{Lv^{−1}}x.⟨φ_{b}⟩_{b∈Δ^{∗}}, where φ_{b}, b ∈ Δ are Lin(L) formulas over some alphabet Σ with free variables in {x} ∪ Y, there exist equivalent formulas in Lin(L), i.e., Lin(L) formulas ψ and ψ′ over Σ in the free variables Y such that for all Y -structures u over Σ,

u ⊧ φ ⇔ u ⊧ ψ and u ⊧ φ′ ⇔ u ⊧ ψ′.

If in addition qd(ψ) ≤ qd(φ) and qd(ψ′) ≤ qd(φ′), for all φ and φ′, then we say that quotients are strictly expressible in Lin(L). We say that quotients are (strictly) expressible in FO(L) if quotients are strictly expressible in Lin(L ∪ {K_{∃}}).

Example 4.4

• Let L contain only the language K_{∃} ⊆ {b_{1}, b_{2}}^{∗}. The only quotients of K_{∃} are K_{∃} and {b_{1}, b_{2}}^{∗}. Since for any φ and x, Q_{{b_{1},b_{2}}^{∗}}x.⟨φ⟩ is equivalent to true, it follows that quotients are strictly expressible in Lin(L), i.e., in FO. Moreover, for any language class L, if quotients are (strictly) expressible in Lin(L), then the same holds for FO(L).

• Suppose that m ≥ 1 and consider the language C_{m}^{0} defined above. Its only quotients are the languages C_{m}^{r}, where 0 ≤ r < m. It is easy to see that quotients are expressible in FO({C_{m}^{0}}). Also, quotients are strictly expressible in Lin({C_{2}^{0}}), since Q_{C_{2}^{1}}x.⟨φ⟩ is expressible as ¬(Q_{C_{2}^{0}}x.⟨φ⟩).

• For any set M of positive integers, quotients are strictly expressible in Lin(C_{M}) and in FO(C_{M}), where C_{M} = {C_{m}^{r} : m ∈ M, 0 ≤ r < m} as above.

• For every m ≥ 1 and r ∈ [m], the quotients of K_{m}^{r} = (b_{2}^{m})^{∗}b_{2}^{r−1}b_{1}(b_{1} + b_{2})^{∗} are the languages ∅, (b_{1} + b_{2})^{∗}, K_{m}^{1}, …, K_{m}^{r} and K_{m}^{r} ∪ (b_{2}^{m})^{∗}, …, K_{m}^{r} ∪ (b_{2}^{m})^{∗}b_{2}^{m−1}. Using this fact, it is easy to see that quotients are expressible in FO({K_{m}^{r}}). It follows that quotients are expressible in FO(K_{M}), where for a set M of positive integers, K_{M} = {K_{m}^{r} : m ∈ M, r ∈ [m]}.

Proposition 4.5 Suppose that quotients are expressible in Lin(L). Then Lin(L) is a literal variety. Moreover, if quotients are strictly expressible in Lin(L), then Lin_{n}(L) is a literal variety, for each n ≥ 0.

Proof. Suppose that φ is a formula of Lin(L) over the finite alphabet Σ possibly containing free variables from the finite set V. Let L_{φ} denote the set of all V -structures over Σ defined by φ. We argue by induction on the structure of φ to prove that for each letter a ∈ Σ, the set of V -structures a^{−1}L_{φ} is definable by some formula ψ of Lin(L) with free variables in V. Moreover, for each letter a ∈ Σ and variable x ∈ V, the set of (V − {x})- structures (a, {x})^{−1}L_{φ} is definable by some formula ψ with free variables in V − {x}. When quotients are strictly expressible in Lin(L), then for each φ, the quantification depth of the formula ψ defining a^{−1}L_{φ} or (a, {x})^{−1}L_{φ} will be at most that of φ. The extension of the argument to left quotients v^{−1}L_{φ}, where v is any word in Σ^{∗}, ore more generally, v is any V_{1}-structure over Σ, for some V_{1} ⊆ V, is left to the reader. Right quotients can be dealt with symmetrically.

The basis case is obvious, including the case when φ is false, as are the cases when φ is of the form φ_{1} ∨ φ_{2} or ¬ψ. One uses the fact that the operation of taking left quotients commutes with the boolean operations. Moreover, a^{−1}L_{φ} = L_{φ}, for all atomic formulas φ. Also, if φ is atomic, then (a, {x})^{−1}L_{φ} is definable by a quantifier-free formula. Suppose finally that φ is of the form Q_{K}x.⟨ψ_{b_{j}}⟩_{b_{j}∈Δ}, where K ⊆ Δ^{∗} = {b_{1}, …, b_{m}}^{∗} is a language in L and each ψ_{b_{j}} is a formula of Lin(L) over Σ with free variables in V ∪{x}, where x ∉ V. For each b_{j}, let L_{b_{j}} denote the set of all (V ∪ {x})-structures defined by ψ_{b_{j}}. It follows by the induction hypothesis that for each b_{j} there is a formula ρ_{b_{j}} of Lin(L) that defines the set (a, {x})^{−1}L_{b_{j}}, i.e., the set of all V -structures u such that (a, {x})u ⊧ ψ_{b_{j}}. Moreover, for each b_{k} there exists a formula ψ′_{b_{k}} of Lin(L) over Σ with free variables in V ∪ {x} defining the set a^{−1}L_{b_{k}}, i.e., the set of all (V ∪ {x})-structures u such that au ⊧ ψ_{b_{k}}. For each b_{j}, let

α_{b_{j}} = ρ_{b_{j}} ∧ Q_{b_{j}^{−1}K}x.⟨ψ′_{b_{k}}⟩_{b_{k}∈Δ}.

Given a V -structure u, we have u ⊧ α_{b_{j}} iff (a, \{x\})u ⊧ ψ_{b_{j}} and \overline{u} ∈ b_{j}^{−1}K, where \overline{u} is the characteristic word determined by u and the formula Q_{b_{j}^{−1}K}x.⟨ψ′_{b_{k}}⟩_{b_{k}∈Δ}. It follows that u ⊧ α_{b_{j}} iff the characteristic word determined by au and the formula φ starts with b_{j} and belongs to K. Thus, letting

α = ⋁_{b_{j}∈Δ} α_{b_{j}},

it holds that u ⊧ α iff au ⊧ φ iff u ∈ a^{−1}L_{φ}, showing that a^{−1}L_{φ} is definable by α. Since by assumption there is a Lin(L) formula equivalent to α, it follows that a^{−1}L_{φ} is in Lin(L). If quotients are strictly expressible in Lin(L), then by the induction hypothesis, qd(ρ_{j}), qd(ψ′_{j}) ≤ qd(ψ_{j}), for all j ∈ [m]. Thus, qd(α) ≤ qd(φ), and since quotients are strictly expressible in Lin(L), it follows that there exists a Lin(L) formula of quantification depth at most qd(φ) which is equivalent to α.

The fact that (a, {x})^{−1}L_{φ} is in Lin(L), for each variable x ∈ V and letter a ∈ Σ, can be established by a similar argument. Again, it follows that if quotients are strictly expressible in Lin(L), then (a, {x})^{−1}L_{φ} is definable by a formula of Lin(L) whose quantification depth is at most that of φ. □

Corollary 4.6 The following conditions are equivalent for a class L of languages:

1. Each quotient of any language in L belongs to Lin(L).

2. Lin(L) is closed with respect to quotients.

3. Lin(L) is a literal variety.

4. Quotients are expressible in Lin(L).

Proof. Let L_{0} denote the class of all quotients of languages in L. If the first condition holds, then since Lin is a closure operator and L ⊆ L_{0} ⊆ Lin(L), we have Lin(L_{0}) = Lin(L). Thus, by Corollary 3.8, for every Lin(L_{0}) formula there is an equivalent Lin(L) formula. In particular, quotients are expressible in Lin(L). This proves that the first condition implies the last. That the last implies the third is the content of Proposition 4.5. Finally, it is clear that the third condition implies the second which in turn implies the first. □

Corollary 4.7 The following conditions are equivalent for a language class L.

1. Each quotient of any language in L belongs to the literal prevariety generated by L.

2. The literal prevariety generated by L is closed with respect to quotients and is thus a literal variety.

3. Each quotient of any language in L is in Lin_{1}(L).

4. Lin_{1}(L) is closed with respect to quotients.

5. Lin_{1}(L) is a literal variety.

6. Lin_{n}(L) is closed with respect to quotients, for all n ≥ 0.

7. Lin_{n}(L) is a literal variety, for all n ≥ 0.

8. Quotients are strictly expressible in Lin(L).

Proof. By Propositions 4.1, 4.2, 4.5 and Corollary 3.9. □

Corollary 4.8 If Lin(L) = Lin(L′) and quotients are expressible in Lin(L), then the same holds for Lin(L′). Similarly, if Lin_{1}(L) = Lin_{1}(L′) and quotients are strictly expressible in Lin(L), then the same holds for Lin(L′).

Proof. Since quotients are expressible in Lin(L), by Corollary 4.6 we have that Lin(L′) = Lin(L) is closed with respect to quotients. Thus, by Corollary 4.6 again, quotients are expressible in Lin(L′). The proof of the second claim uses Corollary 4.7. □

Corollary 4.9 Assume that quotients are expressible in Lin(L). Then Lin(L) = Lin(L′) holds for the least literal variety L′ containing L. And if quotients are strictly expressible in Lin(L), then Lin_{n}(L) = Lin_{n}(L′) holds for all n ≥ 0, where L′ is the literal variety generated by L.

Proof. ¿From Theorem 3.5 and Corollaries 4.3, 4.6 and 4.7. □

Remark 4.10 Suppose that Lin(L) = Lin(L′), where L′ is the literal variety generated by L, or any other literal variety. Then, by Proposition 4.5, Lin(L) is a literal variety. Thus, by Corollary 4.6, quotients are expressible in Lin(L). Also, if Lin_{n}(L) = Lin_{n}(L′) for all n ≥ 0, or if Lin_{1}(L) = Lin_{1}(L′), for the literal variety L′ generated by L, or for any other literal variety, then quotients are strictly expressible in Lin(L).

Remark 4.11 We can show that for any class L of languages, Lin(L) is closed with respect to arbitrary inverse homomorphisms iff every inverse homomorphic image of a language in L belongs to Lin(L).

Remark 4.12 All of the results of this section remain valid if the < predicate is replaced by the successor predicate. In fact, Proposition 4.2 remains valid whenever every atomic formula involving a numerical predicate and a single variable is equivalent to true or false, while in the proof of Proposition 4.5 we only used that when φ is atomic, then for any letter a and variable x, a^{−1}L_{φ} and (a, {x})^{−1}L_{φ} are definable by some quantifier-free formulas.

5 Monoids with a distinguished set of generators

A monoid equipped with a set of distinguished generators, or mg-pair, for short, consists of a monoid M and a nonempty set A of generators of M. When M is finite, we call (M, A) a finite mg-pair. A morphism (M, A) → (N, B) of mg-pairs is a monoid homomorphism h : M → N such that h(A) ⊆ B. It is clear that mg-pairs and their morphisms form a category with respect to function composition. When \underline{1} = \{1\} denotes a trivial monoid, (\underline{1}, \{1\}) is a zero object of this category. We call these mg-pairs trivial. We call a morphism h : (M, A) → (N, B) surjective if h(A) = B, so that also h(M) = N, and injective if it is an injective function. Moreover, we call (N, B) a quotient of (M, A) if there is surjective morphism (M, A) → (N, B), and a sub mg-pair of (M, A) if N ⊆ M and the inclusion N → M is a morphism (thus, B = A ∩ N and N is the submonoid of M generated by B). Finally, we say that (M, A) covers (N, B), or that (N, B) divides (M, A), if (N, B) is a quotient of a sub mg-pair of (M, A). We let < denote this relation. It is clear that when (N, B) < (M, A), the monoid N is a quotient of a submonoid of M, i.e., N < M as defined in [11]. Also, < is reflexive and transitive both on mg-pairs and on monoids.

Remark 5.1 Let (M, A) and (N, B) be mg-pairs. Suppose that there are a subsemigroup S of M and a subset C of A that generates S such that there is a semigroup homomorphism S → N that maps C onto B. Then we have (N, B) < (M, A). (Note that S may not contain the identity element of M.)

Remark 5.2 Suppose that M and N are monoids. We recall from Eilenberg [11] that a covering N → M is a relation φ : N → M, viewed as a function N → P (M), such that • φ(n) ≠ ∅, for all n ∈ N,

• for all n_{1}, n_{2} ∈ N, if n_{1} ≠ n_{2} then φ(n_{1}) ∩ φ(n_{2}) = ∅,

• 1 ∈ φ(1), and

• φ(n_{1})φ(n_{2}) ⊆ φ(n_{1}n_{2}), for all n_{1}, n_{2} ∈ N.

It is known that N < M iff there is a covering N → M. Suppose now that M and N are equipped with the nonempty sets of distinguished generators A and B, respectively. We define a covering (N, B) → (M, A) as a covering φ : N → M such that for each b ∈ B there exists some a ∈ A with a ∈ φ(b). (The first condition above in the definition of covering then becomes redundant.) We will return to coverings in the Appendix.

Example 5.3

• For every monoid M, the pair (M, M) is an mg-pair. Moreover, for monoids M, N, we have that N < M iff (N, N) < (M, M).

• When Σ is an alphabet, (Σ^{∗}, Σ) is an mg-pair. Given any mg-pair (M, A) and function h : Σ → A, there is a unique morphism (Σ^{∗}, Σ) → (M, A) extending h. (We denote this morphism by h as well.) Thus, (Σ^{∗}, Σ) is a free mg-pair.

• Each automaton (Q, Σ, ·) with transition function · : Q×Σ → Q gives rise to an mgpair (M_{Q}, \overline{Σ}). Its monoid component M_{Q} is the monoid of all state transformations Q → Q induced by the words in Σ^{∗}, and the set of generators \overline{Σ} consists of those transformations induced by the letters in Σ.

• Each mg-pair (M, A) may be regarded as an automaton (M, A, ·) whose action is given by right multiplication (m, a) ↦ ma, m ∈ M, a ∈ A. This automaton is freely generated by the identity element of M and is “input reduced”: different input letters induce different state transformations. In fact, the category of mgpairs is equivalent to the category of one-generated input reduced free automata whose morphisms preserve the free generator and the transitions (with a possible change in the alphabet).

• When (M, A) is an mg-pair, B is a nonempty subset of A, and if Q ⊆ M is closed with respect to right multiplication with the elements of B, then Q and B determine an mg-pair (N, \overline{B}). Here, N is the quotient of the submonoid M′ of M generated by the elements in B with respect to the congruence ∼_{Q} defined by x ∼_{Q} y iff qx = qy for all q ∈ Q. Moreover, \overline{B} consists of the congruence classes of the elements of B.

Below we will identify a monoid M with the mg-pair (M, M). Moreover, we call an mg-pair (M, A) an mg-pair with identity, or mgi-pair, if A contains the identity element of M. A gg-pair is an mg-pair whose monoid component is a group.

Each mg-pair may be used as a recognizer. Let (M, A) denote a not necessarily finite mg-pair and let h : (Σ^{∗}, Σ) → (M, A) be a morphism, so that h is a monoid homomorphism Σ^{∗} → M with h(Σ) ⊆ A. Given a set F ⊆ M, the language recognized, or accepted by (M, A) with h and F is the set

h^{−1}(F) = {u ∈ Σ^{∗} : h(u) ∈ F }.

It is clear that a language is regular iff it can be recognized by a finite mg-pair.

Any language can be recognized by an mg-pair. Given a language L ⊆ Σ^{∗}, let M_{L} denote the syntactic monoid of L, and let η_{L} : Σ^{∗} → M_{L} denote the syntactic homomorphism of L, cf. Eilenberg [11], Pin [24]. Then Synt(L) = (M_{L}, η_{L}(Σ)) is an mg-pair, called the syntactic mg-pair of L. Moreover, η_{L} is a morphism (Σ^{∗}, Σ) → Synt(L), called the syntactic morphism of L.

The following fact is an adaptation of well-known results from Eilenberg [11] and Pin [24].

Proposition 5.4

1. The language recognized by Synt(L) = (M_{L}, η_{L}(Σ)) with the syntactic morphism η_{L} and the set η_{L}(L) is L.

2. Suppose that (M, A) accepts L with h : (Σ^{∗}, Σ) → (M, A) and F ⊆ M. Suppose that h is surjective. Then there is a (unique) morphism h′ : (M, A) → Synt(L) such that

η_{L} = (Σ^{∗}, Σ) ⟶^{h} (M, A) ⟶^{h′} Synt(L).

3. A language L ⊆ Σ^{∗} can be recognized by an mg-pair (M, A) iff we have Synt(L) < (M, A).

The following fact is well-known.

Lemma 5.5 Let L ⊆ A^{∗} be a regular language. Then every language in A^{∗} recognizable by the syntactic morphism η_{L} is a boolean combination of quotients of L.

Lemma 5.6 Let L ⊆ A^{∗} be a regular language and let B denote an alphabet. Then every language in B^{∗} recognizable by the syntactic mg-pair of L is the inverse image under a literal morphism B^{∗} → A^{∗} of a language in A^{∗} which is a boolean combination of quotients of L.

Proof. Let h : (B^{∗}, B) → (M_{L}, η_{L}(A)) be a morphism and let K ⊆ B^{∗} with h^{−1}(h(K)) = K. Since η_{L} is surjective and (B^{∗}, B) is free, there exists a literal morphism φ : B^{∗} → A^{∗} such that

h = (B^{∗}, B) ⟶^{φ} (A^{∗}, A) ⟶^{η_{L}} (M_{L}, η_{L}(A)).

Thus, K = φ^{−1}(K′), where K′ = η_{L}^{−1}(h(K)). By Lemma 5.5, K′ is a boolean combination of quotients of L. □

Suppose that K is a class of mg-pairs. We define Lin(K) = Lin(L_{K}) and Lin(K) = Lin(L_{K}), where L_{K} is the class of all languages recognizable by the members of K. Moreover, we define FO(K) = FO(L_{K}), FO(K) = FO(L_{K}), and Lin_{n}(K) = Lin_{n}(L_{K}), FO_{n}(K) = FO_{n}(L_{K}), Lin_{n}(K) = Lin_{n}(L_{K}), FO_{n}(K) = FO_{n}(L_{K}), for each n ≥ 0. Note that L_{K} is closed with respect to quotients and inverse literal homomorphisms. Thus, by Corollary 4.7, quotients are strictly expressible in both Lin(K) and FO(K), for any K.

Remark 5.7 For a class K of mg-pairs, let L′(K) denote those languages that can be recognized by an mg-pair (M, A) ∈ K with the homomorphism (A^{∗}, A) → (M, A) which is the identity function on A. Then L′_{K} ⊆ L_{K} and, moreover, every language in L_{K} is the inverse image of a language in L′_{K} under a literal homomorphism. It follows that Lin(K) = Lin(L′_{K}) and FO(K) = FO(L′_{K}). Moreover, for each n ≥ 0, Lin_{n}(K) = Lin_{n}(L′_{K}) and FO_{n}(K) = FO_{n}(L′_{K}). (For the definition of Lin_{n}(K) and FO_{n}(K), see below.)

Corollary 5.8 For each class K of mg-pairs and for each n ≥ 0, Lin_{n}(K) is a literal variety. Moreover, Lin(K) is a literal variety. If K is a class of finite mg-pairs, then Lin(K) is a literal variety of regular languages.

Proof. ¿From Corollaries 4.6 and 4.7. When K consists of finite mg-pairs, then L_{K} is a class of regular languages. Thus, by Remark 3.11, every language in Lin(L_{K}) is regular. □

For a class L of languages, let K_{L} consist of the mg-pairs Synt(L), where L ∈ L.

Proposition 5.9

1. For any class L of languages, Lin(L) ⊆ Lin(K_{L}).

2. Suppose that L is a class of regular languages. Then:

• Lin(K_{L}) = Lin(L′), where L′ is the literal variety generated by L.

• Lin(L) = Lin(K_{L}) iff quotients are expressible in Lin(L).

Proof. Since every language is recognizable by its syntactic mg-pair, the inclusion Lin(L) ⊆ Lin(K_{L}) is obvious. Assume now that L consists of regular languages. By Lemma 5.6, every language recognizable by some mg-pair in K_{L} is the inverse image with respect to a literal morphism of a boolean combination of quotients of a language in L and thus belongs to the least literal variety containing L. Thus, Lin(K_{L}) ⊆ Lin(L′). But since Lin(K_{L}) is a literal variety containing L′, also L′ ⊆ Lin(K_{L}) and thus Lin(L′) ⊆ Lin(Lin(K_{L})) = Lin(K_{L}) by Corollary 3.6. This proves Lin(K_{L}) = Lin(L′). The last claim now follows from Corollary 4.9 and Remark 4.10. □

Remark 5.10 If Lin(L) = Lin(K) for any class K of mg-pairs, then quotients are expressible in Lin(L). See Remark 4.10.

Let U_{1} denote a two-element semilattice. Note that U_{1} is isomorphic to the syntactic monoid of the language K_{∃}, defined in Example 2.2.

Proposition 5.11 For each class K of mg-pairs, FO(K) = Lin(K∪{U_{1}}).

Proof. By definition, FO(K) = FO(L_{K}) = Lin(L_{K} ∪ {K_{∃}}) and Lin(K ∪ {U_{1}}) = Lin(L_{K} ∪ L_{{U_{1}}}). Thus, since K_{∃} is in L_{{U_{1}}}, we have FO(K) ⊆ Lin(K ∪ {U_{1}}). But every language L ⊆ Δ^{∗} recognizable by U_{1} is either the empty language, or the language Δ^{∗}, or the inverse image of K_{∃} or K_{∀} with respect to a literal morphism Δ^{∗} → {b_{1}, b_{2}}^{∗}. Using this fact and Corollary 4.3, we have Lin(K ∪ {U_{1}}) ⊆ FO(K), as claimed. □

Below we will use the above fact without mention.

Example 5.12

• Recall that for any integers m ≥ 1 and 0 ≤ r < m, C_{m}^{r} denotes the language of all words over the two-letter alphabet {b_{1}, b_{2}} such that the number of occurrences of b_{1} is congruent to r modulo m. The syntactic mg-pair of each C_{m}^{r} is isomorphic to an mg-pair (Z_{m}, {a, 1}), where Z_{m} is a cyclic group of order m generated by the letter a and where 1 denotes the identity element of Z_{m}. Now when M is a set of positive integers and C_{M} = {C_{m}^{r} : m ∈ M, 0 ≤ r < m}, then C_{M} is closed with respect to quotients and thus Lin(C_{M}) = Lin({(Z_{m}, {a, 1}) : m ∈ M}). Moreover, since quotients are expressible in FO({C_{M}}) = Lin(C_{M} ∪ {K_{∃}}), FO({C_{M}}) = FO({(Z_{m}, {a, 1}) : m ∈ M}). In fact, FO({C_{m}^{0} : m ∈ M}) = FO({(Z_{m}, {a, 1}) : m ∈ M}).

• Consider now a language K_{m}^{r} = (b_{2}^{m})^{∗}b_{2}^{r−1}b_{1}(b_{1} + b_{2})^{∗}, where m ≥ 1 and r ∈ [m]. Its syntactic monoid has 2m elements and can be defined by the relations b_{2}^{m} = 1, b_{1}b_{1} = b_{1}b_{2} = b_{1}. Let M_{m} denote this monoid. Then Synt(K_{m}^{r}) = (M_{m}, {b_{1}, b_{2}}). Now for any set M of positive integers, quotients are expressible both in FO(K_{M}) and in FO({K_{m}^{1} : m ∈ M}). Thus, FO(K_{M}) = FO({K_{m}^{1} : m ∈ M}) = FO({(M_{m}, {b_{1}, b_{2}}) : m ∈ M}). Moreover, when M is not empty, then FO({(M_{m}, {b_{1}, b_{2}}) : m ∈ M}) = Lin({(M_{m}, {b_{1}, b_{2}}) : m ∈ M}, since U_{1} is a quotient of any (M_{m}, {b_{1}, b_{2}}).

We may refine the above results by taking into account the quantification depth of the formulas. Using Proposition 4.5 and Corollary 4.7, we have:

Proposition 5.13 For each class K of mg-pairs and any integer n ≥ 0, Lin_{n}(K) is a literal variety. Moreover, if K is a class of finite mg-pairs, then Lin_{n}(K) is a literal variety of regular languages.

Proposition 5.14

1. For any class L of languages and integer n ≥ 0, Lin_{n}(L) ⊆ Lin_{n}(K_{L}).

2. Suppose that L is a class of regular languages. Then the following conditions are equivalent.

(a) The quotient of each language in L belongs to the literal prevariety generated by L.

(b) The literal prevariety generated by L is a literal variety.

(c) Quotients are strictly expressible in Lin(L).

(d) Lin_{1}(L) is a literal variety.

(e) For all n ≥ 0, Lin_{n}(L) is a literal variety.

(f) Lin_{1}(L) = Lin_{1}(K_{L}).

(g) For all n ≥ 0, Lin_{n}(L) = Lin_{n}(K_{L}).

We also have:

Proposition 5.15 For each class K of mg-pairs and n ≥ 0, FO_{n}(K) = Lin_{n}(K ∪ {U_{1}}).

6 Relativization

We say that Lin(L) admits relativization if for each sentence φ in Lin(L), over any alphabet Σ, and for any variable x there exist Lin(L) formulas φ[> x] and φ[< x] over Σ in the free variable x such that for all {x}-structures u = u_{1} … (u_{i}, {x}) … u_{n} over Σ,

u ⊧ φ[> x] ⇔ u_{i+1} … u_{n} ⊧ φ

and

u ⊧ φ[< x] ⇔ u_{1} … u_{i−1} ⊧ φ.

We say that Lin(L) strictly admits relativization if for each φ, the formulas φ[> x] and φ[< x] can be chosen so that their quantification depth does not exceed the quantification depth of φ. We say that FO(L) (strictly) admits relativization if Lin(L ∪ {K_{∃}}) does. Finally, when K is a class of mgpairs, we say that Lin(K) (FO(K), respectively) admits, or strictly admits relativization, if Lin(L_{K}) (FO(L_{K}), respectively) does.

Example 6.1

• It is clear that Lin(∅) and FO strictly admit relativization.

• Assume that L contains the one-letter language (b_{1}^{2})^{∗}. If Lin(L) admits relativization then for each Σ there is a formula ψ in the free variable x satisfied by those {x}-structures over Σ such that x occurs at an even (or odd) position.

• Let L consist of the finite and cofinite languages. We show that Lin(L) does not admit relativization. Suppose it does. Then let first(x) denote the formula (Q_{{ϵ}}y.⟨⟩)[< x] over the one-letter alphabet {a}, where {ϵ} is considered as a one-letter language. Then an {x}-structure u over {a} satisfies first(x) iff u ≠ ϵ and its first letter is (a, {x}). But this leads to a contradiction, since for any formula φ of Lin(L) over {a} in the free variable x, the set L_{φ} of {x}-structures over {a} satisfying φ is either finite or cofinite in the sense that its complement with respect to the set of all {x}-structures is finite. Indeed, any such formula φ is a boolean combination of atomic formulas over {a} in the variable x and of formulas of the sort Q_{K}y.⟨φ_{b}⟩_{b∈Δ}, where K is finite or cofinite and each φ_{b} is a formula over {a} in Lin(L). Since the alphabet has only one letter, the set of {x}-structures satisfying an atomic formula in the variable x is either finite or cofinite. Moreover, the set of {x}-structures satisfying a formula of the sort Q_{K}y.⟨φ_{b}⟩_{b∈Δ} is finite or cofinite depending on whether K is finite or cofinite. Since any boolean combination of finite and cofinite sets is finite or cofinite, it follows that the set of {x}-structures satisfying φ is also finite or cofinite.

• Let L consist of the one-letter language (b_{1}^{2})^{∗}. Then Lin(L) does not admit relativization. Indeed, otherwise there was a formula τ over the one-letter alphabet Σ = {a} in the free variable x satisfied by those {x}-structures over Σ in which x appears at an odd position. But this results a contradiction, since it is easy to show that for any formula φ of Lin(L) over {a} in the free variable x, an {x}-structure over {a} satisfies φ iff all {x}-structures over {a} of the same length satisfy φ. In a similar way, if L is any nonempty collection of languages L_{m}^{r} = (b_{1}^{m})^{∗}b_{1}^{r}, where m ≥ 2 and 0 ≤ r < m, then Lin(L) does not admit relativization. In fact, if L is any set of languages over the one-letter alphabet {b_{1}} containing at least one language different from ∅ and b_{1}^{∗}, then Lin(L) does not admit relativization.

Proposition 6.2

1. Suppose that Lin(L) = Lin(L′). Then Lin(L) admits relativization iff Lin(L′) does.

2. Suppose that Lin_{1}(L) = Lin_{1}(L′). Then Lin(L) strictly admits relativization iff Lin(L′) does.

Proof. The first claim is clear from the fact, shown in Corollary 3.8, that Lin(L) = Lin(L′) iff for each Lin(L) formula there exists an equivalent Lin(L′) formula and vice versa. The second claim follows from Corollary 3.9.

□

Corollary 6.3 Suppose that K_{∃} ∈ Lin(L). Then Lin(L) admits relativization iff FO(L) does.

Proof. Since K_{∃} ∈ Lin(L) and thus Lin(L) = Lin(L ∪ {K_{∃}}), by Proposition 6.2 it holds that Lin(L) admits relativization iff Lin(L ∪ {K_{∃}}) does. But by definition, Lin(L ∪ {K_{∃}} admits relativization iff FO(L) does. □

Corollary 6.4 Suppose that K is a class of finite mg-pairs and V denotes the variety generated by K. Then Lin(K) (strictly) admits relativization iff Lin(V) does.

Proof. This follows from Proposition 6.2, Proposition 8.6 and Proposition 8.8. □

Below, for an alphabet Δ, we let Δ_{0} denote the enlarged alphabet Δ ∪ {b_{0}}, where b_{0} is a new symbol.

Lemma 6.5 Suppose that for each Δ and K ⊆ Δ^{∗} in L there exist languages K_{<}, K_{>} ⊆ Δ_{0}^{∗} with b_{0}^{∗}Δ^{∗}∩K_{>} = b_{0}^{∗}K or b_{0}^{∗}Δ^{∗}∩K_{>} = b_{0}^{+}K, and Δ^{∗}b_{0}^{∗}∩K_{<} = Kb_{0}^{∗} or Δ^{∗}b_{0}^{∗} ∩ K_{<} = Kb_{0}^{+}, and such that the Lindström quantifiers with respect to K_{>} and K_{<} are expressible in Lin(L) (or equivalently, K_{>}, K_{<} are in Lin(L)). Then Lin(L) admits relativization. And if K_{>} and K_{<} are in the literal prevariety generated by L, for each K in L, then Lin(L) strictly admits relativization.

Proof. Given a formula φ in Lin(L) over Σ with free variables in Y, where x ∉ Y, we construct Lin(L) formulas φ[< x] and φ[> x] over Σ with free variables in {x}∪Y such that for all ({x}∪Y)-structures over Σ of the form v(a_{0}, {x})w and w(a_{0}, {x})v, where v is an Y -structure over Σ, w ∈ Σ^{∗} and a_{0} ∈ Σ, we have

v(a_{0}, {x})w ⊧ φ[< x] ⇔ v ⊧ φ
w(a_{0}, {x})v ⊧ φ[> x] ⇔ v ⊧ φ.

We argue by induction on the structure of φ. When φ is an atomic formula or the formula false, then let φ[< x] = φ[> x] = φ. When φ = φ_{1} ∨ φ_{2} or φ = ¬φ_{1}, for some φ_{1}, φ_{2}, define φ[< x] = φ_{1}[< x] ∨ φ_{2}[< x] or φ[< x] = ¬(φ_{1}[< x]), respectively, and define φ[> x] symmetrically. Lastly, suppose that φ = Q_{K}y.⟨φ_{b}⟩_{b∈Δ}, for some (deterministic) family of formulas φ_{b}, b ∈ Δ in Lin(L). We only show how to define φ[> x]. For each b ∈ Δ, let ψ′_{b} be the formula x < y ∧ φ_{b}[> x], and let ψ′_{b_{0}} = x ≥ y. Moreover, let ψ_{b}, b ∈ Δ_{0} be any determinization of the family ψ′_{b}, b ∈ Δ_{0}. Then, if K_{>} ∈ L, we define φ[> x] = Q_{K_{>}}y.⟨ψ_{b}⟩_{b∈Δ_{0}}. Given w(a_{0}, {x})v as above, the characteristic word determined by w(a_{0}, {x})v and φ[> x] can be written as b_{0}^{|w|+1}p, where p denotes the characteristic word determined by v and φ. Since b_{0}^{|w|+1}p ∈ K_{>} iff p ∈ K, it follows that w(a_{0}, {x})v ⊧ φ[> x] iff v ⊧ φ. When K_{>} is not in L, let φ[> x] be a Lin(L) formula equivalent to Q_{K_{>}}y.⟨ψ_{b}⟩_{b∈Δ_{0}}. If K belongs to the literal prevariety generated by L, i.e., to the language class Lin_{1}(L), then by Corollary 3.9, there is such a formula φ[> x] whose quantification depth is at most that of φ. □

Two languages K_{>} satisfying the assumption b_{0}^{∗}Δ^{∗} ∩K_{>} = b_{0}^{∗}K are b_{0}^{∗}K and the padding of K, i.e., the language h^{−1}(K), where h is the homomorphism Δ_{0}^{∗} → Δ which is the identity map on Δ and maps b_{0} to ϵ.

Example 6.6 Let K be a class of mgi-pairs. Then for any K ⊆ Δ^{∗} in L_{K}, the padding of K belongs to L_{K}.

Corollary 6.7 Suppose that for each Δ and K ⊆ Δ^{∗} in L, Kb_{0}^{∗} and b_{0}^{∗}K, or Kb_{0}^{+} and b_{0}^{+}K belong to Lin(L). Then Lin(L) admits relativization. Moreover, if for any language K in L, Kb_{0}^{∗} and b_{0}^{∗}K, or Kb_{0}^{+} and b_{0}^{+}K belong to the literal prevariety generated by L, then Lin(L) strictly admits relativization.

Corollary 6.8 Suppose that for each Δ and K ⊆ Δ^{∗} in L, the padding of K belongs to Lin(L). Then Lin(L) admits relativization. Moreover, if the padding of any language in L belongs to the literal prevariety generated by L, then Lin(L) strictly admits relativization.

Corollary 6.9 For any class K of mgi-pairs, Lin(K) strictly admits relativization.

Lemma 6.10 Suppose that for each Δ and K ⊆ Δ^{∗} in L there exist languages K_{<}, K_{>} with Δ^{∗}b_{0}Δ^{∗} ∩ K_{>} = Δ^{∗}b_{0}K and Δ^{∗}b_{0}Δ^{∗} ∩ K_{<} = Kb_{0}Δ^{∗} and such that the Lindström quantifiers with respect to K_{>} and K_{<} are expressible in Lin(L) (or equivalently, K_{>}, K_{<} are in Lin(L)). Then Lin(L) admits relativization. And if K_{>} and K_{<} are in the literal prevariety generated by L, for each K in L, then Lin(L) strictly admits relativization.

Proof. We argue as in the proof of Lemma 6.5 by constructing appropriate formulas φ[< x], φ[> x] for each φ ∈ Lin(L). In the induction step, when φ = Q_{K}y.⟨φ_{b}⟩_{b∈Δ}, we define φ[> x] as the formula Q_{K_{>}}y.⟨ψ_{b}⟩_{b∈Δ_{0}}, or as a formula equivalent to this formula, where ψ_{b}, b ∈ Δ_{0} is any determinization of the family ψ′_{b}, b ∈ Δ_{0} defined as follows. First, ψ′_{b_{0}} is the formula x = y, moreover, there is some b ∈ Δ with

ψ′_{b} = y < x ∨ (y > x ∧ φ_{b}[> x]),

and for all b′ ∈ Δ with b′ ≠ b,

ψ′_{b′} = y > x ∧ φ_{b}[> x].

We omit the details. □

Proposition 6.11 The following conditions are equivalent for a class L of languages:

1. FO(L) admits relativization.

2. For each Δ and K ∈ L(Δ^{∗}), the languages b_{0}^{∗}K and Kb_{0}^{∗} (or b_{0}^{+}K and Kb_{0}^{+}) belong to FO(L).

3. For each Δ and K ∈ L(Δ^{∗}) there exist languages K_{>} and K_{<} in FO(L) with b_{0}^{∗}Δ^{∗} ∩ K_{>} = b_{0}^{∗}K and Δ^{∗}b_{0}^{∗} ∩ K_{<} = Kb_{0}^{∗}.

Proof. We have already shown that the third condition implies the first. That the second implies the third is obvious. Thus, to complete the proof, we show that the first condition implies the second. So suppose that FO(L) admits relativization and K ∈ L(Δ^{∗}). Let K_{1} denote the language h_{1}^{−1}(K), where h_{1} is a literal morphism Δ_{0}^{∗} → Δ^{∗} which is the identity function on Δ. We know that Lindström quantification with respect to K_{1} is expressible in FO(L). Then b_{0}^{+}K is definable by

∃y [∀z(z ≤ y → P_{b_{0}}(z) ∧ z > y → ⋁_{b∈Δ} P_{b}(z)) ∧ (Q_{K_{1}}z.⟨P_{b}(z)⟩_{b∈Δ_{0}})[> y]] .

Moreover, b_{0}^{∗}K is definable by the disjunction of the above formula with

∀x( ⋁_{b∈Δ} P_{b}(x)) ∧ Q_{K_{1}}z.⟨P_{b}(z)⟩_{b∈Δ_{0}}.

The languages Kb_{0}^{∗} and Kb_{0}^{+} are definable in the same way. □

Proposition 6.12 The following conditions are equivalent for a class L of languages:

1. FO(L) admits relativization.

2. For each Δ and K ∈ L(Δ^{∗}), the languages Δ^{∗}b_{0}K and Kb_{0}Δ^{∗} belong to FO(L).

3. For each Δ and K ∈ L(Δ^{∗}) there exist languages K_{>} and K_{<} in FO(L) with Δ^{∗}b_{0}Δ^{∗} ∩ K_{>} = Δ^{∗}b_{0}K and Δ^{∗}b_{0}Δ^{∗} ∩ K_{<} = Kb_{0}Δ^{∗}.

Proof. We only need to show that the first condition implies the second. But given K, Δ^{∗}b_{0}K is defined by

∃y [∀z((z ≠ y → ⋁_{b∈Δ} P_{b}(z)) ∧ (z = y → P_{b_{0}}(z)) ∧ (Q_{K_{1}}z.⟨P_{b}(z)⟩_{b∈Δ_{0}})[> y]] .

Kb_{0}Δ^{∗} is definable in the same way. □

Open Problem Characterize those classes of (regular) languages L such that Lin(L) admits relativization.

The same question arises when the language contains the successor predicate instead of the < predicate.

7 Double semidirect product and block product

The double semidirect product and the block product of monoids were introduced in [28]. In this section, we extend these notions to mg-pairs.

Suppose that (S, A) and (T, B) are mg-pairs. We write the monoid operation of S additively without assuming that the operation is commutative. We denote by 0 the identity element of S. A (monoidal) left action of T (or of (T, B)) on (S, A) is a function

T × S → S
(t, s) ↦ ts

subject to the following conditions for all s, s′ ∈ S and t, t′ ∈ T:

(tt′)s = t(t′s)
t(s + s′) = ts + ts′
1s = s
t0 = 0.

Moreover, it is required that

ta ∈ A, for all t ∈ T, a ∈ A.

A right action S × T → S, (s, t) ↦ st is defined symmetrically. Actions T × S → S and S × T → S are compatible if

(ts)t′ = t(st′),

for all t, t′ ∈ T and s ∈ S. Due to the above laws, we will write just tst′ for (ts)t′ = t(st′), tt′s for t(t′s) = (tt′)s, etc.

Remark 7.1 Any left action of (T, B) on (S, A) is uniquely determined by a function B × A → A subject to certain conditions.

Given a compatible pair of left and right actions of T on (S, A), we define the double semidirect product (S, A)⋆⋆(T, B) as follows. First, we define

(s, t)(s′, t′) = (st′ + ts′, tt′),

for all s, s′ ∈ S and t, t′ ∈ T. It is known, cf. [28, 31] that S × T, equipped with this operation, is a monoid with identity element (0, 1). This monoid S⋆⋆T is called the double semidirect product of S and T determined by the actions. Let R denote the submonoid of S⋆⋆T generated by the set A × B. We define the double semidirect product (S, A)⋆⋆(T, B) to be the mg-pair (R, A × B). The monoid component R of (S, A)⋆⋆(T, B) is usually much smaller than the monoid S⋆⋆T. Given (s, t) ∈ S × T, we have (s, t) ∈ R iff there is some n ≥ 0 such that (s, t) is an n-fold product over A × B in the monoid S⋆⋆T.

Two special cases are of particular interest. The notion of semidirect product (S, A) ⋆ (T, B) involves only a left action of T on (S, A) and corresponds to the double semidirect product (S, A)⋆⋆(T, B) determined by the same left action and the trivial right action: st = s, for all s ∈ S and t ∈ T. When both actions are trivial, we obtain the direct product (S, A) × (T, B). This is the mg-pair (R, A × B), where R is the submonoid of the usual direct product S × T generated by A × B. The direct product is the categorical product in the category of mg-pairs.

For later use we note:

Proposition 7.2 For any finite mg-pairs (S, A) and (T, B), any language recognizable by (S, A) × (T, B) is a boolean combination of languages recognizable by (S, A) and (T, B).

Remark 7.3 The double semidirect product of monoids is closely related to the triple product of Eilenberg [11], vol. B. Any double semidirect product S⋆⋆T of monoids S and T embeds in a triple product [T, S, T] determined by the same actions. Moreover, as shown in Rhodes, Tilson [28], any triple product [T_{1}, S, T_{2}] of monoids S, T_{1}, T_{2} equipped with a monoidal right action S × T_{1} → S, (s, t_{1}) ↦ st_{1}, and a monoidal left action T_{2} × S → S, (t_{2}, s) ↦ t_{2}s, is isomorphic to the double semidirect product S⋆⋆(T_{1}×T_{2}) with actions (t_{1}, t_{2})s = t_{2}s and s(t_{1}, t_{2}) = st_{1}, for all s ∈ S and t_{i} ∈ T_{i}, i = 1, 2.

Suppose that (S, A) and (T, B) are mg-pairs. Then (S, A)^{T ×T}, the (T × T)- fold direct product of (S, A) with itself is an mg-pair (R, A^{T ×T}), where R is the submonoid of S^{T ×T} generated by the set A^{T ×T}. Thus, a function f : T × T → S belongs to R iff there is some n ≥ 0 such that for all t_{1}, t_{2} in T, f(t_{1}, t_{2}) is an n-fold product over A in the monoid S. The block product (S, A)□(T, B) is the double semidirect product

(R, A^{T ×T})⋆⋆(T, B)

determined by the following compatible left and right actions of T on (S, A)^{T ×T}:

(tf)(t_{1}, t_{2}) = f(t_{1}t, t_{2})
(ft)(t_{1}, t_{2}) = f(t_{1}, tt_{2}),

for all f ∈ R and t, t_{1}, t_{2} ∈ T. The reader should have no difficulty in verifying that tf, ft ∈ R for all f ∈ R and t ∈ T. Moreover, if f ∈ A^{T ×T}, then tf, ft ∈ A^{T ×T}, for all t ∈ T. The wreath product (S, A)∘(T, B) is defined in a similar way. It is the semidirect product (R, A^{T} × B) = (S, A)^{T} ⋆ (T, B) determined by the left action

(tf)(t_{1}) = f(t_{1}t), t_{1} ∈ T,

for all f ∈ R and t ∈ T.

Proposition 7.4 For any mg-pairs (S, A) and (T, B), every double semidirect product (M, A × B) = (S, A)⋆⋆(T, B) is isomorphic to a sub mg-pair of the block product (N, A^{T ×T} × B) = (S, A)□(T, B).

Proof. We follow the proof of Proposition 7.1 in Rhodes, Tilson [28]. For each s ∈ S let f_{s} : T × T → S denote the function (t_{1}, t_{2}) ↦ t_{1}st_{2}, t_{1} ∈ T_{1}, t_{2} ∈ T_{2}. Note that when s ∈ A, then f_{s} maps T × T into A. It is shown in Rhodes [27] that the assignment

(s, t) ↦ (f_{s}, t), (s, t) ∈ S × T

defines an injective morphism S⋆⋆T → S□T. Moreover, if (s, t) ∈ A × B, then (f_{s}, t) ∈ A^{T ×T} × B. To complete the proof we still need to show that if (s, t) ∈ M, then (f_{s}, t) ∈ N. However, if (s, t) is an n-fold product over A × B, for some n ≥ 0, then (f_{s}, t) is an n-fold product over A^{T ×T} × B.

□

For later use we note:

Lemma 7.5 Suppose that (M, A), (N, B) and (N′, B′) are mg-pairs such that (N′, B′) is a sub mg-pair of (N, B). If (S, C) is a sub mg-pair of (M, A)□(N, B) such that C ⊆ A^{N×N} × B′, then (S, C) is isomorphic to a sub mg-pair of a double semidirect product (M, A)^{N×N}⋆⋆(N′, B′).

Proof. Let T denote the monoid component of the direct power (M, A)^{N×N}, so that (M, A)^{N×N} = (T, A^{N×N}). When f ∈ T and n ∈ N, define nf and fn in T by nf(n_{1}, n_{2}) = f(n_{1}n, n_{2}) and fn(n_{1}, n_{2}) = f(n_{1}, nn_{2}), for all n_{1}, n_{2} ∈ N. Since (N′, B′) is a sub mg-pair of (N, B), it follows that the double semidirect product (M, A)^{N×N}⋆⋆(N′, B′) determined by this compatible pair of actions is isomorphic to a sub mg-pair of (M, A)□(N, B). Since this sub mg-pair contains (S, C), it follows that (S, C) is isomorphic to a sub mg-pair of a double semidirect product of (M, A)^{N×N} and (N′, B′).

□

8 Varieties of finite mg-pairs

In this section, other than free mg-pairs (Σ^{∗}, Σ), we will only consider finite mg-pairs.

A (pseudo)variety of finite mg-pairs is a class V of finite mg-pairs containing the trivial mg-pairs closed with respect to the direct product and division, i.e., such that

• (S, A), (T, B) ∈ V ⇒ (S, A) × (T, B) ∈ V, and

• (S, A) < (T, B), (T, B) ∈ V ⇒ (S, A) ∈ V.

A closed class of finite mg-pairs is a class of finite mg-pairs containing the trivial mg-pairs that is closed with respect to the double semidirect product and division. Since the direct product is a special case of the double semidirect product, any closed class of finite mg-pairs is a variety. Therefore we also call closed classes of finite mg-pairs as closed varieties. It is clear that each class K of finite mg-pairs is contained in a least variety V and in a least closed variety V̂ (of finite mg-pairs).

Given varieties V and W of finite mg-pairs, we define

• V⋆⋆W to be the variety generated by all double semidirect products (M, A)⋆⋆(T, B), where (M, A) ∈ V and (T, B) ∈ W,

• V□W to be the variety generated by all block products (M, A)□(T, B), where (M, A) ∈ V and (T, B) ∈ W.

Proposition 8.1 For all varieties V and W of finite mg-pairs, it holds that V⋆⋆W = V□W. Moreover, an mg-pair is in V⋆⋆W iff it is covered by a double semidirect product (S, A)⋆⋆(T, B), or, equivalently, by a block product (S, A)□(T, B), where (S, A) ∈ V and (T, B) ∈ W.

Proof. Since a block product (S, A)□(T, B) is a double semidirect product (S, A)^{B×B}⋆⋆(T, B), and since varieties are closed with respect to the direct product, it follows that V□W ⊆ V⋆⋆W. The reverse inclusion follows from Proposition 7.4.

The proof of the second claim uses the fact that any direct product of double semidirect products is isomorphic to a double semidirect product of direct products. Moreover, if (S_{i}, A_{i}) < (T_{i}, B_{i}), i = 1, 2, then (S_{1}, A_{1})□(S_{2}, A_{2}) < (T_{1}, B_{1})□(T_{2}, B_{2}). The argument is quite standard. All facts formulated in Proposition 8.1 are well-known for varieties of finite monoids. See, e.g., Rhodes [27]. □

Corollary 8.2 A class of finite mg-pairs is a closed variety iff it is not empty and is closed with respect to division and the block product.

Proposition 8.3 For all varieties V_{1}, V_{2}, V_{3} of finite mg-pairs, it holds that

(V_{1}⋆⋆V_{2})⋆⋆V_{3} ⊆ V_{1}⋆⋆(V_{2}⋆⋆V_{3}).

This fact is known to hold for varieties of finite monoids, cf. Rhodes [27], p.

460. As communicated to the authors by John Rhodes, the proof uses the Kernel Theorem (Theorem 7.4) of Rhodes, Tilson [28]. In the Appendix, we extend the kernel construction to mg-pairs.

Corollary 8.4 For every variety V of finite mg-pairs, the least closed variety V̂ containing V can be constructed as the class ⋃_{n≥0} V^{(n)}, where V^{(0)} is the class of all trivial mg-pairs and V^{(n+1)} = V⋆⋆V^{(n)} = V□V^{(n)}, for all n ≥ 0.

A version of Eilenberg’s Variety Theorem [11, 24] holds. The proof is standard.

Theorem 8.5 The function that maps a variety V of finite mg-pairs to the class L_{V} of (regular) languages recognizable by the members of V is an order isomorphism from the lattice of varieties of finite mg-pairs onto the lattice of literal varieties of regular languages. The inverse of this function takes a literal variety of regular languages V to the variety of finite mg-pairs that only accept languages in V.

It follows by Proposition 5.4 that the function V ↦ L_{V} maps a variety of finite mg-pairs V to the class of all (regular) languages whose syntactic mg-pair is in V. Moreover, the inverse assignment takes a literal variety V of regular languages to the variety generated by K_{V}.

Proposition 8.6

1. For a class K of finite mg-pairs, let V denote the variety of finite mg-pairs generated by K. Then Lin(K) = Lin(V).

2. Suppose that L is a class of regular languages and V is the variety generated by K_{L}. Then Lin(L) ⊆ Lin(V). Moreover, Lin(L) = Lin(V) iff quotients are expressible in Lin(L).

Proof. As for the first claim, since K ⊆ V, the inclusion Lin(K) ⊆ Lin(V) is obvious. For the reverse inclusion, note that any language that can be recognized by an mg-pair in V is a boolean combination of languages recognizable by the mg-pairs in K (use Proposition 7.2), and then apply Corollary 4.3. The second claim is immediate from the first and Proposition 5.9. □

Remark 8.7 If Lin(L) = Lin(V), where L is a class of regular languages and V is any variety, then quotients are expressible in Lin(L).

By our previous results we also have:

Proposition 8.8

1. For any class K of finite mg-pairs and integer n ≥ 0, Lin_{n}(K) = Lin_{n}(V), where V denotes the variety generated by K.

2. Suppose that L is a class of regular languages and V is the variety generated by K_{L}. Then Lin_{n}(L) ⊆ Lin_{n}(V), for each n ≥ 0. Moreover, the following conditions are equivalent:

(a) The quotient of each language in L belongs to the literal prevariety generated by L.

(b) The literal prevariety generated by L is a literal variety.

(c) Quotients are strictly expressible in Lin(L).

(d) Lin_{1}(L) is a literal variety.

(e) For all n ≥ 0, Lin_{n}(L) is a literal variety.

(f) Lin_{1}(L) = Lin_{1}(V).

(g) For all n ≥ 0, Lin_{n}(L) = Lin_{n}(V).

9 Lindström quantifiers and the block product

In this section, we assume that K is a class of finite mg-pairs and let V denote the variety of finite mg-pairs generated by K. Moreover, we denote by either K̂ or V̂ the least closed variety containing K (or V).

Proposition 9.1 Suppose that Lin(K) admits relativization. If all languages recognizable by the finite mg-pairs (S, A) and (T, B) belong to Lin(K), then any language recognizable by any double semidirect product (R, A×B) = (S, A)⋆⋆(T, B) belongs to Lin(K).

Proof. Let Σ be an alphabet, and let

h : Σ^{∗} → R

denote a monoid homomorphism with h(Σ) ⊆ A×B, so that h is a morphism (Σ^{∗}, Σ) → (R, A × B). It suffices to show that L = h^{−1}(r_{0}) is in Lin(K), for each r_{0} = (s_{0}, t_{0}) ∈ R.

For each σ ∈ Σ, let s_{σ} ∈ A denote the left-hand component of h(σ). We have

h(w) = ( ∑_{w=w′σw′′} π(h(w′))s_{σ}π(h(w′′)), π(h(w))) ,

for all w ∈ Σ^{∗}, where π denotes the projection R → T, π((s, t)) = t, for all (s, t) ∈ R. Note that each π(h(w′))s_{σ}π(h(w′′)) belongs to A. Since the composite of h and π is a homomorphism Σ^{∗} → T with π(h(Σ)) ⊆ B, it follows from our assumptions that for each t ∈ T there is a sentence α_{t} of Lin(L) such that for all words w ∈ Σ^{∗}, π(h(w)) = t iff w ⊧ α_{t}. For each a ∈ A let φ_{a} = φ_{a}(x) be the formula in the free variable x,

⋁_{t′s_{σ}t′′=a}(P_{σ}(x) ∧ α_{t′}[< x] ∧ α_{t′′}[> x]),

where α_{t′}[< x] and α_{t′′}[> x] denote relativizations of α_{t′} and α_{t′′}, respectively, which exist by assumption. Note that the family φ_{a}, a ∈ A is deterministic. Then let ψ be the sentence

Q_{K}x.⟨φ_{a}⟩_{a∈A},  (6)

where K ⊆ A^{∗} denotes the regular language recognized by (S, A) with the element s_{0} and the morphism (A^{∗}, A) → (S, A) which is the identity function on A. It is clear from the construction that ψ defines the set of all words w ∈ Σ^{∗} such that the left-hand component of h(w) is s_{0}. Thus, α_{t_{0}} ∧ ψ defines L. This shows that L ∈ Lin(Lin(K)). Thus, by Corollary 3.6, L ∈ Lin(K). □

Proposition 9.2 Suppose that Lin(K) strictly admits relativization. If all languages recognizable by the finite mg-pair (T, B) belong to Lin_{n}(K) and if (S, A) ∈ V, then any language recognizable in any double semidirect product (R, A × B) = (S, A)⋆⋆(T, B) belongs to Lin_{n+1}(K).

Proof. The argument is the same as above. The sentence (6) is in Lin_{n+1}(V). But by Proposition 8.8, Lin_{n+1}(V) = Lin_{n+1}(K). □

Suppose that Σ is a finite alphabet and V is a finite set of variables. Given a morphism h : ((Σ × P (V))^{∗}, Σ × P (V)) → (M, A) and a set F ⊆ M, where (M, A) is an mg-pair, the language of V -structures (over Σ) recognized by (M, A) with h and F consists of all V -structures u ∈ (Σ × P (V))^{∗} such that h(u) ∈ F. In other words, it is the intersection of the language of all V -structures over Σ and the language h^{−1}(F) recognized in the usual sense by (M, A) with h and F.

Suppose now that K ⊆ Δ^{∗} = {b_{1}, …, b_{k}}^{∗}, and consider a formula

ψ = Q_{K}x.⟨φ_{b_{i}}⟩_{b_{i}∈Δ},

where each φ_{b_{i}} = φ_{b_{i}}(x, y_{1}, …, y_{m}) is a formula of Lin(K) over the alphabet Σ whose free variables are among x, y_{1}, …, y_{m}. Let (M, A) denote the syntactic mg-pair of K, or any mg-pair by which K can be recognized. For each b_{i} ∈ Δ, let (N_{i}, B_{i}) denote an mg-pair recognizing the language of (V ∪ {x})-structures L_{i} = L_{φ_{b_{i}}} ⊆ (Σ × P (V ∪ {x}))^{∗} defined by φ_{b_{i}}, where V = {y_{1}, …, y_{m}}.

Proposition 9.3 The language L_{ψ} of V -structures over Σ defined by ψ can be recognized by the block product

(M, A)□[(N_{1}, B_{1}) × … × (N_{k}, B_{k})].

Proof. Let (N, B) denote the product (N_{1}, B_{1}) × … × (N_{k}, B_{k}), so that B = B_{1} × … × B_{k} and N is the submonoid generated by B in the direct product N_{1} × … × N_{k}. For each i ∈ [k], let η_{i} denote a morphism

((Σ × P (V ∪ {x}))^{∗}, Σ × P (V ∪ {x})) → (N_{i}, B_{i}),

recognizing L_{i}, and let η_{K} denote the syntactic morphism (Δ^{∗}, Δ) → (M, A) of K, or any morphism recognizing K.

Let us order B by b_{1} < … < b_{k}. We define

θ : ((Σ × P (V))^{∗}, Σ × P (V)) → (M, A)□(N, B)

by

θ((a, X)) = (F_{(a,X)}, η_{1}((a, X)), …, η_{k}((a, X))),

(a, X) ∈ Σ × P (V), where for all n_{1}, n′_{1} ∈ N_{1}, …, n_{k}, n′_{k} ∈ N_{k} such that (n_{1}, …, n_{k}), (n′_{1}, …, n′_{k}) ∈ N,

F_{(a,X)}((n_{1}, …, n_{k}), (n′_{1}, …, n′_{k})) = η_{K}(b_{i})

for the least b_{i} ∈ Δ such that n_{i}η_{i}((a, X ∪ {x}))n′_{i} ∈ η_{i}(L_{i}), if there is such a letter b_{i}. Otherwise, we define F_{(a,X)}((n_{1}, …, n_{k}), (n′_{1}, …, n′_{k})) to be any element of A. Note that we indeed have that

F_{(a,X)} ∈ A^{N×N}

and

θ((a, X)) ∈ A^{N×N} × B_{1} × … × B_{k}.

Let w = (a_{1}, X_{1}) … (a_{n}, X_{n}) ∈ (A × P (V))^{∗} be a V -structure and write F_{i} for F_{(a_{i},X_{i})}, for all i ∈ [n]. Then we have

θ(w) = (F_{1}, η_{1}((a_{1}, X_{1})), …, η_{k}((a_{1}, X_{1}))) …
… (F_{n}, η_{1}((a_{n}, X_{n})), …, η_{k}((a_{n}, X_{n})))
= (F, η_{1}(w), …, η_{k}(w)),

where

F ((1, …, 1), (1, …, 1)) =

= ∏_{i=1}^{n} F_{i}((η_{1}((a_{1}, X_{1}) … (a_{i−1}, X_{i−1})), …, η_{k}((a_{1}, X_{1}) … (a_{i−1}, X_{i−1}))),

(η_{1}((a_{i+1}, X_{i+1}) … (a_{n}, X_{n})), …, η_{k}((a_{i+1}, X_{i+1}) … (a_{n}, X_{n}))))

= ∏_{i=1}^{n} G_{i}.

Now, for each i ∈ [n], since (a_{1}, X_{1}) … (a_{i}, X_{i} ∪ {x}) … (a_{n}, X_{n}) is a (V ∪ {x})-structure, G_{i} = η_{K}(b_{j}) for the unique (and thus least) j such that

η_{j}((a_{1}, X_{1}) … (a_{i}, X_{i} ∪ {x}) … (a_{n}, X_{n})) ∈ η_{j}(L_{j}),

i.e., the unique j with

(a_{1}, X_{1}) … (a_{i}, X_{i} ∪ {x}) … (a_{n}, X_{n}) ∈ L_{j}.

Thus, F ((1, …, 1), (1, …, 1)) = η_{K}(\overline{w}), where \overline{w} is the characteristic word determined by w and the formula ψ. It follows that L_{ψ} is exactly the language of V -structures recognized by θ with those elements (F, n_{1}, …, n_{k}) of the block product satisfying F ((1, …, 1), (1 …, 1)) ∈ η_{K}(K). □

Remark 9.4 Let π denote the projection

(M, A)□[(N_{1}, B_{1}) × … × (N_{k}, B_{k})] → (N_{1}, B_{1}) × … × (N_{k}, B_{k}),

and for each i ∈ [k], let π_{i} denote the projection

(N_{1}, B_{1}) × … × (N_{k}, B_{k}) → (N_{i}, B_{i}).

The morphism θ constructed above has the property that for each i ∈ [k], the composite

(Σ × P (V))^{∗} ⟶^{θ} (M, A)□[(N_{1}, B_{1}) × … × (N_{k}, B_{k})]
⟶^{π} (N_{1}, B_{1}) × … × (N_{k}, B_{k})
⟶^{π_{i}} (N_{i}, B_{i})

is the morphism (Σ×P (V))^{∗} → (N_{i}, B_{i}) obtained by restricting the function η_{i} : (Σ × P (V ∪ {x}))^{∗} → N_{i} to (Σ × P (V))^{∗}. In particular, for each i ∈ [k], the restriction of the above composite morphism to Σ^{∗} agrees with the restriction of η_{i} to Σ^{∗}. (We regard Σ as a subset of Σ × P (V) which in turn is a subset of Σ × P (V ∪ {x}).) Thus, if each (N′_{i}, B′_{i}) = (η_{i}(Σ^{∗}), η_{i}(Σ)) belongs to W, for some variety W, then (θ(Σ^{∗}), θ(Σ)) belongs to V⋆⋆W, since by Lemma 7.5, (θ(Σ^{∗}), θ(Σ)) embeds in a double semidirect product of a direct power of (M, A) and the mg-pair (N′_{1}, B′_{1}) × … × (N′_{k}, B′_{k}).

Recall that by Corollary 8.4, we have K̂ = V̂ = ⋃_{n≥0} V^{(n)}, where V^{(0)} is the class of trivial mg-pairs and V^{(n+1)} = V⋆⋆V^{(n)} = V□V^{(n)}.

We are now ready to prove the main result of this section.

Theorem 9.5 Suppose that K is a class of finite mg-pairs and V denotes the variety generated by K. Then for each n ≥ 0, every language in Lin_{n}(K) is recognizable by some mg-pair in V^{(n)}, i.e., Lin_{n}(K) ⊆ L_{V^{(n)}}. Thus, Lin(K) ⊆ L_{K}. Moreover, if Lin(K) admits relativization, then a language belongs to Lin(K) iff it can be recognized by an mg-pair in K̂, i.e., Lin(K) = L_{K}. And if Lin(K) strictly admits relativization, then for each n ≥ 0, Lin_{n}(K) = L_{V^{(n)}}.

Proof. In order to prove the first claim, suppose that φ is a formula of Lin(K) over the alphabet Σ with free variables included in the finite set V. Let qd(φ) = n. We argue by induction on the structure of φ to show that L_{φ} can be recognized by a morphism θ : (Σ × P (V))^{∗} → (M, A) such that (θ(Σ^{∗}), θ(Σ)) belongs to V^{(n)}. When φ is an atomic formula, or the formula false, then n = 0 and any two words in Σ^{∗} are equivalent with respect to the syntactic congruence of L_{φ}. Let η_{L_{φ}} denote the syntactic morphism ((Σ×P (V))^{∗}, Σ×P (V)) → Synt(L_{φ}). Then (η_{L_{φ}}(Σ^{∗}), η_{L_{φ}}(Σ)) is trivial and thus belongs to V^{(0)}, proving the claim. Suppose now that φ is φ_{1}∨φ_{2}, and that L_{φ_{i}} can be recognized by the morphism θ_{i} : (Σ×P (V))^{∗} → (M_{i}, A_{i}) such that (θ_{i}(Σ^{∗}), θ_{i}(Σ)) belongs to V^{(n)}, i = 1, 2. Then L_{φ} can be recognized by the target pairing

θ = ⟨θ_{1}, θ_{2}⟩ : (Σ × P (V))^{∗} → (M_{1}, A_{1}) × (M_{2}, A_{2})
(σ, X) ↦ (θ_{1}((σ, X)), θ_{2}((σ, X))).

Since

(θ(Σ^{∗}), θ(Σ)) < (θ_{1}(Σ^{∗}), θ_{1}(Σ)) × (θ_{2}(Σ^{∗}), θ_{2}(Σ))

and varieties are closed with respect to direct product and division, and since qd(φ_{1}), qd(φ_{2}) ≤ n, it follows by the induction hypothesis that (θ(Σ^{∗}), θ(Σ)) belongs to V^{(n)}. When φ is of the form ¬ψ, the result follows by using that L_{φ} and L_{ψ} can be recognized by the same mg-pairs. Suppose finally that φ = Q_{K}x.⟨φ_{b_{i}}⟩_{b_{i}∈Δ}, where B ⊆ Δ^{∗}, Δ = {b_{1}, …, b_{k}}, is a language recognized by some mg-pair (M, A) in K, and where each φ_{b_{i}} is a formula of Lin(K) over Σ with free variables in V ∪{x} of quantifier depth at most n−1. By the induction hypothesis, each L_{φ_{b_{i}}} can be recognized by a morphism

θ_{i} : (A × P (V ∪ {x}))^{∗} → (N_{i}, B_{i})

such that (θ_{i}(Σ^{∗}), θ_{i}(Σ)) ∈ V^{(n−1)}. But then, by Proposition 9.3 and Remark 9.4, L_{φ} can be recognized by a morphism

θ : (Σ × P (V))^{∗} → (M, A)□[(N_{1}, B_{1}) × … × (N_{k}, B_{k})]

such that (θ(Σ^{∗}), θ(Σ) is in V^{(n)}.

Assume now that Lin(K) admits relativization. We show that if the syntactic mg-pair Synt(L) of a language L ⊆ Σ^{∗} belongs to V^{(n)}, for some n ≥ 0, then L ∈ Lin(K). When n = 0, Synt(L) is trivial and thus L is either the empty set or Σ^{∗}. In either case, L can be defined by a sentence of Lin(K), namely by false or true, proving that L ∈ Lin(K). We proceed by induction on n. When n > 0 and Synt(L) ∈ V^{(n)}, then L can be recognized by a double semidirect product

(S, A)⋆⋆(T, B),

where (S, A) ∈ V and (T, B) ∈ V^{(n−1)}. By the induction hypothesis, every language recognizable by (T, B) is in Lin(K). Thus, by Proposition 9.1 , L belongs to Lin(K). The same argument using Proposition 9.2 proves that if Lin(K) strictly admits relativization, then Lin_{n}(K) ⊆ L_{V^{(n)}}, for all n ≥ 0.

□

Corollary 9.6 For any class K of finite mg-pairs, FO(K) ⊆ L_{K_{1}}, where K_{1} = K ∪ {U_{1}} and K̂_{1} is the closed variety generated by K_{1}. Moreover, when FO(K) admits relativization, then FO(K) = L_{K_{1}}.

Corollary 9.7 Suppose that K is a class of finite mg-pairs such that FO(K) strictly admits relativization. Let V_{1} denote the variety generated by K_{1} = K ∪ {U_{1}}. Then for each n, FO_{n}(K) = L_{V_{1}^{(n)}}.

Proof. By definition, FO(K) = Lin(L_{K} ∪ {K_{∃}}) ⊆ Lin(K_{1}). It is easy to see that for each n, FO_{n}(K) = Lin_{n}(K_{1}). Moreover, since FO(K) strictly admits relativization, so does Lin(K_{1}). Thus the result follows from Theorem 9.5 applied to K_{1}. □

Corollary 9.8 For any class L of regular languages, Lin(L) ⊆ L_{V}, where V̂ = K̂_{L}, the least closed variety containing the syntactic mg-pairs of the languages in L. Moreover, when quotients are expressible in Lin(L) and Lin(L) admits relativization, then Lin(L) = L_{V}.

Proof. It is clear that Lin(L) ⊆ Lin(K_{L}). Moreover, Lin(K_{L}) ⊆ L_{V}, by Theorem 9.5. Assume now that quotients are expressible in Lin(L) and Lin(L) admits relativization. We know that Lin(L) = Lin(K_{L}) (Proposition 5.9). Since Lin(L) admits relativization, so does Lin(K_{L}), by Proposition 6.2. Thus, by Theorem 9.5, Lin(L) = L_{V}. □

Corollary 9.9 For any class L of regular languages, FO(L) ⊆ L_{V_{1}}, where V̂_{1} denotes the least closed variety containing U_{1} and the syntactic mg-pairs of the languages in L. Moreover, when quotients are expressible in FO(L) and FO(L) admits relativization, then FO(L) = L_{V_{1}}.

Corollary 9.10 Suppose that L is a class of regular languages such that the quotient of any language in L belongs to the literal prevariety generated by L. Suppose that Lin(L) strictly admits relativization. Then for each n ≥ 0, Lin_{n}(L) = L_{V^{(n)}}, where V denotes the variety generated by K_{L}.

Proof. By Theorem 9.5, Proposition 8.8 and Proposition 6.2. □

Corollary 9.11 Suppose that L is a class of regular languages such that the quotient of any language in L belongs to the literal prevariety generated by L. Suppose that FO(L) strictly admits relativization. Then for each n ≥ 0, FO_{n}(L) = L_{V_{1}^{(n)}}, where V_{1} denotes the variety generated by K_{1} = K_{L} ∪ {U_{1}}.

Proof. This follows from Corollary 9.10 by noting that for each n, FO_{n}(L) = Lin_{n}(L∪{K_{∃}}) = Lin_{n}(L∪{K_{∃}}). Moreover, every quotient of any language in L ∪ {K_{∃}} is either K_{∃}, or it belongs to the literal prevariety generated by L. Since by assumption FO(L) strictly admits relativization, so does Lin(L ∪ {K_{∃}}). □

Example 9.12 • Let L consist of the one-letter languages L_{m}^{r} = (b_{1}^{m})^{∗}b_{1}^{r}, m ≥ 1, 0 ≤ r < m, so that L is closed with respect to quotients. Then a language L ⊆ Σ^{∗} belongs to Lin(L) iff there exists some m such that L is the union of some languages h^{−1}(L_{m}^{r}), where h denotes the unique literal homomorphism Σ^{∗} → {a}^{∗}. Also, K_{L} is the class of all mg-pairs of the form (Z_{m}, {a}) where Z_{m} is a cyclic group of order m with cyclic generator a, and K̂_{L} is the is the class of all mg-pairs of the form (Z_{n}, {a}) where n divides m. We have that a language belongs to Lin(L) iff its syntactic mg-pair is in K̂_{L}, yet Lin(L) does not admit relativization. See Example 6.1.

• Let L consist of the finite and cofinite languages, so that L = Lin(L). Then L is closed with respect to quotients, moreover, K̂_{L} is the class of all finite nilpotent mg-pairs, i.e., those finite mg-pairs (M, A) such that for some n ≥ 1, all n-fold products a_{1} … a_{n} of the distinguished generators give the same monoid element. Again, L ∈ Lin(L) holds for a language L iff Synt(L) is in K̂_{L}, but as shown in Example 6.1, Lin(L) does not admit relativization.

Example 9.13 We give an example of a class L of regular languages closed with respect to quotients such that the variety of finite mg-pairs corresponding to FO(L) = Lin(L∪{K_{∃}}) is properly included in the least closed variety V̂_{1} containing the syntactic mg-pairs of the languages in L ∪ {K_{∃}}. Thus, the assumption that Lin(L) admits relativization is essential to have Lin(L) = L_{V} in Corollary 9.8. Similarly, the equality FO(L) = L_{V_{1}} of Corollary 9.9 fails in general if FO(L) does not admit relativization.

Let L = {L_{m}^{r} : m ≥ 1, 0 ≤ r < m}, where for each m and r, L_{m}^{r} is the one-letter language (b_{1}^{m})^{∗}b_{1}^{r}. Note that L is closed with respect to quotients. One can argue by induction on the structure of the formula φ over Σ of FO(L) to show that there exists some m such that φ is equivalent to a formula of the form

(φ_{0} ∧ Q_{L_{m}^{0}}x.⟨⟩) ∨ … ∨ (φ_{m−1} ∧ Q_{L_{m}^{m−1}}x.⟨⟩),

where each φ_{i} is a first-order formula over Σ. Thus, a language L ⊆ Σ^{∗} belongs to FO(L) iff there exists some m ≥ 1 such that for each r with 0 ≤ r < m, L ∩ (Σ^{m})^{∗}Σ^{r} is in FO.

Now let V̂_{1} denote the closed variety generated by K_{L∪{K_{∃}}}, i.e., the closed variety generated by the mg-pairs {U_{1}, (Z_{m}, {a}) : m ≥ 1}. It is known, cf. [2], that an mg-pair (M, A) belongs to V̂_{1} iff it is quasi-aperiodic, i.e., it is finite and for each integer k, every group in M which is contained in the set A^{k} of all k-fold products of the generators is trivial. Let L be the two-letter language (abab)^{∗}. The reader can easily verify that Synt(L) is quasi-aperiodic. Indeed, denoting Synt(L) by (M_{L}, {a, b}) (i.e., we identify the letters a and b with the corresponding generators of M_{L}), the only nontrivial groups contained in M_{L} are two groups of order 2. These are the groups {ab, abab} and {ba, baba}. But the length of any word representing the element ab or ba is congruent to 2 modulo 4, while the length of any word representing abab or baba is congruent to 0 modulo 4. Thus, there exist no k such that both ab and abab can be represented by length k words, and similarly for ba and baba, showing that Synt(L) is quasi-aperiodic. On the other hand, L is not in FO(L). To see this, let m be any positive integer, and let n denote the l.c.m. of m and 4. We have L ∩ (Σ^{m})^{∗} = ((abab)^{n/4})^{∗} which is not aperiodic, since its syntactic monoid contains a group of order 2. Thus, by the theorem of McNaughton and Papert [22], L ∩ (Σ^{m})^{∗} is not in FO, hence L is not in FO(L). It follows that FO(L) ⊂ L_{V_{1}}, or equivalently, the variety W generated by K_{FO(L)} is strictly included in V̂_{1}. (In fact, W is the direct product of the variety of aperiodic mg-pairs and the variety of counters, i.e., mg-pairs of the form (Z_{m}, {a}), m ≥ 1.)

The following results can be derived by combining some facts from Section 6 with Theorem 9.5 and the above corollaries of Theorem 9.5.

Corollary 9.14 Suppose that L is a class of regular languages such that quotients are expressible in Lin(L) and for each K in L, the padding of K belongs to Lin(L). Then Lin(L) = L_{V}, where V̂ denotes the closed variety generated by K_{L}. Moreover, if quotients are expressible in FO(L) and for each K in L, the padding of K belongs to FO(L), then FO(L) = L_{V_{1}}, where V̂_{1} denotes the closed variety generated by K_{L} ∪ {U_{1}}.

Corollary 9.15 Suppose that L is a class of regular languages such that the padding and each quotient of any language in L belong to the literal prevariety generated by L. Then for each n, Lin_{n}(L) = V^{(n)} and FO_{n}(L) = V_{1}^{(n)}, where V denotes the variety generated by K_{L} and V_{1} is the variety generated by K_{L} ∪ {U_{1}}.

Corollary 9.16 For any class K of finite mgi-pairs and for every integer n ≥ 0, Lin_{n}(K) = L_{V^{(n)}} and FO(K) = L_{V_{1}^{(n)}}, where V denotes the variety generated by K and V_{1} is the variety generated by K ∪ {U_{1}}.

Remark 9.17 The main result, Theorem 9.5 extends to the situation when the language contains the successor predicate instead of the < predicate. In fact, the only property one needs to require from the numerical predicates is that for any atomic formula φ over an alphabet Σ involving a numerical predicate, and for any two words u, v ∈ Σ^{∗}, it holds that u and v are collapsed by the syntactic congruence of L_{φ} iff u = v. However, the assumption in the second part of the Theorem that the logic admits relativization seems to be quite strong when the successor predicate is the only numerical predicate.

10 The Krohn-Rhodes theorem

In this section, we first review a version of the fundamental theorem of Krohn and Rhodes [17, 1] which involves the double semidirect product (block product). The original formulation involved the wreath product, and its automata theoretic equivalent, the cascade product. Our presentation follows Straubing [31], Appendix A. Then we review some results from Dömösi, Ésik [9] and Ésik [13] and apply them in conjunction with the Krohn-Rhodes Theorem to obtain descriptions of certain closed varieties of finite mg-pairs. The results of this section will be applied in Section 11 in the characterization of the expressive power of Lindström quantifiers with respect to regular languages.

All monoids considered in this section are assumed to be finite. As before, we will identify a finite monoid M with the mg-pair (M, M). For a class K of finite monoids (mg-pairs), we let K̂ denote the least class of finite monoids (mg-pairs) containing K which is closed with respect to the double semidirect product (block product) and division. It is a simple matter to show that when K is a class of finite monoids and K_{1} is the class of mg-pairs (M, M), where M ∈ K, then an mg-pair (S, A) belongs to K̂_{1} iff S belongs to K̂. If K denotes a class of finite mg-pairs, then we let \overline{K} denote the class of all monoid components of the mg-pairs in K. When K is a class of finite monoids and M is a finite monoid, M < K means that there is a monoid S ∈ K with M < S.

Recall that U_{1} denotes a two-element semilattice. Moreover, recall that a (finite) group G is called simple if it is nontrivial and has no nontrivial normal subgroup. It is a simple matter to show that a finite monoid M is group iff U_{1} < M does not hold. Indeed, if M is not a group, then it contains an idempotent e other than the identity element 1. Then {1, e} is a submonoid of M which is isomorphic to U_{1}.

Theorem 10.1 Krohn–Rhodes Theorem

• Part 1. The following two conditions are equivalent for a nontrivial finite monoid M.

1. M is a simple group or isomorphic to U_{1}.

2. For every class K of finite monoids, if M ∈ K̂ then M < K.

• Part 2. Suppose that M is a finite monoid and K is a class of finite monoids containing at least one monoid which covers U_{1}. Then M ∈ K̂ iff for every finite simple group G, if G < M then G < K. Moreover, when K is a class of finite groups, then M ∈ K iff M is a finite group and for every finite simple group G, if G < M then G < K.

Remark 10.2 If one defines K̂ as the closure of K with respect to the semidirect product (or wreath product) and division, then the result remains true provided that in Part 1 both U_{1} and the three element monoid U_{2} with two right zero elements are allowed, and if U_{1} is replaced by U_{2} in Part 2. In fact, the original formulations of the Krohn-Rhodes Theorem (Krohn, Rhodes [17], Arbib [1]) used the wreath product and/or the corresponding automata theoretic notion of cascade composition.

Recall that a finite monoid M is called aperiodic, cf. Eilenberg [11], Pin [24], if it contains no nontrivial group, or equivalently, if no nontrivial group (or simple group) divides M. Moreover, recall that M is solvable, cf. Pin [24], Straubing [31], if every group included in M is solvable. (Such a group does not necessarily contain the identity element of M.) We denote the class of all aperiodics and the class of all finite groups by A and G, respectively. Moreover, we denote by GSol the class of finite solvable groups, and by MSol the class of finite solvable monoids. Moreover, when P is a set of prime numbers, we denote by GSol_{P} the subclass of GSol determined by those finite solvable groups whose order is a product of primes in P. The variety MSol_{P} is defined likewise. Note that when P is empty, MSol_{P} = A, and when P is the set of all prime numbers, then GSol_{P} = GSol and MSol_{P} = MSol. More generally, when S denotes a class of finite simple groups closed with respect to division, we let G_{S} denote the class of finite groups all of whose simple group divisors lie in S. Moreover, we let M_{S} denote the class of those finite monoids which only contain groups in G_{S}. When S is empty, M_{S} is the class of all aperiodic monoids. Moreover, when S is the class of cyclic groups of prime order, then G_{S} = GSol and M_{S} = MSol. And when S contains all finite simple groups, then G_{S} is the class G of all finite groups, and M_{S} = M is the class of all finite monoids. By the Krohn-Rhodes theorem, the above classes are all closed varieties (of finite monoids), i.e., they are closed with respect to the double semidirect product (block product) and division.

Corollary 10.3 Let K denote a class of finite monoids and let S denote a class of finite simple groups closed with respect to division.

• G_{S} ⊆ K̂ iff G < K holds for all G ∈ S. Moreover, K̂ = G_{S} iff K ⊆ G_{S} and G < K holds for all G ∈ S, iff U_{1} ≮ K and for all finite simple groups G it holds that G < K iff G ∈ S.

• M_{S} ⊆ K̂ iff U_{1} < K and G < K, for all G ∈ S. Moreover, K̂ = M_{S} iff K ⊆ M_{S} and U_{1} < K and G < K, for all G ∈ S, iff U_{1} < K and for all finite simple groups G it holds that G < K iff G ∈ S.

In particular, we obtain:

• K̂ = M iff the monoid U_{1} as well as each finite (non-abelian) simple group is covered by some monoid in K.

• G ⊆ K̂ iff G < K holds for all finite simple groups G. Moreover, K̂ = G iff K ⊆ G and G < K holds for all finite (non-abelian) simple groups G, iff U_{1} ≮ K and G < K holds for all finite (non-abelian) simple groups G.

• A ⊆ K̂ iff U_{1} < K. Moreover, K̂ = A iff K ⊆ A and U_{1} < K, iff no nontrivial finite group divides K and U_{1} < K.

• GSol_{P} ⊆ K̂ iff Z_{p} < K holds for all cyclic groups Z_{p} of prime order p ∈ P. Moreover, K̂ = GSol_{P} iff K ⊆ GSol_{P} and Z_{p} < K holds for all cyclic groups Z_{p} with p ∈ P, iff U_{1} ≮ K an for each simple group G we have G < K iff G is cyclic with order in P.

We now turn our attention to mg-pairs. Below we identify any class K of finite monoids with the class of all mg-pairs (M, A) such that M ∈ K. Thus, for example, M also denotes the class of all finite mg-pairs, MSol the class all finite mg-pairs whose monoid component is solvable, etc. It holds that K is a variety of finite monoids (cf. [24]) iff K is a variety as a class of finite mg-pairs. Moreover, K, as a variety of finite monoids is closed with respect to the double semidirect product iff K, as a class of finite mg-pairs, is a closed variety.

Suppose that M is a finite monoid, (S, A) is a finite mg-pair, and n ≥ 1. Following Dömösi, Ésik [9], we say that M divides (S, A) in length n ≥ 1, denoted M|^{(n)}(S, A), if S contains a subsemigroup T that maps homomorphically onto M under a homomorphism h : T → M such that each set h^{−1}(m), m ∈ M contains an n-fold product of elements in A (i.e., an element in A^{n}). We define M|(S, A) iff there is some n with M|^{(n)}(S, A). (This relation may be called divisibility in equal lengths.)

Proposition 10.4 Let T denote the submonoid generated by A^{n} in S. Then M|^{(n)}(S, A) iff M < (T, A^{n}).

Proof. If (M, M) < (T, A^{n}), then a sub mg-pair (T′, B) of (T, A^{n}) maps homomorhically onto (M, M). Let h denote a surjective homomorphism (T′, B) → (M, M). Since h maps B ⊆ A^{n} onto M, each element of M is the image of an n-fold product over A. Thus, M|^{(n)}(S, A).

Suppose now that M|^{(n)}(S, A). Then let T′ be a subsemigroup of S and h : T′ → M a surjective semigroup homomorphism such that h^{−1}(m) ∩ A^{n} is not empty, for all m ∈ M. For each m ∈ M, let b_{m} = h^{−1}(m) ∩ A^{n}, and let T′′ denote the submonoid of S generated by B = {b_{m} : m ∈ M}, so that (T′′, B) is a sub mg-pair of (T, A^{n}). It is clear that (M, M) is a quotient of (T′′, B), proving (M, M) < (T, A^{n}). □

Proposition 10.5 If M|^{(n)}(S, A) then there is a multiple m of n and a subsemigroup T of S contained in A^{m} such that M is a homomorphic image of T.

This is shown in Ésik [13], cf. Lemma 3.3. Since M is a monoid, T can be chosen to be a monoid as well. However, T may not contain the identity element of S. Also, when M is a group, T can be assumed to be a group as well.

Proposition 10.6 Suppose that (S, A) is a finite mg-pair and M is a finite non-abelian simple group or the monoid U_{1}. If M < S then M|(S, A).

This is a very particular case of Proposition 3.5 in Ésik [13]. See also Maurer, Rhodes [21]. The case M = U_{1} is obvious.

Proposition 10.7 Suppose that M is U_{1} or a finite simple group, moreover, suppose that M|(S, A)⋆⋆(T, B), where (S, A) and (T, B) are finite mgpairs. Then either M|(S, A) or M|(T, B).

Proof. When M is U_{1}, or a finite non-abelian simple group, this follows from the first part of the Krohn-Rhodes Theorem and Proposition 10.6. Thus, to complete the proof, it suffices to establish the claim for (cyclic) groups of prime order. So suppose that G is a cyclic group with prime order p such that G|(S, A)⋆⋆(T, B) = (M, A × B). By Proposition 10.5, G is a homomorphic image of a group in M all of whose members are n-fold products of elements in A × B, for some n ≥ 1. It follows easily that this group in turn contains a cyclic subgroup H of order p. Let (f, e) denote the identity element of H and let (s, t) denote any element of H different from (f, e). If t ≠ e then clearly t generates a cyclic group of order p in T (whose identity element is e), all of whose elements are n-fold products over B. We conclude that G|^{(n)}(T, B). So suppose now that t = e. Then the right-hand component of each element of H is e. It follows as in Straubing [31], p. 64, or Eilenberg [11], v. B, p. 143, that the function (s, e) ↦ ese, (s, e) ∈ H is an injective homomorphism H → S. Since each (s, e) ∈ H is an n-fold product over A × B, it follows that each element ese, (s, e) ∈ H is an n-fold product over A. Thus, we have G|^{(n)}(S, A). □

Suppose that M is a finite monoid, K is a class of finite mg-pairs, and n ≥ 1. Below we will write M|^{(n)}K (M|K, respectively) to denote that there exists an mg-pair (S, A) ∈ K such that M|^{(n)}(S, A) (M|(S, A), respectively).

Corollary 10.8 Let M be U_{1} or a finite simple group, and let K denote a class of finite mg-pairs. If M|K̂ then M|K.

Recall from Example 9.13 that a counter of length n is an mg-pair consisting of a cyclic group Z_{n} of order n and a singleton generating set. We let (Z_{n}, {a}) denote a counter of order n. A nontrivial counter is a counter of length > 1. Given a monoid M and an element a ∈ M, the period of a is the least positive integer p such that there exists some m with a^{m} = a^{m+p}, i.e., the period of the cyclic semigroup generated by a.

The following fact is clear.

Lemma 10.9 Suppose that (T, B) is a finite mg-pair and n ≥ 1. Then (Z_{n}, {a}) < (T, B) iff there is some b ∈ B whose period is a multiple of n.

We say that a sequence s_{0}, s_{1}, s_{2}, … is ultimately periodic if there exist some k ≥ 0 and p ≥ 1 such that s_{i+p} = s_{i} for all i ≥ k. It is clear that if the sequence s_{0}, s_{1}, s_{2}, … is ultimately periodic, then there exists a least p ≥ 1 such that the above property holds for some k. This number p is called the period of the sequence.

Lemma 10.10 Suppose that M is a finite monoid and a ∈ M has period n. Then for each m, m′ in M, the sequence mm′, mam, ma^{2}m′, … is ultimately periodic with a period p that divides n.

Proof. It is clear that the sequence mm′, mam, ma^{2}m′, … is ultimately periodic, moreover, there is an integer k such that ma^{i+n}m′ = ma^{i}m′, for all i ≥ k. But the period p is a divisor of any such n. □

Lemma 10.11 Suppose that a nontrivial counter divides a double semidirect product (S, A × B) = (M, A)⋆⋆(N, B). Then there is a nontrivial counter which divides (M, A) or (N, B).

Proof. By Lemma 10.9, there is some (a, b) ∈ A × B ⊆ S with period n > 1. If the period of b is > 1, then we are done. So suppose that the period of b is 1, i.e., b^{k} = b^{k+1}, for some k. Consider the sequence

(a, b), (a, b)^{2}, …

which is, by assumption, ultimately periodic with period n. But for all ℓ ≥ 0,

(a, b)^{2k+ℓ} =

= (ab^{2k+ℓ−1} + bab^{2k+ℓ−2} + … + b^{2k+ℓ−1}a, b^{2k+ℓ})
= (ab^{k} + bab^{k} + … + \overbrace{b^{k}ab^{k} + … + b^{k}ab^{k}}^{ℓ times} +b^{k}ab^{k−1} + … + b^{k}a, b^{k}).

Thus, by Lemma 10.10, n divides the period of b^{k}ab^{k}. It follows that a counter of length n divides (M, A). □

Corollary 10.12 Given a class K of mg-pairs, K̂ contains a nontrivial counter iff a nontrivial counter divides an mg-pair in K.

Remark 10.13 The proof of Lemma 10.11 can easily be modified to show the following fact: A counter of length n > 1 divides a double semidirect product (M, A)⋆⋆(N, B) iff there exist integers p, q such that n divides pq, moreover, a counter of length p divides (N, B), and a counter of length q divides (M′, A^{p}), where M′ is the submonoid of M generated by A^{p}.

It is shown in Dömösi, Ésik [9] that if M|^{n}(S, A), then M, or more precisely, the mg-pair (M, M) divides a wreath product

(S, A) ∘ (R, B) ∘ (Z_{n}, {a}),  (7)

where R is aperiodic. (Actually this fact is shown in [9] for finite automata and the cascade product, moreover, only a special type of aperiodic automata, namely definite automata are needed in the construction. The wreath product is associative, this is why no parentheses appear in (7).) Thus, by the Krohn-Rhodes Theorem and Proposition 8.3, we have:

Proposition 10.14 Suppose that (S, A) is a finite mg-pair and M is a finite monoid with M|^{n}(S, A). Then M ∈ K̂, where K consists of U_{1}, a counter of length n, and the mg-pair (S, A).

Corollary 10.15 Suppose that K is a class of finite mg-pairs such that U_{1} ∈ K̂ and for each finite simple group G with G < \overline{K} there exists some n ≥ 1 with G|^{(n)}K and (Z_{n}, {a}) ∈ K̂. Then a finite mg-pair (M, A) belongs to K̂ iff for every finite simple group G, if G < M then G < \overline{K}.

Proof. One direction is immediate from the Krohn–Rhodes Theorem. The other direction follows from the Krohn–Rhodes Theorem, Theorem 10.1, and Proposition 10.14. Indeed, assume that every simple group divisor of M divides the underlying monoid of an mg-pair in K. Let G_{1}, …, G_{k} denote, up to isomorphism, all of the simple group divisors of M. By assumption, for each i there exists n_{i} with G_{i}|^{(n_{i})}K and (Z_{n_{i}}, {a}) ∈ K̂. Since also U_{1} ∈ K̂, it follows from Proposition 10.14 that G_{i} ∈ K̂. Since this holds for all i ∈ [k], thus, by the Krohn–Rhodes Theorem, (M, A) ∈ K̂. □

Corollary 10.16 Suppose that K is a class of finite mg-pairs such that K̂ contains U_{1} as well as all the counters. Moreover, suppose that for all finite simple groups G, if G < \overline{K} then G|K. Then a finite mg-pair (M, A) belongs to K̂ iff for every finite simple group G, if G < M then G|K.

Call a class K of finite mg-pairs group-complete if every finite group divides some monoid in \overline{K}. Since every finite group embeds in a finite (non-abelian) simple group, by Proposition 10.6 we have that K is group-complete iff every finite (non-abelian) simple group divides in equal lengths some mg-pair in K.

Corollary 10.17 Let K be a class of finite mg-pairs. Then K̂ is the class of all finite mg-pairs iff the following hold:

1. K̂ contains U_{1} and all counters.

2. K is group-complete.

Remark 10.18 It is clear that K̂ contains all counters iff it contains all counters of prime power length.

Example 10.19 For each n ≥ 1, let S_{n} denote the symmetric group of all permutations of the set [n]. If n ≥ 3, S_{n} is generated by the cyclic permutation ρ = (12 … n) and the transposition π = (12). Hence, (S_{n}, {ρ, π}) is an mg-pair. Let K consist of (U_{1}, U_{1}) and all the mg-pairs (S_{n}, {ρ, π}), n ≥ 3. Then both conditions of Corollary 10.17 are satisfied, so that K̂ is the class of all finite mg-pairs.

Note that (S_{n}, {ρ, π}) is just the mg-pair of the automaton whose states are the integers in the set [n] which has two input letters that induce the permutations ρ and π, respectively.

Example 10.20 We modify the previous example to show that there is a group-complete class K with U_{1} ∈ K such that K̂ contains no counter. So let K consist of U_{1} and, for each n ≥ 3, the mg-pair of the following automaton Q_{n} with 2n + 1 states. The state set of Q_{n} consists of the integers 1, 2, …, 2n and the state 2′, and there are four input letters, a, b, c, d. For each state q and letter x, qx = q, except for the following cases.

(2i − 1)a = 2i, i ∈ [n]
(2i)b = 2i + 1, i ∈ [n − 1]
(2n)b = 1
1c = 2
2d = 3
3c = 2′
2′d = 1.

Thus, on the set of odd integers, the word ab induces the cyclic permutation (13...(2n − 1)) and cd induces the transposition (13). Thus, K is group-complete and contains U_{1}.

However, no non-trivial counter divides any mg-pair in K, since for each Q_{n}, any letter x ∈ {a, b, c, d} induces the same function as x^{2}, and similarly for U_{1}. (See Corollary 10.12).

This example can be modified to show that there is a class K of finite mg-pairs which is group-complete, contains U_{1} as well as each counter whose length is not a multiple of a given prime number p, but such that no counter of length p belongs to K̂.

Corollary 10.21 Let K be a class of finite mg-pairs. Then K̂ ⊇ MSol iff the following hold:

1. K̂ contains U_{1} and all counters.

2. For each (cyclic) group G of prime order, it holds that G|K.

Moreover, K̂ = MSol iff the above conditions hold and K ⊆ MSol.

More generally, we have:

Corollary 10.22 Let K be a class of finite mg-pairs and let S be a class of finite simple groups containing the cyclic groups of prime order and closed with respect to division. Then K̂ ⊇ M_{S} iff the following hold:

1. K̂ contains U_{1} and all counters.

2. For each G ∈ S it holds that G|K.

Moreover, K̂ = M_{S} iff the above conditions hold and K ⊆ M_{S}.

10.1 Mg-pairs with identity

Recall that an mg-pair (M, A) is termed an mgi-pair if the identity element of M belongs to A. For example, (Z_{n}, {a, 1}) is an mgi-pair, for each n ≥ 1, where a is a cyclic generator of Z_{n} and 1 is the identity.

Proposition 10.23 For each n, it holds that Z_{n} divides a direct power of (Z_{n}, {a, 1}).

Proof. Map each (n − 1)-tuple (a^{k_{1}}, …, a^{k_{n−1}}) in the direct power

(Z_{n}, {a, 1})^{n−1} = (Z_{n}^{n−1}, {a, 1}^{n−1})

to the element

a^{k_{1}}a^{2k_{2}} … a^{(n−1)k_{n−1}}

in Z_{n}. □

Proposition 10.24 Suppose that K is a class of finite mg-pairs and P is a set of prime numbers. Then K̂ ⊇ GSol_{P} iff for each prime number p ∈ P it holds that (Z_{p}, {a, 1}) ∈ K̂. Moreover, K̂ = GSol_{P} iff the above condition holds and K ⊆ GSol_{P}.

Proof. This follows from Proposition 10.23 and Corollary 10.3. □

Lemma 10.25 Suppose that S is a monoid and (M, A) is a finite mgi-pair. If S < M then there exists some n_{0} such that S|^{(n)}(M, A) holds for all n ≥ n_{0}. In particular, S|(M, A).

Proof. Since A is a set of generators for M, each element of M can be written as a product of elements of A. Let n_{0} be the maximum number of factors in such a representation for each element of M. Since the identity element is in A, it follows that each m ∈ M is the product of n generators, for every n ≥ n_{0}. Thus, M|^{(n)}(M, A). It follows that S|^{(n)}(M, A) for all monoids S with S < M. □

Lemma 10.26 Let K be a class of finite mgi-pairs. Then U_{1} ∈ K̂ iff \overline{K} contains a monoid which is not a group.

Proof. If U_{1} ∈ K̂, then, by the Krohn-Rhodes Theorem, it holds that U_{1} < \overline{K}. But this is possible only if \overline{K} contains a monoid which is not a group.

Suppose now that (M, A) is a finite mg-pair in K which is not a group. Then A contains the identity element 1. Moreover, since M is not a group and A generates M, there exists some a ∈ A such that a^{k} ≠ 1, for all k ≥ 1. Thus, U_{1} is a homomorphic image of the submonoid M′ of M generated by a. It follows that (U_{1}, U_{1}) is a homomorphic image of (M′, {a, 1}). This proves that U_{1} < K, so that U_{1} ∈ K̂. □

Lemma 10.27 Let K denote a class of finite mgi-pairs. The following conditions are equivalent.

1. There is a nontrivial counter (Z_{n}, {a}) with (Z_{n}, {a}) < K.

2. K̂ contains a nontrivial counter.

3. K̂ contains an infinite number of non-isomorphic counters.

Proof. We already know that the first and second conditions are equivalent (Corollary 10.12). The third condition clearly implies the second. To complete the proof we show that the first condition implies the third. Given that (Z_{n}, {a}) < K, where n > 1, also (Z_{n}, {a, 1}) < K, since K consists of mgi-pairs. Thus, by Proposition 10.24, (Z_{m}, {a}) ∈ K̂ for all integers m such that every prime divisor of m divides n. □

Proposition 10.28 Suppose that K is a class of finite mgi-pairs such that \overline{K} contains a monoid which is not a group and there is a nontrivial counter that divides an mg-pair in K. Then K̂ contains and mg-pair (M, A) iff every simple group divisor of M divides a monoid in \overline{K}.

Proof. By the Krohn-Rhodes Theorem, K̂ contains at most those finite mgpairs (M, A) such that every simple group divisor of M divides a monoid \overline{K}. In the rest of the proof, we show that every such mg-pair is in indeed in K̂.

By Lemma 10.26 we have U_{1} ∈ K̂. Consider now an arbitrary finite monoid M such that M < \overline{K}. By Lemma 10.25 there exist some n_{0} and (S, B) ∈ K such that M|^{(n)}(S, B) for all n ≥ n_{0}. Also, by Lemma 10.27, there exist an infinite number of counters in K̂ of pairwise different length. We conclude that for some n, both M|^{(n)}(S, B) and (Z_{n}, {a}) ∈ K̂ hold. Thus, by Proposition 10.14 and Proposition 8.3, (M, M) ∈ K̂. In particular, it follows that whenever G is a simple group with G < \overline{K}, then (G, G) ∈ K̂. Since also U_{1} ∈ K̂, it follows from the Krohn-Rhodes Theorem that K̂ contains every finite mg-pair (M, A) such that every simple group divisor of M divides a monoid in \overline{K}. □

Corollary 10.29 Suppose that K is a class of finite mgi-pairs. Then K̂ is the class of all finite mg-pairs iff the following hold:

1. \overline{K} contains a monoid which is not a group.

2. There is a nontrivial counter which divides an mg-pair in K.

3. K is group-complete.

Again, the above three conditions are independent.

Corollary 10.30 Suppose that S is a nonempty class of finite simple groups closed with respect to division. Let K be a class of finite mgi-pairs. Then K̂ ⊇ M_{S} iff the following hold:

1. \overline{K} contains a monoid which is not a group.

2. There is a nontrivial counter which divides an mg-pair in K.

3. G < K holds for each G ∈ S.

Moreover, K̂ = M_{S} iff the above conditions hold and K ⊆ M_{S}.

Corollary 10.31 For a class K of finite mgi-pairs, K̂ ⊇ A iff K contains a finite mgi-pair whose underlying monoid is not a group. Moreover, K̂ = A if this condition holds and K ⊆ A.

11 Completeness

Call a class L of regular languages Lindström-complete if Lin(L) is the class of all regular languages, and expressively complete if FO(L) is the class of all regular languages. Similarly, call a class K of finite mg-pairs Lindströmcomplete if Lin(K) is the class of all regular languages, and expressively complete if FO(K) is the class of all regular languages. In this section, we combine results from Section 9 and Section 10 to obtain characterizations of Lindström-complete and expressively complete classes. We will also include relative expressive completeness results.

In the following propositions, L denotes a class of regular languages and K a class of finite mg-pairs.

Lemma 11.1 If L is Lindström-complete then quotients are expressible in Lin(L) and Lin(L) admits relativization. If K is Lindsröm-complete, then Lin(K) admits relativization.

Proof. Since the second claim follows from the first one, we only prove the first. So assume that L is Lindström-complete. Then Lin(L) is the class of all regular languages which is closed with respect to quotients. Thus, by Corollary 4.6, quotients are expressible in Lin(L). Since K_{∃} ∈ Lin(L), by Corollary 6.3 Lin(L) admits relativization iff FO(L) does. But by Proposition 6.11, FO(L) admits relativization. □

Corollary 11.2 If L is expressively complete then quotients are expressible in FO(L) and FO(L) admits relativization. If K is expressively complete, then FO(K) admits relativization.

Lemma 11.3 Every finite mg-pair (M, A) divides a direct product of the syntactic mg-pairs of some regular languages recognizable by (M, A).

Proof. Consider the morphism h : (A^{∗}, A) → (M, A) which is the identity on A. For each m ∈ M, let (N_{m}, A_{m}) denote the syntactic mg-pair of h^{−1}(m). Then let (N, B) denote the image of (A^{∗}, A) under the target tupling η of the syntactic morphisms (A^{∗}, A) → (N_{m}, A_{m}), m ∈ M. Now (M, A) is a quotient of (N, B) under the map η(u) ↦ m iff u ∈ h^{−1}(m), for all u ∈ A^{∗} and m ∈ M. □

Theorem 11.4 A class K of finite mg-pairs is Lindström-complete iff Lin(K) admits relativization, K is group-complete and K̂ contains U_{1} and all counters. Moreover, K is expressively complete iff FO(K) admits relativization, K is group-complete and K̂ contains all counters.

Proof. Suppose that K is Lindström-complete. Then by Lemma 11.1, Lin(K) admits relativization. Thus, by Theorem 9.5, K̂ contains the syntactic mg-pair of every regular language. Thus, by Lemma 11.3, K̂ is the class of all finite mg-pairs. It follows now from the Krohn-Rhodes Theorem that K is group-complete.

Suppose now that Lin(K) admits relativization, moreover, K is groupcomplete and K̂ contains U_{1} and the counters. Then, by Corollary 10.17, K̂ is the class of all finite mg-pairs, and thus by Theorem 9.5, Lin(L) is the class of all regular languages.

Suppose next that K is expressively complete. By Corollary 11.2, FO(K) admits relativization. By Proposition 5.11, K_{1} = K ∪ {U_{1}} is Lindströmcomplete. Hence, K_{1} is group-complete and K̂_{1} contains the counters. Since U_{1} is aperiodic, it follows that K is group-complete. Since K̂_{1} contains the counters, it is not difficult to show that K̂ also contains the counters. (See also Remark 10.13.)

Finally, suppose that FO(K) admits relativization, K is group-complete, and K̂ contains the counters. Let K_{1} be defined as above. Then Lin(K_{1}) admits relativization, K_{1} is group-complete, and K̂_{1} contains U_{1} and the counters. Thus, FO(K) = Lin(K_{1}) is the class of all regular languages.

□

Corollary 11.5 A class L of regular languages is Lindström-complete iff the following hold.

1. Quotients are expressible in Lin(L).

2. Lin(L) admits relativization.

3. Every finite group divides the syntactic mg-pair of a language in L.

4. K̂_{L} contains U_{1} and the counters.

Proof. If L is Lindström-complete, then by Lemma 11.1, quotients are expressible in Lin(L). Moreover, if quotients are expressible in Lin(L), then, by Proposition 5.9, Lin(L) = Lin(K_{L}) and thus Lin(L) admits relativization iff Lin(K_{L}) does (cf. Proposition 6.2). Thus, our claim follows from Theorem 11.4. □

Corollary 11.6 A class L of regular languages is Lindström-complete iff the following hold.

1. Quotients are expressible in Lin(L).

2. Lin(L) admits relativization.

3. Every finite group divides the syntactic mg-pair of a language in L.

4. K_{∃} ∈ Lin(L), and for each n, the one-letter language (a^{n})^{∗} belongs to Lin(L).

Proof. This follows from Corollary 11.5 and Corollary 9.8 by noting that (U_{1}, U_{1}) is the syntactic mg-pair of K_{∃} and for each n, the syntactic mg-pair of (a^{n})^{∗} is a counter of length n. □

Corollary 11.7 A class L of regular languages is expressively complete iff the following hold.

1. Quotients are expressible in FO(L).

2. FO(L) admits relativization.

3. Every finite group divides the syntactic mg-pair of a language in L.

4. K̂_{L} (or K̂_{1}, where K_{1} = K_{L} ∪ {U_{1}}) contains the counters.

Corollary 11.8 A class L of regular languages is expressively complete iff the following hold.

1. Quotients are expressible in FO(L).

2. FO(L) admits relativization.

3. Every finite group divides the syntactic mg-pair of a language in L.

4. For each n, the one-letter language (a^{n})^{∗} belongs to FO(L) (or to Lin(L)).

Example 11.9 The class K presented in Example 10.19 is Lindström-complete. Thus there exists a Lindström-complete class of finite mg-pairs with two generators. Also, there exists a Lindström-complete class of two-letter regular languages. On the other hand, no class of mg-pairs with a single generator is group-complete, hence no such class is Lindström-complete, or expressively complete.

Corollary 11.10 There exists no finite Lindström-complete class of finite mg-pairs, or regular languages. Each Lindström-complete class of finite mgpairs contains an infinite number of mg-pairs with 2 or more generators. Also, any Lindström-complete class of regular languages contains an infinite number of languages over an alphabet with two or more letters.

This corollary is related to the main result of Beauquier, Rabinovitch [5].

Proposition 11.11 Suppose that S is a class of finite simple groups closed with respect to division and suppose that K is a class of finite mg-pairs.

1. Suppose that Lin(K) admits relativization. Then Lin(K) contains all regular languages whose syntactic monoid is in M_{S} iff K̂ contains (the mg-pairs corresponding to) U_{1} and the simple groups in S.

2. Lin(K) is the class of all regular languages whose syntactic monoid is in M_{S} iff Lin(K) admits relativization, each simple group divisor of the monoid component of any mg-pair in K is in S, and K̂ contains (the mg-pairs corresponding to) U_{1} and the simple groups in S.

3. If FO(K) admits relativization, then FO(K) contains all regular languages whose syntactic monoid is in M_{S} iff K̂_{1} contains (the mg-pairs corresponding to) the simple groups in S, where K_{1} = K ∪ {U_{1}}.

4. FO(K) is the class of all regular languages whose syntactic monoid is in M_{S} iff FO(K) admits relativization and each simple group divisor of the monoid component of any mg-pair in K is in S and K̂_{1} contains (the mg-pairs corresponding to) the simple groups in S, where K_{1} = K ∪ {U_{1}}.

Proof. We only prove the first two claims. Assume that Lin(K) admits relativization. Then, by Theorem 9.5, a language belongs to Lin(K) iff its syntactic mg-pair is in K̂. Given a finite group G, let h denote the morphism h : (G^{∗}, G) → (G, G) which is the identity mapping on G. It is not difficult to show that the syntactic mg-pair of the language h^{−1}(1) is isomorphic to (G, G). Thus, if Lin(K) contains all languages whose syntactic monoid is in M_{S}, and if G ∈ S, then K̂ contains (G, G). Since the syntactic mgpair of the language K_{∃} is isomorphic to (U_{1}, U_{1}) and thus aperiodic, it follows that (U_{1}, U_{1}) is also in K̂. Conversely, if K̂ contains S and U_{1}, then M_{S} ⊆ K̂. Thus, by Theorem 9.5, Lin(K) contains all regular languages whose syntactic monoid is in M_{S}.

As for the second claim, assume that Lin(K) is the class of all (regular) languages whose syntactic mg-pair is in M_{S}. Then, by Theorem 3.5, Lin(K) = Lin(M_{S}). Now by Corollary 6.9, Lin(M_{S}) admits relativization.

Thus, by Proposition 6.2, Lin(K) also admits relativization. Thus, by the first claim, K̂ contains U_{1} and the mg-pair corresponding to each group G ∈ S. Moreover, by Theorem 9.5, every simple group divisor of \overline{K} belongs to S. Conversely, if this holds and if Lin(K) admits relativization, then again by the first claim, Lin(K) contains every language whose syntactic mg-pair is in M_{S}. Moreover, by Theorem 9.5 and the Krohn-Rhodes Theorem, it does not contain any other language. □

Proposition 11.12 Suppose that K̂ contains U_{1} and the counters, and has the following property: For every simple group G, if G < \overline{K} then G|K. Suppose that Lin(K) admits relativization. Then a language L is in Lin(K) iff every simple group divisor of the syntactic monoid of L divides K.

Proof. By Corollary 10.16, K̂ = M_{S}, where S is the class of all simple groups G with G < K. Thus, the result follows from Theorem 9.5. □

Proposition 11.13 Suppose that S is a class of finite simple groups closed with respect to division containing all cyclic groups of prime order. Moreover, suppose that K is a class of finite mg-pairs.

1. If Lin(K) admits relativization then Lin(K) contains all regular languages whose syntactic monoid is in M_{S} iff K̂ contains U_{1} and the counters, and for each finite simple group G in S it holds that G|K.

2. Lin(K) is the class of all regular languages whose syntactic monoid is in M_{S} iff Lin(K) admits relativization, K̂ contains U_{1} and the counters, and for every finite simple group G it holds that G ∈ S iff G|K.

3. If FO(K) admits relativization then FO(K) contains all regular languages whose syntactic monoid is in M_{S} iff K̂ contains the counters and for each simple group G in S it holds that G|K.

4. FO(K) is the class of all regular languages whose syntactic monoid is in M_{S} iff FO(K) admits relativization, K̂ contains the counters, and for every finite simple group G it holds that G ∈ S iff G|K.

Proof. From Proposition 11.11 and Corollary 10.22. □

Without proof we mention:

Proposition 11.14 Suppose that S is a class of finite simple groups closed with respect to division. If Lin(K) admits relativization then Lin(K) contains all regular languages whose syntactic monoid is in G_{S} iff K̂ contains (the mg-pairs corresponding to) the simple groups in S. Moreover, Lin(K) is the class of all regular languages whose syntactic monoid is in G_{S} iff Lin(K) admits relativization, K̂ contains (the mg-pairs corresponding to) the simple groups in S, and K ⊆ G_{S}.

If Lin(K) admits relativization then Lin(K) contains all regular languages whose syntactic monoid is in M_{S} iff K̂ contains U_{1} and the simple groups in S. Moreover, Lin(K) is the class of all regular languages whose syntactic monoid is in M_{S} iff Lin(K) admits relativization, K̂ contains U_{1} and the simple groups in S, moreover, K ⊆ M_{S}.

By taking S to be the class of all cyclic groups of prime order, from Proposition 11.13 we obtain:

Proposition 11.15 1. If Lin(K) admits relativization then Lin(K) contains all regular languages whose syntactic monoid is in MSol iff K̂ contains U_{1} and the counters, and for every prime number p it holds that Z_{p}|K. Moreover, Lin(K) is the class of all regular languages whose syntactic monoid is in MSol iff Lin(K) admits relativization, K ⊆ MSol, K̂ contains U_{1} and the counters, and for every prime number p it holds that Z_{p}|K.

2. If FO(K) admits relativization then FO(K) contains all regular languages whose syntactic monoid is in MSol iff K̂ contains the counters, and for every prime number p it holds that Z_{p}|K. Moreover, FO(K) is the class of all regular languages whose syntactic monoid is solvable iff FO(K) admits relativization, K ⊆ MSol, K̂ contains the counters, and for every prime number p it holds that Z_{p}|K.

Proposition 11.16 Let P denote a set of prime numbers. If Lin(K) admits relativization then Lin(K) contains all regular languages whose syntactic monoid is in GSol_{P} iff for every prime number p ∈ P it holds that (Z_{p}, {a, 1}) ∈ K̂). Moreover, Lin(K) is the class of all regular languages whose syntactic monoid is in GSol_{P} iff Lin(K) admits relativization, K ⊆ GSol_{P}, and for every prime number p ∈ P it holds that (Z_{p}, {a, 1}) ∈ K̂).

Proof. This follows from Proposition 11.14 and Proposition 10.24. □

We also have:

Proposition 11.17 Suppose that P is a set of prime numbers.

1. Lin(K) is the class of all regular languages whose syntactic monoid is in MSol_{P} iff Lin(K) admits relativization, K ⊆ MSol_{P}, moreover, U_{1} ∈ K̂ and (Z_{p}, {a, 1}) ∈ K̂, for all p ∈ P.

2. FO(K) is the class of all regular languages whose syntactic monoid is in MSol_{P} iff FO(K) admits relativization, K ⊆ MSol_{P}, moreover, (Z_{p}, {a, 1}) ∈ K̂_{1}, for all p ∈ P, where K_{1} = K ∪ {U_{1}}.

In particular, when P is empty, we have:

Proposition 11.18 Lin(K) = FO iff Lin(K) admits relativization, U_{1} ∈ K̂, and K ⊆ A.

We now translate some of the above results to classes L of regular languages.

Corollary 11.19 Suppose that S is a class of finite simple groups closed with respect to division and suppose that L is a class of regular languages.

1. Suppose that Lin(L) admits relativization and quotients are expressible in Lin(L). Then Lin(L) contains all regular languages whose syntactic monoid is in M_{S} iff K̂_{L} contains (the mg-pairs corresponding to) U_{1} and the simple groups in S.

2. Lin(L) is the class of all regular languages whose syntactic monoid is in M_{S} iff Lin(L) admits relativization, quotients are expressible in Lin(L), each simple group divisor of the monoid component of any mg-pair in K_{L} is in S, and K̂_{L} contains (the mg-pairs corresponding to) U_{1} and the simple groups in S.

3. If FO(L) admits relativization and quotients are expressible in FO(L), then FO(L) contains all regular languages whose syntactic monoid is in M_{S} iff K̂_{1} contains (the mg-pairs corresponding to) the simple groups in S, where K_{1} = K_{L} ∪ {U_{1}}.

4. FO(L) is the class of all regular languages whose syntactic monoid is in M_{S} iff FO(L) admits relativization, quotients are expressible in FO(L), each simple group divisor of the monoid component of any mgpair in K_{L} is in S, and K̂_{1} contains (the mg-pairs corresponding to) the simple groups in S, where K_{1} = K_{L} ∪ {U_{1}}.

Corollary 11.20 Suppose that S is a class of finite simple groups closed with respect to division containing all cyclic groups of prime order. Moreover, suppose that L is a class of regular languages.

1. If Lin(L) admits relativization and quotients are expressible in Lin(L) then Lin(L) contains all regular languages whose syntactic monoid is in M_{S} iff K̂_{L} contains U_{1} and the counters, and for each finite simple group G in S it holds that G|K_{L}.

2. Lin(L) is the class of all regular languages whose syntactic monoid is in M_{S} iff Lin(K) admits relativization, quotients are expressible in Lin(L), K̂_{L} contains U_{1} and the counters, and for every finite simple group G it holds that G ∈ S iff G|K_{L}.

3. If FO(L) admits relativization and quotients are expressible in FO(L) then FO(L) contains all regular languages whose syntactic monoid is in M_{S} iff K̂_{L} contains the counters and for each simple group G in S it holds that G|K_{L}.

4. FO(L) is the class of all regular languages whose syntactic monoid is in M_{S} iff FO(K) admits relativization, quotients are expressible in FO(L), K̂ contains the counters, and for every finite simple group G it holds that G ∈ S iff G|K_{L}.

Corollary 11.21 1. If Lin(L) admits relativization and quotients are expressible in Lin(L) then Lin(L) contains all regular languages whose syntactic monoid is in MSol iff K̂_{L} contains U_{1} and the counters, and for every prime number p it holds that Z_{p}|K_{L}. Moreover, Lin(L) is the class of all regular languages whose syntactic monoid is in MSol iff Lin(L) admits relativization, quotients are expressible in Lin(L), K_{L} ⊆ MSol, K̂_{L} contains U_{1} and the counters, and for every prime number p it holds that Z_{p}|K_{L}.

2. If FO(L) admits relativization and quotients are expressible in FO(L) then FO(L) contains all regular languages whose syntactic monoid is in MSol iff K̂_{L} contains the counters, and for every prime number p it holds that Z_{p}|K_{L}. Moreover, FO(L) is the class of all regular languages whose syntactic monoid is solvable iff FO(L) admits relativization, quotients are expressible in FO(L), K_{L} ⊆ MSol, K̂_{L} contains the counters, and for every prime number p it holds that Z_{p}|K_{L}.

Corollary 11.22 Suppose that P is a set of prime numbers.

1. If Lin(L) admits relativization and quotients are expressible in Lin(L), then Lin(L) contains all regular languages whose syntactic monoid is in MSol_{P} iff K̂_{L} contains U_{1} and the mgi-pairs Z_{p}^{1} = (Z_{p}, {a, 1}), where p is any prime in P. Moreover, Lin(L) is the class of all regular languages whose syntactic monoid is in MSol_{P} iff the syntactic monoid of each language in L belongs to MSol_{P}, Lin(L) admits relativization, quotients are expressible in Lin(L), and the above conditions hold.

2. If FO(L) admits relativization and quotients are expressible in FO(L), then FO(L) contains all regular languages whose syntactic monoid is in MSol_{P} iff K̂_{1} contains the mgi-pairs Z_{p}^{1} = (Z_{p}, {a, 1}), where p is any prime in P and K_{1} = K_{L} ∪ {U_{1}}. Moreover, FO(L) is the class of all regular languages whose syntactic monoid is in MSol_{P} iff the syntactic monoid of each language in L belongs to MSol_{P}, FO(L) admits relativization, quotients are expressible in FO(L), and the above condition holds.

Corollary 11.23 Suppose that P is a set of prime numbers. If Lin(L) admits relativization and quotients are expressible in Lin(L), then Lin(L) contains all regular languages whose syntactic monoid is in GSol_{P} iff K̂_{L} contains the mgi-pairs Z_{p}^{1} = (Z_{p}, {a, 1}), where p is any prime in P. Moreover, Lin(L) is the class of all regular languages whose syntactic monoid is in GSol_{P} iff the syntactic monoid of each language in L belongs to GSol_{P}, Lin(L) admits relativization and quotients are expressible in Lin(L), and the above condition holds.

Corollary 11.24 Lin(L) = FO iff Lin(L) admits relativization, quotients are expressible in Lin(L), U_{1} ∈ K̂_{L} and the syntactic monoid of each language in L is aperiodic.

11.1 Completeness and padding

Our characterizations become simpler when K is a class of mgi-pairs that we assume in the rest of this section. We only present three results and skip the proofs that use Corollaries 10.29, 10.30 and 10.31. So let K denote a class of mgi-pairs.

Proposition 11.25

1. K is Lindström-complete iff K is group-complete, contains an mgi-pair whose underlying monoid is not a group, moreover, there exists some n > 1 with (Z_{n}, {a}) < K.

2. K is expressively complete iff K is group-complete and there exists some n > 1 with (Z_{n}, {a}) < K.

Proposition 11.26 Suppose that S is a nonempty class of simple groups closed with respect to division.

1. Lin(K) contains the regular languages whose syntactic monoids are in M_{S} iff for each G ∈ S it holds that G < K, moreover, K contains an mgi-pair whose underlying monoid is not a group and there exists some n > 1 with (Z_{n}, {a}) < K. Further, Lin(K) is the class of all regular languages whose syntactic monoid is in M_{S} iff the above conditions hold and \overline{K} ⊆ M_{S}.

2. FO(K) contains the regular languages whose syntactic monoids are in M_{S} iff for each G ∈ S it holds that G < K and there exists some n > 1 with (Z_{n}, {a}) < K. Further, Lin(K) is the class of all regular languages whose syntactic monoid is in M_{S} iff the above conditions hold and \overline{K} ⊆ M_{S}.

Proposition 11.27 Lin(K) ⊇ FO iff K contains an mgi-pair whose monoid component is not a group.

In the next three corollaries, we assume that L is closed with respect to quotients and padding.

Corollary 11.28

1. L is Lindström-complete iff every (non-abelian simple) group divides the syntactic monoid of some language in L, moreover, L contains a language whose syntactic monoid is not a group, and there is some n > 1 such that the one-letter language (a^{n})^{∗} is the inverse image of a language in L under a literal homomorphism.

2. L is expressively complete iff every (non-abelian simple) group divides the syntactic monoid of some language in L, moreover, there is some n > 1 such that the one-letter language (a^{n})^{∗} is the inverse image of a language in L under a literal homomorphism.

Corollary 11.29 Suppose that S is a nonempty class of simple groups closed with respect to division.

1. Lin(L) contains the regular languages whose syntactic monoids are in M_{S} iff for each G ∈ S it holds that G < K_{L}, moreover, K_{L} contains an mgi-pair whose underlying monoid is not a group and there exists some n > 1 such that (a^{n})^{∗} is the inverse image of a language in L under a literal homomorphism. Further, Lin(L) is the class of all regular languages whose syntactic monoid is in M_{S} iff the above conditions hold and \overline{K}_{L} ⊆ M_{S}.

2. FO(L) contains the regular languages whose syntactic monoids are in M_{S} iff for each G ∈ S it holds that G < K_{L} and there exists some n > 1 such that (a^{n})^{∗} is the inverse image of a language in L under a literal homomorphism. Further, Lin(L) is the class of all regular languages whose syntactic monoid is in M_{S} iff the above conditions hold and \overline{K}_{L} ⊆ M_{S}.

Corollary 11.30 Lin(L) ⊇ FO iff L contains a language whose syntactic monoid is not a group.

12 Further work

Extensions of the main result to other structures including ω-words, ordinal words, words over discrete linear orders and trees will be considered in subsequent papers.

13 Acknowledgment

Most of the results of this paper were obtained during the first author’s visit at BRICS and the Department of Computer Science of Aalborg University. He is indebted to members of these institutions for their hospitality. The present version of the paper was completed during the first author’s visit as a JSPS fellow at Kyoto Sangyo University. This author would like to thank Masami Ito for his very kind hospitality.

Both authors would like to thank Prof. John L. Rhodes for communicating to them an outline of the argument that proves Proposition 8.3 for varieties of finite monoids. In the Appendix, we have modified this argument for varieties of mg-pairs.

References

[1] M. A. Arbib, Ed.: Algebraic Theory of Machines, Languages, and Semigroups, With a major contribution by Kenneth Krohn and John L. Rhodes, Academic Press, 1968.

[2] D. A. Mix Barrington, K. Compton, H. Straubing and D. Therien: Regular languages in NC^{1}, J. Computer and System Sciences, 44(1992), no. 3, 478–499.

[3] D. Barrington, N. Immerman and H. Straubing: On uniformity within NC^{1}, J. Computer System Science, 41(1990), 274–306.

[4] A. Baziramwabo, P. McKenzie and D. Therien: Modular temporal logic, in: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, 1999, IEEE Computer Society, 344–351.

[5] D. Beauquier and A. Rabinovitch: Monadic logic of order over naturals has no finite base, Journal of Logic and Computation, to appear.

[6] J. R. Büchi: Weak second order logic and finite automata, Zeit. Math. Logik Grund. Math., 6(1960), 66–92.

[7] H.-J. Burtschick and H. Vollmer: Lindström quantifiers and leaf language definability, International J. of Foundations of Computer Science, 9(1998), 277-294.

[8] J. Cohen, D. Perrin, J.-E. Pin: On the expressive power of temporal logic, J. Computer and System Sciences, 46(1993), 271–294.

[9] P. Dömösi and Z. Ésik: Critical classes for the α_{0}-product, Theoret. Comput. Sci., 61(1988), 17–24.

[10] H.-J. Ebbinghaus and J. Flum: Finite Model Theory, 2nd. ed., Springer, 1999.

[11] S. Eilenberg: Automata, Languages, and Machines, vol. A and B, Academic Press, 1974, 1976.

[12] C. Elgot: Decision problems of finite automata design and related arithmetics, Trans. Amer. Math. Soc., 98(1961), 21–51.

[13] Z. Ésik: Results on homomorphic realization of automata by α_{0}- products, Theoret. Comput. Sci., 87(1991), 229–249.

[14] Z. Ésik and M. Ito: Temporal logic with cyclic counting and the degree of aperiodicity of finite automata, 16(2003), 1–28.

[15] M. Galota, H. Vollmer: A generalization of the Büchi–Elgot– Trakhtenbrot theorem, in: Computer Science Logic, 15th International Workshop, CSL 2001, Paris, 2001, LNCS 2142, Springer, 355–368.

[16] N. Immerman: Descriptive Complexity, Graduate Texts in Computer Science, Springer-Verlag, New York, 1999.

[17] K. Krohn and J. Rhodes: Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines, Trans. Amer. Math. Soc., 116(1965), 450–464.

[18] C. Lautemann, P. McKenzie and Th. Schwentick: The descriptive complexity approach to LOGCFL, J. Computer System Science, 62(2001), 629–652.

[19] P. Lindström: First order predicate logic with generalized quantifiers. Theoria, 32(1966), 186–195.

[20] P. McKenzie, Th. Schwentick, D. Therien, H. Vollmer: The many faces of a translation, in: Automata, Languages and Programming, 27th International Colloquium, ICALP’00 LNCS 1853, 890–901.

[21] W. D. Maurer and J. L. Rhodes: A property of finite simple non-abelian groups, Proc. Amer. Math. Soc., 16(1965), 552–554.

[22] R. McNaughton and S. Papert: Counter-Free Automata, MIT Press, 1971.

[23] T. Peichl and H. Vollmer: Finite automata with generalized acceptance criteria, in: Automata, Languages and Programming, 26th International Colloquium, ICALP’99, Prague, LNCS 1644, Springer, 605-614.

[24] J.-E. Pin: Varieties of Formal Languages, Plenum, 1986.

[25] J.-E. Pin: Logic, semigroups and automata on words, Ann. Math. Artificial Intelligence, 16(1996), 343–384.

[26] A. Pnueli: The temporal logic of programs, in: 18th IEEE Symp. Foundations of Computer Science, Providence, 1977, 46–57.

[27] J. Rhodes: Undecidability, automata, and pseudovarieties of finite semigroups, Int. J. of Algebra and Computation,, 9(1999), 455–473.

[28] J. Rhodes and B. Tilson: The kernel of monoid morphisms, J. Pure and Appl. Alg., 62(1989), 227–268.

[29] M. P. Schützenberger: On finite monoids having only trivial subgroups, Information and Control, 8(1965), 190–194.

[30] H. Straubing: Families of recognizable sets corresponding to certain varieties of finite monoids, J. Pure Appl. Algebra, 15(1979), 305–318.

[31] H. Straubing: Finite Automata, Formal Logic, and Circuit Complexity, Birkhauser, 1994.

[32] H. Straubing: On logical descriptions of regular languages, in: LATIN 2002, LNCS 2286, Springer, 2002, 528–538.

[33] H. Straubing, D. Therien: Regular languages defined with a bounded number of variables, in: STACS 2001, LNCS 2010, Springer, 2001, 555–562.

[34] H. Straubing, D. Therien and W. Thomas: Regular languages defined with generalized quantifiers, Automata, languages and programming (Tampere, 1988), Lecture Notes in Comput. Sci., 317, Springer, Berlin, 1988, 561–575.

[35] H. Straubing, D. Therien and W. Thomas: Regular languages defined with generalized quantifiers, Information and Computation, 118(1995), 289–301.

[36] D. Therien: Classification of finite monoids: The language approach, Theoretical Computer Science, 14(1981), 195-208.

[37] D. Therien and Th. Wilke: Temporal logic and semidirect products: An effective characterization of the until hierarchy, in: 37th Annual Symposium on Foundations of Computer Science, FOCS ’96, Burlington, IEEE Computer Society, 1996, 256-263.

[38] W. Thomas: Automata on infinite objects, in: Handbook of Theoretical Computer Science, Vol. B, Elsevier, Amsterdam, 1990, 133–191.

[39] W. Thomas: Languages, automata, and logic, in: Handbook of Formal Languages, Vol. 3, Springer, 1997, 389–455.

[40] B. A. Trakhtenbrot: Finite automata and logic of monadic predicates, Doklady Akademii Nauk SSSR, 140(1961), 326–329.

[41] J. Väänänen (Ed.): Generalized Quantifiers and Computation, LNCS 1754, Springer, 1997.

Appendix

In this appendix, we prove Proposition 8.3. The argument is an adaptation of the proof of the corresponding fact for monoid varieties, communicated to the authors by John Rhodes. In this section, by a monoid or category we will always mean a finite monoid, or category, respectively.

First, we recall from Rhodes, Tilson [28] the notion of the kernel K_{φ} of a monoid morphism φ : M → N. It is a category constructed as a quotient of category W_{φ} defined as follows. The objects of W_{φ} are all ordered pairs n = (n_{L}, n_{R}) of elements n_{L}, n_{R} in the image φ(M) of M. (We will follow the convention of [28] that if a boldface letter x denotes a pair of elements of a monoid, then x_{L} and x_{R} are the left and right hand components of this pair.) An arrow n → n′ of W_{φ} takes the form (n_{L}, (m, n), n′_{R}), where m ∈ M, n ∈ N with n = φ(m) are such that n_{L}n = n′_{L} and nn′_{R} = n_{R}. (Thus, we could as well just write (n_{L}, m, n′_{R}), but we want to keep the notation consistent with that of [28]. The reason for the more complex notation of [28] is due to the fact that the kernel construction also applies to relational morphisms φ of monoids, whereas in this paper we only consider the particular case when φ is a function.) Note that n_{R} and n′_{L} and thus n and n′ can be recovered from the notation (n_{L}, (m, n), n′_{R}). Below we will sometimes just write (m, n) for (n_{L}, (m, n), n′_{R}) when there is no danger of confusion. The composite of consecutive arrows (n_{L}, (m, n), n′_{R}) : n → n′ and (n′_{L}, (m′, n′), n′′_{R}) : n′ → n′′ is defined as (n_{L}, (mm′, nn′), n′′_{R}). Note that the identity arrows of W_{φ} take the form (n_{L}, (1, 1), n_{R}). Each arrow (n_{L}, (m, n), n′_{R}) induces a function

[n_{L}, (m, n), n′_{R}] : φ^{−1}(n_{L}) × φ^{−1}(n′_{R}) → M
(m_{L}, m_{R}) ↦ m_{L}mm_{R}.

The relation that identifies any two parallel arrows inducing the same function is shown to be a (category) congruence in [28]. The kernel K_{φ} is then defined as the quotient of W_{φ} with respect to this congruence. Following [28], we will denote a morphism of K_{φ} as [n_{L}, (m, n), n′_{R}], or just [m, n].

Suppose now that (M, A) and (N, B) are mg-pairs and φ is a morphism (M, A) → (N, B), so that φ is also a monoid homomorphism M → N. Then we define the kernel of φ to be the pair (K_{φ}, A_{φ}), where K_{φ} is the category constructed above, and where A_{φ} is a distinguished collection of morphisms of K_{φ}: it consists of those morphisms [a, b] of K_{φ} with a ∈ A. Since b = φ(a), and since φ is a morphism of mg-pairs, it follows that b ∈ B. Since A is a generating set of M and φ preserves the generators, it follows that (K_{φ}, A_{φ}) is a category equipped with a distinguished set of generators, or cg-pair: each arrow of K_{φ} is either an identity arrow or the composite of some arrows in A_{φ}.

Suppose that K is a category, N is a monoid, and φ is a relation from the arrows of K to N, viewed as a function from the arrows of K to the set of all subsets of N. We say that φ is a covering K → N if the following conditions hold:

• φ(m)φ(m′) ⊆ φ(mm′), for all composable arrows m, m′.

• For all identity arrows e it holds that 1 ∈ φ(e).

• For all arrows m it holds that φ(m) ≠ ∅.

• For all m, m′, if m ≠ m′ then φ(m) ∩ φ(m′) = ∅.

When K and N are equipped with distinguished sets of generators, i.e., when (K, A) is a cg-pair and (N, B) is an mg-pair, then a covering φ : (K, A) → (N, B) also satisfies that for each a ∈ A there is some b ∈ B with b ∈ φ(a). Since A is a set of generators, the third condition above becomes redundant. Note that each covering φ : (K, A) → (N, B) contains a covering φ′ such that whenever n ∈ φ′(m), it holds that either m is an identity arrow and n = 1, or there exist a_{1}, …, a_{k} ∈ A, b_{1}, …, b_{k} ∈ B, k ≥ 1 with b_{1} ∈ φ(a_{1}), …, b_{k} ∈ φ(a_{k}) such that m is the composite a_{1} … a_{k} and n is b_{1} … b_{k}. The above definition also applies to one object categories K which may conveniently be identified with their hom-sets. In that case the concept reduces to the notion of covering defined earlier in Section 5. Note that each injective morphism (M, A) → (N, B) is a covering (M, A) → (N, B), moreover, the relational inverse of each surjective morphism (M, A) → (N, B) is a covering (N, B) → (M, A), i.e., in the opposite direction.

The notion of covering can be generalized to a pair of categories, and in fact to cg-pairs. Given categories K and K′, a covering φ : K → K′ assigns an object to each object of K, a set φ(m) of morphisms of K′ to each morphism m of K, compatible with the object map, such that the obvious analogies of the above conditions hold. A covering φ : (K, A) → (K′, B) between cg-pairs (K, A) and (K′, B) also satisfies that for each arrow a ∈ A there is an arrow b ∈ B with b ∈ φ(a). The composite of two coverings is defined in the expected way.

Lemma 13.1 The composite of coverings ψ : K → K′ and ψ′ : K′ → K′′ is a covering K → K′′. Similarly, if ψ : (K, A) → (K′, A′) and ψ′ : (K′, A′) → (K′′, A′′) are coverings, then the composite of ψ with ψ′ is a covering K → K′′.

The notion of covering is related to the double semidirect product by the Kernel Theorem of Rhodes, Tilson [28], also known as the Covering Lemma. We need a version of this result.

Theorem 13.2 Let φ : (M, A) → (N, B) be a morphism of mg-pairs, and let (V, C) be an mg-pair satisfying (K_{φ}, A_{φ}) < (V, C). Then (M, A) < (V, C)□(N, B).

Proof. We follow the argument given in the proof of the Kernel Theorem (Theorem 7.4) in Rhodes, Tilson [28]. Let ψ : (K_{φ}, A_{φ}) → (V, C) be a covering. For each pair m ∈ M, n ∈ N with n ∈ φ(m), define

F (m, n) = {f ∈ V^{N×N} : f(n_{1}, n_{2}) ∈ ψ([n_{1}, (m, n), n_{2}]), n_{1}, n_{2} ∈ φ(M)}.

Then let the relation θ : M → V □N be defined by

θ(m) = {(f, n) : n ∈ φ(m), f ∈ F (m, n)}.

It is shown in [28] that θ is a covering M → V □N. For each m ∈ M let θ′(m) = θ(m)∩W, where W denotes the monoid component of (V, C)□(N, B), i.e., (V, C)□(N, B) = (W, C^{N×N} × B). If we can show that for each a ∈ A there is some b ∈ B and f ∈ C^{N×N} with (f, b) ∈ θ(a), then, using the fact that W is a submonoid of V □N, it follows that θ′ is a covering (M, A) → (V, C)□(N, B). Given a, let b = φ(a). Since ψ is a covering (K_{φ}, A_{φ}) → (V, C), for each n_{1}, n_{2} ∈ φ(M) there is some c ∈ C with c ∈ ψ([n_{1}, (a, b), n_{2}]). So let f map each pair (n_{1}, n_{2}) ∈ φ(M)^{2} to such a c, and let f(n_{1}, n_{2}) be an arbitrary element of C if n_{1} or n_{2} is not in φ(M).

□

Suppose now that (M, A)⋆⋆(T, C) and (N, B)⋆⋆(T, C) are double semidirect products so that T acts on M and on N on the left and on the right. Following Rhodes Tilson [28], we say that these actions are compatible with a morphism φ : (M, A) → (N, B) if for all m ∈ M, n ∈ N and t ∈ T, if φ(m) = n then φ(tm) = tn and φ(mt) = nt. In this case we define a morphism

φ⋆⋆(T, C) : (M, A)⋆⋆(T, C) → (N, B)⋆⋆(T, C)
(m, t) ↦ (φ(m), t).

The reader should have no difficulty to check that φ⋆⋆(T, C) is indeed a morphism. In the same way, we define

φ⋆⋆T : M⋆⋆T → N⋆⋆T
(m, t) ↦ (φ(m), t),

where M⋆⋆T and N⋆⋆T are respectively the double semidirect products of M and N with T determined by the actions.

Proposition 13.3 Under the previous assumptions, if the actions of T on M and on N are compatible with φ, then

(K_{φ⋆⋆(T,C)}, A_{φ⋆⋆(T,C)}) < (K_{φ}, A_{φ}).

Proof. In the proof of Rhodes and Tilson [28], Theorem 6.2, it is shown that K_{φ⋆⋆T} < K_{φ}. This is achieved by mapping each object (n, t) of K_{φ⋆⋆T} to the object (n_{L}t_{R}, t_{L}n_{R}) of K_{φ}, and by relating each arrow

[(m, t), (n, t)] : (n, t) → (n′, t′)

in K_{φ⋆⋆T} to

[t_{L}mt′_{R}, t_{L}nt′_{R}] : (n_{L}t_{R}, t_{L}n_{R}) → (n′_{L}t′_{R}, t′_{L}n′_{R}).

Note that when m ∈ A (and thus by φ(m) = n, also n ∈ B), then t_{L}mt′_{R} ∈ A and t_{L}nt′_{R} ∈ B. Let ψ denote this covering. By Lemma 13.4 and its proof, there is a covering

ρ : K_{φ⋆⋆(T,C)} → K_{φ⋆⋆T}

which is the identity on objects and relates a morphism [(a, c), (b, c)] in K_{φ⋆⋆(T,C)}, where a ∈ A, b ∈ B and c ∈ C, with the corresponding morphism [(a, c), (b, c)] in K_{φ⋆⋆T}. The composite of the two coverings ρ and ψ is the required covering. □

Lemma 13.4 Suppose that φ is a homomorphism M → N, M′ is a submonoid of M, and N′ is a submonoid of N such that the restriction of φ to M is a homomorphism M′ → N′. Then K_{φ′} < K_{φ}.

This is proved in Rhodes and Tilson [28], Corollary 5.4. It is clear that every object of K_{φ′} is an object of K_{φ}. It is shown in [28] that the relation that is the identity function on objects and relates each morphism [(m, n)] in K_{φ′} with the morphism [(m, n)] in K_{φ} is a covering.

We let ¯1 denote a trivial monoid ¯1 = {1}. Thus, (¯1, {1}) is a trivial mg-pair.

Proposition 13.5 Let (M, A) denote an mg-pair and let φ denote the unique (collapsing) morphism (M, A) → (¯ 1, {1}). Then

(K_{φ}, A_{φ}) < (M, A).

Proof. The relation that relates each arrow [1, (m, 1), 1] with m is a covering. □

Corollary 13.6 Suppose that (M, A)⋆⋆(N, B) is a double semidirect product. Let π denote the projection (M, A)⋆⋆(N, B) → (N, B), (m, n) ↦ n. Then (K_{π}, A_{π}) < (M, A).

Proof. The projection π is (essentially) φ⋆⋆(N, C), where φ denotes the collapsing morphism (M, A) → (¯1, {1}). (Note that φ is compatible with any actions.) Thus, the result follows from Propositions 13.5 and Proposition 13.3. □

Given a double semidirect product ((M, A)⋆⋆(N, B))⋆⋆(T, C), where we denote (M, A)⋆⋆(N, B) = (V, A × B), we say that the actions of T (on V) are pointwise if there exist left and right actions of T on M and on N such that

t(m, n) = (tm, tn)
(m, n)t = (mt, nt),

for all (m, n) ∈ V and t ∈ T. It follows that the left and right actions of T on N are compatible and determine a double semidirect product (N, B)⋆⋆(T, C).

Lemma 13.7 Suppose that ((M, A)⋆⋆(N, B))⋆⋆(T, C) is a double semidirect product of finite mg-pairs such that the actions of T are pointwise and thus determine a double semidirect product (N, B)⋆⋆(T, C). Then the actions of T on (M, A)⋆⋆(N, B) and on (N, B) are compatible with the projection morphism π : (M, A)⋆⋆(N, B) → (N, B).

Proof. Immediate from the definitions. □

Proposition 13.8 Suppose that V_{1}, V_{2} and V_{3} are varieties of finite mgpairs. Then an mg-pair is in (V_{1}⋆⋆V_{2})⋆⋆V_{3} iff it divides a semidirect product

((M, A)⋆⋆(N, B))⋆⋆(T, C)

such that (M, A) ∈ V_{1}, (N, B) ∈ V_{2}, (T, C) ∈ V_{3} and the actions of T are pointwise.

Proof. One direction is trivial. Suppose now that (S, D) is in (V_{1}⋆⋆V_{2})⋆⋆V_{3}. Then, by Proposition 8.1, (S, D) divides a block product

((M, A)□(N, B))□(T, C)

which is a double semidirect product

((M, A)^{N×N}⋆⋆(N, B))^{T ×T} ⋆⋆(T, C)

with suitable actions. This double semidirect product is in turn isomorphic to a double semidirect product

((M, A)^{N×N×T ×T} ⋆⋆(N, B)^{T ×T})⋆⋆(T, C),

where the actions of T are given by

t(f, g) = (f′, g′)
(f, g)t = (f′′, g′′),

where

f′(n_{1}, n_{2}, t_{1}, t_{2}) = f(n_{1}, n_{2}, t_{1}t, t_{2})
g′(t_{1}, t_{2}) = g(t_{1}t, t_{2}),

and similarly for f′′ and g′′. Since f′ does not depend on g and g′ does not depend on f, the left action is pointwise. Likewise the right action. Now let

(M′, A′) = (M, A)^{N×N×T ×T}
(N′, B′) = (N, B)^{T ×T} .

We have that (S, D) divides a double semidirect product

((M′, A′)⋆⋆(N′, B′))⋆⋆(T, C)

such that the actions of T are pointwise. Since varieties are closed with respect to the direct product, we have (M′, A′) ∈ V_{1} and (N′, B′) ∈ V_{2}.

□

We now complete the proof of Proposition 8.3. We want to prove that for all varieties of finite mg-pairs V_{1}, V_{2} and V_{3},

(V_{1}⋆⋆V_{2})⋆⋆V_{3} ⊆ V_{1}⋆⋆(V_{2}⋆⋆V_{3}).

By Proposition 8.1, we only need to show that each mg-pair

((M, A)⋆⋆(N, B))⋆⋆(T, C)

such that (M, A) ∈ V_{1}, (N, B) ∈ V_{2} and (T, C) ∈ V_{3} is in V_{1}⋆⋆(V_{2}⋆⋆V_{3}). Moreover, by Proposition 13.8, we may assume that the actions of T are pointwise. But then, by Lemma 13.7, the projection π : (M, A)⋆⋆(N, B) → (N, B) is compatible with the actions of T, and moreover, by Corollary 13.6, it holds that

(K_{π⋆⋆(T,C)}, A_{π⋆⋆(T,C)}) < (M, A).

Thus, by Theorem 13.2 applied to the morphism

π⋆⋆(T, C) : ((M, A)⋆⋆(N, B))⋆⋆(T, C) → (N, B)⋆⋆(T, C),

we have

((M, A)⋆⋆(N, B))⋆⋆(T, C) < (M, A)□((N, B)⋆⋆(T, C)),

proving that ((M, A)⋆⋆(N, B))⋆⋆(T, C) is in V_{1}⋆⋆(V_{2}⋆⋆V_{3}). □

Recent BRICS Report Series Publications

RS-03-28 Zoltán Ésik and Kim G. Larsen. Regular Languages Definable by Lindström Quantifiers. August 2003. 82 pp. This report supersedes the earlier BRICS report RS-02-20.

RS-03-27 Luca Aceto, Willem Jan Fokkink, Rob J. van Glabbeek, and Anna Ingólfsdóttir. Nested Semantics over Finite Trees are Equationally Hard. August 2003. 31 pp.

RS-03-26 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. August 2003. 23 pp. Extended version of a paper appearing in Hu and Rodríguez-Artalejo, editors, Sixth International Symposium on Functional and Logic Programming, FLOPS ’02 Proceedings, LNCS 2441, 2002, pages 134–151. This report supersedes the earlier BRICS report RS-02-30.

RS-03-25 Biernacki Dariusz and Danvy Olivier. From Interpreter to Logic Engine: A Functional Derivation. June 2003.

RS-03-24 Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines. June 2003.

RS-03-23 Korovin Margarita. Recent Advances in Σ-Definability over Continuous Data Types. June 2003. 26 pp.

RS-03-22 Ivan B. Damgård and Mads J. Jurik. Scalable Key-Escrow. May 2003. 15 pp.

RS-03-21 Ulrich Kohlenbach. Some Logical Metatheorems with Applications in Functional Analysis. May 2003. 55 pp.

RS-03-20 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. May 2003. 16 pp. Final version to appear in Leuschel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’03 Proceedings, 2003. This report supersedes the earlier BRICS report RS-03-11.

RS-03-19 Christian Kirkegaard, Anders Møller, and Michael I. Schwartzbach. Static Analysis of XML Transformations in Java. May 2003. 29 pp.

RS-03-18 Bartek Klin and Pawe� Sobociński. Syntactic Formats for Free: An Abstract Approach to Process Equivalence. April 2003. 41 pp.