{'fraction_non_alphanumeric': 0.05356859586826274, 'fraction_numerical': 0.008627106441654158, 'mean_word_length': 3.80318837182042, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 69, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Monadic Monadic Second Order Logic

One of the main reasons for the correspondence of regular languages and monadic second-order logic is that the class of regular languages is closed under images of surjective letter-to-letter homomorphisms. This closure property holds for structures such as finite words, finite trees, infinite words, infinite trees, elements of the free group, etc. Such structures can be modelled using monads. In this paper, we study which structures (understood via monads in the category of sets) are such that the class of regular languages (i.e. languages recognized by finite algebras) are closed under direct images of surjective letter-to-letter homomorphisms. We provide diverse sufficient conditions for a monad to satisfy this property. We also present numerous examples of monads, including positive examples that do not satisfy our sufficient conditions, and counterexamples where the closure property fails.

For more about these results, see the survey by Thomas [12]. The large number of examples calls for a more systematic framework, where the notion of a composable structure (be it a finite word, ω-word, finite tree etc.) would be a parameter, and a characterization of the expressive power of MSO, a result. In our view, the lack of such a framework is a manifestation of what Samson Abramsky has recently called a remarkable divide in the field of logic in Computer Science, between two distinct strands: one focussing on semantics and compositionality ("Structure"), the other on expressiveness and complexity ("Power"). It is remarkable because these two fundamental aspects of our field are studied using almost disjoint technical languages and methods, by almost disjoint research communities. [13, p. 1].
A generic approach to MSO was proposed in [14], using monads. Monads are a standard categorical tool to study compositionality, and they are firmly rooted in the "Structure" strand of Theoretical Computer Science. Applying them to study the expressive power of MSO is a step towards building a bridge over the divide.
Monads are general enough to capture structures such as words, trees, graphs, etc. but specific enough to describe concepts such as recognizable languages (as observed by Eilenberg and Wright in [15,Section 11]), syntactic algebras [14,Section 3] or pseudovarieties [14,Section 4]. Another advantage of monads is that they can model infinite objects (such as infinite words or trees, which are central topics in automata theory), which is not the case for some alternative approaches, such as Steinby's approach via universal algebra [16].
When discussing the relationship of MSO and recognizable languages, there are two implications to consider.
• Recognizable ⇒ definable in MSO. This implication is easy for structures such as finite words or trees, where MSO can be used to define some canonical decomposition. In other cases, the proof can be much harder. Indeed, the proofs are relatively recent in the cases of countable linear orders [8,Theorem 3], graphs of bounded treewidth [11,Theorem 2.10], or graphs of bounded linear cliquewidth [17,Theorem 3.5]. The implication is known to fail for graphs of unbounded treewidth or cliquewidth [18,Proposition 4.36], and it also fails for infinite trees under a naive definition of finite algebras [19,Section 4]. Sometimes, e.g. for graphs of bounded cliquewidth, the implication remains an open question [17,Section 8]. A general understanding of this implication seems to be a hard problem, and we do not make any attempts in that direction in this paper.
• Definable in MSO ⇒ recognizable. In all known cases, when recognizable languages are defined in terms of finite algebras, this implication is relatively straightforward. 1 Roughly speaking, languages recognized by finite algebras are automatically closed under Boolean combinations, and closure under existential quantification is proved using some kind of powerset construction. This argument is so deceptively simple that [14,Lemma 6.2] wrongly claimed that it works for every monad. One purpose of our paper is to correct this mistake, show counterexamples to the claim, and study conditions that make the implication hold; the resulting landscape of monads turns out to be quite interesting.
Motivating example: finite words To explain how MSO can be defined for an arbitrary monad, we begin by describing MSO for finite words in a manner which can be translated to a more generic setting. A word w over an alphabet Σ can be understood as a relational structure [12, Section 2.1], denoted by w, where the universe is the positions of the word, there is a binary predicate x < y for the order on positions, and for every a ∈ Σ there is a unary predicate Q a which selects positions that have label a. To define properties of a word w, we can use sentences of first-order logic or monadic second-order logic over the vocabulary of w. For example, if w ∈ {a, b} * then the sentence there is a position with label a ∧ ∀y (y > x ⇒ Q a (x)) such that all later positions also have label a is true in w if and only if w belongs to the regular language (a + b) * a + . This sentence uses only first-order logic (quantification over positions), but some regular languages need monadic secondorder logic (quantification over sets of positions). A famous example is the regular language of words of even length, which is defined by the sentence ∃X there is a set of positions                    ∀x ∃y y ≤ x ∧ y ∈ X the first position is in X ∀x ∃y y ≥ x ∧ y ∈ X the last position is not in X ∀x ∀y (x < y ∧ ¬(∃z x < z < y)) ⇒ (x ∈ X ⇔ y ∈ X) for every two consecutive positions, exactly one is in X .
The theorem of Büchi, Elgot and Trakhtenbrot that we mentioned above says that a language of finite words is regular if and only if it can be defined by a sentence of MSO. The "regular ⇒ definable in MSO" implication can be proved by using the logic to formalise the semantics of a nondeterministic finite automaton (or a regular expression). For the converse implication, one shows that the class of regular languages has all the closure properties that are used in MSO. This observation is formalised in the following result. (A letter-to-letter homomorphism is defined to be a function of the form f * : Σ * → Γ * for some f : Σ → Γ.) [14,Lemma 6.1]] For finite words, the class of MSO definable languages is the least class of languages over finite alphabets that contains the languages 0 * ⊆ {0, 1} * and 0 * 1 * ⊆ {0, 1} * and is closed under union, intersection, complement, inverse images and direct images along surjective letter-to-letter homomorphisms.
Proof. (Sketch) Following [12,Section 2.3], one can eliminate first-order variables from MSO, and keep only the monadic second-order variables. Instead of the usual atomic predicates x < y and Q a (x), which use first-order variables, one uses atomic predicates X ⊆ Y set inclusion X < Y every position in X is before every position in Y X ⊆ Q a all positions in X have label a A formula with free variables φ(X 1 , . . . , X n ) over an alphabet Σ can be seen as a language over an extended alphabet Σ × 2 n . The idea is to interpret a word over the extended alphabet as a word together with a valuation of the sets X 1 , . . . , X n , as indicated by the n bits stored by every position. For instance, if φ(X, Y ) = X ⊆ Y and ψ(X, Y ) = Y ⊆ X, then the word w = (a, 0, 0)(a, 1, 0)(b, 1, 1), does not satisfy φ, but satisfies ψ.
The set of words that satisfy ∃X φ(X, Y 1 , . . . , Y n ) is exactly the direct image of the set of words that satisfy φ(X, Y 1 , . . . , Y n ) under the letter-to-letter homomorphism π * which is obtained by lifting to words the projection π : Σ × 2 n+1 → Σ × 2 n (a, x, y 1 , . . . , y n ) → (a, y 1 , . . . , y n ) In this sense, the second-order existential quantifier is abstractly captured by direct images under (surjective) letter-to-letter homomorphims. Given the above observations, one can show the theorem by induction of the structure of MSO formulas. The language 0 * ⊆ {0, 1} * corresponds to the predicates X ⊆ Y and X ⊆ Q a by means of an inverse image (the idea is that the letter 0 represents the positions which satisfy X ⊆ Y and 1 represents the other positions, likewise for X ⊆ Q a ). The language 0 * 1 * ⊆ {0, 1} * corresponds to the predicate X < Y , again by an inverse image. Direct images of surjective letter-to-letter homomorphisms correspond to the quantifier ∃. Closure under union, intersection and complement come from the logical connectives ∨, ∧ and ¬, respectively.
Motivated by Proposition 1, one can define an abstract version of MSO in any monad, at least over the category of sets, as the least class of languages with the closure properties stated in the proposition. This definition was proposed in [14, Section 6.1], and is described in more detail in Section 3. A parameter of the definition is a choice of atomic languages (such as 0 * and 0 * 1 * in Proposition 1). If the atomic languages are recognizable, and the class of recognizable languages has the required closure properties, then all MSO definable languages are going to be recognizable. As mentioned previously, most closure properties for recognizable languages are straightforward: Boolean combinations and inverse images under surjective letterto-letter homomorphisms (or, indeed, under arbitrary homomorphisms). There is one exception: direct images under surjective letter-to-letter homomorphisms. The main topic of this paper is understanding this last closure property.
As we will see, there are examples of monads for which the closure property fails. Also, when the property holds, it can hold for various reasons. We identify three rather diverse sufficient conditions: weakly epi-cartesian) which guarantees that a powerset construction works. Many monads are weakly epi-cartesian, including monads for all structures that have been traditionally considered in automata theory (words, trees, etc.).
As a by-product, we prove that weakly cartesian monads admit distributive laws over the powerset monad (Theorem 22). This result is of independent interest: it extends previous results by Jacobs [20], and it contrasts with recent negative results of Klin and Salamanca [21] and Zwart and Marsden [22].
2. Another sufficient condition is having a Mal'cev term (see Section 4.2). For example, the free group monad has a Mal'cev term, but it does not admit a powerset construction.
3. Yet another reason is that the monad preserves finiteness, which implies that all languages over finite alphabets are trivially recognizable. Although seemingly trivial, this condition can cover interesting examples, such as the monad of idempotent monoids, where preservation of finiteness is true but not obvious.
We will also show several examples of monads where the closure property holds, but which do not fall into any of the three classes described above. The project of understanding MSO for monads -even in the restricted setting of the category of sets -is still far from complete. We hope, however, that the reader will be intrigued by the rich variety of examples -we show 27 of them altogether.
Structure of the paper. In Section 2 we recall basic notions and results about monads, followed by an abstract monadic definition of MSO in Section 3. In Sections 4 and 5 we present three sufficient conditions which guarantee that recognizable languages are closed under direct images of surjective letter-to-letter homomorphisms. We show numerous examples there. Other positive examples, which do not satisfy any of the three conditions, are shown in Section 6. Section 7 lists a few counterexamples where the closure property fails. In Section 8 we illustrate what would happen if somewhat stronger closure properties were required of a monad. We conclude in Section 9 by sketching main directions of future work.

