David Janin
email: janin@labri.fr

On labeled birooted tree languages: algebras, automata and logic

With an aim to developing expressive language theoretical tools applicable to inverse semigroup languages, that is, subsets of inverse semigroups, this paper explores the language theory of finite labeled birooted trees: Munn's birooted trees extended with vertex labeling.

To this purpose, we define a notion of finite state birooted tree automata that simply extends finite state word automata semantics. This notion is shown to capture the class of languages that are definable in Monadic Second Order Logic and upward closed with respect to the natural order defined in the inverse monoid structure induced by labeled birooted trees.

Then, we derive from these automata the notion of quasi-recognizable languages, that is, languages recognizable by means of (adequate) premorphisms into finite (adequately) ordered monoids. This notion is shown to capture finite Boolean combinations of languages as above. Applied to a simple encoding of finite (mono-rooted) labeled tree languages in of labeled birooted trees, we show that classical regular languages of finite (mono-rooted) trees are quasi-recognizable in the above sense.

The notion of quasi-recognizability thus appears as an adequate remedy to the known collapse of the expressive power of classical algebraic tools when applied to inverse semigroups.

Illustrative examples, in relation to other known algebraic or automata theoretic frameworks for defining languages of finite trees, are provided throughout.

Introduction

For decades, one of the main challenges faced by theoretical computer science is to develop mathematical frameworks that can be used for the specification, design and validation of computerized systems [START_REF] Thomas | Logic for computer science: The engineering challenge[END_REF]. A formal method such as event B [START_REF] Janin | Modeling in Event-B -System and Software Engineering[END_REF], whose applicability to industry is clearly demonstrated regards to its use in automated public transport, offers a especially good example of how topics as varied as logic, proof theory, automata theory and formal languages can be combined and shaped towards applications [START_REF] Thomas | Logic for computer science: The engineering challenge[END_REF].

Since the early 80s [START_REF] Hoare | Communicating Sequential Processing[END_REF][START_REF] Milner | Communication and concurrency[END_REF], many algebraic frameworks have been developed for such a purpose. They are based on the general idea that models of complex systems should be definable by means of combinations of the models of some simpler subsystems. Various notions of sequential composition, alternative composition or parallel composition of system components have thus been defined and studied accordingly.

However, some examples of system modeling show that such a distinction does not necessarily fit the abstraction/refinement methodology that system designers may follow [START_REF] Janin | Modeling in Event-B -System and Software Engineering[END_REF]. For instance, the well known distributed algorithm for leader election in a graph [START_REF] Chalopin | An efficient message passing election algorithm based on mazurkiewicz's algorithm[END_REF] is, at the abstract specification level, based upon the sequential execution of two global phases: the construction of a spanning tree followed by the pruning of that spanning tree. However, at the concrete execution level these two phases may overlap in time. The pruning phase may start locally as soon as the spanning tree phase is locally completed. In other words, when composing two global computation phases one "after" the other, a composition of this type is neither purely sequential nor purely parallel: it is both ! Computational music, a field of application that is greatly in demand of modular, multi-scale and hierarchical modeling tools that would allow, in a single formalism, both the abstract modeling of the musical intention of the composers and the concrete modeling of their music, also offers a plentiful supply of examples of this type. The simplest notion of "starting the music at the same time" is one of such example. At the concrete level of musical performance, it should allow the first notes to be played at different time. At the more abstract level of musical intention, it clearly means agreeing on some more logical notion of start time. This is especially well illustrated by the notion of musical anacrusis [START_REF] Janin | Vers une modélisation combinatoire des structures rythmiques simples de la musique[END_REF].

In other words, when composing models of system behaviors, one may need a product that could be interpreted, on the abstract level, as a sequential composition, but that would also allow, on a more concrete level, parallel overlaps. Thus we may seek for a structural means to combine graph structures with some overlaps. An existing and well developed mathematical theory does happen to be available for such a purpose: the theory of inverse semigroups [START_REF] Pietrich | Inverse semigroups[END_REF][START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF].

Experiments conducted in mathematical physics already show that some notion of higher dimensional strings can be defined and applied to the local and modular description of global quasi-crystal structures [START_REF] Kellendonk | The local structure of tilings and their integer group of coinvariants[END_REF]. These studies led to the definition of tiling semigroups with a notion of product of tiles that allows partial overlaps [START_REF] Kellendonk | Tiling semigroups[END_REF][START_REF] Kellendonk | Universal groups for point-sets and tilings[END_REF].

Experiments conducted in computational music such as [START_REF] Janin | Vers une modélisation combinatoire des structures rythmiques simples de la musique[END_REF][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], based on earlier work [START_REF] Desain | LOCO: a composition microworld in Logo[END_REF], show that timed versions of the monoid of birooted words, that is, the monoid of McAlister [START_REF] Mcalister | Inverse semigroups which are separated over a subsemigroups[END_REF][START_REF] Lawson | McAlister semigroups[END_REF], can effectively be used as a model of complex system behaviors.

Further development in the field of functional programming for multimedia applications led to the definition of a tiled extension of the notion of polymorphic temporal media (PTM) [START_REF] Hudak | An algebraic theory of polymorphic temporal media[END_REF][START_REF] Hudak | A sound and complete axiomatization of polymorphic temporal media[END_REF]. Equipped with the related notion of tiled product, this data type induces an algebraic structure that is also an inverse monoid [START_REF] Hudak | Tiled polymorphic temporal media[END_REF].

Modeling experiments conducted in the field of distributed algorithm [START_REF] Janin | A lazy real-time system architecture for interactive music[END_REF] also show that birooted trees, a central notion in inverse semigroup theory, can be efficiently used for an incremental and modular description of some distributed algorithms.

All these experiments give high incentive for developing a formal language theory adapted to inverse semigroup language, that is, subsets of inverse semigroups. Such a theory will provide the robust mathematical framework that is needed for defining some well founded specification, analysis and synthesis tools for these newly emerging inverse semigroup based modeling techniques.

From the mathematical point of view, the existence of the free inverse monoids [START_REF] Scheiblich | Free inverse semigroups[END_REF][START_REF] Munn | Free inverse semigroups[END_REF] says that it would suffice to develop the language theory of birooted trees, that is, a certain kind of edge labeled trees with two distinguished vertices: their so called input and output roots. However, from the computer science point of view, the trees most commonly encountered are trees with labels on both edges and vertices.

In this paper, we develop the language theory of (edge and vertex) labeled birooted trees, that is, Munn's birooted trees extended with vertex labeling.

The fact is that languages of labeled birooted trees are more easily related to the classical language theory of trees and, beyond, the known results on the logical definability of tree languages [START_REF] Thomas | Chap. 7. Languages, automata, and logic[END_REF]. Moreover, labeled birooted trees induce inverse monoids that are simple quotients of free inverse monoids. It follows that, despite this rather ad hoc extension by means of vertex labelings, the mathematical robustness of inverse semigroup theory is preserved.

Outline

We briefly review in Section 1 the notion of inverse semigroups and the notion of birooted trees that arise in free inverse monoids [START_REF] Scheiblich | Free inverse semigroups[END_REF][START_REF] Munn | Free inverse semigroups[END_REF]. This section can be seen as a very short introduction to inverse semigroup theory. A thorough description of such a theory can be found in [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF].

Birooted labeled trees, called birooted F, A-trees, are presented in Section 2. Equipped with an extension of Scheiblich-Munn's product of (unlabeled) birooted trees [START_REF] Scheiblich | Free inverse semigroups[END_REF][START_REF] Munn | Free inverse semigroups[END_REF], the resulting algebraic structures are inverse monoids that are quite similar to discrete instances of Kellendonk's tiling semigroups [START_REF] Kellendonk | The local structure of tilings and their integer group of coinvariants[END_REF][START_REF] Kellendonk | Tiling semigroups[END_REF].

Links with classical definitions such as ranked trees (see Section 2.4) or unranked trees and forests (see Section 2.5) are provided. They illustrate the versatile modeling power of birooted F, A-trees.

Languages of (non zero) birooted trees are studied in Section 3. Preliminary results on languages definable in Monadic Second Order (MSO) logic first led to a simple refinement of the classical notion of tree automata that capture MSO on birooted F, A-trees (Theorem 3.1.3).

A notion of birooted tree automata, that simply extends word automata semantics to birooted trees, is then defined and studied. Examples of birooted tree automata and languages are described in Section 3.2. They illustrate how direction handling in birooted trees is a little more complex than in trees.

By construction, languages recognized by these finite automata are upward closed in the natural order. It follows that they fail to capture all languages definable by means of Monadic Second Order (MSO) formulae. However, this loss of expressive power is shown to be limited to the property of upward closure.

We prove (Theorem 3.3.1) that every upward closed language of birooted trees which is MSO definable is recognized by a finite state birooted tree automata.

As a case in point, when F is seen as a functional signature, by embedding the classical F -terms (see [START_REF] Thomas | Chap. 7. Languages, automata, and logic[END_REF]) into birooted F, A-trees, we show (Theorem 3.4.1) that the birooted tree image of every regular language L of F -terms is of the form U L ∩ D L for some MSO definable and upward closed (resp. downward closed) language U L (resp. language D L ).

The algebraic counterpart of birooted tree automata is presented in Section 4. The notions of adequately ordered monoids and adequate premorphisms are defined. The induced notion of quasi-recognizable languages of birooted F, A-trees is shown to be effective (Theorem 4.2.3).

As for expressive power, it is shown that every birooted tree automaton simply induces an adequate premorphism that recognizes the same language (Theorem 4.3.1) and that every quasi-recognizable language is MSO definable (Theorem 4.5.1). Languages of positive Boolean birooted are studied as examples in Section 4.4.

The picture is made complete by proving that quasi-recognizable languages of birooted trees correspond exactly to finite Boolean combinations of upward closed MSO definable languages (Theorem 4.6.1) : a class of language strictly included into MSO definable languages (Theorem 4.7.1)

Together with Theorem 3.4.1, this result demonstrates that our proposal can also be seen as yet another algebraic characterization of regular languages of trees completing that previously obtained by means of preclones [START_REF] Ésik | On logically defined recognizable tree languages[END_REF] or, to some extent, by means of forest algebras [START_REF] Bojańczyk | Forest algebras[END_REF].

Potential extensions of these results, especially in relation to a recent extension of the notion of recognizability by means of partial algebra [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF], are discussed as a conclusion.

Related works

Semigroup theory has amply demonstrated its considerable efficiency over the years for the study and fine grain analysis of languages of finite words. These results triggered the development of entire algebraic theories of languages of various structures elaborated on the basis of richer algebraic frameworks such as, among others, ω-semigroups for languages of infinite words [START_REF] Wilke | An algebraic theory for regular languages of finite and infinite words[END_REF][START_REF] Perrin | Semigroups and automata on infinite words[END_REF][START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF], preclones or forest algebra for languages of trees [START_REF] Ésik | On logically defined recognizable tree languages[END_REF][START_REF] Bojańczyk | Forest algebras[END_REF][START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF], or ω-hyperclones for languages of infinite trees [START_REF] Blumensath | Recognisability for algebras of infinite trees[END_REF]. With an aim to describing the more subtle properties of languages, several extensions of the notion of recognizability by monoids and morphisms were also taken into consideration, e.g. recognizability by monoids and relational morphisms [START_REF] Pin | Relational morphisms, transductions and operations on languages[END_REF] or recognizability by ordered monoids and monotonic morphisms [START_REF] Pin | Syntactic semigroups[END_REF].

As (monotonic) morphisms are particular cases of premorphisms, the notion of quasi-recognizability developed here, that is, recognizability by means of (adequate) premorphisms into (adequately ordered) ordered monoids, can be seen as a generalization of recognizability by (ordered) monoids and (monotonic) morphisms [START_REF] Pin | Syntactic semigroups[END_REF].

Inverse semigroup theory itself is already known to have very close connections with classical tree language theory (see e.g. [START_REF] Margolis | Inverse monoids, trees and context-free languages[END_REF]). The development of a birooted tree language theory has been initiated as such by Silva [START_REF] Silva | On free inverse monoid languages[END_REF]. However, it is known that the homomorphic image of an inverse monoid is an inverse monoid. Then, the automata stemming from morphisms into finite monoids are thus reversible in a certain sense [START_REF] Margolis | Languages and inverse semigroups[END_REF][START_REF] Silva | On free inverse monoid languages[END_REF]. It follows that, when applied to inverse monoids, classical recognizability has a relatively weak expressive power 1 . The notion of quasi-recognizability, that almost captures the class MSO definable languages, thus appears has as a remedy to such a collapse of expressive power.

The first definition of quasi-recognizability appears in the study of languages of birooted words [START_REF] Janin | Quasi-recognizable vs MSO definable languages of onedimensional overlapping tiles[END_REF][START_REF] Janin | Overlaping tile automata[END_REF] or, equivalently, subsets of the (inverse) monoid of McAlister [START_REF] Lawson | McAlister semigroups[END_REF][START_REF] Janin | On languages of one-dimensional overlapping tiles[END_REF]. The notion of birooted F, A-tree automata defined in this paper is an extension of the notion previously defined [START_REF] Janin | Overlaping tile automata[END_REF] for languages of birooted words.

