Si dans ces équations, on ne garde que celles pour lesquelles $E = \phi[\gamma]$ (elles sont en nombre fini), en appliquant le corollaire 3.8 et l'hypothèse de récurrence, on obtient

$$t_q^{-1}(\phi[\gamma]) = (\nu y[q].\{y[q] = F(q, \phi) \mid q \in Q\})[\gamma].$$

□

**Corollaire 3.49** Le domaine de définition d'un transducteur déterministe est $\mu$-définissable.

**Remarque 3.50** L'image directe ne se comporte pas aussi bien que l'image inverse. En particulier, l'image directe d'un ensemble $\mu$-définissable n'est pas nécessairement $\mu$-définissable. Considérons par exemple sur l'alphabet $\mathcal{F} = \{f : 2, a : 1, c : 0\}$ le transducteur déterministe $(\mathcal{F}, \mathcal{F}', \{q\}, q, \{q(a(x)) \to f(q(x), q(x)), q(c) \to c\})$. Ce transducteur déterministe transforme les termes de la forme $a^n(c)$ en arbres équilibrés sur $f$ et $c$ de hauteur $n$. Ainsi, l'image de ce transducteur est l'ensemble des termes équilibrés sur $f$ et $c$, et cet ensemble n'est pas $\mu$-définissable. En empruntant la terminologie de la récriture et des transducteurs finis, ceci provient du fait que les règles définissant les transducteurs sont linéaires à gauche, mais pas nécessairement à droite.

**Propriété 3.51** Les transducteurs déterministes sont clos par composition.

**Preuve.** Considérons deux transducteurs déterministes $\mathbf{t} = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$ et $\mathbf{t}' = (\mathcal{F}', \mathcal{F}'', Q', q'_{init}, \delta')$.

Comme habituellement, il s'agit de construire une forme d'automate produit. L'ensemble des états du nouveau transducteur déterministe est donc $Q \times Q'$. A partir d'un état $(q, q')$, les transitions se déroulent comme suit. Si une transition de production peut être effectuée depuis l'état $q'$ par $\mathbf{t}'$, alors elle est effectuée par l'automate produit. Lorsque de l'état $q'$ peut être effectuée une anticipation de $L$ dans $\mathbf{t}'$, une anticipation similaire est effectuée, mais cette fois-ci avec le langage $\mathbf{t}_q^{-1}(L)$. Lorsque $q$ est un état de production de $\mathbf{t}$ et $q'$ un état de consommation de $\mathbf{t}'$, et que le même symbole est à la fois produit et consommé, alors les deux transitions sont effectuées simultanément : le nouveau transducteur déterministe effectue une transition à vide. Dans les autres cas, c'est la transition issue de $q$ qui est choisie.
On a donc $\mathbf{t}'' = (\mathcal{F}, \mathcal{F}'', Q \times Q', (q_{init}, q'_{init}), \delta'')$ avec $\delta''$ défini par :