Monads
We now introduce some basic concepts and intuitions related to monads. Everything in this section is completely standard (see e.g. [23,24]). One of the several possible intuitive understandings of monads is that they formalize "ways to collect things". Given a set Σ (understood as an alphabet), a monad returns a set T Σ of collections, or structures, built out of letters from Σ. The kind and shape of these structures depends on the monad: for example, the finite list monad sets T Σ to be the set of all finite sequences of elements of Σ, and the powerset monad returns the set of all subsets of Σ. A monad must provide further structure: • A way to apply functions to structures element-wise; formally, a function f : Σ → Γ should yield a function T f : T Σ → T Γ so that identity functions and function composition are preserved (formally, this makes T a functor); • A way to build "singleton" structures, formalized as a function η Σ : Σ → T Σ, called the unit, for each alphabet Σ; • A way to "flatten" structures of structures to single-layer structures, formalized as a function µ Σ : T (T Σ) → T Σ, called the multiplication, for each alphabet Σ.
These ingredients are subject to a few axioms. First, both the unit and the multiplication must be natural, i.e., they must be invariant under arbitrary renamings of elements. Formally, the "naturality squares" must commute for every function f : Σ → Γ. Furthermore, the multiplication operation must be associative and the unit must be the actual two-sided unit for it, in the sense made formal in the following definition: A monad (T, η, µ) (on the category Set of sets and functions) is a functor T : Set → Set together with natural transformations η : Id ⇒ T and µ : T T ⇒ T , subject to axioms: for all sets Σ.
We will usually denote a monad (T, η, µ) simply by T . If a risk of confusion arises (i.e. in the presence of more than one monad), its unit and multiplication will then be called η T and µ T .
Here are a few standard examples of monads.
Monad 2. The same definitions restricted to non-empty lists form the non-empty list monad T Σ = Σ + , also called the free semigroup monad.
Monad 4. The nonempty powerset monad P + is defined exactly the same but with T Σ restricted to nonempty subsets of Σ.
Monad 5. The finite powerset monad is also defined the same but with T Σ restricted to finite subsets of Σ. This is also called the free semilattice monad. Monad 6. The bag monad B, also known as the multiset monad or the free commutative monoid monad, is defined so that BΣ is the set of functions from Σ to N that are zero almost everywhere, and the action on functions is defined by the sum is well-defined since β returns zero almost everywhere. The unit of B maps an element x ∈ Σ to the function [x → 1] that maps x to 1 and is zero everywhere else. Multiplication is defined by: We shall be looking at numerous examples of monads in the following. Many of them are best presented in terms of operations and equations. A useful recipe for defining a (finitary) monad on Set begins by considering an algebraic signature, i.e., a set of operation symbols, each with an associated finite arity. With a signature fixed, the notion of a term over a set X of variables is defined as usual: a variable x ∈ X is a term, and σ(t 1 , . . . , t n ) is a term whenever σ is a symbol of arity n and t 1 , . . . , t n are terms. An equation is a pair of terms (over the same set of variables). A set of equations defines, for any alphabet Σ, a congruence relation on the set of terms over Σ in the expected way: it is the least equivalence relation that is compatible with the operations and satisfies all the equations. One then defines T Σ to be the set of equivalence classes of terms over Σ, under that congruence relation. For the unit, η Σ (x) is (the equivalence class of) the variable x, and multiplication is defined by term substitution. It is standard to check that these ingredients form a monad on Set, and the original set of equations is then called an equational presentation of that monad.
Example 3. Let the signature contain a binary symbol • and a constant (i.e., a symbol of arity zero) e. The unit and associativity equations: form a presentation of the free monoid monad (Monad 1). Adding a further equation for commutativity: one obtains the free commutative monoid monad (Monad 6). Adding yet another equation: yields a presentation of the finite powerset monad (Monad 5).
Definition 4. Given a monad T , an (Eilenberg-Moore) algebra for T (shortly, a T -algebra) is a set A together with a function α : T A → A subject to two axioms: commutes. T -algebras and their homomorphisms form a category, denoted Alg(T ).
It is easy to check that for any set Σ, the set T Σ with µ Σ : T T Σ → T Σ is a T -algebra. This is the free T -algebra over Σ; its fundamental property is that for any T -algebra A, homomorphisms from T Σ to A are in bijective correspondence with functions from Σ to A.
Example 5. For T the list monad (Monad 1), a T -algebra on A is a function that interprets arbitrary finite sequences over A as elements of A. The two axioms of T -algebras mean that the function is associative in the obvious sense; indeed, it easy to check that T -algebras correspond to monoids. Moreover, T -algebra homomorphisms are monoid homomorphisms. T Σ = Σ * is the free monoid over Σ.
The same schema applies to any equationally definable class of algebras. We can therefore consider "free X monad" where X can stand for semigroup, commutative semigroup, group, abelian group, lattice, distributive lattice, Boolean algebra and so on, with algebras for the "free X monad" being exactly X's.

Monadic Monadic Second Order Logic
We now define our abstract monadic MSO, inspired by Proposition 1. First we define a general notion of a recognizable language [15].
Definition 6 (Recognizable T -languages). Let T be a monad on Set and Σ a finite set of symbols, called the alphabet in this context. A T -language over Σ is a subset of T Σ. A Talgebra A = (A, α) recognizes a T -language L over Σ iff there is a homomorphism h : T Σ → A, and a subset S ⊆ A, such that L is the inverse image of S along h. A T -language is recognizable if it is recognized by some finite T -algebra.
For a fixed T , let Rec T denote the class of all recognizable T -languages. Proof. Let L i be a language that is recognized by a finite T -algebra A i with S i ⊆ A i through homomorphisms h i : T Σ → A i , i = 1, 2. Then: • L 1 ∩ L 2 is recognized by A 1 × A 2 through the homomorphism h 1 , h 2 and the subset {(a 1 , a 2 ) | a 1 ∈ S 1 and a 2 ∈ S 2 }; • L 1 ∪ L 2 is recognized by A 1 × A 2 through the homomorphism h 1 , h 2 and the subset Let h : T Σ → T Γ be a T -algebra homomorphism. If a language L ⊆ T Γ is recognizable then the inverse image ← − h (L) ⊆ T Σ is recognizable as well: it is recognized by the same Talgebra and subset as L. So recognizable languages are closed under inverse images of T -algebra homomorphisms. One may ask the same question about direct images: if L ⊆ T Σ is recognizable, is − → h (L) ⊆ T Γ recognizable as well? This question will be the our main technical focus in the following.
We call an algebra homomorphism h : T Σ → T Γ a letter-to-letter homomorphism if h = T f for some function f : Σ → Γ. We call it surjective if f is surjective 2 . Proposition 1 motivates the following definition [14,Sec. 6].
Definition 9. Let T be a monad on Set. Let L be a family of T -languages over finite alphabets. We define MSO(L) as the least class of T -languages over finite alphabets that contains L and is closed under Boolean operations, inverse images of homomorphisms, and direct images of surjective letter-to-letter homomorphisms.
2 All functors on Set preserve surjective functions since every surjective function f has a right inverse g in the sense that f • g = id, then we apply T to the last equation to obtain that T f is also surjective. Conversely, under the assumption that each component of η is injective, we have that T is faithful and faithful functors reflect epimorphisms (=surjections in the category Set). To show that T is faithful assume T f = T g for f, g : which implies g = f since ηY is injective. There will be no confusion between T f being surjective and f being surjective since all the monads we consider are such that ηΣ is injective for each Σ. Now we are ready to state the main technical question of this paper, which is a necessary step towards a result similar to Proposition 1 for other monads, namely: • When does L ⊆ Rec T imply MSO(L) ⊆ Rec T ? By Proposition 8, Rec T is closed under Boolean operations. Trivially, inverse images of recognizable languages are also recognizable. Thus the question is reduced to: • When is Rec T closed under direct images of surjective letter-to-letter homomorphisms?
Asking this specific question is, to some extent, a design decision. In the classical setting of finite words, recognizable languages are closed under direct images along arbitrary homomorphisms, so one may reasonably ask for a stronger closure property: under arbitrary homomorphisms, or perhaps under arbitrary (i.e. possible non-surjective) letter-to-letter homomorphisms. We will look at these variants of the question in Section 8.
In any case, one may wonder whether perhaps the question (say, in the weak version as stated above) has an affirmative answer for every monad. Indeed, this was mistakenly claimed as a fact in [14,Lemma 6.2]. However, as the following counterexample shows, the situation is not so simple.
Monad 7. Let T be the free monoid monad quotiented by the additional equation The congruence (which we denote ∼) induced on Σ * by (3) has been the subject of some research: Brzozowski in [25] asked whether all equivalence classes of this congruence are regular languages, and the question has remained open ever since (see [26]). We do not need to answer that question for our purposes. Elements of T Σ are ∼-equivalence classes of finite Σ-words, and so a T -language over Σ can be identified with a ∼-closed language of Σ-words. It is easy to see that a T -language is recognizable if and only if its associated language of Σ-words is regular.
Let Γ = {a, b, c} and Σ = Γ ∪ {0, 1}. Consider the language of finite Σ-words: It is obviously regular. It is also ∼-closed. Indeed, assume that u0v1 = w for some u, v ∈ Γ * and w ∈ Σ * . This means that there is a finite sequence of applications of (3) that transforms u0v1 into w. If this sequence is nonempty then its first step must detect a square, that is, a word of the form xx, in u0v1. (The other option is that a cube xxx must be present, which implies a square anyway). Since 0 and 1 occur in that word only once each, it is clear that the square subword must occur entirely within u or within v. This means that the result of applying (3) to u0v1 still belongs to L. By induction, also w must belong to L.
We have thus proved that L, considered as a subset of T Σ, is T -recognizable. Now consider Σ ′ = Γ ∪ {0} and let h : Σ → Σ ′ map 1 to 0 and act identically on all other letters. The direct image of L along h, construed (as it should be) as a subset of T Σ ′ , corresponds to a language K of Σ ′ -words which arises as a ∼-closure of the language Γ * 0Γ * 0. (Note that the language itself is not ∼-closed, as e.g. a0a0 ∼ a0a0a0. ) We shall show that K is not regular, which will imply that the direct image of L under h is not recognizable.
First, it is a well-known fact that since Γ has 3 elements, the language Γ * contains infinitely many square-free words. Moreover, two distinct square-free words cannot be ∼-equivalent, since the equation (3) cannot be applied to a square-free word.
Were the language K regular, its Myhill-Nerode congruence would have a finite index, and so there would be two distinct square-free words v, w ∈ Γ * which are Myhill-Nerode equivalent with respect to K.
Thanks to (3) we have v0v0v0 ∈ K so, since v and w are Myhill-Nerode equivalent, also v0w0v0 ∈ K.
But it is easy to check that if v and w are square-free and v = w then v0w0v0 is also square-free, and so it is not ∼-equivalent to any word other than itself. We arrive at a contradiction, and so K cannot be regular.
More counterexamples of this kind are presented in Section 7. But first, now knowing that our main technical question is non-trivial, let us study some conditions on the monad T that guarantee an affirmative answer to it.