Although closely related, we can observe that an extension of this type is by no means straightforward. Going from the linear structure of overlapping tiles to the tree shaped structure of birooted F, A-trees already induces a tangibly increased level of complexity. Moreover, in overlapping tiles, all edges go in the same direction while, in birooted F, A-trees, edges can go back and forth (almost) arbitrarily. Proving Theorem 3.3.1 is thus much more complex than proving an analogous result for overlapping tiles.

The automata theoretic tools that are developed in this paper are based on the notion of non deterministic tree automata. The notion of tree walking automata (see [START_REF] Bojańczyk | Tree-walking automata[END_REF]) offers an alternative automata theoretical approach for defining languages of birooted trees.

As already observed by Péchuchet [START_REF] Pécuchet | Automates boustrophedon, semi-groupe de Birget et monoide inversif libre[END_REF] for two-way automata, partial runs of walking automata implicitly defines birooted structures: input roots being defined as start nodes and output roots being defined as stop nodes. The algebra of runs induced by two-way automata or walking automata is studied in [START_REF] Dicky | Two-way automata and regular languages of overlapping tiles[END_REF] and [START_REF] Janin | Walking automata in the free inverse monoid[END_REF].

Extended with pebbles, tree walking automata induce a strict hierarchy of classes of definable languages: from recognizable to quasi-recognizable languages via rational languages [START_REF] Janin | Walking automata in the free inverse monoid[END_REF]. The non deterministic birooted tree automata presented here can be seen as tree walking automata with infinitely many pebbles that guarantee every vertex is labeled by a single state.

Comparing our proposal with other known algebraic characterizations of languages of (mono-rooted) F -trees [START_REF] Ésik | On logically defined recognizable tree languages[END_REF][START_REF] Bojańczyk | Forest algebras[END_REF] is not easy. Of course, our proposal induces a larger class of definable languages since we are dealing with birooted F, A-trees and not just F -trees. Of course Theorem 3.4.1 implies that all (encodings of) regular languages of trees are quasi-recognizable.

A more relevant comparison would be to compare the classification of languages that can be achieved by restricting even further the allowed recognizers: be they preclones [START_REF] Ésik | On logically defined recognizable tree languages[END_REF], forest algebras [START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF] or adequately ordered monoids as proposed here. This is a study yet to be done.

More precisely, we illustrate the notion of birooted F, A-trees by providing encodings of ranked tree and unranked tree algebras into birooted F, A-trees (see Section 2.4). These encodings suggest that the language theory of labeled birooted trees that is developed in this paper encompasses the language theory defined by pre-clones [START_REF] Ésik | On logically defined recognizable tree languages[END_REF] or forest algebras [START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF]. However, such a fact remains to be precisely stated and proved.

A source of difficulty for such a comparison also comes from the fact that adequate premorphisms are not morphisms : only disjoint products are preserved. The notion of disjoint product is thus a partial product.

Rephrasing the language theory of birooted F, A-trees that is developed here within the mathematical framework of partial algebra [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF] has recently led to the characterization of syntactic recognizers for languages of birooted trees [START_REF] Blumensath | A syntactic congruence for languages of birooted trees[END_REF] that allows the characterization of both MSO definable and quasi-recognizable languages. This extension goes far beyond the purpose of the present paper. We refer the interested reader to [START_REF] Blumensath | A syntactic congruence for languages of birooted trees[END_REF] for a presentation of such a follow-up on the material presented here.

Last, it must be mentioned that the notion of quasi-recognizability that is presented here provides a rather unexpected application to the notion of semigroup with local units, the study of which was initiated by Fountain [START_REF] Fountain | Right PP monoids with central idempotents[END_REF][START_REF] Fountain | Adequate semigroups[END_REF][START_REF] Hollings | From right PP monoids to restriction semigroups: a survey[END_REF][START_REF] Gould | Restriction and Ehresmann semigroups[END_REF]. The first definition of quasi-recognizable languages was even stated for languages of positive birooted words [START_REF] Janin | Quasi-recognizable vs MSO definable languages of onedimensional overlapping tiles[END_REF], that is, within the framework of such monoids: quasi-inverse in some sense [START_REF] Janin | Quasi-inverse monoids (and premorphisms)[END_REF].

The notion of adequately ordered monoids that is used in this paper very close connections, as detailed in [START_REF] Janin | Quasi-inverse monoids (and premorphisms)[END_REF], with the notion of semiadequate semigroups studied in [START_REF] Lawson | Semigroups and ordered categories. I. the reduced case[END_REF] and the notion of Ehresmann semigroups studied in [START_REF] Lawson | Semigroups and ordered categories. I. the reduced case[END_REF][START_REF] Gould | Restriction and Ehresmann semigroups[END_REF].

The fact is that restricting our attention to languages of positive birooted trees, that is, subsets of the free ample monoid [START_REF] Fountain | The free ample monoid[END_REF], allows us to develop further the available algebraic tools for the study of quasi-recognizable languages as shown in [START_REF] Dubourg | Algebraic tools for the overlapping tile product[END_REF].

Nota : this article is a revised and extended version of [START_REF] Janin | Algebras, automata and logic for languages of labeled birooted trees[END_REF].

Preliminaries: the free group and the free inverse monoid

Before defining the notion of labeled birooted trees in the next section, we review in this section the notion of the free group and the free inverse monoid generated by a finite alphabet. This can be seen as a short introduction to inverse semigroup theory. 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 free group

Let A be a finite alphabet and let Ā be a disjoint copy of A with, for every letter a ∈ A, its copy ā ∈ Ā. Let (A + Ā) * be the free monoid generated by A + Ā with neutral element denoted by 1. In the sequel, as for any semigroup, the product u • v of two elements of (A + Ā) can simply be written uv.

Let u → u -1 (sometimes also written u → ū) be the syntactic inverse mapping from (A + Ā) * to itself inductively defined by

1 -1 = 1 , (ua) -1 = ā u -1 , and (uā) -1 = a u -1 ,
for every u ∈ (A + Ā) * and every a ∈ A. This mapping is involutive, that is, (u -1 ) -1 = u for every u ∈ (A + Ā) * , and it is an anti-morphism, that is, (uv) -1 = v -1 u -1 for every word u and v ∈ (A + Ā) * .

The free group F G(A) generated by A is defined as the quotient of (A + Ā) * by the least semigroup congruence ≃ G such that, for every letter a ∈ A, aā ≃ G 1 and āa ≃ G 1 A word u ∈ (A + Ā) * is said to be reduced when it contains no factors of the form aā nor āa for a ∈ A. Clearly, every class [u] ∈ F G(A) contains a unique reduced element red(u), the reduced form of u.

The free group F G(A) is thus represented by the set of reduced words equipped with the product the product u • v of every two reduced words u and v ∈ F G(A) defined by u • v = red(uv).

We check that for every u ∈ F G(A), we have u•1 = u, 1•u = u and u•u -1 = 1 hence F G(A) is a group. The syntactic inverse u -1 of u ∈ F G(A) is the group inverse of u. Moreover, for every group G, for every mapping ϕ : A → G, there is a unique group morphism ψ : F G(A) → G such that ψ|A, that is, the restriction of ψ to the set A, equals ϕ. It follows that F G(A) is the free group generated by A.

Elements of F G(A), represented by reduced words, are ordered by the (syntactic) prefix order relation ≤ p . This relation is defined, for every (reduced word) u and v ∈ F G(A) by u ≤ p v when there exists (a reduced word) w ∈ F G(A) such that red(uw) = uw = v in the free monoid2 . The associated predecessor relation ≺ p is then defined, for every v and w ∈ F G(A), by v ≺ p w when v ≤ p w and w = vx for some x ∈ A + Ā.

Inverse and free inverse monoid

A monoid M is an inverse monoid when, for every x ∈ M there exists a unique

x -1 ∈ M such that xx -1 x = x and x -1 xx -1 = x -1
Such an element x -1 is the semigroup inverse of the element x.

Clearly, every group is an inverse monoid. But the converse is false as shown, for instance, by the free inverse monoid F IM (A) generated by A which definition is reviewed below.

There are two possible presentations of the free inverse monoid F IM (A). The first one is due to Scheiblich [START_REF] Scheiblich | Free inverse semigroups[END_REF]. It can be seen as a fairly compact way to represent the second one, more graphical, independently due to Munn [START_REF] Munn | Free inverse semigroups[END_REF].

Here, in both cases, elements of the free monoid are called birooted trees. Following Scheiblich's presentation, a birooted tree on the alphabet A is a pair B = (P, u)

where P ⊆ F G(A) is a finite prefix closed subset of the free group generated by A, henceforth with 1 ∈ P called the input root, and u ∈ P is a distinguished vertex called the output root. Following Munn's presentation, every such a pair can be depicted as a directed (tree shaped) birooted graph with edges labeled on the alphabet A

M B = (V, {E a } a∈A , in, out)
defined by: ⊲ the set of vertices V = P with the distinguished input root vertex in = 1 and the distinguished output root vertex out = u, ⊲ for every a ∈ A, the set of edges E a defined by all pairs (v, w)

∈ V × V such that v • a = w.
Such a definition is depicted in Figure 1, with the name of the vertices marked

(ab) • • a • c • b • a • b Figure 1: (1) (a) (bā) (ac) (b)
The birooted tree M (P,u) with domain P = {1, a, b, ab, ac, bā} and output root bā between parentheses, and the input and output roots marked by dangling input and output arrows. We observe that on Munn's representations, the underlying tree-shaped graphs are both forward and backward deterministic in the edge alphabet A. This means that every vertex is uniquely determined by the unique (reduced) word on the alphabet A + Ā defined by the shortest path from the input root to that vertex. This shows that vertex names, as depicted in the above figure, are redundant with the underlying graph structure and can thus be omitted. Moreover, this also shows that Munn's and Scheiblich's representations are, as expected, in a bijective correspondance.

The product of two birooted trees B 1 = (P 1 , u 1 ) and B 2 = (P 2 , u 2 ) is defined by

B 1 • B 2 = (P 1 ∪ u 1 • P 2 , u 1 • u 2 )
The resulting algebra, denoted by F IM (A), is an inverse monoid. The unit is given by 1 = ({1}, 1) and, for every birooted tree B = (P, u) the inverse B -1 of B given by

B -1 = (u -1 • P, u -1 )
Scheiblich-Munn theorem [START_REF] Scheiblich | Free inverse semigroups[END_REF][START_REF] Munn | Free inverse semigroups[END_REF] states that F IM (A) is the free inverse monoid generated by A. In other words, for every inverse monoid M , for every mapping ϕ : A → M there is a unique morphism of inverse monoid ψ : F IM (A) → M such that ψ|A equals ϕ.

From free monoids to free inverse monoids

Inverse semigroup theory provides another characterization of free inverse monoids, due to Wagner [START_REF] Pietrich | Inverse semigroups[END_REF][START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF], that is worth being recalled. It is obtained as follows. Let ≃ W be the least semigroup congruence on the monoid (A + Ā) * ) such that uu -1 u ≃ W u and uu -1 vv -1 ≃ W vv -1 uu -1 for every u ∈ (A + Ā) * and let θ : (A + Ā) * → (A + Ā) * / ≃ W be the induced canonical surjective morphism.

Then, Wagner theorem states that the free inverse monoid F IM (A) generated by A is (isomorphic to) the quotient of the free monoid (A + Ā) * by the congruence ≃ W .

This result first makes explicit an alternative definition of inverse semigroup. The first identity states the existence of semigroup inverses. Since idempotent elements are self inverse, the second identity states the commutation of idempotent elements. It is well known (see [START_REF] Pietrich | Inverse semigroups[END_REF][START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF]), that the commutation of idempotents implies the unicity of the semigroup inverses.

Interpreting every letter a ∈ A (resp. ā ∈ Ā) as the forward traversal (resp. backward traversal) of an a-labeled edge, this results also shows that every word u ∈ (A + Ā) * defines a complete traversal (or walk) from the input root to the output root of the birooted tree θ(u) it induces. This observation motivates the extension of tree walking automata semantics to birooted trees as done in [START_REF] Janin | Overlaping tile automata[END_REF].

Last, as studied for instance in [START_REF] Lohrey | Inverse monoids: Decidability and complexity of algebraic questions[END_REF], this result also shows that one can define certain classes of A-generated inverse semigroups by the set of words identities over the (image of the) free monoid (A + Ā) * these inverse semigroups satisfies. Then, every such a class clearly admits a free algebra simply defined as the quotient of the free inverse monoid generated by A under the least congruence generated by these identities.

The inverse monoid of (partially) labeled birooted tree that is defined in the next section is such a kind of free algebra. This means in particular that the language theory developed here may well be adapted to other quotients of this type.

The inverse monoid of labeled birooted trees

We define in this section the notion of (vertex labeled) birooted F, A-trees and the related birooted F, A-tree product. This defines the inverse monoid of labeled birooted trees B(F, A).

Beyond the study of the basic properties of this monoid, the modeling power of labeled birooted trees is also illustrated at the end of the section by encoding ranked and unranked trees or forests into birooted F, A-trees.

Labeled birooted trees

