# Représentations et propriétés de structures infinies

Thomas Colcombet

► To cite this version:

Thomas Colcombet. Représentations et propriétés de structures infinies. Logique en informatique [cs.LO]. Université de Rennes 1, 2004. Français. NNT: 2004REN10094. tel-04504198

HAL Id: tel-04504198

https://cnrs.hal.science/tel-04504198

Submitted on 14 Mar 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
THÈSE

présentée

devant l'université de Rennes 1

pour obtenir

le grade de : DOCTEUR DE L'UNIVERSITÉ DE RENNES 1
Mention INFORMATIQUE

par

Thomas COLCOMBET

Équipe d'accueil : Galion

École doctorale : MATISSE

Composante universitaire : IFSIC/IRISA

Titre de la thèse :

Représentations et propriétés de structures infinies

soutenue le 18 mars 2004 devant la commission d'examen

M. : Erich

GRÄDEL

Président

MM. : Bruno

COURCELLE

Rapporteurs

Wolfgang

THOMAS

MM. : Damian

NIWIŃSKI

Examinateurs

Jean-Claude

RAOULT

Didier

CAUCAL
<figure><img src="image_2.png" /></figure>
## Remerciements

Je tiens à remercier tout d'abord les membres du Jury de cette thèse. En premier lieu, je remercie Bruno Courcelle et Wolfgang Thomas qui ont tous deux accepté de rapporter ce travail en se pliant à un calendrier difficile. Bruno Courcelle, par ses nombreuses remarques et conseils a beaucoup participé à la qualité de ce travail. Je remercie Erich Grädel qui a tant fait pour la notoriété de la thématique. Je remercie Damian Niwiński qui en plus de m'accueillir à Varsovie et de me transmettre tant de connaissances, a accepté de participer à ce Jury. Je remercie Jean-Claude Raoult, qui a aussi gentiment accepté de faire partie de ce jury.

Enfin, je tiens à remercier Didier Caucal qui, entre autres facéties, a bien voulu diriger mes travaux de thèse. Ses conceptions de la recherche, de l'esprit de la recherche, ont une influence certaine sur mon futur.

Je remercie Tanguy Urvoy qui est un merveilleux collègue et ami. Je remercie Karine Heydemann qui a su aussi me soutenir en de nombreuses occasions.

Je remercie les différentes personnes avec lesquelles j'ai eu l'occasion de travailler et de publier durant cette thèse, Arnaud Carayol, Pascal Fradet et Christophe Löding.

Je remercie mes parents, qui m'ont laissé m'orienter vers un métier que j'aime, quitte à y blanchir quelques cheveux.

Pour finir, je remercie Marion, pour son soutien indéfectible. Sans elle, ce pénible accouchement n'aurait pu aboutir.
<figure><img src="image_3.png" /></figure>
# Table des matières

<table><tbody><tr><td>1</td><td>Introduction</td><td>1</td></tr><tr><td>2</td><td>Définitions et notions de base</td><td>8</td></tr><tr><td>2.1</td><td>Structures</td><td>9</td></tr><tr><td>2.1.1</td><td>Cas général</td><td>9</td></tr><tr><td>2.1.2</td><td>Graphes</td><td>10</td></tr><tr><td>2.1.3</td><td>Les automates</td><td>11</td></tr><tr><td>2.1.4</td><td>Arbres et termes</td><td>12</td></tr><tr><td>2.2</td><td>Logiques</td><td>15</td></tr><tr><td>2.2.1</td><td>Logique du premier ordre</td><td>15</td></tr><tr><td>2.2.2</td><td>Logique monadique</td><td>17</td></tr><tr><td>2.2.3</td><td>Extensions de la logique monadique</td><td>20</td></tr><tr><td>2.2.4</td><td>Construction de Feferman-Vaught</td><td>21</td></tr><tr><td>2.3</td><td>Opérations sur les structures</td><td>25</td></tr><tr><td>2.3.1</td><td>Modification finie</td><td>26</td></tr><tr><td>2.3.2</td><td>Interprétation logique</td><td>26</td></tr><tr><td>2.3.3</td><td>Union disjointe</td><td>29</td></tr><tr><td>2.3.4</td><td>Produits</td><td>30</td></tr><tr><td>2.3.5</td><td>Transduction monadique</td><td>35</td></tr><tr><td>2.3.6</td><td>Dépliage</td><td>36</td></tr><tr><td>2.3.7</td><td>Structure arborescente</td><td>37</td></tr><tr><td>2.4</td><td>Propriétés structurelles</td><td>42</td></tr><tr><td>2.4.1</td><td>La largeur arborescente</td><td>42</td></tr><tr><td>2.4.2</td><td>Graphe uniformément creux</td><td>44</td></tr><tr><td>2.4.3</td><td>Sous-graphes bipartis complets</td><td>45</td></tr><tr><td>3</td><td>Systèmes d'équations</td><td>47</td></tr><tr><td>3.1</td><td>Ordres partiels complets et algèbres</td><td>48</td></tr><tr><td>3.1.1</td><td>Définitions</td><td>48</td></tr><tr><td>3.1.2</td><td>Quelques ordres partiels complets</td><td>52</td></tr><tr><td>3.1.3</td><td>Algèbres et algèbres continues</td><td>54</td></tr></tbody></table>
<table><tr><td>3.2</td><td>Systèmes d'équations</td><td>56</td></tr><tr><td>3.2.1</td><td>Une première définition</td><td>56</td></tr><tr><td>3.2.2</td><td>Systèmes d'équations comme graphes</td><td>57</td></tr><tr><td>3.3</td><td>μ-définissabilité et μ-calcul</td><td>59</td></tr><tr><td>3.3.1</td><td>Généralités sur les points fixes</td><td>60</td></tr><tr><td>3.3.2</td><td>Syntaxe et sémantique du μ-calcul</td><td>63</td></tr><tr><td>3.3.3</td><td>Décomposition du μ-calcul</td><td>65</td></tr><tr><td>3.3.4</td><td>Extension vectorielle du μ-calcul</td><td>65</td></tr><tr><td>3.3.5</td><td>Termes marqués</td><td>67</td></tr><tr><td>3.3.6</td><td>μ-définissabilité</td><td>68</td></tr><tr><td>3.4</td><td>Transducteurs déterministes</td><td>72</td></tr><tr><td>3.4.1</td><td>Définition</td><td>72</td></tr><tr><td>3.4.2</td><td>Normalisation</td><td>75</td></tr><tr><td>3.4.3</td><td>Propriétés</td><td>77</td></tr><tr><td>3.4.4</td><td>Lien avec les systèmes d'équations</td><td>80</td></tr><tr><td>3.4.5</td><td>Utilisation des transducteurs déterministes</td><td>83</td></tr></table>

<table><tr><td>4</td><td>Graphes et structures sur les piles</td><td>89</td></tr><tr><td>4.1</td><td>Langages rationnels et systèmes d'équations</td><td>90</td></tr><tr><td>4.1.1</td><td>Automates</td><td>90</td></tr><tr><td>4.1.2</td><td>Automates déterministes</td><td>90</td></tr><tr><td>4.2</td><td>Les graphes préfixes</td><td>91</td></tr><tr><td>4.3</td><td>Les structures HR-équationnelles</td><td>94</td></tr><tr><td>4.3.1</td><td>Première approche: grammaires de structures</td><td>94</td></tr><tr><td>4.3.2</td><td>Représentation équationnelle</td><td>95</td></tr><tr><td>4.3.3</td><td>Propriétés des graphes HR-équationnels</td><td>99</td></tr><tr><td>4.4</td><td>Graphes préfixes reconnaissables et extensions</td><td>101</td></tr><tr><td>4.4.1</td><td>Représentation équationnelle</td><td>103</td></tr><tr><td>4.4.1.1</td><td>Opérateurs sur les graphes</td><td>103</td></tr><tr><td>4.4.1.2</td><td>Extension aux structures</td><td>105</td></tr><tr><td>4.4.1.3</td><td>Un opérateur de fusion supplémentaire</td><td>109</td></tr><tr><td>4.4.2</td><td>Représentation interne</td><td>116</td></tr><tr><td>4.4.2.1</td><td>Graphes préfixes reconnaissables</td><td>116</td></tr><tr><td>4.4.2.2</td><td>Les relations PR</td><td>118</td></tr><tr><td>4.4.3</td><td>Représentation par transformations</td><td>121</td></tr><tr><td>4.4.3.1</td><td>Premier contact</td><td>121</td></tr><tr><td>4.4.3.2</td><td>Des transductions monadiques vers les relations PR</td><td>122</td></tr><tr><td>4.4.4</td><td>Application à la hiérarchie de Caucal</td><td>123</td></tr><tr><td>4.4.5</td><td>Liens entre VR et HR</td><td>123</td></tr><tr><td>4.4.5.1</td><td>Intuitions sur la preuve</td><td>124</td></tr><tr><td>4.4.5.2</td><td>Normalisation</td><td>125</td></tr></table>
<table><tr><td>4.4.5.3</td><td>Premières propriétés</td><td>126</td></tr><tr><td>4.4.5.4</td><td>Hypothèses de récurrence</td><td>127</td></tr><tr><td>4.4.5.5</td><td>Le résultat</td><td>128</td></tr></table>

5 Structures automatiques sur les termes 129

5.1 Langages de termes 129

5.1.1 Automates d'arbres 129

5.1.1.1 Le cas général 130

5.1.1.2 Automates descendants déterministes 131

5.1.2 Représentation équationnelle 131

5.1.2.1 Langages rationnels 131

5.1.2.2 Automates descendants déterministes 131

5.2 Structures terme-automatiques 132

5.2.1 Présentation terme-automatique 133

5.2.1.1 Relations terme-synchronisées 133

5.2.1.2 Structures à présentation terme-automatique 134

5.2.2 Représentation équationnelle 135

5.2.2.1 Définition 135

5.2.2.2 Normalisation 136

5.2.2.3 Équivalence avec la représentation automatique 138

5.2.3 Représentation logique 141

5.2.3.1 Interprétation des parties 141

5.2.3.2 D'un système d'équations à la représentation logique 143

5.2.3.3 De la représentation logique à un système d'équations 146

5.2.4 Structures automatiques 149

6 Graphes de récriture suffixe de termes 151

6.1 Représentation interne 151

6.1.1 Contexte 152

6.1.2 Graphes de récriture suffixe de termes 153

6.2 Représentation équationelle 155

6.3 Équivalence de représentations 156

6.3.1 Des équations aux récritures 158

6.3.2 De la récriture aux équations 159

6.4 Premier ordre avec accessibilité 160

6.5 Largeur arborescente 164

6.5.1 Croissance pour la largeur arborescente 164

6.5.2 Élimination des produits 166

6.5.3 Décidabilité et effectivité 171

6.6 Largeur de clique 172
<table><tr><td>6.6.1 Contexte</td><td>172</td></tr><tr><td>6.6.2 Un arbre de théorie monadique indécidable</td><td>173</td></tr><tr><td>6.6.3 Opérateur de retrait</td><td>174</td></tr><tr><td>6.6.4 La construction</td><td>175</td></tr><tr><td><b>7 Conclusion et perspectives</b></td><td><b>180</b></td></tr><tr><td><b>A Annexes</b></td><td><b>188</b></td></tr><tr><td>A.1 Complément sur les tranducteurs déterministes</td><td>188</td></tr><tr><td>A.2 Complément sur le théorème 16</td><td>193</td></tr><tr><td>A.3 Complément sur le théorème 26</td><td>196</td></tr></table>
# Chapitre 1

## Introduction

### Contexte

L'apparition de l'informatique a été accompagnée et a même précédé d'intenses efforts de formalisation dans l'objectif de préciser ce qu'est un «calcul». L'étude de cette question fit rapidement apparaître que cette notion était inti-mement reliée à celle de preuve mathématique. Depuis lors, les rapprochements entre informatique et logique mathématique n'ont fait que grandir en nombre et en importance. Citons, d'un point de vue pratique, l'apparition de langages de programmation dits logiques permettant d'exprimer l'exécution d'un programme comme la démonstration d'un énoncé logique. Citons d'un point de vue théo-rique, les travaux de Fagin qui donnèrent naissance à la complexité descriptive; une théorie identifiant la notion informatique de classe de complexité à celle de définissabilité dans une certaine logique.

Une autre branche dont les applications sont des plus prometteuses est l'uti-lisation de la logique dans le cadre de la vérification. Dans une telle approche, la logique permet d'exprimer des propriétés auquelles doit se conformer un pro-gramme (ou tout autre objet). Ces techniques de développement peuvent être classées suivant leur niveau d'automaticité. Nous nous intéressons ici à la vérifica-tion totalement automatique de propriétés. Celle-ci est bien entendue indécidable dans la plupart des cas. Néanmoins, il est possible d'établir automatiquement des propriétés pour certains systèmes plus simples que les machines de Turing. Décider de la vacuité d'un langage rationnel à partir de la donnée d'un automate le reconnaissant peut être vu comme un cas simple de telle vérification. Pour pouvoir donner toute sa généralité à cette vérification, il convient de paramétrer l'étude par un formalisme de description de l'objet à vérifier et une syntaxe des propriétés à vérifier. C'est ce que propose l'approche logique.
# Logique

Deux notions logiques fondamentales nous intéressent tout particulièrement, celle de structure et celle de formule.

Les structures (relationnelles) permettent de décrire l'objet d'étude. Dans le contexte de la vérification, la structure décrit le programme à vérifier. Plus précisément, une structure est un ensemble d'éléments munis de relations. Dans le cas d'un automate par exemple, chacun des éléments représente un état et les relations codent les transitions, les ensembles des états initiaux et finaux. Pour l'étude de comportement, chaque élément est une configuration et les relations décrivent les transitions du programme.

Les formules permettent quant à elles de décrire les propriétés que l'on cherche à établir. Ainsi, on se fixe un langage de formules, c'est-à-dire un ensemble de mots. À chaque formule logique est attribuée une sémantique qui précise pour toute structure si elle «satisfait la formule» ou non. On dit dans ce cas que la structure est un modèle de la formule. Une formule logique peut, par exemple, énoncer l'existence d'un chemin entre deux sommets d'un graphe. Dans le cadre des automates, cela permet d'exprimer la non vacuité du langage accepté et, dans le cadre de la vérification de programmes, cela peut servir à exprimer la possibilité d'atteindre une configuration non valide. Une logique est décrite par la donnée de l'ensemble des formules et par la relation de satisfaction.

Dans la pratique, de très nombreuses logiques ont été développées, variant par leur expressivité ou leur objectif. Deux principales variantes concernent la vérification.

*Les logiques temporelles* expriment des propriétés sur les graphes orientés (appelés dans ce contexte «structures de Kripke»). Ces graphes représentent des systèmes de transition, et une formule de la logique exprime des contraintes sur le comportement du système. Les logiques temporelles se décomposent en logiques du temps linéaire (comme LTL) pour lesquelles une exécution est une suite de configurations et les logiques du temps arborescent (comme CTL, CTL\* ou le µ-calcul modal) qui peuvent faire référence simultanément à toutes les exécutions possibles. Ces logiques peuvent être enrichies par l'ajout de modalités de retour permettant à une formule d'inverser le temps et de faire référence au «passé».

*La logique du premier ordre* et ses variantes. Ces logiques peuvent faire référence aux éléments de l'univers (resp. aux sommets) au moyen de variables et tester si ces éléments sont en relation dans la structure.

Une grande différence par rapport aux logiques temporelles est que la logique du premier ordre ne peut exprimer que des propriétés locales, ce qui est insuffisant dans beaucoup de cas.

La logique (du second ordre) monadique est une extension particulièrement intéressante de la logique du premier ordre. Elle enrichit cette dernière par la pos-
sibilité d'utiliser des variables représentant des parties de l'univers de la structure (resp. des ensembles de sommets du graphe). Cette augmentation d'expressivité permet, entre autre, d'exprimer l'existence d'un chemin entre deux sommets. Cette propriété n'est plus locale.

Structures finies

Lorsque les informaticiens se sont penchés sur la logique, et plus précisément le problème de la vérification de modèle (le *model checking*), c'est tout naturellement sur la vérification de structures finies et de famille de structures finies qu'ils se sont d'abord attachés. Ces études ont été à l'origine de nombreux résultats et de nombreuses pistes de recherche.

En général, déterminer si une structure finie satisfait une certaine formule logique est décidable. Il suffit pour cela que la logique ne soit pas intrinsèquement trop puissante. On peut néanmoins s'intéresser aux questions d'existence d'un modèle pour une formule (le problème de satisfaisabilité), de complexité du problème de satisfaction et de la satisfaisabilité au sein d'un ensemble de structures finies.

Le problème de la satisfaisabilité consiste à déterminer si une formule logique donnée admet un modèle fini. Ce problème est décidable pour les logiques temporelles (LTL, CTL, μ-calcul modal ou μ-calcul modal avec modalité de retour). Quand il est question de logique du premier ordre, l'existence d'un modèle fini est indécidable (Traktenbrot). Naturellement, pour des logiques plus expressives comme la logique monadique, la situation n'est pas plus favorable.

Cependant, quand il s'agit de déterminer l'existence d'un modèle fini possèdant certaines contraintes géométriques, le problème peut redevenir décidable. Ainsi, déterminer s'il existe un arbre fini satisfaisant une propriété exprimée en logique monadique est décidable. Ce résultat se généralise aux structures qui ne s'éloignent pas trop d'un arbre. Pour cela, on introduit la notion de largeur arborescente qui est une mesure de la ressemblance d'une structure à un arbre. Pour *k* fixé, déterminer l'existence d'un modèle fini de largeur arborescente inférieure à *k* pour une formule monadique est décidable. Une autre mesure de la ressemblance entre une structure et un arbre est la largeur de clique<fnref n="1" />. Là encore, décider de l'existence d'un modèle de largeur de clique bornée pour une formule monadique est décidable. En fait, un résultat de Seese établit que déterminer l'existence d'un modèle pour une formule de la logique du second ordre gardée (une extension de la logique monadique) parmi une famille de graphes finis ne peut être décidable que si cette famille est de largeur arborescente bornée. Une relation similaire entre

<footnote n="1">1. Le terme de ressemblance peut sembler dans ce cas excessif car cette mesure n'a rien de «visuelle». Elle correspond néanmoins à la possibilité de décrire la structure à partir d'un arbre.</footnote>
la logique monadique et les familles de structures de largeur de clique bornée est
connue sous le nom de «conjecture de Seese».

Si l'on s'intéresse aux questions de complexité, là encore les notions de largeur
arborescente et de largeur de clique entrent en compte. En effet, étant données
une structure et une formule logique du premier ordre, déterminer si la structure
est un modèle de la formule est PSPACE-complet. Il en est de même pour la
logique monadique. Si la formule est fixée, alors le problème se trouve dans la
hiérarchie polynomiale pour ces deux logiques<fnref n="2" />. Pourtant, pour une formule fixée
de la logique monadique et un entier *k*, déterminer si une structure de largeur
arborescente inférieure à *k* est un modèle de la formule n'est que linéaire dans la
taille de la structure, ce qui correspond à un remarquable gain en complexité. Le
phénomène reste valable pour la largeur de clique.

Simultanément des travaux se sont attachés à la description de familles de
structures finies. Ceci peut être fait par caractérisation logique (e.g. l'ensemble
des modèles d'une formule), par utilisation de propriétés géométriques (planarité,
exclusion de mineurs ...) ou par une approche algébrique. L'approche algébrique
consiste à se fixer un alphabet (éventuellement infini) d'opérations permettant de
transformer et de combiner des structures. Une structure complexe peut être alors
décrite comme évaluation d'une expression mettant en jeu ces opérations. Cela
permet de représenter des ensembles de structures par des ensembles de termes.

Deux familles d'opérations sont usuellement considérées dans ce contexte : les
opérateurs **HR** et les opérateurs **VR** (qui travaillent sur les graphes mais peuvent
être étendus aux structures). Les opérateurs **HR** capturent exactement la notion
de largeur arborescente : pour tout entier *k*, il existe un ensemble fini d'opéra-
teurs **HR** tels qu'un graphe est de largeur arborescente inféreure à *k* si et seulement
si il est (à isomorphisme près) évaluation d'une expression n'utilisant que ces opé-
rateurs. Une relation identique relie les opérateurs **VR** et la largeur de clique (en
fait, il s'agit de la définition de la largeur de clique).

Cette approche se combine avec la notion de reconnaissabilité sur les termes
finis. Au moyen d'automates finis (ou de définition logique, ou d'expressions ra-
tionnelles ou de grammaires), il est possible de définir des ensembles de termes,
appelés langages. Lorsque l'on évalue les termes d'un langage, cela permet de
définir une famille de structures.

Structures infinies

Avec les structures (et les graphes) infinies, une nouvelle problématique appa-
raît: comment décrire finiment un objet infini.

Plusieurs approches sont possibles :

- la représentation interne consiste à décrire explicitement l'univers et les

<footnote n="2">2. Le niveau dans la hiérarchie correspond au nombre d'alternances de quantifications.</footnote>
relations,

- la représentation équationnelle décrit une structure infinie comme la solution d'un système d'équations utilisant un ensemble d'opérateurs fixé,

- la représentation par transformations à pour point de départ une structure infinie connue, et revient à décrire de nouvelles structures comme des transformations de cette structure,

- la définissabilité logique consiste à décrire une (ou des) structure(s) comme le (ou les) modèle(s) d'une formule dans une logique donnée. Peu de résultats sont connus dans ce domaine (e.g. Blumensath).

Historiquement, les travaux de Müller et Schupp sur les graphes des automates à pile ont initié les recherches sur les familles de structures infinies. La représentation que les auteurs choisissent est interne: chaque sommet d'un graphe est la configuration d'un automate à pile (au sens classique de la théorie des langages), et ce graphe contient un arc entre deux sommets si une transition de l'automate permet de passer de la configuration du premier à celle du second. Les auteurs montrent par une analyse géométrique que ces graphes ont une théorie monadique décidable. Des résultats ultérieurs de Caucal montrent qu'il est possible de représenter ces graphes par transformations. Cette représentation donne une démonstration simplifiée du résultat de décidabilité de la théorie monadique.

Les travaux de Courcelle furent quant à eux inspirés par l'approche algébrique. Il adapte les opérateurs HR pour traiter les structures d'univers dénombrable. En particulier, il s'agit de rendre ces opérateurs continus. Les graphes HR-équationnels sont alors définis comme les solutions de systèmes finis d'équations utilisant ces opérateurs. Courcelle montre que ces structures ont une théorie au second ordre gardé décidable.

Enfin, Caucal décrit la famille des graphes préfixes reconnaissables par des systèmes de récriture de mots et par transformation d'un graphe particulier. Une conséquence directe de cette caractérisation est la décidabilité de leur théorie monadique. Barthelmann montre que cette famille de graphes admet une représentation équationnelle au moyen des opérateurs VR, en fait, l'extension naturelle aux graphes infinis des opérateurs VR. Barthelmann montre aussi que les graphes de cette famille possédant une largeur arborescente bornée sont exactement les graphes HR-équationnels. Blumensath donne quant-à lui une représentation par définissablité en logique du second ordre gardée de cette même famille.

Toutes ces familles partagent une représentation à base de pile. Ce n'est plus le cas des structures ci-dessous.

Les structures automatiques ont été introduites par Senizergues puis Khoussainov et Nerode. Elles sont décrites au moyen d'une représentation interne. Chaque élément de l'univers est un mot, et les relations associées aux symboles sont décrites par des relations synchronisées. Ces structures possèdent une théorie au premier ordre décidable.
Elles sont étendues aux structures termes-automatiques par Blumensath et Grädel. Des définitions antérieures semblabes peuvent être trouvées dans les tra vaux de Dauchet et Tison. Nous verrons dans ce travail qu'il est possible de donner une représentation équationnelle à cette famille de structures. Toutes ces familles possèdent une théorie au premier ordre décidable.

Enfin, les familles de graphes décrites par récriture suffixe de termes sont intro duites par Löding. Là encore, des familles similaires antérieures ont été étudiées par Dauchet et Tison. Löding montre que, quand restreints aux graphes de lar geur arborescente bornée, ces graphes coïncident avec les graphes des automates à piles de Müller et Schupp.

## Contributions

Le présent travail étudie la plupart des familles de structures précédemment décrites sous l'angle des systèmes d'équations.

Pour cette raison, la première adaptation concerne les transducteurs déter-ministes avec anticipations; il s'agit d'un outil permettant de transformer les systèmes d'équations. Ces transducteurs ont étés étudiés en détail dans le cadre des termes finis, et nous adaptons cet outil au cas des termes infinis. Ces tra vaux recouvrent partiellement le contenu d'une collaboration entre C. Löding et l'auteur [CL04]. Il s'agit de l'outil essentiel utilisé dans le reste du mémoire.

La seconde contribution (chapitre 4) concerne plusieurs équivalences généralisant des résultats connus sur les graphes préfixes reconnaissables; en particulier, la possibilité d'ajouter un opérateur de fusion dans les systèmes d'équations VR. Il s'agit d'une collaboration entre A. Carayol et l'auteur [CC03]. Nous redémontrons aussi le résultat de Barthelmann concernant les graphes préfixes reconnaissables de largeur arborescente bornée en utilisant les transducteurs déterministes.

La troisième contribution n'a pas fait l'objet de publication; il s'agit d'une représentation équationnelle de la famille des graphes dits terme-automatiques. Elle est au cœur du chapitre 5.

La quatrième et dernière contribution concerne l'introduction de la famille des graphes VRA-équationnels (chapitre 6), des différentes représentations qui peuvent en être données ainsi que de ses propriétés géométriques. Cette famille admet une représentation interne sous forme de système de récriture suffixe de termes (elle est donc similaire à la famille de graphes introduits par Löding, bien que les deux soient incomparables). Nous montrons ici que cette famille restreinte aux graphes de largeur arborescente bornée coïncide avec la famille des graphes HR-équationnels. Ces résultats ont été partiellement publiés dans [Col02a]. Enfin, nous établissons qu'une extension de ce résultat aux graphes de largeur de clique bornée n'est pas vérifiée. Ce dernier résultat est aussi issu d'une collaboration entre C. Löding et l'auteur.
L'auteur s'est aussi intéressé au cours de sa thèse aux systèmes de récriture de termes modulo associativité et commutativité [Col02b], ainsi qu'au sujet plus éloigné de la programmation par aspects en collaboration avec P. Fradet [CF00]. Ces travaux ne sont pas présentés dans ce document.

# Plan

Le reste de ce mémoire est découpé en cinq chapitres.

Le chapitre 2 présente les définitions de base concernant les structures, les graphes, la logique et les propriétés géométriques de graphes.

Le chapitre 3 est dédié à l'étude de systèmes d'équations. On s'intéresse tout particulièrement au développement d'outils permettant de manipuler ces systèmes : les transducteurs déterministes.

Le chapitre 4 commence l'étude des structures et des graphes infinis proprement dite. Il a trait aux structures pouvant être décrites par récriture suffixe (ou préfixe) de mots; chaque élément de l'univers est un mot, et une relation relie plusieurs mots si ceux-ci s'obtiennent les uns des autres par remplacement suffixe (resp. préfixe). Ces familles de structures admettent des représentations internes, équationnelles et par transformations, et nous établissons ces équivalences. Certains résultats présentés sont déjà connus dans le contexte des structures finies et des systèmes d'équations finis. Le principal apport consiste en une utilisation systématique des transducteurs déterministes permettant d'étendre ces résultats aux systèmes d'équations infinis.

Le chapitre 5 étudie une famille de structures dont l'univers est un ensemble de termes finis, et dont les relations sont décrites au moyens d'automates. Il s'agit des structures terme-automatiques. Nous donnons, là encore, une triple équivalence de représentations pour ces structures.

Le chapitre 6 s'intéresse aux graphes dont les sommets sont des termes, et dont les arcs sont décrits par récriture suffixe, c'est-à-dire en remplaçant un sous-terme par un autre. Nous établissons l'équivalence entre une représentation équationnelle et une représentation interne de ces graphes, et nous nous intéressons à une étude géométrique de cette famille.
# Chapitre 2

## Définitions et notions de base

La notion de structure relationnelle est issue de la logique et en particulier de la théorie des modèles. Une structure est formée d'un ensemble d'éléments, son univers, et de relations liant ces éléments.