Simple sufficient conditions
In this section, we present two conditions on a monad T that guarantee that the class Rec T is closed under direct images of surjective letter-to-letter homomorphisms. Another, more elaborate sufficient condition will be presented in Section 5.

Monads that preserve finiteness
One straightforward case where direct images of recognizable languages are also recognizable, is the case where the functor part of the monad preserves finiteness, i.e., maps finite sets to finite sets. Trivially, then, any language over Σ is recognized by the identity homomorphisms into the finite algebra T Σ, so in particular any direct image is recognizable.
Examples of monads with this property include: the powerset monad and its variants, the double contravariant powerset monad 2 2 Σ , monads for idempotent semigroups, idempotent monoids, distributive lattices, Boolean algebras, semimodules over a finite semiring, and, in general, any locally finite variety. A variety is locally finite if every finitely generated algebra is finite.
For a given equational theory, checking if a finitely generated algebra is finite could be a challenging problem. For instance, the fact that a finitely generated idempotent semigroup is finite is a nontrivial fact, with multiple proofs published in different papers, (see e.g. [27,28]). Another interesting case are distributive lattices, where the exact size of the free algebra on n generators is still unknown for values of n > 8.

Monads with a Mal'cev term
Equational theories over finite signatures that have a Mal'cev term induce monads for which direct images of recognizable languages along surjective letter-to-letter homomorphisms are also recognizable. A Mal'cev term is defined as follows [29,II.12].
Definition 11. A ternary term p(x, y, z) on an equational class V is called a Mal'cev term if the following identities hold in V : Equational classes with a Mal'cev term are congruence-permutable [29, Theorem II.12.2], i.e., any two congruences commute in them. Examples of such classes include: The free group monad, presented by a binary operation • , a unary operation (−) −1 and a constant operation 1, subject to the usual group axioms. A Mal'cev term p is given by Similarly, Mal'cev terms can be found for any equational class that has a group reduct, including abelian groups, rings, vector spaces over a field and algebras over a field. In this case, if the group reduct is given in additive notation, then the term p is given by p(x, y, z) = x−y +z.

Monad 10.
The free Boolean algebra monad, presented by binary operations ∨ and ∧, a unary operation ¬ and constants 0 and 1, subject to familiar equations. A Mal'cev term is Monad 11. The free Heyting algebra monad, presented by binary operations ∨, ∧ and →, and constants 0 and 1, subject to the standard equations of Heyting algebras. A Mal'cev term is Note that, apart from the case of Boolean algebras, in all the above examples finitely generated free algebras are infinite.

Proposition 12. For a monad T presented by a set of equations that admits a Mal'cev term, the class Rec T is closed under direct images of surjective letter-to-letter homomorphisms.
Before proceeding with the proof, we recall the standard notion of a congruence. Let F = {f i } i∈I be a type of algebras, where each operation symbol f i has arity n i , and let A be an F-algebra. A binary relation θ on A is a congruence on A if it is an equivalence relation and has the compatibility property in the following sense: Given such a congruence, the quotient A/θ has an F-algebra structure (see e.g. [29,II.5] for more properties of congruences and quotient algebras).
Without loss of generality, we may assume that h is a surjective homomorphism. Let g : Σ → Γ be a surjective function. Define the relation ≈ on T Γ as Then ≈ is a congruence on T Γ, which implies that T Γ/≈ is a T -algebra. Indeed, the relation ≈ is clearly reflexive, symmetric and has the compatibility property (the latter because h is a homomorphism). To prove transitivity, let p(x, y, z) be a Mal'cev term and assume since ≈ is reflexive and has the compatibility property. Let τ : T Γ → T Γ/≈ be the canonical quotient map. Define a function e : A → T Γ/≈ by: this is well defined since h is surjective and by the definition of ≈ and τ . Moreover, e is surjective because both T g and τ are; as a result, the T -algebra T Γ/≈ is finite. We show that the direct image of L along T g is recognized by the homomorphism τ to T Γ/≈ through the subset − → e (S) ⊆ T Γ/≈. In other words, we will show that To this end, for any w ∈ T Γ calculate: which finishes the proof.
Remark. The key step in the above proof is the general observation that in a congruencepermutable variety, every reflexive and symmetric relation with the compatibility property is a congruence [30,Proposition 3.8.]. Reflexive, symmetric relations with the compatibility property are called tolerances.
In Section 7.3 we shall see that relaxing the Mal'cev condition even slightly does not guarantee recognizable languages to be preserved under direct images along surjective letter-to-letter homomorphisms.

Weakly epi-cartesian monads
In this section, we present a class of monads -called weakly epi-cartesian monads -where a powerset construction can be used to prove that recognizable languages are closed under direct images of letter-to-letter homomorphisms. This class includes the classical case of finite words (Monad 1).
We begin with an intuitive description of the powerset construction. Consider a monad T and a language L ⊆ T Σ which is recognized by a homomorphism h : T Σ → A for some T -algebra A = (A, α). For a surjective function on the alphabet f : Σ → Γ, we want to show that the direct image of L under the letter-to-letter homomorphism T f : T Σ → T Γ is also recognizable.
A natural idea is to consider a powerset algebra, where the universe is the family of nonempty subsets of A, and the product operation is defined using: can be obtained from t by choosing an element from each set can be made precise, see (8) in Definition 19 }.
There are two issues that need to be addressed here. First, one must check that the powerset algebra is indeed a T -algebra, i.e., that it satisfies the axioms of Definition 4. The second issue is finding a homomorphism into the powerset algebra that recognizes the direct image of L under T f . The natural idea is to consider the function however, it is not immediately clear that this function is a homomorphism. In fact this does not happen in every monad, contrary to what was claimed in [14, Lemma 6.2]. For example, in the monad of groups (Monad 8) the powerset algebra does not satisfy, in general, the axiom The goal of this section is to establish a condition on the monad T which ensures that the above powerset construction works as expected.