$$
\begin{align*}
\delta'' &= \{(q, q')(x) \to f((q, q'_{1})(x), \dots, (q, q'_{|f|})(x)) \mid q'(x) \to f(q'_{1}(x), \dots, q'_{|f|}(x))\} \\
&\cup \{(q, q')(x \in \mathbf{t}_{q}^{-1}(L)) \to (q, r')(x) \mid q'(x \in L) \to r'(x) \in \delta'\} \\
&\cup \{(q, q')(f(x_{1}, \dots, x_{|f|})) \to (r, q')(x_{i}) \mid \begin{array}{@{}l@{}} q(f(x_{1}, \dots, x_{|f|})) \to r(x_{i}) \in \delta \\ \text{et } q' \text{ état de consommation} \end{array} \\
&\cup \{(q, q')(x \in L) \to (r, q')(x) \mid \begin{array}{@{}l@{}} q(x \in L) \to r(x) \in \delta \\ \text{et } q' \text{ état de consommation} \end{array} \\
&\cup \{(q, q')(x) \to (q_{i}, r')(x) \mid \begin{array}{@{}l@{}} q(x) \to f(q_{1}(x), \dots, q_{|f|}(x)) \in \delta \\ \text{et } q'(f(x_{1}, \dots, x_{|f|})) \to r'(x_{i}) \in \delta' \end{array} \}
\end{align*}
$$

On montre maintenant par récurrence sur l'entier $n$ que pour tout $\mathcal{F}$-terme $t$, et tous états $q \in Q$ et $q' \in Q'$, il existe un entier $k$ tel que :

1. si $\delta'_n(q', \mathbf{t}_q(t))$ n'est pas défini, alors $\delta''_k((q, q'), t)$ n'est pas défini,

2. sinon $\delta''_n((q, q'), t) \subseteq \delta'_n(q', \mathbf{t}_q(t)) \subseteq \delta''_k((q, q'), t)$.

□

### 3.4.4 Lien avec les systèmes d'équations

La propriété suivante permet de se servir des transducteurs déterministes comme d'un outil pour manipuler les systèmes d'équations.

**Théorème 11 (Colcombet et Löding [CL04])** *Pour tous alphabets gradués $\mathcal{F}$ et $\mathcal{F}'$ et tout transducteur déterministe $\mathbf{t}$ de $\mathcal{T}^\omega(\mathcal{F})$ dans $\mathcal{T}^\omega(\mathcal{F}')$, il existe effectivement une transduction monadique $\mathbf{t}^*$ qui à chaque $\mathcal{F}$-système d'équations $S$ associe un $\mathcal{F}'$-système d'équations $\mathbf{t}^*(S)$, tel que,*

$$ \mathbf{t}(\text{Depliage}(S)) = \text{Depliage}(\mathbf{t}^*(S)). $$

**Preuve.** Considérons un transducteur déterministe $\mathbf{t} = (\mathcal{F}, \mathcal{F}', Q, q_{init}, \delta)$ dont l'image ne contient pas le symbole $\perp$. La construction s'effectue en deux temps. Dans le premier temps, on utilise un nouvel opérateur unaire $i$ dont la sémantique est pour tout $e, i(e) = e$, c.a.d. l'identité. La deuxième étape consiste à éliminer ces opérateurs $i$.

Commençons par définir une transduction monadique $\mathbf{t}' T = (\delta, N, \phi, \psi)$.

*Domaine de $\mathbf{t}^*$:* la transduction $\mathbf{t}'$ est effectuée si $S \models \delta$ avec $\delta = \phi_D^*\{\text{racine}/y\}$ où $\phi_D$ représente le domaine de $\mathbf{t}$ sous forme d'une formule du $\mu$-calcul, et $\phi_D^*$ la formule monadique équivalente obtenue par le théorème 9.

*Ensemble de sommets de $\mathbf{t}'$:* c'est $N \times V_S$ avec $N = Q \times \{0, 1\}$. On pose donc pour tout $(q, n) \in N, \phi_{q,n} = \text{vrai}$.
pour $f \in \mathcal{F}'$,

$$
\begin{align*}
\psi_{g,(r,n),(r',n')}(x,y) &= \begin{cases}
x=y & \text{si } r=r', n=0, n'=1 \\
& \text{et } r(z) \to g(q_1(z), \dots, q_{|g|}), \\
\text{faux} & \text{sinon.}
\end{cases} \\
\psi_{i,(r,n),(r',n')}(x,y) &= \begin{cases}
x=y & \text{si } r=r', n=0, n'=1 \\
& \text{et } r \text{ est un état de production ou d'anticipation} \\
\text{faux} & \text{sinon.}
\end{cases}
\end{align*}
$$

pour $k \in \mathbb{N}$,

$$
\psi_{k,(r,n),(r',n')}(x,y) =
\begin{cases}
x=y & \begin{array}{l} \text{si } r(z) \to g(q_1(z), \dots, q_{|g|}(z)), \\ n=1, n'=0, k \in [|g|], r'=q_k, \end{array} \\
\exists x'. \quad x \xrightarrow{f} x' & \text{si } r(f(z_1, \dots, z_{|f|})) \to r'(z_i), \\
\wedge \quad x' \xrightarrow{i} y & n=1, n'=0, \\
x=y \wedge \Phi_L(x) & \begin{array}{l} \text{si } r(z \in L) \to r'(z), \\ n=1, n'=0, \end{array} \\
\text{faux} & \text{sinon.}
\end{cases}
$$

<caption>FIG. 3.2 – *Constructions de la transduction t' du théorème 11.*</caption>

Racine de **t**: c'est (racine<sup>S</sup>, q<sub>init</sub>), et on pose

$$
\psi_{\text{racine}, (q,n)}(x) = \begin{cases} \text{racine}(x) & \text{si } q = q_{\text{init}}, \\ \text{faux} & \text{sinon.} \end{cases}
$$

Relations de t': elles sont définies informellement par.

- si $q(x) \to f(q_1(x), \dots, q_{|f|}(x)) \in \delta$, alors pour tout sommet $v$ de $V_S$, l'hyperarc $(v, q) = f((q_1, v), \dots, (q_{|v|}, v))$ est ajouté,

- si $q(x \in L) \to r(x) \in \delta$, alors pour tout sommet $v$ de $V_S$ tel que $S, v \models \Phi$, l'hyperarc $(q, v) = i((r, v))$ est ajouté, où $\Phi$ est la formule monadique obtenue de $L$ par le théorème 10 page 71,

- si $q(f(x_1, \dots, x_n)) \to r(x_i) \in \delta$, alors pour tout hyperarc $v = f(v_1, \dots, v_{|f|})$ de $S$, l'hyperarc $(q, v) = i((r, v_i))$ est ajouté.
Formellement, cela correspond aux expressions présentées à la figure 3.2

On vérifie d'abord que le graphe obtenu par cette transduction suivie d'une restriction aux sommets accessibles est bien un système d'équations. En particulier, il y a exactement un opérateur d'après l'hypothèse de normalisation.

On montre alors par récurrence sur $n$ que pour tout état $q$ et tout sommet $v$,

$$ \delta_n(q, \text{Depliage}(S, v)) \subseteq \bar{i}(\text{Depliage}(\mathbf{t}'(S), (q, v))), \quad (3.11) $$

où $\bar{i}(t)$ représente le terme $t$ dans lequel les occurrences du symbole $i$ ont été éliminées.

La deuxième étape consiste à éliminer les symboles $i$. Pour celà, on utilise la formule de logique monadique accessibilité$[(i1)^*f](x, y)$ qui teste s'il existe un chemin étiqueté par un mot du langage $(i1)^*f$ entre le sommet $x$ et le sommet $y$. On applique alors l'interprétation monadique :

$$ \mathcal{I} = \left| \begin{array}{ll} \text{racine}(x) : & \text{racine}(x) \\ x \xrightarrow{f} y & : \text{accessibilite}[(i1)^*f](x, y), \quad f \in \mathcal{F}' \\ x \xrightarrow{n} y & : x \xrightarrow{n} y, \quad n \in \mathbb{N} \end{array} \right| $$

On a alors la propriété pour tout $\mathcal{F}'$-système d'équations $S$

$$ \text{Depliage}(\mathcal{I}(S)) = \bar{i}(\text{Depliage}(\mathbf{t}'(S))). $$

Combiné avec l'équation (3.11), on obtient que pout tout $\mathcal{F}$-système d'équations,

$$ \text{Depliage}((\mathcal{I} \circ \mathbf{t}')(S)) = \mathbf{t}(\text{Depliage}(S)). $$

On pose donc $\mathbf{t}^* = \mathcal{I} \circ \mathbf{t}'$

□

**Remarque 3.52** Une certaine forme de réciproque à ce théorème est aussi vraie (cf. [CL04]): si une transduction monadique $T$ entre systèmes d'équations est telle que pour tout systèmes d'équations $S$ et $S'$,

$$ \text{Depliage}(S) = \text{Depliage}(S') \Rightarrow \text{Depliage}(T(S)) = \text{Depliage}(T(S')), $$

et si de plus $T$ satisfait une certaine contrainte technique d'uniformité<fnref n="10" /> alors il existe un transducteur $\mathbf{t}$ tel que $\mathbf{t} \circ \text{Depliage} = \text{Depliage} \circ T$.

<footnote n="10">10. Qui informellement stipule que seul le sommet *racine* du système d'équations résultat dépend de la position de la *racine* dans le premier système d'équations.</footnote>
### 3.4.5 Utilisation des transducteurs déterministes

L'objectif est de disposer d'un lemme permettant d'établir des relations entre algèbres au moyen de transducteurs déterministes. On présente tout d'abord la notion de relation continue. Quelques considérations techniques sur l'arbre d'exécution d'un transducteur sont ensuite énoncées. Enfin, nous pourrons énoncer le résultat de correction (lemme 3.59).

#### Relations continues

Les transducteurs déterministes permettent de transformer des termes en termes. Il s'agit ici d'utiliser cet outil pour passer d'un cpo quelconque à un autre. Dans l'approche classique des transducteurs déterministes, c'est-à-dire quand ils servent à manipuler des termes finis, ceci correspond simplement à associer des invariants à chaque règle. Le principe de récurrence permet alors de conclure. L'exemple 3.53 montre (comme on peut s'y attendre) que ceci n'est plus suffisant en présence de termes infinis. Les relations continues présentées ici apportent un début de réponse à ce problème.

**Exemple 3.53** Considérons le transducteur déterministe $t$ reliant les $N$-termes aux $N$-termes suivant (pour simplifier on ne considère pas les symboles $\infty$ et $*$), possédant deux états $q_{+1}$ (initial) et $q_{id}$ :

$$ 
\begin{array}{l@{\quad}l}
q_{+1}(t+t') & \rightarrow q_{+1}(t) + q_{id}(t') , & q_{id}(t+t') \rightarrow q_{id}(t) + q_{id}(t') , \\
q_{+1}(0) & \rightarrow 1 , & q_{id}(0) \rightarrow 0 , \\
q_{+1}(1) & \rightarrow 1+1 , & q_{id}(1) \rightarrow 1 .
\end{array}
$$

On peut légitimement s'attendre à avoir la propriété $[[t(t)]] = [[t]] + 1$ ($*$). En effet, les invariants suivants sont vérifiés (ils correspondent syntaxiquement aux transitions associées à l'état $q_{+1}$) :

$$ 
\begin{array}{l}
(n + n') + 1 = (n + 1) + n' , \\
0 + 1 = 1 , \\
1 + 1 = 1 + 1 .
\end{array}
$$

La propriété ($*$) est effectivement vérifiée pour tous les termes finis : une simple récurrence suffit. En revanche, si l'on considère le terme infinité solution de l'équation $t = t + 0$, il satisfait $t(t) = t$, et donc $[[t]] + 1 = 1 \neq [[t(t)]]$. Ainsi, ($*$) n'est pas satisfaite.

Le propos de ce paragraphe est de dégager des conditions suffisantes pour assurer la correction de ce type de raisonnement. Le lemme 3.59 concrétise cette approche.

Dans le cas général, prouver qu'un transducteur déterministe $t$ effectue bien la tâche souhaitée s'exprime comme $R([[t]], [[t(t)]])$ pour tout terme $t$ tel que $t(t)$
est défini, où $\mathcal{R}$ est un relation fixée. En particulier, on ne peut pas se limiter aux relations de la forme $[[t(t)]] = f([t])$ pour une certaine fonction $f$: établir l'isomorphisme de graphes est un exemple de propriété dépassant ce cadre. Il s'agit donc tout d'abord de préciser quel type de relations il est légitime de considérer, et en particulier les hypothèses de continuité qui les concernent.

Soient trois cpos $E_1, E_2$ et $\mathcal{R}$ et deux applications $\rho_1$ et $\rho_2$ de respectivement $\mathcal{R}$ dans $E_1$ et $\mathcal{R}$ dans $E_2$. On dit que $(\mathcal{R}, \rho_1, \rho_2)$ (ou simplement $\mathcal{R}$ quand il n'y a pas d'ambiguïté) relie continuement $E_1$ et $E_2$ si $\rho_1$ et $\rho_2$ sont continues. Pour $\mathcal{R}$ un élément de $\mathcal{R}$, $e_1$ et $e_2$ des éléments de respectivement $E_1$ et $E_2$, on note $R(e_1, e_2) \in \mathcal{R}$ si $e_1 = \rho_1(\mathcal{R})$ et $e_2 = \rho_2(\mathcal{R})$ et qu'il n'y a pas d'ambiguïté sur $\rho_1$ et $\rho_2$. On écrit $\mathcal{R}(e_1, e_2)$ s'il existe $R \in \mathcal{R}$ tel que $R(e_1, e_2)$.

Les propriétés de 3.54 à 3.58 énoncent les constructions qui permettent, par combinaison, d'obtenir toutes les relations continues du reste de ce travail. La première de ces propriétés concerne l'isomorphisme de structures.

**Propriété 3.54** Si $E_1$ et $E_2$ sont des cpos de structures avec quotient, alors on pose :

$$ \approx = \{ (S_1, \Upsilon, S_2) \mid S_1 \in E_1, S_2 \in E_2, S_1 \approx_{\Upsilon} S_2 \}, $$

$$ \rho_1(S_1, \Upsilon, S_2) = S_1, $$

$$ \rho_2(S_1, \Upsilon, S_2) = S_2. $$

L'ensemble $\approx$ est ordonné par $\subseteq$ défini comme suit :

$$ (S_1, \Upsilon, S_2) \subseteq (S'_1, \Upsilon', S'_2) \quad \text{si} \quad S_1 \subseteq S'_1, S_2 \subseteq S'_2 \quad \text{et} \quad \Upsilon = \Upsilon' \cap (\mathcal{U}_{S_1} \times \mathcal{U}_{S_2}). $$

Ainsi ordonné, $\approx$ est un cpo et $(\approx, \rho_1, \rho_2)$ est une relation continue.

**Propriété 3.55 (produit)** Soient $E_1, E_2$ des cpos et soit une relation $\mathcal{R} \subseteq E_1 \times E_2$ telle que $\mathcal{R}$ est clos par $\sqcup$, alors $(\mathcal{R}, \pi_1, \pi_2)$ où $\pi_1$ est la projection sur la première composante et $\pi_2$ sur la seconde composante, relie continuement $E_1$ et $E_2$.

**Corollaire 3.56 (applications continues)** Soient $E_1$ et $E_2$ des cpos et $f$ une application continue de $E_1$ dans $E_2$, alors $(E_1, \text{id}, f)$ relie continuement $E_1$ et $E_2$.

**Propriété 3.57 (composition)** Soient $E, E'$ et $E''$ trois cpos tels que $E$ et $E'$ sont reliés continuement par $(\mathcal{R}, \rho_1, \rho_2)$ et $E'$ et $E''$ sont reliés continuement par $(\mathcal{R}', \rho'_1, \rho'_2)$, alors $E$ et $E''$ sont reliés continuement par $(\mathcal{R}'', \eta_1, \eta_2)$ défini par :

$$ \mathcal{R}'' = \{ (R, R') \mid R \in \mathcal{R}, R' \in \mathcal{R}', \rho_2(R) = \rho'_1(R') \}, \\ \text{ordonné par } (R, R') \subseteq (S, S') \text{ si } R \subseteq S \text{ et } R' \subseteq S', $$

$$ \eta_1(R, R') = \rho_1(R), $$

$$ \eta_2(R, R') = \rho'_2(R'). $$
**Propriété 3.58 (intersection)** Soient $(\mathcal{R}, \rho_1, \rho_2)$ et $(\mathcal{R}', \rho'_1, \rho'_2)$ reliant continuement E et E'. Soit

$$
\begin{align*}
\mathcal{R}'' &= \{(R, R') \in \mathcal{R} \times \mathcal{R}' \mid \rho_1(R) = \rho'_1(R'), \rho_2(R) = \rho'_2(R')\}, \\
\eta_1(R, R') &= \rho_1(R), \\
\eta_2(R, R') &= \rho_2(R),
\end{align*}
$$

alors $(\mathcal{R}'', \eta_1, \eta_2)$ relie continuement E et E'.

**Lemme de correction**

Il nous reste à énoncer le lemme 3.59 exprimant la correction d'une trans-
formation décrite par un transducteur déterministe. L'annexe A.1 précise ces
constructions et donne les preuves manquantes.

Dans la suite, on appelle état (resp. transition) inévitable tout état (resp. toute transition) qui apparaît une infinité de fois dans chaque «branche de calcul infini» d’une exécution, et ce pour toutes les exécutions du transducteurs (cf. annexe A.1).

Soient un alphabet gradué $\mathcal{F}$ et $t^0$ un terme de $\mathcal{T}^\omega(\mathcal{F})$. On note $\overleftarrow{t^0}$ l'ensemble $\{t \in \mathcal{T}_\perp^\omega(\mathcal{F}) \mid t \sqsubseteq t^0\}$. L'ensemble $\overleftarrow{t^0}$ muni de l'ordre $\sqsubseteq$ est un cpo. Au sein de ce cpo, tout ensemble de termes admet une borne supérieure, notée $\sqcup$. Soit $T \sqsubseteq \overleftarrow{t^0}$, on note $\sqcap T$ le plus grand terme $t$ tel que pour tout $t' \in T$, $t \sqsubseteq t'$, c.a.d. $\sqcap T = \sqcup \{t \sqsubseteq t' \mid t' \in T\}$.

**Lemme 3.59 (correction)** *Soit t = (*F*, *F'*, *Q*, *q*<sub>init</sub>, *δ*) un transducteur déterministe. Si*

1. les transitions de consommation sont inévitables dans $\mathbf{t}$,

2. pour tout $q \in Q$ et tout $t^0 \in \mathcal{T}^\omega(\mathcal{F})$, il existe un cpo $\mathcal{R}[q, t^0]$ qui relie continuement $\overleftarrow{t^0}$ et $\mathcal{T}_\perp^\omega(\mathcal{F}')$ ; on note $\perp_{q,t^0}$ son plus petit élément, $\rho$ la projection sur $\overleftarrow{t^0}$ et $\rho'$ la projection sur $\mathcal{T}_\perp^\omega(\mathcal{F}')$,

3. il existe un ensemble d'états $Q_\perp \subseteq Q$ inévitable dans **t** tel que pour tout $q \in Q_\perp$ et tout $t^0 \in \mathcal{T}^\omega(\mathcal{F})$ on a $\rho'(\perp_{q,t^0}) = \perp$,

a. pour toute transition $\gamma = q(x) \rightarrow g(r_1(x), \dots, r_{|g|}(x))$ de $\delta$ et tout terme $t^0 \in \mathcal{T}^\omega(\mathcal{F})$, il existe une application continue $h_{\gamma,t^0}$ de $\mathcal{R}[r_1, t^0] \times \dots \times \mathcal{R}[r_{|g|}, t^0]$ dans $\mathcal{R}[q, t^0]$ telle que,

$$
\begin{align*}
\text{pour } (R_1, \dots, R_{|g|}) \in \mathcal{R}[r_1, t^0] \times \dots \times \mathcal{R}[r_{|g|}, t^0], \\
\quad \sqcap \{\rho(R_1), \dots, \rho(R_{|g|})\} &\subseteq \rho(h_{\gamma,t^0}(R_1, \dots, R_{|g|})), \\
\text{et } \rho'(h_{\gamma,t^0}(R_1, \dots, R_{|g|})) &= g(\rho'(R_1), \dots, \rho'(R_{|g|})),
\end{align*}
$$
b. pour toute transition $\gamma = q(f(x_1, \dots, x_{|f|})) \to r(x_i)$ de $\delta$ et pour tout terme $t^0 = f(t_1^0, \dots, t_{|f|}^0) \in \mathcal{T}^\omega(\mathcal{F})$, il existe une application continue $h_{\gamma,t^0}$ de $\mathcal{R}[r, t_i^0]$ dans $\mathcal{R}[q, t^0]$ telle que

$$ \text{pour } R \in \mathcal{R}[r, t_i^0], \quad f(t_1^0, \dots, t_{i-1}^0, \rho(R), t_{i+1}^0, \dots, t_{|f|}^0) \sqsubseteq \rho(h_{\gamma,t^0}(R)), \\ \text{et } \rho'(h_{\gamma,t^0}(R)) = \rho'(R), $$

c. pour toute transition $\gamma = q(x \in L) \to r(x)$ de $\delta$ et tout terme $t^0 \in L$, il existe une application continue $h_{\gamma,t^0}$ de $\mathcal{R}[r, t^0]$ dans $\mathcal{R}[q, t^0]$ telle que

$$ \text{pour } R \in \mathcal{R}[q, t^0], \quad \rho(R) \sqsubseteq \rho(h_{\gamma,t^0}(R)), \\ \text{et } \rho'(h_{\gamma,t^0}(R)) = \rho'(R), $$

alors pour $t^0$ un $\mathcal{F}$-terme et $q \in Q$, si $\mathbf{t}_q(t)$ est défini alors $\mathcal{R}[q, t^0](t^0, \mathbf{t}_q(t^0))$.

**Remarque 3.60** Dans la pratique on s'autorise à utiliser des transitions non atomiques. Ainsi, considérons une transition combinant consommation, production et anticipation de la forme suivante.

$$ \text{si } x_1 \in L_1, \dots, x_{|f|} \in L_{|f|}, \quad q(f(x_1, \dots, x_{|f|})) \to u, \\ \text{où } u \text{ est un terme fini sur l'alphabet } \mathcal{F}' \cup \{r(x_i): 0 \mid r \in Q, i \in [[|f|]]\}. $$

Soient $r_1(x_{\pi(1)}), \dots, r_n(x_{\pi(n)})$ les symboles de $\{r(x_i): 0 \mid r \in Q, i \in [[|f|]]\}$ apparaissant dans $u$ (chaque $r(x)$ apparaissant autant de fois que dans $u$). L'hypothèse permettant d'utiliser le lemme 3.59 s'exprime alors comme suit.

Pour tout $t^0 = f(t_1^0, \dots, t_{|f|}^0) \in \mathcal{T}^\omega(\mathcal{F})$, il existe une application continue $h$ de $\mathcal{R}[r_1, t_{\pi(1)}^0] \times \dots \times \mathcal{R}[r_n, t_{\pi(n)}^0]$ dans $\mathcal{R}[q, t^0]$ telle que :

$$ \text{pour } (R_1, \dots, R_n) \in \mathcal{R}[r_1, t_{\pi(1)}^0] \times \dots \times \mathcal{R}[r_n, t_{\pi(n)}^0], \\ \text{alors } f(\sqcap\{\rho(R_i) \mid \pi(i) = 1\}, \dots, \sqcap\{\rho(R_i) \mid \pi(i) = |f|\} \sqsubseteq \rho(h(R_1, \dots, R_n)), \\ \text{et } \rho'(h(R_1, \dots, R_n))) = u\{\rho(R_i) / r_i(x_{\pi(i)})\}, $$

où $u\{\rho(R_i) / r_i(x_{\pi(i)})\}$ représente le terme $u$ dans lequel pour tout $i$, l'occurence de $r_i(x_{\pi(i)})$ est remplacée par $\rho(R_i)$.

Cette hypothèse généralise celle de l'énoncé du lemme 3.59. Elle peut être décomposée en sous-règles correspondant à la décomposition de la transition en transitions atomiques. Le lemme 3.59 s'applique alors.

**Remarque 3.61** Le lemme 3.59 permet d'établir des relations entre algèbres de termes. il peut aussi être utilisé pour mettre en relations deux algèbres quelconques. En effet, si $(\mathcal{R}, \rho_1, \rho_2)$ relie continuellement une $\mathcal{F}$-algèbre $\mathbf{A}$ et une $\mathcal{F}'$-algèbre $\mathbf{A}'$, alors la relation $(\mathcal{R}', \rho'_1, \rho'_2)$ définie par

$$ \mathcal{R}' = \{(t_1, R, t_2) \in \mathcal{T}_{\perp}^{\omega}(\mathcal{F}) \times \mathcal{R} \times \mathcal{T}_{\perp}^{\omega}(\mathcal{F}') \mid \rho_1(R) = [[t_1]]_{\mathbf{A}}, \rho_2(R) = [[t_2]]_{\mathbf{A}'}\} \\ \text{avec } (t_1, R, t_2) \sqsubseteq (t'_1, R', t'_2) \quad \text{si } t_1 \sqsubseteq t'_1, R \sqsubseteq R' \text{ et } t_2 \sqsubseteq t'_2, \\ \text{et } \rho'_1(t_1, R, t_2) = t_1, \quad \rho'_2(t_1, R, t_2) = t_2. $$
relie continuement $\mathcal{T}_{\perp}^{\omega}(\mathcal{F})$ et $\mathcal{T}_{\perp}^{\omega}(\mathcal{F}')$. De plus, par définition $\mathcal{R}'(t_1, t_2)$ est vrai si et seulement si $\mathcal{R}(\llbracket t_1 \rrbracket_{\mathbf{A}}, \llbracket t_2 \rrbracket_{\mathbf{A}'})$ l'est. En appliquant ce principe, on peut directement utiliser le lemme de validité 3.59 pour établir des relations entre algèbres quelconques, et non plus uniquement entre algèbres de termes.

**Exemple 3.62** Dans l'exemple 3.53, la construction ne fonctionne pas, ou en tout cas, ne produit pas l'effet espéré. Cela provient du fait que l'hypothèse 3 du lemme 3.59 n'est pas vérifiée : en particulier, pour aucun $n \in N$ on a $n + 1 = 0$, et il existe un cycle ne passant que par l'état $q_{+1}$.

Un transducteur **t** permettant de remédier à ce problème est par exemple le suivant dont l'état initial est $q_{+1}$:

$$
\begin{array}{ll}
\text{si } \llbracket t \rrbracket = 0, & q_{+1}(t) \to 1, \\
\text{si } \llbracket t \rrbracket = \infty, & q_{+1}(t) \to \infty, \\
\text{sinon} & q_{+1}(1) \to 1 + 1, \\
\text{sinon} & q_{+1}(t+t') \to q_{+1}(t) + q_{id}(t'),
\end{array}
$$

$$
\begin{array}{l}
q_{id}(0) \to 0, \\
q_{id}(1) \to 1, \\
q_{id}(t+t') \to q_{id}(t) + q_{id}(t').
\end{array}
$$

Toutes les relations continues utilisées ici sont de la forme ($\mathcal{R}$, $\rho$, $\rho'$) avec $\mathcal{R} \subseteq N \times N$, $\rho(n, n') = n$ et $\rho'(n, n') = n'$ (dans ce contexte, toute application est continue si et seulement si elle est croissante).

On peut alors point à point préciser quelles sont les hypothèse du lemme 3.59.

1. les transitions de consommations sont inévitable dans **t**, car les seules transitions ne contenant pas de consommation se trouvent dans des feuilles de l'exécution,

2. on pose pour tout $n \in N$, $\mathcal{R}[q_{+1}, n] = \{(k, k+1) \mid 0 \le k \le n\}$ et $\mathcal{R}[q_{id}, n] = \{(k, k) \mid 0 \le k \le n\}$

3. on vérifie que {$q_{id}$} est un ensemble inévitable (et en particulier aucune branche infinie d'exécution ne peut contenir une infinité d'états $q_{+1}$ grâce aux deux premières transitions), et on a bien pour tout $n \in \mathbb{N}$, $\mathcal{R}[q_{id}, n](0,0),$
a-c. les règles suivantes correspondent respectivement aux transitions de t,

$$ \mathcal{R}[q_{+1}, 0](0, 1) $$

$$ \mathcal{R}[q_{+1}, \infty](\infty, \infty) $$

$$ \mathcal{R}[q_{+1}, 1](1, 2) $$

$$ h_{q_{+1},(n+n')}: (k, l), (k', l') \mapsto (k + k', l + l') $$

est une application continue de $\mathcal{R}[q_{+1}, n] \times \mathcal{R}[q_{id}, n']$ dans $\mathcal{R}[q_{+1}, n + n']$

$$ \mathcal{R}_{id}(0, 0) $$

$$ \mathcal{R}_{id}(1, 1) $$

$$ h_{q_{id},(n+n')}: (k, k'), (l, l') \mapsto (k + l, k' + l') $$

est une application continue de $\mathcal{R}[q_{id}, n] \times \mathcal{R}[q_{id}, n']$ dans $\mathcal{R}[q_{+1}, n + n']$.

Une preuve de correction pour un transducteur déterministe est donc délicate à formaliser. Dans la pratique, de nombreuses libertés sont prises. En particulier, ne pas préciser explicitement les applications continues. Ainsi, dans l'exemple précédent, on dira que si $\mathcal{R}[q_{+1}, n](k, l)$ et $\mathcal{R}[q_{id}, n'](k', l')$ alors $\mathcal{R}[q_{+1}](k+k', l+l')$ sans expliciter l'application $h_{q_{+1},(n+n')}$. Comme déja mentionné, ce raccourci omet la caractéristique de continuité de cette implication. Cependant, pour ne pas trop nuire à la lisibilité, cette manière de faire prévaut dans la suite de ce travail.
# Chapitre 4

## Graphes et structures sur les piles

Ce chapitre a pour but de présenter les structures définies sur les piles. Par structures définies sur les piles, on entend structure dont le codage le plus naturel est de considérer un ensemble de piles comme univers et des familles de relations «simples» construites par combinaison d'actions *dépiler* et *empiler*.

Cette définition, bien qu'informelle, capture un ensemble très précis de familles de structures dont les propriétés se distinguent clairement des familles de structures sur les termes (chapitres 5 et 6).

L'une des principales questions concernant ces structures est le choix d'une représentation. Trois grandes approches sont possibles :

- la représentation interne consiste à donner explicitement l'univers de la structure et à décrire séparément les relations définissant l'interprétation de chaque symbole;

- la représentation par systèmes d'équations consiste à décrire une famille de structures par une algèbre continue. Les structures de la famille sont alors exactement les solutions de systèmes d'équations sur les opérateurs de l'algèbre;

- la représentation par transformation] consiste à se donner une structure initiale et à s'autoriser un ensemble de transformations sur cette structure. La famille de structures décrite est alors l'ensemble des structures que l'on peut obtenir en appliquant à la structure initiale une ou plusieurs de ces transformations.

Chacune de ces représentations possède ses avantages et ses inconvénients. Ainsi, la représentation interne est la plus intuitive car elle correspond à la notion de machine : l'univers est l'ensemble des configurations de cette machine, et les relations sont un programme. La représentation par systèmes d'équations possède quant à elle l'avantage d'être facilement manipulable car les transformations algébriques d'équations sont un outil puissant. Enfin, la représentation par transformation procure la plupart des résultats de décidabilité sur les structures.
Chacune des familles de structures décrites dans la suite de ce chapitre possède éventuellement plusieurs représentations distinctes qui seront tour à tour étudiées. Établir les équivalences entre ces différentes représentations est l'objectif principal de ce chapitre.

Le paragraphe est décomposé comme suit. Suit la présentation des familles de graphes préfixes (4.2) puis des structures HR-équationelles (4.3). Le paragraphe 4.4 sur les structures préfixes reconnaissables est le plus complexe car de nombreuses représentations de ces familles sont possibles.

# 4.1 Langages rationnels et systèmes d'équations

La théorie des langages se prête bien à la description en terme de système d'équations. Cela nous fournit des exemples plus simples que les graphes ou les structures étudiés par la suite. Nous présentons ici la hiérarchie de Chomsky sous cet angle. De nombreux ouvrages traitent de ce domaine comme [HU79].

## 4.1.1 Automates

Un jeu d'opérateurs simple permet de représenter fidèlement le comportement des automates non déterministes de mots. Pour un alphabet $\mathbf{A}$, les opérateurs $Auto[\mathbf{A}]$ (ou plus simplement $Auto$ si aucune confusion n'en résulte) sont au nombre de trois :

- l'union de langages (notée +),

- le langage $\{\varepsilon\}$,

- la concatenation à gauche d'une lettre $a \in \mathbf{A}$ notée $a$, associe à tout langage $L$ le langage $a.L$ défini comme usuellement.

Bien entendu, le lien avec les langages rationnels est naturel.

**Propriété 4.1** *Les langages rationnels sont les solutions des Auto-systèmes d'équations finis.*

## 4.1.2 Automates déterministes

Un automate déterministe quant à lui consomme systématiquement une lettre lors de chaque transition, et la destination de cette transition est entièrement déterminée par cette lettre. De plus, à partir de chaque état, l'automate peut accepter ou refuser le mot vide.

Ces remarques se traduisent en deux opérateurs sur les langages. Pour un alphabet $\mathbf{A} = \{a_1, \dots, a_n\}$, il y a deux opérateurs $Auto_d[\mathbf{A}]$ (ou plus simplement $Auto_d$)

- l'opération qui aux langages $L_1, \dots, L_n$ associe le langage $a_1L_1 + \dots + a_nL_n$,
- l'opération qui aux langages $L_1, \dots, L_n$ associe le langage $\varepsilon + a_1 L_1 + \dots + a_n L_n$.

Par exemple, le langage rationnel $(ab)^*$ est la solution en $X$ du Auto$_d$-système d'équations suivant :

$$ 
\begin{aligned}
X &= \varepsilon + aY + bZ, \\
Y &= aZ + bX, \\
Z &= aZ + bZ.
\end{aligned}
$$

On a alors le résultat classique suivant.

**Propriété 4.2** *Les langages rationnels sont les solutions des Auto$_d$-systèmes d'équations finis.*

Précisons tout de même que, comme il s'agit d'automates en forme déterministe, il n'est pas possible de passer d'un Auto-système d'équation à un Auto$_d$-système d'équations par un transducteur déterministe (le contraire est en revanche vrai).

## 4.2 Les graphes préfixes

Les graphes préfixes sont la forme la plus simple de structures infinies que nous considérons dans ce travail. Ces graphes se décrivent par un ensemble rationnel de sommets et les relations arcs s'obtiennent par récriture préfixe du mot représentant le sommet.

**Définition 4.3 (graphe préfixe)** *Un graphe est préfixe s'il est isomorphe au graphe de sommets $V$ et dont les arcs étiquetés par $a$ sont définis par*

$$ \rightarrow^{a} = \{(uv, u'v) \in V^2 \mid (u, a, u') \in \Delta, v \in \Sigma^*\} \quad \text{avec} $$

- $\Sigma$ un alphabet fini,

- $V$ une partie rationnelle de $\Sigma^*$,

- $\Delta$ une partie finie de $\Sigma^* \times A \times \Sigma^*$.

<figure><img src="image_25.png" /><figcaption>FIG. 4.1 – *Un graphe préfixe : l'échelle.*</figcaption></figure>
**Exemple 4.4** La figure 4.1 donne un exemple simple de graphe préfixe : l'échelle. L'ensemble des étiquettes est {a, b, c}; l'alphabet est Σ = {A, B, C}; l'ensemble des sommets est V = (B + C)A*; l'ensemble des règles de récriture est

$$ \Delta = \{(B, a, BA), (B, b, C), (CA, c, C)\}. $$

Le premier travail s'intéressant aux graphes préfixes est dû à Müller et Schupp [MS85]. Leur formalisme est néanmoins différent pour deux raisons :

- les auteurs considèrent les graphes des transitions des automates à pile. Ainsi, l'ensemble des sommets n'est pas un ensemble de mots comme pour les graphes préfixes, mais un ensemble de configurations d'automate, c'est-à-dire de couples formés de l'état de cet automate et d'un mot de pile (sur un alphabet de pile donné);

- la seconde différence est la restriction qu'ils effectuent : ils ne considèrent comme sommets du graphe que les configurations accessibles à partir d'une configuration initiale donnée. Les graphes considérés sont donc nécessairement connexes.

En 90, Caucal [Cau90] étend cette définition originale à celle des graphes préfixes<fnref n="1" />. Pour cela, il remarque qu'il n'est pas nécessaire de distinguer l'état de l'automate de la pile courante : on peut toujours coder cet état dans le sommet de pile. Ainsi, dans l'exemple 4.4 les lettres B et C jouent le rôle des états de l'automate alors que les mots sur A* se comportent les mots de la pile. Il n'y a alors plus besoin que du mot de pile pour représenter une configuration et une transition de l'automate correspond à une récriture préfixe sur ce mot.

La seconde amélioration concerne l'ensemble des sommets : il ne s'agit plus de l'ensemble des configurations accessibles à partir d'une configuration initiale, mais d'un ensemble rationnel. Il se trouve que l'ensemble des mots accessibles par récriture préfixe à partir d'un mot donné est un ensemble rationnel (un résultat bien antérieur, dû à Büchi [Büc64]). On en déduit que les graphes préfixes contiennent les graphes considérés par Müller et Schupp. Cette extension est d'ailleur stricte puisqu'il existe des graphes préfixes non connexes.

Cette extension du travail de Müller et Schupp se justifie pourtant aisément car elle préserve l'une des propriétés fondamentales qu'ils avaient mise en évidence.

**Théorème 12 (Müller et Schupp [MS85])** La théorie monadique des graphes préfixes est décidable.

<footnote n="1">1. Notons que les graphes préfixes présentés dans ce travail se distinguent légèrement de la définition originale car ils peuvent contenir des sommets isolés alors que ceux-ci sont implicite-ment éliminés dans les travaux de Caucal.</footnote>
Les propriétés suivantes donnent des méthodes de construction des graphes préfixes.

**Propriété 4.5** *Les graphes préfixes contiennent*

- les graphes finis,

- les arbres réguliers de degré fini.

*Les graphes préfixes sont clos par*

- union disjointe,

- substitution finie inverse,

- modification finie,

- restriction rationnelle (lorsqu'ils sont enracinés),

- produit (synchrone où asynchrone) avec un graphe fini,

- restriction à une composante connexe.

Enfin, il est important de rappeler l'une des propriétés fondamentales des graphes préfixes, c'est à dire leurs traces. En effet, les graphes préfixes étant issus des automates à pile, ils reconnaissent comme eux les langages algébriques.

**Théorème 13** *Les traces des graphes préfixes entre un sommet initial et un sommet final sont les langages algébriques.*

L'inclusion des traces des graphes préfixes dans les langages algébriques est classique. La démonstration de la réciproque nécessite quant à elle une mise sous forme normale dite de Greibach de la grammaire. Nous ne présentons pas ici cette opération. Il s'agit néanmoins d'un grand classique de la théorie des langages et le lecteur intéressé peut se rapporter, entre autre, au livre de Hopcroft et Ullman [HU79], où encore à celui de Mateescu et Salomaa [MS97].

**Exemple 4.6** *Le graphe de la figure 4.1 a pour traces entre le sommet B et le sommet C le langage $\{a^n b^n \mid n \in \mathbb{N}\}$. Ce langage est algébrique car il est la plus petite solution de l'équation $X = a.X.c + b$.*

Les graphes préfixes s'étendent naturellement aux structures en considérant des récritures faisant intervenir plus de deux mots. Nous n'explicitons pas ici cette extension; elle sera présentée de manière plus générale dans le contexte des graphes préfixes reconnaissables.

Étant donné un sommet d'un graphe préfixe, le nombre de sommets auquel il est susceptible d'être relié (par un arc avant ou retour) est borné par deux fois le nombre de règles de récriture (une fois pour les arcs avant et une fois pour les arcs retour). Les graphes préfixes sont donc de degré borné. La famille des structures HR-équationnelles lève cette restriction.
## 4.3 Les structures HR-équationnelles

Ce paragraphe est dédié à la présentation des structures dites HR-équationnelles, ainsi que des graphes correspondants. Nous en donnons une première approche intuitive à l'aide des grammaires de graphes (4.3.1). La définition de référence de cette famille est quant à elle donnée au paragraphe 4.3.2. Enfin, la présentation de ces graphes se termine par une étude de quelques-unes de leurs propriétés (4.3.3).

### 4.3.1 Première approche : grammaires de structures

<figure><img src="image_26.png" /><figcaption>FIG. 4.2 – Graphe HR-équationnel.</figcaption></figure>

Les structures HR-équationnelles ont été proposées par Courcelle [Cou89]. Suivant les travaux, elles sont qualifiées simplement d'équationnelles, ou de régulières. Afin de lever toute ambiguïté, elles sont appelées dans le reste de ce travail structures HR-équationnelles. Cette terminologie fait référence à la définition 4.8 qui donne une caractérisation de la famille en termes de solutions de systèmes d'équations.

Ce n'est pourtant pas la première présentation de cette famille que nous donnons ici. En effet, il existe une autre définition classique de la même famille de structures : il s'agit d'une définition en termes de grammaires de structures (originellement d'hyper-graphes). Cette approche est assez délicate à formaliser mais possède l'avantage d'être intuitive. Nous la présentons au travers d'un exemple.

Il s'agit d'obtenir le graphe de la figure 4.2, c'est-à-dire l'arbre de degré infini étiqueté par *a* et augmenté d'une relation successeur entre frères étiquetée par *b*. Pour cela, on utilise un symbole relationnel intermédiaire (dit "non terminal") A d'arité 2 en plus des deux étiquettes *a* et *b*. Le graphe de la figure 4.2 est alors
obtenu comme limite de la suite de structures ($H_n$) définie par :

- $H_0$ est la structure à deux sommets en relation par $A$,

- $H_{n+1}$ se déduit de $H_n$ par application parallèle de la règle de récriture suivante :

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

c'est à dire en remplaçant chaque non terminal $A$ de $H_n$ par le motif correspondant (les sommets marqués par 1 et 2 sont ceux que la récriture conserve, les autres sont insérés comme de nouveaux sommets).

<figure><img src="image_28.png" /><figcaption>FIG. 4.3 – *Structures successivement obtenues par récriture.*</figcaption></figure>

La figure 4.3 présente les quatre premières structures de cette suite. Le non terminal $A$ est représenté en pointillé comme s'il s'agissait d'un arc. Cette suite de graphes a pour limite le graphe de la figure 4.2.

L'approche présentée au travers de cet exemple se généralise sans difficultés aux structures et permet de définir la famille des structures dites HR-équationnelles. Le paragraphe suivant a pour objectif de donner une description équationelle de cette famille de structures.
4.3.2 Représentation équationnelle

Dans le reste de ce travail, il n’est plus question de ces grammaires «de struc-
tures». Il leur est substitué les systèmes d’équations HR dont la définition est
donnée ci-dessous. Cette définition nécessite de pouvoir fusionner des éléments
de l’univers dans le système d’équations. Pour cela, on travaille sur le cpo des
structures colorées avec quotient.

Pour $C$ un ensemble fini de symboles unaires appelés *couleurs* et $\Sigma$ un ensemble disjoint de symboles relationnels, une $\Sigma$-structure colorée par $C$ est une structure dont la signature est $\Sigma \cup C$, et telle que les interprétations des $c \in C$ forment une partition de l’univers : une couleur $c$, et une seule, est attachée à chaque élément $u$ de l’univers ; on dit que $u$ a la couleur $c$. Un graphe coloré par $C$ est similairement une structure possédant la signature d’un graphe augmentée de $C$. Lorsque l’on représente ces graphes colorés, les couleurs sont placées directement à l’emplacement du sommet.

L’intention est de se servir de ces couleurs pour identifier un ou plusieurs
sommets dans les opérations de construction des structures.

Dans le cas des structures HR-équationnelles, on considère des structures co-
lorées avec quotient.

<figure><img src="image_29.png" /><figcaption>FIG. 4.4 – Union disjointe puis fusion (couleur 0 non représentée).</figcaption></figure>
Les opérateurs $\text{HR}[\Sigma, C]$ (ou plus simplement $\text{HR}$) opèrent sur le cpo des $\Sigma$-structures colorées par $C$. Ce sont les suivants.

- Les structures finies colorées par $C$ avec quotient, que l'on note simplement $\mathcal{S}$ pour $\mathcal{S}$ une structure finie.

- L'union disjointe $\oplus$ avec sa sémantique habituelle.

- Le recoloriage par $\alpha$, noté $\text{recol}[\alpha]$, où $\alpha$ est une application de $C$ dans $C$. La sémantique du recoloriage laisse invariante la structure, si ce n'est que les éléments de l'univers de couleur $c$ ont pour nouvelle couleur $\alpha(c)$ :

$$ \text{recol}[\alpha](\mathcal{S}) = \left| \begin{array}{ll} \alpha(c)(x) & : c(x), \qquad c \in C \\ R(x_1, \dots, x_{|R|}) & : R(x_1, \dots, x_{|R|}) \quad R \in \Sigma \\ x \sim y & : x \sim y \end{array} \right| (\mathcal{S}). $$

On utilise parfois la notation $\text{recol}[c_1 \to c_2]$, où $c_1$ et $c_2$ sont des couleurs, pour signifier $\text{recol}[\alpha]$, $\alpha$ étant défini par $\alpha(c) = c$ pour toute couleur $c \neq c_1$, et $\alpha(c_1) = c_2$.

- La fusion de couleur $c_0$, notée $\text{fusion}[c_0]$, étend la relation d'équivalence de telle sorte que tous les sommets de couleur $c_0$ soient dans la même classe :

$$ \text{fusion}[c_0](\mathcal{S}) = \left| \begin{array}{ll} c(x) & : c(x), \qquad c \in C \\ R(x_1, \dots, x_{|R|}) & : R(x_1, \dots, x_{|R|}), \qquad R \in \Sigma \\ x \sim y & : x \sim y \lor (c_0(x) \land c_0(y)) \end{array} \right| (\mathcal{S}) $$

Pour $E = \{c_1, \dots, c_n\}$ un ensemble de couleur, $\text{fusion}[E]$ est un raccourci pour $\text{fusion}[c_1] \circ \dots \circ \text{fusion}[c_n]$.

**Exemple 4.7** Soit $C = \{0, 1, 2, 3\}$. La figure 4.4 présente trois graphes $G_1, G_2$ et $G_3$ et le résultat du calcul $G = \text{fusion}[\{1, 2, 3\}](G_1 \oplus G_2 \oplus G_3)$. Les rectangles pointillés montrent comment les sommets sont fusionnés par les opérateurs fusion. Les graphes $G_1$ et $G_3$ s'obtiennent par recoloriage de $G$. On obtient donc le système d'équations :

$$ X = \text{fusion}[\{1, 2, 3\}](X_1 \oplus G_2 \oplus X_3), \\ X_1 = \text{recol} \left[ \begin{array}{l} 0 \to 0 \\ 1 \to 2 \\ 2 \to 0 \\ 3 \to 0 \end{array} \right] (X), \quad X_3 = \text{recol} \left[ \begin{array}{l} 0 \to 0 \\ 1 \to 1 \\ 2 \to 3 \\ 3 \to 0 \end{array} \right] (X). $$

La plus petite solution de ce système d'équations est le graphe $G$.

**Définition 4.8** Les structures HR-équationnelles (resp. graphes équationnels) sont les structures (resp. graphes) solutions des HR-systèmes finis d'équations et élimination des couleurs.
Remarquons que dans cet énoncé, il n’est pas nécessaire de quotienter la structure par $\sim$ car la notion d’isomorphisme traite la relation $\sim$ de manière spécifique.

Telle qu'elle a été présentée ci-dessus, l'opération **fusion** semble compliquée, car elle fait intervenir un calcul de clôture réflexive et symétrique. En fait, cette opération peut être effectuée par une interprétation existentielle positive. Le lemme 4.9 donne une formalisation précise de ce fait.

**Lemme 4.9** *Pour $\mathcal{S}$ une $\Sigma$-structure colorée, $R \in \Sigma$ un symbole, $x_1, \dots, x_{|R|}$ des variables et $\gamma$ une valuation de $x_1, \dots, x_{|R|}$ sur $\mathcal{S}$, on a*

$$
\begin{array}{l}
\gamma, \text{fusion}[c_0](\mathcal{S}) \models R(x_1, \dots, x_{|R|}) \\
\qquad \text{ssi } \gamma, \mathcal{S} \models \bigvee_{E \subseteq [|R|]} \phi_{R,E} \\
\text{avec } \phi_{R,E} = \exists(z_i)_{i \in E}. R(z_1^E, \dots, z_{|R|}^E) \wedge \bigwedge_{i \in E} (c_0(x_i) \wedge c_0(z_i^E)) \\
\text{avec pour } i \in [|R|], \quad z_i^E = \begin{cases} \text{variable fraîche} & \text{si } i \in E, \\ x_i & \text{sinon.} \end{cases}
\end{array}
$$

**Preuve.** Soit $\mathcal{S}$ une $\Sigma$-structure colorée. Soit

$$
S' = \left|
\begin{array}{ll}
c(x) & : c(x), & c \in C \\
R(x_1, \dots, x_{|R|}) & : R(x_1, \dots, x_{|R|}), & R \in \Sigma \\
x \sim y & : x \sim y \lor (c_0(x) \land c_0(y)) &
\end{array}
\right|
(S)
$$

Telle quelle, cette structure n'est pas bien formée car il n'y a aucune garantie à
priori que la relation $\sim^{S'}$ soit une équivalence et encore moins une congruence.

Montrons tout d'abord que $\sim^{S'}$ est une relation d'équivalence. Symétrie et réflexivité sont héritées de la relation $\sim^{S}$ et de la structure de la troisième règle. Soient $u, v$ et $w$ tels que $u \sim^{S'} v$ et $v \sim^{S'} w$. Deux cas sont à considérer, si $c_0^{S}(v)$ alors $c_0^{S}(u)$ et $c_0^{S}(w)$ (propriété de $\sim^{S}$). D'où par définition de $\sim^{S'}$, $u \sim^{S'} w$. Si pour un certain $c \neq c_0$, $c^{S}(v)$, alors $u \sim^{S} v$ et $v \sim^{S} w$ (définition de $c^{S'}$). Par transitivité de $\sim^{S}$, $u \sim^{S} w$ et donc $u \sim^{S'} w$. Ainsi $\sim^{S'}$ est une relation d'équivalence. Par conséquence, $\sim^{S'} = \sim^{\overline{S'}}$.

Supposons $R^{\overline{S'}}(u_1, \dots, u_{|R|})$ avec pour tout $i$, $u_i = \gamma(x_i)$. Par définition de $\overline{S'}$, il existe $v_1, \dots, v_{|R|} \in \mathcal{U}_S$ tels que pour tout $i \in [|R|]$, $u_i \sim^{S'} v_i$ et $R^{\mathcal{S}}(v_1, \dots, v_{|R|})$. Soit $E = \{i \mid \mathcal{S} \models c_0(u_i)\}$. Si $i \in E$ alors $\mathcal{S} \models c_0(u_i)$ et donc par définition de $\sim^{\mathcal{S}}$, $\mathcal{S} \models c_0(v_i)$. Pour $i \notin E$, par définition de $\sim^{\mathcal{S}}$, on a $u_i \sim^{\mathcal{S}} v_i$. On peut donc remplacer $v_i$ par $u_i$ pour tout $i \notin E$ dans $R^{\mathcal{S}}(u_1, \dots, u_{|R|})$. Ainsi, $\gamma, \mathcal{S} \models \phi_{R,E}$.

On montre similairement l'autre implication.

□
### 4.3.3 Propriétés des graphes HR-équationnels

Énonçons le résultat fondamental de décidabilité associé aux structures HR-équationnelles.

**Théorème 14 (Courcelle [Cou89])** *Les solutions des HR-systèmes d'équations de théorie monadique décidable ont une théorie au second ordre gardée décidable.*
En fait, le résultat de Courcelle est plus général.

**Théorème 15 (Courcelle [Cou89])** *Pour toute formule close $\phi$ du second ordre gardée, les modèles de $\phi$ sont HR-$\mu$-définissables.*

La famille des structures HR-équationnelles contient strictement les graphes préfixes. Il est même possible d’en donner une caractérisation exacte.

**Propriété 4.10 (Caucal [Cau90])** *Les graphes HR-équationnels de degré borné sont les graphes préfixes.*

**Propriété 4.11** *Les structures HR-équationnelles sont closes par :*

- modification finie,

- union disjointe,

- restriction à une composante connexe,

- marquage rationnel,

- restriction rationnelle.

Nous ne donnons pas ici de preuve directe de ces résultats. Ils peuvent être déduits des résultats sur les graphes VR-équationnels.

En revanche, il manque une propriété de clôture simple aux structures HR-équationnelles : la clôture par interprétation au premier ordre (et en particulier par substitution finie inverse pour les graphes).

La propriété suivante s’intéresse à la largeur arborescente des graphes HR-équationnels. Cette même famille de graphe était définie en utilisant un jeu différent d’opérateurs.

**Propriété 4.12 (Courcelle [Cou92])** *Les graphes solutions de HR-systèmes d'équations (éventuellement infinis) sont de largeur arborescente bornée.*

**Preuve.** Pour $C$ un ensemble de couleurs et $\mathcal{G}$ un graphe coloré, notons $LA_C(\mathcal{G})$ la largeur arborescente du graphe $\mathcal{G}$ restreint aux sommets possédant une couleur dans $C$. On a alors les inégalités suivantes :

1. Pour tout ensemble fini $C$ de couleurs, $LA_C(\perp) = 0$, le cas pathologique du graphe sans sommet a pour largeur arborescente 0 par convention.

2. Pour tous graphes colorés finis $\mathcal{G}$ et $\mathcal{H}$ et tout ensemble fini de couleurs $C$, $LA_C(\mathcal{G} \oplus \mathcal{H}) \leq \max(LA_C(\mathcal{G}), LA_C(\mathcal{G}'))$. Il suffit pour cela de remarquer que dans un jeu du voleur et des policiers sur le graphe $\mathcal{G} \oplus \mathcal{G'}$, le voleur choisit
une position de départ qui est soit dans $\mathcal{G}$ soit dans $\mathcal{G}'$, et il ne pourra plus sortir de ce graphe en empruntant les arcs. Les policiers n'ont donc qu'à appliquer une stratégie gagnante sur ce graphe pour attraper le voleur.

3. Pour tout graphe coloré $\mathcal{G}$ fini, tout ensemble fini $C$ de couleurs et toute application $\alpha$ des couleurs dans les couleurs, $LA_C(\text{recol}[\alpha](\mathcal{G})) = LA_{\alpha^{-1}(C)}(\mathcal{G})$. Les deux membres de l'égalité correspondent au même jeu : seules les couleurs ont changé, et elles n'interviennent pas dans le jeu.

4. Pour $\mathcal{G}$ un graphe et $c_0$ une couleur,

$$ LA_C(\text{fusion}[c_0](\mathcal{G})) \le \begin{cases} LA_{C-\{c_0\}}(\mathcal{G}) + 1 & \text{si } c_0 \in C \\ LA_C(\mathcal{G}) & \text{sinon} \end{cases} $$

Le cas où $c_0 \notin C$ est évident (et correspond en fait à une égalté). Si $c_0 \in C$, supposons que $k$ policiers aient une stratégie gagnante sur $\mathcal{G}$ privé des sommets de couleur $c_0$. Alors, pour obtenir une stratégie gagnante sur $\text{fusion}[c_0](\mathcal{G})$, il suffit de rajouter un $(k+1)$-ème policier sur le sommet de couleur $c_0$ et d'utiliser la stratégie gagnante à $k$ policiers sur les autres sommets.

Notons $C(\mathcal{G})$ les couleurs effectivement utilisées dans un graphe coloré $\mathcal{G}$. Naturellement $|C(\mathcal{G})|$ représente le nombre de couleurs distinctes apparaissant dans $\mathcal{G}$. Considérons maintenant un ensemble fini $J$ d'opérateurs HR sur les couleurs $C_0$, et dont les opérateurs graphes finis sont $\mathcal{H}_1, \dots, \mathcal{H}_n$. Posons $K = \max\{LA_{C_0}(\mathcal{H}_i) - |C(\mathcal{H}_i)| \mid i \in [n]\}$. On montre alors que pour tout $J_\perp$-terme fini $t$ et pour tout ensemble de couleurs $C \subseteq C_0$,

$$ LA_C(\llbracket t \rrbracket) \le K + |C(\llbracket t \rrbracket)| \quad (*) $$

Ce résultat s'obtient par récurrence sur $t$, en utilisant la définition de $K$ pour les graphes finis, et les inégalités 1 à 4 pour les autres opérateurs.

Considérons maintenant un jeu sur un graphe infini valeur d'un $J$-terme infini $t$. La première étape consiste, pour le voleur, à sélectionner un sous-graphe fini $H$ sur lequel le jeu se déroule. Comme le graphe est décrit comme limite d'une suite croissante de graphes finis $(\mathcal{G}_n)_{n \in \mathbb{N}}$ (correspondante aux valeurs des $J_\perp$-termes finis de limite $t$), il existe un indice $i$ tel que $H \subseteq \mathcal{G}_i$. Ce graphe est valeur d'un $J_\perp$-terme fini, donc, d'après (*) $LA_{C_0}(H) \le LA_{C_0}(\mathcal{G}_i) \le K + |C(\mathcal{G}_i)| \le K + |C_0|$. Donc, la largeur arborescente du graphe $\llbracket t \rrbracket$ est inférieure à $K + |C_0|$. $\square$

Les opérateurs VR du paragraphe suivant se distinguent des opérateurs HR entre autre par le fait qu'ils ne possédent plus cette propriété de largeur arborescente bornée.
## 4.4 Graphes préfixes reconnaissables et extensions

Les graphes préfixes reconnaissables sont une extension des graphes du paragraphe précédent. Bien des descriptions équivalentes de ces graphes sont connues. Elles se décomposent en représentations internes, par transformations et équationnelles.

**Représentation interne.** La première description de cette famille de graphes est due à Caucal: ce sont les graphes dont l'ensemble des sommets est rationnel, et les relations arcs sont définies par des règle de récriture de mots décrites par des ensembles reconnaissables [Cau96].

**Représentation par transformations.** Caucal montre aussi que les mêmes graphes peuvent être déduits de l'arbre binaire complet par applications d'un marquage rationnel, d'une substitution rationnelle et d'une restriction rationnelle [Cau96]. Ces transformations sont des cas particuliers d'interprétations monadiques, dont se déduit la décidabilité de la théorie monadique de ces graphes. En fait, les graphes préfixes reconnaissables sont exactement ceux obtenables par interprétation monadique de l'arbre binaire complet [Bar97].

**Représentation équationnelle.** Barthelman donne une représentation équationnelle des graphes préfixes reconnaissables; ce sont les solutions des systèmes d'équations finis sur une ensemble adapté d'opérateurs, appelés opérateurs VR [Bar97].

En fait, une autre direction d'extension est aussi possible. Il s'agit d'autoriser des systèmes d'équations infinis dans la représentation équationnelle. Cette extension peut être traduite dans les deux autres types de représentations. On obtient alors pour toute famille acceptable de systèmes d'équations $Λ$, l'équivalence des trois familles de graphes suivantes.

**Représentation interne.** Les graphes dont les sommets sont formés d'un ensemble de mots reconnus par un automate déterministe $A \in \Lambda$, et dont les relations arcs sont représentées par des règles de récriture suffixe décrites par des ensembles reconnaissables.

**Représentation par transformations.** Les interprétations monadiques du dépliage des graphes de $Λ$.

**Représentation équationnelle.** Les solutions de VR-systèmes d'équations de $Λ$. Cette triple équivalence coïncide avec la précédente quand $Λ$ est l'ensemble des graphes finis. En fait, une seconde représentation équationnelle est établie dans ce chapitre, celle avec les graphes solutions de systèmes d'équations sur les opérateurs VR augmentés d'un opérateur de fusion (hérité des opérateurs HR).

Tous ces résultats s'adaptent relativement aisément aux structures. Ces extensions seront présentées tout au long du chapitre.
<figure><img src="image_30.png" /><figcaption>FIG. 4.5 – *Principaux résultats du paragraphe*</figcaption></figure>
Enfin, une dernière équivalence structurelle nous intéresse. Il s'agit d'un résultat de Barthelmann énonçant que les graphes préfixes reconnaissables dont les sous-graphes bipartis complets sont bornés sont exactement les graphes HR-équationnels [Bar98]. Ce résultat devient dans le cadre présent : pour toute famille acceptable de systèmes d'équations Λ, les solutions de VR-systèmes d'équations dans Λ dont les sous-graphes bipartis complets sont bornés, sont les solutions des HR-systèmes d'équations de Λ. Ainsi, il est possible de caractériser uniformément et de manière externe les solutions des HR-systèmes au sein des solutions des VR-systèmes.

Tous ces résultats d'équivalence sont répartis dans différents théorèmes. Une carte des principales dépendances est donnée à la figure 4.5. Chaque flèche représente une inclusion des familles de graphes.

Le reste de ce paragraphe est construit comme suit. L'aspect équationnel est traité en premier (4.4.1). Le paragraphe 4.4.2 s'attache aux représentations internes de ces familles de structures. Les représentations par transformations sont ensuite abordées (4.4.3). Le paragraphe 4.4.4 est dédié aux liens entre ces familles de graphes et la hiérarchie de Caucal. Enfin, l'étude de ces familles s'achève par la preuve que les graphes dont les sous-graphes bipartis complets sont bornés solutions de VR-systèmes d'équations peuvent être traduit au moyen d'un transducteur déterministe en solutions de HR-systèmes d'équations.

## 4.4.1 Représentation équationnelle

L'objectif ici est de décrire les différents opérateurs permettant de représenter les graphes préfixes reconnaissables au moyen de systèmes finis d'équations. La finitude de ces systèmes n'étant jamais utilisée, ce paragraphe dépasse le simple cadre des graphes préfixes reconnaissables.

Nous commençons par la présentation des opérateurs VR qui travaillent sur le domaine des graphes (4.4.1.1). Le paragraphe 4.4.1.2 présente les opérateurs VR' qui sont une extension des opérateurs VR aux structures. Le paragraphe 4.4.1.2 présente un premier résultat de normalisation de ces opérateurs dont l'intérêt est principalement d'illustrer les techniques qui seront ensuite utilisées dans des cadres plus compliqués. Enfin, l'ajout d'un opérateur de fusion est envisagé au paragraphe 4.4.1.3. Celui-ci peut-être éliminé par un transducteur déterministe (théorème 16).

### 4.4.1.1 Opérateurs sur les graphes

Pour A un alphabet d'étiquettes et C un ensemble de couleurs, les opérateurs VR[A, C] (ou plus simplement VR) opèrent sur les graphes colorés par C étiquetés
par A. Ils sont au nombre de quatre.

- L'union disjointe de graphes colorés, notée $\oplus$.

- Le graphe à un seul sommet de couleur $c$, noté $\text{sommet}[c]$. Pour $E \subseteq C$ un ensemble de couleurs, $\text{sommet}[E]$ est une abréviation représentant l'expression $\text{sommet}[c_1] \oplus \dots \oplus \text{sommet}[c_n]$, où $\{c_1, \dots, c_n\} = E$. Bien entendu, à isomorphisme près, la valeur de cette expression ne dépend pas du choix de numérotation des éléments de $E$.

- Le recoloriage par une application $\alpha$ des couleurs dans les couleurs, noté $\text{recol}[\alpha]$ qui a la même sémantique que pour les opérateurs HR.

- L'ajout d'arcs étiquetés par $a \in A$ entre les couleurs $c \in C$ et $c' \in C$. Il est noté $\text{arc}[c, a, c']$. Sa sémantique est de conserver le graphe inchangé, si ce n'est qu'un arc étiqueté par $a$ est ajouté entre tout couple de sommets $x, x'$ de couleurs respectives $c$ et $c'$. Pour $\mathcal{G}$ un graphe coloré,

$$ \mathbf{arc}[c, a, c'](\mathcal{G}) = \left| \begin{array}{lcl} c(x) & : & c(x) \qquad c \in C \\ x \xrightarrow{b} y & : & x \xrightarrow{b} y \qquad b \in A \\ x \xrightarrow{a} y & : & c(x) \wedge c'(y) \end{array} \right| (\mathcal{G}). $$

Pour $D$ une partie de $C \times A \times C$, $D = \{(c_1, a_1, c'_1), \dots, (c_n, a_n, c'_n)\}$, alors $\text{arc}[D]$ est une abréviation pour

$$ \text{arc}[D](\mathcal{G}) = \text{arc}[c_1, a_1, c'_1](\dots \text{arc}[c_n, a_n, c'_n](\mathcal{G})\dots). $$

où $D = \{(c_1, a_1, c'_1), \dots, (c_n, a_n, c'_n)\}$. Là encore, cette notation ne dépend pas du choix de numérotation des éléments de $D$ car les opérateurs $\text{arc}$ commutent.

Les graphes obtenus comme plus petites solutions de VR-systèmes d'équations finis sont appelés graphes VR-équationnels.

**Exemple 4.13** La figure 4.6 présente un graphe coloré $\mathcal{G}$ assimilable aux entiers positifs munis de la relation successeur étiquetée par $a$, de la relation $\leq$ étiquetée par $b$, et coloré par 1 pour 0 et par 2 pour les autres entiers.

On obtient le même graphe coloré $\mathcal{G}$ en effectuant la succession d'opérations suivante à partir de $\mathcal{G}$ :

1. ajouter un nouveau sommet isolé de couleur 0,

2. ajouter un arc étiqueté par $a$ entre le sommet de couleur 0 et le sommet de couleur 1,

3. ajouter un arc étiqueté par $b$ du sommet de couleur 0 vers tous les autres sommets,

4. recolorier le sommet de couleur 1 en couleur 2 et le sommet de couleur 0 en couleur 1.
<figure><img src="image_31.png" /><figcaption>FIG. 4.6 – Les entiers munis de la relation successeur (a) et inférieur (b).</figcaption></figure>

Ainsi, ce graphe est solution de l'équation :

$$ \mathcal{G} = \text{recol} \begin{bmatrix} 0 & \to 1 \\ 1 & \to 2 \\ 2 & \to 2 \end{bmatrix} (\text{arc}[\{(0, b, 0), (0, b, 1), (0, b, 2), (0, a, 1)\}](\mathcal{G} \oplus \text{sommet}[0])) . $$

Le paragraphe suivant montre comment il est possible d'étendre cette définition aux structures.

### 4.4.1.2 Extension aux structures

Le paragraphe précédent a permis de décrire des opérateurs sur les graphes infinis. Il s'agit ici d'étendre ces opérateurs aux structures. On construit ainsi les opérateurs VR'. Lorsque ces opérateurs servent à décrire des graphes, ils peuvent être traduits en opérateurs VR bien que nous n'établissions pas ce résultat (il s'agit d'un prolongement de la propriété 4.18).

#### Définition

L'extension des opérateurs VR aux structures se fait en unifiant les opérations de recoloriage et d'ajout d'arc : toutes deux sont des interprétations booléennes positives. Dans les opérateurs VR', l'interprétation booléenne positive est une opération à part entière.

Pour $\Sigma$ un alphabet de symboles relationnels, les opérateurs $VR'[\Sigma]$ (ou plus simplement $VR'$) opèrent sur les $\Sigma$-structures. Ils sont au nombre de trois.

- La structure à un élément un, c.a.d. telle que $\mathcal{U} = \{0\}$ et l'interprétation de tous les symboles (sauf $\sim$) est vide. On s'autorise une variante $\text{un}[R]$
où $R \in \Sigma$ est une symbole d'arité 1. Cette structure est égale à un si ce n'est que l'interprétation de $R$ est $\{0\}$.

- L'union disjointe de structures, notée $\oplus$.

- L'interprétation booléenne positive notée comme l'interprétation elle même. Bien entendu, dans le cadre des graphes colorés, l'interprétation booléenne positive permet d'exprimer le recoloriage tout comme l'ajout d'arcs. Ainsi, les opérateurs $VR'$ sont naturellement plus expressifs que les opérateurs $VR$.

Nous voyons maintenant comment montrer que $VR$ et $VR'$ coïncident sur les graphes colorés. Pour celà, il convient tout d'abord de normaliser les opérateurs $VR'$. Tel est le propos du paragraphe suivant.

## Normalisation

Dans ce paragraphe, nous montrons qu'il est possible de normaliser un système d'équations $VR'$ au moyen d'un transducteur déterministe (propriété 4.18). Cette forme normale est une restriction sur les formules booléennes positives autorisées dans les interprétations. Le rapport entre la version normalisée des opérateurs $VR'$ et les opérateurs sans restriction correspond au rapport entre automates non-déterministes et automates alternants. Ce résultat ne présente pas de difficulté particulière et peut être déduit d'autres constructions de ce travail. Néanmoins, cette preuve permet d'illustrer diverses techniques qui seront utilisées dans d'autres contextes ultérieurement.

Une *conjonction linéaire* est une formule booléenne positive formée uniquement de conjonctions et de prédicats relationnels, et dans laquelle chaque variable libre apparaît au plus une fois. Une formule booléenne est *en forme linéaire* si elle s'écrit comme une disjonction de conjonctions linéaires. Ainsi $a(x) \lor b(x)$ est en forme linéaire alors que $a(x) \land b(x)$ et $f(x, x)$ ne le sont pas. Une interprétation booléenne positive est en forme linéaire si toutes les formules qui la composent sont linéaires.

Une formule booléenne positive est *linéaire complète* vis à vis des variables $\{x_1, \dots, x_n\}$ si elle est linéaire, et que dans chacune des conjonctions apparaissent toutes les variables $x_i$. Ainsi, $a(x) \lor b(x)$ est linéaire complète vis à vis de $\{x\}$ mais ne l'est pas vis à vis de $\{x, y\}$. Remarquons que la formule *vrai* ne peut être mise sous forme linéaire complète que vis à vis de $\emptyset$ alors que la formule *faux* l'est pour tout ensemble de variables. On dit qu'une interprétation booléenne positive est linéaire complète si pour toute règle $R(x_1, \dots, x_n) : \phi, \phi$ est linéaire complète vis à vis de $\{x_1, \dots, x_n\}$.

Il s'agit maintenant de transformer les $VR'$-termes en $VR'$-termes dont les opérateurs interprétations sont linéaires complets. Soit donc $\Sigma$ un ensemble fini de symboles relationnels, et soit $N$ la plus grande des arités des symboles de $\Sigma$. Dorénavant, $\mathcal{X}$ représente l'ensemble de variables du premier ordre $\{x_1, \dots, x_N\}$.
Cet ensemble est naturellement totalement ordonné par $x_i \le x_j$ si $i \le j$. De la sorte, pour tout ensemble fini de variables $X \subseteq \mathcal{X}$ de cardinal $n$, il existe une unique séquence de variables $(y_1, \dots, y_n)$ strictement croissante telle que $X = \{y_1, \dots, y_n\}$. On note cette séquence $\bar{X}$.

Pour $X \subseteq \mathcal{X}$, $C(X)$ est l'ensemble des conjonctions booléennes positives dont les variables libres appartiennent à $X$. Modulo les invariants logiques usuels, $C(X)$ est fini. On introduit alors le nouvel ensemble de symboles relationnels suivant :

$$ \Sigma' = \{ \langle X, \phi \rangle \mid X \subseteq \mathcal{X}, \phi \in C(X) \} \quad \text{avec } |\langle X, \phi \rangle| = |X|. $$

L'interprétation $\mathcal{I}_0$ des $\Sigma$-structures dans les $\Sigma'$-structures est définie comme suit,

$$ \mathcal{I}_0 = \left| \langle X, \phi \rangle (\bar{X}) : \phi \right|. $$

On s'intéresse, pour une $\Sigma$-structure $S$ à construire une $\Sigma$-structure $S'$ telle que $\mathcal{I}_0(S) = S'$. Un problème subsiste: la relation entre $S$ et $S'$ ainsi définie ne relie aucun élément à la structure vide. En effet, $\perp \models \emptyset, \text{vrai} >$ et $\mathcal{I}_0(\perp) \neq \perp$. Cette relation ne permet pas de remplir les conditions de l'hypothèse 3 du lemme 3.59. Pour résoudre ce problème, on introduit l'interprétation booléenne positive $\mathcal{I}'_0$ définie comme suit.

$$ \mathcal{I}'_0 = \left| \begin{array}{ll} \langle X, \phi \rangle (\bar{X}) & : \langle X, \phi \rangle (\bar{X}), \quad X \neq \emptyset, \phi \in C(X) \\ \langle \emptyset, \text{vrai} \rangle & : \text{vrai} \end{array} \right|. $$

La relation $\mathcal{R}$ définie par $\mathcal{R}(S, S')$ si $\mathcal{I}_0(S) = \mathcal{I}'_0(S')$ est donc continue et satisfait $\mathcal{R}(\perp, \perp)$. Remarquons de plus que $\mathcal{I}'_0$ est linaire complète.

**Lemme 4.14** Soit $\phi$ une formule booléenne positive sur la signature $\Sigma$ de variables libres $X$. Il existe effectivement une formule $\phi^*$ linéaire complète vis à vis de $X$ sur la signature $\Sigma'$ telle que pour toute $\Sigma$-structure $S$ et toute valuation $\gamma$ de $X$ sur $S$,

$$ \gamma, S \models \phi \quad \text{ssi} \quad \gamma, \mathcal{I}_0(S) \models \phi^*. $$

**Preuve.** Il suffit de mettre la formule $\phi$ sous forme normale disjonctive $\phi = \phi_1 \lor \dots \lor \phi_k$ où les $\phi_k$ sont des conjonctions. On pose alors $\phi^* = \langle X, \phi_1 \rangle (\bar{X}) \lor \dots \lor \langle X, \phi_k \rangle (\bar{X})$. $\square$

**Corollaire 4.15** Pour toute interprétation booléenne positive $\mathcal{I}$ des $\Sigma$-structures vers les $\Sigma$-structures, il existe une interprétation booléenne positive linéaire complète $\mathcal{I}^*$ des $\Sigma'$-structures vers les $\Sigma'$-structures telle que :

$$ \mathcal{I}_0 \circ \mathcal{I} = \mathcal{I}^* \circ \mathcal{I}_0. $$
**Preuve.** Il suffit d'appliquer le lemme 4.14 à chacune des formules booléennes positives apparaissant dans l'interprétation $\mathcal{I}_0 \circ \mathcal{I}$. $\square$

**Lemme 4.16** Il existe une interprétation booléenne positive linéaire complète $\mathcal{I}_{\oplus}$ des $\Sigma'$-structures dans les $\Sigma'$-structures telle que pour toutes $\Sigma$-structures $S_1$ et $S_2$,

$$ \mathcal{I}_0(S_1 \oplus S_2) = \mathcal{I}_{\oplus}(\mathcal{I}_0(S_1) \oplus \mathcal{I}_0(S_2)). $$

**Preuve.** Il s'agit d'une application du lemme 2.13. $\square$

**Lemme 4.17** Pour toute signature $\Sigma$, il existe un transducteur déterministe $\mathbf{t}_0$ des $VR'[\Sigma]$-termes dans les $VR'[\Sigma']$-termes à interprétations linéaires complètes tel que pour tout $VR'[\Sigma]$-terme $t$, on a :

$$ [[\mathbf{t}_0(t)]] = \mathcal{I}_0([t]). $$

**Preuve.** Comme déja mentionné, $\mathcal{I}_0(S) = \mathcal{I}'_0(S')$ est continue et satisfait $\mathcal{I}_0(\perp) = \mathcal{I}'_0(\perp)$. Le corollaire 4.15 et le lemme 4.16 s'interprètent alors comme les hypothèses de récurrence démontrant la validité du transducteur déterministe suivant dont l'état initial est $q_0$ :

$$ \begin{align*} q_0(x) &\rightarrow \mathcal{I}'_0(q(x)) & (\text{cf. lemme 4.16}) \\ q(x \oplus y) &\rightarrow \mathcal{I}_{\oplus}(\mathcal{I}'_0(q(x)) \oplus \mathcal{I}'_0(q(y))) \\ q(\mathcal{I}(x)) &\rightarrow \mathcal{I}^*(\mathcal{I}'_0(q(x))) & (\text{cf. corollaire 4.15}) \\ q(\mathbf{un}) &\rightarrow \mathcal{S}' & \text{avec } \mathcal{S}' = \mathcal{I}_0(\mathbf{un}). \end{align*} $$

$\square$

On peut dès lors énoncer la propriété de normalisation qui nous intéresse.

**Propriété 4.18** Pour $\Sigma$ un alphabet relationnel, il existe un transducteur déterministe $\mathbf{t}$ des $VR'[\Sigma]$-termes dans les $VR'$-termes à interprétations linéaires complètes telle que pour tout $VR'[\Sigma]$-terme $t$,

$$ [[\mathbf{t}(t)]] = [[t]]. $$

**Preuve.** D'après le corollaire 4.15 appliqué à l'interprétation identité sur la signature $\Sigma$, il existe une interprétation linéaire complète $\mathcal{I}_0^{-1}$ tel que pour toute $\Sigma$-structure $S$, $\mathcal{I}_0^{-1}(\mathcal{I}_0(S)) = S$. On pose alors simplement $\mathbf{t} = \mathcal{I}_0^{-1} \circ \mathbf{t}_0$ ($\mathbf{t}_0$ est le transducteur déterministe du lemme 4.17). $\square$
### 4.4.1.3 Un opérateur de fusion supplémentaire

Il s'agit d'autoriser une opération supplémentaire de fusion (similaire à celle des opérateurs HR) aux opérateurs VR'. On montre alors que, au moyen d'un transducteur déterministe, cette opération peut être éliminée d'un système d'équations (théorème 16). Une conséquence de ce résultat est la classique inclusion à isomorphisme près des structures HR-équationnelles dans les structures VR'-équationnelles [Cau96].

Ce résultat est comparable à celui énoncé par Courcelle et Makowsky dans le contexte des structures finies [CM02]. La démonstration présente emprunte une partie des techniques de ce travail bien que la manière de conclure soit très différente. Une autre preuve est donnée dans [CC03] de ce résultat. Elle est moins générale que celle présentée dans ce mémoire qui se rapproche plus de celle de Courcelle et Makowsky.

Le reste de ce paragraphe consiste tout d'abord à présenter plus formellement les opérateurs VR' + fusion. On présente ensuite une famille de formules logiques dites «existentielles gardées». Suivent cinq lemmes énonçant le bon comportement de ces formules vis à vis des opérateurs VR'. Le paragraphe suivant s'attarde sur la récurrence proprement dite. Le théorème 16 est présenté dans le dernier paragraphe.

#### Les opérateurs VR' + fusion

Les opérateurs VR' + fusion travaillent sur des *structures colorées avec quotient*. Les opérateurs VR' n'affectent pas les couleurs. Les couleurs ne sont modifiées que par l'opération de recoloriage (héritée des opérateurs HR). L'opération de fusion (notée fusion) est paramétrée par une couleur (là encore, il s'agit de la même que pour les opérateurs HR). Pour $\Sigma$ un alphabet relationnel et $C$ un ensemble fini de couleurs, les opérateurs $(VR' + fusion)[\Sigma, C]$ (ou plus simplement $VR' + fusion$) sont les suivants.

- La structure à un seul élément de couleur $c$, notée sommet[c],

- L'union disjointe de structures colorées avec quotient, notée $\oplus$,

- L'interprétation booléenne positive notée $\mathcal{I}$ pour $\mathcal{I} = (\text{vrai}, \Sigma, (\phi_R)_{R \in \Sigma})$. Sa sémantique est définie comme suit.

$$ \mathcal{I}(S) = \left| \begin{array}{ll} c(x) & : c(x), \quad \text{pour } x \in C \\ R(x_1, \dots, x_{|R|}) & : \phi_R(x_1, \dots, x_{|R|}), \quad \text{pour } R \in \Sigma \\ x \sim y & : x \sim y \end{array} \right| $$

Ainsi $\mathcal{I}$ se comporte comme une interprétation sans restriction sur les symboles de $\Sigma$, tout en gardant les couleurs de $C$ non modifiées.

- Le recoloriage par une application $\alpha$ de $C$ dans $C$, noté recol[$\alpha$] est défini comme pour les opérateurs HR.
La fusion des éléments d'une même couleur c, notée fusion[c], a la même sémantique que pour les opérateurs HR.

**Remarque 4.19** Une autre opération naturelle de fusion peut être envisagée. Cette opération se sert d'un symbole relationnel unaire quelconque (et non d'une couleur) pour décrire la fusion. Savoir si le théorème 16 reste valable quand l'opération de fusion est de ce type est une question ouverte (la question correspondante pour les structures finies l'est tout autant [CM02]).

Dorénavant, nous supposons la signature $\Sigma$ et l'ensemble de couleurs $C$ fixés. L'entier $N$ est la plus grande arité présente dans $\Sigma$.

## Formules existentielles gardées

La démonstration du théorème 16 repose sur l'étude d'une famille précise de formules logiques. On s'intéresse aux formules logiques au premier ordre existentielles (c.a.d. ne possédant pas de quantification universelle) sur les prédicats $C \cup \Sigma$. On cherche à rendre chaque variable de telles formules indissociable de sa couleur. Cela revient à associer une couleur aux variables libres et à préciser la couleur des autres variables lors de leur introduction par une quantification.

Soit $X$ un ensemble de variables, une garde de $X$ est une application $g$ de $X$ dans $C$. On définit la formule $\bar{g}$ par

$$ \bar{g} = \bigwedge_{x \in X} (g(x))(x). $$

Ainsi, une garde permet d'attacher une couleur à chacune des variables libres d'une formule. Pour $g$ une garde, $x$ une variable et $c$ une couleur, alors $g, x \to c$ représente la garde $g'$ qui coïncide avec $g$ sur son domaine et telle que $g'(x) = c$.

On ajoute aussi une construction permettant d'attacher une couleur aux variables liées. Une formule existentielle avec quantifications gardées est une formule $\phi$ sur $\Sigma$ telle que toutes les quantifications existentielles qu'elle contient sont de la forme $\exists x:c.\psi$, où $x$ est une variable et $c \in C$ une couleur. Une formule $\exists x:c.\psi$ a la même interprétation que $\exists x.c(x) \wedge \psi$. Une telle construction quantifie donc uniquement sur les sommets d'une certaine couleur.

Une formule existentielle gardée est une conjonction $\bar{g} \wedge \phi$ où $\phi$ est une formule existentielle avec quantifications gardées et $g$ est une garde de $FV(\phi)$.

La propriété suivante montre que l'on peut toujours se limiter à l'utilisation de telles formules.

**Propriété 4.20** Toute formule existentielle sur les prédicats $\Sigma \cup C$ est équivalente à une disjonction de formules existentielles gardées.
**Preuve.** Considérons une formule existentielle $\phi$, on construit alors la formule $\phi^*$ par :

$$ \phi^* = \bigvee_{g \in C^{FV(\phi)}} (\bar{g} \wedge \phi^g) $$

où $\phi^g$ pour $g$ une garde de $FV(\phi)$ est définie récursivement par :

$$ (R(x_1, \dots, x_{|R|}))^g = R(x_1, \dots, x_{|R|}) \qquad (\exists x.\phi)^g = \bigvee_{c \in C} \exists x:c.\phi^{g,x \to c}, $$

$$ (c(x))^g = \begin{cases} \text{vrai} & \text{si } g(x) = c, \\ \text{faux} & \text{sinon} \end{cases} \qquad (x \sim y)^g = x \sim y, $$

$$ \begin{gathered} (\phi \wedge \psi)^g = \phi^g \wedge \psi^g, \qquad (\phi \vee \psi)^g = \phi^g \vee \psi^g, \\ \text{vrai}^g = \text{vrai}, \qquad \text{faux}^g = \text{faux}. \end{gathered} $$

On montre aisément par récurrence sur la structure de $\phi$ que pour toute structure $S$, toute garde $g$ de $FV(\phi)$ et toute valuation $\gamma$ de $FV(\phi)$ sur $S$,

$$ \gamma, S \models \bar{g} \wedge \phi \quad \text{ssi} \quad \gamma, S \models \bar{g} \wedge \phi^g. $$

Notons que ceci n'est vrai que parce que l'interprétation des couleurs forme une partition de l'univers. Les conclusions du lemme en découle. □

Il s'agit enfin de trouver une mesure de la complexité des formules existentielles gardées permettant d'assurer qu'elles soient finies modulo invariants syntaxiques. Pour cela, on compte le nombre d'imbrication de quantifications existentielles gardées par une même couleur. Pour $c \in C$ une couleur, et pour $\phi$ une formule gardée par $C$, on définit l'entier naturel $l_c(\phi)$ comme suit :

$$ \begin{gathered} l_c(\text{vrai}) = 0 \qquad l_c(\text{faux}) = 0 \\ l_c(\phi \wedge \psi) = \max(l_c(\phi), l_c(\psi)) \qquad l_c(\phi \vee \psi) = \max(l_c(\phi), l_c(\psi)) \\ l_c(R(x_1, \dots, x_{|R|})) = 0 \qquad l_c(\exists y:c'.\phi) = \begin{cases} l_c(\phi) & \text{si } c' \neq c \\ l_c(\phi) + 1 & \text{sinon.} \end{cases} \end{gathered} $$

On pose $l_C(\phi) = \max\{l_c(\phi) \mid c \in C\}$.

## Comportement des formules existentielles gardées vis à vis des opérateurs VR' + fusion

Nous montrons ici comment, pour chacun des opérateurs VR' + fusion, la satisfaction d'une formule existentielle gardée par une structure après application de
l'opérateur se ramène à la satisfaction de (combinaisons de) formules existentielles gardées sur la/les structures arguments.

Suivent donc quatre lemmes — un pour chaque opérateur sauf pour sommet
qui n'en nécessite pas — formalisant ce principe. Ces constructions sont classiques
si ce n'est la construction associée à l'opérateur fusion (lemme 4.22).

**Lemme 4.21 (opérateur interprétation)** *Soit* $\mathcal{I}$ *une interprétation booléenne positive des structures colorées par C dans les structures colorées par C. Pour toute formule existentielle gardée $\phi$ il existe un formule existentielle gardée $\phi^\mathcal{I}$ de même variables libres telle que pour toute $\Sigma$-structure $S$ et toute valuation $\gamma$ de $FV(\phi)$ sur $S$, on a :*

$$
\gamma, \mathcal{I}(S) \models \phi \quad \text{ssi} \quad \gamma, S \models \phi^{\mathcal{I}}.
$$

$$
\textit{De plus, si } l_C(\phi) \leq N, \textit{ alors } l_C(\phi^{\mathcal{I}}) \leq N.
$$

**Preuve.** Il suffit de remplacer chaque ocurrence d'un prédicat $R(y_1, \dots, y_n)$ dans $\phi$ par sa définition dans $\mathcal{I}$. Cette opération ne change pas les imbrications de quantifications car $\mathcal{I}$ ne contient pas de quantifications. $\square$

**Lemme 4.22 (opérateur fusion)** *Soit $c_0 \in C$ une couleur. Pour toute formule existentielle gardée $\bar{g} \wedge \phi$, il existe un formule existentielle à quantifications gardées $\phi_{g,c_0}$ telle que*

$$
- FV(\phi_{g,c_0}) = \{x \in FV(\phi) \mid g(x) \neq c_0\},
$$

- pour toute $\Sigma$-structure $S$ et toute valuation $\gamma$ de $FV(\phi)$ sur $S$, on a

$$
\gamma, \text{fusion}[c_0](S) \models \bar{g} \wedge \phi \quad \text{ssi} \quad \gamma, S \models \bar{g} \wedge \phi_{g,c_0},
$$

- si $l_C(\phi) \leq N$, alors $l_C(\phi_{g,c_0}) \leq N$.

**Preuve.** La formule $\phi_{g,c_0}$ est définie récursivement comme suit.

$$
\begin{align*}
R(y_1, \dots, y_{|R|})_{g,c_0} &= \exists z_{p_1}:c_0 \dots \exists z_{p_k}:c_0 \cdot R(z_1, \dots, z_n) , \\
&\quad \text{avec } \{p_1, \dots, p_k\} = \{p \mid g(y_p) = c_0\} , \\
&\quad \text{et } z_i = \begin{cases} y_i & \text{si } g(y) \neq c_0 , \\ \text{variable fraîche} & \text{sinon} , \end{cases}
\end{align*}
$$

$$
(\exists y:c.\phi)_{g,c_0} = \begin{cases} \phi_{g,y \to c_0,c_0} & \text{si } c = c_0, \\ \exists y:c.\phi_{g,y \to c,c_0} & \text{sinon}, \end{cases}
$$
$vrai_{g,c_0} = vrai$

$$ (\phi \wedge \psi)_{g,c_0} = \phi_{g,c_0} \wedge \psi_{g,c_0} $$

$faux_{g,c_0} = faux$

$$ (\phi \vee \psi)_{g,c_0} = \phi_{g,c_0} \vee \psi_{g,c_0} $$

Cette construction élimine toutes les quantifications de variables associées à la couleur $c_0$. De nouvelles sont simultanément réintroduites au niveau des prédicats relationnels.

**Exemple 4.23** Supposons $C = \{1, 2\}$ et $\Sigma = \{R\}$ avec $|R| = 2$, alors on a

$$ (\exists x:1.R(x,x))_{\emptyset,2} = \exists x:1.R(x,x), $$

$$ (\exists x:1.R(x,x))_{\emptyset,1} = \exists z_1:1.\exists z_2:1.R(z_1,z_2). $$

Ainsi, dans le premier cas, lorsque l'on fusionne une couleur n'apparaisant pas dans la formule, celle-ci est inchangée. Le second cas montre comment, lorsqu'une variable de la couleur fusionnée est utilisée en plusieurs endroits, alors autant de nouvelles variables fraîches sont introduites (ici $z_1$ et $z_2$), celles-ci étant reliées par le fait qu'elles ont la même couleur.

Le dernier cas montre comment il est convenable de réinsérer la quantification au niveau du prédicat relationnel. Cette fois-ci $g(x_1) = 2$ et $g(x_2) = 2$.

$$ (\exists y:1.R(x_1,y) \wedge R(y,x_2))_{g,1} = (\exists z:1.R(x_1,z)) \wedge (\exists z:1.R(z,x_2)). $$

La preuve exacte de la validité de cette construction consiste à montrer par récurrence sur la structure de $\phi$ que :

$\gamma, \text{fusion}[c_0](S) \models \bar{g} \wedge \phi \quad \text{ssi} \quad \gamma, S \models \bar{g} \wedge \phi_{g,c_0}.$

Le lemme 4.9 traite le cas des prédicats relationnels.

□

**Lemme 4.24 (opérateur recol)** Soit $\alpha$ une application de $C$ dans $C$. Pour toute formule existentielle gardée $\bar{g} \wedge \phi$, il existe un formule existentielle avec quantifications gardées $\phi_\alpha$ telle que :

- $FV(\phi) \subseteq FV(\phi_\alpha)$,

- Pour toute $\Sigma$-structure $S$ et toute valuation $\gamma$ de $FV(\phi)$ sur $S$, on a

$$ \gamma, \text{recol}[\alpha](S) \models \bar{g} \wedge \phi \quad \text{ssi} \quad \gamma, S \models \bigvee_{\alpha \circ g' = g} \bar{g}' \wedge \phi_\alpha. $$

- Si $l_C(\phi) \le N$, alors $l_C(\phi_\alpha) \le N$.
**Preuve.** On définit $\phi_\alpha$ par récurrence sur $\phi$:

$$
\begin{align*}
R(x_1, \dots, x_{|R|})_{\alpha} &= R(x_1, \dots, x_{|R|}) && (\exists x : c. \phi)_{\alpha} = \bigvee_{c' \in \alpha^{-1}(c)} \exists x : c'. \phi_{\alpha}, \\
\text{vrai}_{\alpha} &= \text{vrai} && \text{faux}_{\alpha} = \text{faux} \\
(\phi \wedge \psi)_{\alpha} &= \phi_{\alpha} \wedge \psi_{\alpha} && (\phi \vee \psi)_{\alpha} = \phi_{\alpha} \vee \psi_{\alpha}
\end{align*}
$$

On montre par récurrence sur $\phi$ que pour toute garde $g'$ de $FV(\phi)$, toute
structure $\mathcal{S}$ et toute valuation de $FV(\phi)$ sur $\mathcal{S}$, on a

$$
\gamma, \text{recol}[\alpha](\mathcal{S}) \models \overline{\alpha \circ g'} \wedge \phi \quad \text{ssi} \quad \gamma, \mathcal{S} \models \overline{g'} \wedge \phi_{\alpha}.
$$

□

**Lemme 4.25 (opérateur ⊕)** *Pour toute formule existentielle gardée $\overline{g} \wedge \phi$, il existe un ensemble fini $\phi_g^{\oplus}$ de paires de formules existentielles gardées tel que :*

- pour tout $(\psi_1, \psi_2) \in \phi_g^{\oplus}, FV(\psi_1)$ et $FV(\psi_2)$ sont disjoints et $FV(\psi_1) \cup FV(\psi_2) \subseteq FV(\psi)$,

- pour toutes $\Sigma$-structures colorées $S_1$ et $S_2$ et toute valuation $\gamma$ de $FV(\phi)$ sur $S_1 \oplus S_2$ on a, $\gamma, S_1 \oplus S_2 \models \phi$ si et seulement si il existe $(\psi_1, \psi_2) \in \phi_g^{\oplus}$ tel que

$$
\begin{array}{ll}
\mathrm{FV}(\psi_1) \subseteq \mathrm{dom}(\pi_1 \circ \gamma), & \text{et } \pi_1 \circ \gamma, \mathcal{S}_1 \models \overline{g|_{\mathrm{FV}(\psi_1)}} \wedge \psi_1, \\
\text{et } \mathrm{FV}(\psi_2) \subseteq \mathrm{dom}(\pi_2 \circ \gamma), & \text{et } \pi_2 \circ \gamma, \mathcal{S}_2 \models \overline{g|_{\mathrm{FV}(\psi_2)}} \wedge \psi_2.
\end{array}
$$

- si $l_C(\phi) \le N$, alors pour tout $(\psi_1, \psi_2) \in \phi_g^{\oplus}$, $l_C(\psi_1) \le N$ et $l_C(\psi_2) \le N$.

**Preuve.** Par application du lemme 2.13.

□

**Lemmes de récurrence**

Soit $\mathcal{X} = \{x_1, \dots, x_N\}$. Pour tout $X \subseteq \mathcal{X}$, $F_{\exists}(X)$ représente l'ensemble des formules existentielles avec quantifications gardées $\phi$ dont les variables libres ap- partiennent à $X$ et telles que $l_C(\phi) \le N$. Modulo les équivalences syntaxiques habituelles, $F_{\exists}(X)$ est fini. Pour $X \subseteq \mathcal{X}, \bar{X}$ représente l'unique suite de variables $x_{p_1}, \dots, x_{p_n}$ telle que $p$ est strictement croissant et $\{x_{p_i} \mid i \in [n]\} = X$.

On construit une nouvelle signature $\Sigma'$ comme suit.

$$
\Sigma' = \{ \langle X, g, \phi \rangle \mid X \subseteq \mathcal{X}, g \in C^X, \phi \in F_{\exists}(X), \}, \\
\text{avec pour tout } \langle X, g, \phi \rangle \in \Sigma', |\langle X, g, \phi \rangle| = |X|.
$$
On définit aussi les interprétations $\mathcal{I}_0$ et $\mathcal{I}'_0$ comme suit.

$$ 
\begin{aligned}
\mathcal{I}_0 &= \left| \begin{array}{lcl} <X, g, \phi > (\bar{X}) & : & \bar{g} \wedge \phi \\ c(x) & : & c(x) \end{array} \right|, \\ 
\mathcal{I}'_0 &= \left| \begin{array}{lcl} <\emptyset, \emptyset, \text{vrai} > (\bar{X}) & : & \text{vrai} \\ <X, g, \phi > (\bar{X}) & : & <X, g, \phi > (\bar{X}) \end{array} \right|.
\end{aligned}
$$

L'interprétation $\mathcal{I}_0$ annote sur la structure l'ensemble des interprétations des formules de $F_{\exists}(X)$ pour $X \subseteq \mathcal{X}$. L'interprétation $\mathcal{I}'_0$ quant à elle laisse toute $\Sigma'$-structure inchangée si ce n'est que le symbole $<\emptyset, \emptyset, \text{vrai} >$ d'arité 0 a pour nouvelle valeur vrai. Remarquons que $\mathcal{I}_0(\perp) = \mathcal{I}'_0(\perp)$ et $\mathcal{I}'_0 \circ \mathcal{I}_0 = \mathcal{I}_0$.

Soit $E \subseteq C$ un ensemble de couleurs et $\mathcal{S}$ une structure colorée par $C$ alors $\mathcal{S}|_E$ dénote la structure induite de $\mathcal{S}$ par les éléments de couleurs dans $E$, c.a.d.

$$ \mathcal{S}|_E = \mathcal{S}|_{\{u \in \mathcal{U}^\mathcal{S} \mid \exists c \in E, c(u)\}}. $$

Le lemme 4.26 montre que cette opération commute avec les interprétations booléennes positives.

**Lemme 4.26** *Pour $\mathcal{I}$ une interprétation booléenne positive et $E \subseteq C$ un ensemble de couleurs, alors pour toute structure colorée $\mathcal{S}$,*

$$ \mathcal{I}(\mathcal{S})|_E = \mathcal{I}(\mathcal{S}|_E). $$

Les relations sur lesquelles reposent la construction sont alors les suivantes :

$$ \text{pour } E \subseteq C, \quad \mathcal{R}[E](\mathcal{S}, \mathcal{S}') \quad \text{ssi} \quad \mathcal{I}_0(\mathcal{S})|_E \approx \mathcal{I}'_0(\mathcal{S}'). $$

La relation $\mathcal{R}[E]$ relie continuellement les $\Sigma$-structures colorées aux $\Sigma'$-structures. L'interprétation $\mathcal{I}'_0$ ne sert qu'à obtenir $\mathcal{R}[E](\perp, \perp)$. Remarquons que si $\mathcal{I}_0(\mathcal{S}) = \mathcal{S}'$, alors $\mathcal{R}[E](\mathcal{S}, \mathcal{S}')$.

## L'équivalence

En annexe (A.2) se trouvent les lemmes A.5, A.6, A.8, A.9 et A.7 établissant la validité de chacune des étapes de récurrences. Techniquement, ces lemmes sont des applications directes des lemmes 4.21, 4.22, 4.24 et 4.25.

Le théorème suivant énonce la conclusion de toutes les constructions qui ont été présentées précédemment.

**Théorème 16** *Pour tout ensemble fini de couleurs $C$ et pour tout alphabet relationnel $\Sigma$, il existe un transducteur déterministe $t$ des $(VR' + \text{fusion})[\Sigma, C]$-termes dans les $VR'$-termes tel que pour tout $(VR' + \text{fusion})[\Sigma, C]$-terme $t$, on a :*

$$ [[t(t)]] \approx [[t]]. $$
**Preuve.** Les lemmes A.5, A.6, A.8, A.9 et A.7 correspondent aux étapes de récurrence de la preuve de validité du transducteur déterministe $t_0$ défini comme suit.

- l'ensemble des états est $\{q[E] \mid E \subseteq X\}$,

- l'état initial est $q[C]$,

- les transitions sont définies par

$$
\begin{align*}
q[E](x \oplus y) &\rightarrow f^{\oplus,E}(q[E](x) \oplus q[E](y)), \\
q[E](\mathbf{recol}[\alpha](x)) &\rightarrow f^{\mathbf{recol}[\alpha],E}(q[E^{\mathbf{recol}[\alpha]}](x)), \\
q[E](\mathcal{I}(x)) &\rightarrow f^{\mathcal{I},E}(q[E](x)), \\
q[E](\mathbf{fusion}[c_0](x)) &\rightarrow q[E](x) \qquad \text{si } |[x]|_{c_0} = 0, \\
q[E](\mathbf{fusion}[c_0](x)) &\rightarrow f^{\mathbf{fusion}[c_0],E}(q[E - \{c_0\}](x)) \qquad \text{sinon.}
\end{align*}
$$

Des lemmes A.5, A.6, A.8, A.9, A.7 et 3.59 se déduit la validité de ce transducteur. On a donc pour tout $(\mathbf{VR}'+\mathbf{fusion})[\Sigma, C]$-terme $t$, $\mathcal{R}[C]([\mathbf{t}], [[\mathbf{t}_0(t)]])$, c'est-à-dire que $\mathcal{I}_0([\mathbf{t}]) \approx \mathcal{I}'_0([\mathbf{t}_0(t)])$.

Soit l'interprétation booléenne positive suivante :

$$
\mathcal{I}_1 = \left| R(\overline{X}) : \bigvee_{g \in C^X} <X, g, \phi > (\overline{X}), X = \{x_1, \dots, x_{|R|}\} \right|.
$$

Alors pour toute $\Sigma$-structure colorée $S$, on a $\mathcal{I}_1(\mathcal{I}_0(S)) = S$. On pose donc $\mathbf{t} = \mathcal{I}_1 \circ \mathcal{I}'_0 \circ \mathbf{t}_0$, et $\mathbf{t}$ satisfait les conclusions du théorème 16. $\square$

4.4.2 Représentation interne

Les graphes solutions des VR-systèmes d’équations admettent une représentation interne sous forme de récriture de mots. Nous présentons d’abord les définitions originales de Caucal puis le résultat d’équivalence énoncé par Barthelmann : ces travaux se limitent au cas des systèmes finis d’équations. Ensuite, après reformulation, nous généralisons ce résultat en en donnant une forme restant valable pour des systèmes d’équations non finis et pour les opérations VR’.

4.4.2.1 Graphes préfixes reconnaissables

La première définition que nous donnons de ces graphes correspond à la simple extension des graphes préfixes à des ensembles rationnels de règles.

**Définition 4.27 (graphe préfixe reconnaissable)** *Un graphe est préfixe reconnaissable si il est isomorphe au graphe de sommets V et dont les arcs étiquetés par a sont définis par*

$$
\to^a = \{ (uv, u'v) \in V^2 \mid (U, a, U') \in \Delta, u \in U, u' \in U' \} \text{ avec}
$$
<figure><img src="image_32.png" /><figcaption>FIG. 4.7 – Un graphe préfixe reconnaissable.</figcaption></figure>

- $\Sigma$ un alphabet fini,

- $V$ une partie rationnelle de $\Sigma^*$,

- $\Delta$ un ensemble fini de triplets $(U, a, U')$ où $U$ et $U'$ sont des parties rationnelles de $\Sigma^*$ et $a$ est une étiquette.

On peut noter pour plus de simplicité les relations de ce graphe par :

$$ \xrightarrow{a} = \left( \bigcup_{(U,a,U') \in \Delta} (U \times U') \Sigma^* \right) \Big|_V . $$

**Exemple 4.28** La figure 4.7 donne un exemple de graphe préfixe reconnaissable. Il s'agit de la demi-droite étiquetée par $a$ et augmentée de la relation d'accessibilité étiquetée par $b$ (c'est à dire les entiers munis de la relation successeur et de la relation $\le$).

L'alphabet est $\Sigma = \{A\}$, l'ensemble de sommets est $V = A^*$ et

$$ \Delta = \{(\varepsilon, a, A), (\varepsilon, b, A^*)\} . $$

Pour décrire un graphe préfixe reconnaissable il peut être pratique d'utiliser des règles gardées de récriture. On peut ainsi utiliser un ensemble rationnel de suffixes autorisés pour chaque règle. Cette extension n'enrichit pas la famille de graphes comme le formalise le théorème suivant.

**Théorème 17 (Caucal [Cau96])** Un graphe est préfixe reconnaissable si et seulement si il est isomorphe au graphe de sommets $V$ et dont les arcs étiquetés par $a$ sont définis par

$$ \xrightarrow{a} = \{(uw, u'w) \mid (U, a, U', W) \in \Delta, u \in U, u' \in U', w \in W\} \text{ avec} $$

- $\Sigma$ un alphabet fini,
- V une partie rationnelle de $\Sigma^*$,

- $\Delta$ un ensemble fini de quadruplets $(U, a, U', W)$ où $a$ est une étiquette et $U, U'$ et $W$ sont des parties rationnelles de $\Sigma^*$.

Remarquons que cette équivalence n’est valable qu’à isomorphisme près. Comme pour la définition originale des préfixes reconnaissables, on peut donner une notation compacte de ce type de récriture:

$$ \underset{(U,a,U',W) \in \Delta}{\stackrel{a}{\rightarrow}} = \bigcup (U \times U')W . $$

Le résultat fondamental de décidabilité pour la famille des graphes préfixes reconnaissables est donné par le théorème 18.

**Théorème 18 (Caucal [Cau96])** *La théorie monadique des graphes préfixes reconnaissables est décidable.*

Pour établir ce résultat, Caucal montre que ces graphes s’obtiennent pas interprétation monadique de l’arbre binaire complet. Nous empruntons un chemin similaire dans la suite de ce travail.

**Théorème 19 (Barthelmann [Bar97])** *Les graphes préfixes reconnaissables sont les graphes solutions de VR-systèmes finis d’équations.*

Dans ce travail, nous étendons ce résultat aux structures (ce qui a déjà été considéré par Barthelmann [Bar97] et Blumensath [Blu01]), et surtout en autorisant la restriction du graphe préfixe reconnaissable par un langage reconnu par un automate infini. Dans ce paragraphe, une moitié de ce résultat est énoncé; il s’agit du théorème 20. La réciproque est montrée ultérieurement en passant par une étape intermédiaire (plus précisément en appliquant le théorème 23 puis le théorème 24).

### 4.4.2.2 Les relations PR

Il s’agit ici de généraliser la notation $(U \times V)W$ pour représenter cette fois-ci des relations $n$-aires sur les mots. On fait aussi le choix, pour des raisons d’homogénéité avec le reste de ce travail, de ne plus considérer des relations «préfixes reconnaissables» [Cau96], mais plutôt ce qui devrait symétriquement s’appeler des relations suffixes reconnaissables, c.a.d. correspondant à la notation $U(V \times W)$. Bien entendu, ces deux approches produisent des graphes isomorphes (pourvu que l’on ne mélange pas ces deux types de règles dans un même graphe). Les relations ainsi définies sont néanmoins appelées relations PR (pour préfixe reconnaissable) dans le reste de ce travail.

Les relations PR ont été introduites pour la première fois dans [CC03]. Une notion similaire a été présentée antérieurement par Blumensath [Blu01] ou encore
dans [NT01]. La définition peut aussi être attribuée à Caucal [Cau96] qui utilisait
déja la notation $(U \times V)W$ pour représenter les relation élémentaires dont sont
formés les graphes préfixes reconnaissables.

Soit $\mathbf{A}$ un alphabet fini, soit $N$ son cardinal et soient $a_1, \dots, a_N$ les lettres qui le composent. Les relations $\mathbf{PR}$ sur $\mathbf{A}$ sont définies par récurrence comme suit :

- la relation non vide $\{()\}$ d'arité 0 est une relation $\mathbf{PR}$,

- le singleton $\{\varepsilon\}$ est une relation $\mathbf{PR}$ d'arité 1 notée $\varepsilon$,

- soit $R$ une relation $\mathbf{PR}$ d'arité $n$ et $L$ un langage rationnel sur $\mathbf{A}^*$, la relation $L.R$ est une relation $\mathbf{PR}$ d'arité $n$ définie par

$$
L.R = \{(uv_1, \dots, uv_n) \mid u \in L, (v_1, \dots, v_n) \in R\},
$$

- l'union de deux relations $\mathbf{PR}$ de même arité est une relation $\mathbf{PR}$,

- soit $R$ une relation $\mathbf{PR}$ d'arité $n$ et $R'$ une relation $\mathbf{PR}$ d'arité $n'$, la relation $R \times R'$ est une relation $\mathbf{PR}$ d'arité $n + n'$ définie par

$$
R \times R' = \{(u_1, \dots, u_n, v_1, \dots, v_{n'}) \mid (u_1, \dots, u_n) \in R, (v_1, \dots, v_{n'}) \in R'\},
$$

- soit $R$ une relation $\mathbf{PR}$ d'arité $n$ et $\sigma$ une permutation de $[1, n]$, alors $\sigma(R)$ est une relation $\mathbf{PR}$ d'arité $n$ définie par

$$
\sigma(R) = \{(u_1, \dots, u_n) \mid (u_{\sigma(1)}, \dots, u_{\sigma(n)}) \in R\}.
$$

**Exemple 4.29** Les langages rationnels sont des relations PR d'arité 1 car un tel langage $L$ s'écrit $L.\varepsilon$. On écrit alors simplement $L$ à la place de $L.\varepsilon$. La relation vide d'arité $n \ge 1$ est PR car elle s'écrit $\emptyset.(\varepsilon \times \cdots \times \varepsilon)$ (et $\emptyset$ est rationnel). Toute relation singleton $\{(u_1, \dots, u_n)\}$ est PR car elle s'écrit $u_1 \times \cdots \times u_n$ (et chaque $\{u_i\}$ est un langage rationnel). Toutes les relations finies sont PR car ce sont des unions de singletons. Plus généralement, toutes les relations reconnaissables sont PR : elles s'écrivent comme une union finie de produits le langages reconnaissables d'après le théorème de Mezei [Eil74].

La relation égalité $\{(u, u) \mid u \in \mathbf{A}^*\}$ est PR car elle s'écrit $\mathbf{A}^*.(\varepsilon \times \varepsilon)$. La relation différent $\{(u, v) \mid u \in \mathbf{A}^*, v \in \mathbf{A}^*, u \neq v\}$ est PR car elle s'écrit

$$
\mathbf{A}^*.(\varepsilon \times \mathbf{A}^+) \cup \mathbf{A}^*.(\mathbf{A}^+ \times \varepsilon) \cup \bigcup_{\substack{a,b \in \mathbf{A} \\ a \neq b}} \mathbf{A}^*.(a.\mathbf{A}^* \times b.\mathbf{A}^*)
$$

Pour $R$ une relation sur $\mathbf{A}^*$, $\mathrm{Res}(R)$ est le plus petit ensemble de relations contenant $R$ et clos par :

**Projection.** Pour $R' \in \mathrm{Res}(R)$ et $k \in [|R'|]$,

$$
\{(u_1, \dots, u_{k-1}, u_{k+1}, \dots, u_{|R'|}) \mid (u_1, \dots, u_{|R'|}) \in R'\} \in \mathrm{Res}(R).
$$
**Résidu à gauche.** Pour $a \in \mathbf{A}$ et $R' \in \mathrm{Res}(R)$,

$$ \{(u_1, \dots, u_{|R'|}) \mid a.(u_1, \dots, u_{|R'|}) \in R'\} \in \mathrm{Res}(R). $$

**Lemme 4.30** *Pour toute relation PR $R$ sur $\mathbf{A}^*$, $\mathrm{Res}(R)$ est fini et ne contient que des relations PR.*

**Preuve.** Standard. Par récurrence sur la définition de $R$, en utilisant le fait que les résidus d'un langage rationnel sont finis, et que le résidu d'un produit est le produit des résidus. $\square$

La remarque suivante, montre qu'une forme de réciproque est aussi vraie.

**Remarque 4.31** *Une relation $R$ est PR si et seulement si $\mathrm{Res}(R)$ est fini.*

**Lemme 4.32** *Pour toute relation $R$ sur $\mathbf{A}^*$, il existe un ensemble fini $\mathrm{dec}(R)$ de $(N+1)$-uplets $(\sigma, R_1, \dots, R_N)$ où $\sigma$ est une permutation de $[|R|]$, les $R_i \in \mathrm{Res}(R)$ sont des relations et*

$$ R = \bigcup_{(\sigma, R_1, \dots, R_N, k) \in \mathrm{dec}(R)} \sigma(a_1.R_1 \times \dots \times a_N.R_N \times \varepsilon^k) \quad \text{où } k = |R| - \sum_{i \in [N]} |R_i| . $$

**Preuve.** Standard. Toujours par récurrence sur la structure de $R$. $\square$

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

**Traduction de PR vers VR'**

Considérons un ensemble fini $T$ de relations PR tel que $\mathrm{Res}(T) = T$. On définit la signature $\Sigma[T]$ par $\Sigma[T] = \{< R > \mid R \in T\}$ avec $< R > \mid$ l'arité de $R$. Soit $S_T$ la $\Sigma[T]$-structure dont l'univers est $\mathbf{A}^*$ et telle que $< R >^{S_T} = R$ pour tout $R \in T$.

**Lemme 4.33** *Il existe un transducteur déterministe $\mathbf{t}_T$ des $\mathbf{Auto}_d[\mathbf{A}]$-termes<fnref n="2" /> dans les VR'-termes tel que pour tout $\mathbf{Auto}_d[\mathbf{A}]$-terme $t$,*

$$ [[\mathbf{t}_T(t)]] \approx \mathcal{S}_T|_{[t]} . $$

**Construction.** On utilise le transducteur $\mathbf{t}_T$ possédant un unique état $q$ (init- tial) et dont les transitions sont les suivantes:

$$ \begin{align*} q(a_1x_1 + \dots + a_Nx_N) &= \mathcal{I}(\mathcal{I}_{a_1}(q(x_1)) \oplus \dots \oplus \mathcal{I}_{a_N}(q(x_N))) \\ q(a_1x_1 + \dots + a_Nx_N + \varepsilon) &= \mathcal{I}(\mathcal{I}_{a_1}(q(x_1)) \oplus \dots \oplus \mathcal{I}_{a_N}(q(x_N)) \oplus \mathrm{un}[\emptyset]) \end{align*} $$

<footnote n="2">2. Tous les termes considérés dans ces résultats de conversions ne sont pas nécessairement finis. Nous ne précisions plus ce point dans la suite du mémoire.</footnote>
$$
\text{avec } \mathcal{I}_a = \begin{array}{c} <R>_a(x_1, \dots, x_{|R|}) : <R>_a(x_1, \dots, x_{|R|}), R \in T \\ <R>_a(x_1, \dots, x_{|R|}) : \bigwedge_{i \in [N]} <R_i>_a (y_1^i, \dots, y_{|R_i|}^i) \wedge \bigwedge_{j \in [k]} \circ(z_j) \\ \text{et } \mathcal{I} = \text{ pour } (\sigma, R_1, \dots, R_N, k) \in \text{dec}(R) \\ \text{ et } (y_1^1, \dots, y_{|R_1|}^1, \dots, y_1^N, \dots, y_{|R_N|}^N, z_1, \dots, z_k) \\ = (x_{\sigma(1)}, \dots, x_{\sigma(|R|)}) \end{array}
\qquad \square
$$

Le théorème suivant énonce que toute structure dont l'univers est accepté par un automate déterministe et dont les relations sont PR (restreintes à l'univers) est isomorphe à la solution d'un VR'-système d'équations, et cette traduction s'effectue au moyen d'un transducteur déterministe. Ainsi, ce résultat établit un lien entre une représentation interne (un univers décrit par un automate et des relations décrites explicitement) et une représentation équationnelle. Nous verrons dans la suite que la réciproque est aussi vraie. Notons que la version originale de ce résultat ne fait pas intervenir la notion de transducteur déterministe.

**Théorème 20 (Carayol, Colcombet [CC03])** Soit $\mathbf{A}$ un alphabet, $\dot{R}_1, \dots, \dot{R}_n$ des symboles relationnels et $R_1, \dots, R_n$ des relations PR sur $\mathbf{A}^*$ telles que l'arité de $\dot{R}_i$ soit $|R_i|$. Il existe un transducteur déterministe $\mathbf{t}$ des Auto$_d[\mathbf{A}]$-termes dans les VR'-termes tel que

$$
S \approx [\mathbf{t}(t)] \quad \text{avec } S \text{ tel que } \begin{cases} \mathcal{U}_S = [t], \\ \dot{R}_i^S = R_i \cap [t]^{|R_i|}. \end{cases}
$$

**Preuve.** Soit $T = \text{Res}(\{R_1, \dots, R_n\})$. L'ensemble $T$ est fini d'après le lemme 4.30. En appliquant alors le lemme 4.33, on obtient un transducteur $t_T$ satisfaisant les conclusions du lemme. On a alors $S \approx \mathcal{I}(t_T(t))$ avec

$$
\mathcal{I} = \left| \dot{R}_i(x_1, \dots, x_{|\dot{R}_i|}) : <R_i> (x_1, \dots, x_{|R_i|}) \right| .
$$

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

4.4.3 Représentation par transformations

4.4.3.1 Premier contact

Une dernière façon de représenter les graphes préfixes reconnaissables est de partir de l'arbre binaire et d'effectuer une succession de transformations sur ces
graphes. Le premier de ces résultats est dû à Caucal et a permis la preuve de la
décidabilité de la théorie monadique de ces graphes.

**Théorème 21 (Caucal [Cau96])** *Les graphes préfixes reconnaissables sont les graphes obtenus par marquage rationnel, substitution rationnelle inverse et élimination de sommets marqués de l'arbre binaire.*

Cette approche ne convient qu'aux graphes puisque la substitution rationnelle inverse ne peut mettre en relation que deux sommets. Barthelmann présente une version logique de ce résultat, en termes d'interprétations.

**Théorème 22 (Barthelmann [Bar97])** *Les graphes préfixes reconnaissables sont les transductions monadiques de l'arbre binaire complet.*

Ce résultat se prolonge naturellement en une définition de structures «préfixes reconnaissables» particulièrement simple: ce sont les structures obtenues par *transductions monadiques de l'arbre binaire*.

Nous verrons que cette définition est bien compatible avec les autres définitions : les solutions des VR'-systèmes finis d'équations, et les structures sur les mots dont l'interprétation de chaque symbole est une relation PR.

**Théorème 23 (Barthelmann [Bar97])** *Pour toute signature $\Sigma$ il existe une interprétation monadique $\mathcal{I}$ telle que pour tout $VR'[\Sigma]$-terme $t$,*

$$ \mathcal{I}(t) \approx [t]. $$

Nous présentons ci-dessous une preuve similaire pour une famille plus générale de structures. La remarque 5.29 page 146 revient sur ce point.

### 4.4.3.2 Des transductions monadiques vers les relations PR

Il nous reste donc à établir que toute structure obtenue comme interprétation monadique du dépliage d'un graphe peut être obtenue comme valeur d'un VRS'-système d'équations (théorème 24). De plus, passer du graphe au système d'équations s'effectue par application d'une interprétation monadique.

**Théorème 24 (Carayol, Colcombet [CC03])** *Pour tout alphabet $\mathbf{A}$, tout alphabet relationnel $\Sigma$ et toute interprétation monadique $\mathcal{I}$ des $\mathbf{A}$-arbres déterministes dans les $\Sigma$-structures, il existe des relations $\mathrm{PR}(\dot{\mathbf{R}})_{R \in \Sigma}$ sur $\{0,1\}^* \text{ telles que } |\dot{\mathbf{R}}| = |\mathbf{R}| \text{ et une transduction monadique } \mathbf{T} \text{ des graphes déterministes vers les } \mathrm{Auto}_d\text{-systèmes d'équations tels que pour tout graphe enraciné déterministe } \mathcal{G}, \text{ on a }*

$$ \mathcal{I}(\mathrm{Depliage}(\mathcal{G})) \approx \mathcal{S} \quad \text{avec } \mathcal{S} \text{ tel que } \begin{cases} \mathcal{U}_\mathcal{S} = \mathrm{Solution}(\mathbf{T}(\mathcal{G})), \\ \mathcal{R}^\mathcal{S} = \dot{\mathbf{R}} \cap \mathrm{Solution}(\mathbf{T}(\mathcal{G}))^{|\mathbf{R}|}. \end{cases} $$

Nous ne prouvons pas cette implication qui est similaire à la preuve du lemme 5.30 (cette dernière est en fait plus complexe).
### 4.4.4 Application à la hiérarchie de Caucal

Le dépliage des graphes finis donne les arbres réguliers de degré fini. L'application des substitutions rationnelles inverses sur les arbres réguliers donne les graphes préfixe reconnaissables. Que se passe-t-il quand on itère ces deux opérations ? Cela définit les graphes de la hiérarchie de Caucal.

**Définition 4.34** *Les graphes du niveau zéro sont les graphes finis. Pour un entier strictement positif n, les graphes du niveau n de la hiérarchie s'obtiennent par application d'un dépliage suivi d'une substitution rationnelle inverse et d'une élimination de sommets marqués<fnref n="3" /> à un graphe du niveau n – 1 de la hiérarchie.*
Il s'agit de la première définition de cette famille [Cau98]. Seule une propriété de ces graphes était connue à ce moment : ils possèdent une théorie monadique décidable. Cette propriété est évidente puisqu'elle résulte de la préservation bien connue de la décidabilité de la théorie monadique par toutes les transformations mises en jeu.

L'intérêt pour cette famille n'est revenu que plus tard à la lumière de récents travaux sur les termes infinis. Knapik, Niwinsky et Urzyczyn montrent que les termes infinis solutions de schémas de programme récursifs d'ordre supérieur (sous une certaine hypothèse de «sûreté») possèdent une théorie monadique décidable [KNU02]. (Courcelle avait déjà montré une version à l'ordre deux de ce résultat [Cou95]). A peu près simultanément, Courcelle et Knapik montrent un résultat similaire sur une famille de termes obtenus par applications successives d'une certaine forme de «substitutions» [CK02]. Caucal montre alors que ces deux familles de termes sont égales et qu'elles coïncident avec les termes obtenus par dépliage des graphes de la hiérarchie.

D'autres travaux sur le sujet montrent la robustesse de cette famille. L'aspect représentation est étudié par Carayol et l'auteur dans [CC03]. Des investigations de structures et de clôture sont présentées dans [CW03]. Dans une thématique plus éloignée, des travaux sont menés sous l'angle des jeux de parité<fnref n="4" /> [Cac03].

### 4.4.5 Liens entre VR et HR

Remarquons tout d'abord que les familles de graphes obtenues comme solutions de VR-systèmes d'équations sont nécessairement distinctes des familles de graphes obtenues comme solution de HR-systèmes d'équations. Il s'agit d'une conséquence de la propriété 4.35.

<footnote n="3">3. L'élimination des sommets marqués n'existe pas dans le travail original de Caucal. Elle arrive naturellement lorsque l'on considère ces graphes sous l'angle de la logique.</footnote>

<footnote n="4">4. Les jeux de parité donnent une description alternative sous forme de jeu du $\mu$-calcul modal. Décider si un joueur possède une stratégie gagnante d'un de ces jeux est équivalent à décider de la satisfaction d'une formule du $\mu$-calcul modal. Cette équivalence est particulièrement riche d'enseignements.</footnote>
**Propriété 4.35** *Il existe un graphe solution d'un VR-système fini d'équations qui n'est pas de largeur arborescente bornée.*

**Preuve.** Il suffit de considérer le graphe préfixe reconnaissable de la figure 4.7 (page 117). Modulo nommage, orientation des arcs et absence des boucles, il s'agit de la clique infinie qui n'est pas de largeur arborescente bornée. □

Barthelmann a montré que, si l'on contraint un graphe solution d'un VR-système d'équations fini à ne pas contenir de graphe biparti complet aussi grand que l'on veut (une contrainte moins forte que la finitude de la largeur arborescente), alors ce graphe est HR-équationnel.

**Théorème 25 (Barthelmann [Bar98])** *Les graphes VR-équationnels dont les sous-graphes bipartis complets sont bornés sont HR-équationnels.*

Nous redémontrons ce résultat dans le présent paragraphe. Le principe des preuves est similaire. L'apport consiste à utiliser les transducteurs déterministes comme unique outil de traduction. La preuve reste ainsi valable pour tout système d'équations.

### 4.4.5.1 Intuitions sur la preuve

Supposons que l'on applique une opération $arc[c, a, c']$ à un graphe contenant un unique sommet de couleur $c$ et un «grand nombre de sommets» de couleur $c'$. Il est impossible d'obtenir le même résultat au moyen d'opérateurs HR. En effet, ajouter un arc à un sommet de couleur $c'$ à l'aide d'opérateurs HR nécessite de fusionner les sommets de couleur $c'$ et ceci n'a absolument pas l'effet souhaité (il n'y aurait plus qu'un seul sommet de couleur $c'$ au lieu d'un «grand nombre»).

La seule solution est donc d'anticiper l'opérateur $arc[c, a, c']$ et de produire un graphe dans lequel ces arcs sont déja présents. Ceci justifie la présence, dans chaque état du transducteur que l'on construit, d'un ensemble (appelé $D$ dans la suite) collectant l'ensemble des arcs qu'il faut produire «en plus». Dans le cas présent, cet ensemble est augmenté de $(c, a, c')$ lorsque le transducteur consomme l'opérateur $arc[c, a, c']$. Il s'agit de la technique fondamentale de la construction.

Tout ceci fonctionne bien jusqu'à la rencontre d'un opérateur d'union disjointe. Il est alors nécessaire de produire de nouveaux sommets utilisant des couleurs fraîches afin de pouvoir propager les arcs à produire vers les deux arguments de l'union. L'ensemble des nouvelles couleurs (noté $E$ dans la suite) est ainsi susceptible d'augmenter. Il est néanmoins possible d'en borner le nombre en utilisant l'hypothèse sur les graphes bipartis complets. Ceci permet de garantir que le transducteur possède un nombre fini d'états.

Ces remarques permettent de donner une première ébauche d'hypothèse de récurrence. Étant donnés un graphe coloré par $C$ (décrit par un VR-terme), un
nouvel ensemble de couleur E et un ensemble d'arcs $D \subseteq (E \cup C) \times A \times (E \cup C)$, il s'agit de produire un graphe $\mathcal{H}$ (décrit par un HR-terme) coloré par $E \cup C$ tel que :

$$ \mathrm{arc}[D](\mathrm{sommet}[E] \oplus \mathcal{G}) \approx \mathcal{H}. $$

Le détail de la preuve est technique. La première partie de la démonstration (4.4.5.2) consiste à normaliser les VR-termes afin que chaque couleur utile soit utilisée par un unique sommet ou par un «grand nombre» de sommets. Certaines propriétés générale sont ensuite mentionnées (4.4.5.3). On présente alors les hypothèses de récurrence (4.4.5.4). Le paragraphe 4.4.5.5 conclut.

### 4.4.5.2 Normalisation

L'opération fusion ne peut opérer que sur une couleurs à la fois, et tous les sommets de cette couleur se retrouvent identifiés. Ce n'est pas le cas de l'opération arc. Pour cette raison, les couleurs n'affectant qu'un unique sommet dans un graphe jouent un rôle particulier dans la preuve du théorème 26. L'objectif de ce paragraphe, formalisé par le lemme 4.37, est de normaliser un système d'équations vis à vis de cette problématique.

Le premier outil dont nous avons besoin est la possibilité de compter le nombre de sommets d'une certaine couleur dans un graphe. Soient donc $\mathcal{G}$ un graphe coloré et $c$ une couleur, on pose $|\mathcal{G}|_c = |\{v \in V_{\mathcal{G}} | \mathcal{G} \models c(v)\}|$.

**Lemme 4.36** Soient $k$ un entier positif et $c$ une couleur, l'ensemble $\{\mathcal{G} \mid |\mathcal{G}|_c = k\}$ est VR-$\mu$-définissable.

**Preuve.** On a les égalités suivantes :

$$ \begin{align*} |\mathrm{sommet}[c_0]|_c &= \begin{cases} 0 & \text{si } c \neq c_0 \\ 1 & \text{si } c = c_0, \end{cases} & |\mathcal{G} \oplus \mathcal{G}'|_c &= |\mathcal{G}|_c + |\mathcal{G}'|_c, \\ |\mathrm{recol}[\alpha](\mathcal{G})|_c &= \sum_{\alpha(c')=c} |\mathcal{G}|_{c'}, & |\mathrm{arc}[c_0, a, c_1](\mathcal{G})|_c &= |\mathcal{G}|_c, \\ |\perp|_c &= 0 \end{align*} $$

Ces équivalences s'interprètent comme un transducteur déterministe sans antécipation des VR-termes vers les $N$-termes (voir exemple ?? page ??). Le singleton $\{k\}$ étant $N$-$\mu$-définissable et l'image inverse d'un ensemble $\mu$-définissable par un transducteur déterministe étant $\mu$-définissable (lemme 3.48), on obtient que $\{\mathcal{G} \mid |\mathcal{G}|_c = k\}$ est VR-$\mu$-définissable. $\square$

Supposons $k$ fixé. On peut dès lors, en faisant usage d'un transducteur déterministe, assurer que toutes les couleurs apparaissant dans un calcul affectent 0,
1 ou plus de $k$ sommets. Ainsi, on dit qu’un graphe $\mathcal{G}$ satisfait la propriété (*) si pour toute couleur $c$, $|\mathcal{G}|_c \notin \{2, \dots, k\}$. Le lemme 4.37 nous permet de supposer cette propriété lorsque l’on utilise les opérateurs VR.

**Lemme 4.37** Soient $C$ un ensemble de couleurs et $A$ un ensemble d’étiquettes. Il existe un nouvel ensemble de couleurs $C'$, un transducteur déterministe $t$ des VR[$A, C$]-termes dans les VR[$A, C'$]-termes et une application $\beta$ de $C'$ dans $C$ tels que

1. pour tout VR[$A, C$]-terme $t$, $\text{recol}[\beta](\llbracket t(t) \rrbracket) = \llbracket t \rrbracket$,

2. pour tout sous-terme $t'$ de $t(t)$, $\llbracket t' \rrbracket$ satisfait (*).

Le preuve se trouve à l’annexe A.3, page A.3.

### 4.4.5.3 Premières propriétés

On suppose dorénavant que $k$ est pair, et on s’intéresse à la propriété pour un graphe de ne pas contenir un sous-graphe biparti complet de taille $k/2$. Le choix de $k/2$ est explicité par le lemme ci-dessous.

**Lemme 4.38** Soient $\mathcal{G}$ un graphe, $c, c'$ deux couleurs et $a$ une étiquette. Si $|\mathcal{G}|_c > k$ et $|\mathcal{G}|_{c'} \ge k$, alors $\text{arc}[c, a, c'](\mathcal{G})$ contient un graphe biparti complet de taille $k/2$.

Dans la suite, l’ensemble de couleurs $C$ est fixé. Soit $\mathcal{G}$ un graphe coloré par $C$ satisfaisant (*). On pose $C_0(\mathcal{G}) = \{c \in C \mid |\mathcal{G}|_c = 0\}$, $C_1(\mathcal{G}) = \{c \in C \mid |\mathcal{G}|_c = 1\}$ et $C_+(\mathcal{G}) = \{c \in C \mid |\mathcal{G}|_c \ge k\}$. La propriété (*) équivaut alors à $C = C_0(\mathcal{G}) \cup C_1(\mathcal{G}) \cup C_+(\mathcal{G})$.

Soient $E \subseteq C$ et $E' \subseteq C$ deux ensembles de couleurs, alors $D(E, E')$ représente l’ensemble $(E \times A \times E') \cup (E' \times A \times E)$, c’est-à-dire le plus grand ensemble $D$ tel que $\text{arc}[D]$ n’ajoute des arcs qu’entre des sommets de couleurs $E$ et des sommets de couleur $E'$. Pour $D \subseteq D(C, C)$, alors $C(D)$ représente l’ensemble $\{c \mid (c, a, c') \in D \text{ ou } (c', a, c) \in D\}$, c’est-à-dire l’ensemble des couleurs apparaissant dans $D$.

Nous mentionnons ici certaines propriétés des opérateurs VR+fusion qui seront utilisées implicitement par la suite.

$$ \text{fusion}[E] \circ \text{fusion}[E'] = \text{fusion}[E \cup E'] = \text{fusion}[E'] \circ \text{fusion}[E] $$

$$ \text{arc}[D] \circ \text{arc}[D'] = \text{arc}[D \cup D'] = \text{arc}[D'] \circ \text{arc}[D] $$

$$ \text{fusion}[E] \circ \text{arc}[D] = \text{arc}[D] \circ \text{fusion}[E] $$

$$ \text{fusion}[E](\mathcal{G}) = \mathcal{G} \quad \text{si } E \cap C(\mathcal{G}) \subseteq C_1(\mathcal{G}) $$

$$ \text{fusion}[E](\mathcal{G}) \approx \text{fusion}[E](\mathcal{G} \oplus \text{sommet}[E]) \quad \text{si } E \subseteq C(\mathcal{G}) $$

Enfin, deux dernières égalités nous sont utiles.
**Lemme 4.39** Soient deux graphes colorés $\mathcal{G}$ et $\mathcal{H}$, $E \subseteq C$ et $D \subseteq D(C, C)$.

$$ \text{Si } C(\mathcal{H}) \cap C(D) \subseteq C(\mathcal{G}) \cap E \quad \text{alors} \\ \text{fusion}[E](\text{arc}[D](\mathcal{G} \oplus \mathcal{H})) = \text{fusion}[E](\text{arc}[D](\mathcal{G}) \oplus \mathcal{H}). $$

La seconde égalité s'obtient par double application de la précédente.

**Lemme 4.40** Soient deux graphes colorés $\mathcal{G}$ et $\mathcal{H}$, $E \subseteq C(\mathcal{G}) \cap C(\mathcal{H})$ et $D \subseteq D(E, C)$. Alors,

$$ \text{fusion}[E](\text{arc}[D](\mathcal{G} \oplus \mathcal{H})) = \text{fusion}[E](\text{arc}[D](\mathcal{G}) \oplus \text{arc}[D](\mathcal{H})). $$

#### 4.4.5.4 Hypothèses de récurrence

On construit maintenant les relations continues $\mathcal{R}$ et $\mathcal{R}'$ qui correspondent aux invariants associés aux états du transducteur déterministe que l'on cherche à obtenir.

La relation $\mathcal{R}$ a pour paramètres $\mathcal{G}^{\infty}$, $E$ et $D$ satisfaisant (A),(B) et (C) définis comme suit.

(A) $E$ est un ensemble de couleurs fraîches (c.a.d. $C \cap E = \emptyset$),

(B) $D \subseteq D(C \cup E, C \cup E)$,

(C) $\text{arc}[D](\text{sommet}[E] \oplus \mathcal{G}^{\infty})$ ne contient pas de graphe biparti complet de taille $k/2$.

La relation $\mathcal{R}[\mathcal{G}^{\infty}, E, D](\mathcal{G}, \mathcal{H})$, où $\mathcal{G}$ est un graphe coloré par $C$ et $\mathcal{H}$ un graphe coloré par $C \cup E$ est alors satisfaite si

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

- $C_1(\mathcal{G}) = C_1(\mathcal{G}^{\infty})$,

- et $\text{arc}[D](\text{sommet}[E] \oplus \mathcal{G}) \approx \mathcal{H}$.

Pour tous $\mathcal{G}^{\infty}$, $E$ et $D$, $\mathcal{R}[\mathcal{G}^{\infty}, E, D]$ relie continuellement les graphes colorés par $C$ aux graphes colorés par $C \cup E$.

La relation $\mathcal{R}'[\mathcal{G}^{\infty}, E, D](\mathcal{G}, \mathcal{H})$ est un raffinement de $\mathcal{R}$. En effet, $\mathcal{R}'[\mathcal{G}^{\infty}, E, D]$ n'est définie que si

(D) $D \subseteq D(C_1(\mathcal{G}^{\infty}) \cup E, C_+(\mathcal{G}^{\infty}))$,

(E) et $E \subseteq C(D)$,

et dans ce cas $\mathcal{R}'[\mathcal{G}^{\infty}, E, D](\mathcal{G}, \mathcal{H})$ ssi $\mathcal{R}[\mathcal{G}^{\infty}, E, D](\mathcal{G}, \mathcal{H})$.

La relation $\mathcal{R}'$ permet, par rapport à $\mathcal{R}$, de borner le nombre de couleurs nécessaire dans $E$ (et par conséquent le nombre d'états du transducteur déterministe).

**Lemme 4.41** Il existe un entier $K$ (dépendant de $k$, $|C|$ et $|A|$) tel que pour tout graphe coloré $\mathcal{G}^{\infty}$, $E$ et $D$ satisfaisant (A-E), on a $|E| \le K$.
**Preuve.** Soit $C'_1 = C_1(\mathcal{G}^\infty) \cup E, C_+ = C_+(\mathcal{G}^\infty)$ et soit $K = 2k|C||A|$. D'après (D-E), $|D| \ge |E| \ge K$. Supposons sans perdre de généralité (cf hypothèse D) que $|D \cap (C'_1 \times A \times C_+)| \ge K/2$. Alors, il existe $a$ et $c \in C_+(\mathcal{G}^\infty)$ tel que $|D'| \ge k$, avec $D' = D \cap (C'_1 \times \{a\} \times \{c\})$. Par suite $\mathrm{arc}[D'](\mathrm{sommet}[E] \oplus \mathcal{G}^\infty)$ contient un sous-graphe biparti complet de taille $k/2$, et il en est donc de même pour $\mathrm{arc}[D](\mathrm{sommet}[E] \oplus \mathcal{G}^\infty)$. Cela contredit (C). $\square$

Le détail des lemmes de récurrence ainsi que les preuves principales sont en annexes (cf. page 197). Il s'agit des lemmes A.10, A.11, A.12, A.13 et A.14.

### 4.4.5.5 Le résultat

**Théorème 26** Pour tout ensemble de couleurs $C$, tout ensemble d'étiquettes $A$ et tout entier positif $k$, il existe un transducteur déterministe $t$ des $\mathrm{VR}[A, C]$-termes vers les HR-termes tel que pour tout $\mathrm{VR}[A, C]$-terme $t$, si $[[t]]$ ne contient pas de sous-graphe biparti complet de taille $k$, alors $t(t)$ est défini et

$$[[t(t)]] \approx [[t]].$$

**Preuve.** Il suffit d'utiliser les lemmes A.10, A.11, A.12, A.13 et A.14 comme autant de règles de validité d'un transducteur déterministe. Il ne manque que l'hypothèse 3 du lemme de validité 3.59. Pour cela, on utilise une relation supplémentaire $\mathcal{R}''[\mathcal{G}^\infty, E, D](\mathcal{G}, \mathcal{H})$ qui, sous les hypothèses (A-C), est définie par

$$\mathrm{arc}[D](\mathrm{sommet}[E] \oplus \mathcal{G}) \approx \mathrm{fusion}[E](\mathrm{sommet}[E] \oplus \mathcal{H}).$$

Bien entendu, on a $\mathcal{R}''[\mathcal{G}^\infty, E, D](\perp, \perp)$. De plus si $\mathcal{R}[\mathcal{G}^\infty, E, D](\mathcal{G}, \mathcal{H})$ est vrai, alors $\mathcal{R}''[\mathcal{G}^\infty, E, D](\mathcal{G}, \mathcal{H})$ l'est aussi. Réciproquement si $\mathcal{R}''[\mathcal{G}^\infty, E, D](\mathcal{G}, \mathcal{H})$ alors $\mathcal{R}[\mathcal{G}^\infty, E, D](\mathcal{G}, \mathrm{fusion}[E](\mathrm{sommet}[E] \oplus \mathcal{H}))$. Ces deux équivalences s'interprètent comme une transition supplémentaire permettant de remplir les conditions de satisfaction de l'hypothèse 3 du lemme de validité 3.59. $\square$

**Corollaire 4.42 (Barthelmann)** Les familles de graphes suivantes sont équivalentes :

- les graphes VR-équationnels de largeur arborescente bornée,

- les graphes VR-équationnels uniformément creux,

- les graphes VR-équationnels dont les sous-graphes bipartis complets sont bornés,

- les graphes HR-équationnels de largeur arborescente bornée.
# Chapitre 5

## Structures automatiques sur les termes

Dans le chapitre 4, les structures considérées étaient construites sur un univers de mots et par récriture suffixe (ou préfixe). Les structures étudiées ici sont définies sur des ensembles de termes et les relations sont décrites au moyen d'automates. Les propriétés de cette famille sont fondamentalement différentes de celles de la famille précédente.

Nous commençons par un rappel sur les langages de termes et présentons les opérateurs correspondants (paragraphe 5.1). Le paragraphe 5.2 s'intéresse à la famille des structures à présentation terme-automatique proprement dite.

### 5.1 Langages de termes

Si les langages sur les mots sont bien connus, c'est moins le cas des langages de termes qui en sont pourtant une extension naturelle. Nous présentons dans ce paragraphe quelques résultats classiques de cette théorie. Une étude détaillée de ce domaine se trouve en ligne [CDG+97].

Nous abordons les langages de termes sous deux angles, celui des automates (paragraphe 5.1.1), puis celui des systèmes d'équations (paragraphe 5.1.2).

#### 5.1.1 Automates d'arbres

Nous présentons tout d'abord les automates d'arbres et les langages de termes qu'ils reconnaissent (paragraphe 5.1.1.1), puis le cas particulier des automates déterministes descendants 5.1.1.2.
### 5.1.1.1 Le cas général

Un automate d'arbres sur l'alphabet gradué $\mathcal{F}$ est un triplet $(Q, \delta, F)$ où

- $Q$ est un ensemble fini d'états,

- $\delta$ est un ensemble de transitions de la forme $(f(q_1, \dots, q_{|f|}), q)$, avec $f \in \mathcal{F}$ et $q_1, \dots, q_{|f|}, q \in Q$,

- $F \subseteq Q$ est l'ensemble des états d'acceptation.

On suppose dorénavant que $Q$ et $\mathcal{F}$ sont disjoints, et on attribue à chaque élément de $Q$ l'arité 0 afin de pouvoir l'utiliser comme un symbole. On étend alors $\delta$ en une unique plus petite relation $\dot{\delta}$ de $\mathcal{T}(\mathcal{F} \uplus Q) \times Q$ satisfaisant :

- pour tout $q \in Q$, $(q, q) \in \dot{\delta}$,

- si il existe $(f(q_1, \dots, q_{|f|}), q) \in \delta$ telle que pour tout $i$, $(t_i, q_i) \in \dot{\delta}$ alors $(f(t_1, \dots, t_{|f|}), q) \in \dot{\delta}$.

Dans la pratique, on identifie $\delta$ et $\dot{\delta}$, et on note $\delta^{-1}(q)$ l'ensemble des termes $t$ tels que $(t, q) \in \delta$. On dit qu'un automate d'arbres $(Q, \delta, F)$ accepte un terme $t$ si $t \in \delta^{-1}(F)$. Un langage de termes $L$ est rationnel (ou reconnaissable) si il existe un automate d'arbres $(Q, \delta, F)$ tel que $L = \delta^{-1}(F) \cap \mathcal{T}(\mathcal{F})$.

**Exemple 5.1** Considérons l'alphabet gradué $\mathcal{F} = \{\text{vrai} : 0, \text{faux} : 0, \neg : 1, \wedge : 2, \vee : 2\}$. Chaque terme sur cet alphabet correspond à une formule booléenne. Il s'agit de déterminer si une formule s'évalue à vrai. Pour cela, on prend $Q = \{q_0, q_1\}$, $F = \{q_1\}$ et les transitions suivantes :

$$ \delta = \{ (\text{vrai}, q_1), (\text{faux}, q_0), (\neg(q_0), q_1), (\neg(q_1), q_0), (\vee(q_0, q_0), q_0), (\vee(q_1, q_0), q_1), (\vee(q_0, q_1), q_1), (\vee(q_1, q_1), q_1), (\wedge(q_0, q_0), q_0), (\wedge(q_1, q_0), q_0), (\wedge(q_0, q_1), q_0), (\wedge(q_1, q_1), q_1) \}. $$

On vérifie alors qu'un terme est accepté par un automate si et seulement si la formule booléenne correspondante s'évalue à vrai.

Un automate $(Q, \delta, F)$ est déterministe ascendant si pour tout symbole $f$ et pour tous états $q_1, \dots, q_{|f|}$, il existe au plus un état $q$ tel que $(f(q_1, \dots, q_{|f|}), q) \in \delta$. Il est complet si il existe toujours un tel état. Pour cette forme de déterminisme, le résultat classique de déterminisation des automates sur les mots s'étend sans difficulté aux termes comme le montre le résultat suivant.

**Propriété 5.2** Un langage est rationnel si et seulement si il est l'ensemble des termes acceptés par un automate d'arbres déterministe ascendant (cf. [CDG$^+$ 97]).
### 5.1.1.2 Automates descendants déterministes

Une autre forme de déterminisme est néanmoins possible pour les automates d'arbres. Il s'agit du déterminisme descendant. Un automate $(Q, \delta, F)$ est déterministe descendant si $F$ est un singleton et pour tout symbole $f$ et tout état $q$, il existe au plus une transition de la forme $(f(q_1, \dots, q_{|f|}), q)$. En ce sens, il n'est plus possible de déterminiser tous les langages rationnels comme l'illustre l'exemple 5.3.

**Exemple 5.3** Considérons sur l'alphabet $\{f : 2, a : 0, b : 0\}$ le langage $L = \{f(a, b), f(b, a)\}$. Supposons qu'un automate déterministe descendant $(Q, \delta, F)$ accepte ce langage. Supposons $F = \{q_0\}$ et $(f(q, q'), q_0)$ comme seule transition associée au symbole $f$ et à l'état $q_0$. Comme $f(a, b) \in L$, on $a(a, q) \in \delta$. Comme $f(b, a) \in L$, on $a(a, q') \in \delta$. Il s'ensuit que $f(a, a) \in L$. Contradiction.
En fait, on peut caractériser précisément l'ensemble des termes reconnus par un automate déterministe descendant par leurs branches.

**Propriété 5.4 (folklore)** Un langage de termes $L$ est accepté par un automate déterministe descendant si et seulement si il existe un langage rationnel de mots $B$ tel que :

$$L = \{t \mid \mathcal{LB}(t) \subseteq B\}.$$

## 5.1.2 Représentation équationnelle

Tout comme pour les mots, les automates d'arbres admettent une représentation équationnelle. Nous considérons deux telles représentations, l'une pour les automates quelconques et l'autre pour les automates déterministes descendant.

### 5.1.2.1 Langages rationnels

Les langages rationnels de termes sont les solutions des systèmes d'équations finis sur les opérateurs $Auto^T[\mathcal{F}]$ (ou plus simplement $Auto^T$) suivants:

- L'union de langage (notée $+$).

- L'application d'un symbole $f \in \mathcal{F}$, qui à $|f|$ langages $L_1, \dots, L_{|f|}$ associe le langage $f(L_1, \dots, L_{|f|})$.

**Propriété 5.5** Un langage de termes est rationnel si et seulement si il est solution d'un $Auto^T$-système fini d'équations.

### 5.1.2.2 Automates descendants déterministes

Les automates descendants déterministes admettent aussi une représentation équationnelle. Pour $\mathcal{F}$ un alphabet gradué, les opérateurs $Auto^T_{dd}[\mathcal{F}]$ (ou plus
simplement $\mathbf{Auto}_{dd}^{\mathcal{T}}$) sont d'une unique forme :

- pour $f_1, \dots, f_n \in \mathcal{F}$ des symboles distincts, on considère l'opérateur qui aux langages $L_1^1, \dots, L_{|f_1|}^1, \dots, L_1^n, \dots, L_{|f_n|}^n$ associe

$$ \sum_{i \in [n]} f_i(L_1^i, \dots, L_{|f_i|}^i). $$

Bien entendu, un langage est accepté par un automate déterministe descendant si et seulement si il est solution d'un $\mathbf{Auto}_{dd}^{\mathcal{T}}$-système fini d'équations. En fait, la propriété 5.4 se généralise à tout système d'équations.

**Propriété 5.6** Soit $\mathcal{F}$ un alphabet gradué.

Il existe un transducteur déterministe $t$ des $\mathbf{Auto}_{dd}^{\mathcal{T}}$-termes dans les $\mathbf{Auto}_d$-termes tel que pour tout $\mathbf{Auto}_{dd}^{\mathcal{T}}$-terme $t$,

$$ [t] = \{u \in \mathcal{T}(\mathcal{F}) \mid \mathcal{LB}(u) \subseteq [t(t)]\}. $$

Réciproquement, il existe un transducteur déterministe $t'$ des $\mathbf{Auto}_d$-termes dans les $\mathbf{Auto}_{dd}^{\mathcal{T}}$-termes tel que pour tout $\mathbf{Auto}_d$-terme $t$,

$$ [t(t)] = \{u \in \mathcal{T}(\mathcal{F}) \mid \mathcal{LB}(u) \subseteq [t]\}. $$

La preuve de cette propriété est sans difficulté particulière.

## 5.2 Structures terme-automatiques

Les structures terme-automatiques sont des structures qui, à isomorphisme près, ont un ensemble rationnel de termes comme univers, et dont les interprétations des symboles sont décrites «au moyen d'automates».

Là encore, nous donnons une triple représentation de ces structures.

**La représentation interne** s'obtient au moyen d'automates de termes. Elle est décrite au paragraphe 5.2.1.

**La représentation équationnelle** au moyen des opérateurs VRS' qui sont une extension des opérateurs VR' par la possibilité d'utiliser un produit synchrone et de restreindre l'univers. Il s'agit de l'objet du paragraphe 5.2.2.

**La représentation par transformations** utilise une transformation particulière, l'interprétation monadique des parties finies, appliquée à l'arbre binaire complet. Une interprétation des parties finies consiste, au moyen de formules monadiques, à définir une nouvelle structure dont l'univers est un ensemble de parties finies de la structure originale. Cette représentation est étudiée au paragraphe 5.2.3.

Nous montrons que ces trois représentations sont équivalentes.

Pour finir, nous énonçons au paragraphe 5.2.4 comment ces résultats peuvent être adaptés à la famille des structures automatiques, un cas particulier des structures terme-automatiques.
## 5.2.1 Présentation terme-automatique

Nous commençons par présenter la famille des relations «terme-synchronisées» sur les termes (paragraphe 5.2.1.1), puis comment l'appliquer pour décrire des structures : les structures à présentation terme-automatique (paragraphe 5.2.1.2).

### 5.2.1.1 Relations terme-synchronisées

Dorénavant $\Omega$ est un nouveau symbole d'arité 0. Soit $\mathcal{F}$ un alphabet gradué. Considérons les alphabets gradués $\mathcal{F}_{\Omega}^n$ et $\mathcal{F}_{\Omega}^*$ définis par

$$ 
\begin{array}{l}
\mathcal{F}_{\Omega}^{n} = \{[f_1, \dots, f_n] \mid f_1, \dots, f_n \in \mathcal{F} \uplus \{\Omega\}\}, \\
\text{avec } |[f_1, \dots, f_n]| = \max_{i \in [n]} |f_i|, \\
\text{et } \mathcal{F}_{\Omega}^{*} = \bigcup_{n \in \mathbb{N}} \mathcal{F}_{\Omega}^{n}.
\end{array}
$$

La projection sur la ième composante pour $i \in [n]$ de $[f_1, \dots, f_n] \in \mathcal{F}_{\Omega}^*$, notée $\pi_i([f_1, \dots, f_n])$ est $f_i$. On étend $\pi_i$ aux $\mathcal{F}_{\Omega}^n$-termes comme suit. Pour $i \in [n]$ et $t$ un $\mathcal{F}_{\Omega}^n$-terme, $\pi_i(t)$ est le $\mathcal{F} \cup \{\Omega\}$-terme défini par l'équation suivante.

$$ \pi_i([f_1, \dots, f_n](t_1, \dots, t_k)) = f_i(\pi_i(t_1), \dots, \pi_i(t_{|f_i|})) \quad \text{avec } k = \max_{j \in [n]} |f_j|. $$

Le $n$-uplet de termes $\pi(t)$ est alors égal à $(\pi_1(t), \dots, \pi_n(t))$.

Par exemple, considérons l'alphabet gradué $\mathcal{F} = \{f : 2, a : 0, b : 0\}$ et le $\mathcal{F}_{\Omega}^2$-terme $t = [f, f]([a, b], [f, a]([a, \Omega], [b, \Omega]))$, alors $\pi(t) = (f(a, f(a, b)), f(b, a))$.

Un $\mathcal{F}_{\Omega}^n$-terme $t$ est bien formé si pour tout sous-terme de $t$ de la forme $[f_1, \dots, f_n](t_1, \dots, t_k)$, on a :

$$ \text{pour tout } i \in [k], j \in [n], \quad \pi_i(t_j) = \Omega \quad \text{ssi } j > |f_i|. $$

Soit $N_{\Omega}^n$ le langage des $\mathcal{F}_{\Omega}^n$-termes bien formés tel que le symbole à la racine ne contient pas $\Omega$. Ce langage est rationnel (en fait, il est même reconnu par un automate d'arbres déterministe descendant).

**Lemme 5.7 (Dauchet et Tison [DT90])** *Pour tout $n$, l'application $\pi$ est une bijection de $N_{\Omega}^n$ sur $\mathcal{T}(\mathcal{F})^n$.*

Une relation $R \subseteq \mathcal{T}(\mathcal{F})^n$ est terme-synchronisée (RR dans les travaux de Dauchet et Tison) si elle est l'image par $\pi$ d'un langage rationnel $L \subseteq N_{\Omega}^n$. Les propriétés de clôture des langages rationnels s'étendent alors aux relations terme-synchronisées directement grâce au lemme 5.7.

**Lemme 5.8 ([DT90])** *Les relations terme-synchronisées sont closes par union, intersection et complémentation.*
Comme pour le lemme 5.8, les deux propriétés ci-dessous sont classiques et simples à établir.

**Lemme 5.9 ([DT90])** *Les relations terme-synchronisées sont closes par projection et cylindrification.*

### 5.2.1.2 Structures à présentation terme-automatique

Nous utilisons ici la terminologie introduite par Blumensath [Blu99]. Une présentation terme-automatique<fnref n="1" /> est un quadruplet $P = (\mathcal{F}, U, \Sigma, I)$ où $\mathcal{F}$ est un alphabet gradué, $U \subseteq \mathcal{T}(F)$ est un langage rationnel, $\Sigma$ est un alphabet relationnel fini et $I$ est une application qui à chaque $R \in \Sigma$ associe une partie rationnelle de $\mathcal{T}(\mathcal{F}_{\Omega}^{|R|})$. La $\Sigma$-structure $[P]$ associée à $P$ a pour univers $U$, pour signature $\Sigma$ et $\pi(I(R))$ comme interprétation d'un symbole $R \in \Sigma$. Une structure $\mathcal{S}$ admet une présentation terme-automatique si il existe une présentation terme-automatique $P$ telle que $\mathcal{S}$ est isomorphe à $[P]$.

Les lemmes 5.8 et 5.9 permettent alors de simplement établir le théorème fondamental 27.

**Théorème 27 (Dauchet et Tison [DT90])** *La théorie au premier ordre des structures admettant une présentation terme-automatique est décidable.*

La représentation donnée précédemment est pratique pour effectuer des codages. Il est néanmoins possible de la simplifier en utilisant un alphabet restreint à un symbole binaire et une constante. Il s'agit du lemme 5.10.

**Lemme 5.10** *Toute structure admettant une présentation terme-automatique, admet une présentation terme-automatique sur l'alphabet gradué $\{p : 2, c : 0\}$.*

**Preuve.** Considérons une présentation $(\mathcal{F}, U, \Sigma, I)$. Appelons $\mathcal{F}_0$ l'alphabet gradué $\{p : 2, c : 0\}$. Il s'agit de se donner un codage «convenable» sous forme d'un morphisme injectif de $\mathcal{T}(\mathcal{F})$ dans $\mathcal{T}(\mathcal{F}_0)$. Pour cela, soient $f_1, \dots, f_K$ les symboles de $\mathcal{F}$. On suppose que l'on dispose de $K + 1$ $\mathcal{F}_0$-termes finis distincts $\dot{f}_1, \dots, \dot{f}_K$ et $\dot{\Omega}$. Soit $N$ la plus grande des arité des symboles de $\mathcal{F}$. On définit alors le morphisme $\rho$ des $\mathcal{F}$-termes dans les $\mathcal{F}_0$ termes par l'équation suivante:

$$ \rho(f(t_1, \dots, t_{|f|})) = p^{N+1}(\dot{f}, \rho(t_1), \dots, \rho(t_{|f|}), \underbrace{\dot{\Omega}, \dots, \dot{\Omega}}_{N-|f| \text{ fois}}), \\ \text{avec pour tout } n \in \mathbb{N}, \quad p^n(t_1, \dots, t_n) = p(t_1, p(t_2, \dots, p(t_n, \dot{\Omega}) \dots)). $$

<footnote n="1">1. Pour être précis, il s'agit d'une présentation injective. Une présentation en générale dispose d'une relation terme-synchronisée supplémentaire permettant de «quotienter» la structure. Quand les classes d'équivalences de cette relation sont réduites à un unique élément, on parle de présentation injective. Blumensath montre que toute présentation peut être rendue injective.</footnote>
L'application $\rho$ ainsi définie est un morphisme, donc $U' = \rho(U)$ est une partie rationnelle de $\mathcal{T}(\mathcal{F}_0)$. Il est évident de plus que $\rho$ est injective. Il s'agit donc d'une bijection de $U$ sur $U'$.

Il reste à montrer que l'image d'une relation terme-synchronisée par $\rho$ est elle-même terme-synchronisée. Nous ne donnons pas ici le détail de cette preuve. Notons juste que la construction est telle que la position des arguments d'un symbole après codage par $\rho$ ne dépend que de leur numéro et non du symbole lui même. C'est cette propriété essentielle qui fait fonctionner la construction. $\square$

## 5.2.2 Représentation équationnelle

Nous donnons ici une définition des structures à présentation terme-automatique au moyen de systèmes finis d'équations. Les opérateurs correspondants sont présentés au paragraphe 5.2.2.1. Suit un résultat de normalisation (5.2.2.2). L'équivalence avec la présentation terme-automatique est établie au paragraphe 5.2.2.3.

### 5.2.2.1 Définition

Les opérateurs $\mathbf{VRS}'$ sont une extension des opérateurs $\mathbf{VR}'$ par (principalement) l'ajout d'un opérateur de produit synchrone. Ainsi, $\mathbf{VRS}'$ signifie $\mathbf{VR}'+\text{produit Synchrone}$. Pour $\Sigma$ un alphabet relationnel, les opérateurs $\mathbf{VRS}'[\Sigma]$ (ou plus simplement $\mathbf{VRS}'$) sont les suivants:

- La structure à un élément $\mathbf{un}[R]$ où $R \in \Sigma$ est un symbole d'arité 1. On se contente aussi parfois de $\mathbf{un}$ dont l'interprétation de tous les symboles est vide.

- L'union disjointe.

- L'interprétation booléenne positive.

- Le produit synchrone.

- La restriction à l'interprétation d'un symbole relationnel unaire $R$, notée $\text{restrict}[R]$, a pour sémantique

$$ \text{restrict}[R](S) = S|_{R^s} . $$

Ainsi, les opérateurs $\mathbf{VRS}'$ ne sont qu'une extension des opérateurs $\mathbf{VR}'$ par la possibilité d'utiliser un produit synchrone et la restriction. Cette dernière opération, si elle n'augmente pas l'expressivité des opérateurs $\mathbf{VR}'$, est cruciale dans le cas présent. Concernant l'opérateur de produit et d'après la propriété 2.22, il est possible d'utiliser indifféremment le produit synchrone ou le produit généralisé.

Le paragraphe 5.2.2.2 montre comment normaliser ces systèmes d'équations.
### 5.2.2.2 Normalisation

Le lemme 4.17 (page 108) énonce que les opérateurs $VR'$ admettent une version normalisée dans laquelle les interprétations booléennes positives sont en forme linéaire complète. Nous montrons dans ce paragraphe que ce résultat reste valable dans le cas des opérateurs $VRS'$. En fait, nous montrons ici un résultat plus fort qui, de plus, précise qu'une seule restriction est suffisante (lemme 5.13). La première étape consiste à éliminer les opérations de restriction (lemme 5.11). Le reste de la preuve n'est alors plus qu'une simple extension du lemme 4.17.

#### Retard de la restriction

Il s'agit ici d'éliminer les opérateurs de restriction d'un $VRS'$-système d'équations. Il n'est pas possible de les éliminer totalement. En revanche, il est possible de les retarder afin qu'un seul de ces opérateurs soit nécessaire.

La construction se fait au moyen d'un transducteur déterministe. La solution naturelle consistant à utiliser un nouveau symbole relationnel • d'arité 1 «marquant» les éléments de l'univers qui n'ont pas encore été éliminés par une restriction fonctionne parfaitement.

Ainsi, étant donnée une $\Sigma$-structure $\mathcal{S}$ (obtenue en utilisant éventuellement des opérateurs de restriction), on cherche à produire une $\Sigma \uplus \{\bullet\}$-structure $\mathcal{S}'$ telle que :

$$ \mathcal{I}_{\bullet}(\mathcal{S}) = \text{restrict}[\bullet](\mathcal{S}'), \\ \text{avec } \mathcal{I}_{\bullet} = \left| \begin{array}{ll} R(x_1, \dots, x_{|R|}) & : R(x_1, \dots, x_{|R|}), \ R \in \Sigma \\ \bullet(x) & : \text{vrai} \end{array} \right| $$

Supposons $\mathcal{I}_{\bullet}(\mathcal{S}_1) = \text{restrict}[\bullet](\mathcal{S}'_1)$ et $\mathcal{I}_{\bullet}(\mathcal{S}_2) = \text{restrict}[\bullet](\mathcal{S}'_2)$. Alors

$$ \begin{align*} \mathcal{I}_{\bullet}(\mathcal{S}_1 \oplus \mathcal{S}_2) &= \mathcal{I}_{\bullet}(\mathcal{S}_1) \oplus \mathcal{I}_{\bullet}(\mathcal{S}_2) \\ &= \text{restrict}[\bullet](\mathcal{S}'_1) \oplus \text{restrict}[\bullet](\mathcal{S}'_2) \\ &= \text{restrict}[\bullet](\mathcal{S}'_1 \oplus \mathcal{S}'_2) \end{align*} $$

et de même, $\mathcal{I}_{\bullet}(\mathcal{S}_1 \otimes \mathcal{S}_2) = \text{restrict}[\bullet](\mathcal{S}'_1 \otimes \mathcal{S}'_2)$.

Supposons maintenant $\mathcal{I}_{\bullet}(\mathcal{S}) = \text{restrict}[\bullet](\mathcal{S}')$, alors,

$$ \begin{align*} \mathcal{I}_{\bullet}(\text{restrict}[R](\mathcal{S})) &= \text{restrict}[R](\mathcal{I}_{\bullet}(\mathcal{S})) \\ &= \text{restrict}[R](\text{restrict}[\bullet](\mathcal{S}')) \\ &= \text{restrict}[\bullet](\mathcal{I}_{\text{restrict}[R]}(\mathcal{S})) \\ \text{avec } \mathcal{I}_{\text{restrict}[R]} &= \left| \begin{array}{ll} R'(x_1, \dots, x_{|R'|}) & : R'(x_1, \dots, x_{|R'|}), \ R' \in \Sigma \\ \bullet(x) & : \bullet(x) \wedge R(x) \end{array} \right| \end{align*} $$
**Preuve.** Comme pour le lemme 4.17, on utilise le lemme 5.12 pour traiter l'opérateur $\otimes$. $\square$

En combinant les lemmes 5.11 et 5.13 on obtient le résultat de normalisation complet énoncé ci-dessous.

**Propriété 5.14** *Pour tout alphabet relationnel fini $\Sigma$, il existe un transducteur déterministe $t'$ des VRS$^{'}[\Sigma]$-termes vers les VRS$^{'}$-termes sans restriction et à interpétation linéaire complète, et une interprétation linéaire complète $\mathcal{I}_e$ tels que pour tout VRS$^{'}[\Sigma]$-terme $t$,*

$$ \mathcal{I}'_e(\text{restrict}[\bullet][\mathbf{t}'(t)]) = [t]. $$

### 5.2.2.3 Équivalence avec la représentation automatique

Il s'agit d'établir le résultat suivant.

**Théorème 28** *Une structure admet une présentation terme-automatique si et seulement si elle est isomorphe à la solution d'un VRS'-système fini d'équations.*

Ce résultat s'obtient en combinant les lemmes 5.16 et 5.17. Ces deux lemmes sont successivement présentés.

#### De la présentation terme-automatique au système d'équations

On suppose pour commencer que l'alphabet est égal à $\{p : 2, c : 0\}$; cela est possible d'après le lemme 5.10.

Informellement, une structure d'univers $\mathcal{T}(\{p : 2, c : 0\})$ a un univers isomorphe à la solution de l'équation $X = (X \otimes X) \oplus \text{un}$. En effet, le produit code la présence des deux arguments de l'opérateur $p$, et l'union permet d'ajouter un nouvel élément représentant le terme $c$. La structure du système d'équations que nous produisons est la même; il ne manque que les interprétations permettant de «calculer» les relations de la structure proprement dite.

On considère donc une structure terme-automatique représentée par $(\mathcal{F}, U, \Sigma, I)$, avec $\mathcal{F} = \{p : 2, c : 0\}$. La première étape de la démonstration (lemme 5.15) consiste à montrer le résultat sans restriction à un univers rationnel, c'est à dire pour $U = \mathcal{T}(\mathcal{F})$. L'entier $N$ représente dorénavant la plus grande des arités des symboles dans $\Sigma$. L'ensemble de variables $\{x_1, \dots, x_N\}$ est noté $\mathcal{X}$. pour $E \subseteq [n]$, $\mathcal{X}_E$ représente l'ensemble de variables $\{x_i \mid i \in E\}$, et $\overline{\mathcal{X}}_E$ représente le vecteur de variables $(x_{\sigma(1)}, \dots, x_{\sigma(|E|)})$ où $\sigma$ est l'unique bijection croissante de $|E|$ sur $E$.

*Remarque de notation:* les symboles de $\mathcal{F}_{\Omega}^*$ peuvent être d'arité 2 ou 0 suivant qu'ils contiennent le symbole $p$ ou non. Ainsi, les transitions de $\delta$ sont de la forme $([f_1, \dots, f_n](q_1, \dots, q_n), q)$, où $n = \|[f_1, \dots, f_n]|$, et $n = 0$ ou $n = 2$. Dans ce qui suit, toutes les notations sont énoncées pour $n = 2$. La version $n = 0$ se déduit directement et ne provoque pas de conflit.
Chaque langage $I(R)$ est accepté par un automate de termes $\mathcal{A}_R$. On considère l'automate $\mathcal{A}$ formé de l'union (disjointe) de tous les automates $\mathcal{A}_R$ pour $R \in \Sigma$. L'ensemble des états de cet automate est $Q$ et l'ensemble des transitions est $\delta$. Pour tout $R \in \Sigma$, $q_R \in Q$ est l'état initial de l'automate $\mathcal{A}_R$ dans $\mathcal{A}$. Pour tout $q \in Q$, $L_q$ représente le langage de $\mathcal{F}_{\Omega}^{|q|}$ accepté par $\mathcal{A}$ avec pour état initial $q$. De plus, $F(q)$ représente l'ensemble $\{i \in [|q|] \mid \exists t \in L_q, \pi_i(t) \neq \Omega\}$. Soit $\gamma = ([f_1, \dots, f_n](q_1, q_2), q)$ une transition, $F_\rho(\gamma)$ représente l'ensemble $\{i \in [n] \mid f_i = p\}$ et de même, $F_c(\gamma) = \{i \in [n] \mid f_i = c\}$

Si $L$ est un langage de $\mathcal{F}_{\Omega}^n$ et $E \subseteq [n]$, $L|_E$ représente le langage $L$ «projeté» sur les composantes d'indice $i \in E$. Formellement et récursivement,

pour $t = ([f_1, \dots, f_n](t_1, \dots, t_k)) \in \mathcal{T}(\mathcal{F}_{\Omega}^n)$, $t|_E = [f_{\sigma(1)}, \dots, f_{\sigma(n)}](t_1|_E, \dots, t_k|_E)$,

où $\sigma$ est la bijection croissante de $[|E|]$ sur $E$,

et pour $L \subseteq \mathcal{T}(\mathcal{F}_{\Omega}^n)$, $L|_E = \{t|_E \mid t \in L\}$.

Bien entendu, si un terme $t \in \mathcal{F}_{\Omega}^n$ est bien formé, alors il en va de même de $t|_E$ pour tout $E \subseteq [n]$.

L'alphabet relationnel qui nous permet de construire la structure est le suivant :

$$
\begin{align*}
\Sigma' &= \{ \langle q, E \rangle \mid q \in Q, E \subseteq F(q), E \neq \emptyset \} \\
&\quad \cup \{ \langle \gamma, E \rangle_c \mid \gamma \in \delta, E \subseteq F_c(\gamma), E \neq \emptyset \} \\
&\quad \cup \{ \langle \gamma, E \rangle_p \mid \gamma \in \delta, E \subseteq F_p(\gamma), E \neq \emptyset \},
\end{align*}
\text{avec pour tous } q \in Q, E \subseteq F(q), E \neq \emptyset, \quad |\langle q, E \rangle| = |E|, \\
\text{pour tous } \gamma \in \delta, E \subseteq F_c(\gamma), E \neq \emptyset, \quad |\langle \gamma, E \rangle_c| = |E|, \\
\text{et pour tous } \gamma \in \delta, E \subseteq F_p(\gamma), E \neq \emptyset, \quad |\langle \gamma, E \rangle_p| = |E|.
$$

On s'intéresse alors à la structure $\mathcal{S}$ dont l'univers est $\mathcal{T}(\mathcal{F})$ et pour tout $q \in Q$, et tout $E \subseteq F(q)$ tel que $E \neq \emptyset$, on a $\langle q, E \rangle^{\mathcal{S}} = \pi(L_q|_E)$.

On pose alors :

$$
\mathcal{I} = \left| \begin{array}{l} \langle q, E \rangle (\overline{\mathcal{X}_E}) : \left\{ \begin{array}{ll} \langle \gamma, E_c \rangle_c (\overline{\mathcal{X}_{E_c}}) & \text{si } E_p = \emptyset \\ \langle \gamma, E_p \rangle_p (\overline{\mathcal{X}_{E_p}}) & \text{si } E_c = \emptyset \\ \langle \gamma, E_p \rangle_p (\overline{\mathcal{X}_{E_p}}) & \text{et } \langle \gamma, E_c \rangle_c (\overline{\mathcal{X}_{E_c}}) \text{ sinon} \end{array} \right. \\ \\ \text{pour } \gamma \in \delta, \quad \begin{array}{l} E_c = E \cap F_c(\gamma), \\ E_p = E \cap F_p(\gamma) \end{array} \end{array} \right|
$$
et pour tout $i \in [2]$,

$$ \mathcal{I}_i = \left| \begin{array}{l} < \gamma, E >_p (\overline{\mathcal{X}_E}) : < q_i, E > (\overline{\mathcal{X}_E}) \\ \text{avec } \gamma = ([f_1, \dots, f_{|q|}](q_1, q_2), q) \in \delta \end{array} \right| $$

La structure $\mathcal{S}$ satisfait l'équation suivante (sur les opérateurs VRS').

$$ \mathcal{S} \approx \mathcal{I}((\mathcal{I}_1(\mathcal{S}) \otimes \mathcal{I}_2(\mathcal{S})) \oplus \mathcal{I}_c(\text{un})), \\ \text{avec } \mathcal{I}_c = \left| \mathcal{I}_c = \left. \left< \gamma, E > (\overline{\mathcal{X}_E}) \quad : \text{vrai} \quad \gamma \in \delta, E \neq \emptyset, E \subseteq F_c(\gamma) \right| \right. . $$

Il s'agit en fait, à isomorphisme près, de la plus petite solution de cette équation. La démonstration ne pose pas de problème car les relations $I(R)$ sont elles-mêmes définies par un plus petit point fixe. Notons tout de même que les symboles relationnels d'arité 0 ont été évités dans cette construction. Il aurait fallu sinon les traiter séparément.

**Lemme 5.15** *Pour toute structure $\mathcal{S}$ admettant une présentation terme-automatique ($\{c: 0, p: 2\}$, $\mathcal{T}(\{c: 0, p: 2\})$, $\Sigma$, $I$), il existe un VRS'-système fini d'équations $\mathcal{S}$ tel que*

$$ \mathcal{S} \approx \text{Solution}(\mathcal{S}). $$

**Preuve.** Une fois la structure $\mathcal{S}$ obtenue par un VRS'-système d'équations, il est aisé de réobtenir les relations $I(R)$. Il suffit d'appliquer à $\mathcal{S}$ l'interprétation suivante :

$$ \left| R(x_1, \dots, x_{|R|}) \quad : \quad \langle q_R, \{x_1, \dots, x_{|R|}\} \rangle > (x_1, \dots, x_{|R|}) \quad \text{pour } R \in \Sigma \right| . $$

□

**Lemme 5.16** *Pour toute structure $\mathcal{S}$ admettant une présentation terme-automatique, il existe un VRS'-système fini d'équations $\mathcal{S}$ tel que :*

$$ \mathcal{S} \approx \text{Solution}(\mathcal{S}). $$

**Preuve.** On se ramène au cas de l'alphabet $\mathcal{F}_0 = \{p: 2, c: 0\}$ par le lemme 5.10. Soit $P = (\mathcal{F}_0, U, \Sigma, I)$ la présentation correspondante. L'univers $U$ étant rationnel, il s'agit d'un cas particulier de relation synchronisée d'arité 1. On ajoute à la signature un nouveau symbole $\bullet$ d'arité 1 dont l'interprétation est $U$. Soit $\mathcal{F}_\bullet = \mathcal{F}_0 \cup \{\bullet\}$. Après application du lemme 5.15, on obtient un VRS'-système fini d'équations $\mathcal{S}$ dont la solution est isomorphe à $[(\mathcal{F}_\bullet, \mathcal{T}(\mathcal{F}_\bullet), \Sigma, I')]$ où $I'$ coïncide avec $I$ sur $\Sigma$ et $I(\bullet) = U$. On a alors :

$$ \begin{gathered} [P] \approx \mathcal{I}_e(\text{restrict}[\bullet]), \\ \text{avec } \mathcal{I}_e = \left| R(x_1, \dots, x_{|R|}) \quad : \quad R(x_1, \dots, x_{|R|}) \quad R \neq \bullet \right| . \end{gathered} $$
☐

On peut remarquer que la structure définie ainsi est déja normalisée au sens du lemme 5.13.

## Du système d'équations à la présentation terme-automatique

**Lemme 5.17** *Pour tout VRS'-système fini d'équations S, Solution(S) admet une présentation terme-automatique.*

Nous ne donnons pas la preuve ici de ce résultat; elle est très similaire à la preuve du lemme 5.28 (remplacer pour cela le $\mu$-calcul par un Auto$^T$-système d'équations).

### 5.2.3 Représentation logique

Il s'agit dans ce paragraphe de montrer l'équivalence entre les solutions de VRS'-systèmes d'équations et les structures obtenues par une certaine transformation appliquée au dépliage d'un graphe (théorème 29). La transformation en question est une «interprétation des parties finies» présentée au paragraphe 5.2.3.1. Le résultat d'équivalence est énoncé par le théorème 29. Les paragraphes 5.2.3.2 et 5.2.3.3 établissent chacun l'une des directions de l'équivalence.

#### 5.2.3.1 Interprétation des parties

Une façon de construire une structure possédant une théorie au premier ordre décidable consiste à partir d'une structure $S_0$ ayant une théorie au second ordre monadique décidable, puis de définir l'univers comme un ensemble MSO-définissable de parties de l'univers de $S_0$ et d'utiliser des formules monadiques pour décrire l'interprétation des relations.

Formellement, une interprétation monadique des parties est un quadruplet $\mathcal{I} = (\Sigma, \Sigma', \delta, (\phi_R))$ où $\Sigma$ et $\Sigma'$ sont des alphabets relationnels, $\delta(X)$ est une formule monadique sur $\Sigma$ possédant une variable libre monadique $X$, et pour tout $R \in \Sigma'$, $\phi_R(X_1, \dots, X_{|R|})$ est une formule monadique sur $\Sigma$ possédant $|R|$ variables libres monadiques $X_1, \dots, X_{|R|}$.

L'application de $\mathcal{I} = (\Sigma, \Sigma', \delta, (\phi_R))$ à une $\Sigma$-structure $S$ est la $\Sigma'$-structure $\mathcal{I}(S)$ définie comme suit.

$$ \begin{gathered} \mathcal{U}_{\mathcal{I}(S)} = \{U \subseteq \mathcal{U}_S \mid S \models \delta(U)\}, \\ \text{et pour } R \in \Sigma', \quad R^{\mathcal{I}(S)} = \{(U_1, \dots, U_{|R|}) \subseteq (\mathcal{U}_{\mathcal{I}(S)})^{|R|} \mid S \models \phi_R(U_1, \dots, U_{|R|})\}. \end{gathered} $$
Cette construction peut produire des structures ayant un univers non dénombrable. Ainsi, appliquée à l'arbre binaire complet, on obtient les structures $\omega$-terme-automatiques selon la terminologie de Blumensath [Blu99].

On restreint donc cette définition aux structures dont l'univers est formé d'ensembles finis. Ainsi une interprétation monadique des parties finies est une interprétation monadique des parties $\mathcal{I} = (\Sigma, \Sigma', \delta, (\phi_R))$ telle que pour toute $\Sigma$-structure $S$ et tout $U \subseteq U_S$, si $S \models \delta(U)$ alors $U$ est fini.

L'intérêt de l'introduction de ces définitions est énoncé par le lemme suivant et son corollaire.

**Lemme 5.18** *Pour $\mathcal{I}$ une interprétation monadique des parties et $\phi$ une formule du premier ordre, il existe une formule monadique $\Phi$ telle que pour toute structure $S$, $\mathcal{I}(S) \models \phi$ si et seulement si $S \models \Phi$.*

**Preuve.** Il suffit de transformer les variables de $\phi$ en variables du second ordre monadique et de substituer aux relations leur définition dans $\mathcal{I}$. $\square$

**Corollaire 5.19** *Si $S$ est une structure ayant une théorie monadique décidable et $\mathcal{I}$ est une interprétation des parties, alors $\mathcal{I}(S)$ a une théorie au premier ordre décidable.*

Il est maintenant possible d'énoncer le résultat qui nous intéresse.

**Théorème 29** *Les familles de graphes suivantes sont isomorphes :*

- les solutions des VRS'-systèmes d'équations,

- les images par interprétation monadique des parties finies du dépliage d'un graphe,

et ces conversions sont effectives.

Les détails concernant l'effectivité des conversions se trouvent dans les deux lemmes 5.28 et 5.30 dont le théorème 29 est la combinaison.

Avant de s'intéresser à ces démonstrations, précisons quelques unes des conséquences.

**Corollaire 5.20** *Pour $\phi$ une formule du premier ordre et $\Sigma$ une signature, l'ensemble des modèles de $\phi$ est VRS'[$\Sigma$]-reconnaissable.*

**Corollaire 5.21** *Les solutions des VRS'-systèmes d'équations de théorie monadique décidable ont une théorie au premier ordre décidable.*

**Remarque 5.22** (extension) Blumensath [Blu99] considère une logique plus expressive que la simple logique du premier ordre. Il s'agit d'étendre cette logique par des quantifications de la forme $\exists^\omega x.\phi$ signifiant «il existe une infinité de valuations possibles pour $x$ telles que $\phi$$^»$. L'opération duale $\forall x.\phi = \neg\exists^\omega x.\neg\phi$ signifiant «$\phi$ est satisfaite pour toute valuation de $x$ sauf pour un nombre fini» est aussi
autorisée. Blumensath montre que cette logique est décidable sur les structures à présentation terme-automatique. C'est en fait toujours le cas pour les solutions des VRS'-systèmes d'équations de théorie monadique décidable.

Il suffit pour cela de montrer qu'un quantificateur $∃^{\omega,F} X.\phi$ signifiant «il existe une infinité de valuations de $X$ finies vérifiant $\phi$» peut être ajouté à la logique monadique pourvu que l'on dispose d'un prédicat $F(Y)$ exprimant la finitude de la valuation d'une variable monadique $Y$.

En effet, pour toute formule monadique $\phi$, toute variable monadique $X$, toute structure $S$ et toute valuation $\gamma$ de $FV(\phi) - \{X\}$, on a

$$ \gamma, S \models \exists^{\omega,F} X.\phi \quad \text{ssi} \quad \gamma, S \models \forall Y.F(Y) \Rightarrow \exists X.(X \not\subseteq Y) \wedge \phi. $$

Il se trouve que, dans le cas présent, la structure $S$ est un arbre (le dépliage du système d'équations). Il est donc possible d'exprimer le prédicat $F(Y)$ par une formule monadique (voir remarque 2.12 page 21).

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

Il s'agit dans ce paragraphe d'établir le lemme 5.28 permettant de passer de la sémantique des opérateurs VRS' à une interprétation monadique des parties finies.

On considère une signature $\Sigma$ et un VRS'[$\Sigma$]-terme $t$. Supposons pour commencer que les interprétations du terme soient sous forme linéaire complète sans relation d'arité 0. Supposons de plus que $t$ ne comporte pas d'opérateurs de restriction. Dans la suite de ce paragraphe, on note $\mathcal{F}$ cet ensemble d'opérateurs.

Il s'agit de coder pour tout $\mathcal{F}$-terme chaque élément de $[[t]]$ par une partie finie des sommets principaux de $t$. Pour cela, on définit pour tout terme $t$ la fonction partielle $\rho_t$ des parties finies des sommets principaux de $t$ dans l'univers de $[[t]]$. La fonction $\rho_t$ est décrite par récurrence (cette récurrence a bien un sens car $\rho_t(U)$ n'est défini que pour $U$ fini) comme suit:

si $t = \text{un}[R]$ alors $\rho(\{\text{racine}^t\}) = 0$,

si $t = \mathcal{I}(t')$ alors $\rho_t = \rho_{t'}$,

si $t = t_1 \oplus t_2$ alors $\rho_t(X)$ est défini si il existe $i \in [2]$ tel que $X \in \text{dom}(\rho_{t_i})$ et dans ce cas $\rho_t(X) = (i, \rho_{t_i}(X))$,

si $t = t_1 \otimes t_2$ alors $\rho_t(X)$ est défini si $X = X_1 \cup X_2$ avec pour tout $i \in [2]$, $X_i \in \text{dom}(\rho_{t_i})$, et dans ce cas, $\rho_t(X) = (\rho_{t_1}(X_1), \rho_{t_2}(X_2))$.

Pour comprendre cette définition, il convient de revenir à la définition interne de chaque opérateur. Ainsi, le sommet $\rho(\{\text{racine}^t\}) = 0$ du graphe $\text{un}[R]$ est-il son seul sommet. Les cas de l'union disjointe et du produit s'interprètent similairement.

**Exemple 5.23** Considérons le terme suivant (le paramètre des opérateurs un est
omis).

$$t = (\underbrace{\mathbf{un}}_{v_0} \oplus \underbrace{\mathbf{un}}_{v_1}) \otimes (\underbrace{\mathbf{un}}_{v_2} \oplus \underbrace{\mathbf{un}}_{v_3}).$$

Les sommets correspondants aux opérateurs un sont identifiés par $v_0, v_1, v_2$ et $v_3$.

La valeur de ce terme produit une structure dont l'univers contient quatre éléments $((1,0), (1,0)), ((2,0), (1,0)), ((1,0), (2,0))$ et $((2,0), (2,0))$. L'application $\rho_t$ est alors définie comme suit:

$$\begin{align*}
\rho_t(\{v_0, v_2\}) &= ((1,0), (1,0)) \\
\rho_t(\{v_1, v_2\}) &= ((2,0), (1,0)) \\
\rho_t(\{v_0, v_3\}) &= ((1,0), (2,0)) \\
\rho_t(\{v_1, v_3\}) &= ((2,0), (2,0))
\end{align*}$$

et $\rho_t$ n'est pas défini partout ailleurs.

Ainsi, $\rho_t$ est une bijection de son domaine sur l'univers de $[[t]]$. Le lemme suivant généralise cette remarque.

**Lemme 5.24** Pour tout terme $t$, $\rho_t$ est une bijection de $dom(\rho_t)$ sur $U_{[t]}$.

**Preuve.** Par récurrence sur la définition de $\rho$. $\square$

**Lemme 5.25** L'ensemble $\{(t, U) \mid U \in dom(\rho_t)\}$ est $\mathcal{F}_{[1]}$-reconnaissable.

**Construction.** Considérons un ensemble $U$ de sommets principaux de $t$. Alors $U$ appartient au domaine de $\rho_t$ si et seulement si $(t, U) \in \text{sommet}]$ avec sommet une formule du $\mu$-calcul définie comme suit:

$$\begin{align*}
\mathbf{vide} &= \nu y.(\neg 1) \wedge (\mathcal{I}(y) \cup (y \oplus y) \cup (y \otimes y) \cup \mathbf{un}) \\
\mathbf{sommet} &= \mu x.(1 \cap \mathbf{un}) \cup ((\neg 1) \cap (\mathcal{I}(x) \cup (x \oplus \mathbf{vide}) \cup (\mathbf{vide} \oplus x) \cup (x \otimes x)))
\end{align*}$$

La formule **vide** vérifie qu'aucune marque n'est présente dans un terme. La formule sommet décompose un terme en suivant les règles définissant $\rho$. Le plus petit point fixe provient du fait que seuls les ensembles finis sont considérés. $\square$

Soit $N$ la plus grande arité des symboles de $\Sigma$. Pour $R \in \Sigma$ et $\pi$ une injection de $[[R]]$ dans $[N]$, on définit l'ensemble de $\mathcal{F}_{[N]}$-termes $L_{R,\pi}$ comme suit:

$$L_{R,\pi} = \{(t, U_1, \dots, U_N) \mid R^{[[t]]}(\rho_t(U_{\pi(1)}), \dots, \rho_t(U_{\pi(|R|)}))\}.$$

La preuve du lemme 5.28 revient alors principalement à montrer que $L_{R,\pi}$ pour tout $R$ et toute injection $\pi$ est $\mathcal{F}_{[N]}$-reconnaissable. Pour cela, on construit un
système d'équations (au sens de l'extension vectorielle du μ-calcul) possédant les variables suivantes:

$$V = \{ \langle R, \pi \rangle \mid \pi \text{ injection de } [|R|] \text{ dans } [N] \}.$$

Soient $R \in \Sigma$ et $\pi$ une injection de $|R|$ dans $[N]$. La $\mu$-formule $\phi_{R,\pi}$ est définie comme suit:

$$ \begin{align*} \phi_{R,\pi} &= (\mathbf{un}[R] \cap \bigcap_{i \in \mathrm{dom}(\pi)} i \cap \bigcap_{i \in [N] - \mathrm{dom}(\pi)} \neg i) \\ &\quad \cup \bigcap_{i \in [N]} \neg i \\ &\quad \cap (<R, \pi> \oplus \mathbf{1}) \cup (\mathbf{1} \oplus <R, \pi>) \\ &\quad \cup (<R, \pi> \otimes <R, \pi>) \\ &\quad \cup \bigcup_{\mathcal{I}} \mathcal{I} \left( \bigcap_{i \in [k]} <R_i, \pi \circ \alpha_i> \right) \\ &\qquad \text{où } R(x_1, \dots, x_{|R|}) : \bigcap_{i \in [k]} R_i(x_{\alpha_i(1)}, \dots, x_{\alpha_i(|R_i|)}) \\ &\qquad \text{est une règle de } \mathcal{I} \text{ (une conjonction linéaire complète).} \end{align*} $$

**Lemme 5.26** Pour tout symbole $R \in \Sigma$ et toute injection $\pi$ de $|R|$ dans $[N]$, on a

$$L_{R,\pi} = \phi_{R,\pi}[\gamma] \quad \text{avec } \gamma(<S, \alpha>) = L_{S,\alpha} \text{ pour tout } <S, \alpha>> \in V.$$

**Preuve.** En traitant séparément le cas de chaque opérateur. $\square$

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

**Lemme 5.27** Pour tout symbole $R \in \Sigma$ et toute injection $\pi$ de $|R|$ dans $[N]$, on a

$$(\mu <R, \pi> . \{<S, \alpha> = \phi_{S,\alpha}\})] = L_{R,\pi}.$$

On en déduit le lemme suivant.

**Lemme 5.28** Pour toute signature finie $\Sigma$, il existe une interprétation monadique des parties finies $\mathcal{I}$ telle que pour tout $\mathrm{VRS}'[\Sigma]$-terme $t$,

$$\mathcal{I}(t) \approx [t].$$

**Preuve.** On suppose que le terme est normalisé en appliquant la propriété 5.14. À chaque formule $\psi_R$ du $\mu$-calcul est associé une formule monadique $\Psi_R(X_1, \dots, X_N)$ par le lemme 3.38. On construit alors l'interprétation des parties

$$\mathcal{I} = (\Sigma[\mathrm{VRS}'], \Sigma, \delta, (\Psi'_{R,\pi}))$$
avec

$$
\begin{align*}
\delta(X) &= \exists X_2, \dots, X_N \cdot \Psi_\bullet(X, X_2, \dots, X_N), \\
\Psi'_R(X_1, \dots, X_{|R|}) &= \exists X_{|R|+1}, \dots, X_N \cdot \Psi_{R, \mathrm{id}_{[R]}}(X_1, \dots, X_N).
\end{align*}
$$

□

**Remarque 5.29 (Cas particulier en l'absence de produit)** *Supposons que le terme t soit un VR'-terme. Dans ce cas, la fonction ρ n'est définie que sur des ensembles singletons. Un tel ensemble se représente naturellement par une variable du premier ordre. On en déduit que pout toute signature Σ, il existe une interpretation monadique I telle que pour tout VR'[Σ]-terme t, on a I(t) ≈ ⌊t⌋. Cette remarque établit le théorème 23 de Barthelmann.*

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

Le propos de ce paragraphe est d'établir le lemme ci-dessous.

**Lemme 5.30** *Pour toute signature Σ, tout ensemble fini d'étiquettes A et toute interprétation des parties finies I<sub>F</sub> des arbres déterministes étiquetés par A vers les Σ-structures, il existe une transduction monadique T des graphes déterministes étiquetés par A vers les VRS'-systèmes d'équations telle que pour tout graphe déterministe G étiqueté par A on a*

$$
\mathcal{I}_F(\mathrm{Depliage}(\mathcal{G})) \approx \mathrm{Solution}(T(\mathcal{G})) .
$$

Soit $\mathcal{I}_F = (\mathbf{A}, \Sigma, \delta, (\phi'_R)_{R \in \Sigma})$. Soit $\mathcal{F} = \{p : 2, c : 0\}$. Le lemme 3.39 permet de se ramener à la situation dans laquelle $\mathcal{G}$ est un $\mathcal{F}$-système d'équations. Il n'est plus dans la suite question que du dépliage de ce système d'équations : c.a.d. d'un $\mathcal{F}$-terme.

Pour commencer, on suppose que $\delta = \text{vrai}$ et on ajoute un symbole relationnel $\delta$ d'arité 1 tel que $\phi_{\delta} = \delta$. Ainsi, les sommets à conserver sont traités comme l'interprétation d'un symbole relationnel.

On considère les formules du μ-calcul $\phi_R$ obtenues à partir des formules monadiques $\phi'_R$ au moyen du lemme 3.38. Le lemme 3.39 nous précise que l'interprétation des parties finies $\mathcal{I}_F$ ne fait référence qu'aux sommets $P_t^c$. Grâce à cela, il est possible de supposer que les formules $\phi_R$ n'utilisent que l'alphabet $\mathcal{F}'_{[R]}$ défini comme suit:

$$
\text{pour } n \in \mathbb{N}, \quad \mathcal{F}'_n = \{(p, \emptyset) : 2\} \cup \{(c, E) : 0 \mid E \subseteq [n]\}.
$$

Soit $N$ la plus grande aritéd'un symbole apparaissant dans $\Sigma$. On pose pour tout entier $n \in [M]$, $M_n = \text{Cl}(\{\phi_R \mid R \in \Sigma, |R| = n\})$. Soit $\Sigma' = \{<\phi, n, E> \mid n \in$
$[N]$, $\phi \in M_n$, $E \subseteq [n]\} \cup \{\sharp\}$ avec $|<\phi, n, E>| = |E|$ et $|\sharp| = 1$. Pour tout $\mathcal{F}$-terme $t$, on définit la structure $S_t$ comme la $\Sigma'$-structure dont l'univers est l'ensemble des parties finies de $P_t^c$ et dont l'interprétation d'un symbole relationnel $<\phi, n, E> \in \Sigma'$ est défini comme suit:

$$
\begin{align*}
\langle \phi, n, E \rangle^{S_t} &= \{ (U_{\sigma(1)}, \dots, U_{\sigma(|E|)}) \mid (t_0, U_1, \dots, U_n) \in \phi \}, \quad \forall i, U_i \neq \emptyset \Rightarrow i \in E \}, \\
\sharp^{S_t} &= \{ U \subseteq P_t^c \mid U \text{ fini}, U \neq \emptyset \}.
\end{align*}
$$

Pour $t' \subseteq t$, on pose de plus $S_{t,t'} = S_t|_{S_{t'}^c}$.

La structure $S_{t,t'}$ peut contenir une infinité de sommets. Ils sont tous marqués par $\sharp$ sauf exactement un qui correspond à $\emptyset$. Si $t' = \perp$, alors $t'$ ne contient aucun sommet $c$ et donc $S_{t,t'}$ contient $\emptyset$ comme unique sommet.

**Lemme 5.31** Il existe un entier $k$, une partition de $\mathcal{T}^\omega(\mathcal{F})$ en $k$ parties $L_1, \dots, L_k$ et $k$ applications $f_1, \dots, f_k$ VRS'-définissable telles que pour tout $i \in [k]$, tout $\mathcal{F}$-terme $t \in L_i$ et tout $t' \subseteq t$ on a

$$
S_{t,t'} \approx f_i(S_{t,t'}) \quad \text{et} \quad S_{t,\perp} \approx f_i(\emptyset) .
$$

**Preuve.** L'égalité $S_{t,\perp} = \emptyset$ n'est pas satisfaite pour deux raisons. D'une part, les relations d'arité 0 peuvent avoir des interprétations non vides. D'autre part, l'univers de $S_{t,\perp}$ n'est pas vide car il contient l'élément $\emptyset$.

On construit alors la partition de $\mathcal{T}^\omega(\mathcal{F})$ induite par $M_n$. Ainsi, pour tout $\phi \in M_n$, notons $\phi|_0$ la formule obtenue en remplaçant partout dans $\phi$, $(f, \emptyset)$ par $f$, $(c, \emptyset)$ par $c$ et $(c, E)$ pour $E \neq \emptyset$ par $\emptyset$. Cette formule est telle que $\phi|_0[] = \{t \in \mathcal{T}^\omega(\mathcal{F}) \mid (t, \emptyset, \dots, \emptyset) \in \phi[]\}$.

Soit pour $W \subseteq M$, $\psi_W = (\cap_{\phi \in W} \phi|_0) \cap (\cap_{\phi \in M-W} (\mathcal{T}^\omega(\mathcal{F}) - \phi|_0))$. Les $\psi_W$ forment une partition de $\mathcal{T}^\omega(\mathcal{F})$. On a de plus pour toute formule $\phi \in M$, $\phi[] = \cup_{W \ni \phi} \psi_W$]. Soit maintenant $\mathcal{I}_W$ définie par

$$
\mathcal{I}_W = \left|
\begin{array}{ll}
\langle \phi, n, \emptyset \rangle () & : \text{vrai} \qquad \text{si } \phi \in W \\
\langle \phi, n, E \rangle (x_1, \dots, x_{|E|}) & : \langle \phi, n, E \rangle (x_1, \dots, x_{|E|}) \\
\sharp(x) & : \sharp(x)
\end{array}
\right|
$$

Pour tout $\mathcal{F}$-terme $t$ et tout terme $t' \subseteq t$, si $t \in \psi_W$ alors

$$
S_{t,t'} = \mathcal{I}_W(\mathrm{net}(S_{t,t'}))
$$

où net est l'interprétation qui laisse la structure invariante si ce n'est pour les symboles d'arité 0 qui ont pour nouvelle interprétation $\emptyset$.

Il reste maintenant à traiter l'élément $\emptyset$ de $S_{t,t'}$. Pour cela, on restreint d'abord
la structure aux éléments de l'interprétation de $\sharp$, c'est-à-dire que l'on élimine
l'élément $\emptyset$, puis on insère un nouvel élément pour le remplacer. Le symbole
relationnel ◦ d'arité 1 sert temporairement à identifier le sommet nouvellement ajouté. Il faut alors reconstruire les interprétations des symboles relationnels pour tenir compte de cette transformation.

$$
f(X) = \mathcal{I}_{\circ}(\mathbf{restrict}[\#](X) \oplus \mathbf{un}[\circ]),
$$
$$
\mathcal{I}_{\circ} = \left|
\begin{array}{l}
\langle \phi, n, E \rangle (x_{\sigma(1)}, \dots, x_{\sigma(|E|)}) : \bigwedge_{i \in E - E'} \circ(x_i) \\
\phantom{\langle \phi, n, E \rangle (x_{\sigma(1)}, \dots, x_{\sigma(|E|)}) : \bigwedge} \wedge \langle \phi, n, E' \rangle (x_{\sigma'(1)}, \dots, x_{\sigma'(|E'|)}) \\
E' \subseteq E \text{ et } \sigma \text{ bijection croissante de } [|E|] \text{ sur } E \\
\phantom{E' \subseteq E \text{ et }} \sigma' \text{ bijection croissante de } [|E'|] \text{ sur } E' \\
\#(x) : \#(x)
\end{array}
\right|
$$

On a alors la propriété suivante: pour tout $t \in \mathcal{T}^{\omega}(\mathcal{F})$ et $t' \subseteq t$,

$f(S_{t,t'}) \approx S_{t,t'} .$

Soit maintenant $f_W = f \circ \mathcal{I}_W$. Pour tout $t \in \psi_W$] et tout $t' \subseteq t$, on a
$f_W(\mathcal{S}_{t,t'}) \approx \mathcal{S}_{t,t'}$. De plus,

$$
\begin{align*}
f_W(\emptyset) &= f_W(\mathbf{restrict}[\#] \circ \mathbf{net}(\mathcal{S}_{t,\perp})) \\
&= \mathcal{I}_\circ(\mathbf{restrict}[\#] \circ \mathcal{I}_W \circ \mathbf{restrict}[\#] \circ \mathbf{net}(\mathcal{S}_{t,\perp}) \oplus \mathbf{un}[\circ]) \\
&= \mathcal{I}_\circ(\mathbf{restrict}[\#] \circ \mathbf{restrict}[\#] \circ \mathcal{I}_W \circ \mathbf{net}(\mathcal{S}_{t,\perp}) \oplus \mathbf{un}[\circ]) \\
&= \mathcal{I}_\circ(\mathbf{restrict}[\#](\mathcal{S}_{t,\perp}) \oplus \mathbf{un}[\circ]) \\
&= f_W(\mathcal{S}_{t,\perp}) \\
&= \mathcal{S}_{t,\perp}
\end{align*}
$$

□

**Lemme 5.32** *Il existe une interprétation booléenne positive *I*<sub>*p*</sub> telle que pour tous *F*-termes *t*<sub>1</sub>, *t*<sub>2</sub> et tous *t*'<sub>1</sub> ⊑ *t*<sub>1</sub> et *t*'<sub>2</sub> ⊑ *t*<sub>2</sub>, on a *I*<sub>*p*</sub>(*S*<sub>*t*<sub>1</sub>,*t*'<sub>1</sub></sub> ⊗<sub>*g*</sub> *S*<sub>*t*<sub>2</sub>,*t*'<sub>2</sub></sub>) ≈ *S*<sub>*p*(*t*<sub>1</sub>,*t*<sub>2</sub>),*p*(*t*'<sub>1</sub>,*t*'<sub>2</sub>)</sub> .*

**Construction.** Il suffit d'établir que $\mathcal{I}_p(\mathcal{S}_{t_1} \otimes_g \mathcal{S}_{t_2}) \approx \mathcal{S}_{p(t_1, t_2)}$. On pose :

$$
\mathcal{I}_p = \left|
\begin{array}{l}
\langle \phi, n, E \rangle (x_1, \dots, x_n) : \bigvee_{(\psi_1, \psi_2) \in D_{\phi}(p)} \langle \psi_1, n, E \rangle^1 (x_1, \dots, x_n) \\
\phantom{\langle \phi, n, E \rangle (x_1, \dots, x_n) : \bigvee_{(\psi_1, \psi_2) \in D_{\phi}(p)} \langle \psi_1, n, E \rangle^1} \wedge \langle \psi_2, n, E \rangle^2 (x_1, \dots, x_n) \\
\#(x) : \#(x)
\end{array}
\right| .
$$

où $D_{\phi}(p)$ est défini par le lemme 3.35.

□
## Démonstration du lemme 5.30

Considérons le transducteur déterministe $t_0$ d'état initial $q$ suivant :

$$ 
\begin{array}{l@{\qquad}l}
q(t) = f_i(q'(t)) & \text{si } t \in L_i \text{ pour } i \in [k] \\
q'(p(t_1, t_2)) = \mathcal{I}_p(t_1 \otimes_g t_2) & \\
q'(c) = \mathcal{S}_{c,c} &
\end{array}
$$

où $k, L_i$ et $f_i$ sont définis par le lemme 5.31 et $\mathcal{I}_p$ est l'interprétation du lemme 5.32. Soit $t \in L_i$. On définit les relations continues suivantes :

$$ 
\begin{array}{l}
\mathcal{R}[t](t', t'') \text{ si } \mathcal{S}_{t,t'} \approx [[t'』], \\
\mathcal{R}'[t](t', t'') \text{ si } \mathcal{S}_{t,t'} \approx f_i(\llbracket t'' \rrbracket).
\end{array}
$$

Il s'agit d'appliquer le lemme 3.59. La relation $\mathcal{R}$ correspond à l'état $q$ et la relation $\mathcal{R}'$ à l'état $q'$. Le lemme 5.31 montre que l'ensemble inévitable $\{q'\}$ remplit les conditions de l'hypothèse 3 du lemme 3.59. Les lemmes 5.31 et 5.32 établissent les invariants correspondant aux deux premières règles. La troisième transition est évidente. Le transducteur $t_0$ satisfait donc pour tout $\mathcal{F}$-terme $t$ l'isomorphisme suivant :

$$ \mathcal{S}_t \approx [[t_0(t)]] . $$

Pour retrouver $\mathcal{I}_F$, il suffit de restreindre les éléments à $\langle \phi_\delta, 1, [1] \rangle$, puis d'appliquer l'interprétation suivante :

$$ \mathcal{I} = \left| R(x_1, \dots, x_{|R|}) : \langle \phi_R, |R|, [|R|] \rangle (x_1, \dots, x_{|R|}), R \in \Sigma, R \neq \delta \right| . $$

Posons $\mathbf{t} = \mathcal{I} \circ \text{restrict}[\langle \phi_\delta, 1, [1] \rangle] \circ \mathbf{t}_0$. Ainsi, pour tout $\mathcal{F}$-terme $t$, $[[\mathbf{t}(t)]] \approx \mathcal{I}_F(t)$. Le lemme 11 appliqué à $\mathbf{t}$ nous fournit alors une transduction monadique $\mathbf{t}^*$ telle que pour tout $\mathcal{F}$-système d'équations, $\text{Solution}(\mathbf{t}^*(S)) \approx \mathcal{I}_F(\text{Depliage}(S))$.

### 5.2.4 Structures automatiques

La terminologie automatique [KN94] correspond originellement à des structures dont l'univers est un ensemble rationnel de mots et pour lesquelles les relations sont définies au moyen d'automates (de transducteurs synchronisés de mots). Dans notre cas, une structure admet une présentation automatique si elle admet une présentation terme-automatique définie sur des alphabet ne contenant que des symboles unaires et des constantes. Il s'agit d'une représentation interne. Une représentation équationnelle et une représentation par transformations de la famille des structures automatiques sont données ci-dessous. Nous ne précisons pas les démonstrations. Celles-ci sont très similaire aux précédentes.
## Représentation équationnelle

Les opérateurs $VRS'_1$ sont les suivants.

- La structure à un élément.

- L'union disjointe.

- L'interprétation booléenne positive.

- Le produit synchrone avec une structure finie.

- La restriction à l'interprétation d'un symbole relationnel unaire.

Ainsi, la seule distinction par rapport au cas des structures à présentation terme-automatique concerne l'utilisation restreinte du produit.

Nous pouvons maintenant énoncer le lemme attendu.

**Propriété 5.33** Une structure admet une présentation automatique si et seule-ment si elle est solution d'un $VRS'_1$-système fini d'équations.

Notons que des résultats de normalisation comparables à ceux concernants les $VRS'$-systèmes d'équations sont possibles.

## Représentation par transformation

La représentation par transformation est elle aussi très simple.

**Propriété 5.34** Une structure admet une présentation automatique si et seule-ment si elle est obtenue par interprétation monadique des parties finies de la demi-droite des entiers.
# Chapitre 6

## Graphes de récriture suffixe de termes

Nous avons étudié au paragraphe précédent les structures solutions de VR-systèmes d'équations étendus par (principalement) un opérateur de produit synchrone. Il s'agit d'une extension naturelle de ces opérateurs. Pourtant, il semble qu'il y ait de la place entre ces deux familles de structures. En particulier, si l'on considère la représentation interne, entre la récriture suffixe de mots et les relations terme-synchronisées, il est naturel de considérer des relations de récriture suffixe de termes. Il s'agit du propos de ce paragraphe. Cette étude n'est menée que sur les graphes et non sur les structures.

La récriture suffixe de termes procure une représentation interne de cette famille de graphes (paragraphe 6.1). Une représentation équationnelle est présentée au paragraphe 6.2. L'équivalence de ces deux représentations est établie au paragraphe 6.3. Ces graphes possèdent des propriétés de décidabilité plus nombreuses que les graphes termes-automatiques. En particulier, ils possèdent une théorie au premier ordre avec accessibilité décidable (paragraphe 6.4). Nous montrons ensuite un résultat similaire à celui de Barthelmann pour les graphes préfixes reconnaissables : les graphes de récriture suffixe de termes de largeur arborescente bornée sont les graphes HR-équationnels (paragraphe 6.5). Enfin, nous montrons qu'une extension naturelle de ce dernier résultat (les graphes de récriture suffixe de termes de largeur de clique bornée sont-ils les graphes préfixes reconnaissables ?) n'est pas vérifiée (paragraphe 6.6).

### 6.1 Représentation interne

Il s'agit ici de proposer une définition d'une famille de graphes obtenus par récriture suffixe de termes. Comme pour les graphes de récriture suffixe de mots, plusieurs approches successives ont été proposées. Nous les présentons tout d'abord
(paragraphe 6.1.1). Le paragraphe 6.1.2 présente quant à lui la définition que nous considérons par la suite.

## 6.1.1 Contexte

Étant donné un alphabet gradué $\mathcal{F}$, un système de récriture suffixe est un ensemble de règles $\Delta \subseteq \mathcal{T}(\mathcal{F}) \times \mathcal{T}(\mathcal{F})$. La relation de récriture suffixe par $\Delta$, $\to_{\Delta}$, reliant les $\mathcal{F}$-termes, est définie par récurrence comme suit:

- si $(t, t') \in \Delta$ alors $t \to_{\Delta} t'$,

- si $t = f(t_1, \dots, t_{|f|})$ et $t' = f(t'_1, \dots, t'_{|f|})$ pour $f \in \mathcal{F}$ et il existe $i$ tel que $t_i \to_{\Delta} t'_i$ et pour tout $i \neq j$, $t_j = t'_j$ alors $t \to_{\Delta} t'$.

La relation d'accessibilité par $\Delta$, notée $\to_{\Delta}^*$, est la clôture réflexive et transitive de $\to_{\Delta}$.

**Théorème 30 (Dauchet et Tison [DT90])** *Pour $\mathcal{F}$ un alphabet gradué, les graphes dont*

- l'univers est $\mathcal{T}(\mathcal{F})$,

- les arcs sont décrits par récriture suffixe de termes ou par accessibilité d'une relation de récriture suffixe de terme, ont une théorie au premier ordre décidable.*

Ce résultat repose sur le fait que ces graphes admettent une présentation terme-automatique. Le résultat est alors une conséquence directe du théorème de décidabilité de la théorie du premier ordre sur ces structures 5.19.

La définition des relations de récriture suffixe de termes est tout à fait similaire à celle des relations de récriture suffixe de mots. En fait, il s'agit d'une extension. On a vu dans le cadre des mots qu'il était naturel pour construire des graphes (ou des structures) de considérer un ensemble rationnel de sommets (resp. un univers rationnel). Ce type de restriction ne nous convient pas dans le cas présent car il fait perdre le résultat de décidabilité du théorème 30.

**Théorème 31 (Löding [LÖ2c])** *Il existe un graphe dont l'ensemble des sommets est une partie rationnelle de $\mathcal{T}(\mathcal{F})$, les interprétations des arcs sont des relations de récriture suffixe et pour lequel l'accessibilité n'est pas décidable.*

La solution utilisée par Löding pour éviter de perdre les propriétés de décidabilité en effectuant une restriction consiste à fixer un terme particulier, et à restreindre le graphe aux sommets accessibles à partir de ce sommet. Il suit en cela l'orientation des travaux originaux de Muller et Schupp.

Formellement, un *graphe de récriture suffixe avec restriction par accessibilité* (originellement GTRS dans [LÖ2a]) est décrit par un quadruplet $P = (\mathcal{F}, A, \Delta, t_0)$ où $\mathcal{F}$ est un alphabet gradué, $A$ est un ensemble d'étiquettes, $t_0$ est un $\mathcal{F}$-terme et $\Delta$ est une application de $A$ dans les parties finies de $\mathcal{T}(\mathcal{F}) \times \mathcal{T}(\mathcal{F})$. Le graphe $[P]$
<figure><img src="image_36.png" /><figcaption>FIG. 6.1 – Grille infinie comme graphe de récriture suffixe restreint par accessibilité.</figcaption></figure>

représenté par $P$ a alors pour ensemble de sommets $V_{[P]} = \{t \mid t_0 \to_{\cup_{a \in A} \Delta(a)} t\}$ et un arc étiqueté par $a \in A$ relie $t \in V_{[P]}$ à $t' \in V_{[P]}$ si $t \to_{\Delta(a)} t'$.

**Exemple 6.1 (grille infinie)** Considérons l'alphabet gradué $\mathcal{F} = \{P:2, S:1, A:0, B:0\}$, l'ensemble d'étiquettes $A = \{a, b\}$, les règles de récriture $\Delta$ sont définies par $\Delta(a) = \{(A,S(A))\}$ et $\Delta(b) = \{B,S(B)\}$ et l'état initial $t_0 = P(A,B)$. Le graphe présenté par $(\mathcal{F}, A, \Delta, t_0)$ est illustré à la figure 6.1.

On déduit de cet exemple et de la propriété 2.9 que les graphes de récriture suffixe ne possèdent pas une théorie monadique décidable. Par conséquence, ils ne sont pas inclus dans la famille des graphes préfixes reconnaissables.

En fait, l'inclusion inverse n'est pas non plus vérifiée. En effet, la définition des graphes de récriture suffixe restreint par accessibilité ne produit que des graphes connexes alors que certains graphes préfixes reconnaissables ne le sont pas. De plus, les graphes de récriture suffixe restreint par accessibilité sont de degré fini (non nécessairement borné), alors que ce n'est pas nécessairement le cas des graphes préfixes reconnaissables.

Le paragraphe suivant montre comment définir une famille de graphes reposant sur la récriture suffixe de termes et étendant les graphes préfixes reconnaissables.

## 6.1.2 Graphes de récriture suffixe de termes

Nous présentons dans ce paragraphe une famille de graphes étendant les graphes préfixes reconnaissables tout en étant définie par récriture suffixe de termes.

Une première extension consiste à considérer des règles de récriture reconnaissables (au lieu de finies). Rappelons que pour $\mathcal{F}$ un alphabet gradué, une partie de $\mathcal{T}(\mathcal{F}) \times \mathcal{T}(\mathcal{F})$ est reconnaissable si elle est égale à une union finie de produits
de parties reconnaissables de $\mathcal{T}(\mathcal{F})$ (les parties rationnelles).

Engelfriet montre que les relations de récriture suffixe reconnaissables par-
tagent les mêmes propriétés de clôture transitive que les relations de récriture
suffixe finies [Eng99]. Cela signifie qu’autoriser $\Delta(a)$ à être une partie recon-
naissable dans la définition des graphes de récriture suffixe avec restriction par
accessibilité préserve les propriétés de décidabilité.

Il reste toujours le problème de la restriction. Dans la définition de Löding,
seuls les sommets accessibles à partir de la racine sont considérés. Cette solution
ne permet pas de capturer les graphes préfixes reconnaissables. La solution pro-
posée ici consiste à utiliser un ensemble de sommets reconnu par un automate
d’arbres déterministe descendant [Col02a].

Ainsi, un *graphe de récriture suffixe* est décrit par la donnée d'un quadruplet
$P = (\mathcal{F}, A, \Delta, L)$ où $\mathcal{F}$ est un alphabet gradué, $A$ est un ensemble d'étiquettes,
$L \subseteq \mathcal{T}(\mathcal{F})$ est le langage accepté par un automate déterministe descendant et $\Delta$
est une application de $A$ dans les parties reconnaissables de $\mathcal{T}(\mathcal{F}) \times \mathcal{T}(\mathcal{F})$. Le
graphe $[P]$ présenté par $P$ a alors pour ensemble de sommets $V_{[P]} = L$, et un arc
étiqueté par $a$ relie un sommet $t$ à un sommet $t'$ si $t \to^{\Delta(a)} t'$.

On a alors bien la propriété souhaitée de capturer les graphes préfixes recon-
naissables.

**Propriété 6.2** *Les graphes préfixes reconnaissables sont, à isomorphisme près, des graphes de récriture suffixe.*

Il suffit pour montrer cela d'utiliser un codage direct des mots dans les termes.
Tout fonctionne bien car pour les termes ne contenant que des symboles d'arité 0
ou 1, la notion de rationnalité coïncide avec les langages reconnus par les auto-
mates déterministes descendants.

En fait, il est encore plus simple d'utiliser la représentation équationnelle
présentée au paragraphe 6.2 pour établir ce résultat.

**Exemple 6.3** *Reprenons l’exemple 6.1. L’ensemble des sommets de ce graphe est l’ensemble des termes {$P(S^n(A), S^m(B)) \mid n, m \in \mathbb{N}$} (où $S^n$ représente naturellement la puissance n-ième de l’application $t \mapsto S(t)$). Ce langage de termes est reconnu par un automate déterministe descendant. En effet, il s’agit de la valeur de $X$ solution du système d’équations suivant :*

$$
\begin{align*}
X &= P(Y, Z) \\
Y &= A + S(Y) \\
Z &= B + S(Z) .
\end{align*}
$$

La grille présentée à la figure 6.1 est donc aussi un graphe de récriture suffixe au
sens de ce paragraphe.
**Remarque 6.4** Une question naturelle est de savoir si tous les graphes de récriture suffixe restreint par accessibilité sont des graphes de récriture suffixe de termes comme définis ici. Une réponse négative à cette question a été établie par Löding. Nous ne la présentons pas ici.

## 6.2 Représentation équationelle

Tout comme les opérateurs VRS' étaient une extension des opérateurs VR' par un opérateur de produit, les opérateurs VRA sont une extension des opérateurs VR par un opérateur de produit, asynchrone cette fois-ci.

Soit $C$ un ensemble de couleurs et $\mathbf{A}$ un ensemble d'étiquettes. Les opérateurs $\mathrm{VRA}[C, \mathbf{A}]$ (ou plus simplement $\mathrm{VRA}$) sont les suivants :

- Le graphe coloré à un sommet de couleur $c \in C$ noté $\mathrm{sommet}[c]$,

- L'union disjointe de graphes colorés $\oplus$,

- L'ajout d'arcs étiquetés par $a \in \mathbf{A}$ entre un sommet de couleur $c \in C$ et un sommet de couleur $c' \in C$, noté $\mathrm{arc}[c, a, c']$,

- Le recoloriage par un application $\alpha$ de $C$ dans $C$, noté $\mathrm{recol}[\alpha]$,

- Le produit asynchrone $\Box_{\eta}$ où $\eta$ est une application de $C^2$ dans $C$. L'opérateur $\Box_{\eta}$ appliqué à deux graphes colorés $G_1$ et $G_2$ produit le graphe coloré $\mathcal{H} = G_1 \Box_{\eta} G_2$ défini par :

$$ \begin{gathered} \mathcal{U}_{\mathcal{H}} = \mathcal{U}_{G_1} \times \mathcal{U}_{G_2}, \\ \begin{array}{l} \text{pour tout } c \in C, \quad c^{\mathcal{H}} = \{(v_1, v_2) \in c_{G_1} \times c_{G_2} \mid (c_1, c_2) \in \eta^{-1}(c)\}, \\ \text{pour tout } a \in A, \quad \xrightarrow{a}^{\mathcal{H}} = \{((v_1, v_2), (v'_1, v'_2)) \mid v_1 \xrightarrow{a}^{\mathcal{G}_1} v'_1\} \\ \phantom{\text{pour tout } a \in A, \quad \xrightarrow{a}^{\mathcal{H}} =} \cup \{((v_1, v_2), (v_1, v'_2)) \mid v_2 \xrightarrow{a}^{\mathcal{G}_2} v'_2\}. \end{array} \end{gathered} $$

**Exemple 6.5 (Grille infinie)** On se fixe l'ensemble d'étiquettes $A = \{a, b\}$ et l'ensemble des couleurs $C = \{0, 1, 2, 3\}$. La demi-droite des entiers étiquetée par $a$ est solution de l'équation (sur les opérateurs VR) suivante :

$$ X_a = \mathrm{recol} \left[ \begin{array}{c} 0 \to 1 \\ 1 \to 1 \\ 2 \to 0 \end{array} \right] (\mathrm{arc}[2, a, 0](X_a \oplus \mathrm{sommet}[2])) . $$

Une équation similaire sur la variable $X_b$ a pour solution la demi-droite des entiers étiquetée par $b$. On construit alors le graphe solution de l'équation supplémentaire $X = X_a \Box_{\eta} X_b$ où $\eta(n, n') = n + n'$. Le résultat est présenté à la figure 6.2.

Ainsi, si l'on compare le graphe de cet exemple à celui de l'exemple 6.1 (figure 6.1), ils sont isomorphes (pourvu que l'on omette les couleurs). On remarque aussi
<figure><img src="image_37.png" /><figcaption>FIG. 6.2 – *Les demi-droites des entiers étiquetées par a et b, et leur produit asynchrone.*</figcaption></figure>

que l'ensemble des sommets d'une couleur donnée dans la grille de la figure 6.2 correspond à un ensemble rationnel de termes à la figure 6.1. Cet ensemble n'est pas nécessairement accepté par un automate déterministe descendant (considérer la couleur 1 par exemple). Le paragraphe suivant a pour objet de généraliser cet isomorphisme.

## 6.3 Équivalence de représentations

<figure><img src="image_38.png" /><figcaption>FIG. 6.3 – *Union disjointe de grilles carrées colorées.*</figcaption></figure>

Indiquons pour commencer le résultat démontré dans ce paragraphe (il s'agit en fait d'une extension du résultat présenté dans [Col02a]).

**Théorème 32** *Les familles de graphes suivantes sont isomorphes :*

- les solutions des VRA-systèmes d'équations,
- les graphes de récriture suffixe reconnaissable de termes restreints par les solutions d'Auto<sub>dd</sub><sup>T</sup>-systèmes d'équations, et ces conversions sont effectives.

Les détails concernant l'effectivité des conversions se trouvent dans les deux
lemmes 6.8 et 6.11 dont le théorème 32 est la combinaison.

Commençons par illustrer ce résultat.

**Exemple 6.6** *Considérons de nouveaux l'ensemble des couleurs C = {0, 1, 2, 3} et l'ensemble des étiquettes A = {a, b}. On définit pour n ∈ N le graphe G[a]n comme suit:*

$$
\mathcal{G}[a]_n = \underbrace{0 \xrightarrow{a} 1 \xrightarrow{a} 1 \cdots 1 \xrightarrow{a} 1}_{n+1 \text{ sommets}} .
$$

Ce graphe se définit par récurrence en utilisant les équations suivantes :

$$
\begin{align*}
\mathcal{G}[a]_0 &= \text{sommet}[0], \\
\mathcal{G}[a]_{n+1} &= \text{recol} \begin{bmatrix} 0 \to 1 \\ 1 \to 1 \\ 2 \to 0 \end{bmatrix} (\text{arc}[2, a, 0](\text{sommet}[2] \oplus \mathcal{G}[a]_n)).
\end{align*}
$$

Des équations comparables permettent de décrire les graphes $\mathcal{G}[b]_n$ définis similai-
rement. On peut maintenant construire le graphe $\mathcal{H}_n$ par l'équation suivante :

$$
\mathcal{H}_n = \mathcal{H}_{n+1} \oplus (\mathcal{G}[a]_n \sqcap \mathcal{G}[b]_n).
$$

Le graphe $\mathcal{H}_0$ décrit par ces équations est présenté à la figure 6.3. Il est formé
de l'union disjointe des graphes $\mathcal{G}[a]_n \sqcap \mathcal{G}[b]_n$, chacun étant une grille carrée de
dimension $n$.

**Exemple 6.7** Le même résultat peut être obtenu par un système de récriture suffixe restreint par un langage algébrique déterministe. Reprenons pour cela l'alphabet, les étiquettes et les règles de récriture de l'exemple 6.1, mais considérons le langage suivant comme ensemble de sommets :

$$
L = \{ S^k (P(S^n(A), S^m(B))) \mid k \in \mathbb{N}, 0 \le n < k, 0 \le m < k \} .
$$

Le graphe obtenu est de nouveau l'union disjointe des grilles carrées (cf. figure 6.3). L'entier k permet de numéroter la grille. Les contraintes 0 ≤ n < k et 0 ≤ m < k assurent que cette grille est bien carrée de taille k × k.

Il nous reste à montrer que le langage *L* est solution d'un Auto<sub>dd</sub><sup>*T*</sup>-système d'équations. Pour cela, commençons par construire les langages *U*<sub>*k*</sub> pour *k* ∈ N définis par *L*[*A*]>*k* = {*S*<sup>*n*</sup>(*A*) | 0 ≤ *n* < *k*}. Ces langages s'obtiennent comme solution des équations suivantes :

$$
\begin{align*}
L[A]_0 &= \emptyset \\
L[A]_{k+1} &= S(L[A]_k) + A
\end{align*}
$$
Des équations similaires produisent le langage $L[B]_k$ (définis comme on s'y attend). Le langage $L_l = \{S^k(P(S^n(A), S^m(B))) \mid k \in \mathbb{N}, 0 \le n < k + l, 0 \le m < k + l\}$ pour $l \in \mathbb{N}$ est alors défini par les équations suivantes :

$$L_l = S(L_{l+1}) + P(L[A]_l, L[B]_l).$$

Les systèmes d'équations apparaissant dans les exemples 6.6 et 6.7 sont struc-
turellement similaires (plus concrètement, il est possible de passer de l'un à l'autre
par une tansduction monadique). Ce n'est bien entendu pas anodin et les para-
graphes 6.3.1 et 6.3.2 établissent ces équivalences dans le cas général.

6.3.1 Des équations aux récritures

Pour la suite de ce paragaphe, on se fixe un ensemble *C* de couleurs et un
ensemble *A* d'étiquettes. On construit l'alphabet et les relations de récriture indé-
pendamment du système d'équations. Celui-ci ne sert qu'à déterminer l'ensemble
des sommets.

On considère donc l'alphabet gradué $\mathcal{F}$ suivant :

$$
\begin{align*}
\mathcal{F} = {}& \{U_1 : 1, U_2 : 1\} \\
& \cup \{P[\eta] : 2 \mid \eta \in C^{C \times C}\} \\
& \cup \{A[c, a, c'] : 1 \mid c, c' \in C, a \in A\} \\
& \cup \{R[\alpha] : 1 \mid \alpha \in C^C\} \\
& \cup \{S[c] : 0 \mid c \in C\}.
\end{align*}
$$

Bien entendu, chacun de ces symboles correspond à un des opérateurs $\mathbf{VRA}[C, A]$,
à savoir $U_1$ et $U_2$ pour $\oplus$, $P[\eta]$ pour $\square_{\eta}$, $A[c, a, c']$ pour l'opérateur $\mathbf{arc}[c, a, c']$,
$R[\alpha]$ pour $\mathbf{recol}[\alpha]$ et enfin $S[c]$ pour $\mathbf{sommet}[c]$. Il est à noter que le produit et
l'union disjointe ont un traitement différent correspondant à leurs sémantiques
distinctes.

Construisons maintenant les ensembles reconnaissables. Ceux-ci correspondent directement aux couleurs. On définit donc l'Auto<sup>T</sup>-système d'équations dont les variables sont les $L_c$ pour $c \in C$ et les équations sont les suivantes :

$$
\begin{align*}
L_c ={}& U_1(L_c) + U_2(L_c) \\
& + \sum_{\substack{\eta \in C^{C \times C} \\ \eta(c_1, c_2)=c}} P[\eta](L_{c_1}, L_{c_2}) \\
& + \sum_{c_1, c_2 \in C} A[c_1, a, c_2](L_c) \\
& + \sum_{\substack{\alpha \in C^C \\ \alpha(c')=c}} R[\alpha](L_{c'}) \\
& + S[c].
\end{align*}
$$
Les relations de récriture reconnaissables sont alors les suivantes.

$$ \Delta(a) = \bigcup_{c_1, c_2 \in C} A[c_1, a, c_2](L_{c_1}) \times A[c_1, a, c_2](L_{c_2}). $$

**Lemme 6.8** Il existe un transducteur déterministe **t** des VRA[$C$, $A$]-termes dans les Auto<sub>dd</sub><sup><i>T</i></sup>[$\mathcal{F}$]-termes tel que pout tout VRA[$C$, $A$]-terme **t**, $[\mathbf{t}]$ est isomorphe à la structure de récriture suffixe de termes de présentation ($\mathcal{F}$, $A$, $\Delta$, $[\mathbf{t}(t)]$).

**Construction.** Le transducteur possède un unique état (initial) $q$ et ses règles de transition sont les suivantes :

$$
\begin{align*}
q(x \oplus y) &\rightarrow U_1(q(x)) + U_2(q(y)) \\
q(x \sqcap \eta y) &\rightarrow P[\eta](q(x), q(y)) \\
q(\mathbf{arc}[c, a, c')(x)) &\rightarrow A[c, a, c')(q(x)) \\
q(\mathbf{recol}[\alpha](x)) &\rightarrow R[\alpha](q(x)) \\
q(\mathbf{sommet}[c](x)) &\rightarrow S[c]
\end{align*}
$$

On montre alors par récurrence sur $n \in \mathbb{N}$ que :

$$ \mathrm{nb}([\mathbf{t}\downarrow_n]) \approx [(\mathcal{F}, A, \Delta, [\mathbf{t}(t)\downarrow_n])] . $$

□

**Remarque 6.9** Dans cette construction, si le VRA-terme $t$ ne contient pas d'opérateur produit, alors l'alphabet utilisé par le terme $t(t)$ ne possède que des symboles d'arité 0 ou 1. Le terme résultat peut donc être assimilé à un mot. Le graphe résultat est alors suffixé reconnaissable restreint par un langage déterministe.

### 6.3.2 De la récriture aux équations

Considérons un alphabet gradué $\mathcal{F}$, un ensemble d'étiquettes $A$ et une application $\Delta$ de $A$ dans les parties reconnaissables de $\mathcal{T}(\mathcal{F}) \times \mathcal{T}(\mathcal{F})$.

À chaque étiquette $a \in A$ correspond par $\Delta$ une partie reconnaissable de $\mathcal{T}(\mathcal{F}) \times \mathcal{T}(\mathcal{F})$.

**Lemme 6.10** Il existe un automate d'arbres $(Q, \delta)$ (sans états terminaux) déterministe ascendant et complet tel que pour tout $a$, il existe $\Delta'(a) \subseteq Q \times Q$ tel que :

$$ \Delta(a) = \bigcup_{(q, q') \in \Delta'(a)} \delta^{-1}(q) \times \delta^{-1}(q'). $$
**Preuve.** En considérant l'ensemble des automates impliqués dans la description de $\Delta$ comme un unique automate, puis en le déterminisant. $\square$

**Lemme 6.11** *Il existe un transducteur déterministe des $Auto_{dd}^T[\mathcal{F}]$-termes vers les VRA-termes tel que pour tout $Auto_{dd}^T[\mathcal{F}]$-terme $t$,*

$$ [(\mathcal{F}, A, \Delta, [[t]])] \approx \mathbf{nb}([\mathbf{t}(t)]) . $$

**Construction.** Soient $Q$ et $\delta$ tels qu'obtenus par le lemme 6.10.

L'ensemble des couleurs du terme produit par le transducteur déterministe est $Q$.

On utilise une version généralisée à toute arité des symboles $\oplus$ et $\square$ (y compris en ce qui concene le paramètre $\eta$ de $\square$).

Le tansducteur déterministe est alors défini comme suit:

$$ q\left(\sum_{f \in F} f(x_{f,1}, \dots, x_{f,|f|})\right) = \mathbf{arc}[D] \left( \bigoplus_{f \in F} \Box_{\eta_f \ i \in \lfloor|f|\rfloor} q(x_{f,i}) \right) \\ \text{avec } D = \{(q, a, q') \mid (q, q') \in \Delta'(a)\} $$

$$ \text{et } \eta_f(q_1, \dots, q_{|f|}) = q \text{ tel que } (f(q_1, \dots, q_{|f|}), q) \in \delta. $$

$\square$

## 6.4 Premier ordre avec accessibilité

La logique du premier ordre avec accessibilité est une simple extension de la logique du premier ordre sur les graphes par un opérateur d'accessibilité. Formellement, étant donné un ensemble d'étiquettes $B \subseteq A$, la relation binaire $B^* \to a$ pour interprétation l'ensemble des couples de sommets $(u, v)$ tels qu'il existe un chemin étiqueté par $B^*$ reliant $u$ à $v$.

Nous montrons ici que l'ensemble des modèles d'une formule du premier ordre augmenté des prédicats d'accessibilité sont VRA-reconnaissable. En fait, le principe de la preuve est simplement de ramener au moyen d'un transducteur déterministe le problème à un problème de décidabilité pour un VRS-système d'équations.
L'hypothèse de récurrence

Supposons l'ensemble d'étiquettes **A** fixé. On s'intéresse aux structures sur l'ensemble des symboles relationnels suivants :

$$
\begin{array}{ll}
\Sigma = \{ \stackrel{a}{\rightarrow} | a \in \mathbf{A} \} & \text{avec } \stackrel{a}{\rightarrow} = 2, \\
\cup C & |c| = 1, \\
\cup \{ \langle B^* \rangle | B \subseteq \mathbf{A} \} & | \langle B^* \rangle | = 2, \\
\cup \{ \langle cB^* \rangle | B \subseteq \mathbf{A}, c \in C \} & | \langle cB^* \rangle | = 1, \\
\cup \{ \langle B^*c \rangle | B \subseteq \mathbf{A}, c \in C \} & | \langle B^*c \rangle | = 1, \\
\cup \{ \langle cB^*c' \rangle | c, c' \in C, B \subseteq \mathbf{A} \} & \text{et } | \langle cB^*c' \rangle | = 0.
\end{array}
$$

L'objectif est, à partir d'un graphe coloré par *C* et étiqueté par *A*, de construire une $\Sigma'$-structure codant à la fois le graphe et les relations d'accessibilité. Les symboles $\xrightarrow{a}$ représentent les arcs originaux du graphe et les symboles binaires $\langle B^* \rangle$ identifient les couples de sommets reliés par un chemin étiqueté par un mot de $B^*$. Les symboles $\langle cB^* \rangle$, $\langle B^*c \rangle$ et $\langle cB^*c' \rangle$ servent aux constructions intermédiaires : ils identifient les chemins dont l'origine et/ou la destination est/sont d'une certaine couleur.

Formellement, étant donné un graphe $\mathcal{G}$ coloré par $C$ et étiqueté par $A$, on construit la structure $*(\mathcal{G})$ définie comme suit.

$$
\begin{align*}
\mathcal{U}_{*(\mathcal{G})} &= V_{\mathcal{G}}, \\
c^{*(\mathcal{G})} &= c^{\mathcal{G}}, \\
\underset{*(\mathcal{G})}{\stackrel{a}{\rightarrow}} &= \underset{\mathcal{G}}{\stackrel{a}{\rightarrow}}, \\
\langle B^* \rangle^{*(\mathcal{G})} &= \{(v, v') \mid \exists w \in B^*. \, v \xrightarrow{w} \mathcal{G} \, v'\}, \\
\langle cB^* \rangle^{*(\mathcal{G})} &= \{v \mid \exists v' \in c^{\mathcal{G}}, w \in B^*. \, v' \xrightarrow{w} \mathcal{G} \, w\}, \\
\langle B^*c \rangle^{*(\mathcal{G})} &= \{v \mid \exists v' \in c^{\mathcal{G}}, w \in B^*. \, v \xrightarrow{w} \mathcal{G} \, v'\}, \\
\langle cB^*c' \rangle^{*(\mathcal{G})} &= \{() \mid \exists v \in c^{\mathcal{G}}. \exists v' \in c'^{\mathcal{G}}. \exists w \in B^*. \, v \xrightarrow{w} \mathcal{G} \, v'\}.
\end{align*}
$$

Récurrence

On s'intéresse maintenant à transformer un VRA-système d'équations en un VRS-système d'équations tel que la solution du second s'obtienne par application de * à la solution du premier. Cette traduction est effectuée par un transducteur déterministe. Il s'agit donc de présenter les propriétés permettant de valider cette construction, et qui sont données par les lemmes 6.12, 6.13, 6.14 et 6.15.
**Lemme 6.12** Pour toute application $\alpha$ de $C$ dans $C$, il existe un interprétation $\mathcal{I}_{\text{recol}[\alpha]}$ booléenne positive des $\Sigma'$-structures dans les $\Sigma'$-structures telle que pour tout graphe coloré $\mathcal{G}$, on a :

$$ \ast(\text{recol}[\alpha](\mathcal{G})) = \mathcal{I}_{\text{recol}[\alpha]}(\ast(\mathcal{G})) . $$

**Construction.** On pose simplement

$$ \mathcal{I}_{\text{recol}[\alpha]} = \left| \begin{array}{lclcl} c(x) & : & c'(x) & & \alpha(c') = c \\ x \xrightarrow{a} y & : & x \xrightarrow{a} y & & \\ < B^* > (x, y) & : & < B^* > (x, y) & & \\ < cB^* > (x) & : & < c'B^* > (x) & \alpha(c') = c & \\ < B^*c > (x) & : & < B^*c' > (x) & \alpha(c') = c & \\ < c_1B^*c_2 > & : & < c'_1B^*c'_2 > & \alpha(c'_1) = c_1 \text{ et } \alpha(c'_2) = c_2 & \end{array} \right| . $$

□

**Lemme 6.13** Pour toutes couleurs $c_1, c_2 \in C$ et toute étiquette $a \in A$, il existe une interprétation $\mathcal{I}_{\text{arc}[c_1, a, c_2]}$ telle que pour tout graphe coloré $\mathcal{G}$ on a :

$$ \ast(\text{arc}[c_1, a, c_2](\mathcal{G})) = \mathcal{I}_{\text{arc}[c_1, a, c_2]}(\ast(\mathcal{G})) $$

**Preuve.**

$$ \mathcal{I}_{\text{arc}[c_1, a, c_2]} = \left| \begin{array}{lclcl} c(x) & : & c(x) & & \\ x \xrightarrow{b} y & : & x \xrightarrow{b} y & \text{pour } b \in A \\ x \xrightarrow{a} y & : & c_1(x) \wedge c_2(y) & & \\ < B^* > (x, y) & : & < B^* > (x, y) & & \\ < B^* > (x, y) & : & < B^*c_1 > (x) \wedge < c_2B^* > (y) & \text{pour } a \in B \\ < cB^* > (x) & : & < cB^* > (x) & & \\ < cB^* > (x) & : & < cB^*c_1 > \wedge < c_2B^* > (x) & \text{pour } a \in B \\ < B^*c > (x) & : & < B^*c > (x) & & \\ < B^*c > (x) & : & < B^*c_1 > (x) \wedge < c_2B^*c > & \text{pour } a \in B \\ < cB^*c' > & : & < cB^*c' > & & \\ < cB^*c' > & : & < cB^*c_1 > \wedge < c_2B^*c' > & \text{pour } a \in B \end{array} \right| . $$

La construction fonctionne sur la remarque suivante : un chemin entre deux sommets $v$ et $v'$ de $\text{arc}[c_1, a, c_2](\mathcal{G})$ peut être de l'une des deux formes suivantes :

- il s'agit d'un chemin n'empruntant aucun des arcs ajoutés par l'opérateur $\text{arc}[c_1, a, c_2]$, et dans ce cas, il était déjà présent dans $\mathcal{G}$,