(en français)

En logique mathématique, on distingue les objets mathématiques, ou structures, et leurs propriétés, ou logique. Les structures à leur tour sont constituées d'éléments et de relations entre ces éléments. Dans cette thèse, nous travaillerons uniquement sur ce que l'on appelle des "graphes colorés dont les arcs sont étiquetés", c'est-à-dire des structures dont les relations sont d'arité au plus 2. De plus, ces structures seront dénombrables -on peut numéroter chaque objet avec un entier -et de présentation finie -il existe une quantité finie d'information permettant de représenter la structure de façon non ambigüe.

"Un chemin entre deux sommets blancs est en pointillés ou passe par un sommet noir." La logique la plus simple est celle dite du premier ordre, car elle manipule simplement les éléments proprement dits de la structure considérée. Elle permet d'exprimer des propriétés du type "tout sommet colorié en noir a un voisin blanc" ou "s'il existe un sommet blanc, alors il existe 3 arcs distincts en pointillés". Elle est cependant restreinte à des propriétés ponctuelles et ne dit rien sur la structure dans sa globalité. Une solution est alors de considérer une logique plus forte, qui permet de manipuler directement des ensembles d'éléments. C'est la logique du second ordre monadique, qui permet d'exprimer des propriétés raisonnablement compliquées. Des exemples classiques sont "il y a un chemin entre x et y" ou "le sous-arbre t est infini". On la notera souvent par le sigle MSO.

De façon générale, la logique du second ordre désigne l'ensemble des formules qui parlent des relations entre les éléments. Mais elle a le défaut d'être paradoxalement trop puissante; elle échappe ainsi aux outils usuels de l'informatique, selon la définition donnée CHAPTER 1. INTRODUCTION ci-après. C'est pourquoi on se restreint aux relations qui ne prennent qu'une variable : ce sont bien les ensembles. Ceci explique l'adjectif monadique.

Notre problème n'est pas de connaître entièrement une structure donnée, mais de savoir exprimer ses propriétés. Cette nuance autorise l'usage d'un automatisme. En effet, la question qui se pose est alors la suivante.

Étant données une logique et une structure, existe-t-il un algorithme qui prenne en entrée une formule close de cette logique et renvoie oui ou non selon que la structure satisfait la formule ou non? C'est la question de la décidabilité de du model-checking de la logique à laquelle appartiennent les formules que l'on veut tester. Savoir construire un tel algorithme est un défi majeur de l'informatique d'aujourd'hui, car cette question est naturellement liée à la notion de vérification de programmes. En effet, savoir si un programme fait effectivement ce que l'on veut -par exemple, savoir s'il termine -est expressible par une formule, que doit vérifier la structure des configurations du programme.

Construction de structures

