- ou bien ce chemin emprunte au moins l'un des arcs ajoutés par $\mathbf{arc}[c_1, a, c_2]$. Dans ce cas, ce chemin s'écrit comme la concaténation de trois chemins de la forme suivante :

1. un chemin entre $v$ et un sommet de couleur $c_1$ n'empruntant aucun des arcs ajoutés par $\mathbf{arc}[c_1, a, c_2]$ ; ce chemin est donc déja présent dans $\mathcal{G}$,

2. un chemin entre un sommet de couleur $c_1$ et un sommet de couleur $c_2$,

3. un chemin entre un sommet de couleur $c_2$ et $v'$, n'empruntant aucun des arcs ajoutés par $\mathbf{arc}[c_1, a, c_2]$ ; ce chemin est donc déja présent dans $\mathcal{G}$.

Il suffit pour tester l'existence d'un tel chemin de vérifier la présence du premier et du troisième. Le second est en fait toujours présent d'après la sémantique de $\mathbf{arc}[c_1, a, c_2]$.

Cette décomposition explique les deux cas utilisés pour chacun des symboles de chemin. $\square$

**Lemme 6.14** *Pour tous graphes colorés $\mathcal{G}$ et $\mathcal{H}$, $*(\mathcal{G} \oplus \mathcal{H}) = *(\mathcal{G}) \oplus *(\mathcal{H})$.*

**Preuve.** Évident. $\square$

Le lemme ci-desous traite du cas du produit.

**Lemme 6.15** *Il existe trois interprétations booléennes positives $\mathcal{I}_{\eta,1}$, $\mathcal{I}_{\eta,2}$ et $\mathcal{I}$ telles que pour tous graphes colorés $\mathcal{G}_1$ et $\mathcal{G}_2$, on a*

$$*(\mathcal{G}_2 \sqcap \eta \mathcal{G}_2) = \mathcal{I}_{\eta}(\mathcal{I}_{\eta,1}(*(\mathcal{G}_1)) \otimes \mathcal{I}_{\eta,2}(*(\mathcal{G}_2))).$$

**Construction.** On utilise l'équivalence avec le produit généralisé (propriété 2.22).

$$ \mathcal{I}_{\eta} = \left| \begin{array}{ll} c(x) & : \quad c_1^1(x) \wedge c_2^2(x) \\ & \qquad \text{pour } c = \eta(c_1, c_2) \\ x \xrightarrow{a} y & : \quad x \xrightarrow{a} y \wedge x \sim^2 y \\ x \xrightarrow{a} y & : \quad x \sim^1 y \wedge x \xrightarrow{a} y \\ < B^* > (x, y) & : \quad < B^* >^1 (x, y) \wedge < B^* >^2 (x, y) \\ < B^*c > (x) & : \quad < B^*c_1 >^1 (x) \wedge < B^*c_2 >^2 (x) \\ & \qquad \text{pour } c = \eta(c_1, c_2) \\ < cB^* > (x) & : \quad < c_1 B^* >^1 (x, y) \wedge < c_2 B^* >^2 (x, y) \\ & \qquad \text{pour } c = \eta(c_1, c_2) \\ < cB^*c' > (\text{ }) & : \quad < c_1 B^*c_2 >^1 (\text{ }) \wedge < c'_1 B^*c'_2 >^2 (\text{ }) \\ & \qquad \text{pour } c = \eta(c_1, c_2) \wedge c' = \eta(c'_1, c'_2) \end{array} \right| $$

$$ \text{On a alors } \mathcal{I}_{\eta}(*(\mathcal{G}_1) \otimes_g *(\mathcal{G}_2)) = *(\mathcal{G}_1 \sqcap \eta \mathcal{G}_2). \quad \square $$
## Le résultat

**Lemme 6.16** Pour tout ensemble d'étiquettes A et tout ensemble de couleurs C, il existe un transducteur déterministe t des VRA[C, A]-termes dans les VRS'-termes tel que pour tout VRA[C, A]-terme t,

$$[t(t)] = *([t]).$$

**Corollaire 6.17 (Colcombet [Col02a])** Soit $\phi$ une formule en logique du premier ordre avec accessibilité étendue par les modalités de comptage $\exists^\omega$ et $\forall^\omega$, l'ensemble des modèles de $\phi$ est VRA-reconnaissable.

## 6.5 Largeur arborescente

Dans ce paragraphe, nous énonçons un résultat similaire à celui de Barthelmann (théorème 25) montrant que les graphes préfixes reconnaissables de largeur arborescente bornée sont les graphes HR-équationnels. Un premier résultat dans cette direction concernant la récriture suffixe de termes restreinte par accessibilité a été établi par Löding.

**Théorème 33 (Löding [LÖ2a])** Les graphes de récriture suffixe avec restriction par accessibilité et de largeur arborescente bornée sont des graphes préfixes.

Löding a ultérieurement étendu ce travail aux systèmes de récriture suffixe reconnaissables [LÖ2b].

Nous montrons ici un résultat similaire, pour les graphes solutions de VRA-systèmes d'équations.

**Théorème 34 (Colcombet [Col02a])** Les graphes solutions de VRA-systèmes finis d'équations de largeur arborescente bornée sont les graphes HR-équationnels.

Pour montrer ce résultat, il s'agit d'abord d'éliminer les opérateurs produit du système d'équations. Une première étape de normalisation est nécessaire (paragraphe 6.5.1). On obtient alors un système VR-équationnel de largeur arborescente bornée. Le résultat de Barthelmann permet alors de transformer ce système d'équations en un système HR-équationnel.

### 6.5.1 Croissance pour la largeur arborescente

On cherche dans ce paragraphe à assurer que dans tout «calcul» effectué par le système d'équations, la largeur arborescente du résultat est supérieure à la largeur arborescente des arguments. Ce raisonnement est à la base de la preuve qui suit.

Pour cela, on introduit le préordre $\leq$ sur les graphes colorés défini comme suit. Pour deux graphes colorés $G$ et $H$, $G \leq H$ si $G$ est un sous-graphe de $H$
à recoloriage près. Le lemme 6.20 permet d'assurer que, dans un VRA-système d'équations, le résultat de tout opérateur est supérieur à ses arguments pour l'ordre $\le$.

Le lemme 6.18 nous enseigne comment se comportent les opérateurs VRA vis à vis de la relation $\le$.

**Lemme 6.18** Pour tous graphes colorés $\mathcal{G}$ et $\mathcal{H}$, toute application $\alpha$ de $C$ dans $C$, toutes couleurs $c$ et $c'$, toute étiquette $a$ et toute application $\eta$ de $C^2$ dans $C$, on $a$,

$$ 
\begin{array}{lll}
\mathcal{G} \le \mathbf{recol}[\alpha](\mathcal{G}), & \mathcal{G} \le \mathbf{arc}[c, a, c'](\mathcal{G}), & \\
\mathcal{G} \le \mathcal{G} \oplus \mathcal{H}, & \mathcal{H} \le \mathcal{G} \oplus \mathcal{H}, & \\
\text{si } \mathcal{H} \ne \emptyset, \quad \mathcal{G} \le \mathcal{G} \sqcap_{\eta} \mathcal{H}, & \text{si } \mathcal{G} \ne \emptyset, \quad \mathcal{H} \le \mathcal{G} \sqcap_{\eta} \mathcal{H}. &
\end{array}
$$

**Preuve.** Évident au cas par cas.

□

Il faut donc éliminer le cas du graphe vide $\emptyset$ si l'on veut garantir que le résultat de l'application d'un opérateur de VRA produit un résulat supérieur pour $\le$ à ses arguments. Pour cela, on dit qu'un VRA-terme $t$ est normalisé si pour tout sous-terme $t'$ de $t$, $[[t']] \ne \emptyset$. On obtient alors directement le lemme suivant.

**Lemme 6.19** Pour tout VRA-terme normalisé $t$ et tout sous-terme $t'$ de $t$,

