Achim Blumensath
email: blumensath@mathematik.tu-darmstadt.dejanin@labri.fr

David Janin

A syntactic congruence for languages of birooted trees

The study of languages of labelled birooted trees, that is, elements of the free inverse monoid enriched by a vertex labelling, has led to the notion of quasi-recognisability. It generalises the usual notion of recognisability by replacing homomorphisms by certain prehomomorphism into finite ordered monoids, called adequate, that only preserve some products: the so-called disjoint ones. In this paper we study the underlying partial algebra setting and we define a suitable notion of a syntactic congruence such that (i) having a syntactic congruence of finite index captures MSO-definability; (ii) a certain order-bisimulation refinement of the syntactic congruence captures quasi-recognisability in the same way.

Introduction

When modelling systems and concepts, it is sometimes handy to consider objects that are composed of overlapping parts. A formal framework for the composition of such overlapping objects is given by the theory of inverse semigroups [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF]. Recent applications of this theory include the modelling of music [START_REF] Janin | Vers une modélisation combinatoire des structures rythmiques simples de la musique[END_REF], interactive music systems [START_REF] Berthaut | Advanced synchronization of audio or symbolic musical patterns: an algebraic approach[END_REF][START_REF] Janin | Multi-scale design of interactive music systems : the libTuiles experiment[END_REF], and distributed systems [START_REF] Dicky | Modélisation algébrique du diner des philosophes[END_REF]. As already observed in [START_REF] Kellendonk | The local structure of tilings and their integer group of coinvariants[END_REF][START_REF] Kellendonk | Tiling semigroups[END_REF] and developed further in [START_REF] Janin | Towards a higher dimensional string theory for the modeling of computerized systems[END_REF], inverse semigroup theory conveys a notion of a higher dimensional string that seems particularly relevant in the context of such applications. This is especially clear in view of Stephen's representation theorem for inverse semigroups [START_REF] Stephen | Presentations of inverse monoids[END_REF] that allows us to define graphical representations of elements of an inverse semigroup. These observations motivate the development of a formal language theory based on the theory of inverse semigroups.

However, the tools of classical formal language theory are not easily applicable for such a purpose. As already observed and studied in detail for languages in the free inverse monoid [START_REF] Silva | On free inverse monoid languages[END_REF], that is, languages of birooted trees, the notion of algebraic recognisability by means of morphisms into finite monoids leads to a notion with rather weak expressive power. Further study of these languages in the context of tree walking automata has led to a strict hierarchy of classes of languages [START_REF] Janin | Walking automata in the free inverse monoid[END_REF] ranging from recognisable languages (definable by means of finite monoids) to logically definable languages (definable in monadic second-order logic) and regular languages (definable with various notions of regular expressions).

It is known that the homomorphic image of an inverse monoid is an inverse monoid. When applied to inverse semigroups, the automata stemming from morphisms into finite monoids are reversible in a certain sense [START_REF] Margolis | Languages and inverse semigroups[END_REF][START_REF] Silva | On free inverse monoid languages[END_REF]. Although leading to interesting studies of reversible computations (see [START_REF] Danos | Reversible, irreversible and optimal lambda-machines[END_REF] for instance), morphisms of inverse monoids preserve far too much structure to be used as a tool for language definability. The collapse of expressive power arises even in the absence of inverses themselves as illustrated by languages of positive birooted words [START_REF] Janin | On languages of one-dimensional overlapping tiles[END_REF] or languages of partially ordered graphs [START_REF] Courcelle | The recognizability of sets of graphs is a robust property[END_REF].

These observations lead us to the definition and the development of a more expressive notion of language definability, called quasi-recognisability. This notion is based on relaxing homomorphisms into adequate premorphisms. While a homomorphism of monoids preserves products, i.e., ϕ(xy) = ϕ(x)ϕ(y), adequate premorphisms of ordered monoids are only required to be monotonic and submultiplicative, i.e., ϕ(xy) ≤ ϕ(x)ϕ(y), effectivity being ensured by additional preservation properties.

Applied first to languages of birooted words [START_REF] Janin | On languages of one-dimensional overlapping tiles[END_REF][START_REF] Janin | Quasi-recognizable vs MSO definable languages of one-dimensional overlapping tiles[END_REF], that is, subsets of the monoid of McAlister [START_REF] Mcalister | Inverse semigroups which are separated over a subsemigroups[END_REF][START_REF] Lawson | McAlister semigroups[END_REF], and then to languages of labelled birooted trees [START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF], this emerging notion of a quasi-recognisable language has been successfully related to classical automata theory. It has also been shown to 'essentially' capture definability by means of MSO-formulae [START_REF] Janin | Overlaping tile automata[END_REF][START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF]. Hence, it provides new algebraic tools for the study of MSO-definable languages of finite trees [START_REF] Thomas | Chap. 7. Languages, automata, and logic[END_REF].

At the moment the theory of quasi-recognisable languages is far from being fully understood. It turns out that the notion of an adequate premorphism is related to two fields of algebra: the theory of partially ordered monoids (adequate premorphisms are order preserving) and the theory of partial algebras (adequate premorphisms preserves a partial operation called the disjoint product).

In this paper we continue the study of languages of birooted trees and we make these connections with the theories of partial algebras and ordered monoids explicit. In short, we show that the theory of partial algebra provides effective tools to characterise MSO-definable languages of birooted trees. Additionally, the theory of partially ordered monoids provides, via the notion of quasirecognisability, a more subtle description of (a large subclass of) these languages. This can be seen as a further example of the use of partially ordered monoids in algebraic language theory [START_REF] Pin | Algebraic tools for the concatenation product[END_REF].

The paper is organised as follows. In the next section, we recall the basic notions from algebra we will need. We quickly review the definitions of a labelled birooted tree, the corresponding monoid, the operations of left and right projection, and the natural order on birooted trees. These notions are taken from the theory of inverse semigroups. We refer the reader to [START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF] for more details on the inverse monoid of labelled birooted trees. A thorough introduction to the theory of inverse semigroups can be found in [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF].

The disjoint product of birooted trees -a notion that plays a key role in quasi-recognisability [START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF] -is reviewed in Section 3. This operation provides a link to the theory of partial algebras [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF] which is exploited in this paper. In particular, we consider the notion of a closed * -congruence (cf. Definition 3.3). The closure property, which plays a central role in the theory of partial algebras, is characterised over birooted trees by means of their so-called root type (cf. Proposition 3.8).

In Section 4, we prove that every language of birooted trees admits a syntactic congruence, that is, a greatest closed * -congruence saturating the language (cf. Theorem 4.2). Then we prove that the syntactic congruence of a language has finite index if, and only if, the language is definable in monadic second-order logic (cf. Theorem 4.7). In this case we also obtain a linear time membership algorithm (cf. Theorem 4.8).

Quasi-recognisable languages, which capture finite boolean combinations of upward closed MSO-definable languages [START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF], are considered in Section 5. The notion of a bisimulation refinement of a closed * -congruence (cf. Definition 5.2) is defined and shown to exist. Quasi-recognisable languages are then characterised by means of the bisimulation refinement of their syntactic congruence (cf. Theorem 5.18).

Birooted labelled trees

Throughout the paper we fix two finite alphabets A = {a, b, c, . . . } of edge labels and F = {f, g, h, . . . } of vertex labels. We assume that A is non-empty, while F is allowed to be empty. Let Ā := {ā, b, c, . . . } be a disjoint copy of A and set A = A + Ā. We define the syntactic inverse mapping x → x -1 from A to itself by a -1 = ā and ā-1 = a, for a ∈ A. This mapping is extended to A * by setting 1 -1 := 1 and (au) -1 := u -1 a -1 for a ∈ A and u ∈ A * .

The free group FG(A) generated by A is the quotient of A * under the congruence generated by the equations aā = 1 and āa = 1 for a ∈ A. Every equivalence class [u] ∈ FG(A) is uniquely determined by the unique word red(u) obtained from u by applying the rewriting rules aā → 1 and āa → 1 for a ∈ A. In the sequel, we thus shall represent elements of FG(A) by their reduced form. In that case, the group product u • v of two elements u, v ∈ FG(A) is defined by u • v = red(uv), and elements of FG(A) are partially ordered by the prefix order (defined over their reduced forms). Then, for every u ∈ FG(A), we have

u -1 ∈ FG(A) and u • u -1 = 1 = u -1 • u,
that is, the syntactic inverse u -1 of u coincides with its group inverse.

Definition 2.1 (Birooted labelled trees).

A (vertex-labelled) birooted tree is a pair x = r, u where r : FG(A) → F ∪ { } is a partial mapping with a prefix-closed domain dom(r) ⊆ FG(A) and u ∈ dom(r) is a distinguished vertex called the output root. The unit vertex 1 ∈ dom(r) is called the input root.