Definition 2.1.1 (Birooted F, A-trees) Let F be finite vertex alphabet. Let A be a non empty edge alphabet. A labeled birooted tree is a pair x = r, u where r : F G(A) → F ∪ {⊤} is a partial mapping with a finite prefix-closed domain dom(r) ⊆ F G(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 elements3 , the set of birooted trees is extended by a zero element 0. The set of all birooted trees is denoted by B(F, A).

Two examples of birooted F, A-trees B 1 and B 2 are depicted in Figure 2, with A-labeled arrows defining edges and an additional dangling input arrow (resp. output arrow) marking the input root (resp. the output root).

(B 1 ) (1) (a) (aa) (a b) g f a g a ⊤ b (B 2 ) (1) (a) (ab) (ac) (b) (a b) f ⊤ a f b g c f b g b Figure 2: Two labeled birooted F, A-trees B 1 = {1 → g, a → f, a b → ⊤, aa → g}, a and B 2 = {1 → f, b → f, a → ⊤, a b → g, ab → f, ac → g}, a b . Definition 2.1.2 (Birooted F, A-tree product) The product B • C of two non-zero birooted trees B = r, u and C = 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

B • 0 = 0 = 0 • B for all B ∈ B(F, A).
As usual, we may omit the dot and simply write BC instead of B • C.

As an example, the product of the birooted F, A-trees B 1 and B 2 from the Figure 2 above is depicted in Figure 3. In that picture, the circle marks the

(B 1 • B 2 ) (1) (a)
B 2 given by B 1 • B 2 = {1 → g, a → f, a b → ⊤, ab → f, aa → g, aab → f, aa b → g, aac → g}, aa b .
synchronization vertex that results from the merging of the output root of B 1 and the input root of B 2 . The edge f a → g from (a) to (aa) in the product results from the fusion of the edge f a → g from (a) to (aa) in B 1 and the edge f a → ⊤ from (1) to (a) in B 2 . This illustrates the fact that overlaps may occurs in a product, the product being set to zero when these overlaps fails to match.

One can check that the product of birooted F, A-tree is associative. With the unit 1 = {1 → ⊤}, 1 , the resulting structure is a monoid still denoted by B(F, A). It is the monoid of birooted F, A-trees.

Remark Observe that, the set of labeled F, A-trees which nodes are only labeled by ⊤ form a submonoid that is isomorphic to F IM (A), the free inverse monoid generated by A. In particular, when F is empty, the semigroup B(∅, A) is itself (isomorphic to) the free monoid F IM (A).

Definition 2.1.3 (Elementary birooted trees)

A birooted tree is said to be elementary when it is either 0 or 1, or of the from

B f = {1 → f }, 1 for some f ∈ F , or of the form B x = {1 → ⊤, x → ⊤}, x for some letter x ∈ A + Ā.
Non zero elementary trees are depicted in Figure 4. In the sequel, for every Clearly, since both F and A are finite, the monoid B(F, A) is finitely generated from B a , B ā and B f for a ∈ A and f ∈ F . This observation can be refined a bit further.

f (B f ) ⊤ (1) ⊤ ⊤ a (B a ) ⊤ ⊤ a (B ā)
Theorem 2.1.4 Let η : F IM (A + F ) → B(F, A) be the (inverse) monoid mor- phism generated by η(a) = B a , η(f ) = B f for all (birooted image of) a ∈ A and f ∈ F . Let ≃ η be the kernel of the morphism η, that is, the monoid congruence ≃ η over F IM (A + F ) defined for all birooted trees B 1 , B 2 ∈ F IM (A + F ) by B 1 ≃ η B 2 iff η(B 1 ) = η(B 2 )
Then, ≃ η is the least congruence such that:

f f ≃ f (henceforth f = f ) and f g ≃ 0 for every (birooted image of) f, g ∈ F with f = g. Proof Let f ∈ F . Since B f is idempotent then ≃ η satisfies the identity f f = f . Moreover, since B f is idempotent, then B f is self inverse and thus ≃ η also satisfies the identity f = f . Given f, g ∈ F with f = g, we have B f •B g = 0 hence ≃ η also satisfies the identity f g = 0 when f = g. This implies that, given ≃ F the least inverse semigroup congruence defined over F IM (A + F ) by the identities f f = f and f g = 0 for every f, g ∈ F with f = g, then the quotient morphism η/ ≃ F : F IM (A + F )/ ≃ F → B(F, A) is well defined and surjective.
The fact that this morphism is also injective can be proven by induction on the size of the strings of (F + F +A+ Ā) * that generates elements of F IM (A+F ). More precisely, it can be shown that every such a string reduces via (≃ F ∪ ≃ W ) * to a unique string u ∈ (A + Ā + F ) that corresponds to a complete canonical traversal from the input root to the output root of the birooted labeled tree induced by u, that is, the birooted labeled tree η • θ(u) ∈ B(F, A). ✷

Remark Following the terminology of inverse semigroup theory [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF], when |F | ≤ 1, the monoid B(F, A) contains no zero. It is a typical E-unitary inverse monoid. When |F | > 1, the monoid B(F, A) contains a zero. It is a typical 0, E-unitary inverse monoid defined as a Rees quotient of a E-unitary inverse monoid: the inverse monoid defined by the identity f f = f , which correspond to the monoid of birooted tree labeled by subsets of F .

Properties of the inverse monoid of birooted F, A-trees

The monoid of birooted F, A-trees is an inverse monoid. We check that 0 -1 = 0 and for every non zero birooted F, A-tree t, u , we have

t, u -1 = t u , u -1
where

t u : F G(A) → (F ∪ {⊤}) is defined by dom(t u ) = u -1 • dom(t) with t u (u -1 v) = t(uu -1 v) for every v ∈ dom(t).
Graphically, as depicted in Figure 5, taking the inverse of a birooted F, Atree just amount to invert the input and output roots.

(B) (1) (a) (aa) (a b) g f a g a ⊤ b (B -1 ) (ā) (1) (a)
B R = BB -1 (resp. B L = B -1 B).
When B is a non zero birooted tree of the form B = t, u , the left (resp. right) projection is equivalently defined to be B R = t, 1 (resp. B L = t u , 1 ). The right projection B R of B is also called the reset of B.

These projections are depicted in Figure 6 below. Both projections are

(B R ) (1) (a) (aa) (a b) g f a g a ⊤ b (B L ) (ā) (1) (a) ( b) g f a g a ⊤ b Figure 6: The projections B R = B • B -1 and B L = B -1 • B of the birooted F, A-tree B.
idempotent and we check that we have B R • B = B = B • B L . Moreover, since idempotents in an inverse semigroup are self inverse and commute, we have B L = B = B R , for every idempotent birooted F, A-trees B. In other words, the left and the right projection mappings are indeed projections from the set of birooted trees onto the set of idempotents.

Since B(F, A) is a inverse monoid, there is the natural order [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF] defined as follows.

Definition 2.2.2 (Natural order) Elements of B(F, A) are ordered by the natural order defined, for every B and

C ∈ B(F, A) by B ≤ C when B = BB -1 C (equivalently B = CB -1 B).
One can check that 0 is the least element and, for every non zero labeled birooted trees r, u and s, v we have r, u ≤ s, v if and only if u = v, dom(r) ⊇ dom(s) and, for every w ∈ dom(s), t(w) ≤ s(w) in the trivial order on F ∪ {⊤} defined by x < y if and only if x ∈ F and y = ⊤. In other words, increasing in the natural order amounts to removing either removing some vertex labels or removing some vertices out the path from the input to the output roots.

An instance of the natural order on non zero birooted trees is depicted in Figure 7. Observe that, on non zero idempotent birooted trees, the natural

(C) (1) (a) (ab) (ac) (b) (a b) f ⊤ a f b g c f b g b (C ′ ) (1) (a) (ab) (b)
(a b) f ⊤ a f b ⊤ b Figure 7: Two naturally ordered birooted F, A-trees with C ≤ C ′ .
order is the reverse of the prefix order on trees. In particular, the bigger is the size of a birooted tree, the smaller is the birooted tree in the natural order.

Disjoint product and strong decomposition

In this section, we prove that there is a restricted notion of product of birooted F, A-trees, called the disjoint product, which suffice, together with the left and the right projections, to finitely generate the monoid of birooted F, A-trees. This notion will be extensively used in the remainder of the text.

Definition 2.3.1 (Disjoint product) The product B 1 • B 2 of two non zero birooted trees B 1 = t 1 , u 1 and B 2 = t 2 , u 2 is a disjoint product when both conditions B 1 • B 2 = 0 and dom(t 1 ) ∩ u 1 • dom(t 2 ) = {u 1 } are satisfied.
Remark This restricted product is called a disjoint product because the condition dom(t 1 ) ∩ u 1 • dom(t 2 ) = {u 1 } implies that the set of edges in B 1 • B 2 is the disjoint union of the set of edges of B 1 and the set of edges of B 2 .

Lemma 2.3.2 (Strong decomposition) For every non zero B ∈ B(F, A), the birooted F, A-tree B can be decomposed into a finite combination of elementary birooted trees by disjoint products and right projections (resets).

Proof Let B = t, u be a non zero birooted F, A-tree. We aim at proving that it can be decomposed as stated above. This is done by induction on the size of dom(t).

For the ground case, when dom(t) = {1}, we have u = 1 and B = B t(1) hence the statement is true.

For the inductive step, we use elementary trees of the form B x with x ∈ A+ Ā to encode connecting edges between (some notion of) idempotent sub-birooted trees. These sub-birooted trees are induced by the prefix order ≤ p (and the associated successor relation ≺ p ) on the elements of birooted tree domains, also distinguishing the vertices that are on the path between the roots from the other vertices.

More precisely, edges are simply encoded as follows. For every vertex v and w ∈ dom(t) such that v ≺ p w, that is, when (v, w) defines an edge in B, let B p v,w be the two vertices birooted F, A-tree defined by B p v,w = B x where x = v -1 w in F G(A). The definition of the sub-birooted trees is slightly more technical. Let

U = {v ∈ dom(t) : 1 ≤ p v ≤ p u}
be the set of vertices that appears on the path from the input root 1 to the output root u. For every v ∈ dom(t), let D p (v) be the greatest prefix closed subset of the set {w ∈ dom(t v ) : v ≤ p vw, vw ∈ U ⇒ w = 1} and let B p v = t v |D p (v), 1 be the idempotent birooted tree obtained from B by restricting the subtree t v rooted at the vertex v to the domain D p (v). In the case F = ∅, the notion of sub-birooted trees is depicted in the Figure 8 below.

Then, the proof proceeds as follows. In the case B is idempotent, that is, when U = {1}, let N be the set of (directed) edge labels that can be read from the roots, that is, N = dom(t) ∩ (A + Ā). We observe that we have

B = { B p 1,x • B p x R : x ∈ N }
with only disjoint products and resets. Moreover, for every x ∈ N , we have

|dom(B)| > |dom(B p x )|.
It follows that the induction hypothesis applies. In the case B is not idempotent, this means that U = {1}. Let then

u 0 = 1 ≺ p u 1 ≺ p u 2 ≺ p • • • ≺ p u n-1 ≺ p u n = u
be the increasing sequence (under the prefix order) of the elements of U . We observe that

B = B p u0 B p u0,u1 B p u1 • • • B p un-1 B p un-1,un B p un 16 (B) (1) (b) b (bā) a (bāb) b ( b) b (c) c (bābb) b (bābc) c (bāc) c (bā b) b ( bb ) b (B p 1 ) (1)
( b) b (c) c ( bb ) b (B p bā ) (1)
(c) c ( b) b (B p b,bā ) (1)
(ā) a The decomposition of a birooted F, A-tree B as a combination of elementary birooted trees by disjoint products and right projections is called a strong decomposition of the birooted F, A-tree B. In the case F = ∅, that is, when B(F, A) is the free inverse monoid F IM (A), a similar decomposition was already considered in [START_REF] Deis | Equations in free inverse monoids[END_REF].

Ranked trees vs birooted trees

We show here how free ranked trees (or terms) algebras can be embedded into the monoid of labeled birooted trees. This allows us, later in the text, to relate languages of trees with languages of labeled birooted trees.

Assume till the end of that section that the set F is a finite functional signature, that is, a finite non empty set of function symbols equipped with some arity mapping ρ : F → P(A) that maps every function symbol f to the set of its arguments' names ρ(f ) ⊆ A.

Definition 2.4.1 (Ranked trees)

A ranked tree, also called F -tree or Fterm, is a partial function t : A * → F with prefix closed finite domain dom(t) such that for every u ∈ dom(t), every a ∈ A, if ua ∈ dom(t) then a ∈ ρ(t(u)). A finite F -term t is said to be complete when, moreover, for every u ∈ dom(t), for every a ∈ A, if a ∈ ρ(t(u)) then ua ∈ dom(t). The set of F -term is denoted by T (F ).

Definition 2.4.2 (Birooted encoding of ranked trees)

We define the encoding mapping ϕ : T (F ) → B(F, A) that maps every F -tree t ∈ T (F ) to the labeled birooted tree ϕ(t) = t, 1 . It is called the birooted image of the F -tree t.

Clearly, the mapping ϕ from F -term to labeled birooted tree that is injective.

Now we aim at studying to which extent the above encoding preserves the structure of F -term. For that purpose, we first show that the syntactic application of a function symbol f ∈ F to a set of argument {t a } a∈ρ(f ) can be encoded into birooted tree operation. This construction is then generalized to the notion of linear F -tree context application and, even more, to the notion of multilinear F -tree contexts.

Definition 2.4.3 (f -application) Let f ∈ F be a functional symbol and, for every a ∈ ρ(f ), let t a be an F -tree. We define the application f ((t a ) a∈ρ(f ) ) of the symbol f to the arguments {t A } a∈ρ(a) to be the F -tree defined by:

⊲ dom(f ((t a ) a∈ρ(f ) )) = a∈ρ(f ) a • dom(t a ), ⊲ f ((t a ) a∈ρ(f ) )(1) = f and f ((t a ) a∈ρ(f ) )(au) = t a (u) for every a ∈ ρ(f ), every u ∈ dom(t a ),
The syntactic application can be uniformly defined over birooted (encodings of) F -trees as stated in the next lemma and depicted in Figure 9.

f (a 1 ) (a) (a k ) a 1 a a k t a1 t a k t a f t a ⊤ ⊤ a ϕ(f ({t a }) a∈ρ(f ) ) ϕ(t a ) a f
Figure 9: Birooted tree uniform encoding of f ({t a }) a∈ρ(f ) from the birooted trees defined by f , {a} a∈ρ(f ) and ϕ(t a ) for every a ∈ ρ(f ).

Lemma 2.4. [START_REF] Blumensath | A syntactic congruence for languages of birooted trees[END_REF] For every function symbol f ∈ F , for every indexed set of F -tree (t a ) a∈ρ(f ) we have

ϕ(f ((t a ) a∈ρ(f ) )) = f • a∈ρ(f ) (a • ϕ(t a )) R
and all the products are disjoint products.

As expected, the product a∈ρ(f ) (a • ϕ(t a )) R above is commutative since idempotents commute. This construction is generalized to the notion of F -tree context application as detailled below.

Definition 2.4.5 (Linear F -context and F -context application)

A linear F -context is a tree c : A * → F ∪ {⊤} such that there is a vertex u ∈ dom(t) with ua / ∈ dom(t) for every a ∈ A, i.e. u is a leaf node, and c(u) = ⊤ such that, for every v ∈ dom(c), if c(v) = ⊤ then v = u. This vertex u, necessarily unique, is called the hole of the context c. The set of linear context is denoted by C 1 (F ).

For every F -context c with hole u and F -tree t, we write c(t) for the F -tree obtained by attaching into the context c the tree t at the hole u of c.

ϕ(c(t)) = (ψ(c) • ϕ(t)) R
and the product is disjoint.

Proof Immediate from the definition. ✷ In other words, the context application operation is uniformly definable on the encodings of linear contexts and trees into birooted trees.

This encoding can go even further. In [START_REF] Ésik | On logically defined recognizable tree languages[END_REF], for arbitrary k ∈ N, there is the notion of k-ary multilinear contexts. We show below how bilinear context can also be encoded by means of (tree-shaped) quadruples of birooted F, A-trees. Clearly, this construction generalizes to arbitrary k ≥ 2.

Definition 2.4.8 (Bilinear F -context and F -context application)

A bi- linear F -context is a tree c : A * → F ∪ {⊤ 1 , ⊤ 2 } such that there is are two distinct (unique) leaf vertices u 1 , u 2 ∈ dom(t) such that c(u 1 ) = ⊤ 1 , c(u 2 ) = ⊤ 2 and, for every v ∈ dom(c), if c(v) ∈ F then v = u 1 or v = u 2 .
The vertices u 1 and u 2 are called the holes of the context c. The set of bilinear context is denoted by C 2 (F ).

For every bilinear context c ∈ C 2 (F ), every trees t 1 , t 2 ∈ T (F ) we write c(t 1 , t 2 ) for the trees obtained by attaching into the context c, the tree t 1 at the first hole u 1 of c and the tree t 2 at the second hole u 2 of c. Lemma 2.4.9 For every bilinear context c ∈ C 2 (F ) with holes u 1 ∈ dom(c) and u 2 ∈ dom(c), there are unique linear contexts c 0 , c 1 , c 2 ∈ C 1 (F ) and a unique tree t ∈ T (F ) such that, for every tree t 1 , t 2 ∈ T (F ), we have

ϕ(c(t 1 , t 2 ) =   ψ(c0) • ϕ(t) • (ψ(c 1 ) • ϕ(t 1 )) R • (ψ(c 2 ) • ϕ(t 2 )) R commuting idempotents    R
and all the product are disjoint.

Proof Since u 1 and u 2 are distinct leaves in c, there necessarily exist (unique)

a 1 , a 2 ∈ A and u 0 ∈ A * such that a 1 = a 2 , u 1 = u 0 • a 1 • u ′ 1 for some u ′ 1 ∈ A * and u 2 = u 0 • a 2 • u ′ 2 for some u ′ 2 ∈ A * .
In particular, the node u 0 is necessarily the greatest common prefix u 1 ∧ p u 2 of the two holes u 1 and u 2 . This situation is depicted in Figure 10.

(1) Then, the expected contexts and trees are necessarily defined as follows. The context c 0 is defined by

(u 0 ) (u 0 a 1 ) (u 0 a 2 ) (u 1 ) (u 2 ) a 1 a 2 c 0 c 1 c 2 t
dom(c 0 ) = dom(c) -u 0 A * with c 0 (u 0 ) = ⊤ and c 0 (v) = c(v) for every v ∈ dom(c 0 ) -u 0 . For i = 1 or i = 2, the context c i is defined by dom(c i ) = (a i (u 0 a i ) -1 dom(c)) ∩ A * with c i (a i u ′ i ) = ⊤ and c i (w) = c(u 0 w) for every w ∈ dom(c 0 ) -a i u ′ i .
Last, the tree t, containing the remaining nodes, is defined by taking

dom(t) = (u -1 0 (dom(c) -u 0 dom(c 1 ) -u 0 dom(c 2 ))) ∩ A *
with t(w) = c(u 0 w) for every w ∈ dom(t).

The expected property and the unicity of such a decomposition are easily checked.

✷

In other words, even bilinear context applications can uniformly be encoded via quadruples of birooted trees.

The fact that the operations on F -tree and F -tree context defined above can uniformly be defined on their birooted tree images by means of the disjoint product and the right projection, says that every notion of birooted tree language recognizability that preserves the disjoint product and the left and right projections is applicable: the notion of quasi-recognizability defined below in Section 4, and the more general notion of partial algebra recognizability defined in [START_REF] Blumensath | A syntactic congruence for languages of birooted trees[END_REF].

Unranked trees and forest vs birooted trees

We show here in this section how (ordered) unranked trees and forests free algebras can also be embedded into the monoid of labeled birooted trees. Definition 2.5.1 (Unranked F -trees and F -forests [START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF]) Assume that F is a non empty alphabet. The sets U(F ) and F(F ) of unranked trees and unranked forest are mutually defined by the rules:

f (s) ∈ U(F ) , (t 1 , t 2 , • • • , t n ) ∈ F(F )
for every f ∈ F , every (possibly empty) finite sequence s ∈ F(F ) and every unranked trees

t 1 , t 2 , •, t n ∈ U(F ).
Following [START_REF] Bojańczyk | Forest algebras[END_REF][START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF], the empty forest is denoted by 0 and the forest concatenation is denoted by +. The resulting monoid of forest is denoted by H F and is called the horizontal monoid.

Examples of unranked F -forests and F -trees are depicted in Figure 11

)) t 3 = a(t 1 + t 1 + t 2 )
Figure 11: Three F -trees t 1 , t 2 and t 3 . Now, we aim at encoding unranked F -trees and F -forests into (ranked) birooted F, A-trees. For such a purpose, let A = {v, h}, with h standing for vertical and v standing for horizontal. Up to the additional nodes labeled by ⊥, our encodings essentially follow the classical encoding of ω-trees in binary trees [START_REF] Rabin | Weakly definable relations and special automata[END_REF] by means of the first child (almost vertical) relation and the next sibling (horizontal) relation.