Definitions
First, a few standard categorical definitions. A commuting diagram of sets and functions: is called a weak pullback if, for each x ∈ X and y ∈ Y such that f (x) = g(y), there is some p ∈ P such that h(p) = x and k(p) = y. If p is unique for each such x and y then the square is a pullback. For every two functions f and g as above a canonical pullback exists and is defined by with h = π 1 and k = π 2 , projections from P into X and Y .
A functor T preserves weak pullbacks iff applying T to everything in a weak pullback as in (5) results in a weak pullback again. A routine categorical argument shows that one may equivalently require only that (canonical) pullbacks are mapped to weak pullbacks; preservation of all other weak pullbacks follows. So, T preserving weak pullbacks means that for all functions f : X → Z and g : Y → Z, and for any t ∈ T X and r ∈ T Y such that T f (t) = T g(r), there exists some p ∈ T P (for P as in (6)) such that T π 1 = t and T π 2 = r.
Intuitively, this means that whenever two terms t and r are sufficiently similar to be equated by equating some variables, then there is some term p, built of compatible pairs of variables, that projects to t and r. Many monads, such as the free monoid monad and the powerset monad and its variants, have this property. The following examples show how the property may fail.
Example 13. The free group monad (Monad 8) does not preserve weak pullbacks: the square k the unique functions of their type) is a pullback, and terms t = 1 ∈ T ∅ and r = a • b −1 ∈ T {a, b} are equated by T f and T g, but there is no term p ∈ T ∅ that would be mapped to r by T k.
Example 14. Monad 7, i.e., the free monoid monad subject to the additional axiom does not preserve weak pullbacks. Indeed, the square (with f, g the unique functions of their type) is a pullback, and the terms t = a • b ∈ T {a, b} and r = c • d • c ∈ T {c, d} are equated by T f and T g, but there is no term p ∈ T ({a, b} × {c, d}) that would project to t and r.
Given Set-functors F and G, a natural transformation α : F ⇒ G is weakly cartesian if for every function f : X → Y the naturality square is a weak pullback. A weaker property is being weakly epi-cartesian, where only naturality squares for surjective f are required to be weak pullbacks.
We can now formulate our main property of interest: is weakly cartesian if T preserves weak pullbacks and η and µ are weakly cartesian. It is weakly epi-cartesian if T preserves weak pullbacks and η and µ are weakly epi-cartesian.
Weakly cartesian monads have been studied in the literature [31,32,33]. The notion of a weakly epi-cartesian monad seems to be new.
The requirement that the naturality square is a weak pullback amounts to saying that whenever a unit term η Y (y) is obtained as a value of T f applied to some t ∈ T X, then T X must itself be a unit term η X (x) for some x such that f (x) = y. So weak (epi-)cartesianness of η intuitively means that one cannot obtain a unit term by equating variables in a non-unit term. This holds for many monads, including the free monoid monad. Notably, the property fails for the powerset monad, where the nonunit term {a, b} ∈ P{a, b} is mapped to the unit {c} ∈ P{c} by Pf , for the unique function Let us now look at the multiplication µ being weakly (epi)-cartesian. To say that the naturality square is a weak pullback means that, for any term t ∈ T X, if a term T f (t) can be decomposed as "term of terms" θ ∈ T T Y (so that T f (t) is the flattening of θ), then the term t itself has a similar decomposition. So, intuitively, weak (epi)-cartesianness of µ means that equating variables in a term does not introduce essentially new ways of decomposing the term.
Theorem 16. If T is a weakly epi-cartesian monad, then Rec T is closed under direct images along surjective letter-to-letter homomorphisms.

Examples
The three conditions of weak (epi-)cartesianness may fail in various configurations. For example, the powerset monad and its variants (Monads 3, 4 and 5) preserve weak pullbacks and have weakly cartesian multiplication, but their unit is not weakly epi-cartesian. On the other hand, Monad 7 does not preserve weak pullbacks, its unit is weakly cartesian and its multiplication is not weakly epi-cartesian. Further examples include: Monad 12. Consider the monad (T, η, µ) associated to the equational theory of a single ternary function symbol p and a single unary symbol s, with axioms p(x, x, y) = s(y) = p(y, x, x). Then T does not preserve weak pullbacks, η is weakly cartesian, and µ is weakly cartesian. We shall study this monad in more detail in Section 7.3.
Monad 13. Consider the monad (T, η, µ) associated to the equational theory on the signature {f, e}, where f is a unary function symbol and e is a constant, with the only axiom f (f (x)) = e. Then T preserves weak pullbacks, η is weakly cartesian, µ is weakly epi-cartesian, but µ is not weakly cartesian, cf. [32,Example 3.4]. This example distinguishes between the notions of weakly cartesian and weakly epi-cartesian monads.
However, many monads are weakly epi-cartesian, as the following examples show.
A rich source of weakly cartesian monads (and therefore of weakly epi-cartesian monads) are equational theories whose axioms are given by regular linear equations. A term is called linear if no variable appears in it more than once. An equation is called regular if each variable appears on the left-hand side if and only if it appears on the right-hand side. An equation is regular linear if it is regular and both sides of it are linear. For instance, the equations , and e • x = x, which axiomatize the variety of monoids, are regular linear. The commutativity axiom x • y = y • x is also regular linear. On the other hand, the group axiom x • x −1 = e and the idempotence axiom x • x = x are not regular linear.
It is not difficult to check that a monad presented by a set of regular linear equations is weakly cartesian. In fact, every such monad is analytic: in addition to being weakly cartesian, its functor weakly preserves wide pullbacks. This is a part of a more general framework, see [34].
In particular, the monads of semigroups, commutative semigroups, monoids, commutative monoids and the variety of all algebras for any given signature, are all weakly cartesian, hence also weakly epi-cartesian.
Example 17. Rec T is closed under direct images of surjective letter-to-letter homomorphisms for the monads of semigroups, commutative semigroups, monoids, commutative monoids and the variety of all algebras for any given signature.
The next four example monads are not finitary, so they do not have finitary equational presentations. Nevertheless, they are all weakly cartesian.
Monad 14 (A monad for ω-words). Consider the following extension of the list monad to infinite words. The monad maps an alphabet Σ to the set Σ + ∪ Σ ω of nonempty words of length at most ω. The unit is the same as in the list monad, while the multiplication operation is defined by µ X (w 1 w 2 · · · ) = w 1 w 2 · · · if all words w 1 , w 2 , . . . are finite w 1 w 2 · · · w k if w k is the first infinite word among w 1 , w 2 , . . .
Algebras for this monad are essentially the same as ω-semigroups [35, Section II.4], which are known to recognize the same languages as Büchi automata on ω-words. This monad is weakly epi-cartesian, so by Theorem 16 the recognizable languages are closed under direct images along surjective letter-to-letter homomorphisms, thus showing that all MSO definable languages are recognized by ω-semigroups.
Monad 15 (Countable linear orders). Monad 14 can be generalised from ω-words to other labelled linear orders, where the order type of the positions is not necessarily ω. Consider the monad where T Σ is the set of countable linear orders labelled by Σ, up to isomorphism. The unit and multiplication are defined in the natural way (contrary to Monad 14, there is no need to truncate). For example, T {a, b} contains the following element: the linear order of the rational numbers, labelled so that the positions with label a are dense and the same is true for the positions with label b. Using a back-and-forth argument, one can show that element described above is unique up to isomorphism. Shelah showed that satisfiability is decidable for MSO over this monad [9, Theorem 6.2], while Carton, Colcombet and Puppis [8, Proposition 3 and Theorem 3] showed that the recognizable languages are exactly the ones that are definable in MSO. This monad is weakly epi-cartesian, and therefore Theorem 16 implies that recognizable languages are closed under direct images of surjective letter-to-letter homomorphisms, which in turn implies that MSO definable languages are recognizable [8,Proposition 3].
In fact, as far as closure under direct images is concerned, there is nothing special about countable linear orders, as shown by the following monad.
Monad 16. One can also consider a variant of the previous monad, but for labelled linear orderings of cardinality at most continuum. This monad is also weakly epi-cartesian, and therefore MSO definable languages are recognizable. There is, however, a price to pay for considering uncountable orders: the satisfiability problem for MSO is undecidable for this monad, as proved by Shelah [9,Theorem 7].
There are also interesting monads that lie between ω-word and all countable linear orders.
Monad 17. Consider the countable linear orders which are scattered, i.e. do not contain any rational sub-ordering. This monad was studied implicitly by Carton and Rispal, where the Eilenberg-Moore algebras for the monad were called ⋄-algebras in [36,Definition 6]. This monad is weakly epi-cartesian, and therefore Theorem 16 implies that MSO definable languages are necessarily recognizable (this was already known in [36]). Some monads do not admit any presentation by regular linear equations, yet they still are weakly (epi-)cartesian. For example: Monad 18 (A left-idempotent operation). For a more unusual example of a weakly cartesian monad, consider a monad T presented by an equational theory with a single binary symbol • and with a single (non-linear) equation: To prove that T preserves weak pullbacks, consider any pullback diagram where P = {(x, y) | f (x) = g(y)} and π 1 and π 2 are the projections from P . Then, for any r ∈ T X, s ∈ T Y and t ∈ T Z such that we need to find p ∈ T P such that T π 1 (p) = r and T π 2 (p) = s. Formally, elements of T Z are equivalence classes of binary trees with elements of Z in leaves; each equivalence class can be represented by its unique smallest element: one where the pattern on the left-hand side of (7) does not appear. We therefore only consider r, s and t of this form, and we proceed by induction on the size of t.
For the base case, if t is a single letter (i.e. t ∈ Z) then obviously r ∈ X and s ∈ Y , therefore we can put p = (r, s).
For the inductive step, let for some s 1 , . . . , s m , y ∈ T Y such that T g(s i ) = t ′ and T g(y) = z. Assume, without loss of generality, that n ≤ m. By the inductive assumption, for each 1 ≤ i ≤ n and 1 ≤ j ≤ m there is a p i,j ∈ T P such that T π 1 (p i,j ) = r i and T π 2 (p i,j ) = s j . Also by the inductive assumption, there is some q ∈ T P such that T π 1 (q) = x and T π 2 (q) = y. Now consider p ∈ T P defined by: It is easy to check that T π 1 (p) = r and T π 2 (p) = s as required. This completes the proof that T preserves weak pullbacks. It is easy to see that the unit of T is cartesian, i.e., that the square for t ∈ T X and y ∈ Y then there must be t = η X (x) for some (necessarily, unique) x ∈ X such that f (x) = y. It remains to be proved that the multiplication of T is weakly cartesian, i.e., that The proof is similar to the proof of the fact that T preserves weak pullbacks. For any r ∈ T T Y , s ∈ T X and t ∈ T Y such that we need to find p ∈ T T X such that T T (p) = r and µ X (p) = s, and the construction proceeds by induction on the size of t. To prove that T preserves weak pullbacks, consider any pullback diagram } and π 1 and π 2 are the projections from P . Let r ∈ T X, s ∈ T Y and t ∈ T Z such that T f (r) = t = T g(s), we need to find p ∈ T P such that T π 1 (p) = r and T π 2 (p) = s. Elements of T Z are equivalence classes of terms on Z; each equivalence class can be represented by its unique smallest element, up to associativity: one where the pattern o(x · x) does not appear. We therefore assume r, s and t of this form, and we proceed by induction on the size of t.
For the base case, if t is a single letter (i.e. t ∈ Z) then obviously r ∈ X and s ∈ Y , therefore we can put p = (r, s).
For the inductive case, let t ∈ T Z. We have the following cases: i) t does not contain the function symbol o. In this case, r and s do not contain o either. Therefore, t is of the form t = z 1 · · · · · z n which implies that r and s are of the form r = x 1 · · · · · x n and s = y 1 · · · · · y n . Hence, we can take p = (x 1 , y 1 ) · · · · · (x n , y n ).
It is easy to check that, in each case, T π 1 (p) = r and T π 2 (p) = s as required. This completes the proof that T preserves weak pullbacks. To see that the unit of T is cartesian, consider a function f : X → Y , t ∈ T X and y ∈ Y such that T f (t) = η Y (y). Then there must be t = η X (x) for some (necessarily, unique) x ∈ X such that f (x) = y.
Finally, the proof that the multiplication µ is weakly cartesian is done by using a similar argument as the one that T preserves weak pullbacks.
Monad 20 (Weakly epi-cartesian monad that is not weakly cartesian). Consider the monad T presented by an equational theory with two unary operation symbols f and g, and a constant symbol e subject to the equations: f (f (x)) = g(g(y)) = e Note that T X is infinite for every non-empty X ({f g(x), f gf g(x), f gf gf g(x), . . .} ⊆ T X for x ∈ X). Also, the multiplication µ is not weakly cartesian since for the inclusion ι : {x} → {x, y} we have that T ι(e) = µ {x,y} f f (y) but f f (y) is not in the image of T T ι. Nevertheless, T is a weakly epi-cartesian monad, so Rec T is closed under direct images along surjective letterto-letter homomorphisms.