In the case where the alphabet F contains at least two elements 1 , the set of birooted trees is extended by a zero element 0. The set of all birooted trees is denoted by B(F, A).

The product x • y of two non-zero birooted trees x = r, u and y = s, v is the birooted tree t, w where dom(t) = dom(r) ∪ u • dom(s) and, for every z ∈ dom(t),

t(z) =      r(z) if z ∈ dom(r) -u • dom(s) , s(u -1 • z) if z ∈ u • dom(s) -dom(r) , r(z) ∧ s(u -1 • z) if z ∈ dom(r) ∩ u • dom(s) .
The meet in the last clause of the definition is computed with respect to the trivial order on F ∪ { } where x ≤ y iff x = y or y = . The product is set to 0 if, for some z, the above meet does not exists, i.e., the labels of r and s at the respective places disagree. We extend the product to 0 by defining x•0 = 0 = 0•x for all x ∈ B(F, A). As usual, we may omit the dot and simply write xy instead of x • y.

An example of labelled birooted trees and products is depicted Figure 1. The input/output roots are marked by dangling incoming/outgoing arrows. Directed edges are only labelled by letters of A, letters of Ā implicitly labelling the reverse of these edges. Observe that, when both x = r, u and y = s, v are non-zero birooted trees, the necessary and sufficient condition for the product x • y to be non-zero is that for every v ∈ dom(s), if uv ∈ dom(s) then we have either t(uv ) = , or s(v ) = , or r(uv ) = s(v ).

As special cases of birooted trees there are elementary birooted trees that are either 0 or consist of a single vertex or a single edge. For all f ∈ F and a ∈ A, there are elementary birooted trees f and a that are defined as follows. The former have a single vertex labelled f , while the latter consist of a single edge labelled a that connects two vertices with label . The formal definitions are f := {1 → f }, 1 and a := {1 → , a → }, a . The neutral element of B(F, A) is the one vertex birooted tree with label formally defined by 1 := {1 → }, 1 .

Most of the properties of birooted trees and their product follows from the following theorem. For the sake of completeness, let us recall that a monoid M is an inverse monoid when, for each x ∈ M , there exists a unique element x -1 ∈ M , called the semigroup inverse of x, such that xx -1 x = x and x -1 xx -1 = x -1 .

Theorem 2.2 ([9], [19]

). The set B(F, A) equipped with the above product is an inverse monoid. It is the quotient of the free inverse monoid FIM(F + A) by the identities f f = f and f g = 0, for f, g ∈ F with f = g, and it is generated by the elementary birooted trees. For F = ∅, the monoid B(∅, A) is just the free inverse monoid FIM(A) itself.

As both alphabets are fixed throughout the paper, we shall simply write B for the set of birooted trees over F and A.

Below we review some basic notions and properties of the monoid B that follow from its definition and the fact that it is an inverse monoid. A detailed presentations of inverse semigroup theory can be found in [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF].

First, note that 0 -1 = 0. The case of non-zero birooted trees is described in the following lemma.

Lemma 2.3 (Inverses and idempotent). The inverse of a non-zero birooted tree

x = r, u is x -1 = r u , u -1 where dom(r u ) = u -1 • dom(r) and r u (v) = r(u • v) , for v ∈ dom(r u ) .
Moreover, x is idempotent if, and only if, u = 1.

The next definition plays a fundamental role in our approach.

Definition 2.4 (Resets and co-resets). The right projection, or reset, of an element

x ∈ B is the element x R := x • x -1 . Its left projection, or co-reset, is x L := x -1 • x.
We easily check that x R x = x = xx L , x R x R = x R , and x L x L = x L . Since idempotents are self inverse, this implies that the reset mapping x → x R and the co-reset mapping x → x L are both projections from the set of birooted trees into the set of idempotents.

As is well known in inverse semigroup theory, these projections are related to Green's relations as follows: for x, y ∈ B, we have x L = y L if, and only if, x and y are L-equivalent, and x R = y R if, and only if, they are R-equivalent.

Definition 2.5 (Natural order).

The natural order ≤ on B is defined by

x ≤ y :iff x = x R • y (equivalently x = y • x L ).
It can be shown that, as in any inverse monoid, a birooted tree x ∈ B is idempotent if, and only if, x ≤ 1, that is, the idempotents are exactly the subunits. The set of idempotent elements of B is thus denoted by U (B) := {x ∈ B : x ≤ 1}. In adequately ordered monoids, which we will introduce below, this is no longer the case, as there may be idempotents that are not subunits.

Every non-zero birooted tree x = s, u can be seen, as depicted in Figure 1, as a relational structure M x with domain dom(s) over the signature A+F+{in, out}, where the symbols in A are interpreted as binary relations, those in F are interpreted as disjoint unary relations, and there are two distinguished vertices in, out ∈ dom(x) representing the input and output root. Encoding zero by the one vertex structure M 0 with non-empty interpretations of every symbol of F or A, the natural ordered can then be characterised as follows.

Lemma 2.6. Let x and y be two birooted trees. Then x ≤ y if and only if there is a morphism ϕ : M y → M x that preserves input and output root. For x = 0, this morphism is injective. Remark 2.7. Using such a representation of all birooted trees as structures, we can consider subsets of B that are definable in a given logic, say, in monadic second-order logic. The study of MSO-definable languages of birooted trees by means of algebraic methods is one of the main purpose of this paper.

The disjoint product

The disjoint product, introduced in [START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF], turns the algebra of birooted trees into a (finitely generated) partial algebra [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF] over the signature consisting of the partial disjoint product, the total reset and co-reset operations, and (if necessary) the constant 0.

The associated notion of a congruence of partial algebras [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF], called a *congruence in this paper, will lead us in the next section to the syntactic congruence of a language. Definition 3.1 (Disjoint product). The partial disjoint product x * y of two elements x, y ∈ B is equal to their usual product x • y if the following two conditions are satisfied:

(D1) x • y = 0, (D2) x = r, u , y = s, v , and dom(r) ∩ u • dom(s) = {u}.
Otherwise, the disjoint product is left undefined. We shall write ∃x * y to denote both the existence of such a partial product and its value.

It is straightforward to check that the disjoint product is associative in the following sense: the disjoint product x * (y * z) is defined if, and only if, (x * y) * z is defined and, if this is the case, both products are equal.

The following lemma shows that the set of birooted trees is a finitely generated partial algebra [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF].

Lemma 3.2 (Strong decomposition [9]). Every birooted tree x ∈ B can be written as a combination of elementary birooted trees by disjoint products, reset and co-reset projections. This combination can be chosen to be of linear size in the number of vertices of x.

The following definition is adapted from the theory of partial algebras (see [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF] Sections 2.4-2.6) albeit with different terminology. (b) We call an equivalence relation on B idempotent pure if it does not identify an idempotent with a non-idempotent.

Proposition 3.4 (Lattice property [2]). The set of * -congruences ordered by inclusion is a meet semi-lattice with intersection as meet. The set of closed

* -congruences ordered by inclusion is a lattice with intersection as meet and the transitive closure of union as join.

Proof. This essentially follows from standard results for partial algebras [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF]. We present the proof for the sake of completeness.

Let R 1 and R 2 be two * -congruences. Clearly, the intersection

R 1 ∩ R 2 is also a * -congruence. Furthermore, if both R 1 and R 2 are closed, then so is R 1 ∩ R 2 . Let R 1 R 2 := (R 1 ∪ R 2 ) + be the transitive closure of the union R 1 ∪ R 2 . Since both R 1 and R 2 are reflexive, we have R 1 R 2 = (R 1 ∪ R 2 ) * = {(R 1 ∪ R 2 ) n : 0 ≤ n < ω} . It suffices to check that the relation R 1 R 2 is a closed * -congruence. By definition it then follows that it is the least closed * -congruence containing both R 1 and R 2 . Let (x, x ), (y, y ) ∈ R 1 R 2 . Since R 1 ∪ R 2 is reflexive,
we can find a number n such that (x, x ), (y, y ) ∈ (R 1 ∪ R 2 ) n . We check Properties (P1)-(P3) by induction on n.

We start with (P1) and (P3). Assume that ∃x * y. If n = 0, then x = x and y = y . Consequently, ∃x * y and (x * y, x * y ) ∈ R 1 R 2 . Hence, suppose that n = m + 1, for some m. Then there exists x ∈ B such that (x, x ) ∈ (R 1 ∪ R 2 ) m and (x , x ) ∈ R i for some i ∈ {1, 2}. By inductive hypothesis, ∃x * y implies ∃x * y and (x * y, x * y

) ∈ R 1 R 2 . But since R i satisfies (P3) with (x , x ) ∈ R i we also have ∃x * y . Hence, (P1) implies that (x * y , x * y ) ∈ R i ⊆ R 1 R 2 . It follows, by transitivity of the relation R 1 R 2 , that (x * y, x * y ) ∈ R 1 R 2 .
The case of Property (P2) is treated similarly. We want to prove that we both have