Par exemple, un résultat fondemental de Rabin [START_REF] Michael Rabin | Decidability of second-order theories and automata on infinite trees[END_REF] indique que l'arbre binaire complet, esquissé Figure 1.2, a une théorie monadique décidable. Plus généralement, pour une logique donnée, peut-on espérer trouver une caractérisation de toutes les structures qui jouissent de la même propriété? Probablement pas, mais cela n'empêche pas les scientifiques de chercher à en décrire le plus possibles. En particulier, pour la logique du second ordre monadique, l'intérêt de la communauté scientifique se porte sur la hiérarchie à pile [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF], aussi appelée hiérarchie de Caucal. Pour décrire historiquement cette hiérarchie, il nous faut remonter à [START_REF] Muller | The theory of ends, pushdown automata, and second-order logic[END_REF], où les auteurs s'intéressent aux graphes des configurations des automates à piles en partant d'une configuration donnée. Il caractérisent exactement ces graphes par un critère géométrique : si on fixe un sommet, et que l'on retire successivement ce sommet, puis les sommets à distance 1, puis à distance 2 et ainsi de suite, on obtient une suite de graphes. Le résultat fondamental est que l'ensemble de ces graphes est fini à isomorphisme près : la suite se répète. Cette propriété leur permet d'étendre le résultat de Rabin à tout une classe de graphes. Ce résultat sera étendu dans [START_REF] Courcelle | Graph rewriting: An algebraic and logic approach[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic[END_REF] aux graphes HR-équationnels.

On a donc deux manières de décrire ces graphes, que l'on peut appeler définition interne -en choisissant un ensemble pour les sommets, et les arcs comme des relations entre ces sommets -ou externe -par les propriétés structurelles du graphe. Si l'on préfère, ces deux approches considèrent que les objets importants sont respectivement les sommets ou les arcs. Dans [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF], le même principe est appliqué pour définir une classe plus large, celle des graphes préfixe-reconnaissables. Ceux-ci sont à la fois définis par des relations de récriture préfixe entre des mots, et par des transformations de graphes à partir d'un graphe fini.

Dans cette thèse, nous utiliserons le plus souvent la caractérisation externe, qui décrit un graphe en donnant une série de transformations à partir d'un arbre fini; un graphe sera donc par définition un ensemble d'arcs. Il y aura deux transformations fondamentales. D'une part, le dépliage d'un graphe renvoie l'arbre des chemins dans ce graphe à partir d'un sommet donné. D'autre part, l'interprétation monadique permet de "réorganiser" de façon régulière la structure d'un graphe. Ces deux opérations préservent la décidabilité de la logique monadique. En partant de la classe des graphes finis, puis en appliquant un dépliage suivi d'une interprétation, on obtient la classe des préfixe-reconnaissables. En itérant ce processus, on obtient une suite de classes de graphes distinctes : c'est la hiérarchie à pile, décrite par Caucal [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF].

Ordinaux

Une autre famille de graphes ayant une logique MSO décidable est bien plus connue. C'est la classe des ordinaux dénombrables, ou classe d'ordres totaux ayant la propriété de bon ordre, c'est-à-dire que chaque sous-ensemble non vide doit avoir un plus petit élément. Ils ont été introduits par Cantor [START_REF] Cantor | Beiträge zur begründung der transfiniten mengenlehre[END_REF] qui en formule les propriétés de base. Ces objets sont fréquemment utilisés dans les mathématiques actuelles. Ils généralisent l'arithmétique des nombres entiers, et surtout bénéficient des preuves par induction : si on prouve qu'une propriété vraie pour tout β < α est vraie pour α, on a alors établi la propriété de façon générale.

Büchi [START_REF] Büchi | Decision methods in the theory of ordinals[END_REF][START_REF] Büchi | The monadic theory of all countable ordinals[END_REF], en utilisant des automates, a prouvé la décidabilité de la logique MSO pour les ordinaux dénombrables; il a été suivi par Shelah [START_REF] Shelah | The monadic theory of order[END_REF] par une méthode compositionnelle entièrement différente.

Il est donc naturel de chercher l'intersection de ces deux grandes familles. Cette thèse prend donc sa racine dans la question suivante : Quels sont exactement les ordinaux du niveau n de la hiérarchie à pile? La question est d'autant plus importante que les exemples concrets de graphes dans la hiérarchie sont nombreux au premier niveau, mais beaucoup moins par la suite. Depuis [START_REF] Maslov | The hierarchy of indexed languages of an arbitrary level[END_REF] et [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF], on sait que la hiérarchie est bien séparée en classes distinctes, mais avoir une collection d'exemples aussi simples que les ordinaux établirait une forme de "mesure de complexité" de la hiérarchie. Dans l'autre sens, la réponse permettrait de mieux comprendre les ordinaux par l'étude des méchanismes nécessaires à leur construction Dans le même ordre d'idée se pose la question plus générale des ordres linéaires, c'està-dire des classes d'ordres totaux n'ayant pas la propriété de bon ordre, dont Z en est le premier exemple. Evidemment, il existe des ordres linaires dénombrables dont la logique MSO n'est pas décidable, même assez simples. On cherche donc un seul sens : un critère nécessaire pour ces ordres. Pour commencer, il est naturel de chercher du côté des ordres dispersés (scattered ), c'est-à-dire ne contenant pas de sous-ordre isomorphe à Q. Cette classe bien connue a été classifiée par Hausdorff [START_REF] Hausdorff | Grundzüge einer theorie der geordnete mengen[END_REF] qui donne une "mesure ordinale" pour chaque ordre. Il existe donc un lien des ordres dispersés vers le cas plus simple et plus connu des ordinaux.

Automates et ordres

L'intersection du domaine des structures liées à des automates et de celui des ordinaux a fait naître bien d'autres résultats. Au sens le plus large, d'anciens travaux de Church [START_REF] Church | The constructive second number class[END_REF] et Kleene [START_REF] Kleene | On notation for ordinal numbers[END_REF] établissent quels sont les plus grands ordinaux récursifs, c'està-dire qui peuvent être exprimés par une machine de Turing. Nous nous intéressons ici à des modèles de calcul plus simples, plus proches du domaine des structures automatiques, c'est-à-dire dont les relations sont définies par un transducteur fini, c'est-à-dire un automate à deux entrées. Les résultats [START_REF] Delhommé | Automaticité des ordinaux et des graphes homogènes[END_REF][START_REF] Khoussainov | Automatic linear orders and trees[END_REF] établissent que les ordinaux automatiques sont plus petits que ω ω , et que les ordinaux arbre-automatiques -où le transducteur reconnaît des relations sur les arbres -sont ceux plus petits que ω ω ω . De la même manière, de récents résultats [B É09, B É10] définissent les ordres linéaires et les ordinaux aux premiers niveaux de la hiérarchie à pile : les ordinaux du deuxième niveau sont plus petits que ω ω ω , et les ordres dispersés ont un rang de Hausdorff plus petit que ω ω . C'est cette voie que cette thèse poursuivra.

Il est également naturel de considérer la notion d'ordre linéaire coloré, c'est-à-dire de mots sur un alphabet fini, mais indexés par un ordre infini : par exemple, un nombre réel entre 0 et 1 peut être vu comme un mot sur l'alphabet [0, 9] indexé par N, ou de façon équivalente comme l'ordre ω coloré par l'alphabet [0, 9]. Les mots infinis acceptés par automates de Büchi [START_REF] Büchi | On a decision method in the restricted second-order arithmetic[END_REF] sont le premier exemple de tels ordres. Un tel automate accepte un mot indexé par N s'il passe infiniment de fois dans un état final. Cette définition a été adaptée dans [START_REF] Nivat | Ensembles reconnaissables de mots biinfinis[END_REF] pour considérer les mots bi-infinis, c'est-à-dire indexés par Z. Büchi [START_REF] Büchi | Decision methods in the theory of ordinals[END_REF] décrit également le processus d'un automate acceptant des mots indexés par des ordinaux, ce qui lui permet de montrer la décidabilité de la logique MSO. Plus récemment, Bruyère et Carton [START_REF] Bruyère | Automata on linear orderings[END_REF][START_REF] Bruyère | Hierarchy among automata on linear orderings[END_REF][START_REF] Bès | A Kleene theorem for languages of words indexed by linear orderings[END_REF] ont considéré des automates acceptant des mots indexés par des ordres dispersés, et obtiennent un théorème de Kleene.

Arbres solutions de schémas récursifs

La notion de mot infini indexé par N mérite également qu'on la recherche dans la hiérarchie à pile. Les premiers mots infinis que l'on rencontre sont les mots ultimement périodiques, qui sont les plus simples des mots infinis. A l'étape suivante, on voit apparaître des mots plus complexes, connus sous le nom de mots morphiques : ce sont les points fixes d'application de morphismes. Si ∆ est une lettre, et que τ est un morphisme tel que τ (∆) est un mot commençant par ∆, alors τ (τ (∆)) également, et ainsi de suite : on obtient alors un mot infini. Ce sont là -à codage près -les mots morphiques.

Cette définition s'approche assez de la construction de termes de la hiérarchie à pile par les schémas récursifs. Ces objets, introduits semble-t-il par Ianov [START_REF] Ianov | The logical schemes of algorithms[END_REF] au premier niveau, puis par Nivat [START_REF] Nivat | Langages algébriques sur le magma libre et sémantique des schémas de programme[END_REF], ont été amenés à l'ordre supérieur par Damm [START_REF] Damm | Languages defined by higher type program schemes[END_REF][START_REF] Damm | The IO-and OI-hierarchies[END_REF]. On peut parler de grammaires de termes : considérons deux ensembles typés dits terminaux et non-terminaux, et également l'ensemble des termes sur ces ensembles en suivant le typage. Chaque non-terminal F a une règle de récriture prenant en compte les arguments de F , de telle façon qu'un terme ayant pour tête ce non-terminal se récrit en un terme. On répète alors l'opération sur un nouveau non-terminal. Même si l'opération est infiniment répétée, de tels schémas peuvent avoir un arbre limite, point fixe de l'opération : c'est une solution du schéma récursif. On a donc une manière simple de construire un arbre infini avec des règles de récriture.

Ces schémas ont récemment été remis sur le devant de la scène, notamment grâce aux travaux [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF][START_REF] Knapik | Higher-order pushdown trees are easy[END_REF] sur la décidabilité de la logique MSO sous une contrainte dite de sûreté, puis en retirant cette contrainte dans [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF][START_REF] Knapik | Unsafe grammars and panic automata[END_REF]. En particulier, les arbres sûrs sont exactement les arbres-termes de la hiérarchie. Pour en revenir aux questions évoquées plus haut, il semble naturel de relier les schémas du premier ordre avec les mots morphiques, et de vérifier que l'on obtient bien les seconds comme ordres sous-tendus par les premiers. Se pose alors la question de la généralisation : comment faire évoluer la notion de mot morphique pour coller à celle de schéma récursif d'ordre supérieur?

Plan et contributions

Le chapitre 2 fixe les notations et les objets utilisés, en commençant par les notions de graphe et d'arbre. Nous rappelons les définitions et premières propriétés des ordres linéaires, ainsi que le cas particulier des ordinaux. Enfin, nous décrivons la hiérarchie à pile par les transformations de graphes.

Dans le chapitre 3, nous illustrons la définition interne de la hiérarchie par la construction d'ordinaux et de puissances du type d'ordre de Z par des transformations de graphes. Le résultat important est que les ordinaux plus petits qu'une tour exponentielle d'ω de taille n+1 sont dans le n-ième niveau de hiérarchie; ceci inclut donc tous les ordinaux plus petits que ε 0 , qui est le plus petit ordinal tel que ω ε 0 = ε 0 . Une définition interne due à [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF] est donnée, et est encore illustrée par les ordinaux. Enfin, nous nous interrogeons sur une propriété essentielle des ordinaux : d'après Büchi [START_REF] Büchi | Decision methods in the theory of ordinals[END_REF], la logique monadique ne peut pas toujours distinguer deux ordinaux. Pour chaque ordinal plus petit que ε 0 , nous exhibons alors une structure aussi expressive n'ayant pas cette contrainte. Les résultats de ce chapitre apparaissent pour la plupart dans [START_REF] Braud | Covering of ordinals[END_REF].

Le chapitre 4 établit le résultat inverse : il prouve que la tour d'exponentielle de taille n + 1 ne peut être dans le n-ième niveau de la hiérarchie. Pour ce faire, nous commençons par établir l'égalité entre ordres comme graphe de la hiérarchie et structure des feuilles, dans l'ordre lexicographique, des arbres de la hiérarchie. Ce résultat nous permet de raisonner par récurrence sur le niveau de la hiérarchie. Nous obtenons un résultat similaire sur le rang de Hausdorff des ordres dispersés, qui mesure une certaine complexité de l'ordre. Enfin, les mêmes techniques aboutissent à un résultat sur la taille des sous-arbre finis des peignes de la hiérarchie, c'est-à-dire des arbres ayant une unique branche infinie, qui est la branche la plus à droite. Ce chapitre apparaît en grande partie dans [START_REF] Braud | Linear orders in the pushdown hierarchy[END_REF].

Le dernier chapitre approche la hiérarchie pas le biais des schémas de récursion d'ordre supérieur. Nous y considérons les feuilles des arbres solutions de ces schémas formant des mots de type ω. Si l'on considère des arbres réguliers, il est simple de voir que ces mots sont ultimement périodiques. Au niveau suivant, nous prouvons que l'on obtient exactement les mots dits morphiques. Ce résultat est alors étendu au niveau supérieur et définit une nouvelle classe de mots bénéficiant des propriétés des graphes de la hiérarchie. Ces résultats font l'objet d'un article en cours de préparation [Bra].

(in English)

Mathematical logic distinguishes mathematical objects, or structures, and their properties, or logic. These structures are in turn made of elements and relations between these elements. In this thesis, we will only work on "colored graphs with labeled arcs", that is structures where relations are of arity at most 2. Moreover, these structures will be countable -the objects can be numbered -and of finite presentation -there is a finite amount of data allowing an unambiguous representation of the structure.

"Each path between two white vertices is hashed or goes through a black vertex." The simplest logic is the so-called first-order logic, and it only quantifies the proper elements of the given structure. We can express properties like "every black vertex has a white neighbour" or "if there at least one white vertex, then there are at least 3 distinct hashed arcs". It is nonetheless limited : for instance, over graphs of bounded degree, it is restricted to local properties, as testified by Gaifman's locality theorem [START_REF] Gaifman | On local and non-local properties[END_REF]. A solution is then to consider a stronger logic, which directly considers sets of elements. This is called the monadic second-order (MSO) logic; it can express more complex properties, like "there is a path between x and y", or "the deterministic subtree t is infinite". More generally, second-order logic is a system where variables range over relations between elements. But is has the paradoxal drawback of being too powerful; usual tools (e.g. decision procedures) of computer science cannot reach this logic. This is why we restrict ourselves to relations with only one variable : these are exactly sets. This explains the adjective monadic.

Our problem is not to know entirely a given structure, but to know its properties. This subtelty allows the use of an algorithm. The question is indeed the following.

For a given logic and structure, is there an algorithm taking a closed formula of this logic and returns whether the formula is true in the structure or not?

It is the question of decidability of the model-checking of the logic in a given structure. Knowing how to build such an algorithm is a challenge of modern computer science, since this question is naturally linked to program verification. Indeed, the required behaviour of a program can be expressed by a formula, which should be checked by the structure of configurations of the program.

Structure constructions

For instance, a fundamental result of Rabin [START_REF] Michael Rabin | Decidability of second-order theories and automata on infinite trees[END_REF] states that the complete binary tree, drawn in Figure 1.4, has a decidable monadic theory. More generally, for a given logic, can we hope to find a characterisation of all structures enjoying the same property? Probably not, but this does not forbid scientists to try and describe as much of these structures as possible. For monadic second-order logic, the scientific community is interested in the pushdown or Caucal hierarchy. The history of this hierarchy goes back to the result of Muller and Schupp [START_REF] Muller | The theory of ends, pushdown automata, and second-order logic[END_REF], where the authors study the configuration graphs of pushdown automata starting from a given configuration. They characterize these graphs with a geometrical criterion. Given a vertex, we remove this vertex, then the vertices a distance 1, then distance 2, and so on. We get a sequence of graphs. The fundamental result is that the resulting set of connected graphs is finite up to isomorphism : the sequence repeats itself. This property extends the result of Rabin to a larger class of graphs, and is extended to HR-equational graphs in [START_REF] Courcelle | Graph rewriting: An algebraic and logic approach[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic[END_REF].

We have therefore two ways to describe these graphs, which can be called inner definition -by giving a set of vertices and constructing relations between vertices -and outer definition -via structural properties of the graph. Said differently, this approach considers that the main objects are respectively the vertices or the arcs. In [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF], the same idea is applied to define the larger set of prefix-recognizable graphs. These graphs also have a twofold definition : one by rewriting relations on words, and the second with graph transformations from a finite graph.

In this thesis, we will most of the time use the external characterization. That is, a graph will be described by a sequence of transformations from a finite tree. There will be two main transformations. First, the unfolding of a graph from one of its vertices yields the tree of the paths from this vertex. Second, the monadic interpretation "reorganizes" the structure in a regular way. These two operations preserve the decidability of modelchecking for monadic second order logic. Starting from the set of finite graphs, and applying an unfolding and an interpretation, we get the set of prefixe-recognizable graphs. By iterating this process, we get a sequence of distinct classes of graphs : it is the pushdown hierarchy, described by Caucal [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF].

Ordinals

Another well-known class of graphs having a decidable MSO logic is the class of countable ordinals, or total orders having the well-ordering property, i.e. where each nonempty subset has a smaller element. They have been introduced by Cantor [Can97] who formulated basic properties. For instance, they generalize the arithmetic of natural number, and enjoy induction proofs : if a property true for all β < α is true for α, then it is true for all ordinals.

With the use of automata, Büchi [START_REF] Büchi | Decision methods in the theory of ordinals[END_REF][START_REF] Büchi | The monadic theory of all countable ordinals[END_REF] proved the decidability of modelchecking of MSO logic for each countable ordinal; it was followed by Shelah, who proves the same result by the very different compositional method.

It is therefore natural to study the intersection of these two large families. This thesis takes its root in the following question :

What are exactly the ordinals found in the n th level of the pushdown hierarchy?

The importance of this question relies on the fact that we have many known examples of graphs in the hierarchy in the first levels, but very few in the next. Since [START_REF] Maslov | The hierarchy of indexed languages of an arbitrary level[END_REF] and [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF], we know that the hierarchy is separated into distinct classes. Nonetheless, a collection of examples as simple as ordinals would establish a "complexity mesure" of the hierarchy. In the other direction, we could have a better understanding of ordinals by studying the mechanisms used in their construction.

The question of more general linear orders follows immediately. We consider the classes of total orders not having the property of well-ordering, the first example being Z, < . Of course, many of those orders have an undecidable monadic theory, even when restricting to countable orders. We look for one direction, i.e. a necessary criterion for these orders. For a start, it is natural to look at scattered orders, i.e. not having any suborder isomorphic to Q. This well-known class of orders has been classified by Hausdorff [Hau08] where he gives an "ordinal measure" for countable scattered orders. There is therefore a link between scattered orders and the easier case of ordinals.

Orders and automata

It is not the first time that the domain of structures linked to automata meets ordinals. For the upper bounds, works of Church [START_REF] Church | The constructive second number class[END_REF] and Kleene [START_REF] Kleene | On notation for ordinal numbers[END_REF] state which are the greatest recursive ordinals, i.e. which can be expressed by a Turing machine. We study here simpler models of computation. For instance, this thesis is closer to works related to automatic structures, which relations are defined by a finite tranducer, i.e. an automaton with several entries. Results of [START_REF] Delhommé | Automaticité des ordinaux et des graphes homogènes[END_REF][START_REF] Khoussainov | Automatic linear orders and trees[END_REF] state that automatic ordinals are smaller that ω ω , and that tree-automatic ordinals -where the tranducer works on trees instead of words -are smaller that ω ω ω . In the same way, recent results [B É09, B É10] characterize orders of the first levels of the pushdown hierarchy : ordinals of the second level are smaller than ω ω ω , and scattered orders have a Hausdorff rank smaller than ω ω . This thesis follows this direction.

It would also be natural to consider the notion of colored linear order, that is words on a finite alphabet, but indexed by an infinite order : for instance, a real number between 0 and 1 can be seen as a word on the alphabet [0, 9] indexed by N, or equivalently as the order ω colored by the alphabet [0, 9]. Infinite words accepted by Büchi automata [START_REF] Büchi | On a decision method in the restricted second-order arithmetic[END_REF] are the first examples of these orders. Such an automaton accepts a word indexed by N if it passes infinitely many time through a final state. This definition was adapted in [START_REF] Nivat | Ensembles reconnaissables de mots biinfinis[END_REF] to consider bi-infinite words, i.e. indexed by Z. Büchi [START_REF] Büchi | Decision methods in the theory of ordinals[END_REF] also describes the process of words indexed by ordinals, and shows decidability of MSO logic for each such structure. Recently, Bruyère and Carton [START_REF] Bruyère | Automata on linear orderings[END_REF] considered automata accepting words indexed by scattered orderings. They reached a stronger Kleene theorem, which was then extended in [START_REF] Bruyère | Hierarchy among automata on linear orderings[END_REF][START_REF] Bès | A Kleene theorem for languages of words indexed by linear orderings[END_REF].

Solutions of recursion schemes

The notion of infinite words indexed by N is of central importance and deserves to be also studied in the hierarchy. The first encountered infinite words are the ultimately periodic words, which are the simplest ones. At the next level, more complex words appear : they are known as morphic words, because they can be built as fixpoints of morphisms on letters. If ∆ is a "starting" letter, and τ is such that τ (∆) begins with ∆, then τ (τ (∆)) also does, and so on. We get therefore an infinite word. Up to a final coding, this defines the morphic words.

This definition is rather close of the construction of terms in the hierarchy by recursion schemes. These objects were introduced by Ianov [Ian60], then Nivat [START_REF] Nivat | Langages algébriques sur le magma libre et sémantique des schémas de programme[END_REF], and have been brought to the higher order by Damm [START_REF] Damm | Languages defined by higher type program schemes[END_REF][START_REF] Damm | The IO-and OI-hierarchies[END_REF]. They can be called term grammars. Let terminals and nonterminals be two typed sets; we can consider the set of terms on these sets respecting the typing rules. Each nonterminal F has a rewriting rule taking in consideration the arguments of F , in such a way that a subterm having F as head symbol can be naturally rewritten in another subterm. The operation is then repeated on another nonterminal. Even if this algorithm does not terminate, a recursion scheme admits a limit (possibly infinite) tree : it is called the solution of the recursion scheme. We have therefore a simple way to construct an infinite tree with rewriting rules.

These schemes were recently reconsidered by the works [KNU01, KNU02] on the decidability of MSO logic under the constraint of safety, then removing this constraint in [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF][START_REF] Knapik | Unsafe grammars and panic automata[END_REF]. In particular, the safe trees are exactly the term-tress of the hierarchy. To go back to the forementioned questions, it is natural to link the firstorder schemes with morphic words. We can check that we get the latter as orders hidden in the former. The natural question is therefore : what happens in the next levels? How can we extend the notion of morphic word to stick to the notion of recursion scheme?

Outline and contributions

The first chapter sets notations and defines the objects used. We begin by the notions of graph and tree, then linear orders and the particular case of ordinals. We then describe the pushdown hierarchy through graph transformations.

Chapter 3 illustrates the internal definition by the construction of ordinals and powers of Z with the help of graph transformations. The important result is that ordinals smaller that a exponential tower of ω of size n + 1 are all in the n th level of the hierarchy; this includes therefore all ordinals smaller than ε 0 , the smallest ordinal such that ω ε 0 = ε 0 . An internal definition due to [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF] is given and illustrated by ordinals again. Next we try and avoid an essential property of ordinals : according to Büchi [START_REF] Büchi | Decision methods in the theory of ordinals[END_REF], MSO logic cannot distinguish two ordinals in general. For each ordinal smaller than ε 0 , we exhibit a structure as expressive as the ordinal but which can be characterized by MSO logic. Most of the results of this chapter appear in [START_REF] Braud | Covering of ordinals[END_REF].

Chapter 4 states the converse result : it shows that the n + 1-exponential tower of ω cannot be in the n th level of the hierarchy. For this result, we start by stating the equality between orders as graphs of the hierarchy and the structure of leaves in lexicographic order of trees of the hierarchy. This result allows the application of induction on the hierarchy. We get a similar result on the Hausdorff rank of scattered orders, measuring a certain complexity of orders. The same techniques lead to a result on the size of subtrees of combs of the hierarchy, i.e. trees having a unique infinite branch. A large part of this chapter appears in [START_REF] Braud | Linear orders in the pushdown hierarchy[END_REF].

The last chapter defines the hierarchy by higher-order recursion schemes. We consider here the case where leaves of trees solution of these schemes form words of type ω. If we consider regular trees, it is easy to see that these words are ultimately periodic. At the next level, we show that we get exactly the morphic words. This result is then extended to the next level and defines a new class of words enjoying the properties of graphs of the hierarchy. These results are gathered in an article in preparation [Bra].

Chapter 2 Preliminaries

This chapter introduces the notions used thoughout the thesis. It begins with simple structures, namely words, graphs and trees. Then orders are detailed, in particular ordinals and other scattered orderings. Then we look at the logics used to express properties. This leads us to the logical graph transformations, which in turn defines the pushdown hierarchy.

Notations and first structures

This thesis is about countable structure enjoying a finite presentation, i.e. described by a finite quantity of information.

We make a frequent use of representation of graphs with arcs labeled by {0, 1}. To lighten the pictures, arcs labeled by 1 are drawn with plain lines and arcs labeled by 0 with hashed lines. Exceptions as Figure 5.4 will be clearly labeled. The powerset of a set S is noted P(S); the closed interval between a and b is noted [a, b]; the index i of a sequence s is noted s i , even in the case when i is an infinite ordinal.

Finite words

The set of words over a finite alphabet Σ is noted Σ * . The length of u ∈ Σ * is noted |u|, and the empty word is ε. We say that u is

prefix of v, noted u ⊑ v, if there is w ∈ Σ * such that u • w = v. If w = ε, u is a strict prefix of v, noted u ⊏ v.
On the contrary, if u, v are incomparable by ⊑, we note u⊥v. In any case, the longest common prefix of two words u, v is noted u ∧ v.

When Σ is provided with an order <, the lexicographic order < lex on Σ * is defined by

u < lex v ⇐⇒      u ⊏ v, or u = w • a • w ′ and v = w • b • w ′′
where w, w ′ , w ′′ ∈ Σ * , a < b.

The collection of regular languages over an alphabet Σ is defined recursively.

L := ∅ | {a} where a ∈ Σ | L • L | L ∪ L | L *

Structures

The notion of structure can be seen as a formal logical framework to express mathematical objects. The following definition will be seldom used as such, but it is the general definition of the objects found in this thesis.

A signature is a finite set (R i ) i∈I of relation symbols, each symbol R i having an arity |R i |. A structure on this signature is a pair (U, ν) where U is a set called universe and the valuation ν is a mapping R i → P(U |R i | ) called the interpretation of the signature. Commonly I = [1, k], and a structure is written U, (R 1 , . . . , R k ) where the valuation is implicit.

Given a universe U and a valuation ν, a binary relation

ν(R) is said reflexive if ∀x ∈ U, (x, x) ∈ ν(R); symmetric if ∀x, y ∈ U, (x, y) ∈ ν(R) ⇒ (y, x) ∈ ν(R); antisymmetric if ∀x, y ∈ U, (x, y) ∈ ν(R) ⇒ ¬(y, x) ∈ ν(R); transitive if ∀x, y, z ∈ U, (x, y) ∈ ν(R) ∧ (y, z) ∈ ν(R) ⇒ (x, z) ∈ ν(R).
Two structures U, ν and U ′ , ν ′ are isomorphic, noted U, ν ≃ U ′ , ν ′ , when there is a bijection π between their signatures which preserves arity, and a bijection κ between U and U ′ preserving valuation of corresponding relation symbols, i.e. for any relation

R, κ(ν(R)) = ν ′ (π(R)).
A structure is countable if is isomorphic to a structure whose universe is a subset of N. In this thesis, we only consider this kind of structures.

Example 2.1.1. A finite word of length k > 0 over an alphabet Σ is a structure of universe [1, k] whose signature consists of one binary relation S (successor) and unary relations (R a ) a∈Σ . The valuation maps S to all pairs (i, i + 1) and each R a to the set of indexes of letter a; thus [1, k] = a∈Σ ν(R a ). The same definition is used for ω-words.

Later on, we will equivalently consider words as structures with binary relation S * , i.e. the reflexive and transitive closure of S, with valuation on all pairs (i, j) such that i < j.

Graphs

The graphs we consider are countable, directed and labeled. Let Σ be a finite set called arc label set. A labeled graph G, or simply graph, is a subset of V × Σ × V where V is a finite or countable set. An element (s, a, t) of V × Σ × V is an arc of source s, target t and label a, and is written s

a -→ G t or simply s a → t if G can be understood from the context.
The notation s → t means "s a → t for some a". Note that we do not consider graphs with multiplicity : there can be only one arc labeled by a between s and t.

Let Γ be another finite set called color set. A colored graph (or labeled and colored graph) is a subset of (V × Σ × V ) ∪ (Γ × V ). More commonly, a graph labeled by Σ is called a Σ-graph, and a Σ-graph colored by Γ is called a Σ, Γ-graph. Note that an equivalent definition would be to allow only one color in P(Γ) per vertex; we prefer the more versatile definition which allows to add or remove colors.

The set of all vertices appearing in G is its support V G , i.e. having a color or being linked to an arc. Hence, graphs are always considered up to mute vertices, i.e. not appearing in G. This can be a matter of discussion for limit cases, especially when a graph has only one vertex. Therefore we may always suppose that all vertices of the support are colored with a "base color".

A graph is deterministic if there are no arcs with the same label that share the same source, i.e. for all a ∈ Σ, if s a → t and s a → t ′ then t = t ′ . The in-degree (resp. out-degree) of a vertex x is the cardinal of the set {y | y → x} (resp. {y | x → y}).

Example 2.1.2. The graph shown in Figure 2.1 is known as the ladder. Its support is V G = {aa i , a i b} i∈N and it is defined by

G = {a i 1 → a i+1 | i > 0} ∪ {a i 0 → a i-1 b | i > 0} ∪ {a i b 1 → a i-1 b | i > 0}.
From a logical point of view, a (colored) graph G can be associated to a structure of universe V G and of signature (R a ) a∈Σ ∪ (R c ) c∈Γ where R b has arity 2 or 1 when b belongs respectively to Σ or Γ. The valuation of this structure maps R a → {(x, y) | x a → y ∈ G} for a ∈ Σ and similarly R c → {x | (c, x) ∈ G} for c ∈ Γ. We will often confuse the graph and its associated structure. Two graphs are isomorphic (still noted ≃) if the CHAPTER 2. PRELIMINARIES corresponding structures are.

A (colored) path in a colored graph G is a sequence p on G such that if p i = x a → y or p i = (c, y) then p i+1 belongs to ({y} × Σ × V G ∪ Γ × {y}) ∩ G.
An uncolored path is such a sequence only of arcs of G. A path is simple if the p i are pairwise distinct.

To consider only the "shape" of the graph, one can consider the delabeled graph where all colors are removed and all arcs labels are replaced by the same label. An unlabeled graph is a class of graphs isomorphic under the delabeling operation. When the arc label set of a graph is labeled by a singleton, we sometimes confuse this graph and the corresponding unlabeled graph.

Deterministic trees

A vertex r of a graph G is called a root when there is a path from r to any other vertex. A graph G is a tree if it has a unique root r such that for any vertex in the graph there exists a unique path from the root r to this vertex. The notions of Σ-and Σ, Γ-graph yield the respective notions of Σ-and Σ, Γ-tree.

For deterministic trees, we may therefore consider a tree presentation of the graph as follows. The root is associated to the empty word ε and for each arc u a → v, we identify v and u • a. Formally, a deterministic tree over an ordered alphabet Σ is a subset T of Σ * closed by prefix. If u ⊏ v, we say that u is an ancestor of v or equivalently that v is a descendant of u. Immediate ancestors and descendants are respectively called father and son. Elements of T are called nodes and nodes without proper descendant are called leaves.

Finally, a colored deterministic tree t is a mapping from a deterministic tree T to a finite set of colors Γ. We note Dom(t) = T the domain of this mapping.

A deterministic tree is prefix of its leaves (or is a prefix tree) if it is equal to the prefix-closure of its set of leaves. A deterministic tree is a binary tree when Σ = {0, 1}. It is said to be full if every node has exactly 0 or |Σ| sons, and complete when every node has |Σ| sons . See the complete (uncolored) binary tree in Figure 1.2.

A branch of t is a maximal subset B of Dom(t) such that if x ∈ B, then all ancestors of x and at most one son of x are in B.

Linear orderings

Linear orderings are the main object of study throughout this thesis. The reason is that they form easily understandable examples with simple properties and nonetheless an arbitrary complexity, for instance in the sense detailed in Section 2.2.2. For a comprehensive introduction to linear orderings, see [START_REF] Rosenstein | Linear orderings[END_REF][START_REF] Roitman | Introduction to Modern Set Theory[END_REF].

A linear ordering, total ordering or simply ordering, is a structure whose signature consists in only one binary relation ≤ which is reflexive, antisymmetric and transitive. Nonetheless, when the universe is not a singleton, we will most of the time consider the structure over the associated irreflexive relation <; this avoids numerous case distinctions.

The order type is an isomorphism class of orders. In our graph vocabulary, it is equivalent to say that an order type is an unlabeled graph of linear orderings. Since we work up to isomorphism, we will often confuse a given ordering with its order type.

The reverse operation * is a mapping from an ordering V, < to the ordering V, < * where x < * y ⇐⇒ y < x. Notable order types include

• the finite orderings noted 0, 1, . . . , k, . . . ;

• the usual ordering of N, noted ω;

• the ordering of N in reverse order, ω * ;

• the usual ordering of Z, noted ζ;

• the usual ordering of Q, noted η;

• the usual ordering of R.

This thesis is dedicated to countable structures, so we will never consider the ordering of R.

The subordering relation is defined on order types by α β iff there is an ordering of type β which has a restriction of type α. This relation is extended to orderings when the order types are similarly ordered. For instance we have ω ζ η, but neither ω ω * nor ω * ω. As we will see later, an order not having η as a suborder is called scattered. An interval I of L is a restriction of L to a subset where if x, y are elements of I and there is z in L such that x < z < y, then z is an element of I.

Let Γ be a finite set of colors. A colored ordering of an ordering V, < is a mapping V → Γ. As hinted by the notations, a (resp. colored) ordering can be associated to a (resp. colored) graph. Consequently, we deliberately confuse the objects and will indifferently use the structural or graph notation.

An ω-word or (mono-)infinite word is a colored ordering of type ω.

There is an available arithmetics on linear orderings : more precisely we use addition and multiplication. Formally, these noncommutative operations are defined as follows. See also [START_REF] Rosenstein | Linear orderings[END_REF].

U, < U + V, < V = U ⊎ V, < U,V
where x < U,V y iff x, y ∈ U and x < U y or x, y ∈ V and x < V y or x ∈ U and y ∈ The graph representation of the ordinal ω + 2. Graph representations of ordinals are hardly readable due to many arcs. The lighter notion of covering graphs will be described in Section 3.4.

V. U, < U . V, < V = V × U, < lex . where (u, v) < lex (u ′ , v ′ ) iff u < U u ′ or u = u ′ ∧ v < V v ′ .

Ordinals

A particular kind of linear orderings are the well-orderings, which have the following equivalent properties :

• each nonempty subset has a smallest element;

• there is no infinite strictly decreasing sequence.

An ordinal is the order type of some well-ordering. However, as noted in Section 2.1.3, we often will identify the order type with the ordering; for instance, the sentence "the ordinal α belongs to the class X" means actually "there is an ordering of order type α in the class X".

All ordinals are themselves well-ordered by the subordering relation. For any ordinal α, the set of ordinals greater than α has a smallest element, which we call the successor of α. The reverse operation, the predecessor, is not defined everywhere. The set where predecessor is defined is naturally called the set of successors, or ordinals of the first kind in old literature; its complementary is called the set of limit ordinals, or ordinals of the second kind. The supremum sup(X) of a set X of ordinals is the smallest ordinal greater than each ordinal in X.

The set-theoretical (or Von Neumann) approach defines each ordinal as the set of smaller ordinals. For instance, 0 = ∅ and 1 = {∅}. We borrow this encoding to define the canonical graph of α as the ordinal graph where vertices are exactly ordinals smaller than α. The fact that we consider graphs up to mute vertices is not a problem, because the equality relation is always implicit; in particular 1 = 0, because there is one non-mute vertex in 1.

Arithmetics

Arithmetic operations can be defined in two ways : either by transfinite iteration or by giving an isomorphic structure. The very first operation available is the successor relation. Then addition is the transfinite iteration of successor, multiplication is the iteration of addition, and exponentiation is the iteration of multiplication :

α + 0 = α, α + (β + 1) = (α + β) + 1, for limit λ, α + λ = sup β<λ (α + β). α.0 = 0, α 0 = 1, α.(β + 1) = α.β + α, α β+1 = α β .α, for limit λ, α.λ = sup β<λ α.β. α λ = sup β<λ α β .
This definition of addition and multiplication matches the structural definition for general linear orders given above. A similar direct definition is available for exponentiation [Ros82, Exercise 3.45]. The reverse lexicographic order means s < rlex t iff ∃α such that s α < t α and for all δ > α, s δ = t δ .

Proposition 2.2.1. β α is isomorphic to the set of α-sequences of β where finitely many elements are non-zero, ordered by reverse lexicographic order.

Proof. When α = 0, β 0 = 1, and there is indeed only one empty sequence. When α = γ+1, β α = β γ .β is the cartesian product β×β γ by lexicographic order, or equivalently β γ × β in reverse lexicographic order. By induction β γ is the set of (finitely non-zero) γ-sequences of β in reverse lexicographic order, which yields the result.

When α is a limit ordinal, let x be an α-sequence where finitely many elements are non-zero. In particular, there is a smallest index γ such that x γ ′ = 0 for all γ ′ ≥ γ. Then x can be mapped to an ordinal smaller than ω γ . This mapping is an isomorphism from (finitely non-zero) α-sequences to ω α . When β = ω, the following definition is easier to use. This is the form we will adopt later on.

Corollary 2.2.2. ω α is isomorphic to the set of finite decreasing sequences of α in lexicographic order.

There is a similar form for some scattered orders; see Section 3.2. We use the Knuth notation [START_REF] Knuth | Coping with finiteness[END_REF] to express more complex operations. The operation ↑ 1 is the exponentiation.

α ↑ n+1 0 = 1; α ↑ n+1 (β + 1) = α ↑ n (α ↑ n+1 β); α ↑ n+1 λ = sup β<λ α ↑ n+1 β for limit λ.
In this thesis we use the case n = 2 and note ↑ 2 =↑↑. It will mostly be used to express ordinals of the form

ω ↑↑ k = ω ω ... w k .
Indeed, this thesis is restricted to ordinals smaller than ε 0 = ω ↑↑ ω.

Remark 2.2.3. This notation is not the generalization of addition, multiplication and exponentiation, because the iteration is done on the right side. If we chose to follow this definition, the operation ↑↑ ′ succeding to exponentiation would rather be defined by

α ↑↑ ′ 0 = 1; α ↑↑ ′ (β + 1) = (α ↑↑ ′ β) α ; α ↑↑ ′ λ = sup β<λ α ↑ n+1 β for limit λ, which would give ω ↑↑ ′ 2 = ω ω , but ω ↑↑ ′ 3 = (ω ω ) ω = ω ω.2 and ω ↑↑ ′ ω = ω ω ω .
This notation is closely related to the family of Veblen functions [START_REF] Veblen | Continuous increasing functions of finite and transfinite ordinals[END_REF]. Let ϕ 0 be a continuous increasing function, i.e. an increasing function such that lim n ϕ 0 (α n ) = ϕ 0 (lim n α n ). For α > 0, ϕ α is the continuous increasing function enumerating common fixed points of (ϕ β ) β<α . In particular, the case ϕ 0 : x → ω x yields a family of functions known as the Veblen hierarchy, and ϕ 1 (α) = ω ↑↑ α. These functions define in fact the ε-numbers.

Cantor normal form

Cantor states a fundamental tool for ordinal analysis. Theorem 2.2.4 ( [START_REF] Cantor | Beiträge zur begründung der transfiniten mengenlehre[END_REF]). Let α be an ordinal. Then α can be uniquely written in the form

ω γ 1 .c 1 + • • • + ω γ k .c k
where γ 1 > • • • > γ k and k, c 1 , . . . , c k are natural numbers ( i.e. finite ordinals).

We will call this form the reduced Cantor normal form (RCNF ), denoted by α. We call Cantor normal form (CNF ) the following version

α = ω γ 1 + • • • + ω γ k where γ 1 ≥ • • • ≥ γ k .
Since this thesis is restricted to ordinals smaller than ε 0 , we have also the additional property α > γ 1 , which allows induction.

Scattered orderings and Hausdorff rank

A linear order is dense if for each x < y, there is a z such that x < z < y. There are only five countable dense order types, depending on whether there is an upper and/or lower bound. They are 1, η, 1 + η, η + 1 and 1 + η + 1.

A linear order is scattered if it does not contain any infinite dense subordering. Ordinals are a particular case of scattered linear orders. However, scattered orders are not necessarily well-orderings; consider for instance ζ or ω + ω * . For a detailed presentation, we refer the reader to [START_REF] Rosenstein | Linear orderings[END_REF].

The following result shows that all linear orders are combinations of these two kinds.

Theorem 2.2.5 (Hausdorff [Hau08]). Any linear ordering L is a dense sum of scattered linear orderings; that is, there is a dense linear ordering D and a map h from D to scattered orderings such that L = i∈D h(i).

In this section we focus on countable scattered orders. A more constructive characterization is provided by Hausdorff Theorem which also gives a measure of the complexity of such orders. From now on, we only consider countable scattered orders.

Theorem 2.2.6 (Hausdorff [START_REF] Hausdorff | Grundzüge einer theorie der geordnete mengen[END_REF]). A countable linear order is scattered if and only if it belongs to α V α where

V 0 = {0, 1} V β = i∈Z L i | ∀i, L i ∈ α<β V α
The Hausdorff rank of a scattered order L, written r(L) (or sometimes V D(L) in the literature), is the smallest α such that L belongs to V α . For instance, we have r(ζ) = r(ω) = 1 and r(ω

+ ω * ) = 2.
As the classes V α are not closed under finite sum, we do not have in general that r(A + B) = max(r(A), r(B)). It is natural to consider W α , the closure under finite sums of V α (i.e. L ∈ W α iff L = i∈[1,m] L i for some L 1 , . . . , L m ∈ V α ). The associated notion of rank, called ∼-rank and written r(L), is the smallest ordinal α such that L ∈ W α . This definition can be found in [START_REF] Khoussainov | Automatic linear orders and trees[END_REF] under the denomination V D * (L). As V α ⊆ W α ⊆ V α+1 , we have r(L) ≤ r(L) ≤ r(L)+1. Along this thesis, we will mostly use this alternate version of the Hausdorff rank.

For instance, the following proposition states that the ∼-rank of the ordinal ω α is α. More generally if α is written k i=1 ω α i in Cantor's normal form then r(α) = α 1 .

Proposition 2.2.7. For any ordinal α, r(ω α ) = r(ω α ) = α.

Proof. To show that r(ω β ) = r(ω β ), we only need to show that if

ω β ∈ W α then ω β ∈ V α .
Assume that for some β, ω β belongs to W α . By definition,

ω β = δ 1 + . . . + δ n with δ i ∈ V α for all i ∈ [1, n]. There exists j ∈ [1, n] s.t. δ j = ω β .
Otherwise, from the definition of ω β , we would have δ j ≤ ω γ i • k i for some γ i < β and k i < ω. We would have ω β ≤ ω max i γ i • i k i < ω β which brings the contradiction.

A straightforward transfinite induction on α shows that for all ordinal β, ω β ∈ V α if and only if β ≤ α.

The following facts are useful properties on scattered orders. CHAPTER 2. PRELIMINARIES Proposition 2.2.8. Let (L i ) i∈Z be a family of scattered orders and let α be an ordinal :

1. if L i L j then r(L i ) ≤ r(L j ); 2. for all n ≥ 1, there exists j ∈ [1, n] s.t. r( i∈[1,n] L i ) = r(L j );
3. r( i∈Z L i ) ≥ α iff either there exists i ∈ Z s.t. r(L i ) ≥ α or for all α ′ < α, there exist infinitely many i s.t. r(L i ) ≥ α ′ ; 4. r( i∈Z L i ) ≤ α iff for all i ∈ Z, r(L i ) ≤ α and there are only finitely many i such that r(L i ) = α.

Remark 2.2.9. The two conditions of property 3 are not exclusive. Take for instance

L 0 = (ω ω ) * , for k > 0, L k = ω k and L -k = 0. Then r(L 0 ) = r( Z L i ) = ω, and r(ω k ) = k.
Remark 2.2.10. It is not difficult to see that we can "inverse Z", i.e. that r(

i∈Z L i ) = r( i∈ω+ω * L i ).
We may therefore replace Z by ω + ω * in the previous proposition. This fact will be used in Proposition 4.4.7.

Proof. Property 1. Let L and L ′ be two scattered orders s.t. L L ′ . From [Ros82, Lem. 5.14], r(L) ≤ r(L ′ ). Assume that r(L) = α. This means that L is equal to the finite sum i∈[1,n] L i where for all

i ∈ [1, n], r(L i ) ≤ α. As L ′ L, L ′ is equal to a finite sum i∈[1,n] L ′ i where for all i ∈ [1, n], L ′ i L i . Hence for all i ∈ [1, n], r(L i ) ≤ r(L i ) ≤ α. This shows that r(L) ≤ r(L) = α.
Property 2. This property can be seen as a particular case of [KRS05, 4.2]. More simply, for i ∈ [1, n], r(L i ) ≤ α by property 1. If r(L i ) < α for all i, then [1,n] L i can be written as a finite sum of (Hausdorff) orders strictly smaller than α and therefore r( [1,n] L i ) < α. Property 3. [⇒] Suppose there is an α ′ < α such that r(L i ) < α ′ for all i. Then each L i is a finite sum of orders of (Hausdorff) rank smaller than α ′ . This means L = i∈Z L i is in V α ′ and therefore L has Hausdorff rank α ′ . This would mean r(L) ≤ α ′ < α.

So for each α ′ < α, {i | r(L i ) ≥ α ′ } is nonempty. If it is always infinite, the proof is done. Otherwise, there is α ′ < α such that this set is finite. Let I be a finite interval containing it. If we write

L = i<I L i + i∈I L i + i>I L i ,
since for i / ∈ I we have r(L i ) < α ′ then r( i<I L i ) < α and r( i>I L i ) < α by the above paragraph. By property 2, this means r( i<I L i ) = r(L), and by property 2 again, this means there is a i ∈ I such that r(L i ) = r(L) ≥ α.

[⇐] If there is i such that r(L i ) ≥ α, then by property 1, r(L) ≥ r(L i ) ≥ α. We suppose only the second property is fulfilled. If α is limit, for each α ′ < α there is a L ′ L such that α ′ ≤ r(L ′ ). So α ′ < r(L) for each α ′ < α and α ≤ r(L). Since r(L) ≤ r(L) + 1 and α is limit, r(L) ≥ α. If α = α ′ + 1, there is infinitely many i such that r(L i ) = α ′ . So r(L) ≥ α ′ , and if actually r(L) = α ′ , there would only be finitely many such i by property 4, part [⇒]. So r(L) > α ′ and r(L) ≥ α.

Property 4. [⇒] Property 1 ensures that r(L i ) ≤ r(L) ≤ α. Suppose I = {i | r(L i ) = α} is infinite. Since I L i L, by property 1, r( I L i ) = α.
This means I L i is a finite sum of orders of (Hausdorff) rank smaller or equal to α. One of these orders M is such that there is an infinite I ′ ⊆ I with I ′ L i M . By the definition of the Hausdorff rank, we may write i∈I ′ L i j∈Z M i where r(M j ) < α for each j ∈ Z. Consider any i which is not an extremum of I (i is neither the first nor the last element). Then there is j - i and j + i such that L i

j + i j=j - i M i . So L i is a finite sum of orders of rank < α : r(L i ) ≤ max j∈[j - i ,j + i ] r(M j ) < α, which is a contradiction. [⇐] If r(L) > α,
since there is no i such that r(L i ) > α, by property 3 part [⇒], there would be infinitely many i such that r(L) = α, which is not the case. So r(L) ≤ α.

Orders in a deterministic tree

Whenever we talk about a deterministic tree, we always may assume that the alphabet is ordered. Thus, the nodes are also ordered by the lexicographic ordering. The frontier of a deterministic tree Fr(t) is the (colored) order of its leaves by lexicographic ordering. We sometime say that a node u is to the left (or right) of a node v to say that u < lex v (resp. v < lex u).

Other orders in deterministic trees that are worth of interest include

• the lexicographic order Dom(t), < lex on the whole tree, not just on leaves.

• the Kleene-Brouwer ordering Dom(t), < KB as seen in [START_REF] Rogers | Theory of recursive functions and effective computability[END_REF], where

x < KB y ⇐⇒ y ⊏ x ∨ (x⊥y ∧ x < lex y).
The equivalence of these three orders with regard to Hausdorff rank will be established in Proposition 4.4.8, and needs the powerful Proposition 4.4.3. For the time being, let us satisfy with the following result.

Proposition 2.2.11. If t is a det. prefix tree which frontier is a well-ordering, then Dom(t) is well-ordered by < lex .

Proof. By contraposition, suppose there is an infinite strictly decreasing sequence of nodes of t. In particular, there is an infinite strictly decreasing subsequence of strictly increasing lengths. If x < lex y and |x| > |y|, then y ⊑ x and for any y ′ , x ′ such that y ⊑ y ′ , x ⊑ x ′ , we have x ′ < lex y ′ . Since t is prefix, there is therefore an infinite strictly decreasing sequence of leaves in t, so t cannot yield a well-ordering.

In contrast, as soon as t is an infinite tree, it has an infinite branch which has order type ω * by < KB ; so the Kleene-Brouwer ordering is not a well-ordering unless t is finite.

Logic

First-order logic

We fix a countable set V 1 of first-order variables x, y, z, . . . . Let (R i ) i∈I be a signature. Formulae over this signature are of the form

ϕ := ⊤ | ϕ ∧ ϕ | ¬ϕ | ∃x ϕ | R i (x 1 , . . . , x |R i | ) where x 1 , . . . , x |R i | ∈ V 1 .
Here ⊤ is the "true" constant, ∧ is the logical conjonction, ¬ is the negation, ∃ is the existential quantifier. It is well-known that additional operators can be encoded, namely the constant ⊥ ("false"), disjonction ∨, the implication ⇒ and the universal quantifier ∀.

There is a priori no relation of equality between variables; however, it is often implicit in first-order logic, and will reveal itself useless in monadic logic.

The set of free variables of ϕ is the set of variables appearing but not quantified in ϕ. We note as usual ϕ(x 1 , . . . , x n ) when the set of free variables of ϕ is {x 1 , . . . , x n }. A formula without free variables is called a closed formula or statement. We note S |= ϕ when the structure S satisfies a closed formula ϕ. More generally, for a given formula ϕ(x 1 , . . . , x n ), we note S |= ϕ[a 1 , . . . , a n ] when the structure S satisfies the formula ϕ where the variable x i is interpreted as the element a i .

The first-order theory of a structure S is the set of closed formulae satisfied by S. It is said to have a decidable first-order theory when this set is recursive, as seen in Section 2.3.3.

Example 2.3.1. The determinism on Σ-graphs can be checked with the following formula when the equality relation is allowed.

a∈Σ ∀x, y, z (x a → y ∧ x a → z) ⇒ y = z Example 2.3.2.
The first-order logic can express the property that a given graph of label set {<} is an order graph. strict order : ∀x, y (¬(x

< → y ∧ y < → x)) ∀x, y, r ((x < → y ∧ (y < → r) ⇒ x < → r) total order : ∀x, y (x < → y ∨ y < → x ∨ x = y)

Monadic second-order logic

The monadic logic extends the first-order logic with new variables interpreted as sets, and a new relation ∈ for membership. Let V 2 be a new set of second-order variables, noted with uppercase letters. A formula ϕ is defined by

ϕ := R i (x 1 , . . . , x |R i | ) | x ∈ X | ϕ ∧ ϕ | ¬ϕ | ∃x ϕ | ∃X ϕ where x, x 1 , . . . , x |R i | ∈ V 1 and X ∈ V 2 .
Empty set ∅, subset relation ⊆, union ∪, intersection ∩, complementation \ are all naturally embedded in MSO-logic, as is second-order equality. By the means of a formula expressing singletons,

singleton(X) := ∃x ∈ X (∀Y (x ∈ Y ⇒ X ⊆ Y )),
first-order equality is also naturally expressible, which solves the problem of having an equality relation in the signature or not.

Example 2.3.3. Adding the following MSO-formula to Example 2.3.2 characterizes structures of signature {<} which are well-orderings. well order :

∀X = ∅, ∃x(x ∈ X ∧ ∀y(y ∈ X ⇒ (x < → y ∨ x = y)))
The set of all monadic formulae satisfied by a structure G is called the monadic theory of G and is noted MTh(G).

Decidability

An important problem of logicians is to decide whether a formula is satisfied by a given structure.

Question 2.3.4. "Model-Checking Decidability" : For a given structure, find an algorithm taking as input a monadic formula and outputting whether the structure satisfies the formula or not.

On orders, the earlier result is by Büchi [START_REF] Büchi | On a decision method in the restricted second-order arithmetic[END_REF]. He introduces the notion of (now called) Büchi automaton, which is a finite-state automaton accepting an infinite sequence iff there is a run which visits at least one of the final state infinitely often. He then proves that each monadic second-order formula can be effectively converted into a Büchi automaton.

Theorem 2.3.5 ( [START_REF] Büchi | The monadic theory of all countable ordinals[END_REF]). The monadic theory of ω is decidable.

Later on, the possibility of transfinite runs was added to the automata. Using Theorem 3.4.2 explained in Section 3.4, we get the following theorem. These results are summed up in [START_REF] Büchi | The monadic theory of all countable ordinals[END_REF]. [START_REF] Büchi | Decision methods in the theory of ordinals[END_REF]). The monadic theory of each countable ordinals is decidable.

Theorem 2.3.6 ([
Shelah [START_REF] Shelah | The monadic theory of order[END_REF] (see also Gurevich [Gur85]) developped an "automata-free" method, now called the compositional method. For a finite sequence k of integers, it defines the notion of k-type of a structure, which is expressive enough to say whether a given formula is satisfied in the structure or not. The composition theorem states that it is possible to compute the k-type of a sum with the types of the summands. With this tools, the two results above are restated. A useful introduction to this method appears in [START_REF] Thomas | Ehrenfeucht games, the composition method, and the monadic theory of ordinal words[END_REF], as well as a comparison between Büchi's and Shelah's methods.

For other orders, the theory of η was proved to be decidable. By using Theorem 2.2.5, it is possible to prove that the theory of all countable orders, i.e. the set of formulae that are true for any order, is decidable. Some results also appeared for uncountable structures. Büchi proved that the theory of ω 1 , the first uncountable ordinal, in decidable, whereas Shelah proved that the theory of the real order was not.

On other structures, the most famous case is the complete binary tree, already seen in Figure 1.2. The proof employs automata on infinite trees.

Theorem 2.3.7 ( [START_REF] Michael Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]). The monadic theory of the complete binary tree is decidable. This theorem was generalized by the regular, then prefix-recognizable graphs, and later by the whole pushdown hierarchy presented in Section 2.5. It may be defined by operations, i.e. graph transformations preserving decidability of MSO logic; some of them are shown in Section 2.4. For more on this subject, see for instance the recent survey [START_REF] Blumensath | Logical theories and compatible operations[END_REF].

In the other way around, a classical example of undecidable monadic theory is the two-dimensional grid, which can be presented as the graph of support N × N and arcs

{(i, j) a → (i + 1, j), (i, j) b → (i, j + 1) | i, j ∈ N}.
The grid is the configuration graph of an automaton with two unary pushdown stacks. It has the same expressive power as a Turing machine; therefore properties like reachibility are not decidable.

Proposition 2.3.8 ( [START_REF] Seese | The structure of the models of decidable monadic theories of graphs[END_REF]). The grid has an undecidable monadic theory.

Graph transformations

This section presents some of the transformation we will use through this thesis. They are here classified by increasing "impact" on the graph. The graph interpretations preserve vertices, but change arcs; a particular case is the graph coloring, which also preserves arcs. The graph expansions extend or completely change the set of vertices.

In regard of Section 2.3.3, it is important to note that all these transformations are MSO-compatible, i.e. they preserve decidability of the monadic theory.

Graph interpretations

These operations re-arrange arcs between existent vertices without adding new vertices. They are presented in decreasing strength. Later in Remark 4.1.4, the TWA-interpretation will be mentioned.

The generic form of interpretation is defined by I = {ϕ a } a∈Σ ∪{ϕ c } c∈Γ , where {ϕ a } a∈Σ is a set of (to be defined) binary formulae and {ϕ c } c∈Γ is a set of unary formulae . The interpretation of a graph G is then

I(G) = {x a → y | G |= ϕ a (x, y)} ∪ {(c, x) | G |= ϕ c (x)}
An example of very strong interpretation is the set interpretation developped in [START_REF] Colcombet | Transforming structures by set interpretations[END_REF]. In this case, each formula ϕ a is a monadic formula with two second-order free variables. This interpretation is not MSO-compatible, but if G has a decidable weak monadic logic, then I(G) has a decidable first-order logic.

Monadic interpretation

A MSO-interpretation I is a finite set {ϕ a } a∈Σ ∪ {ϕ c } c∈Γ of monadic second-order (MSO) formulae with two or one free individual variables. The interpretation of a graph G ⊆ V × Σ × V is the graph I(G) defined by

I(G) = {x a → y | x, y ∈ V ∧ G |= ϕ a (x, y)} ∪{(c, x) | x ∈ V ∧ G |= ϕ c (x)}.
A MSO coloring is a particular case of interpretation where binary formulae are in the form ϕ a (x, y) = x a → y, i.e. an interpretation which do not change the labeling of the graph.

Example 2.4.1. The frontier of a deterministic tree is a MSO-interpretation of this tree.

On a binary tree (arc labels {0, 1}), let

I = {ϕ < } ∪ {ϕ c } c∈Γ . ϕ < (x, y) := ¬∃x ′ (x → x ′ ) ∧ ¬∃y ′ (y → y ′ ) ∧∃z (z 0(0+1) * ----→ x ∧ z 1(0+1) * ----→ y) and for any c, ϕ c (x) := (c, x) ∧ ¬∃x ′ (x → x ′ ).
This example is easily extended to the case of any alphabet Σ.

Inverse rational mapping

Another particular case of monadic interpretation is inverse rational mapping. For a given alphabet Σ, we use the disjoint alphabet Σ to read the arcs backwards. For a rational language L over Σ ∪ Σ, the formula p L -→ q is defined inductively.

p ∅ - → q iff p = p (or any false formula) p {ε} --→ p p {c} --→ p iff (c, p) p {a} --→ q iff p a → q, for any a ∈ Σ p {ā} --→ q iff q a → p, for any a ∈ Σ p L+L ′ ---→ q iff p L -→ q ∨ p L ′ -→ q p L.L ′ --→ q iff ∃r(p L -→ r ∧ r L ′ -→ q) p L ⋆ -→ q iff ∀X(p ∈ X ∧ Closed L (X) ⇒ q ∈ X)
where

Closed L (X) ≡ ∀x, y ∈ X((x ∈ X ∧ x L -→ y) ⇒ y ∈ X).
An inverse rational mapping is a monadic interpretation I = {ϕ a } where each formula

is of the type ϕ a (x, y) = x h(a) --→ y or ϕ a (x) = x h(a)
--→ x and h(a) is a rational language. In this case I is also noted h

-1 . Example 2.4.2. The formula ∃z (z 0(0+1) * ----→ x ∧ z 1(0+1) * ----→ y) used in Example 2.4.1 can be translated into the more compact x ( 0+ 1) * 01(0+1) * ---------→ y.
As this example hints, it was shown that the inverse rational mapping is not a strong constraint on deterministic trees.

Proposition 2.4.3 ([Car06, Prop. 3.2.1]). For any Σ, Γ and monadic interpretation I, there is a monadic coloring µ and a rational interpretation h -1 such that for all deterministic Σ, Γ-tree t,

I(t) = h -1 (µ(t)).
There are even more specific variants of inverse rational mapping. We will see in Section 5.1.2 a version called deterministic rational mapping where the underlying automaton can only branch when looking at colors. It was designed to preserve determinism of graphs.

An even more narrow case is when the language L a is a finite language for each a. This case is naturally called an inverse finite mapping.

Graph expansions

These transformations map a graph G towards a tree or tree-like structure based on G. They are also the source of new vertices for structure of the hierarchy.

Monadic transduction

The MSO-transduction (see the survey [START_REF] Courcelle | Monadic second-order definable graph transductions: A survey[END_REF] for more details) aims at making monadic interpretations more flexible by adding some vertices. Formally, when K is a finite alphabet, a K-copying operation associates to G a (Σ ∪ K)-labeled graph G ′ :

V G ′ = V G ∪ (V G × K) G ′ = G ∪ {x k → (x, k) | k ∈ K}.
A MSO-transduction T = (K, I) is a K-copying operation followed by an MSO interpretation.

Unfolding

The unfolding of a graph from a given vertex is the tree of all paths in the graph from this vertex.

Formally, the unfolding Unf(G, r) of a graph G from a vertex r ∈ V G is the tree T s.t. for all a ∈ Σ, π a → π ′ ∈ T if and only if π and π ′ are two paths in G starting from r and π ′ = π • (s a → t). Moreover for any color c ∈ Γ, (c, π) ∈ T if and only if π is a path in G starting with r and ending in t with (c, t) ∈ G.

When the graph has exactly one root, the shortcut Unf(G) is used to designate the unfolding from this root. A classic example is the unfolding of the ladder (presented in Figure 2.1), shown in Figure 2.3.

The MSO-compatibility of this operation is a particular case of the Muchnik theorem (Th. 2.4.5 below). It has to be noted that the root must be definable by a monadic formula. A counterexample in [START_REF] Carayol | Automates infinis, logiques et langages[END_REF]Rem. 3.3.5] shows that the result is false without this constraint. The idea is that there is a forest of trees with decidable monadic theory where at least one tree with undecidable theory is "hidden".

Treegraph

This operation first appears in a weak form in [START_REF] Shelah | The monadic theory of order[END_REF]. The standard form appears in [START_REF] Semenov | Decidability of monadic theories[END_REF] and is attributed to Muchnik, who never published it. The treegraph of a graph G, noted Treegraph(G), is the set

{x a → y} ⊆ V + G × (Σ G ∪ {#}) × V + G where (x, y) ∈ V + G are sequences of vertices of G, and either • a ∈ Σ G , x = wp, y = wq where w ∈ V * G and p a → q ∈ G,
• or a = #, x = wp and y = wpp.

One can also see the treegraph as the fixpoint of the operation which, to each vertex which is not starting point of an # arc, adds this arc leading to the location of this vertex in a copy of G. The starting graph is called the root graph.

The following result is due to Muchnik, but the first complete proof only appears in [START_REF] Walukiewicz | Monadic second-order logic on tree-like structures[END_REF].

Theorem 2.4.5 (Muchnik). The treegraph operation is MSO-compatible.

The pushdown hierarchy

The pushdown hierarchy -sometimes called the Caucal hierarchy -is a family of sets of graphs having a decidable monadic theory. It covers actually two families : one noted (Graph n ) n≥0 , and one only composed of trees, noted (Tree n ) n≥0 . For all n ≥ 0, we have Tree n ⊆ Graph n , Tree n ⊆ Tree n+1 , and Graph n ⊆ Graph n+1 .

As stated in the introduction, the history of the pushdown hierarchy starts with the result of Muller and Schupp [START_REF] Muller | The theory of ends, pushdown automata, and second-order logic[END_REF] about a geometrical property on configuration graphs of pushdown automata from a given configuration. The graph decomposition of a graph G from a vertex r ∈ V G is the family of the connected components of the subgraphs (G r,n ) n≥0 . The n th decomposition G r,n is the subgraph which support is the set of vertices at distance at least n of r. The graph is said finitely decomposable if, for any vertex r, the graph decomposition is finite up to isomorphism.

Example 2.5.1. If we decompose the complete binary tree from its root, the graph decomposition is reduced to the singleton of the binary tree itself. More generally, if we decompose this tree from a vertex of depth k, the cardinal of the graph decomposition is k + 1.

Theorem 2.5.2 ([MS85]

). Configuration graphs of pushdown automata starting from a given configuration are exactly finitely decomposable graphs of finite degree.

In particular, these graphs have a decidable monadic property. This work was extended to HR-equational graphs by [START_REF] Courcelle | Graph rewriting: An algebraic and logic approach[END_REF], and then to prefix-recognizable graphs [START_REF] Caucal | On the regular structure of prefix rewriting[END_REF][START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF].

In parallel, the notion of tree as infinite solution of a recursion scheme was brought back under the lights thanks to a result of decidability of MSO-theory under a condition of safety [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF][START_REF] Knapik | Higher-order pushdown trees are easy[END_REF]. This approach will be detailed in Chapter 5. A similar result appears in [START_REF] Courcelle | The evaluation of first-order substitution is monadic second-order compatible[END_REF]. Then [START_REF] Caucal | On infinite terms having a decidable monadic theory[END_REF] shows that these term-trees are the same, and that they also are the unfoldings of prefix-recognizable graphs.

This results naturally lead to the full definition of the hierarchy in [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF] : trees are unfolded by graphs, which are in turn inverse rational mappings of trees. It was then showed in [START_REF] Carayol | The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata[END_REF] that the inverse rational mappings can be replaced by general monadic interpretations, and that the graphs of the hierarchy were ε-closures of configurations graphs of higher-order pushdown automata.

Definition

We only define here the outer presentation, i.e. by graph transformations. An inner definition by higher-order stack relations, introduced in [Car05], appears in Section 3.3.2. Chapter 5 presents the recursion schemes approach. The pushdown hierarchy can defined as follows :

• Tree 0 is the set of finite trees,

• for n ≥ 0, Graph n is the set of monadic interpretations of Tree n ,

• for n ≥ 0, Tree n+1 is the set of unfoldings of Graph n .

The lower levels of this two-fold hierarchy are illustrated in Figure 2.5; a practical example of graph constructions can be seen in Figure 2.6.

A major consequence of the Theorem 2.4.4 is that the whole hierarchy enjoys a decidable monadic theory.

Theorem 2.5.3. For all n ≥ 0, the monadic theory of a graph in Graph n is decidable.

Some properties

By [START_REF] Carayol | The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata[END_REF], deterministic trees are enough : a graph of Graph n is the inverse rational mapping of a deterministic tree in Tree n . The same paper also states that there is a generator ∆ n 2 , i.e. a deterministic graph such that each graph is the inverse rational mapping of a rational marking of ∆ n 2 . This generator is defined as follows :

• ∆ 1 2 is the complete binary tree;

# # # # # # b a a b a I 1 U n f I 2 U n f I 3 Figure 2
.6: Exemple of graph constructions in the hierarchy. These graphs belong successively to Tree 0 , Graph 0 , and so on up to Graph 2 . Graphs are always unfolded from their root, i.e. their uppermost leftmost vertex. The three interpretations I 0 , I 1 , I 2 are as follows :

leaf(p) = ¬∃r (p → r) I 0 : ϕ 0 (p, q) = p 0 → q ϕ 1 (p, q) = p = q ∧ ¬leaf(p) I 1 : ψ 0 (p, q) = p 0+ 01 0 ----→ q ψ 1 (p, q) = p 1+ 01 0 ----→ q ψ # (p) = ¬leaf(p) I 2 : η 1 (p, q) = ∃r (p 1 * 0 --→ r 0 * -→ q ∧ leaf(p) ∧ leaf(q) ∧ ¬(#, r)) ∨(leaf(p) ∧ p 1 * 0 --→ q) ∧ (#, q)) ∨(leaf(q) ∧ p 0 * -→ q) ∧ (#, p)) η a (p) = ∃q (η 1 (p, q)) ∧ leaf(p) η b (p) = ∃q (η 1 (p, q)) ∧ (#, p)
The final structure is actually the infinite (morphic) word abaabaaaab . . . , which we will see again in Chapter 5.

• ∆ n+1 2 = Treegraph(∆ n 2 ).
In this thesis, we will extensively use the following closure properties of Tree n and Graph n .

Proposition 2.5.4 ([CW03]). For all n,

• the deterministic trees of Tree n are closed under MSO-coloring;

• Graph n is closed under MSO-transduction.
Deterministic trees of Tree n is also closed by subtree. For any tree t and node u, the subtree of root u is noted t /u . Proposition 2.5.5. For all deterministic tree t ∈ Tree n and for all u ∈ Dom(t), t /u also belongs to Tree n .

Proof. Let t ′ be the tree obtained by coloring any node below u with a fresh color $. By Prop. 2.5.4, t ′ belongs to Tree n . Let G ∈ Graph n and r ∈ V G such that t ≃ Unf(G, r). Let r ′ be the vertex of G corresponding to u and let I be the interpretation erasing all the vertices which are not colored by $ and then removing $. Clearly t /u ≃ Unf(I(G), r ′ ). Hence t /u belongs to Tree n .

Finally, we will make some use of the following selection properties on graphs and trees. These properties are given for completeness sake. Proposition 2.5.6. Let G ∈ Graph n be a deterministic tree, a MSO-formula ϕ(X) and a fresh color $. If G |= ∃X, ϕ(X) then there exists

U ⊆ V G s.t. G |= ϕ[U ] and G ∪ {($, u) | u ∈ U } also belongs to Graph n .
Proof. In [Car06, Theorem 5.3.1] it is shown that for all n ≥ 0, any graph in Graph n can be MSO-interpreted in a unique graph written GStacks n . In [START_REF] Fratani | Automates à piles de piles[END_REF], it is shown that GStacks n has the selection property. That is to say if GStacks n |= ∃X, ϕ(X) then there exists ψ

(x) such that G |= ϕ[U ] where U = {u ∈ V G | G |= ψ[u]}. A proof of this fact is also given in [Car06, Theorem 4.7.6.].
Let G ∈ Graph n and ϕ(X) be an MSO-formula s.t. G |= ∃X, ϕ(X). Let I be an MSO-intrepretation such that G ≡ I(GStacks n ). Let ϕ ′ (X) be an MSO-formula such that for all set U of vertices of GStacks n ,

I(GStacks n ) |= ϕ[U ] iff GStacks n |= ϕ ′ [U ]. In particular GStacks n |= ∃X, ϕ ′ (X).
Let ψ(x) be the formula obtained using the selection property on GStacks n for ϕ ′ (X). Consider the MSO-interpretation I ′ obtained by adding to the formulae defining I a formula ϕ $ (x) = ψ(x). The graph I ′ (GStacks n ) ∈ Graph n satisfies the desidered properties.

Proposition 2.5.7. Let t ∈ Tree n be a deterministic tree, a MSO-formula ϕ(X) and a fresh color $. If t |= ∃X, ϕ(X) then there exists

U ⊆ Dom(t) s.t. t |= ϕ[U ] and t ∪ {($, u) | u ∈ U } also belongs to Tree n .
Proof. Let t be a deterministic tree in Tree n and let ϕ(X) be an MSO-formula s.t. t |= ∃X, ϕ(X).

For all U ⊆ Dom(t), we write t[U ] the deterministic tree colored by {0, 1} with the same set of nodes as t and such that for all u ∈ t, t[U ](u) = 1 iff u ∈ U . We extend this definition to tuples of sets and to graphs. Let A = (Q, q 0 , ∆, Ω) be a parity tree automaton accepting the set of determinstic tree over Σ colored {0, 1} such that:

A accepts t[U ] ⇔ t |= ϕ[U ].
Let B be the automaton obtained by projecting the colors in A (i.e. the set of states of A is Q × {0, 1} where Q is the set of states of A). To obtain our result, it is enougth to show that we can color an accepting run for B on t and still remain in Tree n . Indeed to every accepting run of B correponds a set U ⊆ Dom(t) and an accepting run of A on t[U ].

For technical reason, we are going to color a strategy for the automaton B and not directly an accepting run. A strategy Φ for B on t is a mapping form t to F where F is the finite set of partial functions f from Q to ∆ such that for all q ∈ Q, f (q) (if defined) is a transition starting from q. This strategy Φ is winning if that for all u ∈ Dom(t) s.t. f = Φ(u) and for all q ∈ Dom(f ), the run of B induced by Φ starting from u in state q is accepting. Conversely, for all u ∈ t and all state q of B, if B admits an accepting run from q starting from u on t. As F is a finite set, a strategy for B can be coded by a tuple of sets.

Obviously if we show that t colored with any winning strategy for the automaton B belongs to Tree n . We have also shown that t colored by an accepting run (or colored by a set U such that A |= t[U ]) belongs to Tree n .

The key property we are going to exploit is that we can restrict our attention to so called regular winning strategies. A winning strategy is regular if for all u, v ∈ t, if t /u ≡ t /v then Φ(u) = Φ(v). It follows from the positional determinacy of parity games that any automaton admits a regular winning strategy [Car06, Lemma 1.4.6].

The interest of regular winning strategies becomes apparent when we recall that every tree in t is obtained by unfolding a graph in Graph n . Let G be a graph in Graph n and let r be a vertex in V G such that t ≡ Unf(G, r). By considering regular strategies, we can assume that all points originating from the same vertex of G in the unfolding are assigned the same value by the strategy. This allows us to color t with a regular winning strategy "before unfolding". It follows form [Car06, Proposition 1.4.9] that there exists a formula ψ( X) such that for any tuple Ū of vertices of G, G |= ψ[U ] iff Unf(G[U ], r) correspond to t colored with a winning strategy. By Prop. 2.5.6, there exists Ū such that G |= ψ[ Ū ] and G[ Ū ] belongs to Graph n .

Chapter 3

Linear order construction

This chapter locates some particular scattered orders in the pushdown hierarchy. It begins with the construction of ordinals by graph transformations : the towers of ω of height n are found in Graph n . The same method is then extended to powers of ζ. For ordinals, we also give a higher-order n-regular presentation, i.e. relations on stacks of stacks. In Chapter 5, we will see a third construction of ordinals by schemes. Therefore these well-known structures offer a panorama of techniques that can be used in the hierarchy.

While using MSO logics on ordinals, an important result can be noticed. Büchi's Theorem 3.4.2 states that ordinals larger than ω ω have a "redundant" MSO theory; for instance, MTh(ω ω ) = MTh(ω ω ω ). In other words, a given ordinal cannot be recognized by a MSO formula. The last section of this chapter studies the structure of the so-called canonical fundamental sequences of an ordinal, which is very close to the structure of the ordinal itself, but has the MSO-recognizability. These structures also belong to the hierarchy for ordinals smaller than ε 0 .

Ordinals in the pushdown hierarchy

Finite ordinals are all in Graph 0 , which is the set of finite graphs. On the next level, ordinals smaller than ω ω are also easy to locate in the first level of the hierarchy. This has been proven by [START_REF] Heilbrunner | An algorithm for the solution of fixed-point equations for infinite words[END_REF][START_REF] Bloom | Long words: the theory of concatenation and omega-power[END_REF]. We restate this result.

Proposition 3.1.1. For any α < ω ω , α ∈ Graph 1 .
Proof. Let G k be the finite graph of vertices {a i | 0 ≤ i ≤ k}, as shown in Figure 3.1.

G k = {a i 1 → a i , a i 0 → a i-1 | 0 < i ≤ k}
The leaves of unfolding of G k by a k are of the form 1 c k-1 01 c k-2 . . . 01 c 0 0. Ordered by lexicographic ordering, this set is isomorphic to (ω k-1 .c k-1 +• • •+c 0 ) ∀i<k,c i ≥0 , which is ω k . We have seen in Example 2.4.1 that the frontier of a deterministic tree is a MSO-interpretation of this tree, so ω k ∈ Graph 1 . For details on the sum closure, see Lemma 3.1.3. The natural question is whether greater ordinals belong to the hierarchy, and up to which bound. In particular, [START_REF] Cachat | Tree automata make ordinal theory easy[END_REF] asks whether ω ω ∈ Graph 2 or not. This section partially answers this question by giving examples of ordinals; the other direction will be seen in Chapter 4.

Theorem 3.1.2. If α < ω ↑↑ (n + 1), then α ∈ Graph n .
Using the Cantor normal form of ordinals smaller than ε 0 , we only have to implement addition and the operation α → ω α . Here, we prove that ordinals of Graph n are closed by addition, and that the ω-exponentiation only reaches the next level.

Lemma 3.1.3. If α, β ∈ Graph n , then α + β ∈ Graph n . Proof. It suffice to prove that for any G 1 , G 2 ∈ Graph n , x 1 ∈ V G 1 , x 2 ∈ V G 2 , if x is a new vertex and # 1 , # 2 new letters, the graph G = G 1 ∪ G 2 ∪ {x # 1 → x 1 , x # 2 → x 2 } is also in Graph n . Indeed, if G 1 = α and G 2 = β,
we can supply a monadic interpretation to get the sum. This is true for finite graphs. For n > 0, if

G 1 = I 1 (U nf (H 1 , r 1 )) and G 2 = I 2 (U nf (H 2 , r 2 )),

then by induction we define H as above is in Graph

n-1 : H = H 1 ∪ H 2 ∪ {r # 1 → r 1 , r # 2 → r 2 }. Then U nf (H, r) ∈ Tree n .
It is easy to mark sets isomorphic to V G 1 and V G 2 and to restrict respectively I 1 and I 2 to these sets. We get the required G.

Lemma 3.1.4. If α ∈ Graph n then ω α ∈ Graph n+1 .
Proof. By Corollary 2.2.2, the structure ω α is isomorphic to the finite decreasing sequences of ordinals smaller than α. Let G = Treegraph(α). We are going to find an interpretation I such that I(G) ≃ ω α . For an illustration, the Figure 3.7 page 62 shows the case of ω in the simpler frame of covering graphs, which will be defined in Section 3.4.

G has exactly one root 0. Let M be the formula

M (x) := x = 0 ∨ 0 <#( <#) * -----→ x.
By the definition of treegraph, for any x such that M (x) and x = 0, we have

0 <# --→ γ 1 γ 1 <# --→ γ 1 γ 2 γ 2 <# --→ . . . <# --→ γ 1 . . . γ n γ n = x.
We note s x the sequence (γ 1 , . . . ,

γ n-1 , γ n ) with α > γ 1 ≥ • • • ≥ γ n .
Conversely, each such sequence is associated to a x such that M (x). We define now a monadic interpretation I = {ϕ < } on these marked vertices so that ϕ < (x, y) iff s x < lex s y . Define

+ η). ϕ < (x, y) := M (x) ∧ M (y) ∧ x = 0 ∨ x ( #<) * (# <) + -------→ y.
The case x = 0 is easy, so we suppose that x = 0 and ϕ < (x, y). Then there is a z such that x

( #<) * ---→ z (# <) * ---→ y.
Then there is k such that s x = (γ 1 , . . . , γ k , . . . , γ n ) and

s z = (γ 1 , . . . , γ k-1 , γ ′ k ) with γ k < γ ′ k .
In the same way s y = (γ 1 , . . . , γ k-1 , γ ′ k , . . . , γ ′ n ′ ), so s x < lex s y . The converse is also true.

As a direct consequence of Theorem 3.1.2, ordinals below ε 0 can be expressed by higher-order pushdown automata. This approach is explained in Section 3.3. In fact, this result is useful to illustrate the techniques that may be used in the hierarchy. It is therefore proved four times :

• directly by the above proof;

• by n-regular relations, in Section 3.3;

• by covering graphs, as an application of Propositions 3.4.4 and 3.4.13;

• by higher-order schemes, as an application of Example 5.1.2.

Powers of ζ

More complex orders can also be found in the pushdown hierarchy. In particular, trees of frontier ζ or η (resp. order types of Z and Q), showed in Figure 3.2, are in Graph 1 .

In this chapter, we focus on a particular family of scattered orders : namely, the successive ordinal powers of ζ. They are defined as follows.

ζ 0 = 1 ζ β+1 = ζ β • ω * + ζ β + ζ β • ω ζ λ = α<λ ζ α .ω * + 1 + α<λ ζ α .ω for λ limit.
Note that the last line alone is actually enough for a complete definition, for any ordinal λ. From [Ros82, Thm. 5.37], the Hausdorff-rank of ζ α is α. Furthermore, ζ α is complete among the scattered orders of Hausdorff-rank α in the following sense: a scattered order has Hausdorff-rank less than α if and only if it is a subordering of ζ α .

The following proposition is an extension of Theorem 3.1.2.

Proposition 3.2.1. For all n > 0 and any ordinal α < ω ↑↑ n, ζ α is in Graph n .

For instance, the graph of Figure 3.3 is regular and thus in Graph 1 . Its unfolding by its root (the leftmost vertex) is in Graph 2 and yields the order ζ ω .

To prove the result, we need to extend the definition of the treegraph operation to go in more than one direction. A similar approach can also be found in [START_REF] Pillot | Produits de graphes infinis et logique monadique[END_REF].

Definition. Let Σ, Γ be two alphabets. The Γ-treegraph of a Σ-graph G is the graph in (V G ∪ Γ) * × Σ ∪ Γ × (V G ∪ Γ) * given by G = {ux b → uy | x b → y ∈ G} ∪{ux a → uxax | a ∈ Γ}
Note that the constraint Σ ∩ Γ = ∅ is not required, but this will be the case in our application, and it is easy to see that it is not a restriction.

The main property of this treegraph version is that it does not add more complexity than the standard treegraph, which is isomorphic to the case Γ = {#}.

Proposition 3.2.2. The Γ-treegraph of a graph in Graph n is in Graph n+1 .
Proof. Suppose Σ ∩ Γ = ∅ up to final renaming. Let G ∈ Graph n . For each a ∈ Γ, let T be the transduction adding an arc labeled by a from each vertex of G. Then the Γ-treegraph of G is isomorphic to the interpretation of Treegraph(T (α)) where each path labeled a#ā is changed into a.

Proof of Prop. 3.2.1. This proof is an adaptation of the construction for ordinals. By Theorem 3.1.2, for any n > 0, any ordinal smaller than

ω ↑↑ n is in Graph n-1 . So it is enough to prove that if α ∈ Graph n-1 , then Z α is in Graph n .
In a way similar to Proposition 2.2.1, ζ α is isomorphic to the set of α-sequences over Z where a finite number is non-zero, and ordered by reverse lexicographic order -see again [START_REF] Rosenstein | Linear orderings[END_REF]5.36]. For two α-sequences s, t, we have s < rlex t iff ∃γ such that s γ < t γ and ∀δ > γ, s δ = t δ .

Let α ∈ Graph n-1 such that α < ω ↑↑ n. Let G be the {0, 1}-treegraph of α; by Proposition 3.2.2, G ∈ Graph n+1 . G has still exactly one root r (a vertex co-accessible from V G ). Let M be a marking adding a special color on r and any x such that r

(<+ε)(0 + +1 + )( <(0 + +1 + )) * ----------------→ G x.
Here x = r is of the form (γ 0 a 0 ) c 1 . . . . .(γ k a k ) c k where for all i ≥ 0, c i > 0, a i ∈ {0, 1} and γ i < γ i-1 . To each such x we associate the α-sequence s(x) where

s(x) γ i = -c i if a i = 0 s(x) γ i = c i if a i = 1 s(x) γ = 0 if γ = γ i for any i
The path is finite so a finite number of indexes are non-zero. Conversely, to each αsequence with a finite number of non-zero indexes is associated a unique vertex in V G .

We check that the relation x < y on marked vertices holds iff s(x) < rlex s(y) where < rlex is the reverse-lexicographic order definable by a MSO-interpretation in G. The cases x = 0 and y = 0 are handled separately. Otherwise let

x = (γ 0 a 0 ) c 0 . . . . .(γ k a k ) c k γ k y = (δ 0 b 0 ) d 0 . . . . .(δ h b j ) d h δ h .
We have x < y iff there is a j such that a i = b i , γ i = δ i , c i = d i for all i < j, and one of the following is true. We note ↑= (( 0 + 1) * <) and ↓= ( <(0 + 1) * ). For an example, see Figure 3

.4. Either γ j < δ j , b j = 1 =⇒ x ↑ + 1 + ↓ * ----→ y or δ j < γ j , a j = 0 =⇒ x ↑ * 0+ ↓ + ----→ y or γ j = δ j , j > 0 and a j = b j = 0, c j > d j =⇒ x ↑ * 0+ ↓ * ----→ y or a j = b j = 1, d j > c j =⇒ x ↑ * 1 + ↓ * ----→ y or a j = 0, b j = 1 =⇒ x ↑ * 0+ 1 + ↓ * -----→ y or k < j ≤ h, b j = 1 =⇒ x <1 + ↓ * ----→ y or h < j ≤ k, c j = 0 =⇒ x ↑ * 0+ > ----→ y. (. . . )
. . . White vertices are those used by the interpretation; bracketed dots represent subgraphs where no vertex will be used. Here s x = (-1, -1, 0, . . . ), s y = (0, -1, 0, . . . ), s z = (0, 1, 0, . . . ). We check for instance that

x 0< 01 ---→ z, noted x ↑ 01 --→ z.
In the other direction,

x ↑ * 1 + ↓ * ----→ y =⇒ γ j < δ j , b j = 1 or γ j = δ j , a j = b j = 1, d j > c j x ↑ * 0+ ↓ * ----→ y =⇒ δ j < γ j , a j = 0 or γ j = δ j , a j = b j = 0, c j > d j x ↑ * 0+ 1 + ↓ * -----→ y =⇒ γ j = δ j , a j = 0, b j = 1 x <1 + ↓ * ----→ y =⇒ k < j ≤ h, b j = 1 x ↑ * 0+ < ----→ y =⇒ h < j ≤ k, c j = 0.
There is therefore a monadic interpretation

I such that I(G) ≃ ζ α . Since Graph n is closed under MSO-interpretation, ζ α ∈ Graph n .

n-regular presentation

The graphs on the first level of the hierarchy were originally defined with a prefix-recognizable presentation [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF]. Then this presentation was extended to any level with the help of higher-order pushdown automata of level n [CW03], i.e. automata which use nested stacks of stacks of depth n. Using these results, the construction by monadic interpretations and unfolding can be translated into a pushdown automata description.

Instead of doing so, we prefer the equivalent -and more fluent -notion of regularity [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF] on n-stacks. This notion offers a natural encoding of ordinals by their Cantor normal form. This section gives a presentation of prefix-recognizable graphs, and then of the more general n-regular relations. We show then how to actually build ordinals with this latter tool. As in Section 3.1, this latter operation is split in two parts : one for the α → ω α operation and the other for addition.

Prefix-recognizable graphs

A prefix-recognizable Σ-graph is up to isomorphism a graph of the form

{uw a → vw | (U, a, V, W ) ∈ ∆, u ∈ U, u ′ ∈ V w ∈ W, a ∈ Σ}
where ∆ is a finite set of tuples (U, a, V, W ) such that U, V and W are regular languages.

Theorem 3.3.1 ([Cau96, Theorem 3.3]). Prefix-recognizable graphs are up to isomorphism inverse rational mappings of the complete binary tree. This means that Graph 1 is (up to isomorphism) the set of prefix-recognizable graphs. As a result, the same paper states that the monadic theory of prefix-recognizable graphs is decidable.

Configuration graphs of n-hopdas

For a detailed presentation of these notions, see [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF]. A 1-stack, or simply stack, over a finite alphabet Γ is a word over Γ. To avoid later confusion, we forbid letters of N (see below for the difference between pop x and pop n ). The empty 1-stack is noted [ ] 1 . For all n > 1, a n-stack over Γ is a non-empty finite sequence of (n -1)-stacks over Γ. The empty n-stack containing only the empty (n -1)-stack is noted [ ] n . For all n, the set of n-stacks is noted Stacks n (or Stacks n (Γ)) and the set of all stacks is Stacks = ∪ n∈N Stacks n .

The operations on a 1-stack [a 1 , . . . , a m ] 1 are the usual push and pop. We add pop 1 which can pop any letter.

push x ([a 1 , . . . , a m ] 1 ) := [a 1 , . . . , a m , x] 1 , pop x ([a 1 , . . . , a m = x] 1 ) := [a 1 , . . . , a m-1 ] 1 . pop 1 ([a 1 , . . . , a m ] 1 ) := [a 1 , . . . , a m-1 ] 1 .
For n > 1 and a n-stack [s 1 , . . . , s m ] 1 , the extended operations are as follows. The operation copy n replicates the top-most (n -1)-stack, and copy n is its symetric : it deletes the top-most (n-1)-stack if it equals the penultimate. The pop n operation simply removes the top-most (n -1)-stack. For k < n, the operation on k-stacks are simply propagated in the top-most stack.

copy n ([s 1 , . . . , s m ] n ) := [s 1 , . . . , s m , s m ] n copy n ([s 1 , . . . , s m , s m ] n ) := [s 1 , . . . , s m ] n pop n ([s 1 , . . . , s m ] n ) := [s 1 , . . . , s m-1 ] n copy k ([s 1 , . . . , s m ] n ) := [s 1 , . . . , copy k (s m )] n for 1 < k < n pop k ([s 1 , . . . , s m ] n ) := [s 1 , . . . , pop k (s m )] n for 1 ≤ k < n pop x ([s 1 , . . . , s m ] n ) := [s 1 , . . . , pop x (s m )] n for x ∈ Γ push x ([s 1 , . . . , s m ] n ) := [s 1 , . . . , push x (s m )] n
Let also be an identity function id defined on Stack. The set of operations defined at least one n-stack is denoted Ops n . Instead of dealing with rough higher-order pushdown automata, one can use directly a regularity on stacks. The set of operations forms a monoid with the composition operation. Let Reg(Ops n ) the closure of the finite subsets of this monoid under union, product and iteration, i.e. the set of regular expressions on Ops n .

To each expression E ∈ Reg(Ops n ) we associate the test operation

test E = id |E([ ]n) . By an abuse of language test [ ] k = id |[ ] k . Let T est n be the set of tests. To each F ∈ Reg(Ops n ∪ T est n ) we now associate the set of stacks S n (F ) = F ([ ] n ), the set of relations R(F ) = {(s, s ′ )|s ′ ∈ F (s)}.
The set of stacks S n (F ) will be noted S(F ) if n is clear. Given F and (F a ) a∈Σ in Reg(Ops n ∪ T est n ), the graph of support S(F ) and with arcs s a → s ′ iff (s, s ′ ) ∈ R(F a ) is a configuration graph of a n-hopda. They describe precisely the graphs of the hierarchy. [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF]). The family of configuration graphs of n-hopdas is equal up to isomorphism to Graph n .

Theorem 3.3.2 ([

Encoding ordinals

For each ordinal, we are going to define the expressions dom and inc which respectively fix the domain of the structure and the order relation. We also will build an expression dec to perform the symmetric of inc. In other words, we want the structure S(dom(α)), R(dec(α)), R(inc(α)) to be isomorphic to the structure α, >, < .

Small ordinals

For ω, we consider the set of all 1-stacks (i.e. integers). In this case, dom(ω) is obtained by iterating push a on the empty stack with a fixed letter a. The other operations are also Since we only consider ordinals in Graph n for n > 1, our interest is focused on infinite ordinals. However, since we are going to encode these ordinals through the Cantor normal form, we have to define finite ordinals. For a finite ordinal k > 0, the domain is simply the restriction of dom(ω) to 1-stacks of size bounded by k -1.

To allow iteration and re-prove Theorem 3.1.2, we also need more than ω : we have to encode all ordinals smaller than ω ω with 1-stacks. This is done with more letters. Let

α = ω k 1 .c 1 + • • • + ω.c k-1 + c k . The stack alphabet is {a 1 , . . . , a k }. Stacks belong to a subset of S(push * a 1 . . . push * a k ) where if s = [a d k k . . . a d 1 1 ] 1 , then the sequence (d i ) i∈[0,k] is smaller than (k i ) i∈[0,k]
in lexicographic order. Relations also respect this order. Increasing a stack is done by popping all letters a i where i > j for a given j, then pushing one a j and pushing anything. Decreasing a stack is done by popping all letters a i where i ≥ j for a given j, then pushing only letters a i with i > j.

One step further : exponentiation

Let α be any ordinal smaller than ε 0 , and let n be the smallest value such that dom(α), inc(α) and dec(α) are all in Reg(Ops n-1 ). Informally, each ordinal γ < ω α is either 0 or may be written as γ = ω γ 0 + • • • + ω γ k with γ i < α; so we code γ as a sequence of stacks respectively coding γ 0 . . . γ k .

Let tail(α) := copy n .(id + dec(α)). This operation takes the last stack (representing γ k ) and adds a stack coding an ordinal ≤ γ k , so that the CNF constraint is respected. For the relation <, inc either adds a decreasing sequence (by tail), or it first pops stacks, then increases a given one before adding a tail. Reg(Ops k ) and s, s ′ are two k-stacks such that (s, s ′ ) ∈ R(f ) , and if p, p ′ are the same n-stack except for the top-most k-stack which is respectively s and s ′ , then (p, p ′ ) ∈ R(f ).

Let S = dom(ω α ) and let p ∈ S be a finite sequence of (n -1)-stacks, so p = [s γ 0 , . . . , s γ k ]. In the definition of dom(ω α ), there is no pop n operation, and by definition s γ 0 , . . . , s γ k are all in S(dom(α)). By hypothesis on dec(α), we also have

s γ 0 ≥ • • • ≥ s γ k . As a consequence, the mapping p = [s γ 0 , . . . , s γ k ] → λ = ω γ 0 + • • • + ω γ k
is well defined and is injective. In fact, it is a bijection between S and [1, ω α [; omitting 0 is not a problem for infinite ordinals. We therefore note p λ the n-stack associated to λ. Now let 0 < λ < λ ′ < α be two ordinals, with

λ = ω γ 0 + • • • + ω γ k in CNF. Then either λ ′ = ω γ 0 + • • • + ω γ k + • • • + ω γ k ′ with k < k ′ , or λ ′ = ω γ 0 + • • • + ω γ i + • • • + ω γ ′ i+1 + • • • + ω γ k ′ for some i < k, with γ i+1 < γ ′ i+1 .
For the first case, the use of tail(α) on p λ has already been discussed, so (p λ , p λ ′ ) ∈ R(tail(α) + ). In the second case, pop

(k-i-1) n (p λ ) = [s γ 0 , . . . , s γ i+1 ] and, by induction, ([s γ 0 , . . . , s γ i+1 ], [s γ 0 , . . . , s γ ′ i+1 ]) ∈ R(inc(α)). Again, the tail operation is used. The converse -if (p λ , p λ ′ ) ∈ S 2 ∩ R(inc(ω α )) then λ < λ ′ -is straightforward. So S, R(inc(ω α )) is indeed isomorphic to α, < .
The dec operation is similar. In the first case, pop

(k ′ -k) n (p λ ′ ) = p λ with k ′ -k ≥ 1. In the second case, pop (k ′ -i-1) n (p ′ λ ) = [s γ 0 , . . . , s γ ′ i+1 ] and ([s γ 0 , . . . , s γ ′ i+1 ], [s γ 0 , . . . , s γ i+1 ]) ∈ R(dec(α)).
The converse is direct as well, and proves in the same time the last needed induction property : dec(ω α )(S) ⊆ S. Note that this was not true with inc : inc(ω α )(S) ⊆ S, because we could lose the decreasing constraint of the CNF. Finally S, R(inc(ω α ), R(dec(ω α )) is isomorphic to α, <, > and the induction prop-erties are fulfilled.

Completing with addition

To perform exponentation, dom(ω α ) only uses the letters used by dom(α). For addition, we add some markers. Let α 1 , α 2 < ε 0 and let n be the smallest integer such that dom(α 1 ), dom(α 2 ) ∈ Ops * n . We add new letters α 1 , α 2 . We note test ᾱi for test (Opsn\{push α i }) * , meaning in this context "there is no α i in any stack".

dom(α 1 + α 2 ) = push α 1 dom(α 1 ) + push α 2 dom(α 2 ) inc(α 1 + α 2 ) = test ᾱ2 (inc(α 1 ) + dec(α 1 )pop α 1 test ᾱ1 push α 2 dom(α 2 )) +test ᾱ1 inc(α 2 ) dec(α 1 + α 2 ) = test ᾱ1 (dec(α 2 ) + dec(α 2 )pop α 2 test ᾱ2 push α 1 dom(α 1 )) +test ᾱ2 dec(α 1 ) Proposition 3.3.4. If n > 0 and S(dom(α i )), R(dec(α i )), R(inc(α i )) ≃ α i , >, < for i ∈ {1, 2}
, then the same is true for α 1 + α 2 .

Proof. The α 1 and α 2 parts are respectively encoded by the new marker of the same name at the beginning of each stack. The only way to remove a first letter α 1 is to use pop 1 or pop α 1 , both of which are never used by inc(α 1 ) or dec(α 1 ). So the relations inc and dec cannot accidentally remove this marker; the set dom(α 1 ) is closed by inc(α 1 ) and dec(α 1 ).

To increase a stack, either this stack begins with α 1 or α 2 : this is checked by the operation test push α i Ops * n . In the case of α 2 , using inc(α 2 ) is enough. For stacks in the α 1 part, greater stacks are accessible by the inc(α 1 ) operations and by taking all stacks in the α 2 part. To reach the latter, it is enough to pop everything including the α 1 marker, and start with push α 2 dom(α 2 ). The dec operation works the same way.

Main result

To sum up, we have defined small ordinals in terms of configuration graphs of (standard) pushdown automata. Then we showed how to perform exponentiation by increasing the order, and addition at the same order. We get therefore the main result of this section.

Theorem 3.3.5. For any α < ω ↑↑ n + 1, α is isomorphic to the configuration graph of a n-hopda.

By the equivalence of Theorem 3.3.2, this result is therefore a new proof of Theorem 3.1.2.

Covering graphs

We have seen in Example 2.3.2 that it is possible to recognize the structure of an ordering with the help of FO-logic, and well-ordering with MSO-logic in Example 2.3.3. But is there a formula ϕ α defining precisely the ordinal α, i.e. such that only the ordinal α satisfies ϕ α ? For ordinals smaller than ω ω , it is a simple exercise.

Proposition 3.4.1. For α < ω ω , there is a MSO-formula ϕ α such for any {<}-graph G, G |= ϕ α if and only if G ≃ α.

Proof. The conjunction of formulae of Examples 2.3.2 and 2.3.3 checks the well-ordering of the structure. We define the formulae ϕ k recognizing the k-limit vertices, i.e. limits of (k -1)-limit vertices.

ϕ 0 (x) := ⊤, ϕ k (x) := ∀y < x, ϕ k-1 (y) ⇒ ∃z (ϕ k-1 (z) ∧ y < z < x).
To recognize the ordinal ω k .c k + • • • + ω.c 1 + c 0 , it is enough to find exactly c k vertices satisfying ϕ k , then c k-1 vertices greater than the previous ones and satisfying ϕ k-1 , and so on. This method is not powerful enough for higher ordinals, and in the general case the property was proven false in [START_REF] Büchi | Decision methods in the theory of ordinals[END_REF][START_REF] Büchi | The monadic theory of all countable ordinals[END_REF]. To present this result we need an additional definition. Any ordinal α has a unique representation

α = ω ω .ν + ω k .c k + • • • + ω 1 .c 1 + c 0
The ordinal ω ω .ν is called the ω-head of α, and ω k .c k + • • • + ω 1 .c 1 + c 0 is its ω-tail . The monadic theory of α only depends on the latter and whether or not α < ω ω . Theorem 3.4.2 ([Büc73, Th. 4.9]). For any countable ordinals α and β, the following statements are equivalent :

• MTh(α) = MTh(β)
• either α = β < ω ω or else ω ω ≤ α, β and α, β have the same ω-tail.

This result means informally that ordinals are not easily manipulable by MSO formulae; for instance, in general it is not possible to get a ordinal from a greater one by a monadic interpretation. In this section, we by-pass this problem by considering a structure based on the well-known notion of fundamental sequence. This structure is called the covering graph of an ordinal. One of its important properties is its finite out-degree, which is worked out to bring a specific monadic formula for each covering graph, thus allowing to differentiate them.

Fundamental sequence

For any ordinal α, a subset S ⊆ α is cofinal in α if for any β ∈ α, there is β ′ ∈ S such that β ≤ β ′ . Such S has an ordinal order type. The cofinality of α is the minimal order type of a subset cofinal in α. The cofinality [START_REF] Rosenstein | Linear orderings[END_REF] of any countable ordinal is ω. This means that to each limit ordinal α we may associate an ω-sequence whose supremum is α.

Definition. For α ≤ ε 0 , α = β + ω γ with β < α, γ < α and ω γ is the last term in the CNF of α, the (canonical) fundamental sequence (α[n]) n<ω is defined as follows :

α[n] = β + ω γ ′ .(n + 1) if γ = γ ′ + 1 β + ω γ[n]
otherwise.

We note1 α ′ ⋖ α whenever there is

k such that α ′ = α[k], or if α ′ + 1 = α.
The adjective "canonical" will be implicit for the rest of this section.

Example 3.4.3. The fundamental sequence of ω is the sequence of strictly positive integers. The sequence of ω ω is therefore (ω, ω 2 , ω 3 , . . . ), whereas the sequence of ω 2 is (ω, ω.2, ω.3, . . . ). Here is an example of successively related ordinals.

0 ⋖ 1 ⋖ ω ⋖ ω + 1 ⋖ ω.2 ⋖ ω 2 ⋖ ω ω . . .
Taking the transitive closure of this relation gives back the original order, so there is no information loss. Proposition 3.4.4. The transitive closure of ⋖ is <.

Proof. Let 0 ≤ λ 1 ≤ λ 2 be two ordinals. We prove that λ 1 ⋖ k λ 2 for some finite k by induction on λ 2 . If λ 2 is a successor, consider λ ′ 2 such that λ ′ 2 + 1 = λ 2 , so λ ′ 2 ⋖ λ 2 and λ 1 ≤ λ ′ 2 . Otherwise, since the fundamental sequence of λ 2 bounds all smaller ordinals, there is a smallest n such that

λ 1 ≤ λ 2 [n] ⋖ λ 2 , so let λ ′ 2 = λ 2 [n]. In both cases, by induction λ 1 ⋖ k ′ λ ′ 2 and thus λ 1 ⋖ k ′ +1 λ 2 .
Moreover, the relation is crossing-free as described below, which is a helpful technical tool.

Proposition 3.4.5. If α 1 < λ 1 < α 2 , α 1 ⋖ α 2 and λ 1 ⋖ λ 2 , then λ 2 ≤ α 2 .
To put it more simply, this is the forbidden case :

α 2 λ 2 α 1 λ 1
Proof. We proceed by induction on

α 1 = β + ω γ , γ < α 1 . Note that α 1 + 1 < α 2 .
According to the definition of ⋖, α 1 is in the fundamental sequence of α 2 , which leaves two distinct cases. We suppose λ 1 + 1 < λ 2 , otherwise the lemma is trivially true. Recall that β denotes the RCNF of β. In the first case, α 2 = β + ω γ+1 . Then, in RCNF, λ 1 = β + ω γ .c 1 + δ1 , c 1 > 0 and δ 1 < ω γ . Now if δ 1 = 0, then c 1 > 1 and λ 2 = β + ω γ+1 = α 2 . If δ 1 = 0, note that the only part that changes between an ordinal and a member of its fundamental sequence is the last term in RCNF. So λ 2 is written β + ω γ .c 2 + δ2 in RCNF with δ 2 < ω γ , and therefore λ 2 < α 2 .

In the second case,

α 2 = β + ω γ ′ with γ ⋖ γ ′ , γ + 1 < γ ′ . In RCNF, λ 1 = β + ω µ 1 .c 1 + δ1 with c 1 > 0, δ 1 < ω µ 1 , γ ≤ µ 1 < γ ′
and at least one of the following is true : δ 1 = 0, or γ < µ 1 , or c 1 > 1. Again, we have to deal with several cases.

Either δ 1 = 0 and γ = µ 1 ; then c 1 > 0 and λ 2 = β + ω γ+1 < α 2 .

Or δ 1 = 0 and γ < µ 1 ; then λ 2 = β + ω µ 2 and µ 1 ⋖ µ 2 ; this is where the induction property is applied to get µ 2 ≤ γ ′ , and λ 2 ≤ α 2 .

Finally, if δ 1 = 0, as before

λ 2 = β + ω µ 1 .c 2 + δ2 < β + ω γ+1 < α 2 .

Covering graphs

Definition. For instance, a representation of G ω ω is given in Figure 3.6. We first remark the finite out-degree of the covering graphs.

Let G α = {λ 1 ⋖ λ 2 | λ 1 , λ 2 <
Proposition 3.4.6. For any ω ↑↑ (n -1) < α ≤ ω ↑↑ n and n > 0, the out-degree of G α is n.

Proof. The output degree of λ < α in G α is the cardinal of {µ | λ ⋖ µ < ω ↑↑ n}. If n = 0, λ = 0 and ω ↑↑ 0 = 1, so the set is empty. For n > 0, let λ = β + ω γ and λ ⋖ µ, then either

µ = λ + 1 or µ = β + ω γ ′ with γ ⋖ γ ′ . Since γ ′ < ω ↑↑ (n -1), by induction |{γ ′ | γ ⋖ γ ′ < ω ↑↑ (n -1)}| ≤ n -1, which leads to |{µ | λ ⋖ µ < ω ↑↑ n}| ≤ n.
For the lower bound, if n = 1, then α ∈ [2, ω], and 0 ⋖ 1 has degree 1.

For n > 1, if α > ω ↑↑ (n -1) then ω ↑↑ (n -2) ⋖ ω ↑↑ (n -2) + 1 ⋖ ω ω↑↑(n-3)+1 . . . ⋖ ω ... ω+1 ⋖ ω ... ω 2 ⋖ ω ↑↑ (n -1).
For instance, let n = 3, α = ω ω + 1 :

ω ⋖ ω + 1 ⋖ ω 2 ⋖ ω ω .
So ω ↑↑ (n -2) has degree n in G α .

In the following, we refine this property to get a characterisation of an ordinal covering by the degree of its vertices. We define the degree word d(α) of a covering graph as follows.

Definition. Consider the greatest sequence σ of G α starting from 0, i.e. σ 0 = 0 and for k ≥ 0, σ k+1 is the greatest ordinal smaller that α such that σ k ⋖ σ k+1 if any. The previous lemma ensures that {λ | σ k ⋖ λ} is finite, so σ k+1 exists. Such a sequence may be finite.

The degree word d(α) is a finite or infinite word over [0, n] when α ≤ ω ↑↑ n, and its k th letter is the out-degree of σ k in G α . Note that d(0) = ε and d(1) = 0.

Example 3.4.7. Consider d(ω ω ). Its greatest sequence is (0, 1, ω, ω 2 , ω 3 , . . . ), where all have degree 2 in G ω ω except the first; so d(ω ω ) = 12 ω . Now consider d(ω 3 + ω 2 ) : the sequence is now 0, 1, ω, ω 2 , ω 3 , ω 3 + 1, ω 3 + ω, ω 3 + ω + 1, . . .

which loops into (. . . , ω 3 + ω.k, ω 3 + ω.k + 1, . . . ) so d(ω 3 + ω 2 ) = 12221(21) ω .
These examples hint that the degree word is regular.

Lemma 3.4.8. For any α ≤ ω ↑↑ n, if α is a successor ordinal then d(α) is a finite word of [0, n] * ; otherwise d(α) is an ultimately periodic word of [1, n] ω .
Proof. Lemma 3.4.6 ensures that the degree word of α ≤ ω ↑↑ n is a word on the alphabet [1, n]. Since the transitive closure of G α is isomorphic to α, the greatest sequence σ of G α is unbounded, i.e. ∀λ < α, ∃n(σ n ≥ λ). In particular, if α = λ + 1, there is n such that σ n = λ, and the sequence is finite. The last element has out-degree 0. If α is a limit ordinal, each α[n] must be in σ. Indeed, let m be such that σ m ≤ α[n] ≤ σ m+1 ; if the inequalities are strict, since α[n] ⋖ α, by Proposition 3.4.5 we have σ m+1 ≥ α which is a contradiction. So one of σ m or σ m+1 must be α[n].

We want now to prove that the pattern between the (α[n]) n<ω is always the same. Let α = β + ω γ . As before, we have two cases. If γ = γ ′ + 1, then α[n] = β + ω γ ′ .(n + 1). Given n, there is a path in the greatest sequence

α[n] ⋖ α[n] + δ 1 ⋖ • • • ⋖ α[n] + δ h ⋖ α[n + 1]
with δ i < ω γ for each i, and in fact δ i+1 is the greatest such that δ i ⋖ δ i+1 and δ i+1 ≤ ω γ . This defines the (δ i ) sequence independently of n. If i is fixed and n varies, α[n] + δ i ⋖ α[n] + x whenever δ i < x and x ≤ ω γ , so the degree is still the same. The degree word is therefore ultimately periodic.

In the second case,

α[n] = β + ω γ[n] and γ[n] + 1 ≤ γ[n + 1] < γ. So β + ω γ[n]+1 < α. Since α[n] ⋖ β + ω γ[n]+1
, then the following element of α[n] in the greatest sequence is greater or equal to β + ω γ[n]+1 and is therefore of the form

β + ω δ 1 with γ[n] ⋖ δ 1 . In general α[n] = β + ω γ[n] ⋖ β + ω δ 1 ⋖ • • • ⋖ β + ω δ h ⋖ α[n + 1]
are in the greatest sequence. Then γ[n], δ 1 , . . . , γ[n + 1] are in the greatest sequence of γ and their output degrees are respectively the same than those of ω γ[n] , ω δ 1 , . . . , ω γ[n+1] in α, minus 1. By induction, if the sequence of γ is ultimately periodic, so is the sequence of α.

The degree word is actually a morphism from ordinals to words over the alphabet [0, n] by lexicographic order. Lemma 3.4.9. If α < α ′ ≤ ω ↑↑ n, then d(α) < lex d(α ′ ).

Proof. For any β > 1, d(0) < d(1) < d(β). Suppose therefore n > 0. As before, note that the greatest sequence is unbounded, and that σ 0 = σ ′ 0 = 0. Thus if 0 < α < α ′ and σ ′ is the greatest sequence of G α ′ , there is a smallest n > 0 such that σ n = σ ′ n , or σ n doesn't exist whereas σ ′ n does. In both cases, the output degree of σ n-1 is less in G α than in G α ′ , so d(α) < lex d(α ′ ).

A ultimately periodic pattern can be captured by a monadic formula. This is the goal of the the following lemma.

Lemma 3.4.10. For each finite or infinite word w over [0, n] and a given ordinal α, there is a monadic formula ϕ w such that G α |= ϕ w iff w = d(α).

Proof. The fact that the degree word is finite or ultimately periodic permits to use a finite number of variables. We consider the ultimately periodic case, and d(α) = uv ω .

To simplify the writing, we consider the following shortcuts :

• τ (p, q) if q is the greatest such that p ⋖ q;

• ∂ k (p) if the output degree of p is k;

• root(X, p) and end(X, p) when p is co-accessible (resp. accessible) from each vertex of X, with the entire path in X; root(p) looks for a root of the whole graph;

• inline(X) if the subgraph of support X is a finite or infinite path;

• size k (X) when |X| = k.

All these notations stand for monadic formulae . For instance, the inline(X) property is true when there is a root in X and each vertex has output degree 1, and each except the root has input degree 1. Now we may write the formula ϕ w . For this, we need two finite sets p 1 . . . p |u| ∈ U for the static part, q 1 . . . q |v| ∈ V ′ for the beginning of the periodic part and an infinite set V with V ′ ⊆ V .

ϕ w := ∃p 1 , . . . , p |u| , V, q 1 , . . . , q |v| ∈ V : root(p 1 ) ∧   |u|-1 i=1 τ (p i , p i+1 ) ∧ ∂ u i (p i )   ∧ τ (p |u| , q 1 ) ∧ ∂ u |u| (p |u| ) ∧root(V, q 1 ) ∧   |v|-1 i=1 τ (q i , q i+1 ) ∧ ∂ v i (q i )   ∧ ∂ v |v| (q |v| ) ∧inline(V ) ∧ ∀q ∈ V, ∃X ⊆ V, q ′ ∈ X : inline(X) ∧ size |v|+1 (X) ∧ root(X, q) ∧ end(X, q ′ ) ∧ k≤n ∂ k (q) ⇒ ∂ k (q ′ )
We check that p 1 is the general root 0, and q 1 the root of V , which is an infinite path. Formulae τ and ∂ k force the degree of the uv part. For the periodic part, each q ∈ V must be the root of a finite path X q ⊆ V of size |v| + 1, which end has the same degree that q.

The combination of Lemmas 3.4.9 and 3.4.10 yields the following theorem.

Theorem 3.4.11. For any ordinals α = α ′ smaller than ε

0 , MTh(G α ) = MTh(G α ′ ).
This result is the central point of this section, because it it opposed to the Theorem 3.4.2 on ordinals : the family of covering graphs has the MSO-discernability property. One must take care to the fact that here G α and G α ′ are implicitely supposed to be covering graphs. Whether MTh(G α ) is unique among all {⋖}-graphs (up to isomorphism) is open, and is conjectured false.

A whole set of properties could be tested on covering graphs. For instance, the MSO selection property is known to fail for ordinals greater than ω ω [START_REF] Rabinovich | Selection in the monadic theory of a countable ordinal[END_REF]. It would be interesting to know if covering graphs can also raise this limit.

As a consequence of Theorem 3.4.11, there is no generic monadic interpretation from an ordinal greater than ω ω to its covering graph. Below this limit, there is an interpretation, because it is possible to distinguish successive limit ordinals, as in Proposition 3.4.1.

Other properties of covering graphs

We study here other monadic properties of covering graphs and remark that they also belong to the hierarchy. First of all, by Proposition 3.4.4, there is a monadic interpretation I such that I(G α ) = α. In fact, we have much more : all ordinals smaller than α are interpretable in G α .

Proposition 3.4.12. For any α < β < ε 0 , there is a MSO interpretation I such that

G α = I(G β ).
Proof. Following the definition, we look for an interpretation I = {ψ ⋖ }. We use again the fact that the degree word is unique and MSO-definable. Defining the greatest sequence of G α provides a MSO marking on G β , which bounds the set of vertices. More precisely, let Ψ w (p) be an expression similar to ϕ w of Lemma 3.4.10 but where the part τ (p i , p i+1 ) ∧ δ u i (p i ) has been replaced by τ u i (p i , p i+1 ) meaning "p i+1 is the u th i such that p i ⋖ p i+1 "; the same goes for the q j and for τ (p |u| , q 1 ) ∧ δ u |u| (p |u| ). Also add the condition that p is a part of the sequence : ( i p = p i ) ∨ p ∈ V . Then Ψ w (p) is a marking of the greatest sequence associated to w. For a given α, I simply adds the condition of co-accessibility to a vertex marked by Ψ d(α) . ψ ⋖ (p, q) := p

⋖ → q ∧ ∃r (Ψ d(α) (r) ∧ q ⋖ * → r) Then G α = G β ∩ {p ⋖ → q | ∃r (Ψ d(α) (r) ∧ q ⋖ * → r)}.
We end this section by noting that covering graphs also are in the hierarchy.

Proposition 3.4.13. If α < ω ↑↑ (n + 1), then G α ∈ Graph n .

Proof. For any finite α, G α is in fact a finite path labeled by ⋖ and is in Graph 0 . By Lemma 3.4.14 below iterated n times, every ω ... ω k is in Graph n when there are n times ω and 1 < k < ω. Smaller ordinals are captured by a restriction as in Proposition 3.4.12.

We note p a • → q for the longest possible path labeled by a, and p S → q a shortcut for the successor relation, i.e.

p a • → q := p a * → q ∧ ¬∃r (q a → r) p S → q := p ⋖ → q ∧ ¬∃r(p ⋖ → r ∧ r ⋖ * → q).
Now let I = {ϕ ⋖ } and M(p) respectively be the interpretation and marking

p ⋖• # + #• S# + #⋖# ------------→ q ϕ ⋖ (p, q) := M (p) ∧ M (q) ∧ p ⋖• # --→ q ∨ p #• S# ---→ q ∨ p #⋖# ---→ q M (p) := ∃r : root(r) ∧ r ⋖ * #( ⋖ * #) * -------→ p
The marking M(p) allows to start anywhere on the root graph, but as soon as a #-arc has been followed, ⋖-arcs can only be followed backwards. We consider only goals of a #-arc.

The ϕ ⋖ (p, q) formula states the relation on these vertices, leaving three choices : either to follow ⋖-arcs as long as possible (in practice, until a copy of 0) and go down one #-arc; or on the contrary, to follow # backwards as long as possible, then take the successor and one #-arc; or just to follow one # backwards, one ⋖ and one #. Proof. As stated in Corollary 2.2.2, ω α is isomorphic to the set of decreasing sequences of ordinals smaller than α in lexicographic order. Let T = Treegraph(G α ); the 0 of the root graph is still the only root, we call it r. Each p ∈ V T marked by M can be mapped into a decreasing sequence. If r

⋖ * #( ⋖ * #) * -------→ p, then there is a finite sequence (p i ) i≤k such that r ⋖ * # --→ p 0 , p i ⋖ * #
--→ p i+1 for i < k and p k = p, with the same properties as in the proof of Theorem 3.1.2. Each p is thus mapped to an ordinal β p < ω α .

The interpretation ϕ ⋖ provides the relation to make this bijection an isomorphism. Let G = ϕ ⋖ • Treegraph(G α ). We distinguish the three cases of the definition of ⋖.

• If p ⋖• #

--→ q, then q is mapped to (γ 0 , . . . , γ k , 0). This is the successor case β p +1 = β q .

• If p #• S# ---→ q, then let l be the smallest integer such that γ l = γ l+1 = • • • = γ k . Then q is mapped to (γ 0 , . . . , γ l-1 , γ l + 1). This corresponds to the case

β p = β + ω γ l .(k -l) ⋖ β + ω γ l +1 . • If p #⋖#
---→ q, then q → (γ 0 , . . . , γ k-1 , γ) with γ k ⋖ γ. The marking M ensures that q is mapped to a decreasing sequence. This is the recursive case, where

β p = β + ω γ k , β p = β + ω γ ′ k and γ k ⋖ γ ′ k .
Example 3.4.15. Consider G ω , which is an infinite path. A representation of its treegraph is given in Figure 3.7 (plain lines for ⋖, dotted lines for #). The white labeled vertices are the ones marked by M and therefore they are the only ones kept by the interpretation I. We are allowed to go anywhere on the root G ω structure, but as soon as we follow # we can only go backwards. This reflects the construction of an ordinal smaller than ω α as a decreasing sequence of ordinals : the first one is any ordinal smaller than α, but afterwards we only may decrease.

Covering graphs therefore enjoy the properties of graphs of the hierarchy. For illustrations of the three cases in the proof of Lemma 3.4.14, we have

ω 2 ⋖• # ---→ ω 2 + 1, ω 2 + 1 #⋖# ---→ ω 2 + ω, 2 #• ⋖# ----→ ω.
Corollary 3.4.16. For any α < ε 0 , the monadic theory of G α is decidable.

Strictness of covering graphs in the hierarchy

We will prove in Theorem 4.3.8 that ordinals greater than or equal to ε 0 do not belong to the hierarchy. As a consequence, the same is true for the associated covering graphs.

We present here another version of this result. It is based on Theorem 4.5.3 which will be seen in the next chapter. It is actually a pretext to use logical properties of covering graphs, in which it is possible to interpret other separating graphs. In particular, for any function f : N → N, let K f be the prefix tree defined by the following set of leaves :

Leaves(K f ) = {1 i 0 f (i) }.
Let the exp(m, n, i) operation be defined by exp(m, 0, i) = i exp(m, n + 1, i) = m exp(m,n,i) , Theorem 4.5.3 shows that K exp(2,n,•) is not in Graph n . We use this fact for the following result.

Proposition 3.4.17.

If ω ↑↑ (n + 1) ≤ α ≤ ε 0 , then G α / ∈ Graph n .
The proof is separated in several lemmas. Finding a monadic interpretation from G α to K exp(2,n,•) is enough to prove G α / ∈ Graph n . But in fact, Proposition 3.4.12 already states that if ω ↑↑ n + 1 ≤ α ≤ ε 0 , then there is an interpretation from G α to G ω↑↑ n+1 ; so the interpretation from G ω↑↑ n+1 to K exp(2,n,•) is enough. We build this interpretation.

First of all, let us select the ordinals which stand in the k th finite subtree. Let C k n be the set of ordinals smaller than exp(ω, n, k) where each coefficient in RCNF is at most 1, except for the top-most power : . . .

α.ω α.2 α

Let λ ∈ [α, α.2[, λ = β + ω γ .c + η in RCNF with c > 1 (recall that the notation β is used to note the RCNF of β). By Lemma 3.4.5 again, any path from α to α + λ goes through

λ ′ = β + ω γ and λ ′′ = β + ω γ .c α.2 β + ω γ+1 λ λ ′′ λ ′ α But then λ ′ ⋖ β + ω γ+1 = τ (λ ′′ ) when c > 1, so λ ′′ / ∈ S α . Recursively, we suppose that any path from exp(ω, n-1, k) to γ / ∈ C k n-1 with exp(ω, n- 1, k) ≤ γ < exp(ω, n -1, k).2 goes through γ ′ and γ ′′ , with γ ′ ⋖ τ (γ ′′ ). Then if λ = β + ω γ + η, define λ ′ = β + ω γ ′ and λ ′′ = β + ω γ ′′
which propagates the property to level n. All this proves that if λ = α + ω γ 0 + • • • + ω γ j in CNF and λ ∈ S α , then all γ i are distinct and are in C k n-1 . Therefore S α ⊆ α + C k n . For the other side, let λ ∈ α + C k n . If λ = α the case is done, otherwise

λ = α + ω γ 0 + • • • + ω γ h
with each γ i ∈ C k n-1 . We have to prove that ∃λ ′ ⋖ λ in α + C k n . By induction on n with α = 0, for

γ h > 0, ∃γ ′ h ⋖ γ h in C k n-1 , so λ ′ = α + ω γ 0 + • • • + ω γ ′
h answers to the request (since the γ i are decreasing, γ ′ h is still distinct from the γ i ,i < h). If γ h = 0, then we take

λ ′ = α + ω γ 0 + • • • + ω γ h-1 . If not, now τ (λ) = α + ω γ 0 + • • • + ω τ (γ h ) . If λ ′ ∈ S α is such that λ ′ ⋖ τ (λ), then λ ′ = α + ω γ 0 + • • • + ω γ h-1 + ω γ for some γ ∈ γ h ∩ C k n-1
, but then by induction we never have γ ⋖ τ (γ h ), which is a contradiction. Lemma 3.4.21. The greatest sequence of ω ↑↑ (n + 1) is ultimately (exp(ω, n, k)) k≥1 .

Proof. This is a corollary of the proof of Lemma 3.4.8, since as in the previous proof exp(ω, n, k) ⋖ exp(ω, n, k + 1).

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

Proof of Prop. 3.4.17. We concatenate the previous lemmas. Recall that K exp(2,n,•) is the prefix tree of leaves {1 k 0 exp(2,n,k) }.

We have seen in Prop. 3.4.12 that the greatest sequence of α in selectable in G α . Since we work in G ω↑↑ n+1 , by Lemma 3.4.21 we can restrict ourselves to the sequence (exp(ω, n, k)) k≥1 , which will be the "horizontal path" of K exp(2,n,•) . Let ϕ 1 (x, x ′ ) be the formula satisfied if x, x ′ are part of this sequence and x ⋖ x ′ .

Let ϕ(x, y) be as defined by Lemma 3.4.20. Note that ϕ does not depend on k. If x = exp(ω, n, k) for some k, then the set {y | ϕ(x, y)} has cardinal exp(2, n, k). Moreover, this set is already ordered by ⋖ * , so we may find a formula ϕ 0 (y, y ′ ) restricted to set and satisfied by (y, y ′ such that y ⋖ * y ′ and there is no z between y and y ′ . We have therefore the "vertical path" hanging from exp(ω, n, k) and of length exp(2, n, k).

The interpretation

I n = {ϕ 0 , ϕ 1 } maps therefore G ω↑↑ n+1 into K exp(2,n,•) . In fact, for any ω ↑↑ n + 1 ≤ α < ε 0 , I n maps G α into K exp(2,n,•) .

The case of G ε 0

The covering graph G ε 0 can be defined without changing the definition of fundamental sequence. It has unbounded degree, but has still the property of Proposition 3.4.12 : it can give any smaller ordinal via monadic interpretation. This yields the following corollary of Proposition 3.4.17.

Corollary 3.4.22. G ε 0 does not belong to the pushdown hierarchy.

It would be interesting to know more about the logical properties of this graph. This question is indeed tightly linked to the notion of a "limit operation" preserving decidability of MSO-theory. Some first ideas appear in [START_REF] Thomas | Model transformations in decidability proofs for monadic theories[END_REF].

Conjecture 3.4.23. MTh(G ε 0 ) is decidable.

Chapter 4

The structure of tree frontiers

The first question one may ask after Theorem 3.1.2 is the converse : if any ordinal smaller than ω ↑↑ n + 1 can be constructed at level n, is this classification is strict or not? For a start, can ω ω be in Graph 1 ? For this first question, it is shown in [START_REF] Delhommé | Automaticité des ordinaux et des graphes homogènes[END_REF][START_REF] Khoussainov | Automatic linear orders and trees[END_REF] that ω ω cannot be a (word-)automatic ordinal, whereas structures in Graph 1 are. On the other hand, one can consider the orders composed by frontier of trees, as in [START_REF] Thomas | On frontiers of regular trees[END_REF][START_REF] Courcelle | Frontiers of infinite trees[END_REF]. At the second level, [B É10] considers frontiers of algebraic trees to find out that such ordinals are smaller than ω ω ω . The same paper conjectures that frontiers of trees in the hierarchy yield successive ω ↑↑ n.

In order to follow this presentation, we first need to reduce ourselves to frontiers. Hence a first result of this chapter is that orders of Graph n are exactly frontiers of Tree n . By the result of [B É10], ordinals of Graph 2 are smaller than ω ω ω . In this chapter we work out apply a recursive argument and get the expected generalization for every level, in Theorem 4.3.8. In Section 4.4 we remark that the same result can be extended to general scattered orders, measured by Hausdorff rank. In parallel we study the related Cantor-Bendixson rank of these trees.

To obtain these results, Section 4.1 presents a particular version of monadic interpretation on deterministic trees, in the form of a automaton "walking" on the tree.

Tree-walking automaton

It is well-known that on deterministic trees MSO logic is captured by parity tree automata [START_REF] Michael Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. This equivalence can be used to characterize the binary relations defined by MSO formulae on such trees using a finite state automaton running on the tree. The tree-walking automata is not new [AU71], but they have mostly been used on finite trees [START_REF] Bojanczyk | Tree-walking automata do not recognize all regular languages[END_REF][START_REF] Bojanczyk | Tree-walking automata cannot be determinized[END_REF]; see [START_REF] Bojanczyk | Tree-walking automata[END_REF] for a survey. Here, we use these automata on infinite trees as a "weak form" of monadic interpretations.

Definition.

A non-deterministic tree-walking automaton or simply TWA working on deterministic trees over Σ colored by Γ is a tuple A = (Q, q 0 , F, ∆) where Q is the finite set of states, q 0 ∈ Q is the initial state, F is the set of final states and ∆ is the set of transitions. A transition is a tuple (p, c, q, a) with

• p ∈ Q is the current state,
• c ∈ Γ is the color of the current node,

• q ∈ Q is the next state,

• a ∈ Σ ∪ {ε, ↑} is the action to perform. Intuitively ε corresponds to "staying in the current node", ↑ to "going to the parent node" and d ∈ Σ corresponds to "going to the d-son".

A run of the automaton on a tree t is a sequence (q 0 , u 0 ) . . . (q n , u n ) over Q×Dom(t) where q n ∈ F and for all i < n, if

u i+1 = u i a i with a i ∈ Σ ∪ {ε} then (p i , t(u i ), p i+1 , a i ) ∈ ∆, otherwise if u i ∈ u i+1 Σ then (p i , t(u i ), p i+1 , ↑) ∈ ∆.
We say that A accepts the pair of nodes (u 0 , u n ).

Remark 4.1.1. Note that the automaton is a priori not deterministic; [START_REF] Bojanczyk | Tree-walking automata cannot be determinized[END_REF] shows that a TWA cannot generally be determinized, even when the tree is finite and the only run considered is from the root to the root.

We have restated in Proposition 2.4.3 that a monadic interpretation on a deterministic tree can be encoded in a rational inverse mapping up to monadic marking. But the actual proof of this definition is even stronger, as it constraints the rational mapping to the shortest path between two vertices. This leads to the following rephrasing of this result. A run is said to be simple if the sequence forms a simple path, i.e. each node is visited at most once. Proposition 4.1.2 ([Car06, Prop. 3.2.1]). For any deterministic tree t and any MSOformula ϕ(x, y), there exists an MSO-coloring M adding colors and a TWA A such that t |= ϕ[u, v] if and only if A accepts (u, v) on M(t). In this case there exists a simple run from u to v.

A TWA is therefore a "weak form" of a monadic interpretation. It means that up to a recoloring, the binary formula can be restricted to the smaller connex set containing the interpretations of the two free variables.

Remark 4.1.3. Conversely, for any simple TWA and coloring M, there is a MSO formula ϕ such that (u, v) is accepted in M(t) iff t |= ϕ[u, v] where ϕ only works on the simple path between u and v. In particular, if t ′ is the smallest subtree containing u and v, then

t ′ |= ϕ[u, v].
This can be directly seen by encoding the automaton in a logical formula. The formula defines two set U and V which are paths respectively from u ∧ v to u and from u ∧ v to v. Then each step of the automaton can be reproduced backward on U and forward on V . More formally, there have to be sets X q 0 , . . . , X q |Q| representing states, with u ∈ X q 0 and v ∈ q∈F X q . For the U part, assuming we know that U is a path,

∀x ∈ U ∩ X p \ {u ∧ v}, ∃y ∈ U : y → x ∧ q∈Q   y ∈ X q ⇒ δ(p,c)=(q,↑) (c, x)   and for the V part, ∀x ∈ V ∩ X p \ {v}, ∃y ∈ V : a∈Σ   x a → y ∧ q∈Q   y ∈ X q ⇒ δ(p,c)=(q,a) (c, x)     Remark 4.1.4.
The equivalence between a MSO formula and recognizability by TWA allows us to define another kind of interpretation as in Section 2.4.1. The TWA-interpretation on a deterministic Σ-tree is a tuple (M, (A a ) a∈Γ ) where each A a is a TWA on deterministic Σ-trees. The result of this interpretation on a Σ-tree t is the graph

{x a → y | a ∈ Γ, A a accepts (x, y) in M(t)}.
It follows by Proposition 4.1.2 that graphs of Graph n are exactly TWA-interpretations of deterministic trees of Tree n .

From graphs to frontiers

In this section, we consider the linear orders defined by frontiers of deterministic trees, i.e. the leaves of a deterministic tree under lexicographic ordering as defined in Section 2.1.4. Example 2.4.1 shows that the frontier of a (colored) deterministic tree in t can be defined in t using an MSO-interpretation. Hence the frontiers of the (resp. colored) deterministic trees in Tree n are (resp. colored) linear orders in Graph n . This section proves that the converse inclusion holds : any order of Graph n can be seen as a frontier of a deterministic tree in Tree n . This is Theorem 4.2.6.

As a starting point, it is not difficult to restrict to some kind of normalized trees.

Proposition 4.2.1. For any det. t, there is a full binary prefix tree t ′ with Fr(t) = Fr(t ′ ). Moreover, if t ∈ Tree n , then t ′ can be chosen in Tree n .

Proof. If the order is of type 1, a tree reduced to a root is enough. Suppose otherwise. The first step is that we may only consider prefix trees by pruning. For the binary property, let t be prefix on a ranked alphabet Σ and let τ : Σ → {0, 1} * a prefix binary mapping. For any I ⊆ Σ, let C I be the finite tree of leaves {τ (a) | a ∈ I}. We replace each node x which is not a leaf by C {a|xa∈Dom(t)} , of root r x , so that r xa = r x .τ (a) whenever xa ∈ Dom(t).

The resulting tree is binary and has yields the same order. Finally, to get a full tree, we contract every path 1(1 + 0) * (resp. 0(1 + 0) * )) without branching into 1-arcs (resp. 0-arcs).

To perform these operations within Tree n , we work on the folded graph. The result is obvious for finite trees, so we will suppose that n > 0. Let t ∈ Tree n . We first use a MSOmarking µ to mark the prefix closure of leaves. Let G ∈ Graph n-1 , r ∈ V G such that µ(t) = Unf(G, r). The restriction to marked vertices accessible from r is an MSO-interpretation. Next, the operation substituting x with C {a|∃y,x a -→ G y} is a MSO-transduction. Finally, the contraction of simple paths is again a MSO-interpretation. So all these operations give a graph still in Graph n-1 , which unfolding yields the same frontier than t.

Finite orders are not a problem for us, so we start with n ≥ 1, a finite set of colors Γ together with colored linear order L : D, < L → Γ in Graph n . This order is the MSO-interpretation I of a deterministic tree t in Tree n . The following property recalls that we can suppose that D is exactly Leaves(t).

Proposition 4.2.2. For any interpretation I and deterministic tree t ∈ Tree n , there is an interpretation I ′ and a det. binary prefix tree t ′ such that I(t) ≃ I ′ (t ′ ) and vertices of I ′ (t ′ ) are exactly leaves of t ′ .

Proof. In a deterministic t, we mark each vertex x considered by I. In the folded graph G such that Unf(G, r) = t, a monadic transduction T adds a #-arc from these vertices to a fresh vertex. It is then easy to adapt I to pick leaves of Unf(T (G), r). By marking leaves targets of #-arcs and using Proposition 4.2.1, we get the required result. Using Propositions 2.5.4, 4.1.2 and 4.2.2, we have that there exists a deterministic prefix tree t ∈ Tree n colored by Γ ′ , a TWA A and a projection µ : Γ ′ → Γ such that D is isomorphic to the set of leaves of t, for all u, v ∈ D, u < L v iff A accepts (u, v) with a simple path and for all u ∈ D, L(u) = µ(t(u)).

The construction of this section rearranges the leaves of t into a new deterministic tree s(t) so that lexicographic order on s(t) matches < L on D. For any leaf u ∈ D and for v ⊏ u ∈ D, we consider sequences u 0 > L u 1 > L . . . > L u k of leaves starting with u 0 = u and such that for i ∈ [0, k -1], u i ∧ u i+1 = v. Intuitively, the u i alternate from one subtree of v to the other. Using a pumping argument on A, we can show that there exists n 0 ≥ 0 such that for every leaf u ∈ D and all node v ⊏ u, these sequences have a length less that n 0 . We may then define s(u, v) as the maximal length of such a sequence. Lemma 4.2.3. There exists n 0 ≥ 0 such that for any leaf x of t and for all y ⊏ x, s(x, y) ≤ n 0 .

Proof. Suppose that s is unbounded : for all n, there is x and y ⊏ x such that there is a decreasing sequence seq(x, y) = (x 0 , x 1 , . . . , x n , . . . ), possibly infinite. For each x i+1 in this sequence, there is a simple run of A from x i+1 to x i containing (q i , y), y being their largest common prefix. If n > 2|Q|, there exist i < j such that q 2i = q 2j . This means there are simple runs (q 0 , x 2i+1 ).u i .(q 2i , y).v i .(q ′ i , x 2i ) and (q 0 , x 2j+1 ).u j .(q 2i , y).v j .(q ′ j , x 2j ) for some u i , v i , u j , v j ∈ (Q × Dom(t)) * . Then the sequence (q 0 , x 2i+1 ).u i .(q 2i , y).v j .(q ′ j , x 2j ) is also a run from x 2i+1 to x 2j , so x 2i+1 < x 2j . This is contradictory with the fact that the sequence is decreasing.

To each node x, we associate the finite sequence s(x) of length |x| of elements in [0, n 0 ] defined by s(x, x 0 ), . . . , s(x, x |x|-1 ), where for all k ∈ [0, |x| -1], x k denotes the prefix of x of length k.

For an illustration, consider the (uncolored) finite tree on left of Figure 4.1, where order on leaves is given along with the sequence s. For instance, the leaf number 3 has maximal sequences (3, 0), (3, 2, 1) and (3, 1), so s(3) = (2, 3, 2).

The next lemma shows a key property : s is a morphism from < L to < lex .

Lemma 4.2.4. For all x, y leaves of t, x < L y iff s(x) < lex s(y) and s(x) ⊏ s(y).

Proof. Let x < Ly and let z be the largest prefix of x and y, with x = z = y since x and y are leaves. For each z ′ ⊏ z, there is decreasing sequence seq(x, z ′ ) = (x, x 1 , . . . , x s(x,z ′ ) ), so there is a decreasing sequence (y, x 1 , . . . , x s(x,z ′ ) ) because the largest prefix of y and x 1 is z ′ and x 1 < L x < L y. Thus s(x, z ′ ) ≤ s(y, z ′ ). For z, the sequence seq(x, z) = (x, x 1 , . . . , x s(x,z) ) can be extended into a decreasing sequence (y, x, x 1 , . . . , x s(x,z) ), which means s(x, z) < s(y, z) and s(x) < lex s(y) with s(x) ⊏ s(y). The other direction is straightforward. Consider the tree s(t) over the finite alphabet [0, n 0 ] obtained by taking the prefixclosure of { s(u) | u leaf of t)}. The frontier of s(t) is isomorphic to (D, < L ). To ensure that colored frontier of s(t) is isomorphic to L, we add the appropriate color to the leaves of s(t). In practice, Dom(s(t)) := {y | ∃x ∈ Leaves(t) ∧ y ⊑ s(x)} and s(t)(x) = t(x) for a leaf x. A surprising result is that this tree can be built in the same class than the original tree.

Lemma 4.2.5. If t ∈ Tree n , then s(t) ∈ Tree n .

Proof. Let G ∈ Graph n-1 and r ∈ V G such that Unf(G, r) = t and G is accessible from r. There is a MSO-interpretation I replacing each arc labeled by a ∈ {0, 1} by n 0 + 1 arcs labeled by (i, a) 0≤i≤n 0 . Let t ′ = Unf(I(G), r). In particular, for any i, t ′ restricted to ((i, 0) + (i, 1)) * is isomorphic to t by the projection τ ((i, a)) = a.

0 (1,1) 4 (3,2) 3 (2,3,2) 1 (2,1,1) 2 (2,2) 0 1 1 1 2 3 2 1 2 3 4 2 1 2 3
Figure 4.1: Order in a finite tree t and "arranged" tree s(t).

There is a MSO-formula ψ(x, z) satisfied by nodes x, z such that if s(τ (x), τ (z)) = i then z.(i, a) ⊑ x for some a ∈ Σ and i < n 0 , where n 0 is defined in Lemma 4.2.3. Indeed, by Remark 4.1.3 the pairs of leaves of t accepted by A are recognizable by a MSO-formula. So the formula ψ finds two sets X 0 , X 1 which elements have prefix respectively z.(i, 0) and z.(i, 1), and x ∈ X a . The formula states that for each y (except one) in one set there is a y ′ in the other such that there is a simple run of A between y and y ′ up to projection by τ . Eventually ψ checks that |X 0 ∪ X 1 | = i, and that there is no such sets with

|X 0 ∪ X 1 | = i + 1.
There is therefore a formula ϕ(x) satisfied by nodes such that ψ(x, z) is true for each prefix z of x. Let t ′′ be the tree restricted to the prefix closure of vertices satisfying ψ(x) : t ′′ ∈ Tree n . By Lemma 4.2.4, if ψ(x, z) and ψ(y, z), then either x and y have the same prefix z, or s(τ (x), τ (z)) = s(τ (y), τ (z)); so if z.(i, a) ∈ Dom(t ′′ ), then z.(i, 1a) / ∈ Dom(t ′′ ). This means projecting arcs labels on their first component does not change the tree up to isomorphism. The resulting tree is s(t).

It remains to bind the lemmas and Proposition 4.2.1 to get the main result. Theorem 4.2.6. Any colored linear order of Graph n greater than 1 is the frontier of a full prefix tree in Tree n .

Proof. By Proposition 4.1.2, for each linear order L in Graph n there is a det. binary tree t ∈ Tree n , an automaton A and a recoloring µ such that µ(A(t)) = L. By Proposition 4.2.2, A only works on leaves of t.

The Lemmas 4.2.4 and 4.2.5 prove that there is a tree s(t) on a ranked alphabet such that µ(Fr(s(t))) ≃ L. By Proposition 2.5.4, the recoloring can be applied to s(t) without going out of Tree n . We can eventually apply Proposition 4.2.1 to get a full binary prefix tree.

A particular case of this Theorem is the particular case of ω-words. We will use this result through Chapter 5. Proof. It is a direct consequence of Proposition 2.2.11. Indeed, the set of paths from r to x is a subset of Dom(t) and has therefore a minimum element ℓ(x). If r

ℓ(x) --→ G
x is not a simple path, then there are ℓ(x) = u 1 u 2 u 3 with nonempty u 2 , u 3 and a vertex y ∈ V G such that r

u 1 -→ y u 2 -→ y u 3 -→ x. We may suppose u 1 is such that |u 1 | is maximal and r u 1 -→ y is a simple path. Since G is deterministic,
• either u 2 begins with 0 and u 3 with 1, but then u 1 u 2 u 2 u 3 < lex ℓ(x) is a path too;

• or the converse, but u 1 u 3 < lex ℓ(x).

So u 2 must be empty, and r ℓ(x) --→ x is a simple path.

Let T be the subgraph of G defined by

T = {x a → y | x a -→ G y ∧ ℓ(y) = ℓ(x) • a}.
T is the tree of shortest paths from r, and therefore a "spanning tree" as required.

Lemma 4.3.3. T is a tree where each branch has finitely many 0, and

T ∈ Graph n-1 . Proof. For each x ∈ V G , if r w 1 -→ T x and r w 2 -→ T x, then min < lex {w | r w -→ p} ≥ w 1 and min < lex {w | r w -→ x} ≥ w 2 , so w 1 = w 2 .
Since G is deterministic, so is T and thus T is a det. tree. Therefore T is a subtree of t and its branches have finitely many 0.

There is an interpretation I = {ϕ 0 , ϕ 1 } building I(G) = T . Indeed, it is possible to define subsets containing the smallest path from r to a given x, and to select the smallest such subset by inclusion. Then arcs are selected to build a path. Note that T is not a well-ordered tree, because it is not necessarily a prefix tree. This property will be fixed later on by "completing" the tree.

Since T is a tree, we may take its tree presentation, so that its vertex set is the set of paths from the root, and thus r = ε. This is also the set of vertices of G.

The following lemma states a technical property on arcs of G which are not in T .

Lemma 4.3.4. For each x a → y ∈ G \ T ,

• if x < lex y then x ⊏ y;

• if a = 0, then y < lex x and x⊥y.

Proof. For a ∈ {0, 1}, if As hinted above, we now tranform T to get a prefix tree. Let T be the tree such that T is a subtree of T and whenever x a -→ G y, then xa ∈ T . It easy to see that T can be transducted from G.

x a → q ∈ G \ T , x <
Lemma 4.3.5. T is a well-ordered tree of Graph n .

Proof. Since Comp only add leaves to T , each infinite branch of T is also in T so it may have finitely many 0. Since G is a full binary graph (each vertex has arity 0 or 2), then each vertex of T has also arity 0 or 2. The complete binary tree is not a subtree of T , so each subtree of T has at least one leaf; T is prefix and therefore T is a well-ordered tree. Since Graph n is closed by transduction, T ∈ Graph n .

As a consequence, by Proposition 4.3.1, Fr( T ) is an ordinal.

Example 4.3.6. Figure 4.3 is a example with a finite graph G and Fr( T ) = 6. For each leaf w of Unf(G, r), σ(w) ∈ (ε + 4 * 3 + 5)2 * (0 + 1). So we have

Fr(Unf(G, r)) = ω + ω 2 + ω = ω 2 + ω ≤ ω 6 .
The previous example leads to the central lemma of this section, which is the recursion mechanism. There is a natural isomorphism τ from leaves of T to α. As described in Corollary 2.2.2 and used throughout in Chapter 3, we are going to build a injective morphism from the leaves of t to the set of decreasing sequences of ordinals smaller than α in lexicographic order.

Let w be a leaf of t. There is a path r w -→ p in G where p is a leaf of G. Let (p i ) 0≤i≤|w| be the nodes of this path, i.e. r be the letter such that w i+1 = w i .a i and a |w| = ε. We build the following finite sequence σ(w) associated to w :

σ(w -1 ) = ε (by convention) for 0 ≤ i < |w| -1, σ(w i ) = σ(w i-1 ) if p i+1 = p i .a i , i.e. p i a i → p i+1 ∈ T σ(w i ) = σ(w i-1 ), τ (p i .a i ) if p i a i → p i+1 / ∈ T σ(w) = σ(w |w|-1 ), τ (p |w| )
We prove that σ(w) is decreasing. Suppose σ(w) has at least two elements. Let i < j be the indexes of two consecutive elements, i.e. σ(

w j ) = σ(w i-1 ) • τ (p i .a i ) • τ (p j .a j ). Then p i a i → p i+1 ∈ G \ T . By Lemma 4.3.4, either p i ≥ lex p i+1 or (p i < lex p i+1 and p i ⊏ p i+1 ).
By construction, p i+1 ⊑ p j so p j .a j is in the subtree of T of root p i+1 . Several cases arise.

1. Either p i = p i+1 . Then a i = 1 and p i .1 is the largest leaf of the the subtree of T of root p i+1 , so p i .1 ≥ lex p j .a j .

2. Or p i+1 ⊏ p i . Then again a i = 1, and p i = p i+1 1 k for some k, because a cycle in G cannot contain any 0. So p i .1 is the largest of the subtree of root p i+1 and p i .1 ≥ lex p j .a j .

3. Or p i > lex p i+1 and p i+1 ⊥p i , then p i > lex p j and p i .a i > lex p j .a j .

Or p

i ⊏ p i+1 . Then a i = 1. Since G is deterministic, p i .0 ⊏ p i+1 ⊏ p j . So p i .1 > lex p j .a j .
These cases are summed up in the following figure. Arcs 1, 2 and 4 are necessarily labeled by 1, whereas arc 3 may be labeled by 0 or 1.

p i 1 2 3 4
To sum up, two successive elements τ (p i .a i ), τ (p j .a j ) of σ(w) are such that p i .1 ≥ lex p j .a j and so τ (p i .a i ) > τ (p j .a j ). The sequence σ(w) is decreasing.

Let w < v be two leaves of t of largest common prefix u. Let i < |u| be the largest such that (p i .a i ) is in σ(w) : then σ(w i ) = σ(v i ). Let j w , j v ≥ |u| be the smallest such that (p jw .a jw ) ∈ σ(w) (resp. (p jv .a jv ) ∈ σ(v)). Then p jw .a jw = p i+1 .u w with u.u w ⊑ w.0 (resp. p jv .a jv = p i+1 .u v with u.u v ⊑ v.0) and u w < u v , so p jw .a jw < lex p jv .a jv . This shows that σ is a injective morphism.

We have thus proved that σ is an injective morphism from leaves of t to decreasing sequences of ordinals of α by lexicographic order. So Fr(t) ≤ ω Fr( T ) .

From here, the main theorem is obtained by induction, since finite ordinals are in Graph 0 . Theorem 4.3.8. For n ≥ 1 and any ordinal α, α ∈ Graph n if and only if α < ω ↑↑ (n+1). This results give an alternative proof of the strictness of the pushdown hierarchy and shows that ε 0 does not belong to this hierarchy.

Another direct corollary concerns the interpretation of an ordinal into another. For instance, for any α < ω ω , it is possible to find an interpretation I such that α = I(ω). As a corollary of the previous theorem, we cannot interpret more1 . At any level, if β < ω ↑↑ n ≤ α then α cannot be interpreted in β. Interestingly, the same property applies to covering graphs. It could be interesting to examine precisely the orbit of a given ordinal under monadic interpretations. Theorem 3.4.2 hints that this orbit must actually be very small, i.e. if α has ω-head β, then the orbit would be of the form ω ω ∪ {β + δ | δ < ω ω }; for covering graphs, the orbit is larger.

Scattered linear orders

In Section 3.2, we have proved that any power by α < ω ↑↑ n of ζ is actually in Graph n . In the other way around, we consider the scattered linear orders in the pushdown hierarchy. Using the result of the previous section, we characterize the Hausdorff rank of scattered orderings of the hierarchy : this is Theorem 4.4.12.

To reach this result, we begin with a general proposition on trees have a scattered frontier. Then we notice that we may recursively switch subtrees of such a tree to obtain an ordinal frontier. This does not change the mesure based on the number of infinite branches in the tree, called Cantor-Bendixson rank of the tree. It is then sufficient to prove that this CB-rank is tightly related to the Hausdorff rank, which allows us to conclude.

Trees with scattered frontiers

The countable scattered orders are those which are frontiers of trees with only countably many infinite branches also called tame trees. The following proposition is part of the folklore.

Proposition 4.4.1. Let t be a deterministic prefix binary tree, the following propositions are equivalent:

1. Fr(t) is a scattered linear order, 2. t has countably many infinite branches, 3. t does not contain any branching subset (i.e. a non-empty subset U ⊆ Dom(t) such that for all u ∈ U , u0{0, 1} * ∩ U = ∅ and u1{0, 1} * ∩ U = ∅).

Proof. We will show that 1 ⇒ 3 ⇒ 2 ⇒ 1. 1 ⇒ 3. We prove this implication by contraposition. Assume that t contains a branching subset U . There exists a mapping f :

U × {0, 1} → U s.t. for all u ∈ U and i ∈ {0, 1}, f (u, i) belongs to u • i • {0, 1} * . Furthermore, as t is prefix, for each u there is a leaf v with u ⊏ v.
For any w ∈ {0, 1} * , we define the nodes u w and v w . Let u ε be any node of U . For any u w , we set

u w0 = f (f (u, 0), 0), u w1 = f (u, 1) and v w a leaf such that f (f (u, 0), 1) ⊏ v w . Then v w < lex v w ′ ⇐⇒ (w⊥w ′ ∧ w < lex w ′ ) ∨ (w ′ ⊑ w0) ∨ (w1 ⊑ w ′ ). This order is dense on {0, 1} * , so (v w ) {w∈{0,1} * } is a dense suborder of Fr(t). v w f (f (u w , 0), 0) f (f (u w , 0), 1) f (u w , 0) f (u w , 1) u w
2 ⇒ 1 In the proof of Thm. 7.7 of [START_REF] Khoussainov | Automatic linear orders and trees[END_REF], it is shown that if t has countably many branches then the Kleene-Brouwer ordering KB(t) is scattered (see Section 2.2.3). As Fr(t) KB(t), we can conclude. 3 ⇒ 2 Assume that t has uncountably many infinite branches. Consider the set of U of nodes of t such that there are uncountably many infinite branches going through x0 and through x1. We prove that if there are no point of U below some node u of t then there are only countably many infinite branches going through u. Indeed, suppose that u bears infinitely many branches, we could construct a sequence of consecutive nodes (u i ) i∈N of t starting with u such that for all i ∈ N, u i+1 is a son of u i and its other son v i+1 (if it exists) has only countably many infinite branches going through it. The set of branches going through u is equal to the following countable union:

• the unique branch going through the u i 's,

• the set of infinite branches going through the v ′ i s for i ≥ 1.

A countable union of countable set is again countable. So if x ∈ U , then x0(0+1) * ∩U = ∅ and x1(0 + 1) * ∩ U = ∅, and U is a branching subset.

Remark 4.4.2. The direction 2 ⇒ 3 is also easily shown by contraposition. Assume that Dom(t) contains a branching subset U . As U is branching, there exists a mapping f : U × {0, 1} → U s.t. for all u ∈ U and i ∈ {0, 1}, f (u, i) belongs to ui{0, 1} * . Let x 0 be an arbitrary element of x 0 . To any infinite sequence δ = (δ i ) i∈N ∈ {0, 1} ω , we associate the unique infinite branch of t going through the x i where for all i ≥ 0,

x i+1 = f (x i , δ i ).
This defines an injection from {0, 1} ω into the set of infinite branches of t. Hence t has uncountably many infinite branches.

Permutation of subtrees

We introduce here the notion of permutation of subtrees in a tree. Intuitively, we have already seen the notion of unlabeled trees, i.e. the class of trees which have the same image under label projection (up to isomorphism, as usual). Given a deterministic binary tree t, what other deterministic binary trees are in the same class? And what of their frontiers?

Definition. Given two deterministic trees t and t ′ , we write t ≡ t ′ if there exists a bijection from Dom(t) to Dom(t ′ ) preserving the ancestor relation (i.e. for all u, v ∈

Dom(t), u ⊑ v iff h(u) ⊑ h(v)).
This section is devoted to the following property of this relation.

Proposition 4.4.3. For any prefix tame full binary tree t, there exists a well-ordered tree t ′ such t ≡ t ′ . Furthermore, if t belongs to Tree n than t ′ can also be chosen in Tree n .

Let u 0 , . . . , u n , . . . be the consecutive nodes of B. In particular u 0 = ε and for all i ≥ 0, there exists k i ∈ {0, 1} such that u i+1 = u i k i . Let B ′ be the corresponding infinite branch in t (i.e. B ′ = h -1 (B)) and let v 0 , . . . , v n , . . . be the consecutive nodes of B ′ .

In the play π, Branch plays so as to stay on B ′ . Initially this is satisfied as v 0 = ε. If the token is at some v i and Branch has to play, Branch moves to some v j with j > i such that k j = 0. Such a j always exists as by assumption there infinitely many k j equal to 0. By definition of h, we know that Φ(v j ) = v j+1 . As Spoiler plays according to Φ he moves to v j+1 .

It remains to show that t ′ can be chosen in Tree n if t is in Tree n . A positional winning strategy Φ for Spoiler can be coded by two sets of vertices U 0 and U 1 respectively corresponding to set of nodes u s.t. Φ(u) = 0 and Φ(u) = 1. Consider an MSO-formula ϕ(X 0 , X 1 ) such that t |= ϕ[U 0 , U 1 ] if and only if U 0 and U 1 encode a positional winning strategy for Φ. The formula ϕ simply states that there are no infinite branch

B = b 1 . . . b n • • • ∈ {0, 1} ω such that for infinitely many k ≥ 0, b 1 . . . b k ∈ U b k+1 . As Branch loses G, t |= ∃X 0 , X 1 , ϕ[X 0 , X 1 ].
From Prop. 2.5.7, it follows that there exists a tree t ∈ Tree n colored with two sets U 0 and U 1 coding a positional winning strategy for Spoiler. Let c 0 and c 1 the colors corresponding respectively to U 0 and U 1 . The swapping to obtain t ′ can be obtained by applying an MSO-interpretation to the graph in Graph n-1 whose unfolding is t. More formally, let G be a graph in Graph n and let r ∈ V G s.t. t = Unf(G, r). Consider the MSO-interpretation I which relabels the arcs labeled by 0 (resp. 1) by 1 (resp. 0) if their source is colored by c 1 , erases the colors c 0 and c 1 and otherwise leave the graph untouched. It is easy to check that t ′ ≃ U nf (I(G), r) which concludes the proof.

Cantor-Bendixson rank of deterministic trees

The Cantor-Bendixson rank of a tree is an ordinal assessing the branching complexity of a tree. We use a definition taken from [START_REF] Khoussainov | Automatic linear orders and trees[END_REF].

Definition. For X ⊆ Dom(t), we write ∂(X) the set of nodes x ∈ X with at least two infinite branches from x in X. It is easy to see that if X is prefix closed then so is ∂(X). Hence the operation can be iterated as follows :

∂ 0 (X) = X ∂ α+1 (X) = ∂(∂ α (X)) ∂ λ (X) = α<λ ∂ α (X) for limit λ.
The Cantor-Bendixson rank (CB-rank) of t, noted r CB (t), is the least ordinal α such that ∂ α (Dom(t)) = ∂ α+1 (Dom(t)).

Remark 4.4.6. This is an adaptation [Kec94, Exercice 6.17] of the standard notion of Cantor-Bendixson rank of an arbitrary topological space X. The Cantor-Bendixson derivative DX is the set of accumulation points, i.e. DX = {x ∈ X | x ∈ X \ {x}}.

As [KRS05, Rem. 7.2] points out, it is equivalent to the above definition if we take X as the set of infinite paths in the tree.

From [START_REF] Khoussainov | Automatic linear orders and trees[END_REF], t is tame if and only if there exists α s.t. ∂ α = ∅. On the opposite, a tree with uncountably many branches is such that any node of ∂ r CB (t) (t) belongs to a branching subset.

For tame trees t, we adopt a slightly modified version of the CB-rank, written rCB (t), which is the smallest ordinal α such that ∂ α (t) is finite. The difference between rCB and r CB is at most one as rCB (t) ≤ r CB (t) ≤ rCB (t) + 1.

The CB-rank of tame trees and the Hausdorff rank of their frontier are tightly linked.

Proposition 4.4.7. For every prefix and tame binary tree t,

rCB (t) = r(Fr(t)) if rCB (t) < ω, rCB (t) = r(Fr(t)) + 1 otherwise.
Proof. Let t be a prefix tame binary tree t. As the construction of Fact 4.2.1 does not change neither the CB-rank nor the frontier of the tree, we can assume w.l.o.g. that t is also full. For every prefix tame full binary tree t, we write WF(t) the smallest ordinal α such that there exists a well-ordered tree t ′ with t ≡ t ′ and Fr(t ′ ) = α. Proposition 4.4.3 garantees the existence of at least one such t ′ .

We are going to show by transfinite induction on WF(t) that for every a prefix tame full binary tree t that rCB (t) = r(Fr(t)) + δ with δ = 0 if rCB (t) < ω and δ = 1 otherwise. This is obvious for finite trees.

Assume that the property holds for all α < β for some β. Let t be a prefix tame full binary tree with WF(t) = β. Let t ′ be a full well-ordered tree such that Fr(t) = β and t ≡ t ′ .

We distinguish two cases depending on whether 1 ω is an infinite branch in t ′ . 1 ω is not an infinite branch in t ′ . Let m ≥ 0 be the maximal integer such that 1 m belongs to t ′ . For all i ∈ [0, m -1], let t ′ i be the subtree of t ′ rooted at 1 i 0 et let t ′ m be the tree root in 1 m consisting on only one node. As t ′ is full,

Fr(t ′ ) = [0,m-1] Fr(t ′ 1 ) + 1. In particular for all i ∈ [0, m -1], Fr(t ′ i ) < Fr(t ′ ) = β.
By definition of ≡, there exists a word w = w 1 . . . w m ∈ {0, 1} m which the branch in t corresponding to to the branch 1 m in t ′ . Formally, for all i ∈ [0, m], a tree t i such that

t i ≡ t ′ i and t is the prefix closure of i∈[0,m-1] w 1 • • • w i • (1 -w i+1 ) • t i . Hence r(Fr(t)) = max{r(Fr(t i )) | i ∈ [0, m]} by Proposition 2.2.8 and rCB (t) = max{r CB (t i ) | i ∈ [0, m]}
because the subtree permutation commutes with rCB .

For all i ∈ [0, m], WF(t i ) < β, but by Proposition 2.2.8 again, there is an i max such that r(t imax ) = r(β). So we have by induction hypothesis that rCB (t imax ) = r(Fr(t imax ))+δ. This shows that rCB (t) = r(Fr(t)) + δ.

1 ω is an infinite branch in t ′ . For all i ≥ 0, let t ′ i be the subtree of t ′ rooted at 1 i 0. The frontier of t ′ is equal to i≥0 Fr(t ′ i ). As t ′ is full, Fr(t ′ i ) = 0 for all i ≥ 0. Hence for all i ≥ 0, Fr(t ′ i ) < Fr(t ′ ) = β. By definition of ≡, there exists an infinite branch w = w 1 . . . w m . . . ∈ {0, 1} ω and for all i ≥ 0, a tree t i such that

t i ≡ t ′ i and t = i≥0 w 1 • • • w i • (1 -w i+1 ) • t i . Hence r(Fr(t)) = i∈W Fr(t i ) where W designates the order N ordered by i ≺ j iff w 1 . . . w i .(1 -w i ) < lex w 1 . . . w j .(1 -w j ).
In particular, W has order type

ω + k for some k < ω iff w is ultimately 1 ω k + ω * for some k < ω iff w is ultimately 0 ω ω + ω * otherwise.
Assume that the type of W is ω + ω * ; the proof is only simpler for other types. By Remark 2.2.10, I = {i | r(Fr(t i )) = β} is finite.

• If β = α + 1, note that β < ω ⇐⇒ α < ω. By induction, for j / ∈ I, ∂ α+δ (t j ) is finite. If I = ∅, ∂ β+δ (t)
is reduced to the tree bearing the ∂ β+δ (t i ) for i ∈ I, which are finite. If I is empty, ∂ α+δ (t) has exactly one infinite branch. So rCB (t) = β + δ.

• Otherwise, β is limit and β ≥ ω. If I is empty, for α < β there always infinitely many j / ∈ I such that α ≤ rCB (t j ) < β. So ∂ α (t) always contains the infinite branch w. Otherwise, for i ∈ I, by induction ∂ β (t i ) is infinite. So ∂ β (t) has always at least one infinite branch. For all i ∈ I, ∂ β+1 (t i ) is finite and so is ∂ β+1 (t).

As an unrelated note, we may use the same proof technique to prove the equivalence between different orders on a prefix tame tree. Proposition 4.4.8. For every full binary prefix tame tree t, r(Fr(t)) = r(KB(t)) = r( Dom(t), < lex ).

Proof. We note Lex(t) = Dom(t), < lex . Let again WF(t) be the smallest ordinal α such that there exists a well-ordered tree t ′ with t ≡ t ′ and Fr(t ′ ) = α. We prove the result by induction on WF(t). If WF(t) = 1, since the tree is prefix, it is reduced to a single node and then Fr(t) = KB(t) = Lex(t) = 1.

In the general case, it depends again whether t ′ has an infinite branch 1 ω or not. The t i and t ′ i trees are defined in the same way that in the previous proof; since t ′ i ≡ t i and Fr(t ′ i ) < Fr(t), we may apply the induction hypothesis r(Fr(t i )) = r(KB(t i )) = r( Dom(t i ), < lex ).

Fr(t) = Fr(t 2 ) + Fr(t 4 ) + • • • + Fr(t 3 ) + Fr(t 1 ), KB(t) = KB(t 2 ) + KB(t 4 ) + • • • + 1 + KB(t 3 ) + 2 + KB(t 1 ) + 1, Lex(t) = 2 + Lex(t 2 ) + 2 + Lex(t 4 ) + • • • + Lex(t 3 ) + Lex(t 1 ).
When 1 ω is not an infinite branch in t ′ , it is the successor case. Then Fr(t) = k i=1 Fr(t i ), whereas KB(t) and Lex(t) have the same form

KB(t) = k i=1 (KB(t i ) + c i ) Lex(t) = k i=1 (c ′ i + Lex(t i ))
where c i , c ′ i are integers. We may then apply Proposition 2.2.8 as before to get the result. The limit case is when 1 ω is an infinite branch in t ′ . Now Fr(t) = i∈W Fr(t i ) where W has order type ω + ω * , ω + k or k + ω * . Then we have the same

KB(t) = i∈W (KB(t i ) + c i ) Lex(t) = i∈W (c i + Lex(t i ))
as illustrated in Figure 4.4. The Proposition 2.2.8 along with Remark 2.2.10 leads to the main result.

Obviously, the property fails for the actual Hausdorff rank, since a full prefix tree of frontier ω has a KB-order ω + ω * , which has Hausdorff rank 2 but ∼-rank 1.

It would be interesting to capture all the orders on a tame tree which share the ∼-rank. It may be conjectured that all orders MSO-definable on Dom(t) have the same ∼-rank; however this does not include Fr(t), which concerns only leaves. This raises the more general conjecture.

Conjecture 4.4.9. Let t be a tame tree. All orders definable by a monadic formula such that any vertex is prefix of a vertex selected by the formula have the same ∼-rank.

Remark 4.4.10. The proof of Theorem 7.7 in [START_REF] Khoussainov | Automatic linear orders and trees[END_REF] states that rCB (t) = r(KB(t)), which seems to contradict Proposition 4.4.7. In fact this is true for finite rCB , which is enough to prove the said Theorem, but false for further ordinals. Consider the following counterexample. We define the family (t α ) α≤ω of prefix trees by the following set of leaves.

Leaves(t 1 ) = 1 * 0 Leaves(t 2 ) = 1 * 0 • Leaves(t 1 ) . . . Leaves(t i ) = 1 * 0 • Leaves(t i-1 ) . . . Leaves(t ω ) = i∈N 1 i 0 • Leaves(t i ) We prove that rCB (t ω ) = r(KB(t ω )) + 1. For each i > 1, KB(t i+1 ) = KB(t i ).ω + ω * . In particular since KB(t 1 ) = ω + ω * , for i > 1, by induction KB(t i ) = ω + ζ.ω i-1 + ω * . KB(t ω ) = i≥0 KB(t i ) + ω * = ω + ζ.ω ω + ω *
By another induction, it is easy to see that rCB (t i ) = i. For each j ∈ N and i > j, ∂ j (t i ) is infinite. So in ∂ j (t ω ) there is infinitely many infinite branches. In particular the branch 1 ω is in each ∂ j (t ω ) and therefore in ∂ ω (t ω ). To sum up,

KB(t) r(KB(t)) rCB (t) t 1 ω + ω * 1 1 t 2 ω + ζ.ω + ω * 2 2 t 3 ω + ζ.ω 2 + ω * 3 3 . . . t 3 ω + ζ.ω i-1 + ω * i i . . . t ω ω + ζ.ω ω + ω * ω ω + 1
Proposition 4.4.11. For any two prefix binary tame trees t and t ′ , if t ≡ t ′ then rCB (t) = rCB (t ′ ) and r(Fr(t)) = r(Fr(t ′ )).

Proof. Let t and t ′ be two tame binary trees s.t. t ≡ t ′ . Let h be a bijection from Dom(t) to Dom(t ′ ) which preserves the prefix relation. As h commutes with d, we have

∂ α (Dom(t ′ )) = h(∂ α (Dom(t)
)) for every ordinal α so rCB (t ′ ) = rCB (t). Prop. 4.4.7 implies that r(Fr(t)) = r(Fr(t ′ )).

As the definition of the CB-rank does not use the relative order between the sons of a node, it follows that two prefix deterministic trees having the same underlying unordered tree have frontiers of the same ∼-rank.

Finite combs

As foretold in Section 3.4.4, known examples of graphs separating the hierarchy include the prefix tree K f of well-chosen functions f : N → N, defined by Leaves(K f ) = {1 i 0 f (i) }. In particular, let the exp(m, n, i) operation be defined by exp(m, 0, i) = i exp(m, n + 1, i) = m exp(m,n,i) , then the tree K exp(2,3n,•) was shown in [START_REF] Blumensath | On the structure of graphs in the Caucal hierarchy[END_REF] not to belong to Graph n , using properties on the size of stacks of n-order-pushdown automata. It was then conjectured that already K exp(2,n,•) / ∈ Graph n . This section proves this result. More generally, we consider some comb-shaped graphs of the hierarchy, i.e. acyclic graphs with only one simple infinite path. We state a result of the maximal size of each subgraph not intersecting this path. The proof of this result is very related to the methods employed in Section 4.3.

Recall that a comb is a deterministic tree t over a ordered finite alphabet with a greatest label 1 such that the only infinite branch is 1 ω . In the hierarchy, an equivalent definition specializes this label. A #-comb is a comb on Σ ∪ {#} with a greatest label # / ∈ Σ such that each arc is labeled by # iff this arc is in the infinite branch of ω. The subtree of domain # i Σ * ∩ Dom(t) is noted t i . We alter slightly this definition to get more general graphs.

Definition. Let Σ be an alphabet and # / ∈ Σ another letter. A #-comb-graph over Σ is a deterministic graph G of labels Σ ∪ {#} with a root r and the following properties. Let

V i = {x | r # i Σ *
---→ x} and G i the subgraph of support V i :

• the subset of arcs labeled by # form an infinite path from r;

• for all i, G i is an acyclic graph;

• the only arc between V i and V j =i can be #.

The goal of this section is to get a upper bound for each |V i | when G is a comb-graph of the hierarchy. This is the Theorem 4.5.3.

We first remark that comb-graphs of Graph n cannot be larger than combs of Tree n .

Lemma 4.5.1. If G ∈ Graph n is a #-comb-graph, there is a comb t ∈ Tree n such that for all i, there is a j ≤ i such that

|V i | ≤ |Dom(t j )|.
Proof. Let G be a #-comb-graph of support V . Since each G i is a finite deterministic acyclic graph, there is a MSO-definable order < on V i -for instance, lexicographic order. This order can be extended to V with x < y iff x ∈ G i , y ∈ G j and i < j ∨ (i = j ∧ x < y). So there is an interpretation from G to the ω-word w = i≥0 (ab |V i | ) : each x ∈ V i is colored in a when it is the smallest of V i , and b otherwise.

By Corollary 4.2.7, there is a full binary prefix tree t in Tree n (on the alphabet {0, 1}) with only one infinite branch 1 ω such that Fr(t) ≃ w.

For instance, t could be the following tree (the color c a is defined later on) : We may call t i the subtree of root 1 i 0, if any. The problem is that a subword ab |V i | may be "scattered" in several t j 1 , t j 2 , . . . . To get the required result, we are going to merge these subtrees.

We color each node 1 i with c a if a ∈ Fr(t i ). In particular, ε is colored. Let H ∈ Graph n-1 and s ∈ V H be such that Unf(H, s) is this marked tree. Let I(H) be the graph where there is a &-arc

x & → y when r 1 * -→ H x 1 + -→ H y, (c a , x), (c a , y) ∈ H,
and for all x

1 + -→ z 1 + -→ y, (c a , z) / ∈ H.
In Unf(I(H), s), we remove the subtrees with root & i u such that 1. there is no a-leaf & i v with v ≤ lex u, 2. or there are at least one a-leaf & i 1v such that 1v < lex u or v ∈ u0 * .

We note t i the subtree of domain & i (0 + 1) * . Condition 1 checks that each such subtree begins with an a. Condition 2 looks for the first a-leaf in & i 1(0+1) * and removes subtrees of root greater or equal in lexicographic order. We note t ′ this new tree. Following our previous example, t ′ is shown below. In short, t ′ is a &-comb having the same frontier than t, and such that for each i, Fr(t ′ i ) begins with the letter a. So each ab |G i | is contained in some Fr(t ′ j ), which shows the result.

If n ≥ 1, for any t ∈ Tree n there is a graph H in Graph n-1 and s ∈ V H such that t = Unf(H, s). As usual, we suppose that s is a root of H. • Either S is finite, and then the sequence (t i ) i≥0 is ultimately periodic;

• or S is an infinite path from s.

Proof. Recall that t and H are deterministic. Since there is a infinite path labeled by # in t, there is a infinite or ultimately periodic path labeled by # in H, starting from s.

In particular, for n = 1, H is a finite graph, so the set S is necessarily finite, and the sequence (|Dom(t i )|) i≥0 is bounded. By Lemma 4.5.1, so are the (|V i |) i≥0 .

For further levels, the following result states that the bound is n-exponential in the length of the comb. For a finite tree t, let depth(t) be the maximal path size in t.

Theorem 4.5.3. For n > 0, let t be a #-comb of Tree n+1 and G a #-comb-graph of Graph n+1 . There is a constant C such that for all i,

depth(t i ) ≤ exp(2, n -1, C(i + 1)), |V i | ≤ exp(2, n, C(i + 1)).
Proof. Let t be a #-comb over Σ, and H and s as in Lemma 4.5.2. By Lemma 4.5.1, the result on G is a direct consequence of the result on t. Indeed, since t i is a finite deterministic Σ-tree, then |Dom(t i )| ≤ |Σ| depth(t i ) . So there is a constant

C ′ such that |Dom(t i )| ≤ exp(2, n, C ′ (i + 1)).
First note that deterministic structures of Tree 1 and Graph 1 are regular. Following notations in [START_REF] Muller | The theory of ends, pushdown automata, and second-order logic[END_REF] and Section 2.5, they have therefore finitely many end-isomorphisms, which means that for any #-comb t in Tree 1 , the sequence (|Dom(t i )|) i≥0 is bounded. A similar result applies to #-comb-graphs.

In H, for i ≥ 0, let s i be the vertex such that s

# i -→ H s i . By Lemma 4.5.2, if {s i } i≥0
is finite, the result is trivial. Suppose otherwise. We call the #-level ℓ # (x) of a vertex x ∈ V H the least i such that s i

Σ * -→ x. Let V H i = {x | ℓ # (x) = i}
and H i be the associated subgraph.

The transformation I removing Σ-arcs between any V H i and V H j =i is a monadic interpretation. Moreover, we now that there is exactly one infinite branch in t, so there cannot be any infinite branch in any Unf(H i , s i ), which means each H i is finite and acyclic. So

I(H) is a #-comb-graph of Graph n-1 . A path in t i is smaller than j≤i |V H j |. • If n=2, then |V H i | is bounded by some C, so depth(t i ) ≤ i≤ℓ # (x) |V H j | ≤ C.i. • Otherwise, by induction |V H j | ≤ exp(2, n -1, C(i + 1)) and depth(t i ) ≤ i≤ℓ # (x) |V H j | ≤ exp(2, n -1, C(ℓ # (x) + 2)).
Chapter 5

Schemes and morphic words

In the previous chapter, we left aside the question of the coloring of orders. The first class of colored infinite graphs that comes to the mind are the infinite words, or orders of type ω. Even for such simple objects, we do not know precisely which of them inhabit the pushdown hierarchy. The aim of this chapter is to open the way to a characterization of infinite words of the hierarchy. At the first level, they are well-known.

Proposition 5.0.4. The ω-words of Graph 1 are the ultimately periodic words.

Proof. For any colored ω-order, it is easy to see that the corresponding colored infinite path is also in Graph 1 . This a regular graph, and has therefore finitely end-isomorphisms (see Section 2.5) starting from the root. It follows that there are two isomorphic enddecompositions at step n and m so the structure is ultimately periodic with period |m -n|.

We turn our attention on the next levels, namely Graph 2 and Graph 3 . A direct consequence of [START_REF] Caucal | On infinite terms having a decidable monadic theory[END_REF]Prop. 3.2] is that infinite words well-known as morphic words belong to Graph 2 . For the other direction, by Corollary 5.1.6 we only need to consider the frontier of trees solutions of order-1 schemes whose frontier is of order type ω. Moreover, by Proposition 4.2.1, such a tree can be chosen binary, prefix and full. This tree has therefore exactly one infinite branch, which is 1 ω . As mentioned in the introduction, deterministic trees of Tree 2 can be described by the notion of recursion schemes. We may therefore plug the constrained shape of our trees into this setting to get the characterization of words.

For a slightly more powerful result, we notice that if the frontier of a deterministic tree has an initial segment of type ω, then this segment can be interpreted by an MSO-formula. If we are in the pushdown hierarchy, we can therefore find a correspond comb. For any deterministic tree, we call ω-frontier this initial segment when it exists.

Proposition 5.0.5. For any safe scheme admitting a ω-frontier w, there is a safe scheme of the same order generating a comb with frontier w.

Proof. If a deterministic tree in the pushdown hierachy has an ω-frontier w, then this order can be selected by a monadic interpretation. Indeed, consider the set of leaves by lexicographic order. Once the smallest leaf x 0 in lexicographic order has been found, the initial segment X 0 of underlying type ω is the smallest such that for all x ∈ X 0 and X ⊆ X 0 with x, x 0 ∈ X, x has an immediate predecessor in X.

So w is a word of the same level of the hierarchy. By Theorem 4.2.6, there is therefore a comb in the class of trees of the same level were each node has degree 0 and 2, with frontier w. This means that there is a safe scheme generating this comb.

If words of Graph 2 are morphic words, extending the method to the next level would hopefully bring a natural extension. Since morphic words are well-known, this is not the first attempt for such a generalisation. Already [START_REF] Carton | The monadic theory of morphic infinite words and generalizations[END_REF] proposes more general predicates in the framework of decidable monadic theory. Some more recent propositions tweak an automatic presentation of morphic words, for instance allow the automaton to be infinite [lG06] or generalize the underlying order [START_REF] Bárány | A hierarchy of automatic ω-words having a decidable MSO theory[END_REF]. Another direction is more pushdownautomaton related [START_REF] Fratani | Iterated pushdown automata and sequences of rational numbers[END_REF][START_REF] Marin | Suites de mots et automates[END_REF] and relates to the HDT0L definition of morphic words (see [START_REF] Allouche | Automatic Sequences[END_REF] for details). This rest of this chapter is organized as follows. We first present recursion schemes and their relationship with the hierarchy. Then, we define morphic words and that frontiers of type ω of order-1 recursion schemes are exactly morphic words. Then we extend this proof to so-called hyperalgebraic trees, i.e. trees of Tree 3 . We first introduce the notion of order-2 morphic words, and prove that they correspond exactly to ω-frontiers of order-2 recursion schemes. We therefore obtain a characterization of the ω-words of Graph 3 .

Recursion schemes

We first give a definition of recursion schemes, then recall why schemes with the safety constraint are term trees of the hierarchy.

Definition

We borrow the definitions from [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF]. The notion of recursion scheme, or term grammar , gives a direct presentation of infinite tree by successive rewriting of terms.

Types and terms

First of all, these terms are constrained by their type; the first definition therefore concerns these objects. The set of types T is built from a unique basic type o and the binary operator →.

τ := o | τ 1 → τ 2
The operator → is associative to the right. The order or level ℓ(τ ) of a type is defined by ℓ(o) = 0 and ℓ(τ

1 → τ 2 ) = max(1 + ℓ(τ 1 ), ℓ(τ 2 )). A type τ 1 → . . . → τ n → o is homogeneous if ℓ(τ 1 ) ≥ • • • ≥ ℓ(τ n ). The type o → . . . → o → o with n + 1 times o is written o n → o.
A typed alphabet is a set Γ of symbols with types in T . We note f : τ when f ∈ Γ is of type τ . By notation, ℓ(f ) = ℓ(τ ), and the order of the alphabet is ℓ(Γ) = max f ∈Γ ℓ(f ). The set of applicative terms AT(Γ) is defined by Γ ⊆ AT(Γ) and if f : τ 1 → τ 2 and x : τ 1 , then (f x) : τ 2 ∈ AT(Γ). We say then that x an operand of f . By mirroring type association, applicative terms are associative to the left : f xy = (f x)y. A term is an applicative term of type o; the set of terms is noted T(Γ). The arity ρ of a term is 0, and ρ(f ) = ρ(f x) + 1 otherwise. An applicative subterm is an occurence of some t = f x 1 . . . x n where n is maximum for this occurence; it is a subterm if n = ρ(f ).

Recursion schemes

We are now ready to define the base rules of recursion schemes. Let X be a typed alphabet of variables. We note t[x := t ′ ] with x : τ ∈ X the term where each occurence of the variable x is replaced by a applicative term t ′ : τ . A recursion scheme is a tuple S = (Σ, N, S, E) where Σ is a finite typed 1-order alphabet of (lowercase) terminals, N is a finite typed alphabet of (uppercase) nonterminals, S : o ∈ N is the starting nonterminal and E is a set of productions in bijection with N , of the form F x 1 . . . x ρ(F ) ⇒ w F where F : τ 1 → . . . → τ ρ(F ) → o ∈ N ; for all i, x i : τ i ∈ X and w F is a term in T(Σ ∪ N ∪ {x 1 , . . . , x ρ(F ) }). The order of the scheme is ℓ(S) = ℓ(N ). The set of all n-order schemes is noted S n .

To each scheme S is associated a rewriting relation =⇒ S ⊆ T(Σ∪X ∪N ) 2 . Informally, a subterm which head is a nonterminal F is replaced by its related term w F where variables are in turn replaced by the actual arguments of F . In practice,

• F t 1 . . . t ρ(F ) =⇒ S w F [∀i, x i := t i ]
if there is a production F x 1 . . . x ρ(F ) ⇒ w F in E with x i : τ i and t i : τ i for all i.

• t =⇒ S t ′ , then (st) =⇒ S (st ′ ) and (ts) =⇒ S (t ′ s) whenever the applicative terms exist.

Limit trees

The definition of schemes yet only produces finite terms. To reach infinity, we need the notion of limit tree. This limit in turn demands to build a converging family of trees. The approximation t ⊥ of a term t on Σ ∪ X ∪ N is the term on Σ ∪ {⊥} where nonterminals have been pruned, that is

• if t = f t 1 . . . t ρ(f ) with f ∈ Σ ∪ X, t ⊥ = f t ⊥ 1 . . . t ⊥ ρ(f ) , • if t = F t 1 . . . t ρ(F ) with F ∈ N , then t ⊥ = ⊥.
Let π be a projection from terms on Σ ∪ {⊥} ∪ X to (finite) trees, where each subterm f x 1 . . . x ρ(f ) is mapped to a subtree δ with root r, arcs r i → π(x i ), and color δ(r) = f . An approximation partial ordering can be defined on trees by δ ′ ⊑ δ if Dom(δ ′ ) ⊆ Dom(δ) and, for each w ∈ Dom(δ ′ ), δ ′ (w) = δ(w) or δ ′ (w) = ⊥. Successive approximations are ordered by this ordering : for two terms t 1 =⇒ S t 2 , we have π(t ⊥ 1 ) ⊑ π(t ⊥ 2 ). The scheme is a confluent grammar, so each term t on Σ ∪ N ∪ X generates a unique tree

t = sup{π(s ⊥ ) | t =⇒ S s}.
For any scheme S = (Σ, N, S, E), we note S = S the limit tree of the scheme.

Example 5.1.2. Theorem 3.1.2 and Corollary 5.1.6 state that any ordinal smaller than ω ↑↑ n + 2 is the frontier of a n-order scheme. We show schemes corresponding to the successive towers of ω.

A tree yielding ω is simply given by the 0-order scheme

S 0 = ({f, a}, {S 0 }, S 0 , {S 0 ⇒ f (a, S 0 )}).
At the next level, a tree yielding ω ω is given by S 1 = ({f, a}, {S 1 , F 1 , G 1 }, S 1 , E 1 ) where E 1 is shown in Figure 5.1. Informally, the nonterminal F adds complexity whereas G propagates it. Recursively, a tree yielding ω ↑↑ n is S n = ({f, a}, {S n , F n , G 1 , . . . , G n }, S n , E n ) with E n defined in Figure 5.2.

Here the types used are

τ 1 = o, for n > 1, τ n = τ n-1 → . . . → τ 1 → o
and for all n > 0, x n : τ n and F n , G n : τ n+1 .

Schemes in the pushdown hierarchy

A scheme is safe if for any production rule F x 1 . . . x n ⇒ w F , and for any applicative subterm t of w F , there is no occurence of some x i in t with ℓ(x i ) < ℓ(t). The set of order-n safe schemes is noted S safe n . Note that for n < 2, safety is not a restriction. The safety has been previously called the derived types property [START_REF] Damm | The IO-and OI-hierarchies[END_REF].

Example 5.1.3. From [KNU02], the scheme with production rule S ⇒ F (g, a, b) F (ϕ, x, y) ⇒ f (F (F (ϕ, x), y, h(y)), f (ϕ(y), x))

S 1 =⇒ F 1 a F 1 x =⇒ f x F 1 G 1 x G 1 x =⇒ f x G 1 x S 1 = f a f f a f a . . . f f f a f a . . .
S n =⇒ F n G n-1 . . . G 1 a F n x n . . . x 1 =⇒ f x n x n-1 . . . x 1 F n G n x n x n-1 . . . x 1 G n x n . . . x 1 =⇒ f x n x n-1 . . . x 1 G n x n x n x n-1
x n-2 . . . is unsafe, because there is a subterm F (ϕ, x) such that ℓ(x) < ℓ(F (ϕ, x)). It is conjectured that this scheme produces a tree which cannot be produced by any safe scheme.

The question whether safe schemes produce the same trees than unsafe schemes has been recently solved by the negative using a language defined by Urzyczyn. For more details, see [START_REF] Pawe L Parys | Collapse operation increases expressive power of deterministic higher order pushdown automata[END_REF] and [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF]Prop. 7.13].

Definition. A term tree is a deterministic tree t colored by an alphabet Σ and labeled by [1, k] where k is the maximum out-degree, and the following constraints :

• if u • i ∈ Dom(t), then i = 1 or u • (i -1) ∈ Dom(t);
• all nodes with the same color f have the same out-degree.

The relationship between schemes and the pushdown hierarchy is that trees generated by safe schemes of order n are exactly term trees on the level n + 1 of the hierarchy. This is an application of [Cau02, Theorem 3.5].

Proposition 5.1.4. Limit trees of safe schemes of order n are term trees of Tree n+1 up to isomorphism.

Proof. Let h be a rational mapping as defined in Section 2.4.1 with the following constraints. Suppose that such that for each a, h(a) is recognized by a finite deterministic automaton (S, i, T, η) where

• each final state (in T ) is terminal, i.e. has no output arcs;

• for all q ∈ S, each set P = {q | q c → p ∧ c ∈ Γ} is such that if q ∈ P and q → p then p / ∈ P ;

• it is strongly deterministic on arc labels : if q c → p, q d → p ′ and a ∈ Σ, then c = d. In other words, the disjonctions are made on colors. Such a mapping is called deterministic rational mapping. The set of all these mappings is called DRat.

Theorem 5.1.5 ([Cau02]). For n > 0, S safe n+1 = Unf • DRat -1 ( S safe n ).
At the first level, the recoloring of S 0 are regular trees. To get Prop. 5.1.4, it it enough to show that deterministic trees of Tree n+1 are the image of Tree n under the mapping Unf • DRat -1 , and more precisely that each deterministic graph of Graph n is h -1 (t) for some deterministic t ∈ Tree n and h ∈ DRat.

Let G ∈ Graph n . By Prop. 4.1.2, there is a deterministic tree t ∈ Tree n of color set Γ, a family of simple TWA {A a } a∈Σ and a recoloring µ such that G = µ(A(t)). We build h ∈ DRat such that G = h -1 (t). For a ∈ Σ, let A a = (Q, q 0 , µ F , δ) be the automaton recognizing h(a) and let A = (S, i, T, η).

S = Q ∪ (Q × P(Γ)) i = q 0 T = (q, c) such that q ∈ µ F (c) η(q, c) = (q, c)
for each q ∈ Q, c ∈ P(Γ) ∀a ∈ Σ, η((q, c), ā) = p for each δ(q, c) = (p, ↑) η((q, c), a) = p for each δ(q, c) = (p, a)

Each final state is terminal, since δ(q, c) = ∅ if q ∈ µ F (c). Each P(Γ)-transition is either a final state or followed by a Σ-transition. The determinism condition is also fulfilled : if η((q, c), a) = (p, 0) and η((q, c), b) = (p, 0), then (p, a), (p, b) ∈ δ(q, c), and since A a is deterministic, a = b.

For recoloring, we simply set h(c) = µ(c) for each c ∈ P(Γ).

It is easy to tranform any deterministic tree into a term tree with the same frontier. This remark allows the following corollary of Theorem 4.2.6.

Corollary 5.1.6. A linear order colored by Γ is in Graph n if and only if it is the colored frontier of some tree limit of a safe recursion scheme of order (n -1) with one terminal f of arity 2 and terminal of arity 0 for each c ∈ Γ.

Morphic words

Morphic words are well-known ω-words. They can be seen as a generalisation of automatic sequences, but we prefer to skip this latter definition and give the direct presentation. For a complete introduction, see [START_REF] Allouche | Automatic Sequences[END_REF].

In this section, after the preliminaries we present a construction of the morphic words in the hierarchy. Then we prove that morphic words are the only possible words of Graph 2 by looking at leaves of trees produced by recursion schemes.

Definition and properties

Let Σ be an alphabet. A morphism on Σ * w.r.t. concatenation is a mapping τ such that τ (ab) = τ (a)τ (b). Now let τ : Σ → Σ * a morphism. Suppose there is a letter ∆ ∈ Σ such that the first letter of τ (∆) is ∆. In this case the following sequence admits a limit : Let σ : Σ → Γ be another morphism. The set of morphic words are the words in the form σ(τ ω (∆))).

τ (∆) = ∆ • u τ 2 (∆) = ∆ • u • τ (u) . . . τ ω (∆) = ∆ • u • τ (u) • τ 2 (u) • . . .
Example 5.2.1. The regular paperfolding sequence (see [AS03, Ex. 5.1.6]), or dragon curve sequence, is obtained by folding iteratively a piece of paper in the same direction. By unfolding the paper and looking at the direction of the corners, we get a word on two letters. For n foldings, we get the n th word of the following sequence; see Figure 5 We can chose σ to have a specific form. A coding is a morphism σ such that for all a, |σ(a)| = 1.

Theorem 5.2.2 ([AS03]

). If f, g are two morphisms such that g(f ω (a)) exists, then there is a letter ∆, a non-erasing morphism τ such that τ (∆) begins with ∆, and a coding σ such that g(f ω (a)) = σ(τ ω (∆)).

We are particularly interested by the logical properties of morphic words. The following result was obtained in [START_REF] Carton | The monadic theory of morphic infinite words and generalizations[END_REF] for even larger sets of ω-words.

Theorem 5.2.3 ([CT02]

). The monadic theory of a morphic word is decidable.

As with uncolored ordinals, this result naturally rises the question : which morphic words are in the hierarchy? The following sections answers that they are in fact exactly words of Graph 2 .

Construction in the pushdown hierarchy

The goal of this section is to prove that words of Graph 2 are exactly the morphic words. We begin with the easy direction. It is proved in [START_REF] Caucal | On infinite terms having a decidable monadic theory[END_REF] that morphic words are terms of Tree 3 . If it is not ultimately periodic, such a tree must be unfolded from itself, so morphic words are in Graph 2 . Theorem 5.2.4. Any morphic word is in Graph 2 .

Proof. We reproduce here a proof by Caucal. Any morphic word can be chosen of the form σ(τ ω (∆)) with τ be a morphism on an alphabet Σ with τ (∆) ∈ ∆Σ * , and σ a coding Σ → Γ.

Let n = max a∈Σ (|τ (a)|) + 1. We build the following regular graph of support N ∪ (N × Σ) ∪ Γ, label set [1, n] and colors Γ.

G = {k n → k + 1} ∪ {k i → (k, τ (∆) i ) | k > 0, i > 1} ∪{(k, x) i → (k -1, τ (x) i ) | k > 1, x ∈ Σ, i > 0} ∪{(1, x) 1 → σ(x) | x ∈ Σ} ∪ {0 1 → (0, ∆), (0, ∆) 1 → σ(∆)} ∪{(y, y) | y ∈ Γ}
G is a regular graph, so G ∈ Graph 1 . Let t = Unf(G, 0). By induction, for k > 0, each subtree of root n k i yields the finite word σ(τ k-1 (τ (∆) i )). The leaves of t in lexicographic order form the required morphic word. There is therefore a monadic interpretation building the word from t.

Example 5.2.5. For instance, the word abaabaaaab . . . is obtained by This result implies of course Theorem 5.2.3.

τ (∆) = ∆baa σ(∆) = a τ (a) = aa σ(a) = a τ (b) = b σ(b) = b So Σ = {∆,

Words in Graph 2 are morphic, direct proof

The converse of Theorem 5.2.4 can be obtained by using methods similar to those used in Chapter 4. We follow here this direction. But it is limited to the first level of the hierarchy, so the rest of this chapter will be devoted to an alternative and extensible proof using recursion schemes.

a b 0, ∆ 1 1, a 1 1, b 1 2, a 1 2 2, b 1 . . .
Theorem 5.2.6. ω-words of Graph 2 are morphic words.

To prove this result, we show that a tree having a frontier of type ω is unfolded from a graph having the shape of the graph of Example 5.2.5.

Let w be an ω-word on Γ of Graph 2 . According to Theorem 4.2.6, we consider a prefix full Σ, Γ-tree of Tree 2 which has frontier w. Let t w be this tree. One more step backwards, let G ∈ Graph 1 and r ∈ V G be such that t = Unf(G, r). We may suppose that G is accessible from r. There is only one infinite path from r in G.

Moreover, since G is a deterministic graph, we know by [START_REF] Caucal | An internal presentation of regular graphs by prefix-recognizable graphs[END_REF] that G is in fact a regular graph1 . We actually ignore this property to reach the result, and we prefer to follow the hierarchy backwards one more time : G is it interpreted from a tree t ∈ Tree 1 .

Lemma 5.2.7. There is a MSO-interpretation I and a deterministic regular tree t ∈ Tree 1 such that G = I(t) and t has only one infinite branch.

Proof. Instead of a MSO-interpretation we know that we may chose a TWA-interpretation A = {A a } a∈Σ as described in Remark 4.1.4. There is a regular tree t in Tree 1 such that G is A(t) up to a color projection. As usual, we may suppose that t is the prefix closure of V G . Let (r i ) i≥0 be the infinite path from r, and t r the restriction of t to the prefix closure of {r i } i≥0 . Suppose there are two infinite branches in t r , with greatest common node z. Then there are infinitely many runs r As in Section 4.5, we may note V i the subset of V G such that any path from r to this subset goes through r i , but not necessarily through r i+1 . Each V i is a finite set. Suppose there is another infinite branch B ′ and let b = B ∧ B ′ . Since the tree is deterministic and the V i are finite, there are infinitely many i ∈ N such that r i is supported by B and some vertex z i in V i is supported by B ′ . Since there is a path from r i to z i , we can consider the precise pair (x i , y i such that r

U V 0 V 1 V 2 . . . y x 0 w ′ x 1 w ′ x 1 w x 2 w
i -→ G x i a -→ G y i -→ G z i and |x i ∧ B| > |b| and |y i ∧ B ′ | > |b|.
Since t is deterministic and the pairs (x i , y i ) are pairwise distinct, for all N there is a i > 0 and a ∈ Σ such that there are infinitely many x i a -→ G y i and

|x i ∧ B| -|b| > N |y i ∧ B ′ | -|b| > N.
By applying the same argument than above, we see that there are i = j such that there is also a run of A a from x i to y j , which contradicts the determinism of G.

So t is a regular tree with one infinite branch. This means that it is periodic in the sense that there are two words u, v with sufficiently large u such that if t(uw) = c for some w, then t(uv k w) = c for all k ≥ 0. Indeed, if d M S is the graph decomposition in the sense of [START_REF] Muller | The theory of ends, pushdown automata, and second-order logic[END_REF] (see Section 2.5), then there are n u , n v such that d

(nu+nv) M S (t) = d (nu)
M S (t). We may then chose u to be the prefix of size n u of the branch and v the following factor of size n v .

For any w such that v ⊑ w, we note this vertex x k w = uv k w. For a given k, there are only finitely many such vertices. Let

V k = V G ∩ {x k w | w ∈ Σ * } for k > 0 and U = V G \ k≥0 V k .
These sets are all finite. We also note G U the subgraph of support U , V ≤k = U ∪ i≤k V i and G ≤k the subgraph of support V ≤k . The following technical lemma is illustrated in Figure 5.5. Lemma 5.2.8. There is a choice of u, v such that if k ≥ 1 and

x k w a -→ G y, then • either y ∈ U then x k+1 w a -→ G y, • or y ∈ V k-1 ∪ V k ∪ V k+1 so y = x k ′ w ′ and x k+1 w a -→ G x k ′ +1 w ′ .
Proof. Suppose y ∈ V G \ U and note y = x k ′ w ′ . There is a run of A a from x k w to x k ′ w ′ . This run goes by x k ′ w ′ ∧ B which is of the form x k ′ z with z ⊑ v. By the regularity of the tree, there is also a run from x k+1 w to x k ′ +1 w ′ . Consider the set of h ∈ N such that the run of A a from x k w to x k ′ w ′ goes by x h z . If |k ′ -k| is not bounded, then this set is larger than the set of states of A a ; so there are h = h ′ such that A a has the same state on x h ′ z and x h z . Suppose w.l.o.g. that k

′ ≤ h ′ < h ≤ k. Then there is a run of A a from x k+h-h ′ w to x k ′ w ′ , but also from x k+h-h ′ w to x k ′ +h-h ′ w ′
. This contradicts the determinism of G. So |k ′ -k| is bounded by a constant depending on A a , and there is therefore a choice of v such that whenever

x k w → x k ′ w ′ then k ′ ∈ [k -1, k + 1]
. Suppose now that y ∈ U and k is large. We use again the regularity of t on a sufficiently long run of A a : there is a p w,y such that for all i ≥ 0 x The graph G being deterministic, the second part of this lemma can also be read backwards up to a good choice of

v : if x k+1 w a -→ G x k ′ +1 w ′ , then x k w a -→ G x k ′ w ′ .
Let P be the sequence of vertices of the infinite path in G starting from r. Let x 1 p 1 be the first vertex of P in V 1 . By the previous lemma, x 2 p 1 also belongs to P . Up to a good choice of u, v, the subsequence (x 1 p 1 , . . . , x 2 p 1 ) is all in V G \ V ≤0 . Let S 1 be this subsequence without the last x 2 p 1 . Let G x k w be the graph restricted to (V G \ P ) ∪ {x k w }. For any x k w ∈ V k , we note Fr(x k w ) = Fr(Unf(G x k w , x k w )), i.e. the finite frontier obtained without following the infinite path. This notion can be expressed recursively. Formally, let X = {x w | x 0 w ∈ V 0 } be a new alphabet. By the previous lemma and the fact that G ≤k is an acyclic graph, there is a word s w over Γ ∪ X such that for all k ≥ 1,

Fr(x k w ) = s w [x w ′ := Fr(x k-1 w ′ )].
This allows the definition of the morphic word. The alphabet is X ∪ Γ, and τ and σ are idempotent on Γ.

τ (∆) = ∆. x∈S x σ(∆) = Fr(Unf(G ≤0 , r)) for any w, τ (x w ) = s w σ(x w ) = Fr(x 1 w )

Words in Graph 2 are morphic, by recursion schemes

We prove again Theorem 5.2.6, i.e. that words of Graph 2 are necessarily morphic words, this time using recursion schemes. A first attempt of this proof appears in [START_REF] Lavergne | Prédicats algébriques d'entiers[END_REF]. We show that the morphic word σ(τ ω (∆)) is indeed Fr(S). The scheme is simple recursive, which means that for each i, there is a unique term w i such that F x 1 . . . x n =⇒ S i w i .

S =⇒ F a F x =⇒ f x f b F f x x S = f a f b f f a a f b . . .
Fr(π(w ⊥ 0 )) = ⊥ Fr(π(w ⊥ 1 )) = u F • ⊥ Fr(π(w ⊥ 2 )) = u F • u F [∀k ≤ n, x k := Fr(π(t k ))] • ⊥ for i > 2, Fr(π(w ⊥ i )) = u F • Fr(π(w i-1 ))[∀k ≤ n, x k := Fr(π(t k ))] • ⊥
So for each i, τ (i) (∆).⊥ = ∆.Fr(π(w ⊥ i )). Moreover, replacing variables by terminal terms can permuted with approximation :

Fr(π(w i [∀k ≤ n, x k := s k ] ⊥ )) = Fr(π(w ⊥ i ))[∀k ≤ n, x k := Fr(π(s k )]
so the frontier of the (i + 1) th iteration of S is

u S • Fr(w i )[∀k ≤ n, x k := Fr(π(s k ))] = σ(τ (i) (∆)) • ⊥.
At the limit, since τ ω (∆) is infinite, it is exactly Fr( S ).

Example 5.2.12. Consider the scheme ({f, a, b}, {F, S}, S, E) where E is given in Figure 5.6. The frontier of its limit tree is the morphic word abaab . . . a 2 i b . . . already seen in Example 5.2.5. This scheme is simple recursive and u S = ε, u F = xb. We may hence deduce the following τ and σ.

τ (∆) = ∆xb τ (x) = xx τ (a) = σ(a) = a σ(∆) = ε σ(x) = a τ (b) = σ(b) = b

Second order

It is tempting to try and improve the method used in Section 5.2.4 in order to define an extension of the morphic words which would match exactly the words of any level of the hierarchy. In reality, higher-order schemes are not easily manipulated; in the rest of this chapter, we will only consider Graph 3 . For instance, we would like to express words like the Champernowne word described below, or the Liouville word of Section 5.3.3. These two examples both express some increase of complexity compared to morphic words, respectively in terms of subword complexity and growth.

The Champernowne word [Cha33] (or constant) is the concatenation of numbers starting from 0 in some k-ary notation. Respectively in decimal and binary, it is 0123456789101112131415 . . . 0110111001011101111000 . . . For any base, these words belong to Graph 3 . To prove this fact, it is enough to find a second-order safe scheme yielding it. We present the binary case; other bases are similar. The scheme is S = ({f, 0, 1}, {S, F, G}, S, E) where E is presented in Figure 5.7.

Even if there is more than two nonterminals here, this presentation is very similar to the form of schemes corresponding to (order-1) morphic words : there is one starting nonterminal S and only one "recursive" nonterminal F . We define formally this linearization form for order-2 schemes in Subsection 5.3.2.

Second-order morphic words

We introduce the notion of a second-order morphic word, or 2-morphic word . Its definition mimics the notion of schemes : instead of letters, we use functions with operands.

Let ρ max ≥ 0 and Σ = ρmax i=0 Σ i where Σ i is a set of function symbols of arity i. The symbols of Σ 0 are called letters, and there must be at least one letter. On the opposite, Σ \ Σ 0 is noted Σ >0 .

A term word θ is defined by

θ := ε | a ∈ Σ 0 | f (θ, . . . , θ i ), f ∈ Σ i | θ • θ.
The set of term words on Σ is noted TW(Σ). We use the standard notation f (z) for an arbitrary long f (z 1 , . . . , z n ). Let V be a new set of letters called variables. We note Σ

i (z) the set {f (z) | f ∈ Σ i , z ∈ V i } and Σ(z) = ρmax i=0 Σ i (z). S =⇒ f 0 f 1 F f 1 G ϕ x =⇒ f ϕ f x 0 ϕ f x 1 F ϕ =⇒ f f ϕ 0 ϕ 1 F G ϕ S : o f : o → o → o F : (o → o) → o 0 : o G : (o → o) → o → o 1 : o S =⇒ S 2 f 0 f 1 f f f 1 0 f 1 1 F G f 1 =⇒ S 3 f 0 f 1 f f f 1 0 f 1 1 f f f f 1 f 0 0 f 1 f 0 1 f f 1 f 1 0 f 1 f 1 1 F G G f 1 Figure 5
.7: Order-2 safe scheme which frontier is the Champernowne word.

Let τ, σ be two morphisms on Σ(z) * w.r.t. concatenation.

for a ∈ Σ 0 , τ (a) ∈ TW(Σ) σ(a) ∈ TW(Σ 0 ) for f ∈ Σ >0 and z 1 , . . . , z n ∈ V, τ (f (z 1 , . . . , z n )) ∈ TW(Σ ∪ V) σ(f (z 1 , . . . , z n )) ∈ TW(Σ 0 ∪ V)
This definition is extended on term words by

for f ∈ Σ >0 and t 1 , . . . , t n ∈ TW(Σ), τ (f (t 1 , . . . , t n )) = τ (f (z 1 , . . . , z n ))[∀i, z i := τ (t i )] σ(f (t 1 , . . . , t n )) = σ(f (z 1 , . . . , z n ))[∀i, z i := σ(t i )]
A 2-morphic-word is any word of the form σ(τ ω (∆)), where ∆ is a letter in Σ such that τ (∆) ∈ ∆ • TW(Σ). If ρ max = 0, all symbols are letters and we land back on the classic definition of morphic words. The converse is even more noteworthy : in our examples, the letters are Let n = ρ(F ) and F : τ 1 → . . . → τ n → o. Suppose that i is a useless operand of F , then x i cannot appear in w, where w is any rewriting of a tree containing x i only in an occurrence of F x 1 . . . x ρ(F ) . As in the S 1 case, we can erase this operand, but at the cost of duplication of other nonterminals.

Formally, let ♦ : τ i be a new letter, and F ′ : τ 1 → . . . τ i-1 → τ i+1 → . . . → τ n → o a new nonterminal of the same type than F without the i-operand. Let w F ′ = w F [x i := ♦]. There are two disjoint cases depending on the order of x i .

• If ℓ(x i ) = 1, this case is similar to the first order. Since the scheme has order 2, each app. subterm of root F has an order at most 1; this means that this app. subterm appears as F t 1 . . . t k with k ≥ i. So each occurence of F can be replaced by F ′ where this i-operand is deleted.

• If ℓ(x i ) = 0, then there may be occurences of F without its i-operand in production rules of other nonterminals. In this case the app. subterm is an argument of another nonterminal H. For each nonterminal H : (o h 1 → o) → . . . → o, and each sequence s ∈ [0, h 1 ] ρ(H) , define the duplicate H s . Let (x i ) 1≤x≤ρ(H) be a family of variables where

-if s i = 0, then x i : o h i → o; -otherwise, x i : o h i -1 → o.
Then let H s x 1 . . . x ρ(H) ⇒ w Hs be a copy of w H where types are adjusted accordingly. Formally, if s i = 0, then each occurrence of x i is modified. If its app. subterm has at least s i operands, the s i -operand is erased. Otherwise, it has order 1, so it is the j-operand of an app. subterm of root K, which is changed into the correct duplicate K s ′ where s ′ j = s iρ(x j ). Each time F appears without its i-operand, it has order 1 and must appear as operand of some nonterminal H. So we can change F into F ′ and H into the appropriate H s .

Example 5.3.5. For instance, let

F : o → o ϕ : o → o G : o → o x : o H : (o → o) → o → o f : o → o → o
Suppose the rewriting rule for H is

H ϕ x ⇒ f ϕ x H F H G x
Suppose that the argument of F is revealed useless and has to be deleted. Since G does not change, this implies a duplication of the nonterminal H. Note that in the rule for H 1 , the type of ϕ ′ is now o.

H (1,0) ϕ ′ x ⇒ f ϕ ′ H (1,0) F H (0,0) G x H (0,0) ϕ x ⇒ f ϕ x H (1,0)
F H (0,0)

G x

As before, in the limit tree, this transformation can only change some subtrees into leaves labeled by ♦. But if it did, this means that there was a rewriting S =⇒ S ′ * w such that ♦ appears in w. By the definition of F ′ , this is contradictory with the fact that i is a useless argument of F . So the resulting tree is the same.

We iterate this process for all useless operands of all nonterminals. The number of possible different duplicates of nonterminals is finite, so the whole process is also finite. Among other differences between S 2 and S 1 , nonterminals generating finite trees cannot be avoided. Indeed, an applicative subterm which is not a term cannot be rewritten. To overcome this fact, it is enough to make a clear distinction between nonterminals generating finite or infinite trees.

A nonterminal G with production rule Gx 1 . . . x ρ(G) ⇒ w G is called semiterminal if w G does not contain any nonterminal or does contain only other semiterminals. As before, a nonterminal F is called infinite if F x 1 . . . x ρ(F ) is an infinite tree. "Infinite nonterminal" is shortened in ∞-nonterminal.

The following property shows that these two categories (semi-and ∞-nonterminal) are actually a partition of nonterminals. Later on, we will focus only on ∞-nonterminals to build 2-morphic words.

A subterm is called head applicative subterm whenever its root is nonterminal and it has no other nonterminal above. Since the schemes of this section have order 2, any head applicative subterm has order 0. Lemma 5.3.6. Let S = (Σ, N, S, E) be a scheme without nonproductive or useless nonterminals. A term on Σ ∪ N produces an infinite tree if and only if it contains a nonsemiterminal.

Proof. Let F be a non-semiterminal of arity n. Since F is productive, there is a w such that F x 1 . . . x n =⇒ S * w and the root of w is a terminal. Also, by definition, w contains at least one non-semiterminal nonterminal. Since the scheme has order 2, any head applicative subterm has order 0, so there is a head subterm. Since each nonterminal is useful, there is a sequence of rewriting bringing a head non-semiterminal. This nonterminal has all its operands and can be rewritten. By iterating the process, we build an infinite tree.

We prove now the opposite direction : a term only composed of terminals and semiterminals cannot be infinitely rewritten. We note sN the set of semiterminals. By definition, the graph over sN where F → G iff G is in w F is a acyclic graph. We can provide a (topological) ordering on semiterminals so that F → G ⇐⇒ F > G. This ordering can be extended on Σ ∪ sN with Σ < sN . Then we translate it to T(sN ∪ Σ) as follows.

For any app. subterm t, let root(t) be its root. We introduce the notion of lvl-1branches of a nonterminal subterm t : a lvl-1-branch is a multiset {root(t)} ∪ b where b is a lvl-1-branch of an app. subterm t i of level 1. We call lvl 1 (t) the multiset of lvl-1-branches of t.

For a term t, for any branch b of t we call val(b) the multiset of lvl 1 (t ′ ) for any app. subterm intersecting this branch. Finally, we call B(t) the multiset of val(b) for each branch of t. The values of app. subterms can be totally ordered by multiset ordering. Then {B(t) | t ∈ T (sN ∪ Σ)} is therefore totally ordered by multiset ordering.

We To this extent, we study the four cases above in order.

1. If t G intersects u, since t F and w are both of order 0, the rewriting does not affect lvl 1 (t G ).

2. By definition, any nonterminal appearing in w F is smaller than F . If t G has its root in a v k , a lvl-1-branch of t G is composed of at most one t i , and nonterminals smaller than F . So it is smaller (for multiset ordering) than the corresponding branch number i in t F . So lvl 1 (t G ) < lvl 1 (t F ).

3. When t G is an applied t j k , since ℓ(t j k ) = 1, any lvl-1-branch can be extended in a lvl-1-branch of t F . So lvl 1 (t G ) < lvl 1 (t F ).

4. As in the case of u, for any subterm t G of a t i , lvl 1 (t G ) is unchanged.

To summarize, between b i and b, for all t G of the beginning (in u) or end (in c i h ), lvl 1 (t G ) is copied. Moreover lvl 1 (t F ) disappears, and new values than may appear are necessarily smaller than lvl 1 (t F ). So val(b i ) > val(b).

The definition of simple recursive still holds for order-2 schemes. A scheme S = (Σ, N, S, E) ∈ S 2 is called simple recursive if it has no nonproductive or useless arguments, and there are only two ∞-nonterminals S, F , and {S ⇒ w S , F x 1 . . . x ρ(F ) ⇒ w F } ∈ E where S cannot appear in w S , w F and F can appear at most once.

Lemma 5.3.7. For any scheme in S 2 generating a comb, there is a simple recursive scheme in S 2 with only useful nonterminals generating the same comb.

Proof. Let S = (Σ, N, S, E) ∈ S 2 be a useful scheme producing a comb and let S ⇒ w S ∈ E. If there is no ∞-nonterminal in w S , then S = w S is finite by Lemma 5.3.6. So there is an occurence of an ∞-nonterminal in w S . Since all nonterminals are useful, we can suppose that there is an occurence of a head subterm with ∞-nonterminal root F , modulo some rewriting. There is only one such head subterm in a given rewriting of S, otherwise the limit tree would have two infinite branches. Let n = ρ(F ) and F t 1 . . . t n be this subterm.

In order to get a contradiction, suppose that there is an ∞-nonterminal G in t i for some i. We note ti as a copy of t i where an app. subterm t G of root G is replaced by a variable x (of the same type). Since operands are always useful, there is a term w such that F t 1 . . . ti . . . t n =⇒ S * w where x occurs outside of any nonterminal (even semiterminals). Moreover, since F is infinite, there exists an ∞-nonterminal H in w. In particular, F t 1 . . . t n =⇒ S * w[x := t G ].

If x : o, we fall on the same case than in S 1 ; there would be more than one infinite branch. So the only possibility is that ℓ(t G ) = ℓ(x) = 1 and there is an occurence of x in w containing an occurence of H. Namely, x occurs in w in the form (xu 1 . . . u ρ(x) ) with H ∈ u k for some k. For this to happen, we must have ℓ(t i ) > 0 so that t i can feed x.

By applying the exact same process to G, we find that ℓ(u k ) > 0 so ℓ(x) > 1, which is impossible because then all app. subterms have order at most 1 in a order-2 scheme. So there cannot be any ∞-nonterminal in any t i . As in the order-1 case, the sequence of ∞-nonterminals encountered by rewriting S is ultimately periodic. We may therefore select S and another ∞-nonterminal to get the required form.

(b) Let w be a 2-morphic word defined by τ, σ on Σ. We chose a presentation given by Proposition 5.3.3 in order to obtain a safe scheme.

Mirroring the previous case, we set a nonterminal F which operands in the production rule are the symbols of non-zero arity. Formally, the set of variables is exactly Σ >0 ; they have all type order 1 and same arity (for a symbol a ∈ Σ n , we have the variable a : o n → o). The set of terminals is Σ 0 ∪ {f } where f : o → o → o.

Let a ∈ Σ n such that τ (a(z)) = θ ∈ TW(Σ ∪ z). Suppose a is fixed as the i-operand of F . We define the mapping µ : TW(Σ ∪ z) → AT(Σ 0 ∪ {f } ∪ z) as a "converse of ξ". It uses a set of semiterminals which types are as follows; the types of app. subterms of the i-operand of F are always o n → o. • if θ = z i , then µ(θ) = P n i with P n i (z) ⇒ z i .

• Let θ ∆ be the term word such that τ (∆) = ∆ • θ ∆ . Let t τ be the normal form of µ(θ ∆ )(a 1 . . . a ρ(F ) ), i.e. a term on Σ ∪ {f } such that ξ(t τ ) = θ ∆ . The rule for F is F a 1 . . . a ρ(F ) ⇒ f (t τ , F (µ(τ (a 1 )), . . . , µ(τ (a ρ(F ) )))).

In the same way, the starting nonterminal S has the rule

• If σ(∆) = ε, then S ⇒ F (µ(σ(a 1 )), . . . , µ(σ(a ρ(F ) )))

• otherwise, S ⇒ f (t σ , F (µ(σ(a 1 )), . . . , µ(σ(a ρ(F ) ))))

where t σ is a term on Σ 0 ∪ {f } such that Fr(t σ ) = σ(∆).

Let S be this defined scheme. Note that S is not presented in a cleaned version : most semiterminals have useless arguments. This is not a requirement in this direction.

The important property is that it is safe : indeed, app. subterms of type o k → o are all in w F below F , and their sons have the same type.

It is easy to see that for a ∈ Σ >0 , if μ(θ)(z) is the normal form of µ(θ)(z), ξ(μ(τ (a(z)))(z)) = τ (a(z)), ξ(μ(σ(a(z)))(z)) = σ(a(z)).

By applying the method of part (a), we check that the frontier of the limit tree of S is indeed σ(τ (∆)).

The above properties may sound natural, but they do not work out-of-the-box on further levels. First, at order 3 there are variables of order 2, so head nonterminal app. subterms are not necessarily terms. Consequently, a terminal term can contain nonterminals : the notion of ∞-nonterminal has to be redefined. Moreover, many proofs rely on the fact that the level of an app. subterm has order at most 1.

An immediate question about this result is whether we can transform an arbitrary scheme of ω-frontier w into a comb which frontier is w. Obviously the properties of the hierarchy developped in the previous sections are not available, so the question is open.

This result yields immediate properties on 2-morphic words.

Corollary 5.3.9. Let w be a 2-morphic word on Σ.

1. MTh(w) is decidable.

2. For any MSO-transduction T , if T (w) is an ω-word, then it is a 2-morphic word.

3. Let a ∈ Σ 0 and let a n the index of the i th occurence of a. There is a C > 0 such that for sufficiently large n, a na n-1 = O(2 2 C.n ).

Property 3 is the expected extension of [CT02, Prop. 14]; compare to the lower bound in Example 5.3.2.

Proof. Properties 1 and 2 are straightforward properties of graphs in the hierarchy. Property 3 is a corollary of Theorem 4.5.3 : there is a monadic interpretation transforming the ω-word into a comb where the infinite branch is composed of all vertices marked by a in order. The i-subtree is the rest of intermediate vertices.

Remark 5.3.10. The subword complexity of an ω-word w is the function which maps n on the number of factors of length n in w. For morphic words, this complexity is in O(n 2 ); see [AS03, Section 10.4] for more details. For 2-morphic words the complexity is maximal because of the Champernowne word. This was also noted for k-lexicographic words [START_REF] Bárány | A hierarchy of automatic ω-words having a decidable MSO theory[END_REF].

Remark 5.3.11. The morphism τ can be seen itself as a 1-order scheme. In this sense, it reminds of the transformation in [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF] using the operator @. The similarities end

Figure 1 . 1 :

 11 Figure 1.1: Un graphe fini et une propriété de ce graphe.

Figure 1

 1 Figure 1.2: L'arbre binaire complet.

Figure 1

 1 Figure 1.3: A finite graph and one of its properties.

Figure 1 . 4 :

 14 Figure 1.4: The complete binary tree.

Figure 2 . 1 :

 21 Figure 2.1: Example of a graph : the ladder

Figure

  Figure 2.2: The graph representation of the ordinal ω + 2.Graph representations of ordinals are hardly readable due to many arcs. The lighter notion of covering graphs will be described in Section 3.4.

  Theorem 2.4.4 ([CW98]). Unfolding from a MSO-definable vertex is MSO-compatible.

Figure 2 . 3 :Figure 2 . 4 :

 2324 Figure 2.3: The ladder and its unfolding.

Figure 2 . 5 :

 25 Figure 2.5: The pushdown hierarchy.

Figure 3 . 1 :

 31 Figure 3.1: Finite graph G 3 which unfolding has frontier ω 3 .

Figure 3 . 2 :

 32 Figure 3.2: Folded graphs of trees of frontier ζ, η and ω(1 + η).

Figure 3 . 3 :

 33 Figure 3.3: Folded regular graph of a tree of frontier ζ ω .

<

  Figure 3.4: {0, 1}-treegraph of ω.White vertices are those used by the interpretation; bracketed dots represent subgraphs where no vertex will be used. Here s x = (-1, -1, 0, . . . ), s y = (0, -1, 0, . . . ), s z = (0, 1, 0, . . . ). We

  straighforward. dom(ω) := push * a inc(ω) := push + a dec(ω) := pop + a

pop 2 push a copy 2 pop a pop 2 push a copy 2 pop aFigure 3 . 5 :

 35 Figure 3.5: The operation inc(ω ω ).The stacks here represent ω 3 + ω + 1, ω 3 + ω 2 and ω 3 + ω 2 + ω.

Figure 3 . 6 :

 36 Figure 3.6: Covering graph of ω ω .

  α} be the graph of successor and fundamental sequence relation, or covering graph of the ordinal α.

  Lemma 3.4.14. G ω α = I(Treegraph(G α )).

Figure 3 . 7 :

 37 Figure 3.7: Exponentiation of the covering graph of ω. For illustrations of the three cases in the proof of Lemma 3.4.14, we have

Figure 4 . 2 :

 42 Figure 4.2: Non-full tree of frontier ω having a branch with infinitely many 0's.

  lex y and x⊥y, then the path r xa -→ y is smaller than r y -→ y, which is contradictory with the definition of T . Let x 0 → y ∈ G \ T . If y ⊑ x, then there is a loop in G containing a 0, and thus a branch with infinitely many 0 in t. If x ⊏ y, then x1 ⊑ y and therefore the path r x0 -→ y is smaller than the path r y -→ y. In conclusion, y < lex x and q⊥p.

  Lemma 4.3.7. Fr(t) ≤ ω Fr( T ) .Proof. Let α = Fr( T ). Recall that V G = Dom(T ) ⊆ Dom( T ), i.e. r = ε and r

p

  i where w i ⊑ w, |w i | = i for 0 ≤ i ≤ |w|. Let a i

Figure 4 . 3 :

 43 Figure 4.3: A finite graph G, "spanning tree" T , completed tree T , and unfolding.

Figure 4 . 4 :

 44 Figure 4.4: Orders in a tree.

  Lemma 4.5.2. Let t ∈ Tree n be a #-comb and t = Unf(H, s). Let S = {x #

  Example 5.1.1. Let Σ = {a, b, g, f } with ρ(a) = ρ(b) = 0, ρ(g) = 1 and ρ(f ) = 2. Then f (a) is an applicative term of arity 1, and f (g(a), b) is a term, thus of arity 0.

Figure 5 . 1 :

 51 Figure 5.1: Rules for S 1 , of frontier ω ω .

x 1 Figure 5 . 2 :

 152 Figure 5.2: General rules for S n , of frontier ω ↑↑ (n + 1).

Figure 5 . 3 :

 53 Figure 5.3: Paperfolding sequence. When the corners are set to right angles like in this drawing, the resulting pattern is known as the dragon curve fractal.

  The limit word is a morphic sequence over the alphabet {0, 1} 2 . Define τ (00) = 1000 τ (10) = 1100 τ (01) = 1001 τ (11) = 1101 Then τ ω (11) is the paperfolding sequence.

  a, b}, Γ = {a, b}, n = 5. Figure5.4 shows the part of G accessible from 0. The circled vertices are colored respectively by a and b.

Figure 5

 5 Figure 5.4: A graph which unfolding yields the morphic word abaab . . . a 2 i b . . . .

rr

  i+1 of A a for some a ∈ Σ, where r i and r i+1 have prefixes in different branches. The set of possible states on z being finite, this means that there are r i a j+1 with i = j and thus r i a -→ G r j+1 , which cannot be since G is deterministic. So t r has only one infinite branch B.

Figure 5 . 5 :

 55 Figure 5.5: General shape of the folded graph.

  By considering the least common multiple of all the p w,y , we can adjust v so that x k+1 w a -→ G y and allow k to be simply greater than 1.

Figure 5 . 6 :

 56 Figure 5.6: Rules of a scheme which frontier is a morphic word.

  Example 5.3.1. The Champernowne word has a 2-morphic word presentation. Here Σ 0 = {0, 1} and Σ 1 = {g}.τ (∆) = ∆g(0)g(1) τ (g(z)) = g(z0)g(z1) σ(∆) = 01 σ(g(z)) = 1zImplicitly, τ (1) = σ(1) = 1 and τ (0) = σ(0) = 0. The first steps of rewriting are shown.τ (∆) = ∆ g(0) g(1) τ (2) (∆) = ∆ g(0) g(1)g(00) g(01) g(10) g(11) σ(τ (2) (∆)) Just like the word abaab . . . a 2 n b . . . was shown to be morphic, it is possible to build the 2-morphic word abaaaab . . . a 2 2 n b . . . . Letters a and b are copied by τ and σ. τ (∆) = ∆r(a)b τ (r(z)) = r(r(z)) σ(∆) = ε σ(r(z)) = zz It easy to prove that τ (n) (r(a)) = r (2 n ) (a) and finally σ(τ (n) (r(a))) = a 2 2 n .

  (concatenation)C n : (o n → o) → (o n → o) → o n → o (projection) P n i : o n → o (symbol of non-zero arity) G n b : (o ρ(b) → o) → (o n → o) ρ(b) → o n → o (symbol of arity 0) G n b : o n → o • if θ = θ 1 • θ 2 , then µ(θ) = C n (µ(θ 1 ), µ(θ 2 ))whereC(ϕ 1 , ϕ 2 , z) ⇒ f (ϕ 1 z, ϕ 2 z).

  if θ = b(θ 1 , . . . , θ i ) with b ∈ Σ >0 , then µ(θ) = G n b (b, µ(θ 1 ), . . . , µ(θ ρ(b) )) with G n b (ψ, ϕ 1 , . . . , ϕ ρ(b) , z) ⇒ ψ(ϕ 1 z, . . . , ϕ ρ(b) z). • if θ = b ∈ Σ 0 , then µ(θ) = G n b with G n b (z) ⇒ b.

FFigure 5 . 8 :

 58 Figure 5.8: Order-2 safe scheme which frontier is the Liouville word.

  have now to prove that (1) if t =⇒ (sN ∪ Σ)} is a well-ordering. The latter property comes from the wellknown fact that the multiset operation preserves well-ordering. Yet B(t) is just a chained encapsulation of 4 multisets on a finite ordering.It remains to prove (1). Let t F = F t 1 . . . t n =⇒ By simply looking at w F , we can say that there is h such thatb = u • v 1 • root(t i 1 ) • v 2 • • • • • root(t i h-1 ) • v h • c i hwhere u is the part above the rewritten subterm, (v k ) k∈[1,h] are (possibly empty) segments of branches in w F without variables, and c i h is a (possibly empty) branch of t i h .For any nonterminal G in a branch b, recall that we note t G the associated subterm.val(b) = {val(t G ) | t G intersects u or t G intersects v k , k ≤ h or t G = t i k s 1 . . . s l , k < h, l ≤ ρ(t i k ) or t G intersects c i h }Let b i be a branch in t going through t i h , of the form u • F • c. This branch exists and val(b i ) ∈ B(t). We prove that val(b) < val(b i ), which implies the required result B(t) > B(t ′ ).

S

t ′ , then B(t) > B(t ′ ); (2) the order on

{B(t) | t ∈ T S w = w F [x i := t i ]

be the rewritten term in t with n = ρ(F ). Let b be a branch of t ′ . If b does not intersect w, then val(b) already exists in B(t). Otherwise, b goes through w.

  . . . . . 93 t ⊥ term approximation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 t limit tree of the term t . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

		INDEX
	nonterminal, 93
	∞-nonterminal, 111
	operand, 93 Index order (schemes), 92
	order type, 23
	ordinal, 24
	ω-tail, 54 path, 22	deterministic, 21
	powerset, 19 ancestor, 22 approximation, 93 arc, 21 arithmetics, 23 on ordinals, 24 arity, 20, 93 prefix, 19 prefix tree, 22 production, 93 productive nonterminal, 103 pushdown hierarchy, 37	deterministic tree, 22 finite presentation, 19 FO, 30 frontier, 29 ω-frontier, 91 full tree, 22
	binary tree, 22	fundamental sequence, 55
	branch, 22	graph, 21
	Büchi automaton, 32	Graph n , 38
	Cantor normal form, 26	Hausdorff rank, 27
	Champernowne word, 106	homogeneous, 92
	closed formula, 30 CNF, see Cantor normal form 26 coding, 98 cofinality, 54	infinite nonterminal, 103 interval, 23 inverse rational mapping, 34
	color set, 21 colored	Knuth notation, 25
	deterministic tree, 22	label, 21
	graph, 21	length, 19
	ordering, 23	linear ordering, 22
	comb, 87	Liouville word, 117
	#-comb, 87 #-comb-graph, 87 complete tree, 22 configuration graph of a n-hopda, 50 crossing-free, 55	morphic word, 98 2-morphic word, 106 morphism, 97 MSO, 31 MSO-coloring, 33
	degree, 21	MSO-compatible, 33
	delabeled graph, 22	MSO-interpretation, 33
	dense, 26	MSO-transduction, 35
	descendant, 22	MSO-transduction, 35

Unlike in[START_REF] Braud | Covering of ordinals[END_REF], we adopt the notation ⋖ instead of ≺, in order to avoid confusion with the suborder relation between linear orders.

This result was already obtained in [BNR + 10] in an stronger form : it remains true even when ω is colored with arbitrary predicates.

Given a deterministic prefix-recognizable relation (U → V )W , we have necessarily that |V | = 1 and that a word in U • W must be uniquely decomposable. This satisfies exactly the property 3 of [CK01, Theorem 4.6].

RCNF, see Cantor normal form 26 recursion, see recursion recursion scheme, 92 reverse ordering, 23 rewriting relation, 93 root, 22 safety, 94 scattered, 26 semiterminal, 111 signature, 20 simple, 22 structure, 20 subordering, 23 subterm, 93 applicative, 93 head, 111 successor, 24 support, 21 tame, 78 term, 93 applicative, 93 grammar, see recursion scheme 92 tree, 96 word, 106 terminal, 93 tree presentation, 22 Tree n , 38 tree-walking automaton, see TWA 67 treegraph, 36 Γ-treegraph, 46 TWA, 67 typed alphabet, 93 types, 92 unfolding, 35 unlabeled graph, 22 useful nonterminal, 103 well-ordered trees, 73 well-ordering, 24 word ω-word, 23 finite, 19

• if γ 0 , . . . , γ h are all distinct ordinals of C k n-1 , then

Example 3.4.18. For instance,

The following lemma is only a matter of cardinality of powersets.

Lemma 3.4.19. The cardinality of the set C k n is exp(2, n, k).

We abusively note α + C k n for the set {α

The main difficulty of this section is to define this set with MSO logic.

Lemma 3.4.20. There is a monadic formula ϕ(x, y) such that for all n > 0, ϕ(exp(ω, n, k), y) is satisfied by x ∈ exp(ω, n, k) + C k n in the covering graph of an ordinal greater than exp(ω, n, k).2.

Proof. For each ordinal α, we define a sequence S α of ordinals. We note τ (α) the greatest β such that α ⋖ β.

• α ∈ S α , α + 1 ∈ S α ,

• if λ ∈ S α and α < λ⋖γ, then γ ∈ S α unless ∃λ ′ ≤ λ such that λ ′ ∈ S α and λ ′ ⋖τ (γ).

There is a monadic formula ϕ(α, y) which is satisfied exactly by y ∈ S α . The rest of the proof aims at showing that the set S exp(ω,n,k) is exp(ω, n, k) + C k n in the covering graph of an ordinal greater than exp(ω, n, k).ω. As a starting point, note that if λ ∈ S α , then there is a path of vertices of S α (labeled by ⋖) from α to λ.

Let α = exp(ω, n, k). First of all, τ (α.2) = α.ω and α ⋖ α.ω so α.2 / ∈ S α . By Proposition 3.4.5, any path from α to an ordinal of [α.2, ω exp(ω,n-1,k)+1 ) goes through α.2, which is not in S α . Also, paths from α to ordinals of [α.ω, exp(ω, n, k + 1)) necessarily go through α.ω which is not in S α because α ⋖ α.ω, so S α ∩ [α.2, exp(ω, n, k + 1)) = ∅. Eventually the fundamental sequence of exp(ω, n, k+1) is (α, exp(ω, n-1, ω.2), exp(ω, n-1, ω.3), . . . ), all of which but α are not in S α . To sum up, S α cannot contain ordinals greater or equal to α.2. Corollary 4.2.7. An ω-word of Graph n is the frontier of a full prefix tree in Tree n with exactly one infinite branch 1 ω .

Ordinals

In this section, we characterize the ordinals in the pushdown hierarchy. For more simplicity, orders of this section and of the following are uncolored, but the same applies to colored orders. In Section 3.1, ordinals below ω ↑↑ (n + 1) were shown to be in Graph n ; here, we show that they are the only possible ordinals of Graph n .

By Theorem 4.2.6, we only need to consider the frontier of prefix full binary trees. It is easy to see that frontier of a full binary prefix tree t is an ordinal if and only if t does not have an infinite branch with infinitely many 0's. We call such trees well-ordered trees.

Proposition 4.3.1. A full prefix binary tree has an ordinal frontier if and only if it is a well-ordered tree.

Proof. Let t be a (full binary prefix) well-ordered tree and suppose there is a infinite strictly decreasing sequence of leaves. Let t ′ be the restriction to prefixes of this sequence. Now t ′ is not full but its branches still have finitely many 0's. If t ′ had two distinct infinite branches, the infinitely many leaves supported by the largest would be larger than all the ones on the smallest, and they would fill the sequence. So t ′ has only one infinite branch, which has finitely many 0.

From the leaves of t ′ , we can select a (decreasing) subsequence with increasing largest prefixes on the branch. Let uu ′ be an element of this subsequence with largest prefix on the branch u. For sufficiently large u, u has the maximum number of 0, so that the next element of the subsequence has the form u1 k v for some v. Since t is deterministic, u ′ begins with 0, so uu ′ < lex u1 k v, and the sequence does not decrease.

Conversely, take a tree where one branch has infinitely many 0's. There is an infinite sequence (u i ) i such that for each i, u i 0 is in this branch; so u i 1 is not. Since the tree is prefix, there is a leaf v i such that u i 1 ⊏ v i . Then the sequence (v i ) i is strictly decreasing.

A non-full tree can yield an ordinal and still have a branch with infinitely many 0's, as Figure 4.2 shows. Nonetheless the Proposition 2.2.11 stands.

Let t is a well-ordered tree of Tree n . To characterize t, we are going to look for an order α of the previous level of the hierarchy and show that t is at most ω α . The natural first step is to consider the folded graph of t in the previous level. For n ≥ 1, let G ∈ Graph n-1 and r ∈ V G such that t = Unf(G, r), and such that each vertex of V G is accessible from r. Now we would like to find a well-order in G. Since Section 4.2, we know that it is equivalent to find a tree; so we build a well-ordered "spanning tree" into G, and we show that arcs which not in this tree cannot add too much complexity.

We start with this simple result.

Consider the following game G played by two players Branch and Spoiler by moving a token on t. The two players play in turn starting with Branch. Branch moves the token to a node anywhere below the current position. Spoiler can only move the token to a son of the current position. Branch loses the game if the token reaches a leaf.

The game can easily be translated in an equivalent parity game. For a formal definition of parity games and their properties, we refer the reader to [START_REF] Thomas | Languages, automata, and logic[END_REF]. It follows from the positional determinacy of parity games [START_REF] Law | Infinite games on finitely coloured graphs with applications to automata on infinite trees[END_REF] that either Branch and Spoiler as a positional winning strategy for G. Lemma 4.4.4. Branch wins the game if and only if t contains a branching subset.

Proof.

[⇒] Assume that Branch has a positional winning strategy for G which is a partial function Φ : Dom(t) → Dom(t). Consider the smallest set U ⊆ Dom(t) such that Φ(ε) ∈ U and for all u ∈ U , Φ(u0) and Φ(u1) also belong to U . It is easy to check that U is branching.

[⇐] If t contains a branching subset U , consider any partial function Φ : Dom(t) → Dom(t) such that Φ(ε) ∈ U and for all u ∈ U , Φ(u0) ∈ u0{0, 1} * ∩ U and Φ(u1) ∈ u1{0, 1} * ∩ U . We check that Φ is a positional winning strategy for Branch on G.

As t is tame (and hence does not contain any branching subset), Branch loses the game. Hence Spoiler has a positional winning strategy. There exists a mapping ϕ : Dom(t) → {0, 1} such that in any game where Spoiler choses his moves according to ϕ (i.e. at node u, Spoiler pick the ϕ(u)-son) is won by him.

Consider the tree t ′ obtained from t by swapping the two sons of any node u such that ϕ(u) = 1. Formally consider the mapping h from Dom(t) to {0, 1} defined for all ui ∈ Dom(t) with u ∈ Dom(t) and i ∈ {0, 1} by :

It is easy to check that h(Dom(t)) is prefix closed and that for all u, v ∈ Dom(t), u ⊑ v iff h(u) ⊑ h(v). Let t ′ be the tree such that Dom(t ′ ) is equal to h(Dom(t)). As h is injective, the mapping h a bijection from Dom(t) to Dom(t ′ ) preserving the ancestor relation. Hence t ≡ t ′ . Lemma 4.4.5. The tree t ′ is a well-ordered tree.

Proof. Assume by contradiction that there exists an infinite branch B in t ′ containing infinitely many 0's. We are going to construct an infinite play π for G where Spoiler plays according to Φ. As the play is infinite, Spoiler loses this play which contradicts the fact that Φ is a winning strategy for him.

Hausdorff rank of scattered orders in Graph n

By using invariance of r over ≡, we get the main result of this section.

Theorem 4.4.12. For all n ≥ 0, every scattered linear order in Graph n has an Hausdorff rank strictly less than ω ↑↑ n.

Proof. Let L be a scattered linear order in Graph n . By Theorem 4.2.6 and Proposition 4.4.1, there exists a binary prefix tame tree t ∈ Tree n such that L ≃ Fr(t). By Prop. 4.4.3 there exists a well-ordered tree t ′ ∈ Tree n such that t ≡ t ′ . By Prop. 4.4.11, we have that r(Fr(t)) = r(Fr(t ′ )). As t ′ is a well-ordered tree in Tree n , its frontier is an ordinal in Graph n . Hence by Theorem 4.3.8, Fr(t ′ ) < ω ↑↑ n + 1 and hence r(Fr(t ′ )) < ω ↑↑ n.

Remark 4.4.13. Obviously the converse to this theorem is not true; there are uncountably many scattered orders of Hausdorff rank less than ω ↑↑ n but there are only countably many linear orderings in Graph n .

In practical terms, consider a non-recursive sequence (a i ) i∈N in {1, 2} ω . The scattered order

has Hausdorff rank 2. But as the sequence of a i can be reconstructed by an MSO-formula, it has an undecidable MSO-theory, so it does not belong to the pushdown hierarchy.

By Proposition 4.4.7, the upper-bound of Theorem 4.4.12 directly translates the CBrank of prefix binary tame trees in Tree n . This leads to the following upper bound for all deterministic trees in Tree n .

Theorem 4.4.14. For every deterministic tree t ∈ Tree n , r CB (t) ≤ ω ↑↑ n.

Proof. Let t be a deterministic tree in Tree n . We can assume w.l.o.g. that t is binary.

Consider the tree t ′ obtained by adding a leaf to every node which is its left-most son. Clearly t ′ is prefix, belongs to Tree n and r CB (t) = r CB (t ′ ). The construction of Prop. 4.2.1 gives a prefix binary tree t ′′ ∈ Tree n with the same CB-rank.

As the result is already established for tame trees, we can also assume that t is not tame. Note that for every deterministic non-tame tree t, r CB (t) ≤ λ = sup{r CB (t /u ) | u ∈ Dom(t) and t /u tame}. Indeed, d λ (t) has no tame subtrees. If t has no tame subtrees then d(t) = t. Hence d(t) ≤ λ.

By Proposition 2.5.5 any subtree of t ∈ Tree n is also in Tree n . By Proposition 4.4.7 and Theorem 4.4.12 we have, for all u ∈ Dom(t) such that t /u is tame,

The inequality is conjectured to be strict. By Corollary 5.1.6, it is enough to prove that the frontiers of prefix binary combs generated by order-1 schemes are morphic words. At this order, safety is not a constraint. In order to prove the result, a given scheme will undergo a series of transformations through the following lemmas. Eventually, we show that it is enough to consider specific simple schemes with only 2 nonterminals.

Let S = (Σ, N, S, E) ∈ S 1 be a scheme. We begin by cleaning the scheme of nonproductive nonterminals, where non-terminal F is productive if F x 1 . . . x ρ(F ) = ⊥. It is obvious that for any S ∈ S 1 generating an infinite tree, there is S ′ ∈ S 1 with only productive nonterminals, and generating the same tree.

A nonterminal F ∈ N is infinite if it generates an infinite tree, i.e. for x 1 , . . . , x ρ(F ) ∈ X, the tree F x 1 . . . x ρ(F ) is infinite.

Lemma 5.2.9. For any S ∈ S 1 generating an infinite tree, there is S ′ ∈ S 1 with only infinite nonterminals, and generating the same tree.

Proof. Let S = (Σ, N, S, E) ∈ S 1 with only productive nonterminals producing an infinite tree, so S is infinite. Let F ∈ N be a finite nonterminal and n = ρ(F ). There is a finite term w on Σ ∪ X such that F x 1 . . . x n =⇒ S * w and F x 1 . . . x n = w. For each other nonterminal F ′ , if there is an occurrence of F in w F ′ , then in particular there is an occurence of F t 1 . . . t n without any F in any t i , for 1 ≤ i ≤ n. Replacing F t 1 . . . t n by w[x i := t i ] is done by rewriting. Eventually, we can replace all occurrences of F in w F ′ .

The resulting scheme generates the same tree. Since N is finite, the whole process may be repeated for each finite nonterminal.

The operand index i of a nonterminal F is useful if x i appears in F x 1 . . . x ρ(F ) . A useful nonterminal has only useful arguments.

Lemma 5.2.10. For any scheme in S 1 generating an infinite tree, there is a scheme in S 1 with infinite and useful nonterminals generating the same tree.

Proof. Let S = (Σ, N, S, E) ∈ S 1 generating a comb with only infinite nonterminals. Let F be such a nonterminal. If F is inaccessible from S (i.e. for any S =⇒ S w, F does not appear in w), we safely remove this nonterminal.

Suppose that i is a useless argument of F , then x i cannot appear in π(w), where w is any rewriting of a tree containing x i only in an occurrence of F x 1 . . . x ρ(F ) . We simply erase this argument. Formally, let ♦ be a new letter, S ′ = (Σ∪{♦}, {F ′ }∪N \{F }, S, E ′ ) be the same scheme where ρ(F ′ ) = n -1 and F ′ has production rule F ′ x 1 . . . x i-1 x i+1 . . . x n ⇒ w F [x i := ♦], and all occurrences of F t 1 . . . t n in each production rule are replaced by F ′ t 1 . . . t i-1 t i+1 . . . t n . In the limit tree, this transformation can only change some subtrees into leaves labeled by ♦. But if it did, this means that there was a rewriting S =⇒ S ′ w such that ♦ appears in π(w). By the definition of F ′ , this is contradictory with the lemma that i is a useless argument of F . So the resulting tree is the same. This operation only remove arguments, so iteration is finite.

A scheme S = (Σ, N, S, E) ∈ S 1 is called simple recursive if N = {S, F }, and E = {S ⇒ w S , F x 1 . . . x ρ(F ) ⇒ w F } where S cannot appear in w S , w F and F appears exactly once in both.

Lemma 5.2.11. For any scheme in S 1 generating a comb, there is a simple recursive scheme in S 1 with only infinite and useful nonterminals generating the same comb.

Proof. Let S = (Σ, N, S, E) ∈ S 1 and S ⇒ w S ∈ E. If N = {S}, the recursive form is easy to get : due to the fact that there is only one infinite branch in the limit tree and since S is infinite, there is exactly one occurence of S in w S . Otherwise, since nonterminals are infinite, if there is two nonterminals without nonterminal ancestors in w S , there would be two infinite paths in S . So there only one such nonterminal subterm F t 1 . . . t ρ(F ) , which is infinite and useful. There is a w such that

• there is a nonterminal in w,

• and there is an occurence of each x i to the left of this nonterminal.

In particular, F t 1 . . . t ρ(F ) =⇒ S * w[x i := t i ]. This means there is no nonterminal in any t i , or there would be two nonterminal without nonterminal ancestors in w S . This means that in fact there is exactly one nonterminal in w S . We reach the same conclusion for the right side of each production rule. This means there is only one w i such that S =⇒ S i w i and that w i contains exactly one nonterminal F i . Since there are finitely many nonterminals, the sequence (F i ) i>0 is ultimately periodic and the simple recursive form is easy to obtain.

We are now ready to focus on the proper result, i.e. Theorem 5.2.6.

Proof. Let S = (Σ, {S, F }, S, E) be a simple recursive scheme of S 1 , n = ρ(f ) with production rules S ⇒ w S , F x 1 . . . x n ⇒ w F . Let Σ 0 be the subset of Σ of type o. Up to renaming, suppose that ⊥ / ∈ Σ. Let F s 1 . . . s n and F t 1 . . . t n be the subterms starting with F respectively in w S and w F . Each s i is a term on Σ and each t i is a term on Σ ∪ X. Let u S , u F be finite words on Σ 0 ∪ X such that Fr(π(w ⊥ S )) = u S ⊥, Fr(π(w ⊥ F )) = u F ⊥. We set Σ 0 ∪ {∆, x 1 , . . . , x n } as the alphabet of the morphic word and τ, σ two morphisms on this alphabet. Letters from {∆, x 1 , . . . , x n } are temporary and are erased by σ.

τ

simply copied and symbols which are actually used are of non-zero arity, except for ∆. This hints the following proposition, which seems to be anecdotic but reveals itself useful in Section 5.3.2.

Proposition 5.3.3. For a 2-morphic word w, there is τ, σ, Σ, ∆ such that

• ∆ appears only as the first letter of τ (∆),

• for any other letter a ∈ Σ 0 , τ (a) = a.

. This answers the constraint on ∆.

For any other letter, it is possible to add "fake operands". Formally, for any letter a, take a fresh symbol a 1 of arity 1 such that τ (a 1 (z)) = τ (a), σ(a 1 (z)) = σ(a). Then set τ ′ (a) = a, and for each other symbol b, set

Then w = σ(τ ′ω (∆ ′ )).

Second-order scheme ω-frontiers

We adapt the method of Section 5.2.4 to prove that frontiers of combs generated by order-2 schemes are exactly the 2-morphic words. The main problem is to perform the transformation leading to a "linearized" scheme, where there are only two infinite nonterminals. Once this transformation is done, we may read the values of σ and τ as in the case of 1-order schemes.

A nice property of this method is that is does not use the safety constraint, even though 2-morphic words can be encoded as frontier of safe schemes. This means the ω-frontiers of schemes does not depend on safety.

The previous remark about productive nonterminals is still straighforward. For any S ∈ S 2 generating an infinite tree, there is S ′ ∈ S 2 with only productive nonterminals, and generating the same tree. From now on, we suppose every nonterminal is productive. The second step, deleting useless operands, is more delicate. In this case, simply deleting operands will not work, because it would lead to type mismatches -see below for an example. The solution kept here is to duplicate nonterminals when needed.

Lemma 5.3.4. For any scheme in S 2 generating a tree, there is a scheme in S 2 with only useful nonterminals generating the same tree.

Proof. Let S = (Σ, N, S, E) ∈ S 2 generating an infinite tree. Let F be a nonterminal. If F is inaccessible from S (i.e. for any S =⇒ S * w, F does not appear in w), we may safely remove it.

We are ready to prove the main result.

Theorem 5.3.8. The following sets of ω-words are equal :

1. the ω-words of the third level of the pushdown hierarchy, 2. the ω-frontiers of safe order-2 schemes, 3. the frontiers of combs generated by order-2 schemes, 4. the 2-morphic words.

Proof. The equality 1 = 2 comes from Theorem 4.2.6, and 2 ⊆ 3 comes from Proposition 5.0.5. It is therefore enough to prove that (a) frontiers of combs generated by arbitrary schemes are 2-morphic words, (b) 2-morphic words are ω-frontiers of safe schemes. For (b) it is easier to prove that 2-morphic words are frontiers of safe combs. (a) Let S be a simple recursive scheme producing a comb, and let S, F be the two ∞nonterminals, with production rule S ⇒ w S , F x 1 . . . x ρ(F ) ⇒ w F . For each variable x i : o n → o, we define the symbol x i ∈ Σ n . Let t S i , t F i be the i-operands of F respectively in w S and w F . They are in AT(sN ∪ Σ), and have type o n → o. By Lemma 5.3.6, when fed with appropriate variables, t S i z and t F i z are finite trees. We simply set σ(x i (z)) = Fr( t S i z ). For τ we have to take other variables in consideration, but we will flatten the terminals. Define the mapping ξ from T(Σ ∪ z) to TW(Σ) :

where x is a variable, ξ(t) = x(ξ(t 1 ), . . . , ξ(t ρ(x) )). We set τ (x i (z)) = ξ( tS i ) where tS i is the normal form of t S i z, i.e. such that t S i z =⇒ S * tS i which cannot be rewritten.

The starting letter ∆ is naturally associated to the part "outside of F ". Formally, we can suppose as before that the app. subterm of root F in w S is in fact a head subterm (in w F as well). So if we replace this subterm by ⊥ in order to approximate, we get w ′ S and w ′ F with only terminals and semiterminals. We set σ(∆) • ⊥ = Fr( w ′ S ). For τ , we set ξ(⊥) = ε and we have then τ (∆) = ∆ • ξ( ŵ′ F ) where ŵ′ F is the normal form of w ′ F . By construction, if S ⇒ k s k only by rewriting F , then

here; whereas the role of @ was to study structural properties of the limit tree, the role of τ is simply to reproduce the mechanism of F and depends on the fact that there is only one recursive nonterminal.

Liouville word

The Liouville word or constant is another example of infinite words more complex than morphic words. The constant is k>0 10 -k! = 0.1100010000000000000000010 . . . . We only consider digits after the dot. It is the frontier of the limit tree of the safe order-2 scheme ({f, 0, 1}, {S, F, G, H}, S, E) where E is described in Figure 5.8.

The associated 2-morphic word is defined by the the following morphisms on Σ = {0, 1, ∆, g, n} where g, n have arity 1. As before, 0 and 1 are dumb letters : τ (1) = σ(1) = 1 and τ (0) = σ(0) = 0.

Informally, the goal is to obtain at step k an additionnal number of letters equal to (k + 2)! -(k + 1)! = (k + 1)(k + 1)!. The symbols n, g are such that

) is a word of length k.(k + 1)! + (k + 1)! = (k + 1)(k + 1)!. This is clearer when considering one iteration.