Definition 2.5.2 (Unranked F -trees and F -forests encodings)

The birooted tree encoding of every unranked F -tree and F -forest is defined via the mappings ϕ 1 : U(F ) → B(F, A) and ϕ 2 : F(F ) → B(F, A) given by the following (mutual) inductive rules:

ϕ 1 (f (s)) = (f • v • ϕ 2 (s)) R and ϕ 2 (0) = 1 , ϕ 2 (t) = h • ϕ 1 (t) and ϕ 2 (t + s) = ϕ 2 (t) • ϕ 2 (s)
for every f ∈ F , for every F -tree t ∈ U(F ), also seen as a singleton F -forest when in ψ 2 (t), and every s ∈ F(F ), with all products that are disjoint products.

In particular, the mapping ϕ 2 : F(F ) → B(F, A) is not only a monoid morphism but it also maps sums in F(F ) to disjoint products in B(F, A).

Continuing the example depicted in Figure 11, the birooted encodings ϕ 1 (t 1 ) and ϕ 1 (t 2 ) of the unranked F -trees t 1 and t 2 is depicted in Figure 12.

b ⊤ v c h ⊤ v d ⊤ v a h ⊤ v c h ⊤ v c h ⊤ v ϕ 1 (t 1 ) ϕ 1 (t 2 )
Figure 12: The birooted F, A-tree encodings of t 1 and t 2 .

Continuing the same example, the birooted encodings of the F -forest lifting of t 1 and t 2 and the birooted encoding of the F -tree t 3 are depicted in Figure 13.

⊤ b h ϕ 1 (t 1 ) ⊤ d h ϕ 1 (t 2 ) a ⊤ v b h ϕ 1 (t 1 ) b h ϕ 1 (t 1 ) d h ϕ 1 (t 2 ) ϕ 2 (t 1 ) ϕ 2 (t 2 ) ϕ 1 (t 3 ) = a • v • ϕ 2 (t 1 ) • ϕ 2 (t 2 )
Figure 13: Encodings of the F -forests t 1 and t 2 and the F -tree t 3 .

With the aim to generalizing the f -lifting of forests into trees, the notions of unranked trees and forest are extended to the notion of linear unranked tree and forest context as follows.

Definition 2.5.3 (Unranked F -tree and F -forest linear contexts [6])

Let Ω be a new forest symbol. The set C U (F ) of unranked F -tree contexts and the set C F (F ) of unranked F -forest contexts are mutually defined by

Ω ∈ C F (F ) , s 1 + c + s 2 ∈ C F (F ) and f (s) ∈ C U (F ) for every F -forest context c ∈ C F (F ) and every F -forest s 1 , s 2 ∈ F(F ).
Then, the set C F (F ) of F -forest contexts is turned into a monoid by defining the composition product • by

c 1 • c 2 = c 1 [c 2 /Ω]
where c 1 [c 2 /Ω] is the F -forest context obtained from the context c 1 by replacing the hole Ω in c 1 by the context c 2 .

In [START_REF] Bojańczyk | Forest algebras[END_REF][START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF], the monoid defined by C F (F ) with unit Ω and product • is denoted by V F and is called the vertical monoid. Remark In the definition above, F -forest contexts are still seen as non empty sequences of F -trees and F -tree contexts. It follows that the operation + still denotes the concatenation of sequences with the empty sequence 0 as unit. In particular, the equations Ω + 0 = Ω and 0 + Ω = Ω hold. Definition 2.5.4 (Unranked F -tree and F -forest contexts encodings) The birooted encoding of every F -tree context or F -forest context is defined via the mappings ψ 1 : C U (F ) → B(F, A) and ψ 2 : C F (F ) → B(F, A) given by the following (mutual) inductive rules:

ψ 1 (f (c)) = f • v • ψ 2 (c)
and

ψ 2 (Ω) = h • ⊤ , ψ 2 (t) = h • ψ 1 (t) and ψ 2 (s 1 + c + s 2 ) = ψ 2 (s 1 ) • ψ 2 (t) • ϕ 2 (s 2 )
for every f ∈ F , F -tree context t ∈ C U (F ), also seen as a singleton F -forest context when in ψ 2 (t), every F -forest context c ∈ C F (F ) and every F -forests s 1 , s 2 ∈ F(F ), with all products that are disjoint products.

Then we have: Lemma 2.5.5 For every context c ∈ C F (F ) there exist a unique context c 1 ∈ C F (F ) and a unique forest s ∈ F(f ) such that c = c 1 • (Ω + s) and

ψ 2 (c • c ′ ) = ψ 2 (c 1 ) • (ϕ 2 (s)) R • ψ 2 (c ′ )
for every context c ′ ∈ C F (F ), with only disjoint products. Proof In the case c = s 1 + Ω + s 2 for some forests s 1 , s 2 ∈ F(F ) then we necessarily have c 1 = s 1 + Ω and s = s 2 . Otherwise, there exist f ∈ F and a unique context c ′ 1 such that c = c ′ 1 • f (s 1 + Ω + s 2 ) for some F -forests s 1 and s 2 . Then, by disjointness hypothesis on their encodings, we necessarily have

c 1 = c ′ 1 • f (s 1 + Ω) and s = s 2 .
The equation above is easily verified. ✷

Remark

We thus have proved that the free forest algebras defined in [START_REF] Bojańczyk | Forest algebras[END_REF][START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF] can be uniformly encoded as birooted trees and pairs of birooted trees with only disjoint products and resets. We conjecture that, together with the notion of partial algebra recognizability developed in [START_REF] Blumensath | A syntactic congruence for languages of birooted trees[END_REF], this encoding can be extended further to a full and faithful encoding of the algebraic language theory induced by forest algebras and forest morphisms.

Languages of labeled birooted trees

We are interested in languages of labeled birooted trees, that is, sets of non zero birooted F, A-trees. We first examine definability in Monadic Second Order (MSO) logic and a related notion of top down tree automata. Then, from the notion of finite state word automata, we derive a notion of birooted tree automata that is shown to capture languages that are definable in MSO and upward closed in the natural order.