(x L , x L ) ∈ R 1 R 2 and (x R , x R ) ∈ R 1 R 2 .
If n = 0, then x = x and we are done. Hence, suppose that n = m + 1. Then there exists z ∈ B such that

(x, z) ∈ (R 1 ∪R 2 ) m and (z, x ) ∈ R i for some i ∈ {1, 2}. By inductive hypothesis, this implies that (x L , z L ) ∈ R 1 R 2 and (x R , z R ) ∈ R 1 R 2 . Since R i satisfies (P2) it also follows that (z L , x L ) ∈ R i ⊆ R 1 R 2 and (z R , x R ) ∈ R i ⊆ R 1 R 2 .
We conclude by transitivity.

Definition 3.5 (Root types). The root type of a subunit

z ∈ U (B) is the set rtp(z) := {f ∈ F : zf = z} ∪ {a ∈ A : za R = z}
where we omit the elements of F in the case that |F| ≤ 1.

Clearly, we have rtp(0) = F ∪ A when |F| ≥ 2 (resp. rtp(0) = A when |F| ≤ 1) and, for every non-zero idempotent birooted tree z = t, 1 , we have rtp

(z) = {t(1)} ∪ dom(t) ∩ A when |F| ≥ 2 (resp. rtp(z) = dom(t) ∩ A). In all cases, if z 1 ≤ z 2 ≤ 1 then we have rtp(z 1 ) ⊇ rtp(z 2 ).
Lemma 3.6. For all x, y ∈ B, we have

rtp(x L ) = rtp(y L ) iff ∃x * z ⇔ ∃y * z , for all z ∈ B , rtp(x R ) = rtp(y R ) iff ∃z * x ⇔ ∃z * y , for all z ∈ B .
Proof. (⇐) Assume that, for every z ∈ B, we have ∃z * x if, and only if, ∃z * y.

In the case where x = 0, the disjoint product x * 1 is undefined. Hence, y * 1 is also undefined. This implies that y = 0 and rtp(x R ) = rtp(y R ).

In the remaining cases we may assume, by symmetry, that neither x nor y equals 0. Hence, x = r, u and y = s, v . From the fact that ∃a * x ⇔ a / ∈ dom(s) ∩ A for all a ∈ A, we immediately deduce that rtp(x R ) ∩ A = rtp(y R ) ∩ A.

In the case where |F| ≥ 2, we also have ∃f * x ⇔ f ≤ r( 1) for all f ∈ F. Hence, it follows that rtp(x R ) ∩ F = rtp(y R ) ∩ F. Observe that, in the case where |F| ≤ 1, the vertex labelling plays no role in the definition of the disjoint product.

(⇒) Suppose that rtp(x R ) = rtp(y R ). A similar case study shows that for all z ∈ B we indeed have ∃x * z if, and only if, ∃y * z.

Symmetrical arguments show that the statement rtp(x R ) = rtp(y R ) is equivalent to the fact that, for every z ∈ B, we have ∃z * x if and only if ∃z * y.

Definition 3.7 (Root equivalence). The root equivalence is defined by

x ≈ rt y :iff rtp(x L ) = rtp(y L ) and rtp(x R ) = rtp(y R ) .

The strong root equivalence ≈ srt is defined by

x ≈ srt y :iff x ≈ rt y and x ∈ U (B) ⇔ y ∈ U (B) .
Proposition 3.8. The relation ≈ rt is the greatest closed equivalence. The relation ≈ srt is the greatest idempotent-pure closed * -congruence. Both equivalences have finite index.

Proof. Clearly, ≈ rt is an equivalence and it satisfies (P3), by Lemma 3.6. Hence, it is closed. It follows by Lemma 3.6 that it is the greatest such relation.

It is easy to see that ≈ srt is the greatest idempotent-pure closed equivalence. It therefore remains to show that it is a * -congruence.

Property (P2) easily follows from the observation that, for all idempotents x, y ∈ B, we have x ≈ srt y if, and only if, rtp(x) = rtp(y). Indeed, suppose that x ≈ srt y. Since ≈ srt ⊆ ≈ rt , this means in particular that rtp(x R ) = rtp(y R ). Hence x R ≈ srt y R as both x R and y R are idempotent and idempotents are invariant under projections.

Property (P1) can be proved by a case distinction. Suppose that x * y is defined.

• If both x and y are idempotent then