Proof of Theorem 16
We start by recalling the standard concept of a distributive law between monads [37]. Distributive laws are a standard tool for composing monads; we will use them to lift the powerset functor to the category of algebras for a monad.
Definition 18. Let (T, η T , µ T ) and (S, η S , µ S ) be monads. A distributive law of (T, η T , µ T ) over (S, η S , µ S ) is a natural transformation λ : T S ⇒ ST that satisfies the following axioms: Sometimes one is interested in laws that satisfy only some of these axioms. In particular, a distributive law of the functor T over the monad (S, η S , µ S ) only satisfies the axioms (a) and (c). We will be interested in distributive laws of monads over the powerset or the nonempty powerset, i.e., S = P or S = P + .
Definition 19 (The Jacobs Law). Let T be a functor. For every set X define a function λ X : T PX → PT X by: where ∈ X is the membership relation on X: and π 1 : ∈ X → X and π 2 : ∈ X → P + X are the canonical projections.
It is easy to see that if t ∈ T P + X then λ X (t) is not empty. Indeed, pick any function k : P + X → X such that k(S) ∈ S for all S ∈ P + X. Then k, id : P + X → ∈ X and the element r = T k, id (t) ∈ T (∈ X ) witnesses the fact that λ X (t) is not empty. As a result, λ X restricts to a function λ X : T P + X → P + T X.
The following result is due to Bart Jacobs [20,Section 4].

Proposition 20. If a functor T preserves weak pullbacks, then λ as in Def. 19 is a natural transformation and it is a distributive law of the functor T over the powerset monad P (and over the non-empty powerset monad P + ).
For any sets X and Y , there is a canonical partial order on the set of functions from X to PY : we say that f ≤ g : The following property of λ will be useful later: Proposition 21. If T preserves weak pullbacks then λ as in Def. 19 is monotone: whenever Proof. Assume f ≤ g, and pick some t ∈ T X and s ∈ λ Y (T f (t)). This means that there is some r ∈ T ∈ Y such that T π 1 (r) = s and T π 2 (r) = T f (t).
Consider the pullback Since T preserves weak pullbacks, the square is a weak pullback. By the properties of r, and by the definition of a weak pullback, there is some q ∈ T Q such that T (id × f )(q) = r (hence T π 1 (q) = T π 1 (r)) and T π 2 (q) = t.

Theorem 22. If a monad (T, η, µ) is weakly cartesian, then λ as in Def. 19 is a distributive law of the monad over the powerset monad P. If it is weakly epi-cartesian, then λ is a distributive law of the monad over the non-empty powerset monad P + .
Proof. The proofs of both statements are almost identical, so we shall present only the proof of the first statement (the one for P), and mark with (⋆) the two places where replacing P with P + makes a difference. Since weakly (epi)-cartesian monads preserve weak pullbacks by definition, the naturality of λ and axioms (a) and (c) in Definition 18 follow from Proposition 20. What remains to be proved is that λ satisfies axioms (b) and (d) in Definition 18.
For the axiom (b), we need to prove that λ X (η PX (Z)) = Pη X (Z) for Z ⊆ X.
For the right-hand side: For the right-to-left inclusion of (9), given z as in (11), it is enough to put r = η ∈ X (z, Z) and use naturality of η.
For the left-to-right inclusion of (9), assume r as in (10). Since T is weakly cartesian, the square T ∈ X T π 2 / / T PX is a weak pullback. (⋆) If P is replaced by P + , it is enough to assume that T is weakly epicartesian. Indeed, the function π 2 : ∈ X → P + X is surjective, so weak-epi-cartesianness is enough to conclude that the square is a weak pullback. By the properties of r stated in (10), and by the definition of weak pullback, there is some z ∈ Z such that η ∈ X (z, Z) = r. By naturality of η on π 1 : ∈ X → X, we obtain η X (z) = η X (π 1 (z, Z)) = T π 1 (η ∈ X (z, Z)) = T π 1 (r) = s as required. This completes the proof of (9).
For the axiom (d), we need to prove that λ X (µ PX (t)) = Pµ X (λ T X (T λ X (t))) for t ∈ T T PX.
For the right-hand side: For the left-to-right inclusion of (12), assume r as in (13). Since T is weakly cartesian, the square T ∈ X T π 2 / / T PX is a weak pullback. (⋆) As before, if P is replaced by P + , it is enough to assume that T is weakly epi-cartesian since the function π 2 : ∈ X → P + X is surjective. By the properties of r stated in (13), and by the definition of weak pullback, there is some w ∈ T T ∈ X such that µ ∈ X (w) = r and T T π 2 (w) = t.
Consider a function κ : T ∈ X → ∈ T X defined by: This is well defined: indeed, u ∈ T ∈ X itself witnesses that T π 1 (u) ∈ λ X (T π 2 (u)).
Since T preserves weak pullbacks, the square is a weak pullback. By the properties of v stated in (14), and by the definition of weak pullback, there is some q ∈ T Q such that T (id × λ X )(q) = v (hence T π 1 (q) = T π 1 (v)) and T π 2 (q) = t.
Armed with λ, we are ready to prove Theorem 16. Let L ⊆ T X be a language recognized by a finite T -algebra A = (A, α) as L = ← − h (C), where h : T X → A is a homomorphism and and C ⊆ A.
Seeing λ as a distributive law of the monad T over the functor P + , we can lift the functor P + : Set → Set to P + : Alg(T ) → Alg(T ), see [37]. In particular, as is easy to check using the axioms from Definition 18, is a legal T -algebra.
For a surjective function f : X → Y , define f : Y → P + X as the inverse image function on Y : Let g : X → Y be a surjective function. Since all functors on Set preserve surjectivity, T g : T X → T Y is also surjective. We will show that the direct image of L along T g is recognized by the algebra P + A. To this end, consider the function k : T Y → P + A defined by the composition: A straightforward calculation shows that the direct image of L along T g coincides with the inverse image ← − k (Ĉ). To finish the proof it is enough to show that k is a T -algebra morphism. That is, we need to show that the outer shape of the following diagram commutes: (3) commutes by naturality of λ and part (4) commutes since h is a T -algebra homomorphism. We now show the commutativity of (1) and (2). For (2), given s ∈ T T Y , we have: P + µ X (T T g(s)) = {µ X (r) | r ∈ T T X and T T g(r) = s}, To prove P + µ X (T T g(s)) = T g(µ Y (s)) we consider both inclusions.
For the left-to-right inclusion, put t := µ X (r) and use naturality of µ. For the right-to-left inclusion, use the fact that, since T is weakly epi-cartesian, To prove that (1) commutes, we will use the following simple fact: Lemma 23. Let f : X → Y be a surjective function. Then: Using this together with Proposition 21 and the axiom (a) from Definition 18 for λ, we obtain: Similarly, we obtain that: which completes the proof that (1) commutes, and the proof of the entire theorem.