$$ [[t')] \le [[t]]. $$

Il s'agit donc de normaliser les termes.

**Lemme 6.20** Soit $C$ un ensemble fini de couleurs et $A$ un ensemble fini d'éti-quettes. Il existe un transducteur déterministe des VRA[$C, A$]-termes dans les VRA-termes tel que pour tout VRA[$C, A$]-terme $t$, si $[[t]] \ne \emptyset$ alors $t(t)$ est dé-fini, normalisé et satisfait $[[t]] \approx [[t(t)]]$.

**Construction.** L'identité sur $C$ est notée $\text{id}$. On utilise le transducteur déterministe à un seul état suivant :

$$ 
\begin{array}{lll}
q(x \sqcap_{\eta} y) \rightarrow q(x) \sqcap_{\eta} q(y), & & \\
q(x \oplus y) \rightarrow \mathbf{recol}[\text{id}](q(x)) & \text{si } [[y]] = \emptyset, & \\
q(x \oplus y) \rightarrow \mathbf{recol}[\text{id}](q(y)) & \text{si } [[x]] = \emptyset, & \\
q(\mathbf{arc}[c, a, c'](x)) \rightarrow \mathbf{arc}[c, a, c'](q(x)), & & \\
q(\mathbf{recol}[\alpha](x)) \rightarrow \mathbf{recol}[\alpha](q(x)), & & \\
q(\text{sommet}[c]) \rightarrow \text{sommet}[c]. & &
\end{array}
$$
Les anticipations sont validées par le corollaire 6.17 car être vide s'exprime en logique du premier ordre. L'utilisation de recol[id] permet de garantir l'hypothèse sur les règles de production du lemme 3.59. □

Enfin, le lemme 6.21 montre comment l'ordre $\le$ est relié à la largeur arborescente.

**Lemme 6.21** Soient deux graphes colorés $\mathcal{G}$ et $\mathcal{H}$,

$$ \text{si } \mathcal{G} \leq \mathcal{H} \quad \text{alors} \quad LA(\mathcal{G}) \leq LA(\mathcal{H}). $$

**Preuve.** Évident<fnref n="1" />.

□

**Corollaire 6.22** Si $[[t]]$ est normalisé et de largeur arborescente bornée, alors pour tout sous-terme $t'$ de $t$, $[[t']]$ est de largeur arborescente bornée.

## 6.5.2 Élimination des produits

Il s'agit maintenant de faire disparaître les opérateurs de produit asynchrone d'un terme dont la valeur est de largeur arborescente bornée. Dans la suite de ce paragraphe, on omet le paramètre $\eta$ des opérateurs $\square$ quand il n'intervient pas dans le raisonnement.

L'élimination se fait en deux étapes. Tout d'abord, il s'agit d'éliminer les opérateurs de produit apparaissant une infinité de fois dans une même branche, c'est à dire les termes de la forme $t = t' \square t''$, où $t$ est un sous-terme de $t'$ ou de $t''$. La seconde étape élimine les opérateurs de produit restants.

### Étape 1 : élimination des produits récursifs

Considérons un terme normalisé de la forme $t = t' \square t''$ où $t$ est un sous-terme de $t'$ (le cas de $t''$ étant naturellement symétrique). Le terme $t'$ est normalisé et $t$ est un sous-terme de $t'$, donc $[[t]] \le [[t']]$ (lemme 6.19). D'où $[[t]] \square_{\eta} [[t']] \le [[t]]$. On en déduit que pour tout $n \in \mathbb{N}_+$

$$ \square^n([t'']) \le [[t]], \quad \text{avec } \square^n(\mathcal{G}) = \overbrace{\mathcal{G} \square \dots \square \mathcal{G}}^{n \text{ fois}}. $$

Comme $t$ est de largeur arborescente bornée, il existe un $k \in \mathbb{N}$ tel que pour tout $n \in \mathbb{N}_+$, $LA(\square^n([t'])) \le k$. Le lemme 6.23 précise alors la structure de $[[t]]$.

<footnote n="1">1. En fait, $\le$ est un cas particulier de la relation « est un mineur de » qui satisfait la même propriété.</footnote>
**Lemme 6.23** Soit $\mathcal{G}$ un graphe coloré et $k$ un entier tel que pour tout $n$

$$LA(\square^n(\mathcal{G})) \leq k,$$

alors tous les arcs de $\mathcal{G}$ sont des boucles.

**Preuve.** Supposons que $\mathcal{G}$ possède un arc qui ne soit pas une boucle. Alors $\square^n(\mathcal{G})$ contient un hypercube de dimension $n$. Le nombre d'arcs dans un hypercube de dimension $n$ est $n2^{n-1}$, le nombre de sommets est $2^n$. Donc le ratio nombre d'arcs/nombre de sommets de l'hypercube de dimension $n$ vaut $n/2$ et n'est donc pas borné. Ainsi, le graphe union de tous les hypercubes n'est pas uniformément creux et donc pas de largeur arborescente bornée. Contradiction. $\square$

Peu de graphes satisfont la contrainte de ne posséder que des boucles. En fait, ces graphes sont entièrement décrits par le nombre (éventuellement infini) de sommets de chaque type qu'ils contiennent, le type étant formé de la couleur et de l'ensemble des étiquettes sur une boucle de ce sommet. Soit $\mathcal{G}_0$ un graphe satisfaisant cette contrainte. Il s'agit de remplacer une équation de la forme $X = Y \square \mathcal{G}_0$ par une équation équivalente ne faisant pas intervenir l'opérateur $\square$. L'opérateur **boucle** permet cette opération. Étant donné un ensemble d'étiquettes $E \subseteq A$, l'opérateur **boucle**[$E$] ajoute à tous les sommets d'un graphe et toute étiquette $a \in E$ une boucle étiquetée par $a$ sur ce sommet. Les opérateurs VRA augmentés de cet opérateur sont notés (VRA + **boucle**).

**Lemme 6.24** Soit $\mathcal{G}$ un graphe coloré ne contenant que des boucles et $\eta$ une application de $C^2$ dans $C$ alors il existe une application (VRA+boucle)-définissable $f_G$ (resp. $r_G$) telle que pour tout graphe coloré $\mathcal{H}$, on a continuement :

$$\mathcal{G} \square_{\eta} \mathcal{H} \approx f_G(\mathcal{H}) \qquad (\text{resp. } \mathcal{H} \square_{\eta} \mathcal{G} \approx g_G(\mathcal{H})).$$

**Preuve.** (a) Supposons que $\mathcal{G}$ ne soit formé que d'un sommet de couleur $c_0$. Soit $E$ l'ensemble des étiquettes apparaissant sur ce sommet. On pose $f_G = \text{boucle}[E] \circ \text{recol}[\alpha]$ avec pour tout $c \in C$, $\alpha(c) = \eta(c_0, c)$. On a alors pour tout graphe coloré $\mathcal{H}$, $\mathcal{G}_0 \square_{\eta} \mathcal{H} \approx f_G(\mathcal{H})$.

(b) Si maintenant $\mathcal{G}$ est formé de l'union disjointe d'une infinité de fois un graphe $\mathcal{G}_0$ ne contenant qu'un seul sommet, alors on définit $f_G$ comme plus petite solution de $f_G(\mathcal{H}) = f_{\mathcal{G}_0}(\mathcal{H}) \oplus f_G(\mathcal{H})$. On a alors pour tout graphe coloré $\mathcal{H}$ $\mathcal{G}_0 \square_{\eta} \mathcal{H} \approx f_G(\mathcal{H})$.

Tout graphe ne contenant que des boucles s'écrit comme une union disjointe finie de graphes des types (a) et (b). On en déduit $f_G$ convenable comme une union finie des applications précédemment définies.
L'application $g_G$ s'obtient similairement. □

**Lemme 6.25** Pour tout ensemble de couleurs C, tout ensemble d'étiquettes A et tout VRA[$C, A$]-terme régulier $t$ tel que $[[t]]$ est de largeur arborescente bornée, il existe un (VRA + boucle)[$C, A$]-terme régulier $t'$ tel que

$$- [[t]] \approx [[t']],$$

- aucune branche de $t'$ ne contient une infinité d'opérateurs □,

- $t$ est normalisé.

**Preuve.** On suppose $t$ normalisé.

Soient $G_1, \dots, G_n$ les graphes ne contenant que des boucles apparaissant valeur d'un sous-terme de $t$. Ceux-ci sont en nombre fini car $t$ est régulier. Bien entendu, et pour tout $i \in [n]$, les graphes isomorphes à $G_i$ sont VRA[$C, A$]-reconnaissables (appliquer par exemple le corollaire 6.17, les graphes $G_i$ étant axiomatisables en logique du premier ordre augmentée par les modalités de comptage).

On construit alors le transducteur déterministe $t$ à un seul état $q$ suivant.

$$q(x \sqcap \eta y) \rightarrow f_{G_i}(q(y)) \qquad \text{si } [[x]] \approx G_i$$

$$q(x \sqcap \eta y) \rightarrow g_{G_i}(q(y)) \qquad \text{si } [[y]] \approx G_i$$

$$q(x \sqcap \eta y) \rightarrow q(x) \sqcap \eta q(y) \qquad \text{sinon}$$

$$q(x \oplus y) \rightarrow q(x) \oplus q(y)$$

$$\text{recol}[\alpha](q(x)) \rightarrow \text{recol}[\alpha](q(x))$$

$$q(\text{arc}[c, a, c')(x)) \rightarrow \text{arc}[c, a, c')(q(x))$$

$$q(\text{sommet}[c]) \rightarrow \text{sommet}[c]$$

Le fait que ce transducteur préserve la valeur ne pose pas de problème (on applique pour cela le lemme 6.24 pour les deux premières règles). Il est aussi évident que $t$ préserve la normalisation.

Soit $t' = t(t)$. Supposons que $t$ contienne une branche contenant une infinité d'opérateurs □. Comme $[[t]]$ est de largeur arborescente bornée et d'après le lemme 6.23, l'un de ses paramètres est un graphe ne possédant que des boucles. Or ce graphe était déja présent dans $t$, donc l'une des deux premières règles du transducteur aurait dû être appliquée. Contradiction. □

Après application du lemme 6.25, il ne nous reste plus qu'à éliminer les opérateurs de boucle.

**Lemme 6.26** Pour tout ensemble de couleurs C et tout ensemble d'étiquettes A il existe un transducteur déterministe $t$ des (VRA + boucle)[$C, A$]-termes dans les
VRA-termes tel que pour tout (VRA + **boucle**) [C, A]-terme t,

$$[t] = [[t(t)]] .$$

De plus, si t ne contient pas de branche contenant une infinité d'opérateurs □, alors il en est de même pour t(t). Enfin, si t est normalisé, t(t) est aussi normalisé.

**Construction.** On considère le transducteur déterministe possédant < E > pour tout E ⊆ A comme états. Ce transducteur collecte les opérateurs **boucle** et les propage jusqu'aux feuilles.

$$ 
\begin{align*}
\langle E \rangle (x \sqcap y) &\rightarrow \langle E \rangle (x) \sqcap \langle \emptyset \rangle (y) \\
\langle E \rangle (x \oplus y) &\rightarrow \langle E \rangle (x) \oplus \langle E \rangle (y) \\
\langle E \rangle (\mathbf{boucle}[F](x)) &\rightarrow \mathbf{recol}[id](\langle E \cup F \rangle (x)) \\
\langle E \rangle (\mathbf{recol}[\alpha](x)) &\rightarrow \mathbf{recol}[\alpha](\langle E \rangle (x)) \\
\langle E \rangle (\mathbf{arc}[c, a, c')(x)) &\rightarrow \mathbf{arc}[c, a, c'](\langle E \rangle (x)) \\
\langle E \rangle (\mathbf{sommet}[c]) &\rightarrow \mathbf{arc}[\{c\} \times D \times \{c'\}](\mathbf{sommet}[c])
\end{align*}
$$

Soit $\langle \emptyset \rangle$ l'état initial. On montre sans difficulté que ce transducteur satisfait les conclusions du lemme. □

À ce stade de la transformation, on a obtenu à partir d'un VRA-terme régulier dont la valeur est de largeur arborescente bornée un VRA-terme régulier normalisé dont aucune branche ne contient une infinité d'opérateurs □. L'étape suivante permet d'éliminer les opérateurs □ restants.

## Étape 2 : élimination des produits restants

**Lemme 6.27** Pour deux graphes connexes $\mathcal{G}$ et $\mathcal{H}$, on a,

$$LA(\mathcal{G} \sqcap \mathcal{H}) \geq \min(|V_{\mathcal{G}}|, |V_{\mathcal{H}}|) - 1.$$

**Preuve.** Chaque sommet du graphe est un couple $(v, v') \in V_{\mathcal{G}} \times V_{\mathcal{H}}$. Appelons ligne (resp. colonne) tout ensemble maximal de sommets qui possèdent la même première (resp. seconde) projection. Soit $N$ tel que $|V_{\mathcal{G}}| > N$ et $|V_{\mathcal{H}}| > N$. Considérons un jeu du voleur et des policiers à $N$ policiers. À tout instant du jeu, une ligne et une colonne au moins ne contiennent aucun policier. C'est à l'intersection de cette ligne et de cette colonne que se place le voleur. On vérifie aisément qu'à chaque étape du jeu, le voleur peut se déplacer jusqu'à ce sommet sans rencontrer
de policier. Il gagne.

☐

**Corollaire 6.28** Si le produit asynchrone de deux graphes est de largeur arborescente bornée alors l'un au moins est une union disjointe de composantes connexes de tailles bornées.

**Lemme 6.29** Les graphes préfixes reconnaissables sont clos par produit asynchrone avec les graphes possédant des composantes connexes de taille bornée.

**Preuve.** Standard.

☐

**Lemme 6.30** Pour tout VRA-terme régulier normalisé $t$ dont aucune branche ne contient une infinité d'opérateurs □ et tel que $[t]$ est de largeur arborescente bornée, il existe un VR-terme régulier $t'$ tel que $[t'] \approx [t']$.

**Preuve.** Pour $t$ un terme, notons $S(t)$ l'ensemble des sous-termes de $t$ possédant un opérateur □ à la racine.

On procède alors par récurrence sur $|S(t)|$.

Si $|S(t)| = 0$ alors $t$ est un VR-terme régulier.

Si $|S(t)| > 0$ alors soit $t'$ un sous-terme de $t$ de la forme $t' = t_1' \Box \eta t_2'$. On a pour $i \in [2]$, $S(t_i') \subseteq S(t)$ car $t_i'$ est un sous-terme de $t$. On a de plus $t' \notin S(t_i')$ car $t' \notin S(t')$ par hypothèse sur les branches infinies.

Par hypothèse de récurrence, $[t_1']$ et $[t_2']$ sont préfixes reconnaissables. En appliquant le corollaire 6.28 et le lemme 6.29, on en déduit que $[t']$ est préfixe reconnaissable. Il existe donc un VR-terme $t''$ tel que $[t'] \approx [t'']$. On remplace alors dans $t$ toutes les occurences du terme $t'$ par $t''$, obtenant ainsi le terme $t'''$. On a alors $[t'''] \approx [t]$. De plus, $S(t''') \subseteq S(t) - \{t'\}$, donc, par hypothèse de récurrence, $[t''']$ est préfixe reconnaissable. ☐

☐

## Conclusions

L'application successive des étapes 1 et 2 nous amène alors au lemme ci-dessous.

**Lemme 6.31** Les graphes solutions des VRA-systèmes d'équations finis et de largeur arborscente bornée sont VR-équationnels.

Il ne reste plus alors qu'à appliquer le résultat de Barthelmann (théorème 25) pour conclure que les graphes solutions de VRA-systèmes finis d'équations de largeur arborscente bornée sont HR-équationnels. Réciproquement, les graphes
HR-équationnels sont de largeur arborescente bornée (Courcelle, propriété 4.12). Ceci achève la preuve du théorème 34.

Remarquons que cette preuve est fondamentalement différente de celle de Barthelmann. En effet, l'hypothèse de finitude du système d'équations est utilisée à plusieurs reprises, et donc cette transformation ne peut pas être effectuée (a priori) par un transducteur déterministe. De l'avis de l'auteur, il est fort improbable qu'une telle généralisation soit vraie. Néanmoins, il est possible que la preuve présentée ici puisse être généralisée aux VRA-systèmes d'équations appartenant à la hiérarchie de Caucal: le HR-système d'équations résultant étant éventuellement à un autre niveau de cette hiérarchie.

### 6.5.3 Décidabilité et effectivité

Il s'agit maintenant de montrer que la transformation présentée précédemment permet à la fois de décider si la solution d'un VRA-système fini d'équations est de largeur arborescente bornée, et, le cas échéant, de construire effectivement un HR-système d'équations fini équivalent. Pour établir cela, il s'agit d'observer plus attentivement la preuve précédente, étape par étape.

**Étape 1 :** pour que l'étape 1 puisse être effectuée, il suffit de garantir qu'aucune branche ne contient une infinité de produits avec des graphes possédant des arcs qui ne sont pas des boucles. Les graphes ne possédant que des boucles sont VRA-reconnaissables (car cette propriété est exprimable par une formule au premier ordre). L'existence d'une branche contenant une infinité de produits avec des graphes possédant un arc qui n'est pas une boucle est alors reconnaissable. Pour pouvoir effectuer la transformation du lemme 6.25, il reste à montrer que l'on peut savoir pour tout ensemble d'étiquettes $E \subseteq A$ le nombre de sommets d'un graphe possédant exactement $E$ comme étiquettes de ses boucles. Pour cela, on commence par décider pour un ensemble $E$ s'il concerne une infinité de sommets, ce qui est décidable d'après le corollaire 6.17. Sinon, on compte ces sommets. Le processus se termine car les sommets sont en nombre fini.

**Étape 2 :** pour assurer la validité de l'étape 2, il suffit de pouvoir décider si un graphe préfixe reconnaissable a ses composantes connexes de taille bornée. On sait [Cau96] que les composantes connexes d'un graphe préfixe reconnaissable sont en nombre fini à isomorphisme près. Il suffit donc de décider si les composantes du graphe sont finies. C'est une propriété décidable. Pour reconstruire le graphe correspondant, on utilise un argument similaire au cas précédent.

Enfin, Barthelmann [Bar98] nous enseigne que le problème de savoir si un graphe VR-équationnel est de largeur arborescente bornée est décidable, et la transformation en un HR-système fini d'équations est effective.

Il est alors possible de conclure.

**Propriété 6.32** Le problème de savoir si la solution d'un VRA-système d'équation
tions fini est de largeur arborescente bornée est décidable, et, si c'est le cas, il est effectivement possible de produire un HR-système fini d'équations de solution isomorphe.

Notons que ce résultat n’est possible que grâce à un renforcement des hypothèses par rapport au résultat de Barthelmann (théorème 25). En effet, borner les sous-graphes bipartis complets ou restreindre aux graphes uniformément creux n’est ici pas suffisant (considérer la grille infinie par exemple).

Il est aussi intéressant de comparer ce résultat de décidabilité avec le cas des graphes de récriture suffixe de termes restreints par accessibilité : « décider si un graphe de récriture suffixe avec restriction par accessibilité est de largeur arborescente bornée est une question ouverte (cf [LÖ2b]). » Ce problème de décidabilité s’avère beaucoup plus délicat que celui qui vient d’être présenté.

## 6.6 Largeur de clique

Il s'agit dans ce pragraphe d'étudier une extension possible du théorème 34 : les graphes solutions de VRA-systèmes finis d'équations de «largeur de clique bornée» sont-ils solution de VR-systèmes finis d'équations ? Nous donnons à cette question une réponse négative, et pour cela nous construisons un contre-exemple.

Nous présentons d'abord la problématique et les travaux connexes (paragraphe 6.6.1). Le paragraphe 6.6.2 présente comment construire un arbre possédant une théorie monadique indécidable servant ultérieurement. Le paragraphe 6.6.3 présente un opérateur de retrait et montre comment il est relié aux opérateurs VRA. La construction proprement dite est alors abordée au paragraphe 6.6.4.

### 6.6.1 Contexte

La largeur arborescente correspond aux solutions des HR-systèmes d'équations : un graphe est de largeur arborescente bornée si et seulement s'il est valeur d'un HR[$C, A$]-terme où $C$ est un ensemble fini de couleurs.

Ainsi, le théorème de Barthelmann 34 peut-il s'énoncer : «si un graphe est à la fois valeur d'un VRA-terme régulier et valeur d'un HR-terme, alors il est valeur d'un HR-terme régulier».

À la lumière de cette équivalence, il est naturel de considérer une mesure des graphes correspondant aux opérateurs VR. Courcelle la nomme largeur de clique [Cou00] (Wanke et Blumensath définissent des mesures comparables). On dit qu'un graphe est de largeur de clique bornée si il existe un VR-terme dont il est solution. Une autre caractérisation des graphes de largeur de clique bornée nous intéresse.

**Propriété 6.33** *Un graphe est largeur de clique bornée si et seulement si il*
s'obtient par interprétation monadique d'un arbre.

Ce résultat classique suit des résultats du chapitre 4.

La question naturelle est alors la suivante : les graphes valeur des VRA-termes réguliers et de largeur de clique bornée sont-ils les graphes VR-équationnels ?

Cette question est ouverte dans la thèse de Löding [LÖ2b]. Löding a montré que les graphes de récriture suffixe restreint par accessibilité de largeur de clique bornée étaient HR-équationnels [LÖ2a]. Cette preuve consiste juste à remarquer que dans ce cas, les graphes ayant des sous-graphes bipartis complets bornés, la largeur arborescente bornée et la largeur de clique bornée sont deux notions équivalentes. La véritable question se pose en fait quand les graphes peuvent être de degré infini et contenir «de grands» graphes bipartis complets.

Nous montrons ici que cette conjecture est fausse. Ce résultat est issu d'une collaboration entre Löding et l'auteur.

Le contre-exemple que nous allons construire (cf. théorème 35) ne possède pas une théorie monadique décidable.

## 6.6.2 Un arbre de théorie monadique indécidable

Dans ce paragraphe, nous expliquons brièvement comment construire un arbre dont la théorie monadique est indécidable: le dépliage de la grille infinie avec retour.

<figure><img src="image_39.png" /><figcaption>FIG. 6.4 – Grille infinie avec retour et tests à zéro.</figcaption></figure>

Pour construire un arbre dont la théorie monadique est indécidable, on peut par exemple chercher à réduire la décidabilité de la logique monadique à un problème d'arrêt de machine de Minsky [Min67]. Une machine de Minsky est une machine à états finis disposant de deux compteurs (à valeur dans les entiers naturels), et pouvant les incrémenter, les décrémenter et tester leur éventuelle
égalité à 0. L'arrêt d'une telle machine à partir d'une configuration donnée est un problème indécidable.

Le domaine de calcul d'une telle machine se représente comme une grille infinie avec retour et test à zéro. La figure 6.4 présente une telle grille $K$. Les étiquettes $a, \bar{a}$ permettent d'incrémenter et de décrémenter le premier compteur, l'étiquette $a_0$ de tester son égalité à 0. Les étiquettes $b, \bar{b}$ et $b_0$ jouent le même rôle pour le second compteur. Le problème de l'arrêt d'une machine de Minsky se ramène directement au problème suivant : étant donné un langage rationnel $L$ sur l'alphabet $\{a, \bar{a}, a_0, b, \bar{b}, b_0\}$, existe-t-il un chemin dans $K$ d'origine (0,0) étiqueté par un mot de $L$ ?

Ce problème ne change en fait pas quand on déplie $K$ depuis le sommet (0,0). L'accessibilité rationnelle étant exprimable en logique monadique, on en déduit que la théorie monadique du dépliage depuis (0,0) de $K$ est indécidable.

En fait, il n'est pas nécessaire pour obtenir ce résultat de disposer des arcs étiquetés par $a_0$ et $b_0$. En effet, les sommets de $\text{Depliage}(K)$ correspondant à une valeur du premier (resp. second) compteur égale à zéro sont exactement ceux qui ne sont origine d'aucun arc étiqueté par $\bar{a}$ (resp. par $\bar{b}$). Ceci est exprimable en logique monadique. Ainsi, le dépliage de la grille infinie avec retour sans test à zéro a une théorie monadique indécidable.

### 6.6.3 Opérateur de retrait

Nous voyons dans ce paragraphe, vis à vis des propriétés qui nous intéressent (c'est-à-dire la décidabilité de la théorie monadique et la largeur de clique), comment ajouter des arcs «équivaut» à en enlever (corollaire 6.35).

On introduit pour cela un nouvel opérateur $\text{retrait}[c_1, a, c_2]$ où $c_1$ et $c_2$ sont des couleurs et $a$ est une étiquette. Cet opérateur appliqué à un graphe coloré retire tous les arcs étiquetés par la lettre $a$ reliant un sommet de couleur $c_1$ à un sommet de couleur $c_2$. Formellement, on pose

$$ \text{retrait}[c_1, a, c_2] = \left| \begin{array}{ll} x \xrightarrow{a} y & : \quad x \xrightarrow{a} y \wedge \left( \bigvee_{c \neq c_1} c(x) \vee \bigvee_{c \neq c_2} c(y) \right) \\ x \xrightarrow{b} y & : \quad x \xrightarrow{b} y \\ c(x) & : \quad c(x) \end{array} \right|_{b \neq a} $$

Comme pour l'opérateur $\text{arc}$ et pour $D \subseteq C \times A \times C$, $\text{retrait}[D]$ est un raccourci pour $\text{retrait}[c_1, a_1, c'_1] \circ \dots \circ \text{retrait}[c_n, a_n, c'_n]$ où $D = \{(c_1, a_1, c'_1), \dots, (c_n, a_n, c'_n)\}$.

**Propriété 6.34** Pour $D \subseteq C \times A \times C$, on a

$$ - \text{retrait}[D] = \text{retrait}[D] \circ \text{arc}[D] \text{ et} $$

$$ - \text{arc}[D] = \text{arc}[D] \circ \text{retrait}[D] . $$
**Preuve.** Évident.

□

**Corollaire 6.35** Pour tout $D \subseteq C \times A \times C$ et tout graphe coloré $\mathcal{G}$,

- retrait[$D$]($\mathcal{G}$) est de largeur de clique finie si et seulement si $\mathrm{arc}[D](\mathcal{G})$ est de largeur de clique finie,

- retrait[$D$]($\mathcal{G}$) a une théorie monadique décidable si et seulement si $\mathrm{arc}[D](\mathcal{G})$ a une théorie monadique décidable.

**Preuve.** Si retrait[$D$]($\mathcal{G}$) est de largeur de clique finie, alors $\mathrm{arc}[D](\mathrm{retrait}[D](\mathcal{G})) = \mathrm{arc}[D](\mathcal{G})$ l'est aussi car $\mathrm{arc}[D]$ est une interprétation monadique. Symétriquement, si $\mathrm{arc}[D]$ est de largeur de clique finie, alors retrait[$D$]($\mathcal{G}$) l'est aussi. Le même principe s'applique pour la décidabilité de la théorie monadique. □

### 6.6.4 La construction

Le principe de la preuve est de construire un graphe de la forme

$$ \mathcal{H}' = \mathrm{retrait}[D](\mathcal{G}_1 \sqcap_{\eta} \mathcal{G}_2 \sqcap_{\eta'} \mathcal{G}_3) $$

où $\mathcal{G}_1, \mathcal{G}_2$ et $\mathcal{G}_3$ sont des graphes préfixes et $\mathcal{H}'$ est un arbre de théorie monadique indécidable.

Bien entendu, ce graphe n'est pas solution d'un VRA-système fini d'équations (car il serait de largeur arborescente bornée, donc HR-équationnel, donc de théorie monadique décidable). En revanche, $\mathrm{arc}[D](\mathcal{G}_1 \sqcap \mathcal{G}_2 \sqcap \mathcal{G}_3)$ est un graphe solution d'un VRA-système fini d'équations qui d'après le corollaire 6.35 est de largeur de clique finie et de théorie monadique indécidable.

Il nous reste donc à construire $\mathcal{G}_1, \mathcal{G}_2, \mathcal{G}_3$ et $D$. On pose $A = \{a, \bar{a}, b, \bar{b}, \bullet\}$. Les graphes sont présentés graphiquement à la figure 6.5. Les graphes $\mathcal{G}_1, \mathcal{G}_2$ et $\mathcal{G}_3$ correspondent respectivement à la demi-droite des entiers avec retour étiquetée par $a$ et $\bar{a}$, à la demi-droite des entiers avec retour étiquetée par $b$ et $\bar{b}$ et à l'arbre quaternaire complet étiqueté par $a, \bar{a}, b$ et $\bar{b}$. Chacun des arcs a été scindé en deux parties en insérant un sommet intermédiaire. Cette opération préserve les graphes préfixes et les graphes HR-équationnels mais pas les graphes VR-équationnels. Dans le cas présent, $\mathcal{G}_1, \mathcal{G}_2$ et $\mathcal{G}_3$ sont des graphes préfixes. Plus précisément, l'arc nouvellement ajouté est étiqueté par $\bullet$ et le nouveau sommet se voit attribuer une couleur qui permet d'identifier l'étiquette de l'arc de la scission duquel il provient.

Il s'agit de considérer le produit $\mathcal{H} = \mathcal{G}_1 \sqcap_{\eta} \mathcal{G}_2 \sqcap_{\eta'} \mathcal{G}_3$. Les fonctions de coloriage $\eta$ et $\eta'$ sont choisies de manière à ce que la couleur d'un sommet soit le triplet des couleurs qu'ont ses trois composantes dans $\mathcal{G}_1, \mathcal{G}_2$ et $\mathcal{G}_3$. Ainsi, le graphe $\mathcal{H}$ est-il étiqueté par $C = [3] \times [3] \times [5]$.
<figure><img src="image_40.png" /><figcaption>FIG. 6.6 – Construction du théorème 35.</figcaption></figure>

$D = (C \times A \times C) - D_c$. On considère le graphe $\mathcal{H}' = \text{retrait}[D](\mathcal{H})$.

**Lemme 6.36** Tous les sommets de $\mathcal{H}'$ de couleur appartenant à

$$C' = C - \{(0,0,0), (1,0,0), (1,0,1), (0,0,1), (2,0,0), (2,0,2), (0,0,2), (0,1,0), (0,1,3), (0,0,3), (0,2,0), (0,2,4), (0,0,4)\},$$

sont isolés (c.a.d. origine et destination d'aucun arc).

**Preuve.** Ces couleurs n'apparaissent pas dans $D_c$. $\square$

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

**Lemme 6.37** Tous les sommets de $\mathcal{H}'$ de couleur dans $C'$ sont destination d'au plus un arc.

**Preuve.** Au cas par cas. $\square$

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

**Corollaire 6.38** Le graphe $\mathcal{H}'$ est de largeur arborescente bornée (et donc de largeur de clique).
**Preuve.** On peut montrer que tout graphe fini connexe tel que tout sommet est destination d'au plus un arc est de l'une des deux formes suivantes :

- il s'agit d'un arbre,

- il s'agit d'un graphe tel que, si on lui enlève un arc approprié, il devient un arbre.

Ces deux types de graphes ont une largeur arborescente inférieure à 2. L'union disjointe de tels graphes a donc aussi une largeur arborescente inférieure à 2. □

**Remarque 6.39** *En fait, $\mathcal{H}'$ est une forêt d'arbres (de largeur arborescente 1) bien qu'il ne soit pas nécessaire de le montrer pour conclure.*

On ne s'intéresse plus maintenant qu'aux chemins de longueur 4 reliant ses sommets de couleur (0,0,0). On suppose que l'ensemble des sommets de couleur 0 de $\mathcal{G}_1$ (resp. $\mathcal{G}_2$) est $\mathbb{N}$, et que ce codage est naturel, c.a.d. que le premier sommet est numéroté 0 et que l'on passe de $n$ à $n+1$ en empruntant un arc $a$ (resp. $b$) puis un arc $\bullet$. De même, on identifie les sommets de $\mathcal{G}_3$ de couleur 0 avec $\{a, b, \bar{a}, \bar{b}\}^*$ de manière naturelle.

Un sommet de $\mathcal{H}'$ de couleur (0,0,0) est alors un triplet $(n_1, n_2, u)$ où $n_1, n_2 \in \mathbb{N}$ et $u \in \{a, b, \bar{a}, \bar{b}\}^*$.

**Lemme 6.40** *Tout sommet $(n_1, n_2, u)$ de couleur 0 de $\mathcal{H}'$ est origine d'un unique chemin étiqueté par $aa \bullet \bullet$ (resp. $bb \bullet \bullet$) et la destination de ce chemin est $(n_1 + 1, n_2, ua)$ (resp. $(n_1, n_2 + 1, ub)$).

Tout sommet $(n_1, n_2, u)$ de couleur 0 de $\mathcal{H}'$ est origine d'un arc étiqueté par $\bar{a}$ (resp. $\bar{b}$) si et seulement si $n_1 > 0$ (resp $n_2 > 0$) et dans ce cas la destination de chemin est $(n_1 - 1, n_2, u\bar{a})$ (resp. $(n_1, n_2 - 1, u\bar{b})$).

**Preuve.** Au cas par cas, arcs par arcs. □

**Lemme 6.41** *Il existe une interprétation monadique $\mathcal{I}$ telle que $\mathcal{I}(\mathcal{H}')$ est le dépliage de la grille avec retour.*

**Preuve.** Appliquer d'abord la substitution finie inverse $aa \bullet \bullet \mapsto a, bb \bullet \bullet \mapsto b, \overline{aa} \bullet \bullet \mapsto \bar{a}, \overline{bb} \bullet \bullet \mapsto \overline{b}$ puis restreindre par accessibilité à partir du sommet (0,0,ε) (il s'identifie de manière unique comme le seul sommet de couleur (0,0,0) destination d'aucun arc et origine d'aucun arc étiqueté par une lettre barrée).

La validité de cette construction repose bien sûr sur le lemme 6.40 □

**Corollaire 6.42** *Le graphe $\mathcal{H}'$ a une théorie monadique indécidable.*

Il ne reste plus qu'à conclure.
**Théorème 35** *Il existe un graphe* $\mathcal{G}$ *solution d'un VRA-système fini d'équations*
tel que

- $\mathcal{G}$ est de largeur de clique bornée,

- $\mathcal{G}$ a une théorie monadique indécidable.

**Preuve.** Le graphe $\mathcal{H}'$ est de largeur de clique bornée et a une théorie monadique indécidable. D'après le corollaire 6.35, il en est de même pour $\mathrm{arc}[D](\mathcal{G}_1 \sqcap \mathcal{G}_2 \sqcap \mathcal{G}_3)$ qui est solution d'un VRA-système fini d'équations. $\square$
# Chapitre 7

## Conclusion et perspectives

<figure><img src="image_43.png" /><figcaption>FIG. 7.1 – Familles de graphes solutions de systèmes d’équations finis.</figcaption></figure>

Notre étude a concerné les structures infinies admettant une description finie.

Nous avons montré que l’approche équationnelle, qui est classiquement utilisée pour les opérateurs HR ou VR, pouvait être étendue à d’autres opérateurs. En particulier, l’ajout d’opérateurs de produit (synchrone ou asynchrone) permet de décrire plusieurs classes de familles pour lesquelles aucune représentation de ce type n’était jusqu’alors connue. Nous nous sommes également intéressés dans un cas à étudier l’ajout d’un opérateur supplémentaire de fusion.

Nous avons étudié les différentes relations qu’entretiennent ces familles de structures. La figure 7.1 récapitule une partie de ces résultats. Chaque zone Z symbolise l’ensemble des graphes solutions de Z-systèmes finis d’équations. Ces inclusions sont aussi valables pour les systèmes infinis sauf en ce qui concerne le vide de l’intersection de la zone VRA et de la largeur arborescente bornée (cf. conclusions du paragraphe 6.5.2).
Nous nous sommes aussi attachés à établir les différentes représentation possibles pour ces structures. Celles-ci peuvent être classées en trois catégories : les représentations équationnelles, les représentations internes et les représentations par transformations. Les familles de structures les plus «robustes» admettent ces trois représentations (il s'agit des structures préfixes reconnaissables et des structures à présentation terme-automatique).

Enfin, nous avons montré comment certains résultats se généralisent naturellement aux systèmes infinis d'équations. En particulier, la preuve de Barthelmann reliant les graphes préfixes reconnaissables aux graphes HR-équationnels reste valide dans le contexte des systèmes infinis d'équations. Il en est de même pour la décidabilité du premier ordre (avec modalité de comptage) pour les structures admettant une présentation terme-automatique, ainsi que pour la décidabilité du premier ordre avec accessibilité pour les graphes de récriture suffixe.

Pour mener à bien ces démonstrations, nous avons dû développer les transducteurs descendants déterministes avec anticipation. Nous pensons que l'étude des structures infinies illustre pleinement l'utilité de cet outil.

## Problèmes ouverts

Pour finir, voici une liste de problèmes directement reliés au travail présenté et qui sont pour l'instant sans réponses.

Aussi étonnant que cela puisse paraitre, on ne connait pas les inclusions respectives de toutes les familles de graphes présentées jusqu'à présent. En particulier, la question ci-dessous est ouverte.

**Question 7.1 (C. Löding [Lö2b])** *Les graphes VRA-equationnels admettent-ils une présentation automatique ?*

Löding conjecture que la réponse à cette question est négative. Un graphe solution d'un VRA-système fini d'équations candidat à ne pas admettre une présentation automatique se décrit par récriture suffixe de termes comme suit. L'ensemble de sommets est l'ensemble des termes sur l'alphabet $\{c:0, p:2\}$ et l'unique règle de récriture remplace le sous-terme $c$ par $p(c, c)$. Ce graphe est décomposé en couches (correspondant au nombre de symboles $c$ contenus dans le terme), et tout arc issu d'un sommet de la couche de niveau $n$ a pour destination un sommet de la couche de niveau $(n+1)$. Le nombre de sommets de la couche de niveau $n$ est $\frac{1}{n+1} \binom{2n}{n}$.

Ce nombre est connu sous le nom de nombre de Catalan, et pour cela, on appelle ce graphe *graphe de Catalan*.

Plusieurs questions concernent l'opérateur *fusion*. La première correspond à la remarque 4.19 page 110.

**Question 7.2** *La famille des structures solutions de VR' + fusion-systèmes finis*
d'équations est-elle égale à la famille des structures solutions de VR'-systèmes finis d'équations si l'opérateur fusion peut prendre comme paramètre n'importe quel symbole unaire (contrairement au théorème 16 page 115 dans lequel seules les fusions de couleurs sont autorisées)? Si la réponse est positive, la transformation du système d'équations peut-elle être effectuée par un transducteur déterministe?

L'impact de l'opérateur de fusion reste à étudier pour les autres systèmes d'équations.

**Question 7.3** Les structures solutions de VRS'-systèmes finis d'équations utilisant des opérateurs fusion supplémentaires coïncident-elles avec les structures solutions de VRS'-systèmes finis d'équations? Si la réponse est positive, la transformation des systèmes d'équations peut-elle être effectuée par un transducteur déterministe?

À ces deux questions, il est probable que la réponse est positive et qu'il ne s'agit que d'une adaptation de la preuve du théorème 16 traitant le cas du produit synchrone. Notons toutefois qu'il est nécessaire, pour donner un sens à cette question, de modifier les opérateurs VRS' afin qu'ils puissent gérer les couleurs.

Enfin, une dernière question concerne les graphes de récriture suffixe.

**Question 7.4** Quelle est la nature de la famille de graphes solutions de VRA-systèmes finis d'équations augmentés de l'opérateur fusion ? Est-elle égale à la famille des graphes solutions des VRA-systèmes finis d'équations ?

La réponse à cette question est, d'après l'auteur, négative. Un candidat contre-exemple est le graphe solution en $x$ des équations sur les couleurs $\{0, 1\}$ et l'unique étiquette $a$ ci-dessous.

$$ 
\begin{align*}
x &= \text{fusion}[0](\text{sommet}[0] \oplus (x \sqcap \eta A)) \\
A &= \text{arc}[0, a, 1](\text{sommet}[0] \oplus \text{sommet}[1]) \\
\eta(c, c') &= \begin{cases} 0 & \text{si } c = c' = 0 \\ 1 & \text{sinon} \end{cases}
\end{align*}
$$

Il s'agit d'un hypercube de dimension dénombrable (dont tous les sommets sont de couleur 1 sauf un de couleur 0).

Il est toutefois simple de montrer que la famille des graphes solutions des VRA-systèmes finis d'équations augmentés d'un opérateur de fusion a une théorie au premier ordre avec accessibilité décidable. Ceci rend cette famille attractive.
Bibliographie

[AN01] A. Arnold and D. Niwiński. *Rudiments of μ-Calculus*, volume 146 of *Studies in Logic and the Foundations of Mathematics*. Elsevier, 2001.

[Bar97] K. Barthelmann. On equational simple graphs. Technical Report 9, Universität Mainz, Institut für Informatik, 1997.

[Bar98] K. Barthelmann. When can equational simple graphs be generated by hyperedge replacement? In L. Brim, J. Gruska, and J. Zlatuska, editors, *MFCS'98*, LNCS, pages 543–552. Springer Verlag, 1998.

[Büc60] J. Büchi. On a decision method in restricted second order arithmetic. In *Proceedings of the International Congress on Logic, Methodology and Philosophy of Science*, pages 1–11. Stanford University press, 1960.

[Büc64] J. Büchi. Regular canonical systems. In *Archiv für Mathematische Grundlagenforschung*, volume 6, pages 91–111., 1964.

[Bek67] H. Bekič. Definable operations in general algebras, and the theory of automata and flowcharts. Technical report, IBM Laboratory, Wien, 1967.

[Blu99] A. Blumensath. Automatic structures. Diploma thesis, RWTH-Aachen, 1999.

[Blu01] A. Blumensath. Prefix-recognisable graphs and monadic second-order logic. Technical Report AIB-06-2001, RWTH Aachen, May 2001.

[Cac03] T. Cachat. Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In *Proceedings of the 30th International Colloquium on Automata, Languages, and Programming*, volume 2719 of LNCS, pages 556–569. Springer-Verlag, 2003.

[Cau90] D. Caucal. On the regular structure of prefix rewriting. In *Caap 90*, volume 431 of LNCS, pages 87–102, 1990. Paru dans TCS 106, pp. 61–86, 1992.

[Cau96] D. Caucal. On infinite transition graphs having a decidable monadic theory. In *ICALP'96*, volume 1099 of LNCS, pages 194–205, 1996.

[Cau98] D. Caucal. *Sur des graphes infinis réguliers*. Habilitation à diriger les recherches, Université de Rennes I, 1998.
[Cau02] D. Caucal. On infinite terms having a decidable monadic theory. In *MFCS'02*, pages 79–115. Springer Verlag, 2002.

[CC03] A. Carayol and T. Colcombet. On equivalent representations of infinite structures. In *ICALP'03*, LNCS. Springer Verlag, July 2003.

[CDG+97] H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications, 1997. release October, 1rst 2002.

[CF00] T. Colcombet and P. Fradet. Enforcing trace properties by program transformation. In *27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, January 2000.

[CK02] B. Courcelle and T. Knapik. The evaluation of first-order substitution is monadic second-order compatible. *Theoretical Computer Science*, 281:177–206, 2002.

[CL04] T. Colcombet and C. Löding. On the expressive power of deterministic transducers over infinite trees. In *STACS'04*, LNCS. Springer Verlag, 2004.

[CM02] B. Courcelle and J.A Makowsky. Fusion in relational structures and the verification of mso logic. In *MSCS*, volume 12, pages 203–235, 2002.

[Col02a] T. Colcombet. On families of graphs having a decidable first order theory with reachability. In *ICALP'02*, volume 2380 of LNCS. Springer, July 2002.

[Col02b] T. Colcombet. Rewriting in the partial algebra of typed terms modulo AC. *Electronic Notes in Theoretical Computer Science*, 68(6), 2002.

[Cou89] B. Courcelle. The monadic second-order logic of graphs ii: infinite graphs of bounded tree width. *Math. Systems Theory*, 21:187–221, 1989.

[Cou90] B. Courcelle. Graph rewriting: an algebraic and logic approach. *Handbook of TCS*, B:193–242, 1990.

[Cou92] B. Courcelle. The monadic second-order logic of graphs iii: Tree-decompositions, minors and complexity issues. 26(3):257–286, 1992.

[Cou94] B. Courcelle. Monadic second-order graph transductions: A survey. In *Theoretical Computer Science*, volume 126, pages 53–75. Elsevier, 1994.

[Cou95] B. Courcelle. The monadic second order logic of graphs ix: Machines and their behaviours. In *Theoretical Computer Science*, volume 151, pages 125–162, 1995.

[Cou97] B. Courcelle. On the expression of graph properties in some fragment of monadic second-order logic. In N. Immerman and P. Kolaitis,
<table>
  <tr>
    <td></td>
    <td>editors, Descriptive Complexity and Finite Models, volume 31 of DI-MACS Series in Discrete Mathematics, pages 33–62. AMS, 1997.</td>
  </tr>
  <tr>
    <td>[Cou00]</td>
    <td>B. Courcelle. Clique-Width of Countable Graphs: A Compactness Property. unpublished, 2000.</td>
  </tr>
  <tr>
    <td>[Cou03]</td>
    <td>B. Courcelle. The monadic second-order logic of graphs xiv: Uniformly sparse graphs and edge set quantifications. Theoretical Computer Science, 299(1-36), 2003.</td>
  </tr>
  <tr>
    <td>[CW98]</td>
    <td>B. Courcelle and I. Walukiewicz. Monadic second-order logic, graph coverings and unfoldings of transition systems. In Annals of Pure and Applied Logic, 1998.</td>
  </tr>
  <tr>
    <td>[CW03]</td>
    <td>A. Carayol and S. Wöhrle. The caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In Springer-Verlag, editor, FSTTCS'03, Int. Conf. on Foundations of Software Technology and Theoretical Computer Science, LNCS, 2003.</td>
  </tr>
  <tr>
    <td>[Die00]</td>
    <td>R. Diestel. Graph Theory, second edition. Springer Verlag, 2000.</td>
  </tr>
  <tr>
    <td>[DT90]</td>
    <td>M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In LICS'90, pages 242–248. IEEE, 1990.</td>
  </tr>
  <tr>
    <td>[EGO00]</td>
    <td>C. Hirsch E. Grädel and M. Otto. Back and forth between guarded and modal logics. In 15th IEEE Symposium on Logic in Computer Science, pages 217–228, 2000.</td>
  </tr>
  <tr>
    <td>[Eil74]</td>
    <td>S. Eilenberg. Automata, Languages and Machines, volume A. Academic Press, New York, 1974.</td>
  </tr>
  <tr>
    <td>[Eng77]</td>
    <td>J. Engelfriet. Top-down tree transducers with regular lookahead. Mathematical System Theory, 10:289–303, 1977.</td>
  </tr>
  <tr>
    <td>[Eng94]</td>
    <td>J. Engelfriet. Graph grammars and tree transducers. In S. Tison, editor, CAAP'94, volume 787 of LNCS, pages 15–36. Springer Verlag, 1994.</td>
  </tr>
  <tr>
    <td>[Eng99]</td>
    <td>J. Engelfriet. Derivation trees of ground term rewriting systems. Information and Computation, 152(1):1–15, 1999.</td>
  </tr>
  <tr>
    <td>[FL79]</td>
    <td>M. Fischer and R. Ladner. Propositional dynamic logic of regular programs. Computer and System Sciences, 2(18):194–211, 1979.</td>
  </tr>
  <tr>
    <td>[FV59]</td>
    <td>S. Feferman and R. Vaught. The first order properties of products of algebraic systems. Fundamenta Mathematicæ, 47:57–103, 1959.</td>
  </tr>
  <tr>
    <td>[HU79]</td>
    <td>J.E. Hopcroft and J.D. Ullman. Introduction to automata theory, languages and computation. Addison-Wesley, 1979.</td>
  </tr>
  <tr>
    <td>[KN94]</td>
    <td>B. Khoussainov and A. Nerode. Automatic presentations of structures. In D. Leivant, editor, International Workshop in Logic and Computational Complexity, volume 960 of LNCS, pages 367–392, 1994.</td>
  </tr>
  <tr>
    <td>[KNU02]</td>
    <td>T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In M. Nielsen, editor, FOSSACS'02, LNCS, 2002.</td>
  </tr>
</table>
[Koz83] D. Kozen. Results on the propositional mu-calculus. *Theoretical Computer Science*, 27:333-354, 1983.

[LÖ2a] C. Löding. Ground tree rewriting graphs of bounded tree width. In *STACS'02*, volume 2285 of LNCS, pages 559-570. Springer Verlag, 2002.

[LÖ2b] C. Löding. *Infinite Graphs Generated by Tree Rewriting*. PhD thesis, RWTH Aachen, 2002.

[LÖ2c] C. Löding. Model-checking infinite systems generated by ground tree rewriting. In *FoSSaCS 2002*, volume 2303 of LNCS, pages 280-294. Springer Verlag, 2002.

[Min67] M. Minsky. *Computation: Finite and Infinite Machines*. Prentice hall, 1967.

[MS85] D. Muller and P. Schupp. The theory of ends, pushdown automata, and second-order logic. *Theoretical Computer Science*, 37:51-75, 1985.

[MS97] A. Mateescu and A. Salomaa. *Aspects of classical language theory*, volume 1 of *Handbook of formal languages*. G. Rozenberg, Springer verlag edition, 1997.

[MW67] J. Mezei and J. B. Wright. Algebraic automata and context-free sets. *Information and Control*, 11(2-3):3-29, 1967.

[NT01] M. Napoli and S. La Torre. Automata-based representations for infinite graphs. *Theoretical Informatics and Applications*, 35(4):311-330, 2001.

[Rab69] M. Rabin. Decidability of second-order theories and automata on infinite trees. *Trans. Amer. Math. Soc.*, 141:1-35, 1969.

[RS83] N. Robertson and P. Seymour. Graph minors i, excluding a forest. *Journal of Combinatorial Theory, B*, 35:39-61, 1983.

[RS86] N. Robertson and P. Seymour. Graph minors v, excluding a planar graph. *Journal of Combinatorial Theory, B*, 41:92-114, 1986.

[RS90] N. Robertson and P. Seymour. Graph minors x, obstructions to tree-decomposition. *Journal of Combinatorial Theory, B*, 52:153-190, 1990.

[Sem84] A. Semenov. Decidability of monadic theories. In *MFCS'84*, volume 176 of LNCS, pages 162-175. Springer-Verlag, 1984.

[She75] S. Shelah. The monadic second order theory of order. *Annals of Mathematics*, 102:379-419, 1975.

[Tar55] A. Tarski. A lattice-thoretical fixpoint theorem and its application. *Pacific Journal of Mathematics*, 5:285-309, 1955.

[Tho88] R. Thomas. The tree-width compactness theorem for hypergraphs. *manuscrit*, 1988.
[Tho89] C. Thomassen. Configurations in graphs of large minimum degree, connectivity or chromatic number. In G. S. Bloom, editor, *Proceedings of 3rd International Conference on Combinatorial Mathematics*, volume 555, pages 402–411. New-York Academy of Science, 1989.

[Tho90] W. Thomas. Automata on infinite objects. In J. Leeuven, editor, *Handbook of Theoretical Computer Science*, volume B, pages 995–1072. Elsevier, 1990.

[Tho97] W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, *Handbook of Formal Languages*, volume III, pages 389–455. Springer Verlag, 1997.

[Urv02] T. Urvoy. On abstract families of graphs. In *DLT 02*, 2002.

[Wal96] I. Walukiewicz. Monadic second order logic on tree-like structures. In *STACS'96*, volume 1046 of LNCS, pages 401–414, 1996.
# Annexe A

## Annexes

### A.1 Complément sur les tranducteurs déterministes

#### Arbre d'exécution et états inévitables

Afin de pouvoir énoncer le lemme de correction dans toute sa généralité, il faut pouvoir faire référence à l'exécution d'un transducteur lorsqu'il est appliqué à un terme. Cette exécution est représentée comme un terme, appelé arbre d'exécution, dont chaque symbole représente une transition du transducteur. La totalité du terme représente la totalité de l'exécution du transducteur sur un terme donné. L'arbre d'exécution permet alors de reconstruire par évaluation le résultat de ce transducteur lors de cette exécution.

Il convient tout d'abord de préciser cette notion d'arbre d'exécution. Considérons un transducteur déterministe $t = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$. Soit $T \subseteq \delta$ un ensemble de transitions, on définit l'alphabet gradué $<T>$ suivant :

$$ \langle T \rangle = \{ \langle \gamma \rangle \mid \gamma \in T \}, \\ \text{avec pour tout } \gamma \in T, \quad | \langle \gamma \rangle | = \begin{cases} |f| & \text{si } \gamma = q(x) \rightarrow f(r_1(x), \dots, r_{|f|}(x)), \\ 1 & \text{sinon.} \end{cases} $$

Soit $t^0$ un $\mathcal{F}$-terme. On construit par récurrence sur l'entier $n$ et pour tout
état $q \in Q$, le terme $exec_n^t[q](t^0) \in \mathcal{T}_{\perp}^{\omega}(\langle \delta \rangle)$ comme suit.

$$
exec_n^t[q](t^0) = \left\{
\begin{array}{ll}
\perp & \text{si } n = 0, \\
< \gamma > (exec_{n-1}^t[r_1](t^0), \dots, exec_{n-1}^t[r_{|g|}](t^0)) & \text{si } \gamma = q(x) \to g(r_1(x), \dots, r_{|g|}(x)) \in \delta, \\
< \gamma > (exec_{n-1}^t[r](t_i^0)) & \text{si } \gamma = q(f(x_1, \dots, x_{|f|})) \to r(x_i) \in \delta, \\
\text{et } t^0 = f(t_1^0, \dots, t_{|f|}^0), \\
< \gamma > (exec_{n-1}^t[r](t^0)) & \text{si } \gamma = q(x \in L) \to r(x) \in \delta \\
\text{et } t^0 \in L \\
\text{non défini} & \text{sinon.}
\end{array}
\right.
$$

Pour tout état $q \in Q$, le $<\delta>$-terme $exec^t[q](t^0)$ se définit alors par passage à la limite : $exec^t[q](t^0) = \sqcup_{n \in \mathbb{N}} exec_n^t[q](t^0)$. Cette définition a bien un sens (cf. définition de l'évaluation d'un transducteur). Dans la pratique, on omet de préciser le transducteur déterministe $\mathbf{t}$ de la notation $exec^t$ quand il n'y a a pas d'ambiguïté.

À partir d'un terme sur l'alphabet $< \delta >$, on peut recomposer un $\mathcal{F}'$-terme en l'évaluant dans la $< \delta >$-algèbre $\mathbf{A}^t$ de domaine $\mathcal{T}_{\perp}^{\omega}(\mathcal{F}')$ et dont l'application sémantique est définie comme suit :

$$
\begin{align*}
\mathrm{sem}[\mathbf{A}^t](<q(x) \to g(q_1(x), \dots, q_{|g|}(x))>) (t_1, \dots, t_{|g|}) &= g(\mathrm{sem}[\mathbf{A}^t](t_1), \dots, \mathrm{sem}[\mathbf{A}^t](t_{|f|})) , \\
\mathrm{sem}[\mathbf{A}^t](<q(f(x_1, \dots, x_{|f|}))>) &\to r(x_i)(t) = \mathrm{sem}[\mathbf{A}^t](t) , \\
\mathrm{sem}[\mathbf{A}^t](<q(x \in L) \to r(x)>) (t) &= \mathrm{sem}[\mathbf{A}^t](t) .
\end{align*}
$$

Énonçons un résultat bien naturel.

**Lemme A.1** Soit $\mathbf{t}$ un transducteur déterministe des $\mathcal{F}$-termes dans les $\mathcal{F}'$-termes, $q$ un de ses états et $t^0$ un $\mathcal{F}$-terme, alors $\mathbf{t}_q(t^0)$ est défini si et seulement si $exec^t[q](t^0)$ est défini, et dans ce cas,

$$
\mathbf{t}_q(t^0) = [[exec^t[q](t^0)]]_{\mathbf{A}^t} .
$$

On peut aussi remarquer que la définition de *exec* est très similaire à la définition de l'exécution d'un transducteur déterministe. Ce lien est explicité par le lemme A.2.

**Lemme A.2** Pour $\mathbf{t}$ un transducteur déterministe et $q$ un de ses états, il existe un transducteur déterministe $\mathbf{t}^e$ des $\mathcal{F}$-termes dans les $\mathcal{F}^t$-termes tel que $\mathbf{t}^e = exec^t[q]$.

**Construction.** Le transducteur $\mathbf{t}^e$ s'obtient de $\mathbf{t}$ en :

- remplacant le symbole $g$ produit par une transition $\gamma$ par $<\gamma>$,
- faisant suivre chaque transition de consommation ou d'anticipation $\gamma$ par une transition produisant $< \gamma >$ (cela nécessite d'insérer un état intermédiaire).

□

Soit $\mathbf{t} = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$ un transducteur déterministe et $T \subseteq \delta$ un ensemble de ses transitions. On dit que $T$ est inévitable (dans $\mathbf{t}$) si pour tout $\mathcal{F}$-terme $t^0$ et tout état $q \in Q$ tels que $\mathbf{t}_q(t^0)$ est défini, alors toutes les branches infinies de $exec[q](t^0)$ contiennent une infinité d'occurrences d'un symbole $< \gamma > \in < T >$. La définition s'étend aux états. Soit $Q' \subseteq Q$ un ensemble d'états, $Q'$ est inévitable (dans $\mathbf{t}$) si l'ensemble des transitions de $\delta$ dont l'état de tête est dans $Q'$ est lui-même inévitable.

**Remarque A.3** Soit $T \subseteq \delta$ un ensemble de transitions tel que tout « cycle » de $\mathbf{t}$ contienne une transition de $T$, alors $T$ est inévitable.

La réciproque est fausse, et ce en particulier car le transducteur déterministe peut en utilisant une anticipation s'assurer qu'un état sera atteint au bout d'un nombre (non borné mais) fini d'itérations. Considérons par exemple le transducteur déterministe sur l'alphabet $\{a : 1, b : 0\}$ qui n'est défini que sur les termes finis, et dans ce cas renvoie le terme lui même :

$$ 
\begin{align*}
q(x \in (\mu y.a(y).b)[])) &\rightarrow q', \\
q'(a(x)) &\rightarrow a(q(x)), \\
q'(c) &\rightarrow c.
\end{align*}
$$

Ce transducteur déterministe contient un cycle, et pourtant $\emptyset$ est inévitable car toute exécution de ce transducteur est finie.

**Propriété A.4** Déterminer si un ensemble de transitions d'un transducteur déterministe est inévitable est décidable.

**Preuve.** Soient $\mathbf{t} = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$ un transducteur et $T \subseteq \delta$ un ensemble de transitions dont on cherche à déterminer l'inévitabilité. L'ensemble des $< \delta >$-termes possèdant une branche ne contenant pas une infinité de symboles de $< T >$ est reconnaissable. Son image inverse par $\mathbf{t}^e$ (cf. lemme A.2) l'est aussi. Cet ensemble est vide si et seulement si $T$ est inévitable, et le vide d'une partie reconnaissable est décidable. □

## Preuve du lemme 3.59

**Preuve.** La preuve consiste à évaluer le terme d'exécution associé à $t^0$ en utilisant les applications $h$ comme sémantique. Le cœur de la preuve établit la correc-
tion de cette approche. Formalisons tout d'abord ce que l'on entend par «évaluer» un terme d'exécution. On définit pour tout terme $t^0 \in \mathcal{T}^\omega(\mathcal{F})$, tout état $q$ et tout terme fini $t^e \subseteq \text{exec}[q](t^0)$ l'élément $[[t^e]]_{q,t^0} \in \mathcal{R}[q, t^0]$ par récurrence comme suit

- si $t^e = \perp$, alors $[[t^e]]_{q,t^0} = \perp_{q,t^0}$,

- si $t^e = \gamma(u_1^e, \dots, u_{|g|}^e)$ pour $\gamma = q(x) \to g(r_1(x), \dots, r_{|g|}(x)) \in \delta$ alors,

$$[[t^e]]_{q,t^0} = h_{\gamma,t^0}([u_1^e]_{r_1,t^0}, \dots, [u_{|g|}^e]_{r_{|g|},t^0}),$$

- si $t^e = \gamma(u^e)$ pour $\gamma = q(f(x_1, \dots, x_{|f|})) \to r(x_i)$, et $t^0 = f(t_1^0, \dots, t_{|f|}^0)$ alors,

$$[[t^e]]_{q,t^0} = h_{\gamma,t^0}([u^e]_{r,t_i^0}),$$

- si $t^e = \gamma(u^e)$ pour $\gamma = q(x \in L) \to r(x)$,

$$[[t^e]]_{q,t^0} = h_{\gamma,t^0}([t^e]_{r,t^0}).$$

La définition s'étend par par passage à la limite à $\text{exec}[q](t^0)$. Ainsi, il s'agit de la définition standard dans une algèbre si ce n'est que les information supplémentaires $q$ et $t^0$ sont maintenues simultanément.

Le reste de la preuve consiste à montrer que $[[\text{exec}[q](t^0)]_{q,t^0}(t^0, \mathbf{t}(t^0))$, c.a.d. d'une part $\rho([[\text{exec}[q](t^0)]_{q,t^0}) = t^0$ et d'autre part $\rho'([[\text{exec}[q](t^0)]_{q,t^0}) = \mathbf{t}(t^0)$.

Preuve de $\rho'([\text{exec}[q](t^0)]_{q,t^0}) = \mathbf{t}(t^0)$. D'après le lemme A.1 et par passage à la limite, il est suffisant d'établir que $\text{exec}[q](t^0)$ est limite d'une chaîne de termes finis $(t_n^e)_{n \in \mathbb{N}}$ telle que pour tout $n \in \mathbb{N}$ on a $[[t_n^e]]_{\mathbf{A}^n} = \rho'([[[t_n^e]]_{q,t^0}])$. Pour cela, on construit $t_n^e$ en coupant toutes les branches du terme $\text{exec}[q](t^0)$ au niveau de la n-ième occurence d'un symbole de $< \delta_\perp >$ ou $\delta_\perp$ est l'ensemble des transitions ayant leur état de tête dans $Q_\perp$. On remplace le sous-arbre coupé par $\perp$. D'après l'hypothèse 3 les termes ainsi construits sont bien finis. Ils ont aussi naturellement $t^e$ pour limite. Les hypothèses 3, a, b et c permettent alors par récurrence d'établir que $[[t_n^e]]_{\mathbf{A}^n} = \rho'([[[t^e]]_{q,t^0}])$.

Preuve de $\rho(\text{exec}[q](t^0))_{q,t^0} = t^0$. Remarquons tout d'abord que par définition, $\rho(\text{exec}[q](t^0))_{q,t^0} \subseteq t^0$. Il s'agit de montrer l'autre inégalité.

Soit $t^e$ une terme d'exécution. On note $\text{prof}_c(t^e)$ la hauteur de $t^e$ après que l'on a remplacé tous les sous-arbres ayant une transition de consommation à la racine par $\perp$ (avec par convention la hauteur de $\perp$ égale à 0).

On montre par récurrence sur $t$ la propriété suivante.

**Hyp. réc.:** pour tout terme $t^0 \in \mathcal{T}^\omega(\mathcal{F})$, tout terme fini $t \in \overleftarrow{t^0}$ et tout état $q$, il existe un terme $t^e \subseteq \text{exec}[q](t^0)$ tel que $t \subseteq \rho([[t^e]]_{q,t^0})$.
Remarquons tout d'abord qu'une fois cette hypothèse établie, par passage à la limite, on obtient $t^0 \subseteq \rho(\llbracket exec[q](t^0) \rrbracket)$ et la preuve est terminée.

La récurrence s'effectue sur la hauteur de $t$ et $\text{prof}_c(\text{exec}[q](t^0))$.

- Supposons $t = \perp$, alors $t^e = \perp$ convient.

- Supposons $t = f(t_1, \dots, t_{|f|})$ et $\text{prof}_c(\text{exec}[q](t^0)) = 0$. La deuxième hypothèse implique que le symbole à la racine de $\text{exec}[q](t^0)$ est une transition de consommation $\gamma$. Soit $t^0 = f(t_1^0, \dots, t_{|f|}^0)$. La transition $\gamma$ consomme un symbole $f$ car $\text{exec}[q](t^0)$ est défini et que $f$ est le symbole à la racine de $t^0$. Soit donc $\gamma = q(f(x_1, \dots, x_{|f|})) \to r(x_i)$. Par hypothèse de récurrence, il existe un terme fini $u^e \subseteq \text{exec}[r](t_i^0)$ tel que $t_i \subseteq \rho(\llbracket u^e \rrbracket_{r,t_i^0})$. On a alors,

$$ 
\begin{align*}
t \subseteq f(t_1^0, \dots, t_{i-1}^0, t_i, t_{i+1}^0, \dots, t_{|f|}^0) \quad &(\text{car } \forall j. \ t_j \subseteq t_j^0) \\
\subseteq f(t_1^0, \dots, t_{i-1}^0, \rho(\llbracket u^e \rrbracket_{r,t^0,i}), t_{i+1}^0, \dots, t_{|f|}^0) \quad &(\text{hyp. rec.}) \\
\subseteq \rho(h_{\gamma,t^0}(\llbracket u^e \rrbracket_{r,t_i^0})) \quad &(\text{hyp. b}) \\
\subseteq \rho(\llbracket < \gamma > (u^e) \rrbracket_{q,t^0}) \quad &(\text{def. } \llbracket \rrbracket)
\end{align*}
$$

Donc $t^e = \llbracket \gamma \rrbracket (u^e)$ satisfait l'hypothèse de récurrence.

- Supposons $t \neq \perp$ et $\text{prof}_c(\text{exec}[q](t^0)) > 0$. Soit $\gamma$ la transition à la racine de $\text{exec}[q](t^0)$. Cette transition ne peut pas être une transition de consommation par hypothèse et donc seuls deux cas sont possibles.

1. si $\gamma = q(x) \to g(r_1(x), \dots, r_{|g|}(x))$, alors pour tout $i \in [|g|]$, par hypothèse de récurrence, pour tout $i \in [|g|]$, il existe $t_i^e \subseteq \text{exec}[r_i](t^0)$ tel que $t \subseteq \rho(\llbracket t_i^e \rrbracket_{r_i,t^0})$. On a alors,

$$ 
\begin{align*}
t \subseteq \bigcap \{ & \rho(\llbracket t_1^e \rrbracket_{r_1,t^0}), \dots, \rho(\llbracket t_{|g|}^e \rrbracket_{r_{|g|},t^0}) \} \\
\subseteq & \rho(h_{\gamma,t^0}(\llbracket t_1^e \rrbracket_{r_1,t^0}, \dots, \llbracket t_{|g|}^e \rrbracket_{r_{|g|},t^0})) \quad &(\text{hyp. a}) \\
\subseteq & \rho(\llbracket < \gamma > (t_1^e, \dots, t_{|g|}^e) \rrbracket_{q,t^0}) \quad &(\text{def. } \llbracket \rrbracket)
\end{align*}
$$

Donc $t^e = \llbracket \gamma > (t_1^e, \dots, t_{|g|}^e) \rrbracket$ satisfait l'hypothèse de récurrence.

2. si $\gamma = q(x \in L) \to r(x)$ avec $t^0 \in L$, alors par hypothèse de récurrence il existe $u^e \subseteq \text{exec}[r](t^0)$ tel que $t \subseteq \llbracket u^e \rrbracket_{r,t^0}$. On a alors,

$$ 
\begin{align*}
t \subseteq \rho(h_{\gamma,t^0}(\llbracket u^e \rrbracket_{r,t^0})) \quad &(\text{hyp. c}) \\
\subseteq \rho(\llbracket < \gamma > (u^e) \rrbracket_{q,t^0}) \quad &(\text{def. } \llbracket \rrbracket)
\end{align*}
$$

Donc $t^e = \llbracket \gamma > (u^e) \rrbracket$ satisfait l'hypothèse de récurrence.

□
## A.2 Complément sur le théorème 16

**Lemme A.5 (opérateur sommet)** Soient $E \subseteq C$ et $c \in C$. Il existe une structure $VR'$-définissable $f^{\text{sommet}[c],E}$ telle que :

$$ \mathcal{R}[E](\text{sommet}[c], f^{\text{sommet}[c]}) . $$

**Preuve.** Si $c \in E$, on pose $f^{\text{sommet}[c],E} = \mathcal{I}_0(\text{sommet}[c])$, sinon $f^{\text{sommet}[c],E} = \mathcal{I}_0(\perp)$. Dans tous les cas, $S$ est finie et donc $VR'$-définissable et satisfait de plus la relation $\mathcal{R}[E](\text{sommet}[c], f^{\text{sommet}[c],E})$. $\square$

**Lemme A.6 (opérateur interprétation)** Soient $E \subseteq C$ et $\mathcal{I}$ une interprétation booléenne positive des $\Sigma$-structures dans les $\Sigma$-structures. Alors il existe une application $VR'$-définissable $f^{\mathcal{I},E}$ telle que pour toute $\Sigma$-structure $S$ et pour toute $\Sigma'$-structure $S'$, on a continuement

$$ \text{si } \mathcal{R}[E](S, S') \text{ alors } \mathcal{R}[E](\mathcal{I}(S), f^{\mathcal{I},E}(S')) . $$

**Preuve.** On pose :

$$ \mathcal{I}_0^{\mathcal{I}} = \left| \begin{array}{ll} < X, g, \phi > (\overline{X}) & : < X, g, \phi^{\mathcal{I}} > (\overline{X}) \\ c(x) & : c(x) \end{array} \right| . $$

Supposons $\mathcal{R}[E](S, S')$. On a alors :

$$
\begin{align*}
\mathcal{I}_0(\mathcal{I}(S))|_E &= \left( \left| \begin{array}{ll} < X, g, \phi > \overline{X} & : \overline{g} \wedge \phi^{\mathcal{I}} \\ c(x) & : c(x) \end{array} \right|_{\overline{E}} \right) \quad (\text{lemme 4.21}) \\
&= \mathcal{I}_0^{\mathcal{I}}(\mathcal{I}_0(S))|_E \tag{def $\mathcal{I}_0^{\mathcal{I}}$} \\
&= \mathcal{I}_0^{\mathcal{I}}(\mathcal{I}_0(S)|_E) \tag{lemme 4.26} \\
&\approx \mathcal{I}_0^{\mathcal{I}}(\mathcal{I}'_0(S')) \tag{car $\mathcal{R}[E](S, S')$}
\end{align*}
$$

Donc $f^{\mathcal{I},E}(x) = \mathcal{I}_0^{\mathcal{I}}(\mathcal{I}'_0(x))$ satisfait les conclusions du lemme. $\square$

**Lemme A.7 (opérateur $\oplus$)** Soit $E \subseteq C$. Il existe une application binaire $VR'$-définissable $f^{\oplus,E}$ telle que pour toutes $\Sigma$-structures $S_0$ et $S_1$ et pour toutes $\Sigma'$-structures $S'_0$ et $S'_1$, on a continuement

$$ \text{si } \mathcal{R}[E](S_0, S'_0) \text{ et } \mathcal{R}[E](S_1, S'_1), \text{ alors } \mathcal{R}[E](S_0 \oplus S_1, f^{\oplus,E}(S'_0, S'_1)) . $$
**Preuve.** On pose :

$$ \mathcal{I}^{\oplus} = \left| \begin{array}{l} < X, g, \phi > (\bar{X}) : \bigvee_{(\psi_1, \psi_2) \in \phi_g^{\oplus}} \left\langle FV(\psi_1), g|_{FV(\psi_1)}, \psi_1 > \overline{FV(\psi_1)} \right\rangle \\ \phantom{< X, g, \phi > (\bar{X}) : \bigvee_{(\psi_1, \psi_2) \in \phi_g^{\oplus}} \left\langle} \wedge \\ < FV(\psi_2), g|_{FV(\psi_2)}, \psi_2 > \overline{FV(\psi_2)} \right\rangle \end{array} \right| $$

On pose alors $f^{\oplus,E}(S'_1, S'_2) = \mathcal{I}^{\oplus}(\mathcal{I}'_0(S'_1) \oplus \mathcal{I}'_0(S'_2))$. Cette application satisfait les conclusions du lemme. □

**Lemme A.8 (opérateur fusion)** Soient $E \subseteq C$ et $c_0 \in C$. Il existe une application $\text{VR}'$-définissable $f^{\text{fusion}[c_0],E}$ telle que pour toute $\Sigma$-structure $S$ contenant un sommet de couleur $c_0$ et pour toute $\Sigma'$-structure $S'$, on a continuement

$$ \text{si } \mathcal{R}[E - \{c_0\}](S, S') \text{ alors } \mathcal{R}[E](\text{fusion}[c_0](S), f^{\text{fusion}[c_0],E}(S')) . $$

**Preuve.** Supposons $c_0 \in E$ (le cas $c_0 \notin E$ est similaire).

$$ \mathcal{I}^{\text{fusion}} = \left| \begin{array}{l} < X, g, \phi > (\bar{X}) : \left\langle X - X_0, g|_{X-X_0}, \phi_{g,c_0}} > \overline{(X-X_0)} \right\rangle \\ \text{avec } X_0 = g^{-1}(c_0) \\ c(x) : c(x) \end{array} \right| $$

On pose de plus

$$ \text{net} = \left| \begin{array}{l} < X, g, \phi > (\bar{X}) : < X, g, \phi > (\bar{X}) \text{ si } g^{-1}(c_0) = \emptyset \\ < X, g, \phi > (\bar{X}) : \text{faux} \text{ si } g^{-1}(c_0) \neq \emptyset \\ c(x) : c(x) \end{array} \right|, $$

$$ \text{et } eq = \left| \begin{array}{l} < X, g, \phi > (\bar{X}) : < X, g, \phi > (\bar{X}) \\ c(x) : c(x) \\ x \sim y : x \sim y \lor (c_0(x) \land c_0(y)) \end{array} \right| $$

L'interprétation *net* élimine les hyperarcs impliquant un sommet de couleur $c_0$ et l'interprétation *eq* effectue la fusion par $c_0$ sans pour autant modifier les autres hyperarcs (cela ne conserve pas en général les structures avec quotient). L'interprétation $\mathcal{I}^{\text{fusion}}$ ne dépend pas des hyperarcs impliquant des sommets de couleur $c_0$,

$$ \text{donc } \mathcal{I}^{\text{fusion}} \circ \text{net} = \mathcal{I}^{\text{fusion}}, \qquad (\text{A}) $$

$$ \text{et } \mathcal{I}^{\text{fusion}} \circ eq = eq \circ \mathcal{I}^{\text{fusion}}. \qquad (\text{B}) $$

On a aussi pour toute structure $S$ contenant un sommet de couleur $c_0$ les équivalences suivantes :

$$ \text{net}(S)|_E \approx S|_{E-\{c_0\}} \oplus \text{net}(S|_{\{c_0\}}), \qquad (\text{C}) $$

$$ \text{eq}(S)|_E = \text{eq}(S|_E), \qquad (\text{D}) $$

$$ \text{et } \text{eq}(\text{net}(S)|_{\{c_0\}}) \approx \text{sommet}[c_0]. \qquad (\text{E}) $$
Supposons $\mathcal{R}[E - \{c_0\}](S, S')$ où $S$ contient un sommet de couleur $c_0$. D'après les lemmes A.7 et A.5, il existe une application VR'-définissable $h$ telle que $\mathcal{R}[E - \{c_0\}](S \oplus \text{sommet}, h(S'))$ (F). On a alors :

$$
\begin{align*}
& \mathcal{I}_0(\text{fusion}[c_0](S))|_E \\
&= \left|
  \begin{array}{@{}l@{\quad}l@{}}
    \langle X, g, \phi > (\bar{X}) & : \quad \bar{g} \wedge \phi_{g,c_0} \\
    c(x) & : \quad c(x) \\
    x \sim y & : \quad x \sim y \\
    & \quad \lor \quad c_0(x) \wedge c_0(y)
  \end{array}
\right| (S)|_E \tag{lemme 4.22} \\
&= \operatorname{eq}(\mathcal{I}^{\text{fusion}}(\mathcal{I}_0(S))|_E) \tag{def eq et $\mathcal{I}^{\text{fusion}}$} \\
&= \operatorname{eq}(\mathcal{I}^{\text{fusion}}(\mathcal{I}_0(S))|_E) \tag{D} \\
&= \operatorname{eq}(\mathcal{I}^{\text{fusion}}(\mathcal{I}_0(S)|_E)) \tag{lemme 4.26} \\
&= \operatorname{eq}(\mathcal{I}^{\text{fusion}}(\operatorname{net}(\mathcal{I}_0(S)|_E))) \tag{A} \\
&\approx \operatorname{eq}(\mathcal{I}^{\text{fusion}}(\begin{array}{@{}l@{}}
    \operatorname{net}(\mathcal{I}_0(S)|_{E-\{c_0\}}) \\
    \oplus \operatorname{net}(\mathcal{I}_0(S)|_{\{c_0\}})))
  \end{array})) \tag{C} \\
&\approx \operatorname{eq}(\mathcal{I}^{\text{fusion}}(\begin{array}{@{}l@{}}
    \mathcal{I}_0(S)|_{E-\{c_0\}} \\
    \oplus \operatorname{net}(S|_{\{c_0\}}))
  \end{array})) \tag{F} \\
&\approx \mathcal{I}^{\text{fusion}}(\operatorname{eq}(\begin{array}{@{}l@{}}
    \mathcal{I}_0(S)|_{E-\{c_0\}} \\
    \oplus \operatorname{net}(S|_{\{c_0\}}))
  \end{array})) \tag{B} \\
&\approx \mathcal{I}^{\text{fusion}}(\begin{array}{@{}l@{}}
    \mathcal{I}_0(S)|_{E-\{c_0\}} \\
    \oplus \operatorname{eq}(\operatorname{net}(S|_{\{c_0\}}))
  \end{array})) \tag{C} \\
&\approx \mathcal{I}^{\text{fusion}}(\mathcal{I}'_0(h(S')) \oplus \text{sommet}[c_0]) \tag{E}
\end{align*}
$$

Donc $f^{\text{fusion}[c_0],E}(x) = \mathcal{I}^{\text{fusion}}(\mathcal{I}'_0(h(x)) \oplus \text{sommet}[c_0])$ satisfait les conclusions du lemme. $\square$

**Lemme A.9 (opérateur recol)** Soient $E \subseteq C$ et $\alpha$ une application de $C$ dans $C$. Il existe $E' \subseteq C$ tel que pour toute $\Sigma$-structure $S$ et pour toute $\Sigma'$-structure $S'$, on a continuement

$\text{si } \mathcal{R}[E'](S, S') \text{ alors } \mathcal{R}[E](\text{recol}[\alpha](S), \text{recol}[\alpha](\mathcal{I}'_0(S'))).$

**Preuve.** Preuve similaire à celle du lemme A.6. $\square$

<figure><img src="image_44.png" /></figure>
## A.3 Complément sur le théorème 26

### Preuve du lemme 4.37

**Preuve.** On pose $C' = C \times [k]$ et l'application $\beta$ est définie par $\beta((c, n)) = c$ pour toute couleur $c \in C$ et tout entier $n \in [k]$. Notons $\sigma$ l'application $\text{recol}[\beta]$. Le transducteur que l'on construit attribue les couleurs respectives $(c, 1), \dots, (c, n)$ aux sommets de couleur originale $c$ si ils sont en nombre inférieur à $k$ (le choix de leur numérotation étant arbitraire). Si ils sont en nombre supérieur à $k$, alors tous les sommets se voient attribuer (par convention) la couleur $(c, 1)$. Les transitions maintiennent ce codage.

Formellement, étant donné un graphe coloré $\mathcal{G}^{\infty}$, la relation $\mathcal{R}[\mathcal{G}^{\infty}](\mathcal{G}, \mathcal{H})$ pour $\mathcal{G}$ un graphe coloré par $C$ et $\mathcal{H}$ un graphe coloré par $C'$ est satisfaite si

$$ - \mathcal{G} \subseteq \mathcal{G}^{\infty}, $$

$$ - \mathcal{G} = \sigma(\mathcal{H}), $$

$$ - \text{ pour tout } c \in C, \text{ si } |\mathcal{G}^{\infty}|_c > k \text{ alors} $$

$$ - \text{ pour tout } i \in \{2, \dots, k\}, \ |\mathcal{H}|_{(c,i)} = 0, $$

$$ - \text{ pour tout } c \in C, \text{ si } |\mathcal{G}^{\infty}|_c \leq k, $$

$$ - \text{ pour tout } i \in \{1, \dots, |\mathcal{G}^{\infty}|_c\}, \ |\mathcal{H}|_{(c,i)} \leq 1, $$

$$ - \text{ pour tout } i \in \{|\mathcal{G}^{\infty}|_c + 1, \dots, k\}, \ |\mathcal{H}|_{(c,i)} = 0. $$

Si pour un graphe $\mathcal{G}$, on construit un graphe $\mathcal{H}$ tel que $\mathcal{R}[\mathcal{G}^{\infty}](\mathcal{G}, \mathcal{H})$, alors il satisfait (*) et $\mathcal{G} = \sigma(\mathcal{H})$ ce qui conclut ce lemme.

Les constructions sont alors les suivantes.

1. Pour toute couleur $c$,

$$ \mathcal{R}[\text{sommet}[c]](\text{sommet}[c], \text{sommet}[(c, 1)]). $$

2. Supposons $\mathcal{R}[\mathcal{G}_1^{\infty}](\sigma(\mathcal{H}_1), \mathcal{H}_1)$ et $\mathcal{R}[\mathcal{G}_2^{\infty}](\sigma(\mathcal{H}_2), \mathcal{H}_2)$. Alors,

$$ \begin{align*} \sigma(\mathcal{H}_1) \oplus \sigma(\mathcal{H}_2) &= \sigma(\text{recol}[\gamma_1](\mathcal{H}_1) \oplus \text{recol}[\gamma_2](\mathcal{H}_2)) \\ \text{avec } \gamma_1((c, n)) &= \begin{cases} (c, n) & \text{si } |\mathcal{G}_1^{\infty} \oplus \mathcal{G}_2^{\infty}|_c \le k, \\ (c, 1) & \text{sinon,} \end{cases} \\ \text{et } \gamma_2((c, n)) &= \begin{cases} (c, n + |\mathcal{G}_1^{\infty}|_c) & \text{si } |\mathcal{G}_1^{\infty} \oplus \mathcal{G}_2^{\infty}|_c \le k, \\ (c, 1) & \text{sinon.} \end{cases} \end{align*} $$
3. Soient $c_1$ et $c_2$ des couleurs de $C$ et supposons que $\mathcal{R}[\mathcal{G}^\infty](\sigma(\mathcal{H}), \mathcal{H})$. Alors

$$
\begin{align*}
\mathbf{recol}[c_1 \to c_2](\sigma(\mathcal{H})) &= \sigma(\mathbf{recol}[\gamma](\mathcal{H})) \\
\text{avec } \gamma((c_1, n)) &= \begin{cases} (c_2, 1) & \text{si } \|\|\mathbf{recol}[c_1 \to c_2](\mathcal{G}^\infty)\|\|_{c_2} > k, \\ (c_2, n) & \text{sinon,} \end{cases} \\
\gamma((c_2, n)) &= \begin{cases} (c_2, 1) & \text{si } \|\|\mathbf{recol}[c_1 \to c_2](\mathcal{G}^\infty)\|\|_{c_2} > k, \\ (c_2, n + |\mathcal{G}^\infty|_{c_1}) & \text{sinon,} \end{cases} \\
\gamma((c, n)) &= (c, n) \text{ si } c \notin \{c_1, c_2\}.
\end{align*}
$$

4. Soient $c_1$ et $c_2$ des couleurs de $C$ et supposons $\mathcal{R}[\mathcal{G}^\infty](\sigma(\mathcal{H}), \mathcal{H})$. Alors

$$
\mathrm{arc}[c_1, a, c_2](\sigma(\mathcal{H})) = \sigma(\mathrm{arc}[D](\mathcal{H})) \quad \text{avec } D = \{(c_1, i), a, (c_2, j) \mid i, j \in [k]\}.
$$

Ainsi, d'après le lemme 3.59, ces égalités peuvent être vues comme les transitions
d'un transducteur déterministe t satisfaisant les conclusions du lemme. $\square$

Récurrence

Les lemmes A.10, A.11, A.12, A.13 et A.14 correspondent aux transitions d'un
transducteur déterministe. Ces lemmes sont tous organisés de manière identique
et mettent en évidence leur lien avec le transducteur. Ainsi, leurs conclusions se
divisent explicitement en quatre catégories :

[v] assure la validité, c.a.d. que les hypothèses (A-C) ou (A-E) sont bien satis-
faites,

[a] assure que les différents cas peuvent être séparés par anticipation reconnais-
sable,

[d] garantit que la construction est bien HR-définissable,

[r] explicite l'étape de récurrence proprement dite.

Le premier lemme permet de se ramener de la relation $\mathcal{R}$ à la relation $\mathcal{R}'$. Les autres traitent un par un les opérateurs VR.

**Lemme A.10** Pour tout $\mathcal{G}_\infty$, $E$ et $D$ satisfaisant (A-C), il existe $E'$ et $D'$ et $f$
tels que :

[v] $\mathcal{G}^{\infty}$, $E'$ et $D'$ satisfont (A-E)

[a] $E'$, $D'$ et $f$ ne dépendent que de $E$, $D$ et $C_1(\mathcal{G}^\infty)$,

[d] $f$ est HR-définissable,

[r] et pour tout $\mathcal{G}$ et tout $\mathcal{H}$,

$$
\text{si } \mathcal{R}'[\mathcal{G}^{\infty}, E', D')(\mathcal{G}, \mathcal{H}) \text{ alors } \mathcal{R}[\mathcal{G}^{\infty}, E, D](\mathcal{G}, f(\mathcal{H})) .
$$
**Preuve.** Soit $C_1 = C_1(\mathcal{G}^\infty)$ et $C_+ = C_+(\mathcal{G}^\infty)$. Comme $\mathrm{arc}[D](\mathcal{G}^\infty)$ ne contient pas de graphe biparti complet de taille $k/2$ (d'après (C)), on en déduit que $D \cap D(C_+, C_+) = \emptyset$ (a).

Soient $D_0 = D \cap D(C_1 \cup E, C_1 \cup E)$, $D' = D - D_0$ et $E' = C(D') - C(\mathcal{G})$. Par construction et (a), $E'$, $D'$ et $\mathcal{G}^\infty$ satisfont (A-E).

Supposons $\mathcal{R}'[\mathcal{G}^\infty, E', D'](\mathcal{G}, \mathcal{H})$. Alors,

$$
\begin{align*}
\mathrm{arc}[D](\mathrm{sommet}[E] \oplus \mathcal{G}) & \\
&\approx \mathrm{arc}[D_0 \cup D'](\mathrm{fusion}[E \cup C_1](\mathrm{sommet}[E \cup C_1] \oplus \mathrm{sommet}[E'] \oplus \mathcal{G})) \\
&\qquad (\mathrm{car} \ C_1(\mathcal{G}) = C_1 \ \text{et} \ \text{(A)}) \\
& \\
&\approx \mathrm{fusion}[E \cup C_1](\mathrm{arc}[D_0](\mathrm{sommet}[E \cup C_1]) \oplus \mathrm{arc}[D'](\mathrm{sommet}[E'] \oplus \mathcal{G})) \\
&\qquad (\text{lemme 4.39 deux fois}) \\
& \\
&\approx \mathrm{fusion}[E \cup C_1](\mathrm{arc}[D_0](\mathrm{sommet}[E \cup C_1]) \oplus \mathcal{H}) \\
&\qquad (\mathrm{car} \ \mathcal{R}'[\mathcal{G}^\infty, E', D'](\mathcal{G}, \mathcal{H}))
\end{align*}
$$

Soit donc $\mathcal{H}_0 = \mathrm{arc}[D_0](\mathrm{sommet}[E \cup C_1])$, alors on a

$$
\mathcal{R}[\mathcal{G}^{\infty}, E, D](\mathcal{G}, \mathrm{fusion}[C_1](\mathcal{H}_0 \oplus \mathcal{H})) .
$$

□

**Lemme A.11** *Pour tout, E et D satisfaisant (A-E) et toute couleur $c \in C$, il existe un graphe fini $\mathcal{H}_0$ tel que*

[d] $\mathcal{H}_0$ est fini (et donc HR-définissable),

[r] et $\mathcal{R}'[\text{sommet}[c], E, D](\text{sommet}[c], \mathcal{H}_0)$ .

**Preuve.** Il suffit de prendre $\mathcal{H}_0 = \mathrm{arc}[D](\mathrm{sommet}[E \cup \{c\}])$. $\square$

□

**Lemme A.12** *Pour tout $\mathcal{G}^\infty$, $E$, $D$, $c$, $c'$ et a tels que $\mathrm{arc}[c, a, c'](\mathcal{G}^\infty)$, $E$, $D$ satisfont (A-E), il existe $D'$ et $f$ tels que*

[a] $D'$ et $f$ ne dépendent que de $D$, $c$, $c'$ et $a$,

[v] $\mathcal{G}^{\infty}, E', D'$ satisfont (A-C),

[d] $f$ est HR-définissable,

[r] pour tout graphes $\mathcal{G}$ et $\mathcal{H}$, on a continuement

$$
\begin{array}{ll}
\text{si} & \mathcal{R}[\mathcal{G}^{\infty}, E', D'](\mathcal{G}, \mathcal{H}) \\
& \text{alors } \mathcal{R}'[\mathrm{arc}[c, a, c'](\mathcal{G}^{\infty}), E, D](\mathrm{arc}[c, a, c'](\mathcal{G}), f(\mathcal{H})) .
\end{array}
$$
**Preuve.** Soit, pour $i \in [2]$, $C_1^i = C_1(\mathcal{G}_i^\infty) = C_1(\mathcal{G}_i)$ et $C^i = C(\mathcal{G}_i^\infty) = C(\mathcal{G}_i)$. On peut supposer (ce qui est le cas après normalisation pour $k > 2$) que $C_1^1 \cap C^2 = \emptyset$ et $C_1^2 \cap C^1 = \emptyset$.

*Idée:* L'intention est alors de poser $E_1 = E \cup C^2$, $E_2 = E \cup C^1$ et $D = D_1 = D_2$ ce qui ne satisfait pas l'hypothèse (A). Supposons néanmoins que $\mathcal{R}[\mathcal{G}_1^\infty, E_1, D_1](\mathcal{G}_1, \mathcal{H}_1)$ et $\mathcal{R}[\mathcal{G}_2^\infty, E_2, D_2](\mathcal{G}_2, \mathcal{H}_2)$ sauf en ce qui concerne l'hypothèse (A). On a alors,

$$
\begin{align*}
& \mathrm{arc}[D](\mathrm{sommet}[E] \oplus \mathcal{G}_1 \oplus \mathcal{G}_2) \\
& \approx \mathrm{arc}[D](\mathrm{fusion}[E \cup C^1 \cup C^2]((\mathrm{sommet}[E \cup C^2] \oplus \mathcal{G}_1) \oplus (\mathrm{sommet}[E \cup C^1] \oplus \mathcal{G}_2))) \\
& \approx \mathrm{fusion}[E \cup C^1 \cup C^2](\mathrm{arc}[D]((\mathrm{sommet}[E \cup C^2] \oplus \mathcal{G}_1) \oplus (\mathrm{sommet}[E \cup C^1] \oplus \mathcal{G}_2))) \\
& \approx \mathrm{fusion}[E \cup C^1 \cup C^2](\begin{array}{@{}c@{}} \mathrm{arc}[D](\mathrm{sommet}[E \cup C^2] \oplus \mathcal{G}_1) \\ \oplus \mathrm{arc}[D](\mathrm{sommet}[E \cup C^1] \oplus \mathcal{G}_2) \end{array}) \tag{lemme 4.40} \\
& \approx \mathrm{fusion}[E \cup C^1 \cup C^2](\mathcal{H}_1 \oplus \mathcal{H}_2) \\
& \quad (\mathrm{car} \ \mathcal{R}[\mathcal{G}_1^\infty, E_1, D_1](\mathcal{G}_1, \mathcal{H}_1) \text{ et } \mathcal{R}[\mathcal{G}_2^\infty, E_2, D_2](\mathcal{G}_2, \mathcal{H}_2))
\end{align*}
$$

Donc $f(\mathcal{H}_1, \mathcal{H}_2) = \text{fusion}[E \cup C^1 \cup C^2](\mathcal{H}_1 \oplus \mathcal{H}_2)$ conviendrait.

Il manque l'hypothèse (A). La solution complète combine donc cette technique avec une duplication de $C^1$ et $C^2$ afin de les rendre disjoints de $C$. L'opération de recoloriage permet alors d'obtenir la même équivalence. $\square$
# Index

## – Symboles –

<table><tbody><tr><td>μ-définissabilité</td><td>68</td></tr><tr><td>E<sub>⊥</sub> (cpo pointé)</td><td>49</td></tr><tr><td>Δ<sub>1</sub> (demi-droite infinie)</td><td>11</td></tr><tr><td>Δ<sub>2</sub> (arbre binaire complet)</td><td>12</td></tr><tr><td>|R| (arité de R)</td><td>9</td></tr><tr><td>|f| (arité de f)</td><td>13</td></tr><tr><td>←t</td><td>85</td></tr><tr><td>⊥ (plus petit élément cpo)</td><td>48</td></tr><tr><td>→<sub>w</sub><sup>g</sup> (étiquettes chemin)</td><td>11</td></tr><tr><td>t↓<sub>n</sub> (coupure profondeur n)</td><td>53</td></tr><tr><td>~</td><td>9</td></tr><tr><td>→<sub>a</sub><sup>g</sup> (arc étiqueté par a)</td><td>10</td></tr><tr><td>≈ (isomorphe)</td><td>9</td></tr><tr><td>|= (modèle)</td><td>16</td></tr><tr><td>[[]] (morphisme canonique)</td><td>55</td></tr><tr><td>□ (produit asynchrone)</td><td>32</td></tr><tr><td>⊗<sub>g</sub> (produit généralisé)</td><td>32</td></tr><tr><td>⊗ (produit synchrone)</td><td>31</td></tr><tr><td>→<sub>Δ</sub></td><td>152</td></tr><tr><td>→<sub>Δ</sub><sup>*</sup></td><td>152</td></tr><tr><td>□ (borne supérieure)</td><td>48</td></tr><tr><td>S<sub>l~</sub></td><td>10</td></tr><tr><td>⊕ (union disjointe)</td><td>29, 97, 104</td></tr><tr><td>t<sup>v</sup></td><td>14</td></tr><tr><td>⊥ (plus grand élément treillis)</td><td>64</td></tr><tr><td>Ø (plus petit élément treillis)</td><td>64</td></tr><tr><td>Auto<sub>dd</sub><sup>T</sup></td><td>131</td></tr><tr><td>Auto<sub>d</sub></td><td>90</td></tr><tr><td>Auto<sup>T</sup></td><td>131</td></tr><tr><td>LB(t) (langage des branches)</td><td>13</td></tr><tr><td>Cl(φ)</td><td>65</td></tr><tr><td>dest</td><td>10</td></tr></tbody></table>

<table><tbody><tr><td>d, d<sup>+</sup>, d<sup>-</sup> (degrés)</td><td>10</td></tr><tr><td>final</td><td>11</td></tr><tr><td>fix (plus petit point fixe)</td><td>50</td></tr><tr><td>FV (variables libres)</td><td>16, 63</td></tr><tr><td>HR</td><td>96</td></tr><tr><td>LA (largeur arborescente)</td><td>42</td></tr><tr><td>L (langage accepté)</td><td>11</td></tr><tr><td>L<sub>I,F</sub> (trace)</td><td>11</td></tr><tr><td>orig</td><td>10</td></tr><tr><td>R<sup>S</sup> (interprétation de R)</td><td>9</td></tr><tr><td>racine</td><td>11</td></tr><tr><td>sem[A](f) (sémantique de f dans A)</td><td>54</td></tr><tr><td>Solution[A](S) (solution de S)</td><td>56</td></tr><tr><td>sommet</td><td>104</td></tr><tr><td>T<sub>⊥</sub><sup>ω</sup>(F) (cpo termes infinis)</td><td>53</td></tr><tr><td>T<sub>⊥</sub><sup>ω</sup>(F) (termes infinis)</td><td>13</td></tr><tr><td>T(F) (termes finis)</td><td>13</td></tr><tr><td>U<sub>S</sub> (univers de S)</td><td>9</td></tr><tr><td>V<sub>G</sub> (sommets de G)</td><td>10</td></tr><tr><td>VR'</td><td>105</td></tr><tr><td>VRA</td><td>155</td></tr><tr><td>VRS'</td><td>135</td></tr><tr><td>VR</td><td>103</td></tr><tr><td>arc</td><td>104</td></tr><tr><td>fusion</td><td>97</td></tr><tr><td>recol</td><td>97, 104</td></tr></tbody></table>

## – A –

<table><tbody><tr><td>accessibilité</td><td></td></tr><tr><td>rationnelle</td><td>18</td></tr><tr><td>additivité</td><td>61</td></tr><tr><td>ajout fini</td><td>26</td></tr><tr><td>algèbre</td><td>54</td></tr></tbody></table>
<table><tr><td>continue</td><td>55</td></tr><tr><td>continue sortée</td><td>57</td></tr><tr><td>libre</td><td>54</td></tr><tr><td>alphabet gradué</td><td>13</td></tr><tr><td>arbre</td><td>12</td></tr><tr><td>binaire complet</td><td>12</td></tr><tr><td>arc</td><td>10</td></tr><tr><td>arité</td><td>9, 13</td></tr><tr><td>automate</td><td>11</td></tr><tr><td>automate d'arbre</td><td>130</td></tr><tr><td>complet</td><td>130</td></tr><tr><td>déterministe ascendant</td><td>130</td></tr><tr><td>déterministe descendant</td><td>131</td></tr></table>

### – B –

<table><tr><td>borne inférieure</td><td>60</td></tr><tr><td>borne supérieure</td><td>48, 60</td></tr><tr><td>boucle</td><td>10</td></tr><tr><td>branche</td><td>12</td></tr></table>

### – C –

<table><tr><td>μ-calcul</td><td>63</td></tr><tr><td>chaîne ascendante</td><td>48</td></tr><tr><td>chemin</td><td>10</td></tr><tr><td>conjonction linéaire</td><td>106</td></tr><tr><td>continuité</td><td>50</td></tr><tr><td>couleur</td><td>96</td></tr><tr><td>cpo</td><td>48</td></tr><tr><td>des applications</td><td>49</td></tr><tr><td>des graphes</td><td>53</td></tr><tr><td>des langages</td><td>52</td></tr><tr><td>des parties</td><td>49</td></tr><tr><td>des structures</td><td>52</td></tr><tr><td>des structures avec quotient</td><td>53</td></tr><tr><td>des termes infinis</td><td>53</td></tr><tr><td>fini</td><td>49</td></tr><tr><td>pointé</td><td>49</td></tr><tr><td>produit</td><td>49</td></tr><tr><td>croissante</td><td>61</td></tr></table>

### – D –

<table><tr><td>degré</td><td>10</td></tr></table>

<table><tr><td>demi-droite des entiers</td><td>11</td></tr><tr><td>destination</td><td>10</td></tr></table>

### – E –

<table><tr><td>élimination des sommets isolés</td><td>28</td></tr><tr><td>équation</td><td>56</td></tr><tr><td>escabeau</td><td>11</td></tr><tr><td>étiquette</td><td>10</td></tr><tr><td>expression</td><td></td></tr><tr><td>booléenne</td><td>17</td></tr><tr><td>booléenne positive</td><td>17</td></tr></table>

### – F –

<table><tr><td>feuille</td><td>12</td></tr><tr><td>formule</td><td></td></tr><tr><td>booléenne</td><td>17</td></tr><tr><td>booléenne positive</td><td>17</td></tr><tr><td>close</td><td>16, 63</td></tr><tr><td>du premier ordre</td><td>15</td></tr><tr><td>en forme linéaire [complète]</td><td>106</td></tr><tr><td>existentielle</td><td>17</td></tr><tr><td>monadique</td><td>17</td></tr><tr><td>fusion</td><td>97</td></tr></table>

### – G –

<table><tr><td>graphe</td><td>10</td></tr><tr><td>HR-équationel</td><td>97</td></tr><tr><td>VR-équationnel</td><td>104</td></tr><tr><td>biparti complet</td><td>45</td></tr><tr><td>co-déterministe</td><td>10</td></tr><tr><td>coloré</td><td>96</td></tr><tr><td>déterministe</td><td>10</td></tr><tr><td>de largeur arborescente bornée</td><td>44</td></tr><tr><td>de récriture suffixe</td><td>154</td></tr><tr><td>enraciné</td><td>11</td></tr><tr><td>préfixe</td><td>91</td></tr><tr><td>préfixe reconnaissable</td><td>116</td></tr><tr><td>uniformément creux</td><td>44</td></tr></table>

### – H –

<table><tr><td>hyperarc</td><td>9</td></tr><tr><td>hypergraphe</td><td>8</td></tr></table>
### - I -

<table><tr><td>inévitable</td><td>190</td></tr><tr><td>interprétation</td><td>9, 26</td></tr><tr><td>monadique des parties finies</td><td>142</td></tr><tr><td>isomorphisme</td><td></td></tr><tr><td>de structure avec quotient</td><td>9</td></tr></table>

### - J -

<table><tr><td>jeu du voleur et des policiers</td><td>42</td></tr></table>

### - L -

<table><tr><td>langage</td><td></td></tr><tr><td>accepté par un automate</td><td>11</td></tr><tr><td>de mots</td><td>52</td></tr><tr><td>de termes</td><td>52</td></tr><tr><td>des branches</td><td>13</td></tr><tr><td>rationnel (de termes)</td><td>130</td></tr><tr><td>reconnaissable (de termes)</td><td>130</td></tr><tr><td>largeur arborescente</td><td>42</td></tr><tr><td>largeur de clique</td><td>172</td></tr><tr><td>limite</td><td>48</td></tr><tr><td>logique</td><td></td></tr><tr><td>du premier ordre</td><td>15</td></tr><tr><td>du second-ordre gardée</td><td>20</td></tr><tr><td>monadique</td><td>17</td></tr></table>

### - M -

<table><tr><td>marquage rationnel</td><td>28</td></tr><tr><td>modèle</td><td>16</td></tr><tr><td>modification finie</td><td>26</td></tr><tr><td>morphisme</td><td></td></tr><tr><td>canonique</td><td>55</td></tr><tr><td>d'algèbre</td><td>54</td></tr><tr><td>d'algèbre continue</td><td>55</td></tr><tr><td>inverse</td><td>28</td></tr><tr><td>multiplicativité</td><td>61</td></tr></table>

### - N -

<table><tr><td>nœud</td><td>12</td></tr></table>

### - O -

<table><tr><td>opérateur</td><td>54</td></tr><tr><td>ordre partiel complet</td><td>48</td></tr></table>

<table><tr><td>origine</td><td>10</td></tr></table>

### - P -

<table><tr><td>père</td><td>12</td></tr><tr><td>point fixe</td><td>61</td></tr><tr><td>(plus petit) point fixe</td><td>50</td></tr><tr><td>présentation</td><td></td></tr><tr><td>automatique</td><td>149</td></tr><tr><td>terme-automatique</td><td>134</td></tr><tr><td>produit</td><td></td></tr><tr><td>asynchrone</td><td>32</td></tr><tr><td>généralisé</td><td>32</td></tr><tr><td>synchrone</td><td>31</td></tr><tr><td>projection</td><td>51</td></tr></table>

### - R -

<table><tr><td>racine</td><td>11</td></tr><tr><td>recoloriage</td><td>97</td></tr><tr><td>récriture suffixe</td><td>152</td></tr><tr><td>relation</td><td></td></tr><tr><td>continue</td><td>84</td></tr><tr><td>PR</td><td>119</td></tr><tr><td>terme-synchronisée</td><td>133</td></tr><tr><td>renommage</td><td>27</td></tr><tr><td>restriction</td><td></td></tr><tr><td>par accessibilité</td><td>28</td></tr><tr><td>rationnelle</td><td>28</td></tr></table>

### - S -

<table><tr><td>satisfaction</td><td>16</td></tr><tr><td>sémantique</td><td>54</td></tr><tr><td>signature</td><td>9</td></tr><tr><td>solution (système d'équations)</td><td>56</td></tr><tr><td>sommet</td><td>10</td></tr><tr><td>accessible</td><td>11</td></tr><tr><td>final</td><td>11</td></tr><tr><td>principal</td><td>13</td></tr><tr><td>sous-terme</td><td>14</td></tr><tr><td>structure</td><td>9</td></tr><tr><td>HR-équationnelle</td><td>97</td></tr><tr><td>avec quotient</td><td>9</td></tr><tr><td>colorée</td><td>96</td></tr></table>
<table><tr><td>quotient</td><td>10</td></tr><tr><td>substitution</td><td></td></tr><tr><td>finie inverse</td><td>28</td></tr><tr><td>rationnelle inverse</td><td>28</td></tr><tr><td>symbole</td><td></td></tr><tr><td>fonctionnel</td><td>13</td></tr><tr><td>relationnel</td><td>9</td></tr><tr><td>système d'équations</td><td>56</td></tr><tr><td>normalisé</td><td>57</td></tr></table>

### – T –

<table><tr><td>terme, F-terme</td><td>13</td></tr><tr><td>théorie</td><td></td></tr><tr><td>au premier ordre</td><td>16</td></tr><tr><td>trace (d'un graphe)</td><td>11</td></tr><tr><td>transducteur déterministe</td><td>72</td></tr><tr><td>transduction monadique</td><td>35</td></tr><tr><td>treillis complet</td><td>60</td></tr></table>

### – U –

<table><tr><td>union disjointe</td><td>29</td></tr><tr><td>union disjointe explicite</td><td>30</td></tr></table>

### – V –

<table><tr><td>valeur</td><td>55</td></tr><tr><td>valuation</td><td>16, 56, 64</td></tr><tr><td>variable</td><td></td></tr><tr><td>(du second ordre) monadique</td><td>17</td></tr><tr><td>du μ-calcul</td><td>63</td></tr><tr><td>du premier ordre</td><td>15</td></tr><tr><td>libre</td><td>16</td></tr></table>
<figure><img src="image_45.png" /></figure>
<figure><img src="image_46.png" /></figure>
Résumé

Ce travail est dédié à l'étude de structures et de graphes infinis admettant une représentation finie, aux équivalences entre ces représentations et aux propriétés géométriques et de décidabilité les concernant. En suivant l'approche de Courcelle, nous nous attachons à leur définition en terme de solution de systèmes d'équations.

Nous introduisons tout d'abord la notion de transducteur déterministe (descendant avec anticipation de termes infinis). Cet outil permet de manipuler des systèmes infinis d'équations, et en cela, son usage permet d'étendre nombre de résultats connus antérieurement, établis dans le cas de systèmes finis.

Nous étudions ensuite les familles de structures à base de pile en nous concentrons sur les structures préfixes reconnaissables. Nous établissons diverses équivalences de représentations et étudions la restriction à une largeur arborescente bornée. Nous considérons enfin l'ajout d'un opérateur supplémentaire de fusion aux systèmes d'équations.

La contribution suivante concerne les structures terme-automatiques. Nous montrons qu'elles admettent aussi diverses représentations équivalentes.

Pour finir, nous étudions les graphes décrits par récriture suffixe de termes et montrons diverses équivalences de représentations les concernant. Nous finissons par l'étude de ces graphes quand restreints à une largeur arborescente ou une largeur de clique bornée.

Summary

This work is dedicated to the study of infinite structures and graphs which admit a finite representation, to their geometrical properties as well as decidability properties concerning them. Following Courcelle's work, we focus our study on their representation as solution of equational systems.

We first introduce deterministic transducers (top-down with lookahead for infinite trees). This tool allows us to deal with infinite equational systems, thus extending some previous results, originally stated for finite equational systems.

We then study the stack based families of structures and concentrate ourselves on prefix recognizable ones. We establish various equivalent representations for them, and study their restriction to bounded tree-width. We finally consider the enrichment of those equational systems by an extra operator of fusion.

We then study structures admitting term-automatic presentations. We show once more that those structures admit various equivalent representations.

Finally, we study the family of graphs definable by ground term rewriting and establish some equivalences of representations. We conclude by a study of the nature of those graphs when restricted to bounded tree or clique width.