rtp((x * y) L ) = rtp((x * y) R ) = rtp(x) ∪ rtp(y) . • If x is idempotent and y is not idempotent then rtp((x * y) L = rtp(y L ) and rtp((x * y) R ) = rtp(x) ∪ rtp(y R ) . • Similarly, if x is not idempotent and y is idempotent then rtp((x * y) L ) = rtp(x L ) ∪ rtp(y) and rtp((x * y) R ) = rtp(x R ) . • If neither x nor y is idempotent then rtp((x * y) L ) = rtp(y L ) and rtp((x * y) R ) = rtp(x R ) .
To see that (P1) holds, consider elements x ≈ srt x and y ≈ srt y such that x * y and x * y are defined. By definition of ≈ rt , we have rtp(x L ) = rtp(x L ), rtp(x R ) = rtp(x R ), rtp(y L ) = rtp(y L ) and rtp(y R ) = rtp(y R ). As ≈ srt is idempotent pure, it follows in all of the above cases that rtp((x * y) L ) = rtp((x * y ) L ), rtp((x * y) R ) = rtp((x * y ) R ), and x * y ∈ U (B) ⇔ x * y ∈ U (B). In other words, x * y ≈ srt x * y . Remark 3.9. (a) Note that, as soon as A is not a singleton, the relation ≈ rt is not a * -congruence. Although it satisfies axiom (P2), it does not satisfies axiom (P1). Indeed, given x = a L a R and y = a L aa R , we have x ≈ rt y since rtp(x L ), rtp(x R ), rtp(y L ) and rtp(y R ) are all equal to {a, ā}. However, we have rtp((x * b) R ) = {a, ā, b} while rtp((y * b) R ) = {a, ā}.

(b) Note that a * -congruence needs not to be idempotent pure. An example is the relation R defined from the relation ≈ srt by adding all pairs of birooted trees x, y ∈ B such that rtp(x L ), rtp(x R ), rtp(y L ) and rtp(y R ) contains A. Clearly, the relation R satisfies axiom (P2). Moreover, we do have ≈ srt ⊂ R ⊂ ≈ rt . But no trees in these newly added pairs can be used in a disjoint product. The relation R thus satisfies Properties (P1) and (P3) just for the same reasons the relation ≈ srt satisfies them. Definition 4.1. A * -congruence saturates a set X ⊆ B if x y implies x ∈ X ⇔ y ∈ X , for all x, y ∈ B . Theorem 4.2. For every language X ⊆ B of birooted trees, there exists a greatest closed * -congruence X saturating X.

Proof. By Proposition 3.4, the supremum of all closed * -congruences saturating X exists. This supremum still saturates X. Definition 4.3. We call the relation X of the previous lemma the syntactic congruence of X.

If the syntactic congruence has finite index, we obtain an effective membership algorithm in the same way as for languages of words. To present this algorithm we need to define quotients of partial algebras. (a) The quotient B/ is the partial algebra whose elements are the congruence classes of elements of B and whose operations are as follows: for X, Y ∈ B/ , we define

X L := {x L ∈ B : x ∈ X} , X R := {x R ∈ B : x ∈ X} , X * Y := {z ∈ B : z ∃x * y, x ∈ X, y ∈ Y } ,
where X * Y is only defined if the above set is nonempty.

(b) A morphism of partial algebras is a function ϕ : A → B between partial algebras A and B such that, for all x, y ∈ A,

ϕ(x L ) = (ϕ(x)) L , ϕ(x R ) = (ϕ(x)) R , ∃x * y implies ϕ(x * y) = ∃ϕ(x) * ϕ(y) .
(c) The canonical surjection θ : B → B/ is the function mapping every element of B to its congruence class. Proof. Essentially follows from standard results for partial algebras [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF].

The relationship between the syntactic congruence and definability in monadic second-order logic [START_REF] Thomas | Chap. 7. Languages, automata, and logic[END_REF] is as follows. Recall that M x denotes the structure encoding a birooted tree x. Lemma 4.6. Let be a * -congruence of finite index. For every class X ∈ B/ , there exists an MSO-formula ϕ X such that

M x |= ϕ X iff x ∈ X , for all x ∈ B .
Proof (Sketch). The claim follows from Lemma 3.2 and the fact that B/ is finite: for every birooted tree x ∈ B, the value θ (x) can be defined in MSO by guessing a strong decomposition of x and a corresponding labelling in B/ , in almost the same way as the behaviour of a bottom up tree automaton over a finite tree can be described in MSO.

Theorem 4.7. A language X ⊆ B of birooted trees is definable in MSO if, and only if, its syntactic congruence X has finite index. Proof (Sketch). (⇐) As X saturates X, we can write X = x∈X [x] X . When the syntactic congruence has finite index, this union is finite. Consequently, the formula ψ X = x∈X ϕ [x] defines X, where ϕ [x] are the formulae from Lemma 4.6.

(⇒) If X is definable in MSO, we can use decomposition arguments (see [START_REF] Shelah | The monadic theory of order[END_REF] and [START_REF] Thomas | Ehrenfeucht games, the composition method, and the monadic theory of ordinal words[END_REF]) to prove that X has finite index. Two trees with the same MSOtheory (up to a given quantifier rank) cannot be distinguished by X; hence they must be X -equivalent. Since there are only finitely many such theories, it follows that X has only finitely many classes.

In the simpler setting of birooted words, that is, elements of the monoid of McAlister [START_REF] Lawson | McAlister semigroups[END_REF], a similar characterisation has already been achieved in [START_REF] Janin | On languages of one-dimensional overlapping tiles[END_REF].

Another consequence of Lemma 4.5 worth being mentioned concerns a membership decision algorithm. Theorem 4.8. Let X ⊆ B be a language whose syntactic congruence X has finite index. Given B/ X one can decide whether x ∈ X in time linear in the size of the input x ∈ B.

Proof. By Lemma 3.2, the set of birooted trees is finitely generated as a partial algebra. It follows that, starting from the elementary birooted trees we can inductively compute the image θ X (x) of a birooted tree x ∈ B under the canonical surjection θ X : B → B/ X . The number of steps is linear in the size of x. This proves the claim under the usual assumption that every projection, disjoint product, or equality test in the partial algebra B/ X takes constant time.

We provide here a strengthening of Lemma 4.2 that states the existence of the syntactic congruence in an arbitrary partial algebra over the signature of B. Furthermore, it shows that the syntactic congruence can be computed as the greatest fixed point of a certain mapping. For finite partial algebras, this provides an effective algorithm to compute the syntactic congruence of X from any given closed * -congruence of finite index saturating X. Lemma 4.9. Let C be a partial algebra with disjoint product and left and right projection. Assume that there is a greatest closed equivalence ≈ over C. For every closed relation R ⊆ ≈, let F (R) be the relation consisting of all pairs (x, y) ∈ R such that, for every z 1 , z 2 , z 3 ∈ C, the following properties are satisfied:

(a) (x L , y L ) ∈ R and (x R , y R ) ∈ R, (b) ∃x * z ∈ R ⇔ ∃y * z ∈ R and ∃z * x ∈ R ⇔ ∃z * y ∈ R, for every z ∈ C.
The function F is monotonic with respect to the inclusion order. Furthermore, for every X ⊆ C, there is the greatest closed * -equivalence X saturating X given by the transfinite equation:

X = α F α (≈ X ) where x ≈ X y :iff x ≈ y and x ∈ X ⇔ y ∈ X , and F 0 (R) = id, F α+1 (R) = F (F α (R)) and, F δ (R) = α<δ F α (R), for limit ordinals δ.
Proof. We first check that, if R is an equivalence relation then so is F (R). If R is closed, monotonicity of F then implies that F (R) is also closed. The fixed-point theorem of Tarski thus ensures that F has a greatest fixed point ∼ which is given by the above formula.

By monotonicity, we have ∼ ⊆ ≈ X . Hence, the relation ∼ saturates X. It remains to show that ∼ is a closed * -congruence. Indeed, given any closed *congruence ∼ saturating X, we can prove by induction on α that ∼ ⊆ F α (≈). Hence ∼ ⊆ ∼.

Since it is included in ≈, ∼ is a closed equivalence relation. It thus remains to show that ∼ is a * -congruence. It is straightforward to that Property (a) implies (P2) and Property (b) implies (P1).

Applied to the partial algebra B of birooted trees, this provides an alternative proof of Theorem 4.2. It also provides an effective way to compute the syntactic congruence of a recognisable language. This relation is obviously the greatest closed equivalence over B/ . Therefore, we can use Lemma 4.9 to obtain the greatest closed * -congruence ∼ ϕ(X) over B/ that saturates ϕ(X). For every x, y ∈ B, it follows that x X y if and only ϕ(x) ∼ ϕ(X) ϕ(y). Since every equivalence relation over B/ has index at most n, this relation can be computed in at most O(n) iteration steps (the depth of the lattice of equivalence relation ordered by inclusion) and each step is taking time at most O(n 2 ) (the size of the current relation times the number of possible applications of the separation rules (a) and (b)).

Application to quasi-recognisability

We aim now at a characterisation of quasi-recognisable languages via their syntactic congruence. We start by recalling the definition of quasi-recognisability. Definition 5.1 (Quasi-recognisable languages [START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF]). (a) A function ϕ : B → M from B into an ordered monoid M is an adequate premorphism if it satisfies the following conditions: (c) A language X ⊆ B is quasi-recognisable if there exists an adequate function ϕ : B → M into a finite adequately ordered monoid M such that

(M1) x ≤ y implies ϕ(x) ≤ ϕ(y), (M2) ϕ(xy) ≤ ϕ(x)ϕ(y), (M3) ϕ(x L ) = (ϕ(x)) L and ϕ(x R ) = (ϕ(x)) R , (M4) ∃x * y implies ϕ(x * y) = ϕ(x)ϕ(y).
X = ϕ -1 (ϕ(X)).
It is proved in [START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF] that quasi-recognisable languages corresponds to finite Boolean combinations of upward closed (in the natural order) MSO-definable languages. We now aim at characterising quasi-recognisable languages by means of their syntactic congruence. We need two new notions for this characterisation: that a of * -bisimulation and that of an alternating chain.

The kernel of an adequate premorphism into a finite ordered monoid is clearly a * -congruence of finite index. However, it does not need to be closed. Moreover, since the class of these languages is known to be strictly included into the class of MSO-definable languages3 , we will need additional requirements on the syntactic congruence to characterise such languages. The connections between the syntactic congruence and quasi-recognisability can be done as follows.

Definition 5.2 ( * -bisimulation).

A closed * -congruence is a * -bisimulation if it is idempotent pure and satisfies the property:

(P4) if x ≤ y z then there exists x x such that x ≤ z.
It is a strong * -bisimulation when, additionally, each -class is convex, i.e., (P5) if x ≤ y ≤ z and x z then x y z.

Lemma 5.3 (Lattice property). The set of * -bisimulations ordered by inclusion forms a complete lattice with transitive closure of the union as join.

Proof. Let R 1 and R 2 be two * -bisimulations over the set of birooted trees. By Proposition 3.4, we already know that the relation

R 1 R 2 = (R 1 ∪ R 2 ) * is a closed * -congruence. Since R 1 and R 2 are idempotent pure, so is R 1 R 2 . Let us prove that the relation R 1 R 2 is a * -bisimulation.
Consider elements x, y, y ∈ B with x ≤ y and (y,

y ) ∈ R 1 R 2 .
Then there is a number n < ω such that (y, y ) ∈ (R 1 ∪ R 2 ) n . If n = 0, then y = y and we can take x = x. Otherwise, there exists m < ω and y ∈ B such that n = m + 1 with (y, y ) ∈ (R 1 ∪ R 2 ) m and (y , y ) ∈ R i for some i ∈ {1, 2}. By inductive hypothesis, there exists x ∈ B such that (x, x ) ∈ R 1 R 2 and x ≤ y . As R i satisfies Property (P4), we can find an element x ∈ B such that (x , x

) ∈ R i ⊆ R 1 R 2 and x ≤ y . By transitivity, it follows that (x, x ) ∈ R 1 R 2 .
We have shown that the set of * -bisimulations forms a semi-lattice with as join. Since our proof clearly extends to an arbitrary number of * -bisimulations, this shows that the underlying semi-lattice is actually complete.

Since ≈ srt is the maximum idempotent-pure closed * -congruence and also a *bisimulation, there is a greatest * -bisimulation. Consequently, the * -bisimulations ordered by inclusion form a complete lattice. We give here a fixed point characterisation of the * -bisimulation refinement of a closed * -congruence. Before giving that characterisation, let us first note that the natural order is well-behaved in some sense with respect to projections and the disjoint product. (a) For every z ≤ x R , there exists x ≤ x such that z = x R . (b) For every z ≤ x L , there exists x ≤ x such that z = x L . (c) For every z ≤ x * y, there exist x ≤ x and y ≤ y such that z = x * y .

Proof. This easily follows from the embedding characterisation of the natural order stated in Lemma 2.6.

We consider the following function F on binary relations: F (R) := (x, y) ∈ R : for every x ≤ x there exists y ≤ y with (x , y ) ∈ R , for every y ≤ y there exists x ≤ x with (x , y ) ∈ R . Lemma 5.8. If R is an (idempotent-pure) closed * -congruence, then so is F (R).

Proof. Let R be a closed * -congruence. Clearly, F (R) is a closed equivalence. To prove that is a * -congruence we have to check two properties.

For (P1), let (x 1 , y 1 ), (x 2 , y 2 ) ∈ R and suppose that both x 1 * x 2 and y 1 * y 2 are defined. We have to show that (x 1 * x 2 , y 1 * y 2 ) ∈ F (R). Clearly, (x 1 * x 2 , y 1 * y 2 ) ∈ R as R satisfies (P1). Let z ≤ x 1 * x 2 . By Lemma 5.7, there exists x 1 , x 2 ∈ B such that z = x 1 * x 2 , x 1 ≤ x 1 , and x 2 ≤ x 2 . But since (x 1 , y 1 ) ∈ F (R), by definition, there exists y 1 ∈ B such that (x 1 , y 1 ) ∈ R and y 1 ≤ y 1 . Similarly, there exists y 2 ∈ B such that (x 2 , y 2 ) ∈ R and y 2 ≤ y 2 . Since R satisfies (P1) and it is closed, we have (x 1 * x 2 , y 1 * y 2 ) ∈ R. By monotonicity of the order, we have therefore found z = y 1 * y 2 ≤ y 1 * y 2 such that (z, z ) ∈ R. By a symmetrical argument, if we assume that z ≤ y 1 * y 2 then there exists z ≤ x 1 * x 2 such that (z , z) ∈ R. In other words, (x 1 * x 2 , y 1 * y 2 ) ∈ F (R). Hence, Property (P1) is satisfied.

For (P2), let (x, y) ∈ F (R). We have to show that (x R , y R ) ∈ F (R). Clearly, (x R , y R ) ∈ R since R satisfies (P2). Let z ≤ x R . By Lemma 5.7, there exists x ∈ B such that x ≤ x and z = x R . By definition of F (R), there exists y ∈ B such that y ≤ y with (x , y ) ∈ R. But since R is a * -congruence, by (P2), it follows that (x R , y R ) ∈ R. By monotonicity of the right projection, there therefore exists z = y R ≤ y R such that (z, z ) ∈ R. By applying a symmetrical argument, if we assume that z ≤ y R then there exists z

≤ x R such that (z , z) ∈ R. In other words, (x R , y R ) ∈ F (R). A similar argument shows that (x L , y R ) ∈ F (R). Hence, Property (P2) is satisfied.
Obviously, if R is idempotent pure then so is F (R).

Lemma 5.9 (Fixed point characterisation). The bisimulation refinement

B of a closed * -congruence can be computed as the greatest fixed point

B = α F α (∼) of F that is included in the relation ∼ := ∩ ≈ srt . Proof. It is straightforward to check that, if R is a * -bisimulation, then R = F (R)
. Note that B is the greatest * -bisimulation included in and, therefore, the greatest * -bisimulation included in ∼. As F is monotonic, the claim therefore follows by the fixed point theorem of Knaster-Tarski.

The interest in (strong) * -bisimulations is that they provide a (partial order) preorder relation on the quotient. Strong * -bisimulations are order congruences [START_REF] Körtesi | Congruences and isotone maps on partially ordered sets[END_REF]. Lemma 5.10 (Induced preorder and order). Let be a * -bisimulation. Then the relation

X Y :iff x ≤ y , for some x ∈ X and y ∈ Y is a preorder on B/ . If is strong, is a partial order.
Proof. Reflexivity of is immediate. For transitivity, we first show that X Y implies that, for every y ∈ Y , there is some x ∈ X such that x ≤ y. From this, transitivity follows easily.

Let X, Y ∈ B/ with X Y and let y ∈ Y . By definition, there exists x 0 ∈ X and y 0 ∈ Y such that x 0 ≤ y 0 . As y, y 0 ∈ Y , we have y 0 y. Consequently, x 0 ≤ y 0 y implies, by (P4), that there is some x ∈ X with x ≤ y.

We have shown that is a preorder. Assume now that the * -bisimulation is strong. We have to prove that X is antisymmetric.

Let X, Y ∈ B/ such that X Y X. Let y ∈ Y . Since X Y , we can use the above claim to find some x ∈ X with x ≤ y. Similarly, Y X implies that there exists y ∈ Y such that y ≤ x. But this means that x ≤ y y ≤ x. Hence, we have x y by Property (P5). By definition of B/ , this implies that X = Y .

The order of the quotient induced by a strong * -bisimulation allows us to prove that strong * -bisimulations are kernels of adequate premorphisms. The domain of M consists of all anti-chains of S, that is, all non-empty sets X ⊆ P(S) whose elements are pairwise incomparable with respect to . The product X • Y of two anti-chains X , Y ∈ M is defined by Proof. We start by noting that we have seen in Lemma 5.10 that the relation is a partial order. This implies that the relation ≤ of M is indeed a partial order.

X • Y := µ ( X ) • ( Y) ,
Furthermore, it is easy to check that the function µ in the definition of M is a well-defined mapping P(B) → M and that it is surjective and monotonic. Moreover, we also have µ( X ) = X , for all X ∈ M .

Since the natural order on birooted trees is stable under products and since µ( X ) = X , it is routine to check that this product is associative. Hence, it turns M into a semigroup.

Since is idempotent pure, this means that 1 is the maximal element of its class [START_REF] Berthaut | Advanced synchronization of audio or symbolic musical patterns: an algebraic approach[END_REF]. Therefore,

X • [1] = X = [1] • X , for every X ∈ M .
Consequently, M is a monoid.

We observe that the partial order ≤ is stable under product. Moreover, for every subunit X ≤ [START_REF] Berthaut | Advanced synchronization of audio or symbolic musical patterns: an algebraic approach[END_REF] we have M (( X ) • ( X )) = M ( X ) since xy = x ∧ y for every x, y ≤ 1. Hence X •X = X . In other words, subunits of M are idempotents. It follows that the product of subunits is the meet and, since M is finite, it is therefore an adequately ordered monoid with

X L = {Z ≤ 1 : X • Z = X } and X R = {Z ≤ 1 : Z • X = X }.
To conclude the proof, we define ϕ : B → M by ϕ (x) := {[x]} for every x ∈ B. By definition, the kernel of ϕ equals . It remains to show that ϕ is an adequate premorphism. Clearly, it is monotonic (M1).

For (M2), let x, y ∈ B. Then [xy] ∈ ϕ (x) • ϕ (y). Hence ϕ is submultiplicative.

For (M3), let x ∈ B. By definition, ϕ(x R ) ≤ [START_REF] Berthaut | Advanced synchronization of audio or symbolic musical patterns: an algebraic approach[END_REF]. Moreover, we easily check that all maximal elements of [

x R ] • [x] belong to [x]. Hence ϕ([x R ]) • ϕ(x) = ϕ(x).
Assume now that there is a subunit Z ≤ [START_REF] Berthaut | Advanced synchronization of audio or symbolic musical patterns: an algebraic approach[END_REF] such that Z • ϕ(x) = ϕ(x). This means that M (( Z) • [x]) ⊆ M ([x]). Take x ∈ [x] maximal. This means that there exists z ∈ Z such that zx = x . By definition of right projections in B, it follows that x R ≤ z. Therefore, [x R ] [z] and, thus,

{[x R ]} ≤ {[z]} ≤ Z. In other words, ϕ (x R ) = {[x R ]} = (ϕ (x)) R
A symmetrical argument shows that ϕ also preserves left projections, that is, the mapping ϕ satisfies Property (M3). For (M4), since is a closed * -congruence we have

[x] * [y] = [x] • [y] = [xy]
, for all x, y ∈ B such that x * y is defined. Hence ϕ (x * y) = ϕ (x)ϕ (y), that is, the mapping ϕ satisfies Property (M4).

The second new notion for our characterisation is that of an alternating chain. Definition 5.13. Let be an equivalence relation on an ordered set M . An alternating -chain is an increasing sequence x 0 ≤ • • • ≤ x n such that x i x i+1 , for all i < n. The number n is called the length of the chain.

The following definition and the lemma that follows give a rather simple characterisation of those * -congruences whose bisimulation refinements are strong and of finite index. The link between the alternation depth of (syntactic) closed * -congruences and bisimulation refinements is stated in the following lemma. Moreover, it follows by a straightforward induction on N that x B y implies d (x) = d (y), for all x, y ∈ B. Suppose that x ≤ y B z ≤ x. By (P4), there exists x ≤ z such that x B x. We therefore have x n x for some n ≤ N . Since d (x ) = d (x) this implies that x z. We claim that z n+1 x. Indeed, for every z ≤ z we have z ≤ x since z ≤ x. Conversely, for every z ≤ x, there exists z ≤ x with z n z . But, x ≤ z implies that z ≤ z. Hence, z B x. It follows that B satisfies Property (P5). That is, B is a strong * -bisimulation.

(⇐) Conversely, assume that B is a strong * -bisimulation with finite index. Since B ⊆ , this implies that has finite index. Let x 0 ≤ • • • ≤ x n-1 be an alternating -chain We claim that n is necessarily bounded by the index of B . Otherwise, there are indices i < j such that x i B x j . Hence, x i ≤ x i+1 ≤ x j implies that x i B x i+1 . Consequently, we also have x i x i+1 since B ⊆ . This contradicts the fact that the chain is alternating. We have shown that the alternation depth of is bounded by the index of B . Remark 5.16. It could be the case that for every closed * -congruence , the relation has finite index if, and only if, its bisimulation refinement B has finite index. Of course, this does not hold for arbitrary equivalence relations on ordered sets. consider the set ω with the standard order and the relation of having the same parity. But we suspect that this could be true in the meet-lattice structure of B with the natural order. Lemma 6.7. Strongly adequate premorphisms and adequately ordered monoids (with given disjoint products) form a subcategory StAdP of the category AdP of adequately ordered monoids and adequate premorphisms. Lemma 6.8. Let ϕ : B → M be a strongly adequate morphism with finite codomain M , let ϕ be its kernel, and let M ϕ be the quasi-quotient induced by ϕ . Then ϕ is a strong * -bisimulation and there is a strongly adequate premorphism ι : M → M ϕ such that ϕ = ι • ϕ where, for every a, b ∈ M , the disjoint product a * b := ab is defined in M by ∃a * b if ∃x * y for some 4 x ∈ ϕ -1 (a) and y ∈ ϕ -1 (b).

Proof. The fact that ϕ is an adequate premorphism guarantees that its kernel ϕ is a * -congruence. Property (M5) ensures that it is idempotent pure. Property (M6) ensures it is closed, and Property (M7) ensures (P4). Consequently, it is a * -bisimulation. Property (P5) is immediate from the fact that ϕ is monotonic. Indeed, given elements x, y, z ∈ B with x ≤ y ϕ z ≤ x, we have ϕ(x) ≤ ϕ(y), ϕ(y) = ϕ(z) and ϕ(z) ≤ ϕ(x). By transitivity, it follows that ϕ(x) ≤ ϕ(y) ≤ ϕ(x). Thus, x ϕ y. Therefore, ϕ is a strong * -bisimulation. Hence we can use Theorem 5.12 to obtain the desired premorphism ϕ

ϕ : B → M ϕ . For x ∈ B, set [x] := ϕ -1 (ϕ(x)) ∈ B/ ϕ . Let ι : M → M ϕ be defined by ι(a) := µ(ϕ -1 (a ↓ ))
where a ↓ := {b ∈ M : b ≤ a} and µ is the function from Definition 5.11. The monotonicity of µ implies (M1), i.e., the monotonicity of ι. Property (M8) of ϕ ensures that ι is submultiplicative (M2). Since the mapping ι is clearly idempotent pure (M5) and closed (M6) arguments similar to the ones in the proof of Theorem 5.12 ensure that Properties (M3) and (M4) are satisfied. Properties (M7) and (M8) for ι are inherited from the same properties of ϕ.

In other words, ι is a strongly adequate premorphism from M into M ϕ . Moreover, for every x ∈ B, by definition of ϕ ϕ , we have ι(ϕ(x)) = ϕ ϕ (x). Hence, ϕ ϕ = ι • ϕ.

We obtain the following characterisation of quasi-recognisable languages. Theorem 6.9. A language X ⊆ B of birooted trees is quasi-recognisable if, and only if, it is quasi-recognisable by a strongly adequate premorphism.

Proof. Assume that X is a quasi-recognisable language. By Theorem 5.18, it is recognised by the strongly adequate premorphism ϕ B X . As strongly adequate premorphisms are restrictions of adequate premorphisms, the claim follows. Theorem 6.10. Let X ⊆ B be a quasi-recognisable language. The strongly adequate premorphism ϕ B X : B → M B X of Theorem 5.12 is weakly terminal in the category of all strongly adequate premorphisms recognising X (considered as a subcategory of the comma category (B, StAdP)).

Proof. Let ϕ : B → M be a strongly adequate premorphism recognising X. We have to prove that there is a strongly adequate premorphism ψ : M → M B X such that ϕ B X = ψ • ϕ. Let be the kernel of ϕ and let ϕ : B → M and ι : M → M be the strongly adequate premorphisms given by Lemma 6.8. As is a strong *bisimulation included in the syntactic congruence X of the language X, we have ⊆ B X . Hence, we can define a map η : M → M X by η(X ) := µ X ( X ) that lifts the inclusion surjective mapping B/ ϕ → B B X to a strongly adequate premorphism M → M B X . The composition ψ := η • ι is the desired premorphism (see Figure 2). When X is quasi-recognisable, the monoid M B X can therefore be considered as the syntactic adequately ordered monoid of X. Remark 6.11. Note that we only prove that M B X is weakly terminal in the sense that the strongly adequate premorphism ψ = η • ι found in the above proof may not be unique. This comes from the fact that, in general, the adequate premorphism ϕ may not be surjective.

However, in the category of the partial algebras of the form ϕ/ ordered by as in Lemma 5.10 for every kernel of a strongly adequate premorphism ϕ : B → M recognizing X, and the related (monotonic) partial algebra morphism that becomes surjective, we easily check that the object B/ B X is terminal in the usual sense.

Conclusion

We have characterised both recognisable and quasi-recognisable languages in terms of their syntactic congruences. We have shown that the notion of strong *bisimulation induces a refinement of quasi-recognisability: strong recognisability, which admits minimal recognisers.

As far as the membership problem is concerned, syntactic congruences and the corresponding quotients can be used, whether or not the considered language is quasi-recognisable.

Note that the bisimulation refinement may induce a non-elementary blowup in the index of the congruence. In return we hope that this refinement encodes more subtle properties of a language. We note however that we provide no effective algorithm to compute the bisimulation refinement of a closed * -congruence of finite index.

Although out of the scope of our presentation, it can also be shown that the class of MSO-definable languages is quite robust in the sense that it is closed under (non-zero) products, iterated products, inverses, upward and downward closures, reset and co-reset projections. How do these operations act on the syntactic algebras? An answer might lead to a better understanding of some subclasses of MSO-definable languages.

Last but not least, the monoid of labelled birooted trees studied here is a special case of so-called 0-E-unitary inverse monoids [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF]. These monoids enjoy a similar graphical representation [START_REF] Stephen | Presentations of inverse monoids[END_REF] with, especially, a natural order between non-zero elements characterised by means of injective morphisms. We suspect that the algebraic tools developed here could partially be adapted to this more general setting, perhaps in connection with languages of graphs as studied in [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

Fig. 1 .

 1 Fig. 1. Two compatible labelled birooted trees and their non-zero product.

Definition 3 . 3 .

 33 (a) A * -congruence over B is an equivalence relation that is compatible with the disjoint product * and the two projection operations L and R in the sense that (P1) x x , y y , ∃x * y , ∃x * y implies x * y x * y , (P2) x y implies x L y L and x R y R , A * -congruence is closed when it also satisfies the following property: (P3) x x and y y implies ∃x * y ⇔ ∃x * y .

Definition 4 . 4 (

 44 Quotient algebra). Let be a * -congruence over B.

Lemma 4 . 5 .

 45 Let be a * -congruence. The quotient algebra B/ is well-defined and the canonical surjection θ : B → B/ is a morphism of partial algebras.

Corollary 4 . 10 .

 410 Let be a closed * -congruence of saturating a language X ⊆ B. Let B/ be the quotient and let ϕ : B → B/ be the corresponding projection. Then we can compute the syntactic congruence X in time O(n 3 ) where n is the index of .Proof. Let ≈ be the relation over B/ defined by Y ≈ Z :iff y ≈ rt z for some 2 y ∈ Y and z ∈ Z .

  (b) An ordered monoid M is adequately ordered if all subunits of M are idempotent and both x R = min{z ≤ 1 : zx = x} and x L = min{z ≤ 1 : x = xz} exist for every x ∈ B.

Remark 5 . 4 .Corollary 5 . 5 .Definition 5 . 6 .

 545556 (a) Note that the meet of two * -bisimulations is not necessarily their intersection.(b) In general, the lattice property does not seems to hold for strong *bisimulations. Every closed * -congruence contains a greatest * -bisimulation B .Proof. The relation m := ∩ ≈ srt is the greatest idempotent-pure closed *congruence included in . We can define B as the transitive closure of the union of all * -bisimulations included in m . By Lemma 5.3, this is a * -bisimulation. We call the * -bisimulation B the bisimulation refinement of .

Lemma 5 . 7 .

 57 Let x, y, z ∈ B.

Definition 5 . 11 .

 511 Let be a strong * -bisimulation. We define the quasi-quotient M induced by as follows.Let S := B/ be the quotient of B under . For x ∈ B, let [x] := {y ∈ B : x y} be the equivalence class of x. For [x], [y] ∈ S, we define [x] [y] :iff x ≤ y for some x ∈ [x] and y ∈ [y] .

Theorem 5 . 12 (

 512 where µ : P(B) → M is defined byµ(X) := {[z] ∈ S : z a maximal element of X} .Elements of M are ordered by the relationX ≤ Y :iff (∀X ∈ X )(∃Y ∈ Y)[X Y ] . Induced premorphism).Let be a strong * -bisimulation with index κ. The quasi-quotient M induced by is an adequately ordered monoid of size |M | ≤ 2 κ . There exists an adequate premorphism ϕ : B → M such that x y iff ϕ (x) = ϕ (y) , for all x, y ∈ B .

Definition 5 . 14 (

 514 Equivalence alternating depth). Let be an equivalence relation on birooted trees. (a) The -depth of a birooted tree x ∈ B is the least ordinal d (x) ≤ ω such that every alternating -chain x 0 ≤ • • • ≤ x n = x ending in x has length n ≤ d (x). (b) The alternation depth d( ) of the relation is defined by d( ) := sup x∈B d (x)

Lemma 5 .

 5 15. A closed * -congruence has finite index and alternating depth if, and only if, its bisimulation refinement B is strong and has a finite index.Proof. (⇒) Assume that has finite index and finite alternating depth. By Lemma 5.9, we know that B = F n (∼) where ∼ := ∩ ≈ srt . Let x, y ∈ B and let n := d (x) ∨ d (y) be the supremum of the -alternating depths of x and y. By induction on n one can show that, (x, y) ∈ F n (∼) iff (x, y) ∈ F m (∼) , for all m ≥ n . It follows that B = F N (∼) where N := d( ) is the alternation depth of . Since |F n+1 (∼)| ≤ 2 |F n+1 (∼)| , for all n < ω, this shows that B has finite index.

Fig. 2 .

 2 Fig. 2. Minimal strong recogniser.

otherwise, there is no need of a zero

This proposition guarantees the existence of syntactic congruences, which will be defined and studied in the next section. We spend the rest of this section showing that there is a greatest idempotent-pure, closed * -congruence of finite index.

The syntactic congruenceIn this section, we show that our framework induces a notion of a syntactic congruence that captures MSO-definability and that has a linear time membership algorithm.

The left (or right) projection of a quasi-recognisable language may not be quasirecognisable,

or, by (M6), for all

Lemma 5.17. The syntactic congruence X of a quasi-recognisable language X of birooted trees has finite index and alternation depth.

Proof. Suppose that X is quasi-recognisable. Let ϕ : B → M be an adequate premorphisms into a finite adequately ordered monoid M recognising X and let ϕ be the kernel of ϕ. Clearly, the relation ∼ := ϕ ∩≈ rt is a closed * -congruence of finite index saturating X. Consequently, ∼ ⊆ X .

For a contradiction, suppose that the relation X does not have finite alternation depth. Then there exist alternating X -chains of arbitrary length. As the relation ≈ rt has finite index, this also means that there are such chains whose elements are ≈ rt -equivalent, i.e., with the same root types. Fix an alternating

where all x i are ≈ rt -equivalent and n is greater than the index of ∼. Then there are indices i < j such that x i ∼ x j . In particular, we have x i ϕ x j . By monotonicity of ϕ, it follows that x i ϕ x i+1 . As all elements have the same root type, this implies that x i ∼ x i+1 . Since ∼ is included in X , it follows that x i X x i+1 . This contradicts the assumption that x 0 , . . . , x n is alternating.

We conclude by proving our main characterization of quasi-recognizable languages.

Theorem 5.18. Let X ⊆ B. The following properties are equivalent:

(1) The language X is quasi-recognisable.

(2) The bisimulation refinement B X of the syntactic congruence X is a strong * -bisimulation of finite index.

(3) The syntactic congruence X has finite index and the length of alternating X -chains is bounded.

Proof. (3) ⇒ (2) follows by Lemma 5.15 and (2) ⇒ (1) was proved in Theorem 5.12. (1) ⇒ (3) follows by Lemma 5.17

Strong recognisability and minimal recognisers

All the material developed above also leads us to the notion of a strongly quasirecognisable language that, although equi-expressive, admits minimal recognisers.

A priori, the disjoint product is only defined over B. Hence there is not a defined notion of an adequate premorphism between arbitrary adequately ordered monoids. A simple remedy is to enrich the notion of an adequately ordered monoid by a given disjoint product operation. Definition 6.1 (Enriched adequately ordered monoid). An enriched adequately ordered monoid is an adequately ordered monoid M equipped with a partial product * that is compatible with the usual product in the sense that, if x * y is defined, then x * y = xy.

The notion of an adequate premorphism can be extended as follows: Definition 6.2 (Adequate premorphism). An adequate premorphism is a mapping ϕ : M → N between two enriched adequately ordered monoids M and N such that (M1) x ≤ y implies ϕ(x) ≤ ϕ(y), (M2) ϕ(xy) ≤ ϕ(x)ϕ(y), (M3) ϕ(x L ) = (ϕ(x)) L and ϕ(x R ) = (ϕ(x)) R , (M4) ∃x * y implies ∃ϕ(x) * ϕ(y) and ϕ(x * y) = ϕ(x) * ϕ(y). Remark 6.3. By default, for every adequate premorphism ϕ : B → M , the disjoint product in M is defined as follows: the product xy of two elements x, y ∈ M is disjoint, which is denoted by x * y when there exists x ∈ ϕ -1 (x) and y ∈ ϕ -1 (x) such that ∃x * y ∈ B. Lemma 6.4. The identity id : M → M is an adequate premorphism for every adequately ordered monoid M . The composition

again an adequate premorphism. Consequently, we obtain a category AdP of adequately ordered monoids with adequate premorphisms.

The question of finding a syntactic adequately ordered monoid recognising a given language X ⊆ B amounts to finding a terminal object in the subcategory of AdP that is induced by the adequately ordered monoids that recognise X.

However, it seems that such a terminal object does not exist. Indeed, the kernel ϕ defined by an adequate premorphism ϕ is a convex * -congruence, i.e., x ≤ y ≤ z and x ϕ z implies x ϕ y. In general, there may not exist a greatest convex relation saturating a language as illustrated, for instance, by the language X = {a, c, d} on the four element set S = {a, b, c, d} where the order is defined by a < b < c while d is incomparable.

The techniques developed in the proof of Theorem 5.12 lead us to the following strengthening of the notion of quasi-recognisability and a corresponding refinement of the category AdP where syntactic recognisers exist. Definition 6.5 (Strongly adequate premorphisms). An adequate premorphism ϕ : B → M is strongly adequate if, additionally, its satisfies the following properties.

Remark 6.6. Property (M5) ensures that the kernel of ϕ is idempotent pure. Property (M6) ensures that it is closed. Property (M7) ensures that ϕ is strongly monotonic in the sense of [START_REF] Troelstra | On the connection of partially ordered sets with some pseudo-boolean algebras[END_REF]. Property (M8) ensures that every element in the submonoid ϕ(B) of M generated by the image of ϕ is compatible in some sense with the ordered monoid structure of B. This last axiom, slightly technical, seems crucial for the normalisation Lemma 6.8 below.


Reverdy Anne-Laure
email: anne-laure.reverdy@irstea.fr

Pradel Marilys

Accounting GHG emissions from sludge treatment and disposal routesmethodological problems focused on sludge land spreading in agriculture

In France, more than 70% of sewage sludge is directly land spreading or composted before land spreading. Sludge application is responsible of greenhouse gases (GHG) emissions. In 2010 and 2011, Irstea produces a tool called G E S TABoues to quantify GHG emissions emitted during sludge treatment and disposal routes. This paper aims to present how this tool can be used to quantify GHG emissions of sludge land spreading of a 380 000 per captia equivalent wastewater treatment plant (WWTP) and to point out methodological aspects that could invert results of GHG emissions. Conclusions in GHG emissions results could vary depending on the system boundaries used, especially regarding additional fertilisation with mineral fertilisers and could be responsible for possible misunderstanding in conclusions of environmental assessment.

Introduction

During the last decades, European institution establishes regulations which aim at protecting the environment from the adverse effects of the collection, treatment and discharge of waste water (Directive 91/271/EEC of 21 May 1991 concerning urban waste water treatment) and at maintaining and improving the aquatic environment (Directive 2000/60/EC of 23 October 2000 establishing a framework for community action in the field of water policy). These regulations were transcribed in French laws leading to important constraints on the waste water treatment plants (WWTP). The application of this European and French laws leads to an increase in sludge production (from 947 000 in 2003 to 1 100 000 dry matter tons in 2008) which is eliminated according four main disposal routes: land spreading (directly or after composting), incineration, incineration with household wastes and landfilling. A recent study [START_REF] Reverdy | Les filières de valorisation des boues d'épuration en France[END_REF] shows an increase in sludge land spreading from 60 to 70% with a significant evolution of composted sludge spreading. In order to help stakeholders in their decision making, we developed a decision tool to assess the impact on global warming of different sludge treatment and disposal routes: G E S TABoues. This paper aims to present a possible use of G E S TABoues tool in order to quantify greenhouse gases emissions for sludge land spreading that come from a 380 000 per captia equivalent WWTP and to identify the impact of system boundaries definition on greenhouse gases emission accounting results.

Material and methods

G E S TABoues tool

The G E S TABoues tool allows the calculation of the environmental impact on global warming of sludge treatments and disposal routes. The method underlying this tool is explained in [START_REF] Reverdy | Evaluation des émissions de GES des filières de traitement et de valorisation des boues issues du traitement des eaux usées[END_REF]. It is based on the "Bilan Carbone ® " method (ADEME, 2009) and Life Cycle Assessment standards (ISO 14040 and ISO 14044). In our method, three GHG are recorded: carbon dioxide (CO 2 ), methane (CH 4 ) and nitrous oxide (N 2 O). As the quantification of these gases cannot be directly measured, we used data from literature or calculated them with adequate equations for each processes involved in the studied activities. The amount of each gas is then converted with an emission factor in CO 2 equivalent (CO 2 eq) according to their Global Warming Potential (GWP) over 100 years: 1 for CO 2 , 25 for CH 4 and 298 for N 2 O.

C-CO 2 emissions can be either from fossil or biogenic origin. Biogenic C-CO 2 emissions are belonging to short carbon cycle. They are involved in photosynthesis or thermal or biological ways of oxidation so as the emitted biogenic C-CO 2 is rapidly incorporated in the carbon cycle. These biogenic emissions are not taken into account in national protocols as they are considered (by convention) as "carbon neutral" (GWP equal to zero). In G E S TABoues tool biogenic C-CO 2 is not accounted. As 15th International Conference Ramiran, May 3-6, 2013, Versailles fossil C-CO 2 emissions come from the hydrocarbon combustion, stored in the Earth surface from million years, they are belonging to the long carbon cycle. Releasing this fossil carbon by combustion increases the amount of C-CO 2 in the atmosphere and these emissions need to be accounted. Three types of emissions are considered in G E S TABoues tool: direct, indirect and avoided emissions. Direct emissions are emissions directly produced by the process or the studied activity (ex: CO 2 emissions due to fuel combustion during the activity). Indirect emissions are produced by processes needed by the activity but not directly generated by the activity (ex: CO 2 emissions during transport of goods). Avoided emissions are generated when products are not used and replaced by recyclable products (heat, electricity, fertilizer…). The system boundaries are limited to the sludge treatment including all the possible disposal routes (Figure 1). Two types of analyses are done to assess GHG emissions: a detailed analysis for all the sludge treatment processes and disposal routes and a global analysis for the consumables, transport and infrastructure involved in the system. The GHG emissions are assessed for the total amount of sludge produced by a WWTP of x Per-Captia Equivalent (PCE). Precodd, 2007Precodd, -2011) ) [START_REF] Pacaud | Estimation des émissions azotées au champ et lien avec les performances des machines d'épandage[END_REF] (Table 1). -Direct emissions coming from organic and mineral fertilisers spread on the soil, -Emissions differed in the time coming from nitrate leaching and NH 3 atmospheric deposition.