MSO logic on (non zero) birooted trees

Every non zero birooted F, A-tree B = t, u can be seen as a FO-structure M B with constants in and out, disjoint unary relation symbols {S f } f ∈F and binary relation symbols {E a } a∈A defined over the domain dom(M B ) = dom(t) by in = 1 and out = u for the constants, the unary relation S f = t -1 (f ) for every f ∈ F , and the binary relation E a = {(v, w) ∈ dom(t) × dom(t) : va = w} for every a ∈ A.

Definition 3.1.1 (MSO-definable languages)

A language L ⊆ B(F, A) of non zero labeled birooted trees is definable in monadic second order logic (MSO), or simply MSO-definable, when L = {B ∈ B(F, A) : M B |= ϕ} for some closed MSO formula ϕ on the above FO-signature.

The classical notion of tree automata [START_REF] Thomas | Chap. 7. Languages, automata, and logic[END_REF], that characterizes MSO definable languages of trees, is applicable to birooted F, A-trees. Indeed, as depicted in Figure 14, every birooted tree on the vertex alphabet F and the edge alphabet A can be seen as mono rooted trees on the vertex alphabet F × {0, 1} and the edge alphabet A + Ā, with a unique vertex labeled in F × {1}: the output root.

However, such an encoding of the output root is not very convenient for it changes the underlying signature hence the tree automata that can be defined on birooted trees. Instead, we propose a notion of normalized top down automata that will runs on the birooted tree signature, handling the output root just by checking its state labeling.

Definition 3.1.2 (Normalized top down birooted tree automaton)

A normalized top down tree automaton on the alphabets A + Ā and F is a triple

A = Q, I, O, δ, T
where Q is a finite set of states, I, O, T ⊆ Q are distinguished sets of states respectively called initial, output and terminal (or accepting) states, and

δ : Q × (F ∪ {⊤}) → P(P((A + Ā) × Q))
is a transition function.

An accepting run of the tree automaton A on a birooted tree B = t, u is a mapping ρ : dom(t) → Q such that:

⊲ Roots condition: ρ(1) ∈ I, ρ(u) ∈ O, ⊲ Transition condition: for every v ∈ dom(t), {(x, ρ(vx)) ∈ (A + Ā) × Q : v ≺ p vx, vx ∈ dom(t)} ∈ δ(ρ(v), t(v)) ⊲ Accepting condition: if u ∈ dom(t) is maximal for the prefix order, that is, if u is a leaf, then ρ(u) ∈ T .
The language L(A) ⊆ B(F, A) recognized by the automaton A is then defined as the set of non zero labeled birooted tree B ∈ B(F, A) such that there is an accepting run of A on B.

Theorem 3.1.3 A language L ⊆ B(F, A) of non zero birooted tree is definable in MSO if and only if there exists a finite state normalized tree automaton A such that L = L(A).

Proof Since L is definable in MSO, the theorem of Doner, Thatcher and Wright applies (see Theorem 3.8 in [START_REF] Thomas | Chap. 7. Languages, automata, and logic[END_REF]). Thus, with minor variations on classical definition, there exists a finite state top down tree automaton of the form

A ′ = Q ′ , q ′ 0 , δ ′ , T ′ with finite set of states Q ′ , initial state q ′ 0 ∈ Q ′ , transition function δ ′ : Q ′ × ((F ∪ {⊤}) × {0, 1}) → P(P((A + Ā) × Q))
and terminal states T ′ ⊆ Q ′ , that recognizes (the tree encodings of) L among the set of deterministic trees with edge labeled on the alphabet A+ Ā and vertex labeled on the alphabet F × {0, 1}. More precisely, following [START_REF] Thomas | Chap. 7. Languages, automata, and logic[END_REF], for every birooted tree B = t, u , an accepting run of A ′ on B is a mapping ρ :

dom(t) → Q such that ρ(1) = q ′ 0 , {(x, ρ(vx)) ∈ (A + Ā) × Q : v ≺ p vx} ∈ δ(q, (t(v), b v ))
for every v ∈ dom(t) with b v = 1 if and only if u = v, and, additionally, ρ(v) ∈ T when v is a leaf for the prefix order. By definition of the accepting runs, we may assume, without loss of generality, that for every q ′ ∈ Q ′ , every f ∈ F ∪ {⊤} and every m ′ ∈ δ ′ (q ′ , (f, x))

with x = 0, 1 then m ′ is the relation of a partial function from A + Ā to Q ′ , i.e. |m ′ (a)| ≤ 1 for every y ∈ A + Ā,
We define the expected automaton

A = Q, I, O, δ, T by Q = Q ′ × {0, 1, 2}, I = {q 0 } × {0, 1}, O = Q × {1}, T = T ′ × {0, 1,
2} and, for every state q of the form (q ′ , x) ∈ Q, every vertex label f ∈ F ∪ {⊤}, by defining δ(q, f ) to be the set of all m ⊆ (A + Ā) × Q, functional, such that, given

m ′ = {(a, q ′ a ) ∈ (A + Ā) × Q ′ : ∃x a ∈ {0, 1, 2}, (a, (q ′ a , x a )) ∈ m}
we have m ′ ∈ δ ′ (q ′ , (f, x mod 2)) and, moreover, ⊲ if x = 0 then there exists one and only one a ∈ A + Ā such that we have (a, (q ′ a , x a )) ∈ m(a) for some q a ∈ Q with x a = 0 or x a = 1, ⊲ if x = 1 or x = 2 then for all a ∈ A+ Ā, if (a, (q ′ a , x a )) ∈ m(a) then x a = 2. Then, we check that L(A) = L(A ′ ) by observing that, for every birooted F, Atree B = t, u , for every mapping

ρ : dom(t) → Q ′ × {0, 1, 2}
given the mapping ρ ′ : dom(t) → Q ′ defined as the first projection π 1 (ρ) of the mapping ρ, then the following properties are equivalent:

⊲ ρ is an accepting run of the automaton A on B, ⊲ ρ ′ is an accepting run of the automaton A ′ on B with the additional property that, for every v ∈ dom(t), we have:

-ρ(v) ∈ Q ′ × {0} if and only if 1 ≤ p v < p u, i.e.
v is distinct from the output root and located on the path from the input to output root,

-ρ(v) ∈ Q ′ × {1} if and only if v = u, i.e. v is the output root, -ρ(v) ∈ Q ′ × {2}
if and only if v ≤ p u, i.e. v is strictly above the output root in the prefix order. ✷ This automata theoretic characterization of MSO definable language also leads to an automata theoretic characterization of a smaller class of languages: the MSO definable languages of labeled birooted trees that are moreover upward closed with respect to the natural order. Definition 3.1.4 (Upward closed normalized automaton) A normalized top down tree automaton A = Q, I, O, δ, T is an upward closed top down tree automaton when T = Q and for every (q, f ) ∈ Q×(F ∪{⊤}), the set of relations δ(q, f ) ⊆ P((A + Ā) × Q) is downward closed with respect to the inclusion order with, moreover, δ(q, f ) ⊆ δ(q, ⊤).

Then we have:

Theorem 3.1.5 Let L be a language L ⊆ B(F, A) of non zero labeled birooted trees. Then L is MSO definable and upward closed with respect to the natural order if and only if there exists a finite state upward closed normalized tree automaton A such that L = L(A).

Proof (⇒) Assume that L is MSO definable and upward closed. In the case L is the empty set, then any upward closed automaton with empty output set states O recognizes L.

Otherwise, by applying Theorem 3.1.3, let A = Q, I, O, δ, T be a normalized automaton that recognizes L. Let then,

A ′ = Q ′ , I ′ , O ′ , δ ′ , T ′ be the automaton defined by Q ′ = Q, I ′ = I, O ′ = O, T ′ = Q and δ ′ (q, f
) defined, for every q ∈ Q, for every f ∈ F ∪ ⊤, as the downward closure (under relation inclusion) of the set of relations δ(q, ⊤) ∪ g∈F δ(q, g) when f = ⊤, or the set of relations δ(q, f ) when f = ⊤.

We check that L(A ′ ) is the upward closure (under the natural order) of the language L(A). But since L = L(A) is upward closed, we conclude that L = L(A).

(⇐) Given an upward closed normalized automaton A it is routine to check that L(A) is upward closed. ✷ In the sequel, such an upward closed tree-automaton may simply be denoted by A = Q, I, O, δ omitting the (trivial) set of terminal states.

Remark Clearly, the class of languages of non zero labeled birooted trees definable in MSO is closed under all Boolean connective.

In the proof above, we see that it is also closed under upward closure henceforth, by complement, also under (non zero) downward closure.

Generalizing the case of languages of birooted words presented in [START_REF] Janin | On languages of one-dimensional overlapping tiles[END_REF][START_REF] Dicky | Two-way automata and regular languages of overlapping tiles[END_REF], the class of MSO definable languages is clearly closed under inverses and left and right projections. It can easily be shown that it is closed under (non zero) product, and, although the argument presented in [START_REF] Janin | On languages of one-dimensional overlapping tiles[END_REF][START_REF] Dicky | Two-way automata and regular languages of overlapping tiles[END_REF] no longer holds, it can also be shown that it is closed under iterated product (Kleene star).

This says that the class of MSO definable languages of labeled birooted trees is robust. However, in this paper, we focus our attention on the class of quasi-recognizable languages that is defined later in the text. Proving the above closure properties of the class of MSO-definable languages of birooted F, A-trees goes out of the scope of this paper.

Birooted tree automata

In this section, we define the notion of birooted F, A-tree automata that is shown to capture the class of languages of birooted F, A-trees that are upward closed with respect to the natural order and definable in Monadic Second Order Logic (MSO).

Definition 3.2.1 (Birooted tree automaton) A birooted F, A-tree (finite) automaton with edge alphabet A is a triple of the form

A = Q, ∆, W with a (finite) set of states Q, a (non deterministic) transition table ∆ : (F + A) → P(Q × Q) and a set of accepting pairs W ⊆ Q × Q.
Observe that in the above definition, the transition function is only defined on F and A. There is no reference to the trivial vertex labeling ⊤ nor to the reverse edge labeling alphabet Ā.

Definition 3.2.2 (Runs) A run of a birooted tree automaton

A = Q, ∆, W on a non zero birooted F, A-tree B = t, u is a mapping ρ : dom(t) → Q such that for every v ∈ dom(t): ⊲ Vertex state coherence: if ρ(v) = ⊤ then (ρ(v), ρ(v)) ∈ ∆(t(v)), ⊲ Edge states coherence: for every a ∈ A, -if va ∈ dom(t) then (ρ(v), ρ(va)) ∈ ∆(a), -if vā ∈ dom(t) then (ρ(vā), ρ(v)) ∈ ∆(a).
The run ρ is an accepting run when (ρ(1), ρ(u)) ∈ W .

The language L(å) ⊆ B(F, A) recognized by the automaton A is then defined to be the set of non zero birooted F, A-tree B such that there is an accepting run of A on B.

Remark The definition of automaton runs relies on the intuition that vertex labels can be seen instead as cyclic F -labeled edges on the vertices. In other words, a birooted tree automaton is essentially a word automaton on the alphabet F + A that is running over all paths of a birooted F, A-tree. However, a birooted tree automaton is not a walking automaton since, in all these "runs" on paths, every vertex is always labeled by the same state. A study of walking automata on birooted trees can be found in [START_REF] Janin | Walking automata in the free inverse monoid[END_REF].

The notion of birooted F, A-tree automata is illustrated till the end of the section by showing that the language of idempotent birooted trees is recognized by such a finite state automaton.

Though fairly simple, this language is not recognizable by means of a morphism into a finite monoid. With an empty vertex alphabet F , that is within the free inverse monoid F IM (A), its inverse image in the free monoid (A + Ā) * is a typical context free (and regular) language: the Dyck language (see [START_REF] Silva | On free inverse monoid languages[END_REF] for a detailed study of the recognizable subsets of the free inverse monoid).

More precisely, let A = Q, ∆, W be the birooted F, A-tree automaton defined by

⊲ states : Q = { * } + (A + Ā), ⊲ vertex transition: ∆(f ) = {(q, q) ∈ Q × Q : q ∈ Q} for every f ∈ F , ⊲ edge transition: ∆(a) = {(q, ā) : q ∈ Q} ∪ {(a, q) : q ∈ Q} for every a ∈ A, ⊲ acceptance condition: W = {( * , * )}.
A run of automaton A on a birooted tree is depicted in Figure 15. Vertices are labeled by automaton states. In that figure, we observe that every state uniquely tells which edge to take to go towards the input root.

(B) ( * ) ( b) b (a) a ( b) b (b) b (c) c ( b) b (c) c (c) c (b) b (b) b
This example illustrates one of the main difficulty one is faced with birooted tree automata. A priori, no global orientation is encoded in the birooted tree edges: edge orientation are unrelated with the prefix order. A posteriori, a global orientation from every vertex towards the input root can still be computed as illustrated by the above example.

In other words, provided the input root is marked by the state * , a run of the automaton A on a birooted tree B makes the prefix order or vertices explicit.

The following lemma makes this observation formal. It is worth being proved in detail for it is used in one of the main arguments in the proof of Theorem 3.3.1 below.

Lemma 3.2.3 (Orientation)