Other examples
In this section, we show a few more cases where Rec T is closed under direct images along surjective letter-to-letter homomorphisms. These cases do not satisfy any of the sufficient conditions presented so far. They are also quite varied, with no clear pattern emerging: • the reader monad in Section 6.1 is infinitary, but its finite algebras are rather restricted, and preservation under direct images is proved by a compactness argument, • for the free lattice monad (Section 6.2), preservation follows from a convexity-based argument, • the monad in Section 6.3 is rather peculiar in that almost no language is recognizable for it, so preservation of recognizable languages under direct images holds for trivial reasons, • for the monad in Section 6.4, a construction similar to that described in Section 5 works, but with the powerset replaced by a more complex powerset-squared construction.

The reader monad
Monad 21. Let Σ ω denote the set of ω-sequences of letters from Σ. The functor T = (−) ω acts on functions in the expected way: This is an infinitary monad, with the unit mapping a letter a ∈ Σ to the constant sequence aaa · · · , and the multiplication defined by the diagonal function: This is a particular instance of the Haskell "reader" monad.
We will prove that recognizable T -languages are closed under taking direct images along surjective letter-to-letter homomorphisms. To fix the notation, we choose an arbitrary surjective function f : Σ → Γ for Σ, Γ finite, and any language L ⊆ T Σ recognizable by a homorphism h : T Σ → A to a finite T -algebra A = (A, α). This means that for some subset S ⊆ A: Assuming all this, we shall prove that the direct image of L along T f is recognizable by a homomorphism from T Γ to a finite T -algebra.
Without loss of generality we may assume that L is recognizable by a point in A, i.e. that S = {a} for some a ∈ A. This is because both taking inverse images and taking direct images commutes with unions, and recognizable languages are closed under finite unions. Such languages have a rather rigid "rectangular" structure: for some sequence of subsets Z 1 , Z 2 , . . . ⊆ Σ.
Proof. Given a language L recognizable by a ∈ A for an algebra α : for each n ∈ N. Then the left-to-right inclusion in (16) is obvious. For the right-to-left inclusion, consider a word w ∈ Z 1 × Z 2 × · · · ; this means that for every n ∈ N there is a word v n ∈ L such that v n,n = w n . Then w = µ Σ (v 1 v 2 · · · ), so: For any Σ, the set T Σ is equipped with the product topology, whose basis is the family of all open balls defined by B I (w) = {v ∈ T Σ | ∀n ∈ I. v n = w n } for w ∈ T Σ and finite I ⊆ N. With respect to this topology: Lemma 25. Every L recognizable by a point is closed.
Proof. From Lemma 24 it easily follows that T Σ \ L is open. Indeed, for L as in (16), take any w ∈ L. Then there is an n ∈ N such that w n ∈ Z n , and then B {n} (w) is disjoint from L. Lemma 25, and their union is closed since a finite union of closed sets is closed.

Lemma 26. Every L recognizable by a point in a finite algebra A is open.
We can now prove a stronger version of Lemma 24. Call a language L ∈ T Σ finitely rectangular if for some sequence of subsets Z 1 , Z 2 , . . . ⊆ X such that Z n = Σ for all except finitely many n.

Lemma 27. Every nonempty L recognizable by a point in a finite algebra is finitely rectangular.
Proof. By Lemma 24, L is of the form we need to prove that Z n = Σ for almost all n. Since Σ is a finite set, the space T Σ is compact. Its subspace L is closed by Lemma 25, so it is also compact. Consider the family of all those open balls B I (w) that are contained in L.
Since L is open by Lemma 26, for each w ∈ L there is some I such that B I (w) belongs to this family, so the family is an open cover of L. By compactness, it contains a finite subcover Let I = I 1 ∪ · · · ∪ I k . Fix any w ∈ L and take any v ∈ T Σ such that w n = v n for all n ∈ I. Since L is covered by (18) we have w ∈ B I i (w i ) for some i. Since I i ⊆ I also v ∈ B I i (w i ), so v ∈ L. Since we did not constrain v on the coordinates outside of I, we have that Z n = Σ for n ∈ I.
Finitely rectangular languages are closed under direct images of surjective homomorphisms: and − → f (Σ) = Γ since f is surjective.
The final piece of the puzzle is: Lemma 29. Every finitely rectangular language is recognizable by a finite algebra.
Proof. Let L ⊆ T Σ be as in (17), and let I ⊆ N be the (finite) set of those n where Z n = Σ. Define A = Σ I , and let α : T A → A be defined by: α(a 1 a 2 · · · )(n) = a n (n) for n ∈ I.
For the multiplication axiom, given v = v 1 v 2 v 3 · · · ∈ T T A and n ∈ I, calculate: so both expressions are equal as required, hence α is a T -algebra structure on A.
Define a homomorphism h : T Σ → A as a unique homomorphic extension of the function h 0 : Σ → A that maps every x ∈ Σ to the function in Σ I constant at x. Explicitly, this is defined by: h(w)(n) = α(T h 0 (w))(n) = w n for w ∈ T Σ, n ∈ I.
Recalling (17), define S ⊆ A by: Then, for w ∈ T Σ, calculate: w ∈ L ⇐⇒ ∀n ∈ I.w n ∈ Z n ⇐⇒ h(w) ∈ S, hence L is recognized by S ⊆ A along the homomorphism h.

The free lattice monad
Monad 22. The free lattice monad FL, whose algebras are lattices, has a well-known equational presentation over a signature with two binary symbols ∨ and ∧. It consists of equations: Lattices can be usefully regarded as partial orders, defined by: x ≤ y iff x ∨ y = y; ∨ and ∧ then become respectively join and meet operations.
We will prove that recognizable FL-languages are closed under taking direct images along surjective letter-to-letter homomorphisms. So, to fix the notation, we choose an arbitrary surjective function f : Σ → Γ for Σ, Γ finite, and any language L ⊆ FL(Σ) recognizable by a homorphism h : FL(Σ) → A to a finite lattice A. This means that for some subset S ⊆ A: Assuming all this, we shall prove that − → T f (L), the direct image of L along T f , is recognizable by a homomorphism from FL(Γ) to a finite lattice.
First let us consider the case where L is upwards-closed, i.e., where s ∈ L and s ≤ t implies t ∈ L.
Consider a homomorphism k : FL(Γ) → FL(Σ) defined as the unique extension of the map Note that the above join is nonempty since f is surjective. In particular, we have f (k 0 (y)) = y for all y ∈ Γ and, by definition, k 0 (f (x)) ≥ x for all x ∈ Σ. Since T f and k preserve meets and joins by definition, this extends to: for all t ∈ FL(Γ) and s ∈ FL(Σ).
Then it is easy to see that Indeed, for the right-to-left inclusion, for k(t) ∈ L one has t (19) = T f (k(t)) ∈ − → T f (L).
For the left-to-right inclusion, take any t ∈ FL(Γ) such that t = T f (s) for some s ∈ L. Then ≥ s and, since L is upwards-closed, k(t) ∈ L. The equation (20) implies that − → T f (L) is the inverse image of S ⊆ A along the composite homomorphism h • k : FL(Y ) → A, and so it is recognizable.
An analogous argument works if L is downwards-closed, with k defined using a meet rather than a join. Now consider an arbitrary (i.e. not necessarily upwards-or downwards-closed) language L recognizable by a homomorphism h : FL(Σ) → A to a finite lattice A. Without loss of generality we may assume that L is recognizable by a point in A, i.e., that for some a ∈ A. This is because both taking inverse images and taking direct images commutes with unions, and recognizable languages are closed under finite unions. Let L↑ and L↓ denote the upwards-closure and the downwards-closure of L, respectively. It is not difficult to check that upwards closure commutes with inverse images, in particular: Indeed, this amounts to requiring that, for every t ∈ FL(Σ), The right-to-left implication is immediate since h is monotone. For the left-to-right implication, since h : FL(Σ) → A is surjective, there is some r ∈ FL(Σ) such that h(r) = a. Put s = t ∧ r. Then obviously s ≤ t, and as required.
An analogous argument works for downward closures, i.e.: This means that both L↑ and L↓ are recognizable (by h), hence by the previous argument, their direct images along T f are also recognizable. Since recognizable languages are closed under intersection, it is now enough to prove that To this end, first notice that, since L is recognized by a point, it is convex, i.e., s ≤ t ≤ r and s, r ∈ L implies t ∈ L.
This implies that L↑ ∩ L↓ = L; indeed the right-to-left inclusion is trivial, and the left-to-right inclusion easily follows from the convexity of L. This does not immediately imply (21), as taking direct images does not commute with intersections in general. In this case, however, it does. To see this, first notice that L↑ is a filter, i.e., it is upward-closed and closed under finite intersections. Similarly, L↓ is an ideal, i.e., it is downward-closed and closed under finite unions. Now all we need is the following lemma, which holds for arbitrary lattice homomorphisms: Lemma 30. For any lattice homomorphism g : H → K and any filter U ⊆ H and ideal D ⊆ H such that U ∩ D = ∅: Proof. The left-to-right inclusion is obvious. For the right-to-left inclusion, take any t ∈ K such that ∃u ∈ U.h(u) = t and ∃d ∈ D.h(d) = t.
Pick any x ∈ U ∩ D (it exists by our assumptions), and put: Since x ∈ D and D is downward-closed, also x ∧ u ∈ D and (since D is closed under unions) y ∈ D. On the other hand, since x ∈ U and U is closed under intersections, also x ∧ u ∈ U and (since U is upward-closed) y ∈ U . So y ∈ D ∩ U , and it is enough to calculate: Using this lemma for g = T f , U = L↑ and D = L↓, we obtain (21) which directly implies that L is recognizable. It is shown that this equational theory has no non-trivial finite models, that is, every nonempty finite model has only one element [38,Section 2]. Indeed, if (A, f, g) is a finite algebra, from the equation f gf gg(x) = x we obtain that f is a surjection and g is a injection, which implies that f and g are bijections since A is finite and f : A → A and g : A → A. Hence, from the equation f gf f gg(x) = f gf f gg(y), we conclude that x = y for every x, y ∈ A. Therefore, Rec T is trivially closed under direct images along surjective letter-to-letter homomorphisms.