Specific hypotheses for sludge land spreading

Land spreading

During sludge land spreading, some methodological problems are highlighted regarding fertilisation aspects: sludge application in fields has to be completed with mineral fertilizers due to the lack of nitrogen provided by sludge to fulfil the plant needs. In G E S TABoues, we propose to solve this methodological problem with three hypotheses: (i) We considered N 2 O emissions for both sludge and mineral fertilizers applied to complete the fertilisation, (ii)

We considered emissions from mineral fertilizers manufacturing, (iii)

We considered that fuel consumed for mineral fertilizers application is negligible compared to fuel consumed for sludge application.

Sludge transport and fuel consumption

Sludge transport refers to transport between wastewater treatment plant and the field with a 120 kW tractor equipped with a high capacity spreader. Sludges are transported on 40km. Fuel consumption refers to fuel consumed during sludge loading and land spreading.

Infrastructure

Infrastructure emissions were accounted for each process involved in the system and globalized at the whole WWTP scale regarding 3 WWTP classes (<10 000 PCE, between 10 000 and 100 000 PCE, > 100 000 PCE).

Avoided emissions

Avoided emissions represent emissions that could have occurred if mineral fertilizers were used instead of sludge and CO 2 sequestered in soil after sludge land spreading.

Studied system

To underline the importance of these assumptions, we conduct a study to assess GHG emissions of sludge land spreading. The sludge come from a 380 000 per captia equivalent WWTP and represent 4 630 tons of dry sludge produced during one year.