For every birooted F, A-tree B = t, u there is a unique run of the automaton A on the birooted F, A-tree B such that ρ(1) = * . Moreover, for every v ∈ dom(t), every x ∈ A + Ā such that v ≺ p vx, we have ρ(vx) = x, i.e. ρ(vx) gives the direction towards the input root.

Proof Let B = t, u be a non zero birooted F, A-tree. Clearly, the mapping ρ : dom(t) → { * } + A + Ā inductively defined on the length of reduced words of dom(t) by ρ(1) = * and ρ(vx) = x for every x ∈ A + Ā, every v ∈ dom(t) with v ≺ p vx, is a valid run of the automaton A on B.

Conversely, let ρ : dom(t) → { * } + A + Ā be a valid run of A on B such that ρ(1) = * . We prove, by induction on the length of elements of dom(t), the announced property that also guarantees the unicity of such a run. ✷

Then we can conclude:

Corollary 3.2.4 The recognized language L(A) is the set of non zero idempotent birooted F, A-trees.

Proof Let B = t, u be a non zero birooted F, A-tree. By applying the first part of Lemma 3.2.3 there is a run ρ : dom(t) → Q with ρ(1) = * . If we assume that B is idempotent then we have u = 1 hence (ρ(1), ρ(u)) = ( * , * ) ∈ W , that is, the run ρ is an accepting run. Conversely, let ρ : dom(t) → Q be an accepting run of the automaton A on the birooted F, A-tree B. Since ρ is accepting, this means that ρ(1) = * . Hence, by applying the second part of Lemma 3.2.3, this means in particular that the input root 1 is the unique vertex in dom(B) such labeled by state * in the run ρ. Now, since ρ is an accepting run, we know that (ρ(1), ρ(u)) ∈ W hence ρ(u) = * and thus u = 1, that is, the birooted F, A-tree B is idempotent. ✷ Remark Defining the automaton A ′ just like the automaton A but taking instead W ′ = {( * , q) : q = * } for the accepting condition, the recognized language L(A ′ ) is the set of non idempotent birooted F, A-trees.

One must not deduce from these two examples that the class of languages recognizable by birooted tree automata is closed under complement. We will show below that these languages are necessarily upward closed in the natural order. Their complements are downward closed.

MSO definability and birooted tree automata

We aim now at relating the expressive power of finite birooted tree automata with language definability in Monadic Second Order (MSO). We observe that languages recognized by birooted F, A-tree automata are upward closed in the natural order. Since every such a language is definable in MSO, this upward closure property turns out to be the characteristic property of this class of languages.

Theorem 3.3.1 Let L ⊆ B(F, A) be a language of birooted F, A-trees. The language is recognized by a finite birooted F, A-tree automaton if and only if L is MSO definable and upward closed in the natural order.

Proof Let L ⊆ B(F, A) be a language of birooted F, A-trees. We first prove the easiest direction, from birooted tree automata to MSO. Then, we prove the slightly more difficult direction from MSO to birooted tree automata.

From birooted tree automata to MSO Assume that L is recognizable by a finite state birooted tree automaton A. Without loss of generality, since A is finite, we assume that the set Q of states of A is such that

Q ⊆ P({1, 2, • • • , n}) for some n ≥ log 2 |Q|.
Then, checking that a birooted tree t, u belongs to L(A) just amounts to checking that there exists an accepting run. Following a classical technique [START_REF] Thomas | Chap. 7. Languages, automata, and logic[END_REF], this can be done by means of an existential formula of monadic second order logic of the form

∃X 1 X 2 • • • X n ϕ(X 1 , • • • , X n )
with n set variables X 1 , X 2 , . . . , X n and a universal first order formula ϕ.

The sets

X 1 , • • • , X n encode the mapping ρ : dom(t) → Q defined, for every v ∈ dom(u) by ρ(v) = {i ∈ [1, n] : v ∈ X i }
Then, the formula ϕ, universally quantified, just checks that this run ρ is an accepting run. This amounts to check in the formula ϕ that the vertex and the state coherence conditions are satisfied, hence the mapping ρ is a run, and that the acceptance condition are satisfied, hence it is an accepting run. Clearly, this can be done by means of two universal FO-quantifiers. We incidentally check that, indeed, the defined language is upward closed with respect to the natural order.

From MSO to birooted tree automata Conversely, assume that L is upward closed for the natural order and that L is definable in M SO. By applying Theorem 3.1.5, there exists a finite state upward closed normalized tree automaton A = Q, I, O, T, δ that recognizes L. The intended birooted tree automaton A ′ we are seeking for is then simply defined as the automaton

A ′ = Q ′ , ∆ ′ , I ′ × F ′
with states, transitions and accepting pairs defined as follows. First, the set of states Q ′ is defined as the set of all tuples of the form

(x, q, f, m) ∈ (A + Ā + { * }) × Q × (F ∪ {⊤}) × P((A + Ā) × Q) such that: ⊲ m ∈ δ(q, f ), ⊲ if x = * then m(x) = ∅.
Second, the transition function ∆ ′ is defined by: ⊲ for every g ∈ F , the set of transitions ∆ ′ (g) ⊆ Q ′ × Q ′ is defined as the set of all pairs of states of the form ((x, q, f, m),

(x ′ , q ′ , f ′ , m ′ )) ∈ Q ′ × Q ′ with x = x ′ , q = q ′ , f = f ′ = g, and m = m ′ , ⊲ for every a ∈ A, the set of transitions ∆ ′ (a) ⊆ Q ′ × Q ′ is
defined as the set of all pairs of states of the form ((x, q, g, m),

(x ′ , q ′ , g ′ , m ′ )) ∈ Q ′ × Q ′
such that any of the following condition is satisfied:

forward transition: x ′ = ā and q ′ ∈ m(a), -backward transition: x = a and q ∈ m ′ (ā).

Last, the set of accepting pairs is defined by the set I ′ × F ′ with:

⊲ the set of input root states I ′ ⊆ Q defined as the set of all states (x, q, f, m) with x = * and q ∈ I, ⊲ the set of output root states F ′ ⊆ Q defined as the set of all states (x, q, f, m) with q ∈ F .

Intentionally, the birooted tree automaton A ′ mimics the runs of the tree automaton A by encoding, into every state of the form (x, q, f, m) ∈ Q ′ on a given vertex the following information. The direction x ∈ { * } + A + Ā marks the direction to the input root just as stated and proved in Lemma 3.2.3. The state q ∈ Q is the state of the vertex in the (simulated) run of the automaton A. The label f is (smaller than or equal to) the vertex label (when ⊤). And m is the transition that is chosen in the (simulated) run of the automaton A.

Making this intention explicit allows to prove that L(A) = L(A ′ ). For that purpose, let B = t, u be a birooted F, A-tree. (⇒) Assume that B ∈ L(A), that is, let ρ : dom(t) → Q be an accepting run of the tree automaton A on the birooted F, A-tree B.

Let ρ ′ : dom(t) → Q ′ be the mapping defined, for every v ∈ dom(t) to take ρ ′ (v) = (x, ρ(v), t(v), m) such that x = * when v = 1 and x = 1 when v = wx for some w ∈ dom(t) with w ≺ p v, and m = {(y, ρ(vy))

∈ (A + Ā) × Q : vy ∈ dom(t), v ≺ p vy}.
It is routine to check that the mapping ρ ′ is an accepting run of the automaton A ′ on B hence B ∈ L(A ′ ).

(⇐) Assume that B ∈ L(A ′ ), that is, let ρ ′ : dom(t) → Q ′ be an accepting run of the birooted tree automaton A ′ on the birooted F, A-tree B.

Let ρ : dom(t) → Q be the mapping defined, for every v ∈ dom(t), by ρ(v) = q when ρ ′ (v) is of the form (x, q, f, m) (henceforth with m ∈ δ(q, f ) and f ≤ t(v) in the trivial order on F ∪ {⊤}). Since the automaton A is assumed to be an upward closed automaton (see Definition 3.1.4), it is also routine to check that ρ is an accepting run of the automaton A on B.

✷ From now on, a language of birooted F, A-trees that is definable by a finite birooted F, A-tree automaton is called a regular language of birooted F, A-trees.

Tree languages vs birooted tree languages

We aim now at relating languages of labeled birooted trees and languages of F -trees when F is a functional signature with the arity mapping ρ : F → P(A).

Following Section 2.4, for every set X of F -trees, let L X be the language L X = { t, 1 ∈ B(F, A) : t ∈ X} of the birooted tree images of the trees of X. It is called the birooted tree image of the language X.

Remember that an F -tree t : A * → F is complete when, for every v ∈ dom(t), we have va ∈ dom(t) for all a ∈ ρ(t(v)). Theorem 3.4.1 For every regular language X of complete finite F -trees, there exists a regular language U X of birooted F, A-trees and the complement D X of a regular language of birooted F, A-trees such that

L X = U X ∩ D X .
Proof This essentially follows from Theorem 3.3.1. More precisely, let X be a regular language of finite F -tree.

We observe first that for every complete F -tree t 1 and t 2 , their birooted images t 1 , 1 and t 2 , 1 are incomparable in the natural order. It follows that the elements of L X form an anti-chain in the natural order. It follows that, given U X = {y ∈ B(F, A) : ∃x ∈ L X , x ≤ y} the upward closure of L X and D X = {y ∈ B(F, A) : ∃x ∈ L X , y ≤ x} the downward closure of L X , we have L X = U X ∩ L X . We conclude the proof by observing that if X is regular then it is definable in MSO. This implies that the languages L X , D X and U X are also definable in MSO. Since U X is upward closed and D X downward closed hence his complement is upward closed, we conclude by applying Theorem 3.3.1 that ensures that both U X and the complement of D X are regular languages of birooted trees. ✷

Adequately ordered monoids

A partially ordered monoid is a monoid M ordered by a relation ≤ that is assumed to be stable under product, that is, if x ≤ y then xz ≤ yz and zx ≤ zy for every x, y and z ∈ M . The partially ordered monoid M is an adequately ordered monoid when all subunits of M are idempotents, and for every x ∈ M , both

x L = min{y ∈ U (M ) : xy = x} and x R = min{y ∈ U (M ) : yx = x} exist.
The subunits x L ∈ U (M ) and x R ∈ U (M ) are respectively called the left projection and the right projection of x.

Examples Every monoid M extended with the trivial order x ≤ y if, and only if, x = y is an adequately ordered monoid with x L = x R = 1 for every x ∈ M . These adequately ordered monoids are called trivial.

Every inverse monoid M ordered by the natural order is an adequately ordered monoid with x L = x -1 x and x R = xx -1 for every x ∈ M . As a particular case, the monoid B(F, A) ordered by the natural order is also an adequately ordered monoid.

For every set Q, the monoid P(Q × Q) of all relations on Q ordered by inclusion is also an adequately ordered monoid with, for every X ⊆ Q × Q, the projections defined by

X L = {(q, q) ∈ Q × Q : ∃p ∈ Q, (p, q) ∈ X} and X R = {(p, p) ∈ Q × Q : ∃q ∈ Q, (p, q) ∈ X}.
The basic properties of the adequately ordered monoids are described in the following Lemmas. We refere the reader to [START_REF] Janin | Quasi-inverse monoids (and premorphisms)[END_REF] for more details. Remark One can check that, in an adequately ordered monoid M , both the left and right projections approximate the left and right Green classes [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF]. More precisely, let x and y ∈ M . We say that x and y are L-equivalent when we have x = z 1 y and y = z 2 x for some z 1 and z 2 ∈ M . Then, for every x and y ∈ M , if xLy (resp. xRy) then we have x L = y L (resp. x R = y R ).

In fact, from an equality of the form x = z 1 y we deduce that xy L = x and thus x L ≤ y L . From an equality of the form y = z 2 x, we deduce that yx L = y and thus y L ≤ x L . The case of the R-equivalence is proved similarly.

In general, the reverse implications do not necessarily hold as shown by any trivial adequately ordered monoids with non trivial L and R-classes. However, the reverse implications hold for inverse monoids [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF].

Adequate premorphisms and quasi-recognizable languages

The notion of premorphism already appears in [START_REF] Mcalister | E-unitary covers for inverse semigroups[END_REF] in inverse semigroup theory (see also [START_REF] Hollings | The Ehresmann-Schein-Nambooripad Theorem and its successors[END_REF]). It can be generalized to partially ordered monoid as follows.

Let M and N be two partially ordered monoid. A premorphism is a mapping θ : M → N such that θ(1) = 1 and, for every x and y ∈ M , we have θ(xy) ≤ θ(x)θ(y), i.e. the mapping θ is "submultiplicative", and if x ≤ M y then θ(x) ≤ θ(y), i.e. the mapping θ is monotonic. Definition 4.2.1 (Adequate premorphisms) Let M and N be two adequately ordered monoids. Assume that a notion of disjoint product is defined on M . Then, a premorphism ϕ : M → N is an adequate premorphism when for every x and y ∈ M we have θ(

x L ) = (θ(x)) L , θ(y R ) = (θ(y)) R and, if xy is a disjoint product then θ(xy) = θ(x)θ(y).
Examples When M and N are trivially ordered monoids, then the premorphisms from M to N are exactly the monoid morphisms. Since they preserve every product they are also adequate premorphisms.