Les structures relationnelles peuvent donc être vues comme des sortes de bases de données relationnelles. La différence est que les structures relationnelles ne sont pas étudiées sous l'angle du stockage d'information, mais plutôt dans l'optique d'étudier les interactions entre relations. Dans le cas présent, la vision base de données disparaît totalement puisque l'on s'intéresse à des structures infinies.

Les structures relationnelles peuvent aussi être vues comme une généralisation de la notion de graphe : l'ensemble des sommets est l'univers et les arcs sont représentés par des relations binaires. Sous cet angle, il est souvent fait référence à la notion d'*hypergraphe*. On parle alors d'hyperarcs reliant *n* sommets au lieu d'arcs (qui n'en relient que deux).

Dans la suite de ce travail, il est question de structures plutôt que d'hyper-graphes bien que certaines terminologies seront empruntées à ces derniers. Il s'agit d'un choix arbitraire qui dénote une orientation plus logique qu'algorithmique des résultats présentés. En revanche, la plupart des exemples seront puisés dans les graphes ; ces derniers possèdent l'avantage d'être plus aisément représentables.

Le reste de ce chapitre est décomposé comme suit. Nous commençons par introduire les définitions de structures, graphes et termes au paragraphe 2.1. Puis au paragraphe 2.2 nous présentons les formalismes logiques qui nous seront utiles par la suite. Nous introduirons alors diverses transformations de structures et de graphes au paragraphe 2.3. Enfin, le paragraphe 2.4 à pour but de présenter des critères géométriques permettant d'étudier les graphes infinis.
## 2.1 Structures

Nous présentons dans ce paragraphe la notion de structure et la terminologie s'y rattachant ainsi que les variantes que sont les graphes, les automates, les arbres et les termes.

### 2.1.1 Cas général

Une *signature* est un ensemble fini $\Sigma$ de *symboles relationnels*, chaque symbole $R$ possédant une *arité* entière notée $|R|$. Une *structure relationnelle* (ou plus simplement une structure) $\mathcal{S}$ sur une signature $\Sigma$ est une paire $(\mathcal{U}, \mathcal{Vals})$ où $\mathcal{U}$ est un ensemble appelé *univers*, et $\mathcal{Vals}$ est une application associant à chaque symbole $R$ de la signature son *interprétation*, c'est à dire une partie de $\mathcal{U}^{|R|}$. Nous employerons dorénavant la notation classique $\mathcal{U}_S$ pour représenter l'univers de la structure $\mathcal{S}$, et $\mathcal{R}^S$ en lieu et place de $\mathcal{Vals}(R)$. De plus, pour $u_1, \dots, u_{|R|}$ éléments de l'univers, on note $\mathcal{R}^S(u_1, \dots, u_{|R|})$ au lieu de $(u_1, \dots, u_{|R|}) \in \mathcal{R}^S$. On dit dans ce cas qu'un *hyperarc* $R$ relie les éléments $u_1, \dots, u_{|R|}$.

La notion de signature est pratique dans les définitions mais devient rapidement gênante à l'usage. En particulier, il est fréquent de vouloir que les signatures de différentes structures soient égales. Cela permet par exemple de comparer ou de combiner des structures. On définit donc l'extension d'une structure à une nouvelle signature (plus grande) en fixant pour tous les nouveaux symboles une interprétation vide. On suppose implicitement qu'une telle extension est effectuée quand nécessaire. Ainsi, étant données deux structures, il est toujours possible de les considérer comme de même signature (en les étendant toutes deux à l'union de leur signature). Une conséquence de ce choix est que lorsque l'on parle d'un symbole sans préciser la signature dont il est issu, cela signifie qu'il appartient à une signature étendant les signatures de toutes les structures en présence. Un autre abus du même ordre consiste à considérer des structures sur une signature infinie. En réalité, il s'agit de structures de signature finie contenue dans la signature infinie.

Une *structure avec quotient* $\mathcal{S}$ est une structure sur une signature contenant un symbole binaire $\sim$ (de notation infixe) et telle que l'interprétation de $\sim$ est une congruence pour toutes les relations de la structure. Plus précisément, $\sim^S$ est une relation d'équivalence sur $\mathcal{U}_S$ et pour tout symbole relationnel $R$ d'arité $n$ et tous éléments $u_1 \sim^S v_1, \dots, u_n \sim^S v_n, \mathcal{R}^S(u_1, \dots, u_n)$ si et seulement si $\mathcal{R}^S(v_1, \dots, v_n)$.

Un *isomorphisme* de structures avec quotient entre $\mathcal{S}$ et $\mathcal{S}'$ est une relation $\Upsilon \subseteq \mathcal{U}_S \times \mathcal{U}_{S'}$ telle que pour tout symbole relationnel $R$ d'arité $n$ (éventuellement $\sim$) et tous $E(u_1, v_1), \dots, E(u_n, v_n), \mathcal{R}^S(u_1, \dots, u_n)$ si et seulement si $\mathcal{R}^S(v_1, \dots, v_n)$. On note alors $\mathcal{S} \approx_{\Upsilon} \mathcal{S}'$ et on dit que $\mathcal{S}$ et $\mathcal{S}'$ sont isomorphes si il existe un tel isomorphisme. La notation $\mathcal{S} \approx \mathcal{S}'$ est utilisée quand l'isomorphisme
n'a pas d'importance. Toute structure est isomorphe à elle même, et l'isomorphisme correspondant est simplement l'interprétation de $\sim$. Plus généralement la relation $\approx$ est une relation d'équivalence entre structures avec quotient.

Étant donnée une structure avec quotient $\mathcal{S}$, il lui est associée sa structure quotient $\mathcal{S}_{/\sim}$ dont l'univers est l'ensemble des classes d'équivalences de $\sim^\mathcal{S}$, et dont l'interprétation d'un symbole $R$ d'arité $n$ est l'ensemble des $(c_1, \dots, c_n)$ tels qu'il existe $u_1 \in c_1, \dots, u_n \in c_n$ vérifiant $R^\mathcal{S}(u_1, \dots, u_n)$. La définition d'une structure avec quotient est telle qu'il est équivalent de définir l'interprétation de $R$ comme l'ensemble des $(c_1, \dots, c_n)$ tels que pour tout $u_1 \in c_1, \dots, u_n \in c_n$ on a $R^\mathcal{S}(u_1, \dots, u_n)$. La relation qui à chaque élément associe sa classe déquivalence est alors un isomorphisme entre $\mathcal{S}$ et $\mathcal{S}_{/\sim}$.

Les structures sans quotient s'identifient au cas particulier des structures avec quotient pour lesquelles l'interprétation de $\sim$ est simplement l'identité. Cette équivalence est implicite dans la suite de ce travail et le choix de la présence d'un quotient dépend du contexte. Remarquons que pour toute structure avec quotient, sa structure quotient est en ce sens une structure sans quotient. Pour finir, notons que dans le cas des structures sans quotient, un isomorphisme de structure est bien une bijection entre univers comme on peut s'y attendre.

## 2.1.2 Graphes

Les graphes sont définis dans ce travail comme des cas particuliers de structures. Étant donné un alphabet $A$ d'étiquettes $a,b, \dots$, un graphe $\mathcal{G}$ est une structure de signature $\{\xrightarrow{a} | a \in A\}$, où chaque symbole $\xrightarrow{a}$ est binaire. L'univers d'un graphe est noté $V_{\mathcal{G}}$ et ses éléments se nomment sommets. La notation $(\xrightarrow{a})^{\mathcal{G}}(s, s')$ est remplacée par $s \xrightarrow{a} s'$ et on dit qu'il y a un arc étiqueté par $a$ entre $s$ et $s'$. Un arc d'un sommet vers lui-même est appelé une boucle.