15th International Conference Ramiran, May 3-6, 2013, Versailles

Results

Results on sludge land spreading

During land spreading, we can discern different types of emissions:

-Direct emissions (sludge and mineral fertilizers): 1296.2 tons CO 2 eq, -Mineral fertilizers manufacturing:

1146.6 tons CO 2 eq, -Fuels: 13.2 tons CO 2 eq, -Transports of sludge: 139.6 tons CO 2 eq, -Infrastructure: 0.04 tons CO 2 eq, -Avoided emissions: -1593.3 tons CO 2 eq.

Direct emissions and mineral fertilizers manufacturing are responsible for the most quantities of emitted GHG (94%).

Specific results on direct emissions and mineral fertilizers manufacturing

Direct emissions represent 1296.2 tons CO 2 eq. Among those emissions, we can discern direct emissions from sludge (144 tons CO 2 eq) and direct emissions from mineral fertilizers (1152 tons CO 2 eq).

If we consider emissions from mineral fertilizers manufacturing that represent 1146.6 tons CO 2 eq, we can say that almost all emissions due to sludge land spreading come from the consideration of mineral fertilizers in our system boundaries: 88% of total emissions during land spreading and more than 60% on sludge treatment and disposal routes were related to mineral fertilisers accounting. If we choose to not taken into account emissions from mineral fertilizers in the system boundaries, GHG emissions from sludge land spreading are insignificant. Regarding these two aspects, we suggest to take into account both sludge and mineral fertilisers emissions in order to have a complete overview of sludge impact when it is used as fertiliser (as sludge is rich in P and poor in N, N fertiliser are needed to fulfil the plant needs).