When M and N are naturally ordered inverse semigroups then premorphisms from M to N have already been studied in depth (see [START_REF] Lawson | Inverse Semigroups : The theory of partial symmetries[END_REF], Chap. 3). They are already known to preserve left and right projections. However, no generic notion of disjoint product is yet defined that would allow for studying, in the abstract, adequate premorphisms between inverse semigroups.

Many other examples of adequate premorphisms derive from birooted tree automata as shown in Theorem 4.3.1 below.

It as been shown [START_REF] Janin | On languages of one-dimensional overlapping tiles[END_REF], that premorphisms into finite ordered monoids may recognize languages that are even not computable. The notion of quasi-recognizable languages, built on the notions of adequately ordered monoids and adequate premorphisms, is a remedy to this fact. Definition 4.2.2 (Quasi-recognizable languages) A language L ⊆ B(F, A) of non zero birooted trees is a quasi-recognizable language when there exists a finite adequately ordered monoid M and an adequate premorphism

θ : B(F, A) → M such that L = θ -1 (θ(L)).
Remark Every recognizable subset of A * is also quasi-recognizable. As observed above, every morphism from ϕ : A * → M with finite M is also an adequate premorphism when A * and M are trivially ordered. This means that the notion of quasi-recognizability defined here is a generalization of the classical notion of recognizability by monoids. Proof This essentially follows from the adequacy assumption and the strong decomposition property (Lemma 2.3.2). ✷

From birooted tree automata to quasi-recognizable languages

In this section, we show that every finite state birooted automaton induces an adequate premorphism that recognizes the same language.

Theorem 4.3.1 Let L ⊆ B(F, A) be a language of birooted F, A-trees. If L is recognizable by a finite state birooted tree automaton then it is recognizable by an adequate premorphism into a finite adequately ordered monoid.

Proof Let L ⊆ B(F, A) and let A = Q, ∆, W be a finite birooted tree automaton such that L = L(A).

We define the mapping ϕ A : B(F, A) → P(Q × Q) by saying that ϕ A (B) is, for every labeled birooted tree B = t, u ∈ B(F, A), the set of all pairs of state (p, q) ∈ Q × Q such that there exists a run ρ : dom(t) → Q such that p = ρ(1) and q = ρ(u). The mapping ϕ A is extended to 0 by taking ϕ A (0) = ∅. We observe that ϕ(1)

= I Q = {(q, q) ∈ Q × Q : q ∈ Q}.
The fact P(Q × Q) is an adequately ordered monoid have already been detailled in the examples above. By definition we have

L = ϕ -1 (X ) with X = {X ⊆ Q × Q : X ∩ W = 0}
It thus remains to prove that ϕ A is an adequate premorphism.

The fact ϕ A is monotonic is immediate. For every birooted F, A-tree s, u and t, v , if s, u ≤ t, v this means that u = v thus, for every run ρ : dom(s) → Q of A on s, u , the mapping ρ restricted to dom(t) is clearly a run of A on s|dom(t), u = t, u .

Left and right projections preservation immediately follows from their characterizations in both B(F, A) and P(Q × Q) and the definition of ϕ A .

We show that ϕ A is submultiplicative. Let s, u and t, v be two birooted trees. In the case s, u • t, v = 0 we are done, since ϕ A (0) = ∅. Otherwise, let ρ be a run of A on the product s, u • t, v .

By definition of the product, the mapping ρ 1 : dom(s) → Q defined by ρ 1 (w) = ρ(w) for every w ∈ dom(s) is clearly a run of A on s, u .

Similarly, the run ρ 2 : dom(t) → Q defined by ρ 2 (w) = ρ(uw) for every w ∈ dom(s) is also a run of A on t, v . Now, since ρ 1 (u) = ρ 2 (1) and that construction applies for every run ρ, this shows that

ϕ A ( s, u • t, v ) ⊆ ϕ A ( s, u ) • ϕ A ( t, v )
which proves submultiplicativity.

Last, it remains to show that ϕ A preserves disjoint products. Assume that the product s, u • t, v is disjoint. This means that s(u) ∧ t( 1) is well-defined in the trivial order on F ∪ {⊤} with dom(s) ∩ u • dom(t) = {u}.

Let (p, q) ∈ ϕ A ( s, u ) • ϕ A ( t, v ). By definition of the product of relations, this means that there exists q ′ ∈ Q, such that we have (p, q ′ ) ∈ ϕ A ( s, u ) and (q ′ , q) ∈ ϕ A ( t, v ). But then, by definition of ϕ A this means that there exist a run ρ 1 : dom(s) → Q of A on s, u and a run ρ

2 : dom(t) → Q of A on t, v such that ρ 1 (1) = p, ρ 1 (u) = q ′ , ρ 2 (1) = q ′ and ρ 2 (v) = q.
Let then ρ : dom(s) ∪ u • dom(t) → Q defined by ρ(w) = ρ 1 (w) for every w ∈ dom(s), and ρ(uw) = ρ 2 (w) for every w ∈ dom(t). Since the product of the two birooted F, A-trees is a disjoint product, we have dom(s) ∩ u • dom(t) = {u} with ρ 1 (u) = q ′ = ρ 2 (1) hence ρ is well defined. As it is clearly a run of A on the (non zero) product s, u • t, v with ρ(1) = p and ρ(uv) = q, this means we have (p, q) ∈ ϕ A ( s, u • t, v ).

As this holds for arbitrary pair of states (p, q)

∈ ϕ A ( s, u ) • ϕ A ( t, v ) this proves that ϕ A ( s, u ) • ϕ A ( t, v ) ⊆ ϕ A ( s, u • t, v
) and thus concludes the proof. ✷

Examples: on positive Boolean birooted trees

The language of the positive Boolean birooted trees and the sublanguages of these trees that evaluate to 1, are especially interesting since, following [START_REF] Potthoff | First-order logic on finite trees[END_REF], they allow for giving some finer details on the expressive power of our proposal.

Boolean birooted trees Positive Boolean birooted trees are defined from the sets of vertex labels F = {∧, ∨, 0, 1} and the set of edge labels A = {l, r}.

An example of a (partial) positive Boolean (birooted) tree is depicted in Figure 16 below. Forward edges labeled by l or r are meant to define Boolean The set of (partial) positive birooted trees is recognized by the automaton A 1 = Q 1 , ∆ 1 , W 1 defined by: ⊲ states : Q 1 = {f, c}, with state f standing for "function" and the state c standing for "constant",

∨ ∧ ∧ 1 ∨ 1 0 l r l r l r ∧ 0 r l
⊲ vertex transitions : ∆ 1 (∧) = ∆(∨) = {(f, f )}, ∆ 1 (0) = ∆ 1 (1) = {(c, c)}, ⊲ edge transitions: ∆ 1 (l) = ∆ 1 (r) = {(q 1 , q 2 ) ∈ Q 1 × Q 1 : q 1 = c}, ⊲ accepting pairs: W 1 = Q 1 × Q 1 .
One can check that the language recognized by A 1 is the set of birooted F, Atrees for which no edge exists a constant node, that is, a vertex labeled by 0 or 1.

True Boolean birooted trees Now, we want to restrict the above language of birooted F, A-trees to the birooted trees that can be evaluated to true on the input root. This can be done with the automaton

A 2 = Q 2 , ∆ 2 , W 2 defined by ⊲ states : Q 2 = B × B × B with the Boolean algebra B = {0, 1},
⊲ vertex transitions :

-constant: ∆ 2 (x) = {(q, q) ∈ Q 2 × Q 2 : q = (x, x, x)} for x = 0, 1, -conjunction: ∆ 2 (∧) = {(q, q) ∈ Q 2 ×Q 2 : q = (b 1 , b 2 , b 3 ), b 1 = b 2 •b 3 }, -disjunction: ∆ 2 (∨) = {(q, q) ∈ Q 2 ×Q 2 : q = (b 1 , b 2 , b 3 ), b 1 = b 2 +b 3 }.
⊲ edge transitions:

-left-argument: ∆ 2 (l) = {(q 1 , q 2 ) ∈ Q 2 × Q 2 , π 2 (q 1 ) = π 1 (q 2 )}, -right-argument: ∆ 2 (r) = {(q 1 , q 2 ) ∈ Q 2 × Q 2 , π 3 (q 1 ) = π 1 (q 2 )},
with π i standing for the ith projection of triples, ⊲ accepting pairs :

W 2 = {(q 1 , q 2 ) ∈ Q 2 × Q 2 : π 1 (q 1 ) = 1}.
Intendedly, in a run of the automaton A 2 on a Boolean birooted tree, the first component of every state is to be read as the possible Boolean value of the corresponding vertex, the second component as the Boolean value of its left argument, and the third component as the Boolean value of its right argument. Such a run is depicted in Figure 17. In that picture, vertices are labeled by pairs in Evaluating a partial birooted tree amounts to guessing some Boolean values for its leaves that are not labeled by constant. Edge transitions ensure the bottom up propagation (now following edge orientation) of Boolean values. Vertex transitions ensure that such a propagation is coherent with the Boolean operators ∧ or ∨ and the constants 0 and 1 that are labeling birooted tree vertices.

F × Q. ∨, (1, 1, 0) ∧, (1, 1, 1) ∧, (0, 1 , 0) 1, (1, 1, 1) 1, (1, 1, 1) 1, (1, 1, 1) 0,
This means that a birooted F, A-tree belongs to L(A 2 ) if and only if its input root can be evaluated to 1 with the missing constant leaves acting as unknown Boolean values.

Induced adequately ordered monoid One can show that the adequately ordered monoids induced by the automaton A 2 (as given by Theorem 4.3.1) is an aperiodic monoid. A software like SemiGroupe of Pin [START_REF] Pin | Semigroupe version 2.0[END_REF] allows for making such a verification. It follows that the language of all Boolean birooted tree that evaluate to true is quasi-recognized by an aperiodic monoid.

Since this language is not definable in FO, this indicates that, though we use finite monoids as recognizers, the correspondance between definability in FO and aperiodicity, that holds for recognizable languages of words, no longer holds for quasi-recognizable languages of birooted F, A-trees.

A similar observation has already been made in a slightly different context [START_REF] Potthoff | First-order logic on finite trees[END_REF].

From quasi-recognizability to MSO

We show that every quasi-recognizable language of birooted F, A-trees is definable in MSO. Theorem 4.5.1 Let θ : F IM (A) → M be an adequate premorphism with finite M . For every X ⊆ M , the language θ -1 (X) is definable in Monadic Second Order Logic.

Proof Let θ : F IM (A) → M as above and let X ⊆ M . Uniformly computing the value of θ on every birooted tree by means of an MSO formula is done by adapting Shelah's decomposition techniques [START_REF] Shelah | The monadic theory of order[END_REF].

More precisely, we show that the strong decomposition provided by Lemma 2.3.2 is definable in MSO. Then, the computation of the value of θ on every birooted rooted B can be done from the value of θ on the elementary birooted trees and the sub-birooted F, A-trees that occur in such a decomposition.

More precisely, we first show that the predecessor relation ≺ p (and thus, by transitive closure, the prefix relation ≤ p as well) is definable in MSO. This amounts to saying that there exists an MSO formula ϕ p (x, y) such that, for every birooted tree t, u , for every vertex v and w ∈ dom(t), we have t, u |= ϕ p (v, w) if and only if v ≺ p w.

Defining ϕ p (x, y) amounts to saying that there exists a partition of dom(t) in three sets of vertices X 0 , X 1 and X 2 such that the (input) root 1 belongs to X 0 , all its neighbors (or immediate successors) belong to X 1 , and for every vertex z ∈ Z distinct from the input root, given i ∈ {0, 1, 2} such that z ∈ X i , given j = i -1 mod 3 and k = i + 1 mod 3, the vertex z has a single neighbor in X j (the unique predecessor of z in the predecessor relation ≺ p ) and all other neighbors of z belong to X k (the successors of z in the predecessor relation ≺ p ).

As a consequence, since the reflexive and transitive closure of a definable binary relation is also definable in MSO, there exists a formula ϕ * p (x, y) such that t, u |= ϕ * p (v, w) if and only v ≤ p w. This also means that for every birooted tree B = t, u , the set

U = {z ∈ dom(t) : 1 ≤ p z ≤ p u}
is also MSO definable in every birooted tree t, u and, as well, for every vertex v ∈ dom(t), the sub-birooted tree B p v . Here, by saying the birooted F, A-tree B p v is definable in MSO we mean that its domain D p (v) (defined in the proof of Lemma 2.3.2) is definable and thus its structure: the vertex labels and the edge relations, is just obtained by restricting those of B to the domain D p (v).

The next step is then the following. Given a finite collection of set variables {Y s } s∈U (M ) , one variable Y s per element s ∈ U (M ), writing Y for the tuple of such variables, we claim that there exists a formula ϕ(Y ) such that for every birooted F, A-tree t, u for every v ∈ dom(t), for every subunit s ∈ U (M ), we have

t, u |= ∃Y (v ∈ Y s ∧ ϕ(Y )) if
B p v = { B p v,w • B p w R : w ∈ dom(r), v ≺ p w}
with disjoint products only and the adequacy assumption applies. As the product is of a bounded size, we can check that v ∈ Y s . Then, for every birooted tree B = t, u , given the ordered prefixes of u described by u 0 = 1 < p u 1 < p u 2 < p • • • < p u n-1 < p u n = u, we know, by applying Lemma 2. All these values are computable, either as image by θ of elementary birooted trees, or, by induction, by observing that for every prefix u ′ of u we have θ(B p u ′ ) = s ′ if and only if u ′ ∈ Y s ′ . Then, checking that v ∈ Y s by "computing" in MSO the value s can be done, say, by a left to right "traversal" of the path from 1 to u, simulating the underlying finite state word automaton induced by M on the (images of) elementary birooted trees. ✷