A non-trivial monad whose finite algebras are trivial
Remark. Even though the monad has the trivial algebra as the only finite model, the monad has infinite models. One such model is the set of the positive integers with g(n) = 2 n , f (2 2 n ) = 3 n , f (2 3 n ) = n, and f (m) = 1 otherwise, as shown in [38,Section 2]. Also, it is worth mentioning that given a finite set of identities over a given finitary signature, it is undecidable if there exists a non-trivial finite model that satisfies the given identities [39]. That is, it is undecidable in general if the class Rec T of recognizable languages is non-trivial. This means that describing the class Rec T or even finding a non-trivial element in Rec T could be undecidable.

The x(y(yz)) = x(yz) monad
Monad 24. Consider a monad T presented by an equational theory with a single binary symbol • and with a single equation: This equation is similar to the one that defined Monad 18, but the resulting monad has rather different properties. For one, its multiplication is not weakly epi-cartesian. To see this, consider Then, obviously: Now let r ∈ T Σ be defined by: It is easy to see that T f (r) = µ Y (t). However, there is no p ∈ T T Σ such that T T f (p) = t and µ Σ (p) = r. As a result, the naturality square is not a weak pullback. In spite of this, recognizable T -languages are closed under taking direct images along surjective letter-to-letter homomorphisms.
A T -algebra is simply a set equipped with a binary operation which satisfies (22). Assume finite alphabets Σ and Γ, a surjective function f : Σ → Γ, and a language L ⊆ T Σ that is recognized by a subset S ⊆ A of a finite T -algebra A; in other words, L = ← − h (S) for some T -algebra homomorphism h : T Σ → A. We will show that − → T f (L) is recognized by a finite T -algebra.
To this end, define a T -algebraĀ The intuition is that a tree t ∈ T Γ will be mapped to a value (α L , α R ) ∈Ā such that α L contains those values in A that can be attained by trees in T Σ which are mapped to t and which are left sons of their parents. Similarly, α R will stores values for trees that are right sons of their parents.
Formally, a binary operation • is defined by: where • on the right-hand side of the definition denotes the operation in A. It is not difficult to check that this defines a T -algebra, i.e., that the equation holds for all α L , α R , β L , β R , γ L , γ R ⊆ A. The (slightly) more involved case is the right-to-left inclusion, where one needs to use the equation (22) for A. For the left-to-right inclusion even that is not needed. A homomorphismh : T Γ →Ā is the unique extension of the function that maps every letter a ∈ Γ to (note that h • η Σ : Σ → A is the interpretation of single letters from Σ in the algebra A). Now define a subsetS ⊆Ā by: This subset recognizes the direct image − → T f (L). More explicitly, for any tree t ∈ T Γ, one has h(t) ∈S if and only if t = T f (r) for some r ∈ T Σ such that h(r) ∈ S. Both implications are proved by a straightforward induction on the size of t.

Counterexamples
In this section, we illustrate cases where direct images of recognizable languages along surjective letter-to-letter homomorphisms are not recognizable. One such case, Monad 7, was shown in Section 3. Here we provide three more.
Monad 25. Define a functor T on Set by: with the action on fuctions defined componentwise. It is easy to check that this is well-defined, i.e., that w ⊒ β implies f + (w) ⊒ Bf (β).
T carries a monad structure where both unit and multiplication are componentwise inherited from the monads (−) + and B. Again, it is straightforward to check that this is well defined. To get some intuition, an element of T Σ can be understood as a finite, nonempty word over the alphabet Σ with some positions marked, except that it is not specified exactly which positions those are; we only know how many positions labeled with every letter are marked. So, for example, markings aabcab aabcab and aabcab denote the same element of T {a, b, c}. This intuition is useful because it allows for a simple presentation of the monad structure: the unit of a ∈ Σ is unambiguosly presented as a and multiplication can be illustrated as, for example: (abac)(abb)(abac)(bac) → abacabbabacbac.
This monad has a simple equational presentation over an algebraic signature that consists of one binary symbol • and one unary symbol •. Using the terminology of marked words, the intuition will be that • is an operation that concatenates two words, and • erases the marking from every letter in a word. The equations are as follows: x y x The first three equations ensure that every element of T Σ can be presented as a marked word over Σ, and the last equation characterizes the equivalence of marked words described above. This completes our exhibition of the monad T . Now, for the alphabet Σ = {a, b}, consider the language L ⊆ T Σ defined by: Using the presentation by marked words, L consists of all words of the form abab · · · ab.
We claim that L is recognizable by a finite T -algebra. Intuitively, this is because a word w ∈ L cannot be obtained by concatenating or erasing marks from any other marked words, except by concatenating subwords of w or perhaps erasing a mark from a single letter b. Intuitively, the value BA represents those sub-words of words from L that begin with b and end with a; analogously for AA, AB and BB, except that the latter value represents only words other than the singleton b. That word is represented by a separate value B. The value B represents a singleton marked letter b. Finally, ⊥ is an error value, representing those words that cannot be completed to a word in L by erasing marks from all letters or by concatenating with other words.
Relying on the equational presentation of T , to define a T -algebra on A it is enough to define operations • and • on it. The multiplication table for x • y is: Note that B and BB behave in the same way in this table, and similarly for B and ⊥. However, these pairs of values are distinguished by the operation •, which is defined by: It is easy to check that the operations defined this way satisfy the equational theory of T given above, therefore they make A a T -algebra. Since T Σ is a free T -algebra on Σ, any function from Σ to the set A extends uniquely to a homomorphism from T Σ to the algebra A. Let h be the homomorphism that extends the function mapping a to AA and b to B. Then we have, for every w ∈ T Σ: Now consider an alphabet Y = {c} and the unique function f : Σ → Γ, which maps both a and b to c. The direct image of L under T f is: Using the presentation by marked words, this language consists of all words of the form cccc · · · cc = n times cc · · · cc cc · · · cc n times . This language is not recognizable by any finite T -algebra. For assume any homomorphism h from T Γ to some finite algebra A, and consider w 1 , w 2 , w 3 , . . . ∈ T Γ defined by: Since A is finite, there are some n = m such that h(w n ) = h(w m ). Now consider v = (c n , [c → 0]) = c n ∈ T Γ.
We have that but w n v belongs to the direct image (24) and w m v does not, so h does not recognize the direct image.

The balanced associativity monad
Monad 26. Consider a monad T presented by a single binary symbol • and a single equation: Elements of T Σ do not have a canonical form as simple and intuitive as for the marked words monad, but we shall need only a limited understanding of them. First, notice that for any a ∈ Σ, t ∈ T Σ and n ≥ 1 there is: This is proved by simple induction on n. The base case n = 1 is simply (25) with x = a and y = t, and for the induction step calculate: (on the left, the shaded pattern is repeated n times). This is again proved by induction. The base case n = 1 is (25) with x = a and y = c, and for the induction step calculate: for n ≥ 1. Note that the equation (25) does not apply anywhere in such a tree, so every tree of this shape forms a singleton equivalence class with respect to the congruence induced by (25). It is easy to recognize L with an algebra of six values: with the operation • interpreted by: and x • y = ⊥ for all other combinations of x, y ∈ A. It is easy to check that equation (25) holds in this algebra, indeed for all x, y ∈ A.
Then the unique homomorphism from h : T Σ → A that maps a to a, b to b and c to c recognizes L: t ∈ L ⇐⇒ h(t) = L.
Now consider an alphabet Γ = {a, c} and a function f : Σ → Γ: The direct image of L under T f consists of words as in the equation (27). This language is not recognizable by any finite T -algebra. For assume any homomorphism from T Γ to some finite algebra A, and consider t 1 , t 2 , t 3 , . . . ∈ T Γ defined by: Since A is finite, there are some n = m such that h(t n ) = h(t m ). Then the terms • • a t n a n times and • • a t m a n times have the same value under h, but the one on the left is in the direct image of L along T f (due to (27)) and the one on the right is not, so h does not recognize the direct image.