Un graphe $\mathcal{G}$ est déterministe si pour tout sommet $s$ et toute étiquette $a$, il existe au plus un sommet $s'$ tel que $s \xrightarrow{a} s'$. Un graphe est co-déterministe si le graphe obtenu en retournant tous les arcs est déterministe, c'est à dire que pour tout sommet $s$ et toute étiquette $a$, il existe au plus un $s'$ tel que $s' \xrightarrow{a} s$. Le degré sortant $d^+(s)$ d'un sommet $s$ dans un graphe $\mathcal{G}$ est le nombre d'arcs qui en sont issus. Il peut avoir une valeur dans $\mathbb{N}$ ou $\infty$ s'il existe une infinité de tels arcs. Formellement, $d^+(s)$ est le cardinal de $\{(a, s') \in A \times V_{\mathcal{G}} | s \xrightarrow{\mathcal{G}} s'\}$. Le degré entrant $d^-(s)$ se définit similairement comme le cardinal de $\{(s', a) \in V_{\mathcal{G}} \times A | s' \xrightarrow{a} s\}$. Le degré $d(s)$ d'un sommet $s$ est la somme de ses degrés entrants et sortants.

Un chemin dans un graphe est un mot $\pi = s_0 a_1 s_1 \dots a_n s_n$ de $V_{\mathcal{G}}(AV_{\mathcal{G}})^*$ tel que pour tout $i$ entre 1 et $n$, $s_{i-1} \xrightarrow{a_i} s_i$. Le sommet $s_0$ est l'origine du chemin, noté $\text{orig}(\pi)$, et $s_n$ sa destination notée $\text{dest}(\pi)$. On s'intéresse aussi aux étiquettes
<figure><img src="image_4.png" /><figcaption>FIG. 2.1 – La demi-droite des entiers enracinée $\Delta_1$.</figcaption></figure>

apparaissant sur un chemin, c'est à dire au mot $a_1a_2...a_n$. Pour un mot $w$ de $A^*$, la notation $s \xrightarrow{w} s'$ désigne l'existence d'un chemin étiqueté par $w$ entre $s$ et $s'$.

Étant donnés un graphe $\mathcal{G}$ et deux ensembles de sommets $I \subseteq V_{\mathcal{G}}$ et $F \subseteq V_{\mathcal{G}}$, on appelle *trace de $\mathcal{G}$* entre $I$ et $F$ le langage $\mathcal{L}_{I,F}(\mathcal{G})$ défini par

$$ \mathcal{L}_{I,F}(\mathcal{G}) = \{w \mid \exists s \in I, \exists s' \in F, s \xrightarrow{w} s'\}. $$

Dans le cas d'un graphe fini $\mathcal{G}$, pour tout $I$ et tout $F$, $\mathcal{L}_{I,F}(\mathcal{G})$ est un langage rationnel. Ce n'est plus nécessairement le cas si le graphe est infini.

Un graphe $\mathcal{G}$ est *enraciné* si en plus de sa signature normale de graphe, il possède un symbole unaire *racine* interprété comme un singleton. Par abus de notation, on identifie *racine*$^\mathcal{G}$ avec son seul élément et on appelle cet élément la *racine* du graphe. Graphiquement, ce sommet est identifié par une flèche entrante. Un sommet d'un graphe enraciné est *accessible* si il existe un chemin d'origine *racine* dont il est la destination.

**Exemple 2.1** La figure 2.1 présente la demi-droite des entiers enracinée $\Delta_1$, c'est-à-dire le graphe enraciné de sommets $V = \mathbb{N}$, de racine 0, et dont les arcs étiquetés par $a$ sont :

$$ \xrightarrow{a} \Delta_1 = \{(n, n+1) \mid n \in \mathbb{N}\}. $$

Ce graphe est déterministe et co-déterministe. Il existe un chemin entre deux sommets $n$ et $n'$ si et seulement si $n \le n'$ et ce chemin est étiqueté par le mot $a^{n'-n}$.

### 2.1.3 Les automates

Un automate est un graphe servant de description pour un langage.

Formellement, un automate $\mathcal{A}$ est un graphe enraciné dont la signature est enrichie d'un symbole unaire *final*. Les sommets $s$ tels que $final^\mathcal{A}(s)$ sont appelés sommets *finaux* et sont graphiquement représentés par une flèche sortante. Le langage accepté par un automate d'étiquettes $\mathcal{A}$ est le langage $\mathcal{L}(\mathcal{A})$ de $A^*$ défini par :

$$ \mathcal{L}(\mathcal{A}) = \mathcal{L}_{\text{racine}^\mathcal{A}, \text{final}^\mathcal{A}}(\mathcal{A}) = \{w \mid \exists s \in V_{\mathcal{A}}. \text{racine}^\mathcal{A} \xrightarrow{w} s, \text{final}^\mathcal{A}(s)\}. $$

**Exemple 2.2** La figure 2.2 représente un automate infini, appelé l'escabeau. Le langage qu'il accepte est $\{a^n b^{n+1} c^n \mid n \in \mathbb{N}\}$.
<figure><img src="image_5.png" /><figcaption>FIG. 2.2 – *Un automate.*</figcaption></figure>

### 2.1.4 Arbres et termes

<figure><img src="image_6.png" /><figcaption>FIG. 2.3 – *L’arbre binaire complet, définition (a) et représentation (b).*</figcaption></figure>

Les arbres sont des cas particuliers de graphes enracinés satisfaisant de plus que tout sommet est destination d’un et un seul chemin à partir de la racine. Les sommets d’un arbre sont appelés nœuds. Si pour une certaine étiquette a, deux nœuds s et s’ satisfont $s \xrightarrow{a} s'$ alors on dit que s est le père de s’ (il ne peut en exister qu’un d’après la définition d’un arbre) et que s’ est un fils de s. Si un nœud n’a pas de fils, alors il s’agit d’une feuille de l’arbre.

**Exemple 2.3** *Un exemple important d’arbre infini est l’arbre binaire complet, noté $\Delta_2$ et présenté à la figure 2.3.*

On appelle *branche* d'un arbre, un ensemble maximal (pour l'inclusion) de
nœuds contenant la racine et tel que tout élément de l'ensemble ne possède au plus qu'un fils dans l'ensemble. Le langage des branches d'un arbre t étiqueté sur A, noté $\mathcal{LB}(t)$ est l'ensemble

$$ \mathcal{LB}(t) = \{ w \in A^* \mid \exists u \in V_t, \text{ racine } t \xrightarrow{w} u \} . $$

Les branches d'un arbre apportent une information importante sur celui-ci. En fait, sous l'hypothèse de déterminisme, ce langage s'identifie à l'ensemble des nœuds de l'arbre comme le montre la propriété suivante.

**Propriété 2.4** *Tout arbre déterministe $t$ est isomorphe au graphe enraciné de sommets $\mathcal{LB}(t)$, de racine $\varepsilon$ et dont les arcs étiquetés par $a$ sont définis par :*

$$ \xrightarrow{a} = \{(w, wa) \mid w \in \mathcal{LB}(t), wa \in \mathcal{LB}(t)\} . $$

**Corollaire 2.5** *Pour tout ensemble d'étiquettes A, l'application $\mathcal{LB}$ est une bijection entre les arbres déterministes étiquetés par A et les langages de $A^*$ clos par préfixe.*

Cette propriété permet de manipuler les arbres déterministes comme des langages et de manipuler les nœuds comme des mots de ce langage.

Il s'agit maintenant de définir ce qu'est un terme. Pour cela, il est nécessaire de disposer de symboles fonctionnels. Un symbole fonctionnel $f$ est un symbole accompagné d'une arité notée $|f|$ qui est un entier naturel. On note souvent lors de l'introduction de ces symboles $f:n$ pour préciser que l'arité de $f$ est $n$. Les symboles fonctionnels ne doivent pas être confondus avec les symboles relationnels qui eux sont notés en lettres capitales. Un alphabet gradué est un ensemble fini de symboles fonctionnels. Les définitions qui suivent permettent de donner un sens à un terme comme $f(g(a), b)$ sur l'alphabet gradué $\{f:2, g:1, a:0, b:0\}$.

Un terme sur un alphabet gradué $\mathcal{F}$ (ou plus simplement un $\mathcal{F}$-terme) est un arbre $t$ étiqueté par $\mathcal{F} \uplus \mathbb{N}$ et satisfaisant les trois conditions suivantes :

- il existe un arc étiqueté par une lettre de $\mathcal{F}$ issu de la racine de l'arbre,

- pour tout arc $s \xrightarrow{f} s'$ avec $f \in \mathcal{F}$, alors, il s'agit du seul arc d'origine $s$, et il existe exactement $|f|$ arcs issus de $s'$ étiquetés respectivement par 1, ..., $|f|$,

- pour tout arc $s \xrightarrow{n} s'$ avec $n \in \mathbb{N}$, il existe un arc étiqueté par une lettre de $\mathcal{F}$ issu de $s'$.

L'ensemble des termes, finis ou infinis, sur l'alphabet $\mathcal{F}$ est noté $\mathcal{T}^\omega(\mathcal{F})$. L'ensemble des termes finis sur $\mathcal{F}$ est noté $\mathcal{T}(\mathcal{F})$.

Dans cette définition des termes, deux types de sommets apparaissent : ceux origine des lettres de $\mathcal{F}$ et ceux destination de tels arcs. On appelle les premiers sommets principaux. Étant donné un terme $t$ et $v$ un de ses sommets principaux,
En utilisant la représentation par langage de branches des termes, on obtient une
définition équivalente beaucoup plus simple :

$$
\mathcal{LB}(f(t_1, \dots, t_{|f|})) = \varepsilon + f + f1\mathcal{LB}(t_1) + \dots + f|f|\mathcal{LB}(t_{|f|}).
$$

Cette construction permet d'associer un terme fini à toute expression bien
formée à partir d'un alphabet gradué. En fait, la réciproque est aussi vraie : à
tout terme fini sur un alphabet gradué correspond une unique expression bien
formée sur cet alphabet. Pour cette raison, on dit que l'algèbre des termes finis
est libre. Cette propriété sera présentée plus en détail au paragraphe 3.1.3.

2.2 Logiques

Les logiques permettent d'exprimer des propriétés sur les structures. De nom-
breux formalismes existent permettant de disposer d'une grande diversité d'ex-
pressivités. Dans ce travail, nous nous concentrons sur la logique du premier ordre
(paragraphe 2.2.1) sur la logique du second ordre monadique (paragraphe 2.2.2)
et quelques-unes de ses variantes (paragraphe 2.2.3). Enfin, nous présenterons
la construction de Feferman-Vaught qui permet la décomposition de formules
logiques (paragraphe 2.2.4).

2.2.1 Logique du premier ordre

On se fixe un ensemble dénombrable V de variables du premier ordre notées
x,y ... Étant donnée une signature Σ, les formules du premier ordre sur Σ (on
omet le plus souvent de préciser la signature Σ quand il n'y a pas d'ambiguïtés.)
sont définies récursivement au moyen des construction ci-dessous :

la constante vraie : vrai ,

la conjonction : $\phi \land \psi$ où $\phi$ et $\psi$ sont des formules du premier ordre,

la négation : ¬φ où φ est une formule,

la quantification existentielle du premier ordre : ∃x.φ où x est une variable du
premier ordre et φ une formule du premier ordre,

l'égalité de variables du premier ordre : x = y avec x et y variables du premier ordre,

la relation entre variables du premier ordre : R(x₁, ..., x|R) où R est un symbole relationnel de Σ et x₁, ..., x|R sont des variables du premier ordre.

Les autres connecteurs classiques ne sont que des combinaisons des précédents :

la constante fausse : faux équivaut à ¬vrai ,

la disjontion : $\phi \lor \psi$ équivaut à $\neg((\neg\phi) \land (\neg\psi))$ ,

l'implication : $\phi \Rightarrow \psi$ équivaut à $(\neg\phi) \lor \psi$ ,
l'équivalence : $\phi \Leftrightarrow \psi$ équivaut à $(\phi \Rightarrow \psi) \land (\psi \Rightarrow \phi)$,

la quantification universelle du premier ordre : $\forall x. \phi$ équivaut à $\neg(\exists x.\neg\phi)$.

Étant donnée une formule $\phi$, on définit l'ensemble $FV(\phi)$ des variables libres par récurrence sur la structure de $\phi$ comme suit :

$$
\begin{align*}
FV(\mathbf{vrai}) &= \emptyset & FV(\phi \land \psi) &= FV(\phi) \cup FV(\psi) \\
FV(\neg\phi) &= FV(\phi) & FV(\exists x.\phi) &= FV(\phi) - \{x\} \\
FV(x = y) &= \{x, y\} & FV(R(x_1, \dots, x_{|R|})) &= \{x_1, \dots, x_{|R|}\}.
\end{align*}
$$

Une formule est *close* si elle n'a aucune variable libre. Par abus de langage et pour un ensemble $V \subseteq \mathcal{V}$ de noms de variables, on dit qu'une formule $\phi$ a pour variables libres $V$ si $V$ contient $FV(\phi)$.

Étant donnée une structure $\mathcal{S}$, une formule du premier ordre $\phi$ de variables libres $V$ et une application $\gamma$ de $V$ dans $\mathcal{U}_\mathcal{S}$ appelée *valuation*, on définit par récurrence sur $\phi$ la relation de satisfaction de $\phi$ par $\mathcal{S}$ dans le contexte $\gamma$, notée $\gamma, \mathcal{S} \models \phi$ comme suit.

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\gamma, \mathcal{S} & \models & \mathbf{vrai}, \\
\gamma, \mathcal{S} & \models & \phi \land \psi & \text{si } \gamma, \mathcal{S} \models \phi \text{ et } \gamma, \mathcal{S} \models \psi, \\
\gamma, \mathcal{S} & \models & \neg\phi & \text{si } \gamma, \mathcal{S} \not\models \phi, \\
\gamma, \mathcal{S} & \models & R(x_1, \dots, x_{|R|}) & \text{si } R^{\mathcal{S}}(\gamma(x_1), \dots, \gamma(x_{|R|})) , \\
\gamma, \mathcal{S} & \models & x = y & \text{si } \gamma(x) = \gamma(y), \\
\gamma, \mathcal{S} & \models & \exists x.\phi & \text{si il existe } u \in \mathcal{U}_{\mathcal{S}} \text{ tel que } \gamma, x \to u, \mathcal{S} \models \phi \\
& & & \quad \text{où } \gamma, x \to u \text{ représente la fonction partout égale} \\
& & & \quad \text{à } \gamma \text{ sauf pour } x \text{ où elle vaut } u.
\end{array}
$$

Pour $\phi$ une formule close, si $\emptyset, \mathcal{S} \models \phi$ ($\emptyset$ représente la seule application de domaine $\emptyset$), on dit que $\mathcal{S}$ est un modèle de $\phi$ ou plus simplement que $\mathcal{S}$ satisfait $\phi$. On le note simplement $\mathcal{S} \models \phi$. Une structure $\mathcal{S}$ possède une théorie au premier ordre décidable s'il existe un algorithme prenant en entrée une formule close $\phi$ et décide de sa satisfaction par $\mathcal{S}$.

Il est parfois utile de rendre explicite les variables libres d'une formule. Ainsi, on notera $\phi(x_1, \dots, x_n)$ une formule logique de variables libres $x_1, \dots, x_n$. De plus, on s'autorisera de noter $\mathcal{S} \models \phi(u_1, \dots, u_n)$ pour une structure $\mathcal{S}$ et $n$ éléments de son univers $u_1, \dots, u_n$ à la place de $\gamma, \mathcal{S} \models \phi(x_1, \dots, x_n)$ avec pour tout $i \in [n]$, $\gamma(x_i) = u_i$.

**Exemple 2.6** À titre d'exemple, nous donnons une formule du premier ordre qui exprime le fait, pour un graphe, d'être déterministe, c'est à dire que tout graphe $\mathcal{G}$ étiqueté par $A$ est déterministe si et seulement si $\mathcal{G} \models \text{deterministe}[A]$ avec

$$
\text{deterministe}[A] = \bigwedge_{a \in A} \forall x. \forall y. \forall z. \left( (x \xrightarrow{a} y \land x \xrightarrow{a} z) \Rightarrow y = z \right) .
$$
On remarque sur cet exemple que l'on s'autorise quelques raccourcis de notation,
en particulier l'usage de $\wedge$ n'a de sens que parce que $\wedge$ est associatif et com-
mutatif. Il est donc possible de laisser non spécifié l'ordre sur $A$ ainsi que le
parenthésage.

Différents sous-ensembles de la logique du premier ordre jouent un rôle parti-
culier dans le reste de ce travail. En voici la liste :

- les *expressions booléennes* (ou *formules booléennes*) sont des formules sans quantificateur, elles sont formées des connecteurs $\wedge$, $\vee$ et $\neg$, des constantes *vrai* et *faux*, et des prédicats de relations $R(x_1, \dots, x_{|R|})$,

- les *expressions booléennes positives* (ou *formules booléennes positives*) sont des expressions booléennes sans négation. Elles sont donc formées uniquement des connecteurs $\wedge$ et $\vee$, des constantes *vrai* et *faux*, et des prédicats de relations $R(x_1, \dots, x_{|R|})$,

- les *formules existentielles* sont des formules sans quantification universelle et sans négation. Elles sont donc formées des connecteurs $\wedge$ et $\vee$, des constantes *vrai* et *faux*, des prédicats de relations $R(x_1, \dots, x_{|R|})$ et de la quantification existentielle $\exists$.

2.2.2 Logique monadique

La logique monadique étend la logique du premier ordre par des variables
interprétées comme des parties de l'univers. Il est possible de quantifier existen-
tiellement et universellement sur ces ensembles. Cela correspond à une importante
augmentation d'expressivité par rapport à la logique du premier ordre. La termi-
nologie de logique monadique est en fait une simplification remplaçant l'expres-
sion «logique au second ordre monadique» qui signifie que l'utilisation du second
ordre est restreinte au cas monadique, c'est à dire aux ensembles. Cette logique
pourrait aussi être qualifiée de «premier ordre ensembliste», une dénomination
rendant sa nature plus explicite.

On se fixe un ensemble dénombrable $V_m$ de variables du second ordre monadique (ou plus simplement de variables monadiques). Elles sont notées en lettres capitales : $X, Y \dots$ Les formules de logique monadique (ou plus simplement formules monadiques) sont les formules du premier ordre étendues par la quantification existentielle du second ordre monadique $\exists X.\Phi$ et la proposition atomique d'appartenance $x \in X$. Comme précédemment, on s'autorise à utiliser la quantification universelle du second ordre monadique $\forall X.\Phi$ comme un raccourci équivalent à $\neg\exists X.\neg\Phi$.

Les définitions du paragraphe précédent sont réutilisables sans grandes mo-
difications. Ainsi, les variables libres peuvent être monadiques tout autant que
du premier ordre. La relation $\gamma, S \models \Phi$ est quant à elle étendue de la manière
suivante: le contexte $\gamma$, en plus de toujours associer à chaque variable libre du premier ordre un élément de l'univers, associe à chaque variable monadique un sous-ensemble de l'univers. La définition de la satisfaction est alors complétée par les règles suivantes :

$$ 
\begin{array}{ll}
\gamma, \mathcal{S} \models \exists X.\Phi & \text{s'il existe } U \subseteq \mathcal{U}_{\mathcal{S}} \text{ tel que } \gamma, X \to U, \mathcal{S} \models \Phi, \\
\gamma, \mathcal{S} \models x \in X & \text{si } \gamma(x) \in \gamma(X).
\end{array}
$$

**Exemple 2.7** À titre d'exemple, nous présentons une formule de la logique monadique dont la satisfaction équivaut à la forte connexité d'un graphe étiqueté par A. Cette formule exprime le fait que tout ensemble non vide de sommets clos par les relations arc contient tous les sommets du graphe.

$$ \mathbf{f-connexite}[A] = \forall X. \left( X \neq \emptyset \land \forall x \in X. \forall y. \bigwedge_{a \in A} (x \xrightarrow{a} y \Rightarrow y \in X) \right) \Rightarrow (\forall x. x \in X). $$

Là encore, il y a un abus de notation : l'usage de $\emptyset$. Plus généralement, on s'autorise à utiliser les opérateurs ensemblistes (union, intersection, complémentaire, vide) et les comparaisons (égalité, inclusion). Bien entendu, toutes ces opérations peuvent être traduites en formules monadiques.

L'exemple suivant généralise cette technique et montre qu'il est possible d'exprimer en logique monadique le fait pour deux sommets d'être reliés par un chemin étiqueté par un mot appartenant à un langage rationnel donné.

**Exemple 2.8 (accessibilité rationnelle)** Pour L un langage rationnel, la formule de logique monadique accessible$[L](x, y)$ est définie par récurrence sur la définition de L :

si $L = \emptyset$ alors accessible$[\emptyset](x, y) = \text{faux}$ car aucun mot n'appartient à L,

si $L = \{\varepsilon\}$ alors accessible$[\varepsilon](x, y) = (x = y)$ car le seul mot de L est le mot vide, et qu'il n'existe un chemin étiqueté par le mot vide entre deux sommets que si ceux-ci sont égaux,

si $L = a$ alors accessible$[a](x, y) = x \xrightarrow{a} y$ car il existe un chemin étiqueté par $a$ entre deux sommets ssi ceux-ci sont reliés par un arc étiqueté par $a$,

si $L = L' + L''$ alors

$$ \text{accessibilite}[L' + L'')(x, y) = \text{accessibilite}[L')(x, y) \lor \text{accessibilite}[L'')(x, y). $$

En effet, il existe un chemin étiqueté par un mot de L entre x et y s'il existe un mot de $L'$ étiquetant un chemin reliant ces deux sommets, ou bien s'il existe un mot de $L''$ étiquetant un chemin reliant ces deux sommets,
si $L = L'.L''$ alors similairement,

$$ \text{accessibilite}[L'.L''](x, y) = \\ \exists z. \text{accessibilite}[L'](x, z) \wedge \text{accessibilite}[L''](z, y), $$

enfin si $L = L'^*$ alors on pose

$$ \text{accessibilite}[L'^*](x, y) = \\ \forall X. \left( \begin{array}{l} x \in X \\ \wedge \quad \forall z. \forall z'. (z \in X \wedge \text{accessibilite}[L'](z, z')) \\ \Rightarrow z' \in X) \end{array} \right) \\ \Rightarrow y \in X. $$

Cette formule exprime le fait que tout ensemble $X$ de sommets du graphe close par la relation $\text{accessibilite}[L']$ et contenant $x$ doit aussi contenir $y$.

Deux résultats fondamentaux de l'informatique théorique ont ouvert la voie à l'étude de la théorie monadique sur les structures infinies. Il s'agit tout d'abord du résultat de Büchi [Büc60], puis de son extension par Rabin [Rab69].

**Théorème 1 (Büchi)** La demi-droite des entiers à une théorie monadique décidable.

**Théorème 2 (Rabin)** L'arbre binaire complet à une théorie monadique décidable.

Ces deux démonstrations sont complexes. Une preuve détaillée de ces résultats ainsi que des références sur le sujet se trouvent dans les travaux de Thomas [Tho97]. Des résultats similaires seront aussi énoncés dans le contexte du $\mu$-calcul (voir théorème 9).

D'autres techniques permettent de montrer l'indécidabilité de la théorie monadique sur certaines structures. Citons deux résultats classiques de cet ordre. Le premier fait référence à la *grille infinie*, qui se définit comme le graphe de sommets $N \times N$ et tel que les arcs (non étiquetés) ont pour interprétation $\{((i, j), (i, j+1)) \mid i, j \in N\} \cup \{((i, j), (i+1, j)) \mid i, j \in N\}$.

**Propriété 2.9** La grille infinie à une théorie monadique indécidable.

La démonstration de ce résultat peut s'obtenir par réduction du problème de l'arrêt des machines de Turing. Étant donnée une telle machine, on code son exécution de la manière suivante: chaque ruban de la machine correspond à une ligne de la grille. Passer d'une ligne à la suivante correspond à une étape d'exécution de la machine. Une formule monadique est alors capable de déterminer si la machine de Turing atteint un état final ou non. Ainsi, pour toute machine de Turing, il
existe une formule monadique telle que la grille infinie en est un modèle si et seulement si la machine s’arrête.

**Propriété 2.10** *La structure ayant les entiers naturels comme univers et munie des relations «plus 1» et «fois deux» a une théorie monadique indécidable.*

En fait, cette propriété est plus délicate à obtenir que la précédente mais fonctionne sur le même principe. Il s'agit de retrouver dans la structure une famille de grilles aussi grande que l'on veut (dans les deux dimensions).

Un dernier cas de structure possédant une théorie monadique indécidable est donné par la propriété 2.11

**Propriété 2.11** *L'union disjointe de tous les graphes finis étiquetés par un ensemble non vide a une théorie monadique indécidable.*

Ce résultat s'obtient en montrant qu'il est possible de reconnaître les grilles rec-
tangulaires au sein de ces graphes. Là encore, chaque grille est susceptible d'être
utilisée comme support de calcul d'une machine de Turing. La largeur de la grille
correspond à la longueur du ruban utilisé durant l'exécution, et la hauteur cor-
respond au nombre d'étapes de calcul.

2.2.3 Extensions de la logique monadique

Différentes extensions de la logique monadique ont été considérées. La présen-
tation qui en est faite ici n'a aucune ambition d'exhaustivité.

Bien entendu, l'extension la plus directe consiste à utiliser la totalité de la
logique du second-ordre, c'est à dire la possibilité d'utiliser des variables dont
l'interprétation est une relation d'arité quelconque. La satisfaction de cette logique
devient alors indécidable dès que l'univers de la structure est infini. Il s'agit donc
d'une extension d'un intérêt relatif dans le cadre d'une étude sur les structures
infinies.

Une situation intermédiaire entre la logique monadique et la logique du second-
ordre est la *logique du second-ordre gardée*. Il s'agit dans ce cas d'autoriser l'utilisation
de variables dont l'interprétation est une relation contenue dans une relation
déja présente dans la structure. Cette logique permet en particulier de quantifier
sur des ensembles d'arcs dans un graphe. Le lien entre cette logique et la logique
monadique a été largement étudié [Cou97, EGO00, Cou03].

Une autre possibilité d'extension consiste à ajouter des prédicats de cardinalité à la logique monadique, en particulier la possibilité d'exprimer la finitude de l'interprétation d'une variable monadique [Cou90]. La finitude d'un ensemble d'éléments ne peut pas être exprimée en logique monadique dans le cas général, et il s'agit donc d'une extension stricte de la logique. En revanche, sur les arbres de degré fini, la logique monadique et la logique monadique augmentée d'un prédicat de cardinalité sont de même expressivité. En effet, il est possible d'exprimer en
$$ \mathbf{est}\text{-}\mathbf{prefixe}(X) = \forall x. \forall y. ((\bigvee_{a \in A} x \xrightarrow{a} y) \land y \in X) \Rightarrow x \in X $$

$$ \mathbf{prefixe}(X, Y) = \begin{array}{l} X \subseteq Y \land \mathbf{est}\text{-}\mathbf{prefixe}(Y) \\ \land \quad \forall Z. ((X \subseteq Z \land \mathbf{est}\text{-}\mathbf{prefixe}(Z)) \Rightarrow Y \subseteq Z) \end{array} $$

$$ \mathbf{infini}(X) = \exists W. \begin{array}{l} \text{racine} \in W \\ \land \quad \forall Y. (\mathbf{prefixe}(X, Y) \Rightarrow W \subseteq Y) \\ \land \quad \forall x \in W, \exists y \in W. \bigvee_{a \in A} x \xrightarrow{a} y \end{array} $$

$$ \mathbf{fini}(X) = \neg \mathbf{infini}(X) $$

FIG. 2.4 – Expression de la finitude dans un arbre de degré fini en logique monodique.

logique monadique qu’un ensemble de nœuds d’un arbre de degré fini est infini comme le montre la remarque suivante.

**Remarque 2.12** Un codage est présenté à la figure 2.4.

Remarquons tout d'abord que si $X$ est fini, alors l'ensemble $\mathbf{prefixe}(X)$ des sommets dont est issu un chemin aboutissant dans $X$ est lui même fini. Le lemme de König nous précise qu'un arbre est infini si et seulement si il contient un sommet de degré infini ou une branche infinie. Dans le cas présent, $\mathbf{prefixe}(X)$ est fini si et seulement s'il ne contient pas de branche infinie.

La formule $\mathbf{est}\text{-}\mathbf{prefixe}(X)$ est satisfaite si tout père d'un noeud de $X$ appartient à $X$. L'ensemble $\mathbf{prefixe}(X)$ est alors le plus petit ensemble $Y$ contenant $X$ et satisfaisant $\mathbf{est}\text{-}\mathbf{prefixe}(Y)$, ce qu'exprime le prédicat $\mathbf{prefixe}(X, Y)$. La formule $\mathbf{infini}(X)$ détermine alors l'existence d'une branche infinie $W$ incluse dans $\mathbf{prefixe}(X)$.

### 2.2.4 Construction de Feferman-Vaught

Une construction fondamentale pour la suite de ce travail est celle introduite par Feferman et Vaught dans leur étude du produit de structures [FV59] (voir aussi paragraphe 2.3.4). Cette construction ramène la vérification d'une propriété d'un produit de structure à des vérifications sur les structures composantes d'un nombre fini de propriétés, qui ne dépendent que de la formule définissant la propriété initiale.
<figure><img src="image_7.png" /><figcaption>FIG. 2.5 – *Quelques invariants logiques*.</figcaption></figure>

Dans notre contexte nous considérons cette construction d'un point de vue syntaxique, sans s'intéresser particulièrement au cas du produit. Sous cette angle il s'agit d'une transformation de formules logiques : si il est possible de séparer l'ensemble des variables d'une formule en deux ensembles tels qu'aucun symbole relationnel ne fasse référence à une variable de ces deux ensembles simultanément. alors il est possible de transformer syntaxiquement la formule en une combinaison de formules logiques n'utilisant des variables que de l'un des deux ensembles.

Pour simplifier, on suppose ici que les formules ne contiennent pas de néga-
tions, ce qui est sans conséquence pour la suite.

Précisons tout d'abord les transformations syntaxiques autorisées. Ainsi, on définit la relation d'équivalence syntaxique ⇔$_{s}$ entre formules comme la plus petite relation satisfaisant les invariants de la figure 2.5, réflexive, symétrique, transitive et compositionelle (dans le sens où remplacer une sous-formule par une sous-formule équivalente permet d'obtenir une formule équivalente : cela équivaut à dire que les transformations peuvent être appliquées à l'intérieur des formules).

La relation ⇔$_{s}$ préserve les variables libres. Bien entendu, pour $\mathcal{S}$ une $\Sigma$-structure, $\phi$ et $\psi$ telles que $\phi \Leftrightarrow_s \psi$ et $\gamma$ une valuation de $FV(\phi)$, on a $\gamma, \mathcal{S} \models \phi$ si et seulement si $\gamma, \mathcal{S} \models \psi$. Ainsi, la relation ⇔$_{s}$ est bien «valide».

Soit $\phi$ une formule logique. Appelons $\text{Vars}(\phi)$ l'ensemble des variables appa-
raissant dans $\phi$ (cette définition n'a de sens que parce que $\Leftrightarrow_s$ ne contient pas
l'α-conversion). Soit Rels(φ) l'ensemble des prédicats relationnels apparaissant
dans φ. On vérifie sans peine que Vars(φ) et Rels(φ) sont préservés par ⇔s. En-
fin, pour Σ un alphabet relationnel et X un ensemble de variables, on note Σ(X)
l'ensemble des prédicats relationnels construits sur Σ et X, c'est-à-dire :

$$
\Sigma(X) = \{R(x_1, \dots, x_{|R|}) \mid R \in \Sigma, x_1, \dots, x_{|R|} \in X\} .
$$

**Lemme 2.13 (construction de Feferman-Vaught)** Soit $\phi$ une formule sur la signature $\Sigma = \Sigma_1 \uplus \Sigma_2$ telle que $\mathrm{Vars}(\phi) = X_1 \uplus X_2$ et $\mathrm{Rels}(\phi) \subseteq \Sigma_1(X_1) \cup \Sigma_2(X_2)$. Alors il existe un ensemble fini $\phi^{X_1, X_2}$ de couples de formules tel que :

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
- \text{ pour tout } (\psi_1, \psi_2) \in \phi^{X_1, X_2}, & \mathrm{Vars}(\psi_1) \subseteq X_1, & \mathrm{Rels}(\psi_1) \subseteq \Sigma_1(X_1), \\
& \mathrm{Vars}(\psi_2) \subseteq X_2, & \mathrm{Rels}(\psi_2) \subseteq \Sigma_2(X_2), \\
- \phi \Leftrightarrow_s & \bigvee_{(\psi_1, \psi_2) \in \phi^{X_1, X_2}} \psi_1 \wedge \psi_2 . &
\end{array}
$$

**Construction.** La conclusion du lemme s'exprime comme l'équivalence avec une disjonction de conjonctions. Il est nécessaire pour pouvoir traiter le cas de la quantification universelle de disposer d'une représentation duale sous forme de conjonctions de disjonctions. Il est possible de passer d'une telle disjonction à une conjonction comme suit. Soit Θ un ensemble de couples de formules, alors on a l'équivalence suivante :

$$
\bigvee_{(\phi, \psi) \in \Theta} (\phi \wedge \psi) \iff_s \bigwedge_{(\phi, \psi) \in \bar{\Theta}} (\phi \vee \psi),
$$
$$
\text{avec } \bar{\Theta} = \left\{ \left( \bigvee_{(\phi, \psi) \in \Theta_1} \phi, \bigvee_{(\phi, \psi) \in \Theta_2} \psi \right) \mid \Theta_1 \uplus \Theta_2 = \Theta \right\}.
$$

Ceci se montre par récurrence sur le cardinal de Θ. Un fait important de cette
construction est que si pour tout (φ, ψ) ∈ Θ, FV(φ) ⊆ X₁ et FV(ψ) ⊆ X₂
 resp. Rels(φ) ⊆ Σ₁(X₁) et Rels(ψ) ⊆ Σ₂(X₂)) alors il en est de même pour
tout (φ, ψ) ∈ Θ. Bien entendu, par dualité, une opération similaire qui à Θ
associe Θ permet de passer d'une conjonction de disjonctions à une disjonction
de conjonctions :

$$
\bigwedge_{(\phi, \psi) \in \Theta} (\phi \lor \psi) \Leftrightarrow_s \bigvee_{(\phi, \psi) \in \mathbf{\Theta}} (\phi \land \psi) .
$$
L'ensemble $\phi^{X_1,X_2}$ est alors défini récursivement comme suit :

$$ 
\begin{align*}
(\phi \lor \psi)^{X_1,X_2} &= \phi^{X_1,X_2} \cup \psi^{X_1,X_2} \\
(\phi \land \psi)^{X_1,X_2} &= \overline{\phi^{X_1,X_2} \cup \psi^{X_1,X_2}} \\
(\exists x.\phi)^{X_1,X_2} &= \left\{ \begin{array}{ll} \{(\exists x.\phi_1, \phi_2) \mid (\phi_1, \phi_2) \in \phi^{X_1,X_2}\} & \text{si } x \in X_1 \\ \{(\phi_1, \exists x.\phi_2) \mid (\phi_1, \phi_2) \in \phi^{X_1,X_2}\} & \text{si } x \in X_2 \end{array} \right. \\
(\forall x.\phi)^{X_1,X_2} &= \left\{ \begin{array}{ll} \{(\forall x.\phi_1, \phi_2) \mid (\phi_1, \phi_2) \in \overline{\phi^{X_1,X_2}}\} & \text{si } x \in X_1 \\ \{(\phi_1, \forall x.\phi_2) \mid (\phi_1, \phi_2) \in \overline{\phi^{X_1,X_2}}\} & \text{si } x \in X_2 \end{array} \right. \\
R(x_1, \dots, x_{|R|}) &= \left\{ \begin{array}{ll} \{(R(x_1, \dots, x_{|R|}), \text{vrai})\} & \text{si } R \in \Sigma_1 \\ \{(\text{vrai}, R(x_1, \dots, x_{|R|}))\} & \text{si } R \in \Sigma_2 \end{array} \right. \\
\text{faux}^{X_1,X_2} &= \emptyset \\
\text{vrai}^{X_1,X_2} &= \{(\text{vrai}, \text{vrai})\}
\end{align*}
$$

La validité de cette construction pour $\lor, \exists$, vrai et faux est évidente. La validité pour $\land$ et $\forall$ s'obtient par dualité. La validité pour $R(x_1, \dots, x_{|R|})$ provient de l'hypothèse sur l'ensemble $\text{Rels}(\phi)$. $\square$

De nombreuses variantes de cette construction sont possibles. L'important est son aspect syntaxique, et surtout le fait que les quantifications que l'on trouve dans les formules de $\phi^{X_1,X_2}$ sont plus «simples» que celles de $\phi$. Cette notion de simplification peut être mesurée en terme d'alternance de quantifications ou de niveaux d'imbrication... En fait, il arrive que cette mesure dépende elle-même des variables. C'est par exemple le cas dans la preuve du théorème 16.

## Application

La construction de Feferman-Vaught est utilisée dans la suite pour décomposer des formules faisant référence à deux structures distinctes en formules faisant référence uniquement à l'une ou l'autre de ces structures. Pour formaliser la possibilité pour une formule logique de faire référence à deux structures, on utilise une technique similaire à celle des logiques multi-sortées. Nous présentons ici une technique ad-hoc pour la suite de ce travail.

L'objectif est de modifier la logique (du premier ordre ou monadique) de manière à définir une relation de satisfaction reliant un couple de structures (au lieu d'une seule structure) à une formule. Ainsi, on modifie la logique (premier ordre, monadique ou autre) afin de définir pour deux structures $S_1$ et $S_2$ la satisfaction d'une formule $\phi$ par $(S_1, S_2)$, notée $(S_1, S_2) \models \phi$. L'idée de cette logique est que la formule $\phi$ fait explicitement référence à l'indice des structures et peut donc
quantifier sur un élément de $S_1$ ou un élément de $S_2$. Les symboles relationnels possèdent aussi une marque permettant d'identifier si ils correspondent à une relation de $S_1$ ou de $S_2$ (cela est nécessaire pour traiter le cas des relations d'arité zéro).

On définit donc tout d'abord une signature utilisée par les prédicats de cette logique. Soient $\Sigma_1$ et $\Sigma_2$ deux signatures, notons $\Sigma_1 \sqcup \Sigma_2$ la signature définie comme suit :

$$ \Sigma_1 \sqcup \Sigma_2 = \{R^1 | R \in \Sigma_1\} \cup \{R^2 | R \in \Sigma_2\}, \quad \text{avec } |R^i| = |R|. $$

Les formules sont alors modifiées de la manière suivante. On suppose l'ensemble des variables du premier ordre (resp. monadique) partagé en deux : $\mathcal{V} = \mathcal{V}^1 \oplus \mathcal{V}^2$ (resp. $\mathcal{V}_m = \mathcal{V}_m^1 \oplus \mathcal{V}_m^2$) de telle sorte qu'il existe pour $i \in [2]$ une bijection de $\mathcal{V}$ sur $\mathcal{V}^i$ (resp. de $\mathcal{V}_m$ sur $\mathcal{V}_m^i$). Pour $x$ une variables de $\mathcal{V}$ (resp $X \in \mathcal{V}_m$), $x^i \in \mathcal{V}^i$ (resp. $X^i \in \mathcal{V}_m^i$) est l'image de $x$ (resp. de $X$) par la bijection correspondante.

Un prédicat de la forme $R^i(x_1, \dots, x_{|R|})$ n'est syntaxiquement valide que si toutes les variables $x_j$ appartiennent à $\mathcal{V}^i$ (resp. $x \in X$ n'est syntaxiquement valide que si il existe $i \in [2]$ tel que $x \in \mathcal{V}^i$ et $X \in \mathcal{V}_m^i$).

La relation de satisfaction relie alors une paire de structures à un formule. Soient donc $S_1$ une $\Sigma_1$-structure et $S_2$ une $\Sigma_2$-structure. Soit $\mathcal{X}$ un ensemble de variables, une valuation de $\mathcal{X}$ sur $(S_1, S_2)$ est une application qui à chaque variable telle que $x \in \mathcal{X} \cap \mathcal{V}^i$ pour $i \in [2]$ associe un élément de l'univers de $S_i$ (resp. à toute variable de $X \in \mathcal{X} \cap \mathcal{V}_m^i$ associe une partie de l'univers de $S_i$).

Soit $\phi$ une formule logique et pour $\gamma$ une valuation de $FV(\phi)$ sur $(S_1, S_2)$, on définit la relation de satisfaction $\gamma$, $(S_1, S_2) \models \phi$ par récurrence sur $\phi$ comme précédemment.

**Lemme 2.14** Pour $\Sigma_1$ et $\Sigma_2$ deux alphabets relationnels et toute formule $\phi$ (monadique ou du premier ordre) sur $\Sigma_1 \sqcup \Sigma_2$, il existe un ensemble fini $\phi^*$ de couples de formules tel que :

- pour $(\psi_1, \psi_2) \in \phi^*$, $\psi_i$ est une formule sur la signature $\Sigma_i$,

- pour toute $\Sigma_1$-structure $S_1$ et toute $\Sigma_2$-structure $S_2$, $(S_1, S_2) \models \phi$ si et seulement si il existe $(\psi_1, \psi_2) \in \phi^*$ tel que $S_1 \models \psi_1$ et $S_2 \models \psi_2$.

**Preuve.** Par application du lemme 2.13. $\square$

## 2.3 Opérations sur les structures

Jusqu'à présent, toutes les structures rencontrées étaient définies de manière interne, c'est-à-dire en explicitant l'univers et l'interprétation des relations. Dans
la pratique, il est plus agréable de construire les structures par application successive à une structure simple de transformations dont les propriétés sont connues.

Ce paragraphe a pour objectif de présenter de telles transformations et d'en donner les principales caractéristiques. Nous portons une attention particulière à établir les liens reliant ces différentes opérations, et ce dans l'objectif d'éviter les redondances et les définitions équivalentes dans la suite de ce travail.

Notons enfin que toutes ces transformations partagent une propriété fondamentale, celle d'être définies à isomorphisme près (sauf en ce qui concerne la modification finie). Ainsi, les utiliser permet de s'abstraire du codage des éléments de l'univers.

### 2.3.1 Modification finie

La modification finie de structure ne sert pas tant à décrire des structures qu'à préciser les limites d'une famille de structures.

La modification finie d'une structure consiste à appliquer une combinaison finie des transformations suivantes :

- ajout d'un élément à l'univers (sans changer les interprétations des symboles),

- ajout d'un hyperarc entre des éléments fixés de l'univers,

- élimination d'un élément de l'univers et, par conséquent, de tous les hyperarcs dans lequel il est impliqué,

- élimination d'un hyperarc.

Lorsque seules les deux premières transformations sont utilisées, on parle d'ajout fini à la structure.

### 2.3.2 Interprétation logique

L'interprétation est une méthode classique en logique pour transformer une structure en une autre, la transformation étant décrite par des formules logiques. L'interprétation logique se définit de manière variée suivant la logique choisie. Une interprétation est un triplet $\mathcal{I} = (\delta, \Sigma, (\phi_R)_{R \in \Sigma})$ où $\delta(x)$ est une formule logique d'unique variable libre du premier ordre $x$, $\Sigma$ est une signature, et pour tout symbole $R \in \Sigma$, $\phi_R(x_1, \dots, x_{|R|})$ est une formule logique de variables libres du premier ordre $x_1, \dots, x_{|R|}$. Soit $\mathcal{S}$ une structure, l'interprétation $\mathcal{I}$ appliquée à $\mathcal{S}$ est la structure d'univers $\{u \in \mathcal{U}_\mathcal{S} \mid \mathcal{S} \models \delta(u)\}$, et l'interprétation d'un symbole relationnel $R \in \Sigma$ est

$$ \{(u_1, \dots, u_{|R|}) \mid \forall i \in [|R|]. \mathcal{S} \models \delta(u_i), \mathcal{S} \models \phi_R(u_1, \dots, u_{|R|}) \}. $$

La formule $\delta$ est appelée restriction car elle sélectionne les éléments qui doivent être conservés dans l'univers. Lorsque $\delta = \text{vrai}$, tous les éléments de l'univers sont
conservés par l'interprétation, il s'agit d'une interprétation sans restriction. Suivant la logique choisie pour l'interprétation, on parle d'interprétation booléenne, booléenne positive, au premier ordre ou monadique (ou en fait toute autre variante construite sur la logique du premier ordre).

**Propriété 2.15** La composition de deux interprétations (booléennes/booléennes positives/existentielles/au premier ordre/monadique) est une interprétation dans la même logique.

**Propriété 2.16** L'interprétation (existentielle/au premier ordre/monadique) préserve la décidabilité de la théorie correspondante.

L'interprétation logique est une opération tellement utile pour la suite de ce travail qu'il convient de lui donner une notation spéciale. Considérons une syntaxe logique close par disjonction (i.e. si $\phi$ et $\psi$ sont des formules bien formées, alors $\phi \lor \psi$ l'est aussi). Soient $R_1, \dots, R_n$ des symboles (éventuellement plusieurs fois le même), et $\psi_1, \dots, \psi_n$ des formules logiques dans la logique fixée telles que $\psi_i(x_1, \dots, x_{|R_i|})$ a pour variables libres les $x_1, \dots, x_{|R_i|}$, alors, la notation :

$$ \left| \begin{array}{lcl} R_1(x_1, \dots, x_{|R_1|}) & : & \psi_1(x_1, \dots, x_{|R_1|}) \\ & \vdots & \\ R_n(x_1, \dots, x_{|R_n|}) & : & \psi_n(x_1, \dots, x_{|R_n|}) \end{array} \right| $$

représente l'interprétation logique :

$$ (\text{vrai}, \{R_i \mid i \in [n]\}, \phi), \quad \text{avec } \phi_R = \bigvee_{\substack{i \in [n] \\ R_i = R}} \psi_i(x_1, \dots, x_{|R|}) . $$

On étend cette notation pour avoir la possibilité d'exprimer une restriction.

$$ \left| \begin{array}{lcl} x \in \mathcal{U} & : & \delta(x) \\ R_1(x_1, \dots, x_{|R_1|}) & : & \psi_1(x_1, \dots, x_{|R_1|}) \\ & \vdots & \\ R_n(x_1, \dots, x_{|R_n|}) & : & \psi_n(x_1, \dots, x_{|R_n|}) \end{array} \right| $$

représente l'interprétation logique :

$$ (\delta, \{R_i \mid i \in [n]\}, \phi), \quad \text{avec } \phi_R = \bigwedge_{j \in [|R|]} \delta(x_i) \wedge \bigvee_{\substack{i \in [n] \\ R_i = R}} \psi_i(x_1, \dots, x_{|R|}) . $$

Un cas particulier d'interprétation est le renommage. Soit $\Sigma$ une signature et $K$ une relation binaire entre $\Sigma_1$ et $\Sigma_2$ reliant uniquement des symboles de même arité, alors le renommage des symboles par $K$ est l'interprétation :

$$ \left| R(x_1, \dots, x_{|R|}) : R'(x_1, \dots, x_{|R|}), (R', R) \in K \right|. $$
Cette opération extrêmement simple permet de changer quand nécessaire la signature d'une structure afin, par exemple, d'éviter des confusions dues au choix de nommage des symboles.

Plusieurs autres transformations de graphes [Cau96, Cau02, Urv02] sont des cas particuliers d'interprétations :

*la substitution rationnelle inverse:* pour chaque lettre *a* de l'alphabet du graphe résultat, on se fixe un langage rationnel $L_a$ sur l'alphabet du graphe d'origine. Le graphe résultat a alors le même ensemble de sommets que le graphe originel<fnref n="1" />, et il y a un arc étiqueté par *a* entre deux sommets s'il y a un chemin étiqueté par un mot de $L_a$ entre ces deux sommets dans le graphe originel. On utilise pour cela la formule accessibilité[$L_a$] définie dans l'exemple 2.8. Il s'agit donc d'une interprétation monadique sans restriction.

*la substitution finie inverse:* il s'agit d'un cas particulier de la substitution rationnelle inverse: les langages associés à chaque lettre doivent être finis au lieu de rationnels. Il s'agit d'une interprétation sans restriction en logique du premier ordre.

*le morphisme inverse:* le morphisme inverse est un cas encore plus restreint: chaque langage ne contient au plus qu'un mot. Il s'agit toujours d'une interprétation sans restriction en logique du premier ordre. Le morphisme inverse possède la propriété supplémentaire de préserver le déterminisme d'un graphe.

*l'élimination des sommets isolés:* cette transformation élimine les sommets de degré nul d'un graphe. C'est une interprétation avec uniquement de la restriction en logique du premier ordre.

*la restriction par accessibilité:* cette transformation ne conserve d'un graphe enraciné que les sommets accessibles à partir de sa racine. Il s'agit d'une interprétation en logique monadique ou monadique.

*la restriction rationnelle:* elle est paramétrée par un langage rationnel *L*. Cette transformation ne conserve que les sommets accessibles à partir de la racine par un chemin étiqueté par un mot de *L*.

*le marquage rationnel:* il est paramétré par un langage rationnel *L* et un symbole #. Appliqué à un graphe enraciné, il laisse ce dernier inchangé si ce n'est qu'à les chaque sommet accessible à partir de la racine par un chemin étiqueté par un mot de *L*, est attachée une boucle étiquetée par #.

Toutes ces transformations sont contrôlées par des chemins entre sommets. Il est courant d'en augmenter la puissance en autorisant dans les langages de prendre en sens inverse les arcs. On utilise pour cela la lettre barrée. Ainsi $\bar{a}$ représente

<footnote n="1">1. Dans les travaux originaux de Caucal les sommets sont implicitement restreints aux extrémités des arcs.</footnote>
<figure><img src="image_8.png" /><figcaption>FIG. 2.6 – Demi-droite des entiers enracinée (a), marquée (c), et échelle enracinée (b).</figcaption></figure>

implicitement la relation $\xrightarrow{a}$ inversée. On parle alors de substitution rationnelle inverse (resp. substitution finie inverse, resp. restriction rationnelle, resp. marquage rationnel) *avec retour*.

Il peut paraître *a priori* étonnant qu'une telle profusion de transformations d'expressivité relativement identique ait vue le jour. La raison est d'une part historique, mais de plus, ces interprétations possèdent des propriétés non vérifiées. dans le cas général: elles sont continues (au sens des ordres partiels complets présentés au paragraphe 3.1 et appliqués aux structures page 52), et en ce qui concerne les substitutions inverses, elles correspondent à des transformations naturelles de langages sur les traces [Urv02].

**Exemple 2.17** L'échelle enracinée (figure 2.6(c)) s'obtient à partir de la demi-droite des entiers (figure 2.6(a)) en appliquant tout d'abord un marquage rationnel: tous les sommets atteignables à partir de la racine par un chemin étiqueté par un mot de (aa)* sont marqués d'une boucle # (figure 2.6(b)). Pour obtenir l'échelle, on applique alors une substitution finie inverse avec retour. On met un arc étiqueté par *a* entre un sommet marqué et son deuxième successeur sur la demi-droite des entiers, soit $L_a = \#aa$. On met un arc étiqueté par *b* entre un sommet marqué et son successeur, soit $L_b = \#a$. On met un arc étiqueté par *c* entre un sommet non marqué et son deuxième prédécesseur, soit $L_c = \bar{a}\#\bar{a}$. Nous montrons que la substitution inverse ne permet pas de tester l'absence d'une marque. Pour être sûr que la substitution a lieu au bon endroit, il est nécessaire d'aller chercher une marque un peu plus loin, puis de revenir (ce que fait le mot $\bar{a}\#\bar{a}$).

### 2.3.3 Union disjointe

Soient deux structures $S_1$ et $S_2$, l'union disjointe de $S_1$ et $S_2$, notée $S_1 \oplus S_2$, est la structure d'univers $\{1\} \times S_1 \cup \{2\} \times S_2$ et dont l'interprétation d'un symbole
$R$ est :

$$
R^{S_1 \oplus S_2} = \bigcup \left\{ \begin{array}{l} \left( (1, u_1), \dots, (1, u_{|R|}) \right) \mid R^{S_1}(u_1, \dots, u_{|R|}) \\ \left( (2, u_1), \dots, (2, u_{|R|}) \right) \mid R^{S_2}(u_1, \dots, u_{|R|}) \end{array} \right\} .
$$

L'union disjointe explicite ajoute de l'information à cette construction afin de pouvoir déterminer l'origine des relations. Elle est définie comme suit. Soit $\Sigma_1$ et $\Sigma_2$ deux signatures, l'union disjointe explicite d'une $\Sigma_1$-structure avec une $\Sigma_2$-structure produit une structure de signature $\Sigma' = \{R^1 | R \in \Sigma_1\} \uplus \{R^2 | R \in \Sigma_2\}$. Soient $S_1$ une $\Sigma_1$-structure et $S_2$ une $\Sigma_2$-structure, l'union disjointe explicite de $S_1$ et $S_2$ est la $\Sigma'$-structure $S_1 \oplus_e S_2$ d'univers $\{1\} \times S_1 \cup \{2\} \times S_2$ et dont l'interprétation d'un symbole $R^i \in \Sigma'$ pour $i \in [2]$ est :

$$
(R^i)^{S_1 \oplus_e S_2} = \{ ((i, u_1), \dots, (i, u_{|R^i|})) \mid R^{S_i}(u_1, \dots, u_{|R^i|}) \} .
$$

Le lemme suivant énonce comment passer d'une de ces formes d'union disjointe
à l'autre au moyen de recoloriages.

**Propriété 2.18** Étant données deux signatures $\Sigma_1$ et $\Sigma_2$, il existe trois renom-
mages $\mathcal{I}$, $\mathcal{I}_1$ et $\mathcal{I}_2$ tels que pour toute $\Sigma_1$-structure $S_1$ et toute $\Sigma_2$-structure $S_2$,
on a :

$$
\begin{array}{l}
S_1 \oplus S_2 = \mathcal{I}(S_1 \oplus_e S_2) \\
\text{et} \\
S_1 \oplus_e S_2 = \mathcal{I}_1(S_1) \oplus \mathcal{I}_2(S_2).
\end{array}
$$

**Preuve.** Très naturellement $\mathcal{I}$ renomme chaque symbole $R^i$ en $R$ et pour $i \in [2]$,
$\mathcal{I}_i$ renomme chaque symbole $R$ en $R^i$. $\square$

**Propriété 2.19** *L'union disjointe (resp. l'union disjointe explicite) de deux structures possédant une théorie au premier ordre (resp. monadique) décidable a une théorie au premier ordre (resp. monadique) décidable.*

**Preuve.** Par application du lemme 2.13. $\square$

2.3.4 Produits

L'union disjointe de deux structures produit une structure dont le nouvel
univers est l'union disjointe des univers des deux structures. Il n'y a en fait pas
beaucoup de choix possibles pour de telles opérations. C'est un peu différent dans
le cas du produit. Une fois adopté le principe de produire une structure dont
l'univers est le produit des univers des structures arguments, il reste des choix
<figure><img src="image_9.png" /><figcaption>FIG. 2.7 – Produit synchrone de la demi-droite des entiers avec elle-même</figcaption></figure>

possibles pour définir les interprétations des relations. Ainsi, nous considérons trois types de produits dans ce travail : le produit synchrone, le produit généralisé qui en est une variante, et le produit asynchrone<fnref n="2" />.

Soient $S_1$ et $S_2$ deux structures sur la signature $\Sigma$, le produit synchrone (aussi appelé produit cartésien) de $S_1$ et $S_2$ est la structure $S_1 \otimes S_2$ définie par :

$$ \mathcal{U}_{S_1 \otimes S_2} = \mathcal{U}_{S_1} \times \mathcal{U}_{S_2}, \\ \text{pour } R \in \Sigma, \quad R^{S_1 \otimes S_2} = \left\{ \left( (u_1, v_1), \dots, (u_{|R|}, v_{|R|}) \right) \middle| \begin{array}{l} R^{S_1}(u_1, \dots, u_{|R|}) \\ \wedge R^{S_2}(v_1, \dots, v_{|R|}) \end{array} \right\}. $$

**Exemple 2.20** La figure 2.7 montre le résultat du produit de la demi-droite des entiers avec elle-même. Le résultat est une union disjointe infinie de demi-droites des entiers.

**Propriété 2.21** Soient $A_1$ et $A_2$ deux automates, alors $A_1 \otimes A_2$ est un automate tel que :

$$ \mathcal{L}(A_1 \otimes A_2) = \mathcal{L}(A_1) \cap \mathcal{L}(A_2). $$

**Théorème 3 (Feferman et Vaught [FV59])** Le produit synchrone préserve la décidabilité de la théorie au premier ordre.

Il existe des graphes dont la théorie au second ordre monadique est décidable et dont le produit synchrone possède une accessibilité indécidable. Pour le montrer, on peut par exemple réduire l'indécidabilité de la vacuité de l'intersection de deux langages algébriques à une question d'accessibilité sur un graphe produit. Pour cela, on admet momentanément que pour tout langage algébrique, il existe effectivement un automate possédant une théorie monadique décidable et dont il est le langage accepté (voir théorèmes 12 et 13 page 92). La vacuité de l'intersection de deux langages algébriques étant indécidable, cela signifie que la vacuité

<footnote n="2">2. En général, sous la terminologie de produit sans autres précisions, on entend le produit synchrone ou le produit généralisé.</footnote>
du langage accepté par l'automate produit est indécidable (d'après la propriété 2.21). Pourtant, ceci revient à déterminer s'il existe un chemin entre le sommet initial et un sommet final, c'est à dire une question d'accessibilité.

En revanche, le produit synchrone avec une structure finie préserve la dé-
cidabilité de la théorie monadique. Ce résultat est présenté à titre d'exemple
(exemple 2.26) pour illustrer les transductions monadiques.

Le produit généralisé permet une utilisation plus aisée du produit synchrone.
Il se définit comme suit. Étant données deux structures $\mathcal{S}_1$ et $\mathcal{S}_2$ de signatures
respectives $\Sigma_1$ et $\Sigma_2$, le produit généralisé de $\mathcal{S}_1$ et $\mathcal{S}_2$ est une structure $\mathcal{S}_1 \ltimes_g \mathcal{S}_2$
sur la signature $\Sigma' = \{R^1 \mid R \in \Sigma_1\} \uplus \{R^2 \mid R \in \Sigma_2\}$ avec pour tout $R^i \in \Sigma'$,
$|R^i| = |R|$. La structure $\mathcal{S}_1 \ltimes_g \mathcal{S}_2$ est définie comme suit:

$$
\mathcal{U}_{\mathcal{S}_1 \ltimes_g \mathcal{S}_2} = \mathcal{U}_{\mathcal{S}_1} \times \mathcal{U}_{\mathcal{S}_2}, \\
\text{et pour } R^i \in \Sigma', \quad (R^i)^{\mathcal{S}_1 \ltimes_g \mathcal{S}_2} = \left\{ \left( (u_1^1, u_1^2), \dots, (u_{|R|}^1, u_{|R|}^2) \right) \mid R^{S_i} (u_1^i, \dots, u_{|R|}^i) \right\}.
$$

En fait, produit généralisé et produit synchrone sont des opérations d'expres-
sivité identique si l'on dispose d'interprétations booléennes positives comme le
montre la propriété 2.22.

**Propriété 2.22** *Pour toute signature $\Sigma$, il existe trois interprétations booléennes positives $\mathcal{I}$, $\mathcal{I}_1$ et $\mathcal{I}_2$ telles que pout toutes $\Sigma$-structures $\mathcal{S}_1$ et $\mathcal{S}_2$ on a*

$$
\begin{align*}
\mathcal{S}_1 \ltimes_g \mathcal{S}_2 &= \mathcal{I}_1(\mathcal{S}_1) \ltimes \mathcal{I}_2(\mathcal{S}_2) \\
\text{et } \mathcal{S}_1 \ltimes \mathcal{S}_2 &= \mathcal{I}(\mathcal{S}_1 \ltimes_g \mathcal{S}_2) .
\end{align*}
$$

**Preuve.** L'interprétation $\mathcal{I}_i$ pour $i \in [2]$ renomme $R \in \Sigma$ en $R^i$ et attribue comme interprétation de $R^j$ pour $j \in [2] - \{i\}$ la relation complète d'arité $|R|$. L'interprétation $\mathcal{I}$ donne comme interprétation d'un symbole $R \in \Sigma$ l'intersection des interprétations de $R^1$ et $R^2$. $\square$

Le troisième type de produit que nous considérons est le produit asynchrone.
Etant données deux structures $\mathcal{S}_1$ et $\mathcal{S}_2$, le produit asynchrone de $\mathcal{S}_1$ et $\mathcal{S}_2$ est la
structure $\mathcal{S}_1 \sqcap \mathcal{S}_2$ définie par :

$$
\begin{align*}
\mathcal{U}_{\mathcal{S}_1 \sqcap \mathcal{S}_2} &= \mathcal{U}_{\mathcal{S}_1} \times \mathcal{U}_{\mathcal{S}_2}, \\
\text{pour } R \in \Sigma, \quad R^{\mathcal{S}_1 \sqcap \mathcal{S}_2} &= \left\{ \begin{array}{@{}l@{}}
  \left( (u_1, v), \dots, (u_{|R|}, v) \right) \mid R^{\mathcal{S}_1}(u_1, \dots, u_{|R|}), v \in \mathcal{U}_{\mathcal{S}_2} \end{array} \right\} \\
  \cup \left\{ \left( (u, v_1), \dots, (u, v_{|R|}) \right) \mid u \in \mathcal{U}_{\mathcal{S}_1}, R^{\mathcal{S}_2}(u_1, \dots, u_{|R|}) \right\} .
\end{align*}
$$

**Exemple 2.23** Le produit asynchrone de deux demi-droites des entiers permet d'obtenir le quart de grille infinie (cf figure 2.8). Sachant que la demi-droite des entiers a une théorie monadique décidable (théorème 1 de Büchi), et en appliquant la résultat d'indécidabilité de la théorie monadique du quart de grille infini
<figure><img src="image_10.png" /><figcaption>FIG. 2.8 – Le quart de grille infinie comme produit asynchrone de demi-droites des entiers</figcaption></figure>

(propriété 2.9), on en déduit que le produit asynchrone ne préserve pas la décidabilité de la théorie monadique. En revanche nous verrons que cette opération préserve la décidabilité des propriétés d'accessibilité.

Produits synchrones et asynchrones ont des propriétés bien distinctes. Pourtant, ils sont inter-convertibles au moyen d'interprétations logiques comme le montre la propriété ci-dessous.

**Propriété 2.24** Soit $\Sigma$ un alphabet relationnel, alors

1. il existe un renommage $\mathcal{I}_1$ et une interprétation existentielle $\mathcal{I}$ tels que pour toutes structures $S_1$ et $S_2$ de signature $\Sigma$,

$$S_1 \otimes S_2 = \mathcal{I}(\mathcal{I}_1(S_1) \sqcap S_2),$$

2. il existe deux interprétations booléennes positives $\mathcal{I}_1$ et $\mathcal{I}_2$ et un renommage $\mathcal{I}$ tels que pour toutes structures $S_1$ et $S_2$ de signature $\Sigma$ :

$$S_1 \sqcap S_2 = \mathcal{I}(\mathcal{I}_1(S_1) \otimes \mathcal{I}_2(S_2)).$$

**Preuve.** Soit $\hat{\Sigma}$ l'ensemble des symboles $\hat{R}$ d'arité $|R|$ pour $R$ un symbole de $\Sigma$. La figure 2.9 illustre les constructions de cette propriété.

Résultat 1. L'interprétation $\mathcal{I}_1$ renomme chaque symbole $R$ en un symbole $\hat{R}$. Cela revient à rendre disjointes les signatures des deux structures. L'interprétation existentielle est alors la suivante :

$$ \mathcal{I} = \left| \begin{array}{l} R(x_1, \dots, x_{|R|}) : \exists y_{1,1} \dots \exists y_{1,|R|} \dots \exists y_{|R|,1} \dots \exists y_{|R|,|R|} \\ \quad \bigwedge_{i \in [|R|]} R(y_{i,1}, \dots, y_{i,|R|}) \\ \quad \wedge \bigwedge_{j \in [|R|]} \hat{R}(y_{1,j}, \dots, y_{|R|,j}) \\ \quad \wedge \bigwedge_{i \in [|R|]} x_i = y_{i,i} \end{array} \right| $$
<figure><img src="image_11.png" /><figcaption>(1) du produit asynchrone vers le produit synchrone.</figcaption></figure>

<figure><img src="image_12.png" /><figcaption>(2) du produit synchrone vers le produit asynchrone.</figcaption></figure>

FIG. 2.9 – Illustration des constructions de la propriété 2.24.
La formule logique de cette interprétation devine une matrice d'éléments de l'univers $y_{1,1}, \dots, y_{n,n}$ dont la diagonale est $x_1, \dots, x_n$. Un hyperarc $R$ relie $x_1, \dots, x_n$ si à chaque colonne de la matrice $y$ correspond un hyperarc $R$ de la première structure et à chaque ligne de $y$ correspond un hyperarc $R$ de la seconde structure (c'est à dire un hyperarc $\hat{R}$).

Résultat 2.

$$
\text{Soient } \mathcal{I}_1 = \left| \begin{array}{l} R(x_1, \dots, x_{|R|}) : R(x_1, \dots, x_{|R|}), \quad R \in \Sigma \\ \hat{R}(x_1, \dots, x_{|R|}) : x_1 = x_2 \wedge \dots \wedge x_1 = x_{|R|}, \quad R \in \Sigma \end{array} \right|,
$$
$$
\mathcal{I}_2 = \left| \begin{array}{l} R(x_1, \dots, x_{|R|}) : x_1 = x_2 \wedge \dots \wedge x_1 = x_{|R|}, \quad R \in \Sigma \\ \hat{R}(x_1, \dots, x_{|R|}) : R(x_1, \dots, x_{|R|}), \quad R \in \Sigma \end{array} \right|,
$$
$$
\text{et } \mathcal{I} = \left| \begin{array}{l} R(x_1, \dots, x_{|R|}) : R(x_1, \dots, x_{|R|}) \lor \hat{R}(x_1, \dots, x_{|R|}), \quad R \in \Sigma \end{array} \right|.
$$

Les interprétations $\mathcal{I}_1$ et $\mathcal{I}_2$ remplissent deux tâches : elles renomment les symboles de $S_1$ et $S_2$ afin que les signatures soient disjointes, et elles ajoutent de nouveaux symboles d'interprétation «identité». Le produit synchrone produit alors la structure souhaitée si ce n'est que les symboles de $\Sigma$ sont utilisés sur une composante et les symboles de $\hat{\Sigma}$ sur l'autre. Le renommage $\mathcal{I}$ élimine ce dernier point. $\square$

2.3.5 Transduction monadique

Dans les travaux de Courcelle [Cou94], une opération de base est la trans-
duction monadiquement définissable sans paramètre. Dans le présent travail, le
terme de transduction monadique est employé<fnref n="3" />. Le principe de la transduction
monadique est d'appliquer à la structure successivement une duplication et une
interprétation. Bien entendu, cette opération préserve la décidabilité de la théorie
monadique.

**Théorème 4 (Courcelle)** *Si une structure *S* a une théorie monadique décidable et si *T* est une transduction monadique, alors *T*(*S*) a une théorie monadique décidable.*

Une autre propriété importante de ces transductions est la suivante.

**Propriété 2.25 (Courcelle)** *La composition de deux transductions monadiques est une transduction monadique.*

Formellement, étant donnés deux alphabets $\Sigma$ et $\Sigma'$ de symboles relationnels, une transduction monadique des structures de signature $\Sigma$ dans les structures de signature $\Sigma'$ est un quadruplet

$$
T = (\delta, N, (\phi_n)_{n \in N}, (\psi_{R,n_1,\dots,n_{|R|}})_{R \in \Sigma', n \in N^{|R|}})
$$

<footnote n="3">3. Cette terminologie ne doit pas être confondue avec les transductions MS-compatibles dé-
finies aussi dans les travaux de Courcelle.</footnote>
où :

- $\delta$ est une formule monadique close sur la signature $\Sigma$,

- $N$ est un ensemble fini,

- $\phi_n(x)$ pour $n \in N$ est une formule monadique sur la signature $\Sigma$ d'unique variable libre du premier ordre $x$,

- pour $R$ un symbole de $\Sigma'$ et $n \in N^{|R|}$, $\psi_{R,n_1,\dots,n_{|f|}}(x_1, \dots, x_{|R|})$ est une formule monadique sur la signature $\Sigma$ de variables libres $x_1, \dots, x_{|R|}$.

Soit $\mathcal{S}$ une structure sur la signature $\Sigma$, la structure $T(\mathcal{S})$ sur la signature $\Sigma'$ est définie par :

- si $\mathcal{S} \not\models \delta$, alors $T(\mathcal{S})$ n'est pas défini,

- sinon, l'univers de $T(\mathcal{S})$ est :

$$ \mathcal{U}_{T(\mathcal{S})} = \{(n, u) \in N \times \mathcal{U}_{\mathcal{S}} \mid \mathcal{S} \models \phi_n(u)\}, $$

et l'interprétation d'un symbole $R \in \Sigma'$ est :

$$ R^{T(\mathcal{S})} = \{((n_1, u_1), \dots, (n_{|R|}, u_{|R|})) \mid \mathcal{S} \models \psi_{R, n_1, \dots, n_{|R|}}(u_1, \dots, u_{|R|})\}. $$

**Exemple 2.26** Considérons une structure finie $S_0$. Il s'agit de produire une transduction monadique effectuant le produit synchronisé d'une structure quelconque $\mathcal{S}$ par $S_0$. Cela s'obtient en appliquant la transduction monadique $T = \{\text{vrai}, \mathcal{U}_{S_0}, \phi, \psi\}$ avec

$$ \phi_u = \text{vrai}, $$

$$ \text{et } \psi_{R, u_1, \dots, u_{|R|}}(x_1, \dots, x_{|R|}) = \begin{cases} R(x_1, \dots, x_{|R|}) & \text{si } R^{S_0}(u_1, \dots, u_{|R|}) \\ \text{faux} & \text{sinon.} \end{cases} $$

### 2.3.6 Dépliage

Le dépliage est une opération qui transforme les graphes enracinés en arbres. Si l'on voit un graphe comme une machine dont chaque transition est représentée par un arc et l'état initial est la racine, le dépliage fournit une représentation des exécutions possibles de cette machine (en fait, le graphe déplié est bisimilaire au graphe original).

Étant donné un graphe enraciné $\mathcal{G}$, son dépliage $\text{Depliage}(\mathcal{G})$ est un arbre tel que :

- les nœuds sont les chemins d'origine la racine dans $\mathcal{G}$,

- le nœud racine $\text{racine}^{\text{Depliage}(\mathcal{G})}$ est le chemin de longueur nulle $\text{racine}^{\mathcal{G}}$,

- pour toute étiquette $a$

$$ \xrightarrow{a}^{\text{Depliage}(\mathcal{G})} = \left\{ (\pi, \pi as) \mid \pi \in \mathcal{U}_{\text{Depliage}(\mathcal{G})}, \text{dest}(\pi) \xrightarrow{a}^{\mathcal{G}} s \right\}. $$
<figure><img src="image_13.png" /><figcaption>FIG. 2.10 – L'échelle enracinée (a) et son dépliage (b).</figcaption></figure>

Pour $\mathcal{G}$ un graphe et $v$ un sommet, $\text{Depliage}(\mathcal{G}, v)$ représente le graphe $\mathcal{G}$ déplié après avoir substitué $v$ à la racine.

**Exemple 2.27** L'échelle déjà rencontrée précédemment peut être dépliée. Le résultat est présenté à la figure 2.10.

**Théorème 5 (Courcelle et Walukiewicz [CW98])** Le dépliage préserve la décidabilité de la théorie monadique.

La démonstration de ce résultat dans le cas général dépasse le cadre de ce mémoire. Une version pour graphes déterministes a été donnée par Courcelle [Cou95]. Une autre démonstration de ce cas restreint est donnée au théorème 10 dans le cadre du $\mu$-calcul.

### 2.3.7 Structure arborescente

La structure arborescente peut être vue comme une extension de la notion de dépliage : sous les bonnes hypothèses, et combinées avec d'autres transformations, ces deux opérations sont équivalentes (voir les propriétés 2.29 et 2.30). Il s'agit aussi d'une construction qui a l'avantage d'avoir un sens non seulement sur les graphes, mais aussi sur les structures dans toute leur généralité.

Étant donnée une structure $S$ et une (nouvelle) étiquette #, la structure arborescente de $S$, $S^#$ est définie par :

- l'univers est l'ensemble des suites non vide d'éléments de $U_S$, c.a.d. en emplicitant la notation des langages formels, $U_S^+$,
- la relation $\xrightarrow{\#}$ duplique le dernier élément de chaque séquence. Son interprétation est

$$ \#^{S\#} = \{(Uu, Uuu) \mid U \in \mathcal{U}_S^*, u \in \mathcal{U}_S\}, $$

- la relation $R$ pour tout symbole $R$ se comporte comme dans la structure originale, mais n'affecte que le dernier élément de la séquence: son interprétation est:

$$ R^{S\#} = \{(Uu_1, \dots, Uu_{|R|}) \mid U \in \mathcal{U}_S^*, R^S(u_1, \dots, u_{|R|})\}. $$

Quand la structure arborescente est appliquée à un graphe, le résultat est aussi un graphe. Par convention, la structure arborescente issue d'un graphe enraciné est aussi un graphe enraciné, et sa racine est le mot d'une lettre *racine*.

<figure><img src="image_14.png" /><figcaption>FIG. 2.11 - La structure arborescente obtenue à partir de $\xrightarrow{a} \xrightarrow{b}$.</figcaption></figure>

**Exemple 2.28** La figure 2.11 donne un exemple de structure arborescente d'un graphe à trois sommets.

L'une des propriétés fondamentales qui justifie son introduction est donnée par le théorème 6.

**Théorème 6 (Muchnik-Walukiewicz [Wal96])** La structure arborescente préserve la décidabilité de la théorie monadique.

Historiquement, une première notion de structure arborescente a été introduite par Shelah [She75]. Elle se distinguait de la construction présente en ce qu'elle ne possédait pas la relation $\#^*$ mais à la place une relation binaire *fils* dont l'interprétation est $\{(Uu, Uuv) \mid U \in \mathcal{U}_S^*, u, v \in \mathcal{U}_S\}$. La preuve de préservation de la décidabilité de la théorie monadique de cette construction est attribuée à Stupp dans [Tho90]. Semenov [Sem84] mentionne quant à lui un résultat plus fort pour une construction possédant un prédicat unaire supplémentaire *clone* dont
<figure><img src="image_15.png" /><figcaption>FIG. 2.12 – Exemple d'obtention d'un dépliage par une structure arborescente. Seule une partie du graphe obtenu après construction de la structure arborescente est représentée.</figcaption></figure>
l'interprétation est {$Uuu | U \in \mathcal{U}_S^*, u \in \mathcal{U}_S$}. Il attribue ce résultat à Muchnik. La construction présentée dans ce travail s'obtient à partir de cette dernière par une simple interprétation booléenne positive. Une preuve publiée de ce résultat a été proposée par Walukiewicz [Wal96].

Les deux propriétés suivantes, montrent le lien qui relie cette transformation
au dépliage de graphes.

**Propriété 2.29** *Le dépliage d'un graphe s'obtient par applications successives d'une duplication, d'une construction de structure arborescente, d'une substitution finie inverse avec retour et d'une restriction aux sommets accessibles.*

**Construction.** Soit $A$ l'ensemble des étiquettes du graphe. Le principe est d'appliquer la substitution $L_a = \#a$. Cela ne suffit pas car il y a confusion quand deux arcs étiquetés différemment ont même origine et même destination. Pour résoudre ce problème on effectue en premier une $\hat{A}$-duplication où $\hat{A}$ est l'ensemble $\{\hat{a} | a \in A\}$ d'étiquettes fraîches. Suit la construction de structure arborescente puis une substitution inverse avec retour définie par le langage $L_a = \hat{a}\#\tilde{a}a$. La figure 2.12 illustre cette construction. $\square$

**Propriété 2.30** *Sur un arbre, la structure arborescente s'obtient par applications successives d'une substitution finie inverse avec retour, d'un dépliage, d'une restriction rationnelle et d'une substitution finie inverse.*

**Construction.** De nouveau $\hat{A}$ représente l'alphabet $\{\hat{a} | a \in A\}$. La première étape de la transformation consiste à ajouter des boucles étiquetées par $\#$ sur chaque sommet et à ajouter pour chaque arc étiqueté par $a$, un autre arc de mêmes extrémités mais d'orientation inverse et étiqueté par $\hat{a}$. Pour cela, on applique la substitution inverse avec retour définie par $L_{\#} = \varepsilon$, $L_a = a$ et $L_{\hat{a}} = \bar{a}$. La figure 2.13 présente cette construction.

La deuxième étape consiste à déplier le graphe obtenu. Ensuite, il s'agit d'appliquer la restriction rationnelle définie par le langage

$$
L'(\#L')^*, \quad \text{avec } L' = A^* + \hat{A}^* + \sum_{\substack{a,b \in A \\ a \neq b}} \hat{A}^* \hat{a} b A^* .
$$

La dernière opération consiste à retourner les arcs étiquetés par une lettre de $\hat{A}$.
Elle s'effectue en appliquant la substitution finie inverse avec retour définie pour
tout $a \in A$ par $L_a = a + \tilde{a}$ et par $L_{\#} = \#$. $\square$
<figure><img src="image_16.png" /><figcaption>FIG. 2.13 – Exemple de structure arborescente d’arbre obtenue par dépliage.</figcaption></figure>
## 2.4 Propriétés structurelles

Cette partie décrit des «mesures» appliquables aux graphes infinis. Elles permettent d'exprimer des contraintes structurelles sur ces graphes. En particulier, si deux graphes n'ont pas la même «mesure», alors ils ne sont pas isomorphes.

Nous présentons successivement trois propriétés de ce type et les relations qu'elles entretiennent. Cette présentation n'est aucunement exhaustive.

### 2.4.1 La largeur arborescente

La largeur arborescente associe un entier à tout graphe (ou éventuellement $\infty$) pour les graphes infinis). La définition classique (pour les graphes finis) correspond à l'existence d'une certaine forme de décomposition arborescente du graphe [RS83, RS86, RS90, Die00]. Les travaux de R. Diestel donnent une nouvelle description (à base de jeu) plus simple de cette notion. Nous présentons ici cette version et son adaptation au cas des graphes infinis proposée par Christof Löding.

Le jeu du voleur et des policiers fini se joue sur un graphe fini non étiqueté, non orienté, par deux joueurs nommés le voleur et la police. Le voleur (⊠) se trouve à chaque instant du jeu sur un sommet du graphe. La police possède quant à elle $k$ policiers (■) disposés eux aussi sur les sommets du graphe. Le jeu se déroule alors comme suit.

1. La police place ses $k$ policiers sur les sommets du graphe.

2. Le voleur choisit un sommet initial où il se place.

3. La police choisit un de ses policiers, l'enlève du graphe, et choisit un sommet du graphe sur lequel se trouvera ce policier au tour du jeu suivant.

4. Le voleur se déplace autant qu'il veut en empruntant les arcs du graphe et en évitant les policiers.

5. Le policier momentanément retiré du graphe est placé sur sa destination.

6. Le jeu reprend à l'étape 3.

La police gagne si elle arrive à placer un de ses policiers sur le même sommet que le voleur. Le voleur gagne s'il ne se fait jamais attraper, le jeu ne s'arrête pas.

Un graphe fini $G$ est de largeur arborescente $k$ si $k + 1$ est le nombre minimum de policiers permettant à la police de systématiquement attraper le voleur (c.a.d. en terme de jeu, que la police possède une stratégie gagnante). On la note $LA(G)$.

**Exemple 2.31** La figure 2.14 présente trois situations de jeux.

Le premier jeu (a) se déroule sur un arbre avec deux policiers. Dans une telle configuration les policiers sont sûrs de gagner. Pour cela, à chaque tour de jeu, l'un des policiers reste immobile et isole ainsi le voleur dans un sous-arbre. L'autre policier se déplace alors jusqu'au sommet adjacent à celui de son col- lègue en direction du voleur (comme indiqué en pointillé). Cette tactique diminue
<figure><img src="image_17.png" /><figcaption>FIG. 2.14 – Jeu du voleur et des policiers sur un arbre (a), et une boucle (b et c).</figcaption></figure>

l'espace dont dispose le voleur. Les deux policiers inversent alors leur rôle et re-commencent ainsi jusqu'à acculer le voleur dans une feuille de l'arbre. Ainsi, la largeur arborescente d'un arbre est 1 (sauf dans le cas dégénéré d'un arbre ne contenant aucun arc, auquel cas la largeur arborescente est 0).

Le deuxième jeu (b) se déroule toujours avec deux policiers, mais sur un graphe réduit à un cycle. Cette fois-ci le voleur peut garantir sa liberté. Pour cela, il attend qu'un policier décide de se déplacer, et il se rend à un endroit quelconque où aucun des policiers ne se trouvera au tour de jeu suivant. Il peut toujours le faire car, en présence d'un seul policier, l'autre se déplaçant, tous les sommets du cycle lui sont accessibles.

En revanche, si un troisième policier arrive en renfort (c), ce dernier n'a qu'à se placer sur un sommet du cycle, et ses deux confrères, en adoptant une stratégie comparable à celle de l'arbre poussent le voleur vers lui. La police gagne.

Ainsi, ces deux derniers cas montrent que la largeur arborescente d'un cycle (d'au moins trois sommets) est 2.

**Remarque 2.32** Si les policiers disposent d'une stratégie gagnante, il peuvent toujours l'utiliser avec succès après que l'on a enlevé des arcs ou des sommets du graphe. On en déduit que la largeur arborescente est croissante vis à vis de l'inclusion.

Un cas classique utile de graphe dont la largeur arborescente est connue est celui des grilles. Appelons $k \times k$-grille étiquetée par $a$ le graphe de sommets $[k] \times [k]$ et tel que l'interprétation de $\xrightarrow{a}$ soit

$$ \{((n, m), (n + 1, m)) \mid n \in [k-1], m \in [k]\} \cup \{((n, m), (n, m+1)) \mid n \in [k], m \in [k-1]\}. $$
**Propriété 2.33** Soit $k \ge 2$ un entier, la $k \times k$-grille est de largeur arborescente $k$.

La définition de la largeur arborescente s'étend aux graphes infinis en adaptant
le jeu. Deux définitions équivalentes peuvent être données (sur une idée originale
de Christof Löding):

- au début du jeu, le voleur choisit un sous-graphe fini sur lequel se déroule
le jeu fini.

- le jeu se déroule sur le graphe infini en suivant les règles du jeu fini, mais, cette fois-ci, pour gagner, le voleur doit passer une infinité de fois par un certain sommet (sa planque).

Un graphe est de largeur arborescente bornée si il est de largeur arborescente $k$ pour un $k$ fini.

De ces définitions se déduisent les résultats de Thomas et Thomassen.

**Propriété 2.34 (Thomassen [Tho88, Tho89])** Soit $\mathcal{G}$ un graphe et $k$ un entier, alors $\mathrm{LA}(\mathcal{G}) \le k$ ssi pour tout sous-graphe fini $\mathcal{H}$ de $\mathcal{G}$ on a $\mathrm{LA}(\mathcal{H}) \le k$.

**Remarque 2.35** La grille infinie n'est pas de largeur arborescente bornée, car, quel que soit le nombre de policiers, le voleur peut choisir de jouer sur une grille suffisamment grande pour gagner.

## 2.4.2 Graphe uniformément creux

La notion de graphe uniformément creux permet de mesurer la densité d'arcs
présents dans le graphe.

Un graphe $\mathcal{G}$ est *uniformément k-creux* (*k-sparse*) pour $k$ un entier positif si, pour tout sous-graphe fini $H \subseteq \mathcal{G}$ possédant $n$ sommets et $m$ arcs, on a $m \le k \cdot n$. On dit qu'un graphe est uniformément creux si il existe un entier $k$ tel qu'il soit uniformément $k$-creux.

Courcelle montre que sous cette hypothèse et pour les graphes finis, une formule du second ordre gardée peut être traduite en une formule équivalente en logique monadique [Cou03].

Un cas simple de tels graphes est celui des graphes de degré borné.

**Propriété 2.36** *Les graphes de degré borné sont uniformément creux.*

En particulier, la grille infinie est de degré borné, et donc est creuse. Pourtant, ce
graphe n'est pas de largeur arborescente bornée. Néanmoins, ceux-ci sont aussi
uniformément creux.

**Propriété 2.37** *Les graphes de largeur arborescente bornée sont uniformément creux.*
**Preuve.** Prouvons tout d'abord le résultat pour un graphe tel que deux arcs distincts (d'étiquettes différentes) ne relient pas les mêmes sommets et qu'il n'y a pas de boucles (*).

Par contraposée. Supposons un graphe non uniformément creux, et considérons un jeu à *k* policiers se déroulant sur ce graphe. Comme le graphe n'est pas uniformément creux, il existe un sous-graphe fini contenant *n* sommets et strictement plus de *k*.n arcs. Sur ce graphe, on enlève tous les sommets de degré inférieur à *k*. Cette transformation laisse le ratio arcs/sommets strictement supérieur à *k*. On itère le processus jusqu'à ce qu'il n'y ait plus de sommet de degré inférieur à *k*. Le graphe obtenu est non vide et le voleur choisit de jouer dessus. Il dispose alors d'une stratégie évidente : quand un policier décide d'aller à l'emplacement du voleur, celui-ci dispose d'au moins *k* arcs pour s'enfuir (grâce à (*)), et au plus *k* − 1 des sommets qu'il peut atteindre de la sorte sont gardés par un policier. Un au moins est libre et le voleur s'y rend. Le voleur gagne.

Considérons un graphe possédant *n* sommets, *m* arcs et *p* étiquettes. En lui enlevant toutes ses boucles (au plus *p*.*n*), puis en ne conservant qu'un arc entre toute paire de sommets reliés (un arc est gardé sur au plus 2.*p* arcs), on obtient un graphe satisfaisant (*), possédant *n* sommets et au moins (*m* − *pn*)/(2.*p* ) arcs. Le ratio arcs/sommets ainsi obtenu tend vers l'infini quand *m*/*n* tend vers l'infini. Dans un graphe non uniformément creux, il est donc possible de trouver des sous-graphes satisfaisant (*) et ayant un ratio arcs/sommets aussi grand que voulu. □

2.4.3 Sous-graphes bipartis complets

La présence de sous-graphes bipartis complets permet une autre mesure des
graphes.

Soit $k$ un entier naturel, le graphe biparti complet étiqueté par $a$ de taille $k$ est
le graphe de sommets $V = [2] \times [k]$ possédant un arc étiqueté par $a$ entre $(1, n)$
et $(2, m)$ pour tout $n \in [k]$ et tout $m \in [k]$.

La première propriété nous indique que l'hypothèse de ne pas contenir de
graphe biparti complet aussi grand que possible est moins restrictif pour un
graphe que d'être creux.

**Propriété 2.38** Si un graphe est *k*-creux, alors il existe *l* tel qu'il ne contient pas de graphe biparti complet de taille *l*.

Par contre, ces deux notions ne sont pas équivalentes comme le montre la
propriété suivante.

**Propriété 2.39** Il existe un graphe non-creux ne possédant pas de sous-graphe biparti complet de taille 2.
<figure><img src="image_18.png" /><figcaption>FIG. 2.15 – *Propriétés structurelles de graphes et inclusions mutuelles.*</figcaption></figure>

**Preuve.** Considérons le graphe $\mathcal{H}$ de sommets $\mathbb{N}$ et dont les arcs étiquetés par $a$ sont définis par

$$ \xrightarrow{a} \mathcal{H} = \{(n, n + 2^k) \mid n \in \mathbb{N}, k \in \mathbb{N}\}. $$

Ce graphe n’est pas creux car pour $k$ fixé, le graphe induit par les sommets de $[0, 2^k - 1]$ contient $(k-1)2^k + 1$ arcs pour $2^k$ sommets et le rapport de ces deux quantités n’est pas borné.

Il s’agit de montrer qu’il n’existe pas de sous-graphe de $\mathcal{H}$ de la forme

$$ \mathcal{M} = \begin{array}{ccccccc} & & m & & & p \\ & & \searrow & & \searrow & q \\ n & \rightarrow & & & & \\ & & \swarrow & & \swarrow & \end{array} $$

On a par définition $p = m + 2^k = n + 2^{k'}$ et $q = m + 2^l = n + 2^{l'}$ pour $k,l,k'$ et $l'$ entiers naturels. Supposons sans perdre de généralité que $m < n$. Alors, le calcul de $n - m$ nous donne que $2^{k'}(2^{k-k'} - 1) = 2^l(2^{l-l'} - 1)$ avec $k', k-k', l'$ et $l-l'$ positifs (car $m < n$). On en déduit que $k' = l'$ et $k = l$ et donc $p = q$. Le motif $\mathcal{M}$ n’est donc pas un sous-graphe de $\mathcal{H}$. $\square$

Ces différents résultats nous donnent donc le tableau de la figure 2.15.
# Chapitre 3

## Systèmes d'équations

La notion de système d'équations apparaît très tôt en informatique comme un outil puissant de description d'objets au même titre que les automates. Ainsi Mezei et Wright présentent-ils dès le milieu des années 70 les notions « d'équationnalité» et de «reconnaissabilité» comme propices à une généralisation aux algèbres quelconques des travaux sur les mots et sur les termes [MW67]. Ces premiers travaux sur les systèmes d'équations s'intéressaient à la représentation d'ensembles d'objets finis (les langages de mots finis ou de termes finis par exemple, ou plus généralement d'éléments d'une algèbre de type fini), et le processus de génération consistait à saturer ces ensembles par un nombre fini d'équations.

Concernant le travail présent, il convient d'utiliser une théorie similaire pour la description de structures infinies. On utilise pour cela la théorie des ordres partiels complets (en fait des $\omega$-ordres partiels complets). En effet, la notion d'ordre partiel complet permet de définir une forme de topologie sur des familles d'objets et d'attribuer un sens aux notions de limites et de continuité. Le résultat fondamental dû à Tarski [Tar55] nous enseigne que, dans ce formalisme, toutes les applications continues admettent un unique plus petit point fixe. C'est cette propriété qui permet de donner un sens aux systèmes d'équations. Dans le cas particulier étudié par Mezei et Wright, la notion de limite coïncide avec la terminaison du processus de saturation.

On étudie alors successivement deux outils permettant de travailler sur les systèmes d'équations. Le premier de ces outils est le $\mu$-calcul. Il s'agit d'une théorie qui dépasse largement le cadre de ce mémoire et seule une version restreinte en est présentée. De notre point de vue, le $\mu$-calcul est avant tout un formalisme puissant et concis permettant de décrire des ensembles de termes infinis.

Le second outil permet de transformer les termes. Il s'agit des transducteurs descendants déterministes avec anticipation $\mu$-définissable. Comme il n'y a pas d'ambiguïté dans le présent contexte, le terme de transducteur déterministe est utilisé. Là encore, les transducteurs déterministes peuvent être exécutés directe-
ment sur les systèmes d'équations : ils correspondent aux transductions monodiques de systèmes d'équations.

Le reste de ce paragraphe est construit comme suit. La partie 3.1 présente la notion d'ordre partiel complet et d'algèbre continue. La partie 3.2 introduit les systèmes d'équations et fournit les premières propriétés les concernant. La partie 3.3 est consacrée à la notion de $\mu$-définissabilité. La partie 3.4 présente quant à elle les transducteurs déterministes.

## 3.1 Ordres partiels complets et algèbres

L'outil que nous avons choisi ici pour définir la notion de limite est celui des ordres partiels complets. L'utilisation de catégories $\omega$-complètes est une autre possibilité de formalisme que nous n'avons pas adoptée ici.

Ce paragraphe commence par la présentation de la notion d'ordre partiel complet. Puis quelques exemples utiles sont donnés. Enfin ces ensembles ordonnés sont munis d'opérateurs pour former des algèbres continues.

### 3.1.1 Définitions

Étant donné un ensemble $E$ ordonné, on appelle *chaîne ascendante* (on dit parfois simplement *chaîne*) toute suite croissante, indicée par $\mathbb{N}$, d'éléments de $E$. Un *majorant* d'une chaîne ascendante est un élément de $E$ supérieur à tous les éléments de la chaîne. La *borne supérieure* d'une chaîne ascendante $u$ (si elle existe) est le plus petit majorant des éléments de la chaîne. Elle est aussi appelée *limite* de la chaîne ascendante.

Étant donné un ensemble $E$ ordonné par $\sqsubseteq$, le couple $(E, \sqsubseteq)$ est un *ordre partiel complet* (cpo pour "complete partial order" en anglais) si les deux conditions suivantes sont satisfaites :

- il existe dans $E$ un plus petit élément pour $\sqsubseteq$ (généralement noté $\perp$),

- toute chaîne ascendante $u$ admet une borne supérieure dans $E$ (généralement notée $\sqcup u$ ou encore $\sqcup_{n \in \mathbb{N}} u_n$).

Afin de rendre explicite le plus petit élément et la borne supérieure, on fait aussi référence au cpo $(E, \sqsubseteq, \perp, \sqcup)$.

**Exemple 3.1** Les entiers naturels $\mathbb{N}$ munis de l'ordre usuel $\leq$ ne forment pas un cpo. En effet, la chaîne $(n)_{n \in \mathbb{N}}$ n'est majorée par aucun entier, et donc n'admet pas de borne supérieure.

**Exemple 3.2** Les entiers naturels augmentés d'un symbole infini $\mathbb{N} \uplus \{\infty\}$ et munis de l'ordre usuel $\leq$ étendus pour tout $n$ par $n \leq \infty$ est un cpo. Son plus
petit élément est 0, et étant donné une chaîne ascendante $u$,

- si $u$ est majorée par un entier, alors $u$ est constante à partir d'un certain rang et cette constante est sa borne supérieure,

- si $u$ n'est pas bornée par un entier naturel, alors sa borne supérieure est $\infty$.

Les propriétés 3.3, 3.4, 3.5, 3.6 et 3.7 montrent comment les opérations ensemblistes usuelles peuvent être utilisées pour construire des cpos.

**Propriété 3.3 (cpo fini)** *Tout ensemble fini équipé d'un ordre partiel et possédant un plus petit élément est un cpo.*

**Propriété 3.4 (cpo pointé)** *Pour $E$ un ensemble, l'ensemble $E_\perp = E \uplus \{\perp\}$ ordonné par $u \sqsubseteq u'$ si $u = \perp$ ou $u = u'$ est un cpo appelé cpo pointé sur $E$.*

**Propriété 3.5 (cpo des parties)** *Les parties d'un ensemble, ordonnées par l'inclusion, forment un cpo dont le plus petit élément est l'ensemble vide et la borne supérieure est l'union ensembliste.*

**Propriété 3.6 (cpo produit)** *Étant donnés deux cpo $(E_1, \sqsubseteq_1, \perp_1, \sqcup_1)$ et $(E_2, \sqsubseteq_2, \perp_2, \sqcup_2)$, l'ensemble produit $E_1 \times E_2$ est un cpo quand il est ordonné par $\sqsubseteq_{E_1 \times E_2}$ défini comme suit :*

$$ (x_1, x_2) \sqsubseteq_{E_1 \times E_2} (y_1, y_2) \quad \text{si} \quad x_1 \sqsubseteq_1 y_1 \text{ et } x_2 \sqsubseteq_2 y_2. $$

La borne supérieure d'une chaîne ascendante $((u_n, v_n)_{n \in \mathbb{N}})$ est $(\sqcup_1 u, \sqcup_2 v)$ et le plus petit élément est $(\perp_1, \perp_2)$.

**Propriété 3.7 (cpo des applications)** *Étant donnés un ensemble $D$ et un cpo $(E, \sqsubseteq, \perp, \sqcup)$, l'ensemble des applications de $D$ dans $E$ est un cpo quand il est ordonné par $\sqsubseteq'$ définie par :*

$$ f \sqsubseteq' g \quad \text{si pour tout } x \in D, f(x) \sqsubseteq g(x). $$

Le plus petit élément est l'application constante égale à $\perp$. La limite d'une chaîne ascendante $f$ est alors $\sqcup'f$ définie par :

$$ \text{pour tout } x \text{ de } D, \ (\sqcup'f)(x) = \bigsqcup_{n \in \mathbb{N}} (f_n(x)). $$

**Remarque 3.8 (cpo des fonctions)** *Soient $E$ et $F$ deux ensembles. L'ensemble des applications de $E$ dans $F_\perp$ est un cpo (propriétés 3.4 et 3.7). Cet ensemble d'applications coïncide avec l'ensemble des fonctions de $E$ dans $F$, l'élément $\perp$ s'interprétant comme indéfini. Le cpo ainsi défini correspond à l'ordre de « prolongement » entre fonctions, c.a.d $f \sqsubseteq g$ si le domaine de $f$ est contenu dans le domaine de $g$ et si sur le domaine de $f$ les deux fonctions coïncident.*
Étant donnés deux cpo $(E, \sqsubseteq, \bot, \sqcup)$ et $(E', \sqsubseteq', \bot', \sqcup')$, une application $f$ de $E$ dans $E'$ est *continue* si elle commute avec la limite, c'est à dire que, pour toute chaîne ascendante $u$ de $E$, $(f(u_n))_{n \in \mathbb{N}}$ est une chaîne ascendante (notée $f(u)$), de borne supérieure

$$ \sqcup' f(u) = f(\sqcup u). $$

**Remarque 3.9 (continuité et croissance)** *Toute application continue est croissante (c'est à dire $f(x) \sqsubseteq' f(y)$ pour tout $x \sqsubseteq y$) mais la réciproque est fausse dans le cas général<fnref n="1" />.*

Considérons l'ensemble $E = \mathbb{N} \cup \{0', 1'\}$ ordonné totalement par $0 \sqsubseteq 1 \sqsubseteq \dots \sqsubseteq 0' \sqsubseteq 1'$. On vérifie aisément qu'il s'agit d'un cpo. Considérons maintenant l'application $f$ de $E$ dans $E$ définie par :

$$ \text{pour tout } n \text{ de } \mathbb{N}, f(n) = n, \quad \text{et } f(0') = f(1') = 1'. $$

Cette application est croissante sans être continue :

$$ f\left(\bigsqcup_{n \in \mathbb{N}} n\right) = f(0') = 1' \neq 0' = \bigsqcup_{n \in \mathbb{N}} n = \bigsqcup_{n \in \mathbb{N}} f(n). $$

Le résultat fondamental qui justifie l'introduction des applications continues est le suivant.

**Théorème 7 (Knaster-Tarski [Tar55])** *Toute application continue d'un cpo $(E, \sqsubseteq, \bot, \sqcup)$ dans lui-même admet un plus petit point fixe $\text{fix}(f)$ défini par :*

$$ \text{fix}(f) = \min\{x \mid f(x) = x\} = \min\{x \mid f(x) \sqsubseteq x\} = \bigsqcup_{n \in \mathbb{N}} f^n(\bot). $$

**Preuve.** Remarquons tout d'abord que $f^n(\bot)$ est une chaîne ascendante : il suffit pour cela de montrer par récurrence sur $n$ que $f^n(\bot) \sqsubseteq f^{n+1}(\bot)$ en utilisant la croissance de $f$.

Montrons maintenant qu'il s'agit d'un point fixe :

$$ \begin{aligned} f\left(\bigsqcup_{n \in \mathbb{N}} f^n(\bot)\right) &= \bigsqcup_{n \in \mathbb{N}} f\left(f^n(\bot)\right) && (\text{par continuité}) \\ &= \bigsqcup_{n \in \mathbb{N}} f^n(\bot). \end{aligned} $$

Il reste à montrer que tout point fixe lui est supérieur. Soit $c$ tel que $f(c) = c$. On montre par récurrence et croissance de $f$ que pour tout $n$, $f^n(\bot) \sqsubseteq c$. Par passage à la limite, on en déduit la propriété souhaitée. $\square$

Les propriétés 3.10, 3.11, 3.12, et 3.13 montrent que les constructions usuelles engendrent des fonctions continues.

**Propriété 3.10** *Toute application constante est continue.*

<footnote n="1">1. Elle reste vraie quand l'ensemble d'arrivée est fini.</footnote>
**Propriété 3.11** La composition de deux applications continues est une application continue.

**Propriété 3.12 (continuité dans le cpo produit)**

Étant donnés des cpos $(E, \sqsubseteq)$, $(E_1, \sqsubseteq_1)$ et $(E_2, \sqsubseteq_2)$,

- la projection sur la première composante $\pi_1$ de $E_1 \times E_2$ dans $E_1$ définie par $\pi_1(x, y) = x$ est continue,

- la projection sur la seconde composante $\pi_2$ de $E_1 \times E_2$ dans $E_2$ définie par $\pi_2(x, y) = y$ est continue,

- pour deux applications continues $f$ et $g$ respectivement de $E$ dans $E_1$ et de $E$ dans $E_2$, l'application $f \times g$ de $E$ dans $E_1 \times E_2$ définie par $(f \times g)(x) = (f(x), g(x))$ est continue.

**Propriété 3.13 (continuité dans le cpo des applications)**

Considérons un ensemble $D$ et deux cpos $(E, \sqsubseteq)$, $(E', \sqsubseteq')$ alors,

- pour tout $x$ de $D$, l'application «$eval_d$» de $E^D$ dans $E$ qui à $f$ associe $f(x)$ est continue,

- étant donnée pour tout $d$ de $D$ une application $f_d$ de $E$ dans $E'$, l'application de $E$ dans $E'^D$ qui à $x$ associe l'application qui à $d$ associe $f_d(x)$ est continue<fnref n="2" />.

La combinaison de toutes ces propriétés permet de donner un sens à la continuité des applications de plusieurs variables. En fait, toutes les combinaisons «naturelles» de telles applications sont aussi continues.

Une définition naturelle d'un morphisme précise que celui-ci est continu et préserve le plus petit élément. Un tel morphisme préserve la notion de point fixe.

**Propriété 3.14 (les morphismes de cpos préservent les points fixes)** Soient deux cpos $E$ et $F$ et $\eta$ une application continue de $E$ dans $F$ satisfaisant $\eta(\perp) = \perp$. Pour toutes applications continues $f$ et $g$ respectivement de $E$ dans $E$ et de $F$ dans $F$, si $\eta \circ f = g \circ \eta$ alors $\eta(\text{fix}(f)) = \text{fix}(g)$.

**Propriété 3.15 (continuité à la limite)** Soient $D$ et $E$ des cpos, et $f$ une chaîne ascendante d'applications continues de $D$ dans $E$, alors la borne supérieure de $f$ est une application continue de $D$ dans $E$.

Donnons pour finir une propriété permettant de construire des cpos à partir de fonctions continues.

<footnote n="2">2. Une manière plus intuitive de dire la même chose consiste à revenir à la définition de la continuité et à utiliser la notation d'abstraction $\lambda$: pour toute chaîne ascendante $u$, $\lambda d.f_d(u)$ est une chaîne ascendante et $\sqcup(\lambda d.f_d(u)) = \lambda d.f_d(\sqcup u)$. On peut ainsi dire que la borne supérieure «commute» avec le $\lambda$.</footnote>
**Propriété 3.16 (cpo des points fixes)** Soit $(E, \sqsubseteq)$ un cpo et $f$ une application continue de $E$ dans $E$, alors l'ensemble des points fixes de $f$ munis de l'ordre $\sqsubseteq$ est un cpo. La borne supérieure de ce cpo coïncide avec celle de $E$ restreinte aux points fixes de $f$, mais attention, le plus petit élément est le plus petit point fixe de $f$ et n'est pas en général le plus petit élément de $(E, \sqsubseteq)$.

Si de plus $f$ satisfait pour tout $x \in E$, $x \sqsubseteq f(x)$, alors, pour tout élément $x \in E$, il existe un plus petit point fixe $f^*(x)$ de $f$ qui lui soit supérieur, et l'application $f^*$ est continue.

Une application de ce résultat concerne les relations binaires sur un ensemble $F$. Ces relations forment un cpo pour l'inclusion (les parties du produit $F \times F$). Considérons maintenant l'application des relations binaires dans les relations binaires qui à $R$ associe $R \cup RR \cup R^{-1}$ (où $RR(x, z)$ si $R(x, y)$ et $R(y, z)$ pour un certain $z \in F$ et $R^{-1}(x, y)$ si $R(y, x)$). Elle est continue, et donc l'ensemble de ses points fixes forme un cpo (propriété 3.16). Or, les points fixes de cette application sont les relations d'équivalences. Enfin, la propriété 3.16 nous enseigne que l'application associant à chaque relation sa clôture réflexive symétrique et transitive est continue. Bien entendu, un raisonnement similaire fonctionne pour toute autre forme de clôture.

## 3.1.2 Quelques ordres partiels complets

Nous avons déjà présenté au chapitre précédent la théorie des cpos. Il s'agit ici, de manière plus pragmatique, de l'instancier au travers des constructions dont nous aurons l'usage dans le reste de ce mémoire.

### Cpo des langages

Un *langage de termes* est un ensemble de termes finis. De même, un *langage de mots* est un ensemble de mots finis. L'ensemble des langages de termes (resp. de mots) ordonné par l'inclusion forme un cpo d'après la propriété 3.5. Ils correspondent au contexte des travaux de Mezei et Wright. Le plus petit élément de ces cpos est le langage vide. La borne supérieure coïncide avec l'union ensembliste.

On dispose alors des fonctions continues suivantes :

- l'union est une application continue,

- pour $f$ une application $n$-aire des termes dans les termes (resp. des mots dans les mots), alors son extension aux langages est continue, c.a.d :

$$f(L_1, \dots, L_n) = \{f(t_1, \dots, t_n) \mid t_1 \in L_1, \dots, t_n \in L_n\}.$$

### Cpo des structures et des graphes

Les structures relationnelles sont munies de l'ordre de l'inclusion : étant données deux structures $S$ et $S'$, $S \subseteq S'$ si $U_S \subseteq U_{S'}$ et pour tout symbole relationnel
$R, R^S \subseteq R^{S'}$. Les structures<fnref n="3" /> munies de l'ordre partiel $\subseteq$ forment un cpo (il s'agit de nouveau d'une variante de la propriété 3.5). Le plus petit élément de ce cpo est la structure vide qui a pour univers $\emptyset$ et pour interprétation de toute relation $\emptyset$.

Le cpo des graphes n'est qu'une instantiation du cpo des structures aux graphes. La même notation $\subseteq$ est utilisée.

Une variante du cpo des structures est le *cpo des structures avec quotient*. Il s'agit en fait du même cpo, si ce n'est que l'on utilise la relation $\sim$ et que celle-ci doit-être une congruence (voir d'éfinition des structures avec quotient). Il s'agit bien d'un cpo d'après la propriété 3.16. La relation d'ordre est $\subseteq$, le plus petit élément est la structure vide et la borne supérieure est l'opération $\cup$ sur les structures.

Remarquons que l'application qui a une structure avec quotient associe sa structure quotient n'est pas continue.

## Cpo des termes infinis

Un autre cpo fondamental dans ce travail est celui des termes infinis. Considérons un ensemble de symboles pointés $\mathcal{F}_{\perp}$. Rappelons qu'il existe une bijection entre les termes et leur langage de branches (propriété 2.5). Cette bijection reste valide si l'on restreint le langage aux branches sans le symbole $\perp$. C'est cette caractérisation qui permet d'exprimer l'ordre sur les cpos de la manière la plus compacte.

Ainsi, considérons sur les termes infinis de $\mathcal{T}^{\omega}(\mathcal{F}_{\perp})$, la relation d'ordre $\sqsubseteq$ définie par :

$$ t \sqsubseteq t' \quad \text{si} \quad \mathcal{L}\mathcal{B}(t) \cap (\mathcal{F} + \mathbb{N})^* \subseteq \mathcal{L}\mathcal{B}(t') . $$

Cette relation s'interprète comme "t est obtenu en remplaçant dans $t'$ certains sous-termes (éventuellement une infinité) par $\perp$". Par exemple, $\perp \subseteq f(\perp, \perp) \subseteq f(\perp, a(b(\perp))) \subseteq f(c, a(b(c)))$. Les termes de $\mathcal{T}^{\omega}(\mathcal{F}_{\perp})$ ordonnés par cette relation forment un cpo :

- le plus petit élément est $\perp$,

- la borne supérieure s'obtient en effectuant l'union des langages de branches et en reconstruisant un terme à partir de ce langage.

Une propriété de ce cpo est que tout terme peut être décrit comme la limite d'une suite de termes finis.

Plus précisément, on construit par récurrence sur $n$ pour tout $\mathcal{F}_{\perp}$-terme $t$ (éventuellement infini) le terme fini $t_{\downarrow n}$ qui est identique à $t$ si ce n'est que tous

<footnote n="3">3. Pour être rigoureux, les structures ne forment pas à strictement parler un ensemble et donc un cpo. Pour cela, il faudrait se fixer un univers global. Nous n'entrons pas ici dans ces détails qui obscurcissent le propos et les notations sans pour autant correspondre à une véritable difficulté technique.</footnote>
les sous-termes situés à la profondeur $n$ sont «élagués» et remplacés par $\perp$ :

$$ t_{\downarrow n} = \begin{cases} \perp & \text{si } n = 0, \\ f(t_1 \downarrow_{n-1}, \dots, t_{|f|} \downarrow_{n-1}) & \text{si } n > 0 \text{ et } t = f(t_1, \dots, t_{|f|}). \end{cases} $$

On a alors la propriété suivante.

**Propriété 3.17** Pour tout terme $t$ de $T^\omega(\mathcal{F}_\perp)$,

$$ \bigcup_{n \in \mathbb{N}} t_{\downarrow n} = t. $$

Ce résultat permet ainsi de décrire des applications sur les termes infinis par prolongement d'applications sur les termes finis.

**Propriété 3.18** Soit $f$ une application croissante de $T(\mathcal{F}_\perp)$ dans un cpo $E$. Alors, il existe une unique application continue de $T^\omega(\mathcal{F}_\perp)$ dans $E$ qui coïncide avec $f$ sur $T(\mathcal{F}_\perp)$.

### 3.1.3 Algèbres et algèbres continues

Étant donné un alphabet gradué $\mathcal{F}$, une $\mathcal{F}$-algèbre est un ensemble $\mathbf{A}$ muni d'une application sem$[\mathbf{A}]$ qui associe à chaque symbole $f$ de $\mathcal{F}$ une application de $\mathbf{A}^{|f|}$ dans $\mathbf{A}$. Les symboles de $\mathcal{F}$ sont appelés des opérateurs et sem$[\mathbf{A}]$ est l'application de sémantique. Pour cette raison, on parle aussi de domaines sémantiques au lieu d'algèbres. Les opérateurs d'arité 0 sont appelés opérateurs constants. L'intérêt de cette définition est qu'il est possible de considérer plusieurs $\mathcal{F}$-algèbres sur des ensembles différents mais partageant la même dénomination des opérateurs. Le plus souvent, le contexte permet de déterminer l'application de sémantique sans ambiguïté. Dans un tel cas, pour un symbole $f$ et $e_1, \dots, e_{|f|}$ des éléments de $\mathcal{F}$, on notera simplement $f(e_1, \dots, e_{|f|})$ au lieu de sem$[\mathbf{A}](f)(e_1, \dots, e_{|f|})$.

Un morphisme d'algèbre d'une $\mathcal{F}$-algèbres $\mathbf{A}$ dans une $\mathcal{F}$-algèbre $\mathbf{A}'$ est une application $\phi$ de $\mathbf{A}$ dans $\mathbf{A}'$ telle que pour tout $f \in \mathcal{F}$ et $e_1, \dots, e_{|f|} \in \mathbf{A}$,

$$ \phi(f(e_1, \dots, e_{|f|})) = f(\phi(e_1), \dots, \phi(e_{|f|})). $$

Une $\mathcal{F}$-algèbre $\mathbf{A}$ est libre si pour tous symboles $f$ et $f'$ de $\mathcal{F}$ et tous éléments $e_1, \dots, e_{|f|}, e'_1, \dots, e'_{|f'|}$ de $\mathbf{A}$,

$$ \text{si } f(e_1, \dots, e_{|f|}) = f'(e'_1, \dots, e'_{|f'|}) \text{ alors } f = f' \text{ et pour tout } i, e_i = e'_i. $$

**Propriété 3.19** Pour $\mathcal{F}$ un alphabet gradué, l'ensemble des termes $T^\omega(\mathcal{F})$ (resp. des termes finis $T(\mathcal{F})$) est une algèbre libre.
Pour un alphabet gradué $\mathcal{F}$ et une $\mathcal{F}$-algèbre $\mathbf{A}$, il existe un et un seul morphisme d'algèbre de $\mathcal{T}(\mathcal{F})$ dans $\mathbf{A}$. Il est appelé morphisme canonique et l'image d'un terme $t$ par ce morphisme est notée $\llbracket t \rrbracket_{\mathbf{A}}$. Ce morphisme associe à une expression (c.a.d. un terme) sa valeur dans l'algèbre. On note $\llbracket t \rrbracket$ à la place de $\llbracket t \rrbracket_{\mathbf{A}}$ quand il n'y a pas d'ambiguïté sur l'algèbre concernée.

Une $\mathcal{F}$-algèbre continue $\mathbf{A}$ est une $\mathcal{F}$-algèbre munie d'un ordre partiel complet telle que pour tout opérateur $f \in \mathcal{F}$ l'application $\text{sem}[\mathbf{A}](f)$ est continue. Un morphisme d'algèbres continues est un morphisme continu d'algèbres continues qui préserve le plus petit élément. Bien entendu, la composition de deux morphismes d'algèbres continues est encore un morphisme d'algèbres continues. L'ensemble des termes de $\mathcal{T}^{\omega}(\mathcal{F}_{\perp})$ forme une $\mathcal{F}$-algèbre continue.

Étant donnée une $\mathcal{F}$-algèbre continue $\mathbf{A}$, il existe un unique morphisme d'algèbres continues de $\mathcal{T}^{\omega}(\mathcal{F}_{\perp})$ dans $\mathbf{A}$. Ce morphisme coïncide avec le morphisme canonique sur les termes finis. Il est ensuite prolongé par continuité de manière unique grâce à la propriété 3.18. Naturellement, comme pour les algèbres, ce morphisme est appelé morphisme canonique et l'image d'un terme $t$ par ce morphisme est sa valeur, notée $\llbracket t \rrbracket_{\mathbf{A}}$. On utilise de même la version abrégée $\llbracket t \rrbracket$ lorsqu'il n'y a pas d'ambiguïté sur l'algèbre continue correspondante.

**Exemple 3.20** Considérons l'alphabet gradué $\mathcal{F}_N = \{0:0,1:0,\infty:0,+:2,\ast:\infty:2\}$. On utilise les notations infixes $t+t'$ et $t\ast t'$ au lieu de $(t,t')$ et $(t,t')$ (ainsi que les priorités habituelles sur ces opérateurs).

Soit donc $N$ la $\mathcal{F}_N$-algèbre de domaine $N \cup \{\infty\}$ dont la sémantique est donnée par

$$ \begin{array}{l} \text{sem}[N](0) = 0, \quad \text{sem}[N](1) = 1, \quad \text{sem}[N](\infty) = \infty, \\ \text{sem}[N](+)(n, n') = \begin{cases} n + n' & \text{si } n \in N \text{ et } n' \in N, \\ \infty & \text{sinon}, \end{cases} \\ \text{sem}[N](\ast)(n, n') = \begin{cases} nn' & \text{si } n \in N \text{ et } n' \in N, \\ 0 & \text{si } n = 0 \text{ ou } n' = 0, \\ \infty & \text{sinon}. \end{cases} \end{array} $$

Comme vu précédemment, $N \cup \{\infty\}$ muni de l'ordre usuel $\leq$ forme un cpo. Pour cet ordre, les sémantiques des opérateurs sont continues (en particulier, on a posé $\infty \ast 0 = 0 \ast \infty = 0$ afin d'assurer cette continuité). L'algèbre $N$ est donc une algèbre continue.
## 3.2 Systèmes d'équations

### 3.2.1 Une première définition

Un $\mathcal{F}$-système d'équations est un triplet $(X, x_0, Eq)$ où

- $X$ est un ensemble (éventuellement infini) de variables, identifiable à de nouveaux symboles d'arité 0 ($X$ et $\mathcal{F}$ sont disjoints),

- $x_0 \in X$ est la variable résultat,

- $Eq$ est une application qui à chaque variable $x$ associe un terme de $\mathcal{T}(\mathcal{F} \uplus X)$; on utilise la syntaxe $x = Eq(x)$ qui est appelée équation.

Il est important de noter qu'aucune contrainte de finitude n'est imposée.

Pour attribuer une unique solution à un $\mathcal{F}$-système d'équations, on l'évalue dans une $\mathcal{F}$-algèbre continue. Considérons donc un $\mathcal{F}$-système d'équations $S = (X, x_0, Eq)$ et une $\mathcal{F}$-algèbre continue $\mathbf{A}$. On appelle valuation du système une application $\rho$ de $X$ dans $\mathbf{A}$. L'ensemble des valuations est muni d'une structure de cpo d'après la propriété 3.7. Pour $\rho$ une valuation, $\mathbf{A}\{\rho\}$ dénote la $\mathcal{F} \uplus X$-algèbre dont la sémantique coïncide avec celle de $\mathbf{A}$ sur $\mathcal{F}$, et est égale à $\rho$ sur $X$. Soit alors $F[\mathbf{A}, S]$ l'application des valuations dans elles-mêmes définie par :

$$F[\mathbf{A}, S](\rho) = \rho' \text{ définie pour tout } x \text{ de } X \text{ par } \rho'(x) = [[Eq(x)]]_{\mathbf{A}\{\rho\}}.$$

L'application $F[\mathbf{A}, S]$ s'interprète comme une étape de propagation des calculs dans le système. Les propriétés 3.11, 3.12 et 3.13 montrent alors la continuité de $F[\mathbf{A}, S]$. Cette application admet donc un unique plus petit point fixe (théorème 7) et il est par conséquent valide de définir la solution de $S$ dans $\mathbf{A}$ comme la valeur de la solution de $F[\mathbf{A}, S]$ à la racine :

$$\text{Solution}[\mathbf{A}](S) = (\text{fix}(F[\mathbf{A}, S]))(x_0).$$

Bien souvent, il n'est pas ambigu de ne pas préciser l'algèbre continue $\mathbf{A}$. On note alors simplement $\text{Solution}(S)$ au lieu de $\text{Solution}[\mathbf{A}](S)$.

La propriété suivante montre que la solution d'un $\mathcal{F}$-système d'équations est préservée par morphisme d'algèbres continues.

**Propriété 3.21** Soient deux $\mathcal{F}$-algèbres continues $\mathbf{A}$ et $\mathbf{A}'$, et $\phi$ un morphisme d'algèbres continues de $\mathbf{A}$ dans $\mathbf{A}'$. Pour tout $\mathcal{F}$-système d'équations $S$, on a

$$\phi(\text{Solution}[\mathbf{A}](S)) = \text{Solution}[\mathbf{A}'](S).$$

**Preuve.** Conséquence directe de la propriété 3.14. □

<figure><img src="image_19.png" /></figure>

Le corollaire suivant montre qu'il est suffisant de résoudre les systèmes d'équations dans les termes infinis puis d'envoyer la solution par morphisme canonique dans l'algèbre continue voulue.
**Corollaire 3.22** Pour tout alphabet gradué $\mathcal{F}$, toute $\mathcal{F}$-algèbre continue $\mathbf{A}$ et tout $\mathcal{F}$-système d'équations $S$,

$$ \text{Solution}[\mathbf{A}](S) = [\text{Solution}[\mathcal{T}^{\omega}(\mathcal{F})](S)]_{\mathbf{A}}. $$

**Remarque 3.23** Dans certains contextes, il est utile de pouvoir utiliser plusieurs algèbres continues et des systèmes d'équations mettant en jeu des variables dont la valuation appartient à l'une ou l'autre de ces algèbres. Ce besoin coïncide avec une vision communément admise de la notion de type : chaque valeur possède un type qui définit les différentes opérations dans lesquelles elle est susceptible d'être utilisée.

Le modèle de systèmes d'équations décrit jusqu'à présent ne possède pas cette capacité. Il est pourtant possible de la simuler en utilisant une algèbre contenant l'union disjointe de toutes les algèbres utilisées dans le système d'équations. Plus précisément, une algèbre continue sortée est décrite par la donnée :

- d'une famille de cpos $(E_i)_{i \in I}$,

- un alphabet $\mathcal{F}$,

- d'une application de sorte $\rho$ de $\mathcal{F}$ dans $I^* \times I$,

- et une application sémantique $\rho$ qui à chaque symbole $f$ de $\mathcal{F}$ de type $\rho(f) = (\tau_1 \dots \tau_n, \tau)$ associe une application de $E_{\tau_1} \times \dots \times E_{\tau_n}$ dans $E_{\tau}$.

Le reste des définitions et des propriétés n'est pas modifié par cette extension.

### 3.2.2 Systèmes d'équations comme graphes

Pour représenter un système d'équations comme un graphe, on se restreint aux systèmes d'équations normalisés, c'est-à-dire ceux dont les équations sont de la forme $x = f(x_1, \dots, x_{|f|})$ où $f$ est un symbole et $x_1, \dots, x_{|f|}$ sont des variables du système d'équations.

Normaliser un système consiste à produire un système normalisé dont la solution est la même que celle du système original. Il est toujours possible de normaliser un système d'équations pourvu que l'on dispose d'une représentation de $\perp$ comme solution d'un système d'équations. En effet, le processus de normalisation consiste à introduire des variables intermédiaires pour décomposer les termes de hauteur supérieure à deux en termes de hauteur un. Le problème intervient lorsqu'un terme de hauteur 0 apparaît dans le système comme par exemple dans l'équation $x = x$. La plus petite solution de cette équation étant $\perp$, il faut disposer d'une représentation normalisée de $\perp$ pour normaliser ce système.

Pour représenter un système d'équations normalisé comme un graphe, on utilise des conventions similaires à celles mises en jeu dans la définition des termes (voir page 14). Ainsi, un graphe enraciné représente un $\mathcal{F}$-système d'équations
<figure><img src="image_20.png" /><figcaption>FIG. 3.1 – Un graphe enraciné (a) représentant un système d'équations (b) et son dépliage (c).</figcaption></figure>

normalisé si ses étiquettes sont dans l'alphabet $\mathcal{F} \cup \mathbb{N}$ et que l'ensemble des sommets se partage en deux ensembles $V'$ et $V''$ tels que :

- le sommet racine appartient à $V'$

- les arcs étiquetés par un symbole de $\mathcal{F}$ ont pour origine un sommet de $V'$ et pour destination un sommet de $V''$,

- les arcs étiquetés par un entier ont pour origine un sommet de $V''$ et pour destination un sommet de $V'$,

- chaque sommet de $V'$ est origine d'un unique arc,

- chaque sommet de $V''$ est destination d'un unique arc,

- si un sommet de $V''$ est destination d'un arc étiqueté par le symbole $f \in \mathcal{F}$, alors il est origine d'exactement $|f|$ arcs étiquetés respectivement par 1, ..., $|f|$.

On associe un système d'équations à un graphe enraciné représentant un système d'équations de la manière suivante :

- l'ensemble $X$ de variables est $V'$,

- la variable résultat est la racine du graphe,

- pour $x \in V'$ un sommet, celui-ci n'est origine que d'un arc étiqueté par un symbole de $\mathcal{F}$. Soit $f$ ce symbole et $y$ la destination de cet arc. On a $y \in V''$ et donc $y$ est origine d'exactement $|f|$ arcs étiquetés respectivement 1, ..., $|f|$. Soient donc $x_1, ..., x_{|f|}$ les sommets destinations de ces arcs, on pose $Eq(x) = f(x_1, ..., x_{|f|})$.
Bien entendu, la construction inverse peut être effectuée. Ce codage est donc une bijection entre les systèmes d'équations et les graphes représentant des systèmes d'équations. On se permet donc dorénavant d'identifier chaque système d'équations avec sa représentation sous forme d'un graphe.

**Exemple 3.24** Soit $\mathcal{F} = \{f : 2, g : 1, a : 0\}$ un alphabet gradué. La figure 3.1 illustre un graphe (a) représentant un $\mathcal{F}$-système d'équations (b). Le dépliage du graphe est présenté en (c). Ce terme est aussi égal à $\text{Solution}[\mathcal{T}^{\omega}(\mathcal{F})](S)$.

Cette dernière remarque se généralise comme le montre la propriété suivante.

**Propriété 3.25** Pour $S$ un graphe enraciné représentant un $\mathcal{F}$-système d'équations,

$$ \text{Depliage}(S) = \text{Solution}[\mathcal{T}^{\omega}(\mathcal{F})](S). $$

Lorsque l'on combine cette dernière propriété avec le corollaire 3.22, on obtient le résultat ci-dessous qui identifie la solution d'un système à l'image par morphisme canonique du terme infini obtenu par dépliage du système.

**Corollaire 3.26** Soit $\mathcal{F}$ un alphabet gradué, une $\mathcal{F}$-algèbre continue $\mathbf{A}$ et $S$ un $\mathcal{F}$-système d'équations, alors,

$$ \text{Solution}[\mathbf{A}](S) = [[\text{Depliage}(S)]]_{\mathbf{A}}. $$

## 3.3 $\mu$-définissabilité et $\mu$-calcul

Nous avons vu au paragraphe précédent comment représenter certains éléments d'une algèbre continue :

1. tout d'abord, comme valeur de termes infinis,

2. puis, comme solutions de systèmes d'équations.

Nous avons aussi vu que ces deux approches coïncident et le passage du système d'équations au terme s'obtenait par dépliage.

Le propos de cette partie est de représenter des parties d'une algèbre continue, c'est-à-dire d'introduire une notion de « rationnalité ». Dans cette optique, nous utilisons le $\mu$-calcul et nous définissons les ensembles $\mu$-définissables de termes. Nous verrons que cette famille de langages satisfait de nombreuses propriétés de clôtures utiles par la suite. Nous étendrons ensuite cette notion de $\mu$-définissabilité aux algèbres continues quelconques.

L'intérêt de cette approche est de disposer de tous les résultats classiques concernant le $\mu$-calcul et en particulier de ses procédures de décision. En ce sens, l'un des résultats les plus importants de cette partie est le théorème 10 (page 71) qui traduit toute $\mu$-formule exprimée sur les termes en formule monadique faisant
référence aux système d'équations. Ce résultat nous permet d'utiliser les techniques de décidabilité de la théorie monadique pour décider de l'appartenance de la solution d'un système d'équations à un ensemble $\mu$-définissable.

Le $\mu$-calcul est un formalisme qui a été bien étudié. Le lecteur interessé par une présentation plus complète du domaine peut se reporter au récent ouvrage de Arnold et Niwiński [AN01]. La théorie du $\mu$-calcul possède nombre de points communs avec celle des cpos, ne serait-ce que par la notion de point fixe qui les sous-tend toutes deux. Le parti est pris dans cet exposé de les considérer comme séparées.

### 3.3.1 Généralités sur les points fixes

La construction fondamentale du $\mu$-calcul est la possibilité de calculer des points fixes, plus petits comme plus grands. Ce premier paragraphe présente quelques résultats généraux sur la notion de point fixe. Pour garantir l'existence de points fixes, nous travaillons dans un treillis complet. Un ensemble ordonné $(E, \leq)$ est un treillis complet si :

- toute partie $X$ de $E$ admet une borne inférieure, c'est à dire un élément $e$ de $E$ noté $\wedge X$ tel que

1. pour tout $a \in X$, $e \leq a$,

2. soit $e' \in E$ tel que pour tout $a \in X$, $e' \leq a$, alors $e' \leq e$,

- toute partie $X$ de $E$ admet une borne supérieure, c'est à dire un élément $e$ de $E$ noté $\vee X$ tel que

1. pour tout $a \in X$, $a \leq e$,

2. soit $e' \in E$ tel que pour tout $a \in X$, $a \leq e'$, alors $e \leq e'$.

**Remarque 3.27** En fait, de l'existence d'une borne inférieure peut se déduire de l'existence d'une borne supérieure, et réciproquement. Ceci se montre en utilisant l'équivalence suivante:

$$ \text{pour tout } X \subseteq E, \quad \bigwedge X = \bigvee \{x \in E \mid \forall y \in X, x \leq y\}. $$

Une conséquence directe de la définition est que tout treillis complet possède un plus petit et un plus grand élément (respectivement la borne inférieure et la borne supérieure de $E$). On note $\emptyset$ le plus petit élément et $\mathbf{1}$ le plus grand.

Pour la suite, deux treillis nous intéressent.

**Le treillis des parties** : Étant donné un ensemble $A$, l'ensemble des parties de $A$, ordonné par l'inclusion est un treillis complet dont le plus petit élément est $\emptyset$, le plus grand élément est $E$, la borne inférieure coïncide avec l'intersection ensembliste, et la borne supérieure avec l'union ensembliste.
**Le treillis produit** : Pour des treillis complets $(E_1, \le_1), \dots, (E_n, \le_n), E_1 \times \dots \times E_n$ est ordonné par $(e_1, \dots, e_n) \le (e'_1, \dots, e'_n)$ si pour tout $i$, $e_i \le_i e'_i$. Il s'agit d'un treillis complet. Le plus petit (resp. grand) élément est le vecteur formé des plus petits (resp. grands) éléments des $E_i$. La borne inférieure (resp. supérieure) s'obtient en calculant la borne inférieure (resp. supérieure) composante par composante.

Pour $A_1, \dots, A_n$ des ensembles, les ensembles $E = 2^{A_1 \uplus \dots \uplus A_n}$ et $F = 2^{A_1} \times \dots \times 2^{A_n}$ sont isomorphes. L'ensemble $E$ est muni d'une structure de treillis complet en tant qu'ensemble des parties de $A_1 \uplus \dots \uplus A_n$. L'ensemble $F$ est muni d'une structure de treillis complet en tant que produit des $2^{A_i}$, chacun étant un treillis complet. En fait, les deux treillis sont isomorphes, c'est-à-dire que les ordres ainsi construits coïncident. Cette remarque permet d'assimiler tous les treillis complets que nous considèrerons par la suite à des treillis des parties.

Une application $f$ d'un treillis complet $E$ dans un treillis complet $F$ est croissante si pour tous $e, e' \in E$, si $e \le e'$ alors $f(e) \le f(e')$. Un point fixe d'une application d'un treillis complet $E$ dans lui même est un élément $e$ de $E$ tel que $f(e) = e$. Le théorème de Knaster-Tarski permet d'associer un unique plus petit point fixe et un unique plus grand point fixe à toute application croissante.

**Théorème 8 (Knaster-Tarski)** Étant donnée une application croissante $f$ d'un treillis complet $E$ dans lui même, on a

1. $\bigwedge \{e \mid e = f(e)\} = \bigwedge \{e \mid f(e) \le e\}$ est un point fixe de $f$ (le plus petit),

2. $\bigvee \{e \mid e = f(e)\} = \bigvee \{e \mid e \le f(e)\}$ est un point fixe de $f$ (le plus grand).

**Preuve.** Montrons ce résultat pour le plus petit point fixe. Soit $X = \{e \in E \mid f(e) \le e\}$. On a (a) $f(\wedge X) \le \wedge \{f(e) \mid f(e) \le e\} \le \wedge X$ (par croissance de $f$ et définition de $X$). On en déduit que $\wedge X \in X$. Par croissance de $f$, pour tout $e \in X$, $f(e) \in X$, et donc en particulier $f(\wedge X) \in X$. Il s'ensuit $\wedge X \le f(\wedge X)$. Avec (a), on obtient $f(\wedge X) = \wedge X$. Il est dès lors évident que $\wedge \{e \in E \mid e = f(e)\} = \wedge X$.

Le plus grand point fixe se déduit symétriquement. $\square$

<figure><img src="image_21.png" /></figure>

Une application $f$ d'un treillis complet $E$ dans un treillis complet $F$ est additive si pour toute partie $A$ de $E$, $f(\vee A) = \vee f(A)$. De même, une application est multiplicative si $f(\wedge A) = \wedge f(A)$. Les notions d'additivité et de multiplicitivité servent de notion de «continuité» dans notre cadre: les applications additives (resp. multiplicatives) commutent avec la borne supérieure (resp. inférieure). On s'aperçoit aisément que toute application additive (resp. multiplicative) est croissante et que les applications additives (resp. multiplicatives) sont closes par composition.
La propriété 3.28 nous permet de préciser ce que sont les applications à la fois additives et multiplicatives dans le treillis des parties.

**Propriété 3.28** Soit $f$ une application de $2^A$ dans $2^B$ pour deux ensembles $A$ et $B$. Alors, $f$ est additive et multiplicative si et seulement si il existe une fonction $\eta$ de $B$ dans $A$ et une partie $B_0$ de $B$ telle que pour tout $X \subseteq A$, $f(X) = \eta^{-1}(X) \cup B_0$.

**Preuve.** $\Rightarrow$ Supposons tout d'abord $f(\emptyset) = \emptyset$. On a alors par multiplicativité, pour $a \neq b$ de $E$, $\emptyset = f(\{a\} \cap \{b\}) = f(\{a\}) \cap f(\{b\})$. Donc, pour tout $x$ de $B$, il existe au plus un $a$ tel que $x \in f(\{a\})$. On pose dans ce cas $\eta(x) = a$. Dans les autres cas, $\eta(x)$ n'est pas défini. Par conséquent, pour tout $a \in A$, $\eta^{-1}(\{a\}) = f(\{a\})$. On obtient alors pour tout $X \subseteq A$, $f(X) = \eta^{-1}(X)$ par additivité en remplaçant $X$ par $\cup\{\{a\} \mid a \in X\}$.

Dans le cas général, on pose $B_0 = f(\emptyset)$ et pour tout $X \subseteq A$, $f'(X) = f(X) - B_0$. Par croissance de $f$, pour tout $X \subseteq A$, $B_0 \subseteq f(X)$, et donc $f'(X) \cup B_0 = (f(X) - B_0) \cup B_0 = f(X)$. L'application $f'$ est additive et multiplicative, et d'après le cas précédent, il existe $\eta$ telle que pour tout $X$, $f'(X) = \eta^{-1}(X)$. On a alors $f(X) = \eta^{-1}(X) \cup B_0$.

$\Leftarrow$ évident.

□

**Remarque 3.29** Il existe des applications additives et non multiplicatives (ou vice-versa). Considérons par exemple l'application $f$ de $2^{\{a,b\}}$ dans $2^{\{c\}}$ définie par $f(\emptyset) = \emptyset$ et $f(\{a\}) = f(\{b\}) = f(\{a,b\}) = \{c\}$. L'application $f$ est additive. En revanche $f(\{a\} \cap \{b\}) \neq f(\{a\}) \cap f(\{b\})$, et par conséquent $f$ n'est pas multiplicative.

Sous l'hypothèse d'additivité ou de multiplicativité, il est possible d'envoyer les points fixes de fonctions croissantes d'un treillis vers un autre.

**Lemme 3.30 (lemme de transfert)** Considérons $E$ et $F$ deux treillis complets et les applications

- $f$ croissante de $E$ dans $E$,

- $g$ croissante de $F$ dans $F$,

- et $\rho$ de $E$ dans $F$,

$$ \text{telles que } \rho \circ f = g \circ \rho \left( \begin{array}{ccc} E & \xrightarrow{f} & E \\ \rho|_{\downarrow} & & \rho|_{\downarrow} \\ F & \xrightarrow{g} & F \end{array} \right). $$

1. Si $\rho(\emptyset) = \emptyset$ et $\rho$ est additive alors pour $x$ le plus petit point fixe de $f$ et $y$ le plus petit point fixe de $g$, on a $\rho(x) = y$,

2. si $\rho(\mathbf{1}) = \mathbf{1}$ et $\rho$ est multiplicative alors pour $x$ le plus grand point fixe de $f$ et $y$ le plus grand point fixe de $g$, on a $\rho(x) = y$.
**Preuve.** Vérifions le cas 1. On a $g(\rho(x)) = \rho(f(x)) = \rho(x)$, donc (a) $\rho(x)$ est un point fixe de $g$.

Considérons $X = \{e \mid \rho(e) \leq y\}$. L'ensemble $X$ est non vide puisque $\rho(\emptyset) = \emptyset \leq y$. Pour tout $e \in X$, $\rho(f(e)) = g(\rho(e)) \leq g(y) = y$ donc (b) $f(e) \in X$. On a $\rho(\bigvee X) = \bigvee \rho(X) \leq y$ (additivité de $\rho$, définition de $X$ et non vacuité de $X$), donc (c) $\bigvee X \in X$. (b) et (c) donnent $f(\bigvee X) \in X$ et donc $f(\bigvee X) \leq \bigvee X$. D'après Knaster-Tarski, on a alors $x \leq \bigvee X$, et donc $\rho(x) \leq y$.

Comme $\rho(x)$ est un point fixe de $g$ et que $y$ est le plus petit point fixe de $g$, on a $\rho(x) = y$.

Le cas 2 s'obtient par symétrie du cas précédent. □

### 3.3.2 Syntaxe et sémantique du μ-calcul

Le μ-calcul introduit une syntaxe pour manipuler les notions de points fixes présentées au paragraphe précédent. L'opérateur $\mu$ calcule le plus petit point fixe et l'opérateur $\nu$ le plus grand.

Formellement, il convient de nouveau de se fixer un alphabet infini dénombrable $V_\mu$ de variables du μ-calcul. Pour un alphabet gradué $\mathcal{F}$, les formules du μ-calcul (ou μ-formules) sur $\mathcal{F}$ sont définies récursivement comme suit:

- pour $x \in V_\mu$ une variable, $x$ est une $\mu$-formule,

- pour $f$ un symbole de $\mathcal{F}$ et $\phi_1, \dots, \phi_{|f|}$ des $\mu$-formules, $f(\phi_1, \dots, \phi_{|f|})$ est une $\mu$-formule,

- pour $\phi$ une $\mu$-formule et $x \in V_\mu$ une variable, $\mu x.\phi$ est une $\mu$-formule,

- pour $\phi$ une $\mu$-formule et $x \in V_\mu$ une variable, $\nu x.\phi$ est une $\mu$-formule,

- pour $\phi$ et $\psi$ deux formules, $\phi \cap \psi$ et $\phi \cup \psi$ sont des $\mu$-formules.

On définit l'ensemble $FV(\phi)$ des variables libres d'une formule du $\mu$-calcul de façon usuelle. Une formule sans variables libres est appelée *formule close*. Les conventions habituelles concernant le renommage implicite des variables liées sont adoptées.

Pour $\phi$ et $\psi$ deux $\mu$-formules et $x$ une variable libre de $\phi$ telles que les variables libres de $\psi$ n'apparaissent pas dans $FV(\phi) - \{x\}$, on note $\phi\{\psi/x\}$ la formule $\phi$ dans laquelle toutes les occurrences libres de la variable $x$ ont été remplacées syntaxiquement par $\psi$. Si l'on fait l'hypothèse d'une $\alpha$-conversion implicite, alors il suffit de supposer que $(FV(\phi) - \{x\}) \cap FV(\psi) = \emptyset$. Plus généralement, on note $\phi\{\psi_{i/x_i}\}_{i \in [n]}$ pour signifier qu'aux $n$ variables $x_1, \dots, x_n$ ont été respectivement (et simultanément) substituées les $\mu$-formules $\psi_1, \dots, \psi_n$.

Le domaine de calcul du $\mu$-calcul<fnref n="4" /> est l'ensemble des parties de $\mathcal{T}^\omega(\mathcal{F})$. Pour un ensemble $X$ de $\mu$-variables, une valuation de $X$ est une application $\gamma$ qui

<footnote n="4">4. Pour le μ-calcul présenté dans ce travail.</footnote>
à toute variable $x \in X$ associe $\gamma(x) \subseteq \mathcal{T}^{\omega}(\mathcal{F})$. On note $\gamma, x \to E$ pour $x$ une variable et $E$ une partie de $\mathcal{T}^{\omega}(\mathcal{F})$ la valuation qui coïncide avec $\gamma$ sur le domaine de $\gamma$, et qui à $x$ associe $E$.

Etant donnée une valuation $\gamma$ de l'ensemble $X$ de $\mu$-variables, la valeur d'une
formule $\phi$ de variables libres $X$ dans le contexte $\gamma$ est une partie de $\mathcal{T}^{\omega}(\mathcal{F})$ notée
$\phi[\gamma]$ et définie récursivement par :

$$
- x[\gamma] = \gamma(x),
$$

$$
- f(\phi_1, \dots, \phi_{|f|})[\gamma] = \{f(t_1, \dots, t_{|f|}) \mid t_1 \in \phi_1[\gamma], \dots, t_{|f|} \in \phi_{|f|}[\gamma]\},
$$

$$
- (\mu x.\phi)[\gamma] = \bigcap \{A \subseteq \mathcal{T}^{\omega}(\mathcal{F}) \mid \phi[\gamma, x \to A] = A\},
$$

$$
- (\nu x.\phi)[\gamma] = \bigcup \{A \subseteq \mathcal{T}^{\omega}(\mathcal{F}) \mid \phi[\gamma, x \to A] = A\},
$$

$$
- (\phi \cap \psi)[\gamma] = \phi[\gamma] \cap \psi[\gamma],
$$

$$
- (\phi \cup \psi)[\gamma] = \phi[\gamma] \cup \psi[\gamma].
$$

On a $\mu x.x[\gamma] = \emptyset$ et $\nu x.x = \mathcal{T}^\omega(\mathcal{F})$. Ainsi, $\mathbf{1}$ est une abréviation pour $\nu x.x$, et $\emptyset$ en est une pour $\mu x.x$. Pour $\phi(x_1, \dots, x_n)$ une $\mu$-formule de variables libres $x_1, \dots, x_n$, et $A_1, \dots, A_n$ des parties de $\mathcal{T}^\omega(\mathcal{F})$, on note $\phi(A_1, \dots, A_n)$ pour $\phi(x_1, \dots, x_n)[x_i \to A_i \mid i \in [n]]$.

Une remarque fondamentale pour la suite est que toutes les constructions du
$\mu$-calcul sont croissantes.

**Lemme 3.31** *Pour $\phi(x_1, \dots, x_n)$ une $\mu$-formule de variables libres $x_1, \dots, x_n$, l'application qui à $(A_1, \dots, A_n)$ associe $\phi(A_1, \dots, A_n)$ est croissante, c.a.d. pour tout $A'_1 \subseteq A_1, \dots, A'_n \subseteq A_n$, $\phi(A'_1, \dots, A'_n) \subseteq \phi(A_1, \dots, A_n)$.*

**Preuve.** Par récurrence sur la structure de $\phi$. $\square$

<figure><img src="image_22.png" /></figure>

En combinant ce résultat au théorème 8 de Knaster-Tarski, il s’ensuit que $\mu$
et $\nu$ calculent effectivement des points fixes (ce que formalise le corollaire qui
suit).

**Corollaire 3.32** *Étant donnés une formule $\phi$ de variables libres $x, y_1, \dots, y_n$ et $A_1, \dots, A_n \subseteq \mathcal{T}(\mathcal{F})$,*

$$
\begin{array}{l@{\qquad}l}
\text{si } A = (\mu x.\phi)[y_1 \to A_1, \dots, y_n \to A_n] & \text{ou } A = (\nu x.\phi)[y_1 \to A_1, \dots, y_n \to A_n], \\
\text{alors } \phi[x \to A, y_1 \to A_1, \dots, y_n \to A_n] = A. &
\end{array}
$$

Le lemme de substitution montre qu'effectuer des substitutions à l'intérieur
de $\mu$-formules est consistant avec la valeur de ces formules.

**Lemme 3.33 (de substitution)** Soient $\phi$ et $\psi$ deux $\mu$-formules d'ensemble $X$
de variables libres, $x$ une variable et $\gamma$ une valuation de $X$, on a

$$
\phi\{\psi/x\}[\gamma] = \phi[\gamma, x \to \psi[\gamma]].
$$
**Preuve.** Par récurrence sur la structure de $\phi$.

### 3.3.3 Décomposition du $\mu$-calcul

Il s'agit ici de montrer comment décomposer une formule logique en sous-formules. Il s'agit d'une variante de la clôture de Fischer-Ladner utilisée pour la logique PDL [FL79] puis étendue pour le $\mu$-calcul [Koz83].

Soit $\phi_0$ une $\mu$-formule close, la clôture de $\phi$, notée $Cl(\phi_0)$ est le plus petit ensemble de formules closes défini par :

- $\phi_0 \in Cl(\phi_0)$,

- si $\phi \cap \psi \in Cl(\phi_0)$ alors $\phi \in Cl(\phi_0)$ et $\psi \in Cl(\phi_0)$,

- si $\phi \cup \psi \in Cl(\phi_0)$ alors $\phi \in Cl(\phi_0)$ et $\psi \in Cl(\phi_0)$,

- si $f(\psi_1, \dots, \psi_{|f|}) \in Cl(\phi_0)$ alors pour tout $i$ de $[|f|]$, $\psi_i \in Cl(\phi_0)$,

- si $\mu x.\phi \in Cl(\phi_0)$ alors $\phi\{\mu x.\phi/x\} \in Cl(\phi_0)$,

- si $\nu x.\phi \in Cl(\phi_0)$ alors $\phi\{\nu x.\phi/x\} \in Cl(\phi_0)$.

**Lemme 3.34** Pour $\phi_0$ une formule du $\mu$-calcul, $Cl(\phi_0)$ est fini.

**Preuve.** Classique. Voir [Koz83].

L'ensemble ainsi défini permet d'utiliser une formule du $\mu$-calcul $\phi$ comme un automate d'arbres dont l'ensemble d'états est $Cl(\phi)$. Le lemme ci-dessous explicite les transitions de cet automate.

**Lemme 3.35** Pour toute formule close $\phi$ du $\mu$-calcul sur l'alphabet gradué $\mathcal{F}$, il existe une application $D_{\phi}$ qui à chaque symbole $f \in \mathcal{F}$ associe une partie de $Cl(\phi)^{|f|}$ telle que :

$$ \phi[] = \left( \bigcup_{f \in \mathcal{F}} f(\psi_1, \dots, \psi_{|f|}) \right) . $$

**Preuve.** Classique. Voir [Koz83].

### 3.3.4 Extension vectorielle du $\mu$-calcul

Dans la pratique, il nuit souvent à la lisibilité de devoir traiter chaque variable du $\mu$-calcul indépendamment. C'est en particulier vrai si l'on veut effectuer des conversions entre systèmes d'équations et $\mu$-calcul. Dans de telles constructions,
il est plus aisé de considérer toutes les variables du système d'équations comme un vecteur sur lequel les opérateurs de point fixe peuvent agir. C'est cette possibilité que propose l'extension vectorielle du μ-calcul. La propriété 3.37 montre que cette extension n'augmente pas l'expressivité du formalisme. Cette équivalence nous permet donc d'utiliser ces constructions vectorielles comme des raccourcis de notations.

Soit $\theta \in \{\mu, \nu\}, x_1, \dots, x_n$ des variables, $\phi_1, \dots, \phi_n$ des μ-formules vectorielles et $i \in [n]$,

$$ \theta x_i . \left\{ \begin{array}{l} x_1 = \phi_1 \\ \vdots \\ x_n = \phi_n \end{array} \right\} $$

est une μ-formule vectorielle. On utilise aussi les notations ensemblistes

$$ \theta x_i . \{x_k = \phi_k \mid k \in [n]\}. $$

Les autres constructions du μ-calcul vectoriel sont celles du μ-calcul.

La sémantique de la nouvelle construction μ (resp. ν) est de calculer la plus petite (resp. la plus grande) valeur de $x_i$ solution du système d'équations entre accolades.

Formellement, pour $\gamma$ une valuation,

$$ \mu x_i . \{x_k = \phi_k \mid k \in [n]\} [\gamma] = \bigwedge \{e_i \mid \forall k \in [n], e_k = \phi_k[\delta], \delta = \gamma, x_1 \to e_1, \dots, x_n \to e_n \} $$

Cela revient à effectuer le calcul de point fixe dans le treillis produit, puis de projeter le résultat sur la i-ème composante.

On a bien évidemment pour $\theta \in \{\mu, \nu\}$, toute μ-formule $\phi$ et toute variable $x$ l'équivalence suivante :

$$ \theta x . \{x = \phi\} \equiv \theta x . \phi \qquad (3.1) $$

Pour plus de deux équations, c'est alors la transformation suivante qui s'applique.
**Lemme 3.36** Pour $\theta \in \{\mu, \nu\}, \phi_1, \dots, \phi_n$ des μ-formules et pour $i$ de $[n]$, on a

$$ \theta x_i . \{x_k = \phi_k \mid k \in [n]\} \equiv \theta x_i . \phi_i \{\theta x_j . \{x_k = \phi_k \mid k \in [n], k \neq i\} / x_j\}_{j \in [n] - \{i\}} \quad (3.2) $$

On applique récursivement les équivalences 3.1 et 3.2 pour obtenir la propriété ci-dessous.

**Propriété 3.37 (principe de Bekič [Bek67])** Toute formule du μ-calcul vectoriel est effectivement équivalente à une formule du μ-calcul.

Ainsi, d'un point de vue expressivité, il est équivalent de considérer le μ-calcul ou le μ-calcul vectoriel.
### 3.3.5 Termes marqués

À plusieurs reprises dans ce travail, il est nécessaire de disposer d'une représentation des formules monadiques «effective» sur les arbres déterministes. La réponse classique consiste à utiliser des automates d'arbres infinis avec condition d'acceptation de Rabin ou de parité. Dans notre cas, nous utilisons le $\mu$-calcul qui est équivalent à ces deux formalismes. Deux aménagements sont néanmoins nécessaires.

- Le $\mu$-calcul ne pouvant pas manipuler des ensembles de sommets, il faut disposer d'annotations sur l'arbre pour qu'une formule monadique puisse y faire référence.

- Le $\mu$-calcul est défini pour des termes et non pour des arbres déterministes; en particulier, seuls les sommets principaux d'un terme ont une signification pour le $\mu$-calcul. Il faut donc disposer de résultats permettant de passer des arbres déterministes aux termes et réciproquement.

Les constructions de ce paragraphe ont donc pour but de préciser ces points et les notations. Il s'agit de constructions classiques.

On prend la convention que les termes ont pour ensemble de sommets leur langage de branches (cf corollaire 2.5 page 13). Ainsi, on identifie l'ensemble des sommets principaux d'un $\mathcal{F}$-terme $t$ au langage $P_t = \mathcal{LB}(t) \cap (\mathcal{FN})^*\mathcal{F}$. Pour tout $f \in \mathcal{F}$, on note $P_t^f$ l'ensemble des sommets principaux origine d'un symbole $f$, c.a.d. $P_t^f = \mathcal{LB}(t)f^{-1} = \{u \mid uf \in \mathcal{LB}(t)\}$.

Étant donné un alphabet gradué $\mathcal{F}$ et un ensemble fini $M$ de marques, on considère l'alphabet gradué $\mathcal{F}_M = \mathcal{F} \times 2^M$ avec $|(f, E)| = |f|$ pour tout $(f, E) \in \mathcal{F}_M$. Pour $f \in \mathcal{F}$ et $\phi_1, \dots, \phi_{|f|}$ des formules monadiques, on écrit $f(\phi_1, \dots, \phi_{|f|})$ à la place de $\cup_{E \subseteq M}(f, E)(\phi_1, \dots, \phi_{|f|})$. Pour $m \in M$, on écrit $m$ à la place de $\cup_{f \in \mathcal{F}, m \notin \mathcal{E}}(f, E)(\mathbf{1}, \dots, \mathbf{1})$ et $\neg m$ à la place de $\cup_{f \in \mathcal{F}, m \in \mathcal{E}}(f, E)(\mathbf{1}, \dots, \mathbf{1})$. Soit $t$ un $\mathcal{F}_M$-terme, notons $\bar{t}$ le terme obtenu de $t$ en oubliant les marques.

Un terme sur $\mathcal{F}_M$ peut être vu comme un $\mathcal{F}$-terme augmenté de marques appartenant à $M$ sur chacun des symboles. Les marques sur un $\mathcal{F}_M$-terme $t$ peuvent elles-mêmes être identifiées aux ensembles de sommets principaux de $t$. Ainsi, soit $t$ un $\mathcal{F}_M$-terme et $m \in M$, on pose $m^{-1}(t) = \{v \mid t^v \in m\}$. Pour tout terme $t$ sur $\mathcal{F}$, tout entier $n$ et tous $U_1, \dots, U_n$ ensembles de sommets principaux de $t$, on note $(t, U_1, \dots, U_n)$ l'unique $\mathcal{F}_{[n]}$-terme $t'$ tel que $\bar{t}' = t$ et pour tout $i \in [n]$, $i^{-1}(t') = U_i$.

**Lemme 3.38** Étant donnés $\mathcal{F}$ un alphabet gradué, $n$ un entier naturel, on a les propriétés suivantes.

- Pour toute formule monadique $\Phi(X_1, \dots, X_n)$, il existe une formule close du $\mu$-calcul $\phi$ telle que pour tout $\mathcal{F}$-terme $t$ et tous $U_1, \dots, U_n$ ensembles de
sommets principaux de $t$, on $a$,

$$ t \models \Phi(U_1, \dots, U_n) \quad \text{ssi} \quad (t, U_1, \dots, U_n) \in \phi[\hspace{0.5em}]. $$

- Pour toute formule close du $\mu$-calcul $\phi$, il existe une formule monadique $\Phi(X_1, \dots, X_n)$ telle que pour tout $\mathcal{F}$-terme $t$ et tous $U_1, \dots, U_n$ ensembles de sommets principaux de $t$, on $a$,

$$ t \models \Phi(U_1, \dots, U_n) \quad \text{ssi} \quad (t, U_1, \dots, U_n) \in \phi[\hspace{0.5em}]. $$

**Preuve.** Il s'agit d'une variante du théorème 9 page 70. □

<figure><img src="image_23.png" /></figure>

Ce résultat n'est pas encore suffisant pour traiter les arbres déterministes quelconques. Il faut se ramener à des ensembles de sommets principaux.

**Lemme 3.39** Étant donné un ensemble d'étiquettes $A$, il existe une transduction monadique $T$ telle que pour tout graphe déterministe $\mathcal{G}$ étiqueté par $A$,

- $T(\mathcal{G})$ est un $\{p: 2, c: 0\}$-système d'équations,

- il existe une injection $\rho$ de $V_{\text{Depliage}(\mathcal{G})}$ dans $P_{\text{Depliage}(T(\mathcal{G}))}^c$ telle que pour toute formule monadique $\Phi(X_1, \dots, X_n)$ il existe une formule monadique $\Psi(X_1, \dots, X_n)$ telle que pour toutes parties $U_1, \dots, U_n$ de $V_{\text{Depliage}(\mathcal{G})}$, on a

$$ \text{Depliage}(\mathcal{G}) \models \Phi(U_1, \dots, U_n) \quad \text{ssi} \quad \text{Depliage}(T(\mathcal{G})) \models \Psi(\rho(U_1), \dots, \rho(U_n)). $$

**Preuve.** Codage long sans difficultés particulières. □

<figure><img src="image_24.png" /></figure>

### 3.3.6 $\mu$-définissabilité

Pour $\mathcal{F}$ un alphabet gradué, les parties des termes $\mathcal{T}^\omega(\mathcal{F})$ obtenues comme valeur d'une $\mu$-formule close sont appelées parties $\mathcal{F}$-$\mu$-définissables (ou simplement $\mu$-définissables s'il n'y a pas d'ambiguïté sur l'alphabet).

Une partie $L$ d'une $\mathcal{F}$-algèbre continue $\mathbf{A}$ est $\mu$-définissable si l'ensemble $\{t \in \mathcal{T}^\omega(\mathcal{F}) \mid [[t]]_{\mathbf{A}} \in L\}$ est $\mu$-définissable.

**Remarque 3.40** On ne peut pas considérer que cette définition procure une représentation de l'ensemble $L$ par l'ensemble $L'$. En particulier, si $a \in \mathbf{A}$ est tel que $a \notin \{[[t]] \mid t \in \mathcal{T}^\omega(\mathcal{F})\}$ alors $L \cup \{a\}$ et $L - \{a\}$ sont tout autant représentés par $L'$.

Cette définition procure une représentation effective de parties d'une algèbre. Si on dispose d'algorithmes permettant de décider de l'appartenance d'un terme à
un ensemble $\mu$-définissable, alors ce test d'appartenance se transfère directement à toute algèbre continue.

**Exemple 3.41** *Considérons de nouveau l'algèbre continue N présentée à l'exemple 3.20.*

L'ensemble des termes s'évaluant en une valeur non nulle est alors $N-\mu$-définissable. Une $\mu$-formule correspondante, notée simplement ($>0$) est :

$$ (>0) = \mu x. 1 \cup \infty \cup (\mathbf{1} + x) \cup (x + \mathbf{1}) \cup (x * x), $$

c'est à dire le plus petit ensemble $E$ de termes contenant $1, \infty$, tel que la somme d'un terme de $E$ avec un terme quelconque appartient à $E$ et le produit de deux termes de $E$ appartient à $E$.

L'ensemble des termes d'valeur strictement supérieure à 1 est aussi $\mu$-définissable :

$$ (>1) = \mu x. \infty \cup ((>0) + (>0)) \cup (x + \mathbf{1}) \cup (\mathbf{1} + x) \cup (x * (>0)) \cup ((>0) * x). $$

L'ensemble des termes s'évaluant en $\infty$ est aussi $\mu$-définissable, mais la construction est plus délicate :

$$ (=\infty) = \nu x. \mu y. \begin{array}{l} \infty \\ \cup (y + \mathbf{1}) \cup (\mathbf{1} + y) \cup (y * (>0)) \cup ((>0) * y) \\ \cup (x + (>0)) \cup ((>0) + x) \cup (x * (>1)) \cup ((>1) * x). \end{array} $$

La propriété exprimée est qu'un terme s'évalue en l'infini si,

- il contient la constante $\infty$ (et que celle-ci n'est pas multipliée par 0),

- ou bien il existe une branche infinie sur laquelle :

1. toutes les opérations ont un résultat supérieur à leurs arguments, c'est à dire qu'il peut y avoir des sommes et des multiplications pourvu que l'autre argument des multiplications ne soit pas nul (y dans la formule),

2. il existe une infinité d'opérations dont le résultat est strictement supérieur aux arguments, c'est à dire une somme avec une valeur non nulle ou une multiplication par une valeur supérieure ou égale à 2 ($x$ dans la formule).

La propriété 3.42 liste quelques opérations utiles laissant les parties $\mu$-définissables invariantes.

**Propriété 3.42** *Les propriétés suivantes sont satisfaites :*

- la famille des parties $\mu$-définissables est closes par union, intersection et complémentation de chacune des parties;

- pour $f$ un symbole d'arité $n$ et $L_1, \dots, L_n$ des parties $\mu$-définissables, l'ensemble $f(L_1, \dots, L_n)$ est une partie $\mu$-définissable;
- pour tout symbole $f$ d'aritén, tout entier $i \in [n]$ et toute partie $\mu$-définissable $L$,

$$ (fi)^{-1}(L) = \{t_i \mid f(t_1, \dots, t_n) \in L\} $$

est une partie $\mu$-définissable$^5$.

**Preuve.** Toutes ces propriétés se traduisent directement dans la syntaxe du $\mu$-calcul si ce n'est celles concernant le complémentaire et $(fi)^{-1}$. Le complémentaire (notons le $\neg$) s'obtient simplement en interchangeant $\cup$ et $\cap$, $\mu$ et $\nu$ et en utilisant l'identité suivante :

$$ \neg(f(\phi_1, \dots, \phi_{|f|})) \equiv \bigcup_{g \in \mathcal{F}, g \neq f} g(\mathbf{1}, \dots, \mathbf{1}) \cup \bigcup_{i \in [|f|]} f(\mathbf{1}, \dots, \mathbf{1}, \neg(\phi_i), \mathbf{1}, \dots, \mathbf{1}) \uparrow^{\text{ième position}} $$

Étant donnée une $\mu$-formule $\phi$, la $\mu$-formule $(fi)^{-1}(\phi)$ se construit par récurrence. Si les variables libres de $\phi$ sont les $x_1, \dots, x_n$, alors les variables libres de $(fi)^{-1}(\phi)$ sont les $x_1, \dots, x_n, \hat{x}_1, \dots, \hat{x}_n$. Les variables $x$ correspondent aux mêmes valeurs que dans $\phi$ (l'expression est simplement copiée). Chaque variable $\hat{x}$, quant à elle, représente $(fi)^{-1}(x)$.

$$ \begin{array}{l} (fi)^{-1}(f(\phi_1, \dots, \phi_n)) = \phi_i \\ \text{pour } g \neq f, \quad (fi)^{-1}(g(\phi_1, \dots, \phi_{|g|})) = \emptyset \\ \qquad (fi)^{-1}(\phi \cup \psi) = (fi)^{-1}(\phi) \cup (fi)^{-1}(\psi) \\ \qquad (fi)^{-1}(\phi \cap \psi) = (fi)^{-1}(\phi) \cap (fi)^{-1}(\psi) \\ \text{pour } \theta \in \{\mu, \nu\}, \quad (fi)^{-1}(\theta x.\phi) = \theta \hat{x} \cdot \left\{ \begin{array}{l} \hat{x} = (fi)^{-1}(\phi) \\ x = \phi \end{array} \right\} \\ \qquad (fi)^{-1}(x) = \hat{x} \end{array} $$

On montre alors par récurrence la propriété suivante :

$$ (fi)^{-1}(\phi[\gamma]) = ((fi)^{-1}(\phi))[\gamma], \quad \text{avec} \quad \left\{ \begin{array}{l} \gamma'(x) = \gamma(x), \\ \gamma'(\hat{x}) = (fi)^{-1}(\gamma(x)). \end{array} \right. $$

Plus précisément, on utilise le lemme de transfert 3.30 pour les opérations de point fixe (l'application $(fi)^{-1}$ est additive et multiplicative d'après la propriété 3.28). $\square$

Citons pour finir une variante du théorème de Rabin pour le $\mu$-calcul.

<footnote n="5">5. La notation $(fi)^{-1}$ est choisie pour coïncider avec l'expression correspondante sur le langage de branches : $\mathcal{LB}((fi)^{-1}(t)) = (fi)^{-1}(\mathcal{LB}(t))$.</footnote>
**Théorème 9** Une partie $L$ de $\mathcal{T}^\omega(\mathcal{F})$ est $\mu$-définissable si et seulement si elle est monadiquement définissable, c.a.d. s'il existe une formule monadique close $\Phi$ telle que pour tout terme $t \in \mathcal{T}^\omega(\mathcal{F})$,

$$ t \in L \text{ si et seulement si } t \models \Phi. $$

Dans ce théorème, la partie délicate consiste à traduire la formule monadique en une $\mu$-formule. En fait, le théorème suivant, qui est une variante du résultat de Courcelle [Cou95] montrant que le dépliage est MS-compatible$^6$, présente une forme renforcée de la réciproque: à toute $\mu$-formule correspond une formule monadique qui est satisfaite par un graphe si et seulement si la $\mu$-formule est satisfaite sur son dépliage.

**Théorème 10** *Soit $L$ une partie $\mathcal{F}$-$\mu$-définissable. Il existe une formule monadique $\Phi$ telle que pour tout $\mathcal{F}$-système d'équations $S$ :*

$$ \mathrm{Depliage}(S) \in L \text{ si et seulement si } S \models \Phi. $$

**Preuve.** La construction de la formule monadique s'obtient par simple récurrence sur la structure de la $\mu$-formule définissant $L$. Etant donnée une $\mu$-formule $\phi$ de variables libres $x_1, \dots, x_n$, on construit la formule monadique $\phi^*(y)$ de variables libres du second ordre monadique $\hat{x}_1, \dots, \hat{x}_n$ et possédant une unique variable libre du premier ordre $y$ (exprimée comme un argument), comme suit:

$$
\begin{align*}
x^*(y) &= y \in \hat{x} \\
f(\phi_1, \dots, \phi_{|f|})^*(y) &= \exists z_1 \dots \exists z_{|f|} \bigwedge_{i \in [|f|]} \phi_i^*(z_i) \wedge y = f(z_1, \dots, z_n) \\
(\phi \cap \psi)^*(y) &= \phi^*(y) \wedge \psi^*(y) \\
(\phi \cup \psi)^*(y) &= \phi^*(y) \vee \psi^*(y) \\
(\mu x. \phi)^*(y) &= \forall \hat{x}. (\forall z. \phi^*(z) \Rightarrow z \in \hat{x}) \Rightarrow y \in \hat{x} \\
(\nu x. \phi)^*(y) &= \exists \hat{x}. (\forall z. z \in \hat{x} \Rightarrow \phi^*(z)) \wedge y \in \hat{x}
\end{align*}
$$

On reconnaît dans la traduction de la construction $\mu$ la propriété «y appartient à tout ensemble clos par $\phi^*$» ce qui correspond à un calcul de plus petit point fixe. La construction duale est appliquée à $\nu$. On montre alors par récurrence sur $\phi$ que pour toute valuation $\gamma$ et tout sommet $v$ :

$$ \begin{array}{l} \textit{Depliage}(S, v) \in \phi[\gamma] \quad \text{si et seulement si} \quad \gamma', S \models \phi^*(v) \\ \text{avec } \gamma'(\hat{x}) = \{s \in S \mid \textit{Depliage}(S, s) \in \gamma(x)\}. \end{array} $$

□

<footnote n="6">6. Le résultat complet est généralement attribué à Courcelle et Walukiewicz, mais la restriction aux graphes déterministes dont il est question ici lui est antérieure.</footnote>
## 3.4 Transducteurs déterministes

Nous avons vu comment les systèmes d’équations permettaient de représenter des éléments d’une algèbre continue. Nous avons aussi présenté la notion de $\mu$-définissabilité qui permet de représenter des parties d’une algèbre continue et de tester l’appartenance d’une solution d’un système d’équations à une telle partie. Il s’agit maintenant de fournir un formalisme permettant de transformer les systèmes d’équations : les transducteurs déterministes (descendant avec anticipation $\mu$-définissable).

Historiquement, les transducteurs de termes ont été introduits dans le cadre de la théorie de la compilation au début des années 70. Ces transducteurs permettent de mettre en relation des termes finis. Une introduction à ce domaine est disponible dans [CDG+97]. Une famille particulièrement intéressante de tels transducteurs a été proposée par Engelfriet[Eng77], celle des transducteurs descendants déterministes avec anticipation régulière (deterministic top-down transducers with regular lookahead). Ces transducteurs possèdent de bonnes propriétés de décidabilité et de clôture. Engelfriet [Eng94] a aussi montré l’étroit lien qu’entretiennent ces transformations d’arbres finis avec les transformations de graphes finis.

C’est dans un objectif similaire que nous considérons les transducteurs dans ce mémoire. Cependant, la théorie classique n’est pas suffisante dans le cas présent car il nous faut manipuler des objets infinis à la place de familles d’objets finis. Pour cette raison, nous présentons ici une adaptation d’une partie de cette théorie aux termes infinis (cette extension a été originellement considérée dans [CL04]). L’objectif est de définir une classe de transformations de termes infinis satisfaisant les conditions informelles suivantes :

- elle doit être suffisamment expressive pour capturer les transformations utiles dans le reste de ce travail,

- la validité des transformations doit pouvoir être montrée simplement,

- ces transformations doivent pouvoir être exécutées symboliquement sur une version repliée d'un terme infini, c'est à dire sur un système d'équations.

### 3.4.1 Définition

Un *transducteur descendant déterministe avec anticipation $\mu$-définissable* (ou plus simplement dans le reste de ce travail, un *transducteur déterministe*) est un quintuplet $t = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$ où :

- $\mathcal{F}$ est un alphabet gradué, l'alphabet d'entrée,

- $\mathcal{F}'$ est un alphabet gradué, l'alphabet de sortie,

- $Q$ est un ensemble fini, l'ensemble des états,
- $q_{init}$ est un élément de $Q$, l'état initial,

- $\delta$ est un ensemble fini de transitions de l'une des formes suivantes :

- $q(x) \to f(q_1(x), \dots, q_{|f|}(x)) \quad (\text{production de } f)$
  avec $f \in \mathcal{F}', q_1, \dots, q_{|f|} \in Q$ et $x$ une variable$^7$.

- $q(f(x_1, \dots, x_{|f|})) \to r(x_i) \quad (\text{consommation de } f)$
  avec $f \in \mathcal{F}$, $q, r \in Q$, $i \in [|f|]$ et $x_1, \dots, x_{|f|}$ variables.

- $q(x \in L) \to r(x) \quad (\text{anticipation de } L)$
  avec $q, r \in Q$, $L$ une partie $\mu$-définissable de $\mathcal{T}^\omega(\mathcal{F})$ et $x$ une variable.

On appelle $q$-transition toute transition de $\delta$ dont l'état de tête est $q$. On fait aussi référence à un état $q$ en tant qu'état de production (resp. de consommation, d'anticipation) s'il existe une $q$-transition de production (resp. de consommation, d'anticipation).

Déterminisme: on impose de plus les contraintes suivantes sur les transitions :

- s'il existe dans $\delta$ une $q$-transition de production alors il s'agit de la seule $q$-transition de $\delta$.

- s'il existe dans $\delta$ une $q$-transition de consommation alors il s'agit de la seule$^8$ $q$-transition de $\delta$.

- s'il existe dans $\delta$ une $q$-transition d'anticipation alors toutes les $q$-transitions sont d'anticipation et pour deux $q$-transitions distinctes
  $q(x \in L_1) \to q_1(x)$ et $q(x \in L_2) \to q_2(x)$, on a $L_1 \cap L_2 = \emptyset$.

L'application d'un transducteur déterministe à un terme infini est définie par application des transitions de $\delta$ comme des règles de récriture, puis passage à la limite. Il faut pourtant être prudent: on ne peut en effet construire l'image d'un terme infini par un transducteur déterministe comme la limite de l'image d'une suite de termes finis; en effet, les fonctions calculées par les transducteurs déterministes ne sont pas, en général, continues.

Considérons donc un transducteur déterministe $\mathbf{t} = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$. On définit par récurrence sur $n$, pour tout état $q$ et tout terme $t \in \mathcal{T}^\omega(\mathcal{F})$, le terme $\delta_n(q, t) \in \mathcal{T}(\mathcal{F}'_\perp)$ par :

- pour tout $t \in \mathcal{T}^\omega(\mathcal{F})$ et tout $q \in Q$, $\delta_0(q, t) = \perp$,

- pour tout $t \in \mathcal{T}^\omega(\mathcal{F})$, tout $q \in Q$ et tout entier $n$,
  si $q(x) \to f(q_1(x), \dots, q_{|f|}(x)) \in \delta$, $\delta_{n+1}(q, t) = f(\delta_n(q_1, t), \dots, \delta_n(q_{|f|}, t))$,
  si $q(f(x_1, \dots, x_{|f|})) \to r(x_i) \in \delta$, $\delta_{n+1}(q, f(t_1, \dots, t_{|f|})) = \delta_n(r, t_i)$,
  si $q(x \in L) \to r(x) \in \delta$, et $t \in L$, $\delta_{n+1}(q, t) = \delta_n(r, t)$,

<footnote n="7">7. Nous n'introduisons pas ici d'ensemble de variables : celles-ci sont présentes uniquement pour des raisons de lisibilité des règles. Elles peuvent tout aussi bien être omises dans la définition.</footnote>

<footnote n="8">8. Cette contrainte peut sembler excessive, mais il est toujours possible de s'y ramener en faisant précéder la transition de consommation de transitions d'anticipations.</footnote>
- si aucune règle ne s'applique ou bien si le membre droit de la règle n'est pas défini, alors $\delta_n(q, t)$ n'est pas défini.

Remarquons tout d'abord que, grâce aux hypothèses de déterminisme, deux règles ne peuvent pas s'appliquer sur un même couple état-terme. Par conséquent, si $\delta_n(q, t)$ est défini, alors il l'est de manière unique. On montre ensuite aisément par récurrence sur $n$ que pour tout terme $t$ et tout état $q$, la suite $(\delta_n(q, t))_{n \in \mathbb{N}}$ est soit croissante (pour $\sqsubseteq$), soit non définie à partir d'un certain rang<fnref n="9" />. Dans le premier cas, on pose $t_q(t)$ égale à $\sqcup_{n \in \mathbb{N}} \delta_n(q, t)$, dans le second, $t_q(t)$ n'est pas défini. L'image d'un terme par un transducteur déterministe $t = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$ est alors simplement $t(t) = t_{q_{init}}(t)$.

**Exemple 3.43** Reprenons l'exemple 3.41. Il s'agit maintenant de simplifier un terme de $\mathcal{T}^\omega(N)$ tout en en préservant sa valeur. Ce résultat s'obtient symboliquement grâce à un transducteur déterministe. Considérons le transducteur déterministe $t = (N, N, \{q_0, q\}, q_0, \delta)$ avec $\delta$ défini par :

$$ \begin{array}{lclcl} q_0(x) & \to & \infty & \quad & \text{sin } [x]_N = \infty, \\ \text{sinon} & q_0(x) & \to & 0 & \quad & \text{sin } [x]_N = 0, \\ \text{sinon} & q_0(x) & \to & q(x), & & \\ & & & & & \end{array} $$

$$ \begin{array}{lclcl} q(x) & \to & 1 & \quad & \text{sin } [x]_N = 1, \\ \text{sinon} & q(x+x') & \to & q(x) & \quad & \text{sin } [x']_N = 0, \\ \text{sinon} & q(x+x') & \to & q(x') & \quad & \text{sin } [x]_N = 0, \\ \text{sinon} & q(x+x') & \to & q(x) + q(x'), & & \\ \text{sinon} & q(x \ast x') & \to & q(x) & \quad & \text{sin } [x']_N = 1, \\ \text{sinon} & q(x \ast x') & \to & q(x) & \quad & \text{sin } [x]_N = 1, \\ \text{sinon} & q(x \ast x') & \to & q(x) \ast q(x'). & & \end{array} $$

Certaines libertés sont prises ici par rapport à la définition originale. En voici la liste :

- les transitions ne sont plus « atomiques » et il faut les décomposer pour obtenir des règles compatibles avec la définition. Par exemple, la règle $q(x+x') \to q(x)+q(x')$ nécessite l'usage de trois états intermédiaires $q'$, $r$ et $r'$ et l'usage des quatre règles :

$$ \begin{array}{lclcl} q(x) & \to & q'(x) & \quad & \text{sin } x \in ((> 1) + (> 1)) \\ q'(x) & \to & r(x) + r'(x) & & \\ r(x + x') & \to & q(x) & & \\ r'(x + x') & \to & q(x'), & & \end{array} $$

<footnote n="9">9. Il est possible de voir les éléments non définis comme égaux à un élément supplémentaire *Undef* supérieur à tous les autres termes. Dans ce cadre, la suite $\delta_n(q, t)$ est alors croissante sans restriction.</footnote>
- les anticipations sont placées informellement à l'extérieur des règles et la contrainte qu'elles imposent est exprimée sémantiquement. Cela ne pose pas de problème puisque l'on a vu que les ensembles de termes s'évaluant respectivement à 0, à 1 et à $\infty$ sont $\mu$-définissables (voir exemple 3.41),

- les anticipations font références à des sous-termes. Cela ne pose pas de problème d'après les propriétés de clôture des parties $\mu$-définissables (propriété 3.42).

- les anticipations ne sont plus disjointes, mais l'usage de la construction sinon énonce les priorités relatives des transitions.

Le transducteur déterministe ainsi défini transforme tout terme infini en un terme équivalent fini. Ce terme fini est en quelque sorte normalisé puisqu'il ne contient ni somme avec des arguments nuls ni multiplication impliquant des termes s'évaluant en 0 ou en 1.

### 3.4.2 Normalisation

Un problème technique subsiste: il est possible qu'un terme produit par un transducteur déterministe contienne le symbole $\perp$: considérer par exemple la transition $q(f(x, y)) \to q(x)$, qui ne produit jamais de symbole, mais en consomme. Il est préférable d'éviter ce phénomène comme nous le montre le lemme 3.44. Nous verrons aussi comment se débarrasser de cette situation grâce au lemme 3.47.

**Lemme 3.44** Soit $\mathbf{t} = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$ un transducteur déterministe. Considérons la plus grande (au sens de l'inclusion) application $R$ de $Q \times 2^{\mathcal{T}^\omega(\mathcal{F}')}$ dans $2^{\mathcal{T}^\omega(\mathcal{F})}$ telle que pour tout état $q_0$ et tout ensemble $E \subseteq \mathcal{T}^\omega(\mathcal{F}')$,

$$ R(q_0, E) = \left\{ \begin{array}{ll} \bigcap_{i \in [f]} R(q_i, (fi)^{-1}(E)) & \text{si } q_0(x) \to f(q_1(x), \dots, q_{|f|}(x)) \in \delta, \\ \\ \bigcup_{i \in [n]} (L_i \cap R(r_i, E)) & \text{si les } q_0\text{-transitions sont les } q_0(x \in L_i) \to r_i(x) \text{ pour } i \in [n], \\ \\ f(\mathbf{1}, \dots, \mathbf{1}, R(r, E), \mathbf{1}, \dots, \mathbf{1}) & \text{si } q_0(f(x_1, \dots, x_n)) \to r(x_i). \\ \\ \uparrow \\ \text{ième position} \end{array} \right. $$

$$ \text{Alors } R(q_0, E) = \mathbf{t}_{q_0}^{-1}(\{t' \mid \exists t \in E, t' \sqsubseteq t\}). $$

**Preuve.** Découle des définitions. $\square$
**Corollaire 3.45** En particulier, si $\mathbf{t}_{q_0}(\mathbf{1}) \subseteq \mathcal{T}^\omega(\mathcal{F}')$ (c.a.d. ne contient pas le symbole $\perp$) alors pour toute partie $E$ de $\mathcal{T}^\omega(\mathcal{F}')$, on a

$$R(q_0, E) = \mathbf{t}_{q_0}^{-1}(E).$$

**Corollaire 3.46** Pour tout état $q_0 \in Q$, l'ensemble $\mathbf{t}_{q_0}^{-1}(\perp)$ est $\mu$-définissable.

**Preuve.** On peut toujours supposer qu'il existe une constante $a \in \mathcal{F}'$ qui n'est jamais produite par une transition du transducteur déterministe. Dans ce cas $R(q_0, \{a\}) = \mathbf{t}_{q_0}^{-1}(\perp)$. Dans le système d'équations du lemme 3.44, si l'on remplace $E$ par $\{a\}$, alors le cas de la production se réduit à $\emptyset$. Si on se restreint aux équations accessibles à partir de $R(q_0, \{a\})$, elles ne sont plus qu'en nombre fini (une pour chaque état). Ce système se traduit donc directement en une formule du $\mu$-calcul vectoriel $\nu x[q].\{x[q] = \phi[q] \mid q \in Q\}$ avec :

$$ \phi[q] = \left\{ \begin{array}{ll} \emptyset & \text{si } q(x) \to f(q_1(x), \dots, q_{|f|}(x)) \in \delta \\ \bigcup_{i \in [n]} (L_i \cap x[r_i]) & \text{si les } q\text{-transitions sont les} \\ & q(x \in L_i) \to r_i(x) \text{ pour } i \in [n] \\ f(\mathbf{1}, \dots, \mathbf{1}, x_i[r], \mathbf{1}, \dots, \mathbf{1}) & \text{si } q(f(x_1, \dots, x_n)) \to r(x_i) \\ \uparrow & \\ \text{ième position} & \end{array} \right. $$

□

Le lemme suivant permet d'éliminer $\perp$ de l'image d'un transducteur déterministe, et de se ramener de la sorte aux hypothèses du corollaire précédent.

**Lemme 3.47** Soient $\mathbf{t}$ un transducteur déterministe de $\mathcal{T}^\omega(\mathcal{F})$ dans $\mathcal{T}^\omega(\mathcal{F}')$ et $\perp'$ un nouveau symbole constante. Il existe un transducteur déterministe $\mathbf{t}'$ tel que :

- $\mathbf{t}'(\mathbf{1}) \subseteq \mathcal{T}^\omega(\mathcal{F}' \uplus \{\perp'\})$ (c.a.d. ne contient pas le symbole $\perp$, mais le symbole $\perp'$),

- pour tout $t \in \mathcal{T}^\omega(\mathcal{F})$, $\mathbf{t}'(t) = h(\mathbf{t}(t))$ ou $h(t')$ est le terme $t'$ dans lequel tous les symboles $\perp$ sont remplacés par $\perp'$.

**Preuve.** Il suffit d'ajouter un nouvel état $q_\perp$ produisant un symbole $\perp'$, et (en ajoutant des états intermédiaires) de faire précéder chaque transition d'une anticipation vérifiant que le reste du calcul ne va pas produire $\perp$, et le cas échéant effectuant un branchement vers $q_\perp$. Cette anticipation est bien $\mu$-définissable d'après le corollaire 3.46. □
### 3.4.3 Propriétés

**Lemme 3.48** *L'image inverse d'une partie $\mu$-définissable par un transducteur déterministe est effectivement $\mu$-définissable.*

**Preuve.** Considérons un transducteur déterministe $t = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$.

On définit pour tout état $q$, et toute $\mu$-formule $\phi$ sur $\mathcal{F}'$ une $\mu$-formule $I(q, \phi)$ sur l'alphabet $\mathcal{F}$. Cette construction s'effectue par récurrence sur la structure de $\phi$. Les variables libres sont transformées simultanément, les variables libres de $I(q, \phi)$ sont les $\{x[q] \mid x \in FV(\phi), q \in Q\}$.

L'application $I$ est définie comme suit :

1. Si $q_0$ est un état de production : $q_0(x) \to f(q_1(x), \dots, q_{|f|}(x)) \in \delta$, on pose

$$ I(q_0, g(\phi_1, \dots, \phi_{|g|})) = \emptyset \quad (3.3) $$

$$ I(q_0, f(\phi_1, \dots, \phi_{|f|})) = I(q_1, \phi_1) \cap \dots \cap I(q_{|f|}, \phi_{|f|}) \quad (3.4) $$

$$ I(q_0, \phi \cap \psi) = I(q_0, \phi) \cap I(q_0, \psi) \quad (3.5) $$

$$ I(q_0, \phi \cup \psi) = I(q_0, \phi) \cup I(q_0, \psi) \quad (3.6) $$

$$ \text{pour } \theta \in \{\mu, \nu\}, \quad I(q_0, \theta x. \phi) = \theta x[q_0].\{x[q] = I(q, \phi) \mid q \in Q\} \quad (3.7) $$

2. Si $q_0$ est un état de consommation ou d'anticipation, on pose,

$$ I(q_0, \phi) = \nu y[q_0].\{y[q] = F(q, \phi) \mid q \in Q\} \quad (3.8) $$

avec $F(q, \phi)$ défini par :

(a) si $q$ est un état de production, on pose $F(q, \phi) = I(q, \phi)$.

(b) si $q$ est un état de consommation, $q(f(x_1, \dots, x_{|f|})) \to r(x_i) \in \delta$, on pose

$$ F(q, \phi) = \begin{array}{l} f(\mathbf{1}, \dots, \mathbf{1}, \uparrow \quad y[r] , \mathbf{1}, \dots, \mathbf{1}) \\ \text{i-ème position} \end{array} \quad (3.9) $$

(c) $q$ est un état d'anticipation, soient $q(x \in L_i) \to q_i(x)$ pour $i \in [n]$ les $q$-transitions. On pose :

$$ F(q, \phi) = (L_1 \cap y[q_1]) \cup \dots \cup (L_n \cap y[q_n]) \quad (3.10) $$

On montre par récurrence sur la structure de $\phi$ que pour tout état $q_0$ et toute valuation $\gamma$ de $FV(\phi)$ :

$$ \mathbf{t}_{q_0}^{-1}(\phi[\gamma]) = I(q_0, \phi)[\gamma'], $$
avec pour toute variable $x \in FV(\phi)$ et tout état $q \in Q$, $\gamma'(x[q]) = \mathbf{t}_q^{-1}(\gamma(x))$.

1. Si $q_0$ est un état de production : $q_0(x) \to f(q_1(x), \dots, q_{|f|}(x)) \in \delta$, on a :

$$
\begin{align*}
\text{Pour } g \neq f, \mathbf{t}_{q_0}^{-1}(g(\phi_1, \dots, \phi_{|g|})[\gamma]) &= \emptyset && \text{def.} \\
&= I(q_0, g(\phi_1, \dots, \phi_{|g|})[\gamma']) && (3.3) \\
\mathbf{t}_{q_0}^{-1}(f(\phi_1, \dots, \phi_{|f|})[\gamma]) &= \mathbf{t}_{q_0}^{-1}(\phi_1[\gamma]) \cap \dots \cap \mathbf{t}_{q_0}^{-1}(\phi_{|f|}[\gamma]) && \text{def.} \\
&= I(q_0, \phi_1)[\gamma'] \cap \dots \cap I(q_0, \phi_{|f|})[\gamma'] && \text{hyp. rec.} \\
&= I(q_0, f(\phi_1, \dots, \phi_{|f|})[\gamma']) && (3.4) \\
\mathbf{t}_{q_0}^{-1}(\phi \cap \psi) &= \mathbf{t}_{q_0}^{-1}(\phi[\gamma]) \cap \mathbf{t}_{q_0}^{-1}(\psi[\gamma]) \\
&= (q_0, \phi)[\gamma'] \cap I(q_0, \psi)[\gamma'] && \text{hyp. rec.} \\
&= I(q_0, \phi \cap \psi)[\gamma'] && (3.5) \\
\mathbf{t}_{q_0}^{-1}(\phi \cup \psi) &= \mathbf{t}_{q_0}^{-1}(\phi[\gamma]) \cup \mathbf{t}_{q_0}^{-1}(\psi[\gamma]) \\
&= (q_0, \phi)[\gamma'] \cup I(q_0, \psi)[\gamma'] && \text{hyp. rec.} \\
&= I(q_0, \phi \cup \psi)[\gamma'] && (3.6)
\end{align*}
$$

Cas de $\mu x.\phi$. Soient $r_1, \dots, r_k$ les états du transducteur déterministe. Il s'agit d'une application directe du lemme de transfert 3.30 avec

$$
\begin{align*}
g(E) &= \phi[\gamma, x \to E] \\
f(E_{r_1}, \dots, E_{r_k}) &= (I(r_1, \phi)[\gamma'], \dots, I(r_k, \phi)[\gamma']) \\
&\quad \text{avec } \begin{cases} \gamma'(z[q]) = \mathbf{t}_q^{-1}(\gamma(z)) & \text{pour } z \in FV(\phi) \\ \gamma(x[q]) = E_q \end{cases} \\
\rho(E) &= (\mathbf{t}_{r_1}^{-1}(E), \dots, \mathbf{t}_{r_k}^{-1}(E))
\end{align*}
$$

On a bien $\rho \circ g = f \circ \rho$ d'après l'hypothèse de récurrence. L'application $\rho$ est additive d'après la propriété 3.28. Le lemme de transfert 3.30 conclut.

Cas de $\nu x.\phi$. comme pour $\mu$ (remplacer additivement par multiplicative).

2. Si $q_0$ est un état de consommation ou d'anticipation, on utilise le corol-
laire 3.45. Comme il s'agit d'un calcul de point fixe, on peut substituer
certaines expressions par leur solution, ainsi, $R$ est la plus grande solution
de,

$$
R(q, E) = \begin{cases}
\mathbf{t}_q^{-1}(E) & \text{si } q \text{ est un état de production,} \\
\bigcup_{i \in [n]} (L_i \cap R(r_i, E)) & \text{si les } q\text{-transitions sont les} \\
& \qquad \qquad \qquad q(x \in L_i) \to r_i(x) \text{ pour } i \in [n], \\
& \\
f(\mathbf{1}, \dots, \mathbf{1}, R(r, E), \mathbf{1}, \dots, \mathbf{1}) & \text{si } q(f(x_1, \dots, x_n)) \to r(x_i). \\
\uparrow & \\
i\text{ème position} &
\end{cases}
$$