Quasi-recognizable languages vs MSO definable languages

For the picture to be complete, it remains to characterize the class of quasirecognizable languages with respect to the class of languages definable in Monadic Second Order Logic.

Theorem 4.6.1 Let L ⊆ B(F, A) be a language of birooted F, A-trees. The following properties are equivalent:

(1) the language L is quasi-recognizable,

(2) the language L is a finite Boolean combination of upward closed MSO definable languages,

(3) the language L is a finite Boolean combination of languages recognized by finite state birooted tree automata.

Proof The fact that (1) implies (2) essentially follows from Theorem 4.5.1. The fact (2) implies (3) immediately follows from Theorem 3.3.1. Last, we prove, by a classical argument (e.g. cartesian product of monoids) that the class of quasi-recognizable languages is closed under Boolean operations. Then, by applying Theorem 4.3.1 this proves that (3) implies (1). More precisely, let L ⊆ B(F, A) be a language of birooted F, A-trees.

(1) implies (2) We assume that L is recognized by some adequate premorphism θ : B(F, A) → M . By definition, we have L = θ -1 (θ(L)) hence

θ -1 (θ(L)) = x∈θ(L) θ -1 (D x ) ∩ θ -1 (U x )
with U x = {y ∈ M : x ≤ y} and D x = {y ∈ M : y ≤ x} for every x ∈ M . For every x ∈ M , we have θ -1 (x) = θ -1 (U x ) ∩ θ -1 (D x ). The inclusion θ -1 (x) ⊆ θ -1 (U x ) ∩ θ -1 (D x ) is immediate. Conversely, let B ∈ θ -1 (U x ) ∩ θ -1 (D x ). Since B ∈ θ -1 (U x ) we have x ≤ θ(B) and since B ∈ θ -1 (D x ) we have θ(B) ≤ x hence θ(B) = x and thus B ∈ θ -1 (x). We prove (2) by observing that both θ -1 (U x ) and θ -1 (D x ) = θ -1 (M -D x ) are upward closed (and recognized by θ) hence, by Theorem 4.5.1, they are MSO definable.

(2) implies (3) This immediately follows from Theorem 3.3.1 that ensures that every upward closed and MSO definable languages is recognized by a finite state birooted tree automaton.

(3) implies (1) Assume that L is a finite Boolean combination of languages recognized by birooted tree automata. We want to show that L is quasirecognizable.

By Theorem 4.3.1, every such a regular language is quasi-recognizable. Since the class of quasi-recognizable languages is obviously closed under complement it suffices to prove that it is closed under intersection. This is done using classical algebraic tools on monoids [START_REF] Pin | Syntactic semigroups[END_REF]. More precisely, given two adequate premorphisms θ 1 : B(F, A) → M 1 and θ 2 : B(F, A) → M 2 , the mapping θ : B(F, A) → M 1 × M 2 defined by ϕ(B) = (ϕ 1 (B), ϕ 2 (B)) is an adequate premorphism in the product monoid M 1 × M 2 ordered by the product order. Then, for every X ⊆ M 1 and Y ⊆ M 2 we have ϕ -1 1 (X) ∩ ϕ -1 2 (Y ) = ϕ -1 (X × Y ). This concludes the proof. ✷

More on quasi-recognizable languages

The following separation Theorem is based on an example that was suggested by Marc Zeitoun. 1 ) ∩ U with U the set of idempotent birooted trees. We prove that L 2 is not quasi-recognizable.

(C 0 ) • ∈ L 2 (C 1 ) • ∈ L 2 • a (C 2 ) • ∈ L 2 • a • a (C 3 ) • ∈ L 2 • a • a • a (C 4 ) • ∈ L 2 • a • a • a • a
Assume there is an adequate premorphism ϕ : B(F, A) → M into an adequately ordered monoid. We observe that the sequence {B n a •B -n a } n∈N is strictly decreasing in the natural order. By monotonicity, this means that the sequence {ϕ(B n a • B -n a )} n∈N is also decreasing. Now, if we assume that ϕ recognizes the language L 2 , this means that M is finite and since we have

Remark

The above example shows that the class of quasi-recognizable languages is not closed under product. Curiously enough to be mentioned, closure under product is true when restricting to positive birooted F, A-trees, that is, birooted F, A-trees with output roots that belongs to A * . The induced language theory is worth being studied as already started in the case of birooted words [START_REF] Dubourg | Algebraic tools for the overlapping tile product[END_REF]. With trivial vertex labeling alphabet, the monoid of positive birooted-trees is already known in algebra: it is the free ample monoid generated by the alphabet A [START_REF] Fountain | The free ample monoid[END_REF].

Conclusion

Studying languages of birooted F, A-trees, structures that generalize F -terms and F -forests, we have thus defined a notion of birooted tree automata, a related notion of quasi-recognizability and we have characterized quite in depth their expressive power in relationship with language definability in Monadic Second Order Logic. As a particular case, our results provide a new algebraic characterization of the regular languages of finite F -trees. Potential links with the preclones approach [START_REF] Ésik | On logically defined recognizable tree languages[END_REF] or the forest algebra approach [START_REF] Bojańczyk | Forest algebras[END_REF][START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF] need to be investigated further. It has been shown [START_REF] Blumensath | A syntactic congruence for languages of birooted trees[END_REF] that quasirecognizability can also be seen as a particular case of recognizability in the setting of partial algebras [START_REF] Burmeister | A Model Theoretic Oriented Approach to Partial Algebras[END_REF]. In this more general framework, a notion of (partial algebra) syntactic congruence is available. Restating the language classification results obtained in [START_REF] Bojańczyk | Forest algebras[END_REF][START_REF] Bojanczyk | Wreath products of forest algebras, with applications to tree logics[END_REF] in this new framework remains to be done.

We have already mentioned the application of this theory in computational music. Beyond these applications, it is expected that inverse semigroup theory can be developed much further towards application in computer science and engineering [START_REF] Janin | Towards a higher dimensional string theory for the modeling of computerized systems[END_REF]. Thanks to Stephen's representation theorem [START_REF] Stephen | Presentations of inverse monoids[END_REF], Munn's graphical representation theorem can be generalized to arbitrary inverse semigroup S generated by a distinguished subset A ⊆ S. It follows that, via quotient by adequate equations, the language theory that is developed here may go far beyond the study of languages of birooted trees themselves, possibly in link with recognizable languages of graphs [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

Figure 3 :

 3 Figure 3: The non zero product B 1 • B 2 of the two birooted F, A-trees B 1 and B 2 given by B 1 • B 2 = {1 → g, a → f, a b → ⊤, ab → f, aa → g, aab → f, aa b → g, aac → g}, aa b .

Figure 4 :

 4 Figure 4: The elementary birooted F, A-trees 1 (or B ⊤ ), B f , B a and B ā

Figure 5 :Definition 2 . 2 . 1 (

 5221 Figure 5: A birooted F, A-tree B and its inverse B -1 .

Figure 8 :

 8 Figure 8: A birooted tree B and some elements of its (inductive) decomposition process.

Definition 2 . 4 . 6 (

 246 Birooted encoding of ranked linear context) Every F -context is encoded into a birooted tree via the mapping ψ : C 1 (F ) → B(F, A) defined, for every linear context c ∈ C 1 (F ), by ψ(c) = c, u where u is the hole of the context c. Lemma 2.4.7 For every linear context c ∈ C 1 (F ), every tree t ∈ T (F ), we have:

Figure 10 :

 10 Figure 10: The disjoint decomposition of the bilinear context c into linear contexts and trees.

1 =

 1 , with F = {a, b, c, d}. b(c(0)) t 2 = d(a(c(0) + c(0

Figure 14 :

 14 Figure 14: From birooted F, A-trees to mono-rooted F -trees with (A+ Ā)-labeled edges.

Figure 15 :

 15 Figure 15: A run of the automaton A encoding of the prefix order via the direction to the input root.

Definition 4 . 1 . 1 (

 411 Adequately ordered monoids) Let M be a partially ordered monoid. Let U (M ) = {y ∈ M : y ≤ 1} be the set of subunits of the monoid M .

Lemma 4 . 1 . 2 Corollary 4 . 1 . 3 Lemma 4 . 1 . 4

 412413414 The set U (M ) = {z ∈ M : z ≤ 1} of the subunits of an adequately ordered monoid M is a commutative submonoid and a meet semi-lattice with product as meet.Proof In fact, let x ≤ 1 and y ≤ 1 be two subunits. By stability, we havexy ≤ 1 hence U (M ) is a submonoid of M .By stability again, we have xy ≤ x and xy ≤ y. Moreover, for every z ≤ 1, if z ≤ x and z ≤ y then, by stability and idempotency of z, we have z ≤ xy. Altogether, this proves that x ∧ y exists and x ∧ y = xy.✷ Every finite ordered monoid M with idempotent subunits is also an adequately ordered monoid.ProofTake x L = {y ∈ U (M ) : xy = x} and x R = {y ∈ U (M ) : yx = x} for every x ∈ M .✷ In an adequately ordered monoid M , the left and right projections are projections from M to U (M ), that is, for every subunit x ∈ U (M ),x L = x = x R . Proof Let x ∈ U (M ). By definition of x L , we have xx L = x hence we also have x ≤ x L . Moreover, since xx = x, we also have x L ≤ x. It follows that x = x L . A symmetrical argument proves that x = x R . ✷

Theorem 4 . 2 . 3

 423 Let θ : F IM (A) → M be an adequate premorphism with finite M . For every B ∈ B(F, A) the image θ(B) of the birooted F, A-tree B by the adequate premorphism θ is uniquely determined by the structure of B, the structure of M and the image by θ of elementary birooted F, A-trees. Moreover, it is computable in time linear in the size of B.

Figure 16 :

 16 Figure 16: An (idempotent) partial positive Boolean birooted tree B connective arguments and vertices labeled by 0 or 1 are meant to define Boolean constant.The set of (partial) positive birooted trees is recognized by the automaton A 1 = Q 1 , ∆ 1 , W 1 defined by:

Figure 17 :

 17 Figure 17: The unique run of A 2 on the tree B

  3.2, thatB = B p u0 • B p u0,u1 • B p u1 • • • B p un-1 • B p un-1,un• B p un with disjoint products only. It follows, by adequacy of θ, that the value of θ(B) can be computed as the element s ∈ M defined by s = θ(B p u0 )θ(B p u0,u1 )θ(B p u1 ) • • • θ(B p un-1 )θ(B p un-1,un )θ(B p un )

Corollary 4 . 6 . 2

 462 The birooted image of every regular languages of F -tree is recognizable by an adequate premorphism in a finite adequately ordered monoid.Proof This follows from Theorem 3.4.1 and Theorem 4.6.1.✷

Theorem 4 . 7 . 1

 471 There exists an MSO definable language of birooted F, A-trees that is not quasi-recognizable.Proof Let F = {•} and A = {a} be the trivial alphabets. Let B a be the elementary birooted tree defined by B a = t, a with dom(t) = {1, a}. Let thenL 1 = {B 2n a : n ∈ N} and let L 2 = {B 2n a • B -2n a: n ∈ N}. These birooted trees are depicted in Figure18below.

Figure 18 :

 18 Figure 18: The birooted treesC n = B n a • B -n a with C 0 < C 1 < C 2 < C 3 < C 4 < • • • .Obviously, both the languages L 1 and L 2 are definable in MSO. Moreover,L 2 = (L 1 • L -11 ) ∩ U with U the set of idempotent birooted trees. We prove that L 2 is not quasi-recognizable.

2

 2 this also implies that the sequence {ϕ(B n a • B -n a )} n∈N is strictly decreasing which contradicts the finiteness of M . ✷

  and only if θ(B p v ) = s. This amounts to saying that {Y s } s∈U (M ) form a partition (with possible empty sets) of dom(t) such that, for every vertex v ∈ dom(t), if v is a leaf with respect to the prefix order≤ p then s = θ(B p v ) = θ(B t(v)) and we check that v belongs to Y s . If v is not a leaf, then we must have v ∈ X s with, by adequacy assumption on θ, the value of s that is uniquely determined bys = {(θ(B p v,w ) • s w ) R : v ≺ p w} with s w ∈ M is the unique element of M such that w ∈ Y sw .By the proof of Lemma 2.3.2, we know that

This collapse of expressive power arises even in the absence of inverses themselves as illustrated by the recognizable languages of positive birooted words studied in[START_REF] Janin | On languages of one-dimensional overlapping tiles[END_REF].

in such a case, it is common to say that the product u•w in F G(A) is reduced as presented.

otherwise, there is no need of a zero

Quasi-recognizable languages of labeled birooted treesThe notion of quasi-recognizable languages, that is, languages recognized by adequate premorphisms into finite adequately ordered monoids, is defined in this section. Then, its expressive power is studied and related to both birooted automata and Monadic Second Order logic.

Acknowledgment

The author wishes to express his gratitude to the anonymous referees for providing many helpful comments on earlier versions of this work.

* Partially funded by project INEDIT, ANR-12-CORD-0009 † Temporary research fellow at CNRS/INS2I (2013-2014)