The not-quite-Mal'cev monad
Recall Monad 12, presented by a ternary operation symbol p and a unary operation symbol s subject to the equations p(x, x, y) = s(y) = p(y, x, x).
If, additionally, there were s(y) = y, then the monad would immediately have a Mal'cev term and the machinery of Section 4.2 would apply. 3 Note that any algebra for a monad that has a Mal'cev term induces a T -algebra on the same set. For instance, if (G, ·, e) is a group, then (G, p, s), where p(x, y, z) := x · y −1 · z and s is the identity function, is a T -algebra. A finite T -algebra that does not have a Mal'cev term is P = ({0, 1, 2, 3, 4, 5, 6}, p, s) where p is defined as:  On the other hand, if t 1 = t 2 ∈ T Γ then the direct image of L does not contain the term p(s(t 1 ), s(t 2 ), a).
Since T Γ is infinite, for any homomorphism g from T Γ into a finite T -algebra A there are some terms t 1 = t 2 such that g(t 1 ) = g(t 2 ). Then the terms s(a) = p(s(t 1 ), s(t 1 ), a) and p(s(t 1 ), s(t 2 ), a) are mapped to the same value by g, but only the former one belongs to the direct image of L along T f .

Related problems
Our main focus has been on recognizable languages being preserved under taking direct images of surjective letter-to-letter homomorphisms. This is because, in the proof of Proposition 1, which concerns the particular example of the monad of finite words, direct images are taken only along projection homomorphisms that arise from the logical existential quantifier; those homomorphisms are indeed surjective and letter-to-letter. It therefore makes sense to incorporate this particular closure property in an abstract definition of MSO for other monads. However, it should be noted that Proposition 1 would remain true if surjective letter-toletter homomorphisms were replaced in its statement by arbitrary letter-to-letter, or indeed by arbitrary homomorphisms. The corresponding closure property would become stronger, so one may expect some monads to become non-examples for these more restrictive variants of monadic MSO. In this section we identify some of these monads.

Homomorphisms that are not letter-to-letter
First, let us consider preserving recognizable languages under taking direct images of arbitrary T -algebra homomorphisms, i.e. ones that arise from functions f : Σ → T Γ via Kleisli lifting (as opposed to letter-to-letter homomorphims, which are of the form T f : T Σ → T Γ for a map f : Σ → Γ). This preservation property fails even for very basic monads, such as commutative monoids and seminearrings: Another counterexample is: A seminearring is a set equipped with two monoids, i.e., associative binary operations + and · (called horizontal and vertical composition; the latter is usually denoted simply by juxtaposition) with units respectively 0 and 1, subject to additional axioms (x + y)z = xz + yz and 0x = 0.
As expected, the free seminearring monad T is presented by the equational theory of seminearrings. This is a rather fundamental monad from the perspective of logic: in [40,Sec. 6] it is explained how seminearrings are a reasonable choice for an algebra of trees. Indeed, the free seminearring over a set Σ is the set of all unranked forests with holes (called multicontexts in [40]). f (ab n + ab n ) = f (ab n + ab m ).

Letter-to-letter homomorphisms that are not surjective
One may also consider the preservation of recognizable languages under direct images along arbitrary (i.e. not necessarily surjective) letter-to-letter homomorphisms. In all our counterexamples in Section 7, the failure of preservation seems to be caused by different letters being identified by a homomorphism; in other words, non-injectivity of homomorphisms seems to be the key issue. One may wonder if additionally requiring preservation under non-surjective homomorphisms changes the picture at all. As it turns out, it does. is not recognizable. Indeed, it is not finitely rectangular according to the terminology of Section 6.1 (and, being a singleton, it is not a union of finitely rectangular sets either), so its recognizability would contradict Lemma 27.
Example 33. Recall Monad 23, the monad whose finite models are trivial from Section 6.3. If we consider the inclusion ι : {x} → {x, y} then the direct image of the recognizable language L = T ({x}) under T ι is not recognizable. Indeed, the only recognizable languages are ∅ and T X for any finite X since the only finite model is the trivial model, but L is not one of those languages.
Example 34. Recall Monad 22, the free lattice monad FL from Section 6.2. We shall consult the first chapter of [41] for basic facts about free lattices. First, the following theorem due to Whitman [42] provides an effective procedure for comparing two elements of a free lattice: Writing down terms to denote elements of free lattices, one usually implicitly applies the associativity laws and writes e.g. t 1 ∧ t 2 ∧ t 3 instead of (t 1 ∧ t 2 ) ∧ t 3 . With this convention in mind, the following canonical form of terms is considered: Definition 36. In a free lattice FL(Σ), a formal join t = t 1 ∨ · · · ∨ t n with n > 1 is in canonical form if: • each t i is in Σ or a formal meet in canonical form, • t i ≤ t j for all i = j, • if t i = t ij then t ij ≤ t for all j.
Dual conditions define the canonical form of formal meets.
By [41,, every element in FL(Σ) can be presented by a term in canonical form, and moreover this presentation is unique up to commutativity laws.
It will be important to us that Definition 36 provides a procedure for transforming a term t into canonical form, and that this procedure relies only on removing some redundant subterms from t. As a corollary, if an element in a ∈ FL(Σ) is presented by a term t in canonical form such that some w ∈ Σ appears in t, then a cannot be presented by any term where w does not appear. Indeed, if such a presentation t ′ existed then the canonical form of t ′ would not contain w either, which would contradict the uniqueness of canonical presentation.
The last basic fact about free lattices that we shall need is that for |Σ| ≥ 3 the lattice FL(Σ) is infinite and it contains a strictly increasing infinite chain (see [41,Ex. 1.24]). Now let Σ = {p, q, r} Γ = {p, q, r, s} with ι : Σ → Γ the inclusion function. The language L = T Σ ⊆ T Σ is recognizable by the unique homomorphism to the one-element lattice. We shall show that its direct image − → T ι(L) ⊆ T Γ is not recognizable.
To this end, for any pair of terms t 1 < t 2 ∈ − → T ι(L), consider the term t = (t 1 ∨ s) ∧ t 2 .
Using Theorem 35, it is easy to check that s is incomparable with both t 1 and t 2 , and that t 1 < t < t 2 . Moreover, if t 1 and t 2 are in canonical form then so is t; to prove this use again Theorem 35 and the fact that s is incomparable with t 1 , t 2 and all their subterms. As a result, t cannot be presented by any term where the generator s does not appear; in other words, t ∈ − → T ι(L).
We have just proved that between any two distinct but ordered elements of − → T ι(L) there is some element not in − → T ι(L). Recall that FL(Σ) contains a strictly increasing infinite chain, and since T ι is an injective function, the set − → T ι(L) also contains a strictly increasing infinite chain. Inserting an element out of − → T ι(L) between each two neighbouring elements in that chain, we obtain an infinite, strictly increasing chain that alternates between elements that are in and out of − → T ι(L). This implies that the set − → T ι(L) is not recognizable.
It should be mentioned that for a weakly cartesian monad T , the class Rec T is in fact closed under direct images of all (not necessarily surjective) letter-to-letter homomorphisms. The proof of this is the same as in Section 5.3 but with the full powerset functor P used instead of P + . Only two points are worth making in this case: (1) the "projection" π 2 : ∈ X → PX is no longer surjective (the empty set is not in the image) and (2) the empty set plays the role of an "error state" in a powerset algebra (every letter that is not in the image of the function g is mapped to the empty set and any "operation" that involves the empty set has the empty set as a result).

Future work
Technically, our main object of study in this paper was a notion: a monad for which languages recognizable by finite algebras are closed under taking direct images along surjective letter-toletter homomorphisms. For such monads the abstract definition of monadic MSO makes sense, in that it only describes recognizable languages. Our various sufficient conditions, examples and counterexamples show that the notion seems rather subtle, but they do not provide a full characterization of it. The search for such a characterization is an obvious direction of further study.
It should also be said that the notion itself is a result of a few design decisions. It could be that its variants, such as the ones described in Section 8, lead to simpler characterizations while still covering essentially the same class of practically relevant examples. Some other design decisions we have not even mentioned: for example, is an arbitrary finite algebra the right notion of a recognizing device? Sometimes, in particular for infinitary monads, the answer might not be obvious, and one may want to consider a restricted class of finite algebras instead. (Note that, for an infinitary monad, a finite algebra may not admit a finite description.) Similarly, it is not clear whether one should not restrict even further the class of homomorphisms to take direct images along. This design space deserves careful exploration.
We focussed our attention on monads on the category of sets, but this leaves several natural examples out of scope. For example, the category of ranked sets is a convenient setting to study various algebras of trees and graphs. Other interesting base categories include that of vector spaces, or that of nominal sets. Another interesting idea is to employ the topo-algebraic technology of [43,44], where recognizability of word languages is studied beyond the regular setting. In general, any category where a meaningful notion of direct image of a language can be formulated, may be a territory worth exploring.
The most ambitious goal is to go beyond the "definable ⇒ recognizable" implication of the correspondence between MSO definability and recognizability of languages. Is there a generic version of the converse implication? How far can Proposition 1 be generalized? What about decidability questions about MSO? The paper [14] makes some initial steps in these and other related directions. However, much remains to be done, all in the spirit of bridging the divide between Structure and Power.