Conclusion

As it is show in this example, system boundaries definition is very important to conduct an environmental assessment of GHG emissions during land spreading. Depending on the boundaries, possible misunderstanding in conclusions of environmental assessment can occur. Further work is ongoing to the influence of system boundaries of sludge land spreading of global warming and other life cycle assessment impact categories results.

Figure 1 .

 1 Figure 1. System boundaries

Table 1 . N 2 O emissions for liquid, limed, composted and dry sludges

 1 O emissions from other types of sludge and mineral fertilizers come from Gestim guidebook[START_REF] Gac | Ges'tim Guide méthodologique pour l'estimation des impacts des activités agricoles sur l'effet de serre[END_REF]. There are two categories of N 2 O emissions (Table2):

	Type of sludge	N 2 O emissions (kg N 2 O / ton)
	Liquid sludge	0,0294
	Limed sludge	0,0500
	Composted sludge	0,0500
	Dry sludge	0,2875

Table 2 . N 2 O Emission factor for other types of sludge and mineral fertilizers

 2

	Type of emission	Factor emission	EF	Annual rate of N leached or volatilized
	Direct emissions	0.0157 kg N 2 O / kg N	EF(p)
	Indirect emissions -Leaching	0,0118 kg N 2 O / kg N leached	EF(l) 30%
	Indirect emissions -Atmospheric deposition	0,0157 kg N 2 O / kg N volatilized	EF(v)	10% for mineral fertilizers 20% for sludge
	GHG emissions for the other types of sludge and for mineral fertilizers are calculated according
	Equation (1):
	Eq (1) N

2 O emissions = Nitrogen supply x [EF(p) + rate N leached x EF(l) + rate N volatilized x EF(v)]