RIA
laboria

laboratoire de recherche
en informatique
et automatique

Algorithmes d'équivalence
et de réduction à des
expressions minimales
dans une classe
d'équations récursives
simples

B.Courcelle . G.Kahn . J.Vuillemin

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
78150 - Le Chesnay
Tél. 954.90.20

Rapport de Recherche n° 37

novembre 1973
ALGORITHMES D'EQUIVALENCE ET DE RÉDUCTION A DES
EXPRESSIONS MINIMALES DANS UNE CLASSE D'EQUATIONS
RÉCURSIVES SIMPLES

B. Courcelle, G. Kahn, J. Vuillemin

Résumé.

Nous décrivons ici un algorithme pour décider de l'équiva-
lence dans un domaine dont les éléments sont définis par
des schémas d'équations au point fixe. Cet algorithme est
utilisé pour trouver diverses représentations minimales
des éléments du domaine.

Mots clés.

Points fixes - Schémas de programmes - Domaines de calcul.

Abstract.

In this paper, we describe an algorithm for deciding equi-
valence in a domain whose objects are defined by uninterpre-
ted fixed-point equations. The algorithm is then applied to
finding a minimal representation of those objects or to
removing mutual recursion whenever possible.

Key words.

Fixed-points - Schemas of Mutual recursion - Complete par-
tial order.
# INTRODUCTION.

Plusieurs travaux récents, par exemple [3], [6], [7], [8] utilisent la notion d'équation au point fixe pour exprimer la sémantique des langages de programmation. Nous étudions ici un "pur langage de points fixes" dans lequel aucune fonction de base n'est interprétée, ce qui élimine en particulier l'opérateur conditionnel _si_ - _alors_ - _sinon_.

Au sujet des équations au point fixe, dont un exemple typique est l'équation $X \leftarrow f(X, g(X))$ nous nous posons un certain nombre de questions, par exemple :

- est-ce que $X \leftarrow f(X, g(X))$ est équivalente à

$$Y \leftarrow f(f(Y, g(Y)), g(Y)) ?$$

- existe-t-il une équation plus simple équivalente à

$$Z \leftarrow g(g(Z)) \quad \text{ou au système}$$

$$\begin{cases} X \leftarrow f(Y, g(X), Y) \\ Y \leftarrow g(X) \end{cases}$$

- la variable $X$ définie par le système

$$\begin{cases} X \leftarrow f(X, Y) \\ Y \leftarrow g(X, Y) \end{cases}$$

pourrait-elle l'être par une seule équation ?

Dans la première partie, nous étudions les **équations récursives simples**. Nous montrons l'existence **d'une forme canonique** caractérisant une classe d'équivalence d'équations. La forme cano-
nique minimise la *taille* de l'équation dans sa classe d'équivalence.

La deuxième partie, indépendante de la première (sauf en ce qui concerne les définitions de la syntaxe et de la sémantique) étudie les mêmes problèmes pour les *systèmes d'équations récursives*, dégage une notion de forme *canonique* mais qui ne minimise pas le nombre d'équations du système. Ce dernier problème est ensuite abordé et résolu.

Ce travail est motivé par des questions aussi différentes que l'étude des définitions récursives des modes en Algol 68 (Lewis-Rosen [4]), la formalisation des preuves d'équivalences entre programmes parallèles (Kahn [3]) ou la recherche de sous théories décidables dans la théorie des schémas de programmes.

# I- EQUATIONS RECURSIVES SIMPLES.

Pour la clarté de l'exposé, nous commençons par définir les équations au point-fixe à une seule inconnue.

## 1.1 Syntaxe.

Les *termes* sont construits à l'aide de symboles de fonction $\{F, G, H, ...\}$ ayant chacun une certaine arité, et du symbole de variable $X$ par les règles :

(i) Les symboles de fonction d'arité $O$, ou * constantes * et le symbole $X$ sont des termes.

(ii) Si $T_1, T_2, ... T_n$ sont des termes et $F$ est un symbole de fonction d'arité $n$, alors $F(T_1, T_2, ... T_n)$ est un terme.

Si $T$ est un terme, $X \leftarrow T$ est une équation au point fixe.
Pour la suite il sera utile de munir l'ensemble des termes
d'une structure d'ordre partiel < définie par les règles suivantes:

(i) Pour tout terme T, nous avons X < T.

(ii) Si $T_1 < T'_1$, $T_2 < T'_2$ ... $T_n < T'_n$ alors

$F(T_1, ..., T_n) < F(T'_1, ..., T'_n)$.

Etant donnés deux termes T et T' nous pouvons définir
un minorant $\Sigma (T,T')$ tel que $\Sigma (T,T') < T$ et $\Sigma (T,T') < T'$ de la fa-
çon suivante :

$$
- \Sigma (T, X) = \Sigma (X, T) = X
$$

$$
- \sum (F(T_1, T_2, \dots, T_n), G(T'_1, T'_2, \dots, T'_n)) = X \quad \text{si} \quad F \neq G
$$

$$
- \sum (F(T_1, T_2, \dots, T_n), F(T'_1, T'_2, \dots, T'_n)) = F(\sum (T_1, T'_1), \dots, \sum (T_n, T'_n))
$$

Notation :

Pour un terme T dans lequel figure m fois la lettre X
nous désignons par T{T₁,...T_m} le résultat de la substitution
du terme Tᵢ à la ième occurence de X dans T, pour chaque i
dans [1,m].

Lemme 1 :

Pour tous termes T et T' il existe des termes T₁,...Tm
et T'_1,...T'_m tels que :

$$
T = \sum (T, T') \{T_1, \dots, T_m\}
$$

$$
T' = \sum (T, T') \{T_1', \dots, T_m'\}
$$
Démonstration :

Voir Nivat [7]. De fait, Nivat montre que la relation $\prec$ mutant l'ensemble des termes d'une structure de treillis et que $\Sigma (T,T')$ est la borne inférieure de deux termes $\blacksquare$.

## 1.2 Sémantique.

a) Nous interpréterons les équations au point fixe sur un domaine $\mathcal{B}$ qui doit satisfaire les propriétés suivantes :

(i) L'ensemble $\mathcal{B}$ est muni d'une relation d'ordre partiel $\preceq$.
Nous notons $\equiv$ la relation d'équivalence induite.

(ii) Il existe dans $\mathcal{B}$ un élément minimal $\bot$.

(iii) Toute chaîne croissante dénombrable possède une borne supérieure.

Cette structure, qui est légèrement moins restrictive que celle de treillis complet dont se sert Scott [8], est aussi utilisée dans [5], [6] et [10].

b) - A chaque symbole de constante C est associé un élément $c$ dans $\mathcal{B}$.

- A chaque symbole de fonction $F$ d'aritén est associée une application $f$ de $\mathcal{B}^n$ dans $\mathcal{B}$ qui est *monotone* et *continue* en chacun de ses arguments (Voir [5] pour une définition de ces notions).

- A tout terme $T$ se trouve alors associée de façon naturelle une application $t$ de $\mathcal{B}$ dans $\mathcal{B}$ et à l'équation au point fixe $X \leftarrow T$ on associera le plus petit point fixe de $t$: $\mathcal{B} \to \mathcal{B}$ que l'on appelera encore plus petit point fixe de l'équation.
Il est défini comme la borne supérieure dans $\mathcal{A}$ de l'ensemble

$$ \{t^n(\perp) | n \ge 0\}. $$

(Voir encore Milner [5] pour une construction rigoureuse).

**Convention :**

Nous utiliserons systématiquement des lettres majuscules pour désigner les objets syntaxiques et les minuscules correspondantes pour désigner les objets sémantiques associés.

c) Nous allons maintenant construire une **interprétation canonique** de notre langage, qui joue le rôle de l'univers de Herbrand pour les théories du premier ordre. Le domaine $\mathcal{A}$ de l'interprétation canonique est constitué par l'ensemble des **suites infinies de termes** $\{T_i | i \in N\}$ telles que $T_i < .T_{i+1}$ pour tout $i \ge 0$ construits sur la variable $\Omega$.

Nous définissons maintenant une relation d'ordre $\preceq$ sur $\mathcal{A}$ :
Si $\tau = \{T_i | i \in N\}$ et $\tau' = \{T'_i | i \in N\}$ sont deux éléments de $\mathcal{A}$, alors
$\tau \preceq \tau$ si et seulement si $\exists j: T_i < T_j$.

L'élément minimal de $\mathcal{A}$ est $\perp = \{T_i | \forall i \in N, T_i = \Omega\}$.
Toute chaîne $\tau_1 \preceq \tau_2 \preceq \dots \preceq \tau_i \preceq \dots$ dans laquelle $\tau_i = \{T_j^i | j \in N\}$
admet la borne supérieure $\tau = \bigcup_{i \in N} \tau_i = \{T_k^k | k \in N\}$.

Une constante $C$ est alors interprétée par la suite :

$$ C = \{T_i | T_i = C, i \in N\} $$

L'interprétation f. du symbole n-aire F associe aux suites $\{T_k^i | k \in N\}$ pour $i$ dans $[1,n]$ la suite $\{F(T_k^1, T_k^2, \dots, T_k^n) | k \in N\}$.
Il est aisé de vérifier que nous avons bien là une interprétation légitime.
Notons $P\{A/X\}$ le résultat de la substitution dans un terme $P$ de $A$ à toutes les occurences de $X$. On vérifiera que dans notre interprétation canonique $Y(t) = \{T^i | i \in N\}$ avec

$$T' = T\{\Omega/X\} \text{ et } T^{i+1} = T\{T^i/X\}$$

L'intérêt de l'interprétation canonique vient du lemme suivant :

**Lemme 2 :**

_Deux équations au point fixe sont équivalentes si et seulement si elles sont équivalentes dans l'interprétation canonique._

_Démonstration :_

Il nous suffit de démontrer que si $X \leftarrow T$ et $X \leftarrow T'$ sont équivalentes dans l'interprétation canonique $C$, elles seront équivalentes dans toute autre interprétation $I$.

Soient $Y(t) = \{T^i | i \in N\}$ et $Y(t') = \{T'^j | j \in N\}$ les points fixes de ces équations dans l'interprétation canonique. Il est aisé de vérifier que $T_1 < T_2$ implique $t_1(\perp) \stackrel{C}{=} t_2(\perp)$ pour toute interprétation $I$. Comme $\forall i \exists j \ T^i < T'^j$ on en déduit

$\forall i \exists j \ t_i^i(\perp) \stackrel{C}{=} t'^j(\perp)$ et par symétrie

$\forall k \exists 1 \ t'^k(\perp) \stackrel{C}{=} t^1(\perp)$.

Par suite, dans $I$, $\bigcup_{i \in N} t_i^i(\perp) \equiv \bigcup_{i \in N} t'^j(\perp)$. ■

Nous pouvons maintenant énoncer deux lemmes techniques qui seront utiles dans la suite.
**Lemme 3 :**

Si deux termes $F(T_1, \dots, T_n)$ et $G(T'_1, \dots, T'_m)$ sont égaux dans l'interprétation canonique, alors $F = G, n = m$, et pour tout $i$ $T'_i = T_i$ dans l'interprétation canonique.

**Démonstration :**

Soient $\{T_k^i | i \in N\}$ et $\{T_k'^i | i \in N\}$ les interprétations de $T_k$ et $T_k'$. Puisque :

Pour tous termes $T$ et $T'$, si $Y(t) \subseteq Y(t')$ dans l'interprétation canonique, alors, ou bien $T = X$, ou bien $Y(t) \equiv Y(t')$.

$F = G, n = m$ et

$\forall i \in j \quad T_k^i < T_k'^j \quad (k \in [1,n])$ et l'inégalité symétrique ■

**Lemme 4 :**

**Démonstration :**

a) Définissons d'abord deux notions de "profondeur" d'un terme $T$, $pmax(T)$ et $pmin(T)$ :

$$ 
\begin{cases}
pmax(X) = pmax(C) = 1 & (\text{si } C \text{ est une constante}) \\
pmax(F(T_1, \dots, T_n)) = 1 + \max_{1 \le i \le n} \{pmax(T_i)\} \\
pmin(X) = 1; \quad pmin(C) = +\infty & (\text{si } C \text{ est une constante}) \\
pmin(F(T_1, \dots, T_n)) = 1 + \min_{1 \le i \le n} \{pmin(T_i)\}
\end{cases}
$$

Ces notions nous permettent d'énoncer la propriété d'"alignement" suivante :
si $T_1, T_2, T_3$ vérifient $T_1 \langle T_3$ et $T_2 \langle T_3$ et $pmax(T_1) \le pmin(T_2)$ alors $T_1 \langle T_2$. La preuve se fait aisément par induction sur la structure de $T_3$.

b) Etant donnés maintenant deux points fixes

$Y(t) = \{T^i | i \in N\}$ et $Y(t') = \{T'^i | i \in N\}$, s'ils vérifient $Y(t) \subseteq Y(t')$ alors $\forall i \in j \ T^i \prec T'^j$.

Montrons que l'on a aussi $\forall j \in T^j \prec T'^j \prec T^i$, si $T \ne X$, étant donné $T^j$, on peut toujours trouver un $i \in T$ tel que

$$pmin(T^i) \ge pmax(T^j).$$

Il est alors possible de trouver un $k \in T^k$ tel que $k \ge j$ et $T^i \prec T'^k$. Donc $T^j \prec T'^k$ et d'après la propriété d'alignement, $T^j \prec T^i$. Donc $Y(t') \subseteq Y(t)$. ■

## 1.3 Forme normale et algorithme d'équivalence.

Nous allons montrer que l'ensemble des termes conduisant à des équations au point fixe équivalentes est clos par rapport à l'opération $\Sigma$.

### Notation :

Si deux termes $T$ et $T'$ ont pour interprétation $t$ et $t'$ dans l'interprétation canonique, nous noterons $\sigma(t,t')$ l'interprétation de $\Sigma(T,T')$.

### Lemme 5 :

Si $t(a) \equiv t'(a)$ pour un certain $a$, alors $\sigma(t,t')(a) \equiv t(a) \equiv t'(a)$
## Démonstration :

Par induction sur la structure de $T$ :

1) Si $T = X$ ou $T = C$ la propriété est évidente.

2) Si $T = F(T_1, \dots, T_n)$ deux cas se présentent :

- $T' = X$, donc $\Sigma (T, T') = X$ et la propriété est vraie.

- $T' = G(T_1, \dots, T_m)$ et alors nécessairement $F = G, m = n$ et $t_i(a) = t_i(a)$ pour tout $i$ dans $[1, n]$. Par l'hypothèse d'induction, $\sigma(t_1, t_2, \dots, t_n)(a) = t_i(a)$ et donc

$$t(a) = f(\sigma(t_1, t_1')(a), \dots, \sigma(t_n, t_n')(a)) = \sigma(t, t')(a) \blacksquare$$

## Lemme 6 :

Si deux termes $T$ et $T'$ ont le même point fixe, alors $\Sigma (T, T')$ a aussi le même point fixe. Autrement dit $Y(t) = Y(t')$ implique $Y(t) = Y(\sigma(t, t'))$.

## Démonstration :

Nous avons $Y(t) = t(Y(t)) = Y(t') = t'(Y(t')) = t'(Y(t))$. Par le lemme 4 nous obtenons $\sigma(t, t')(Y(t)) = Y(t)$ et par minima-lité $Y(\sigma(t, t')) = Y(t)$. Le lemme 3 implique alors :

- ou bien $Y(\sigma(t, t')) = Y(t)$ et la preuve est finie ;

- ou bien $\Sigma (T, T') = X$, mais ceci n'est compatible avec $Y(t) = Y(t')$ que si $T = T' = X$ auquel cas nous avons en-core $Y(\sigma(t, t')) = Y(t)$. ■

Nous sommes maintenant prêts à démontrer (de manière non constructive) l'existence d'une **forme minimale** pour l'ensemble
des termes conduisant à des équations au point fixe équivalentes.

Désignons par $||T||$ la "taille" d'un terme T définie récursivement par :

$$1) \quad ||X|| = 0$$

$$2) \quad \| F(T_1, \dots, T_n) \| = 1 + \sum_{i=1}^{n} \| T_i \|.$$

**Lemme 7 :**

Dans l'ensemble $E(T) = \{T' | Y(t') \equiv Y(t)\}$ des termes ayant même plus petit point fixe que T, il existe un élément unique T de taille minimale.

**Démonstration :**

Soient $T_1$ et $T_2$ deux termes de $E(T)$ différents et de taille minimale. Alors $T_1$ et $T_2$ sont forcément incomparables, sinon, d'après le lemme 1, l'un deux serait de taille strictement plus petite que l'autre. Mais alors, toujours d'après le lemme, $||\Sigma (T_1, T_2)|| < ||T_1||$. Comme $E(T)$ est fermé par $\Sigma$ d'après le lemme 6, $T_1$ et $T_2$ ne pourraient être minimaux. ■

Pour l'instant, le lemme 7 ne permet pas de construire $T^*$, mais nous allons exhiber une relation syntactique entre tous les termes ayant même point fixe que $T^*$. Notons $T' \to T''$ la relation définie par les axiomes suivants :

$$i) \quad \vdash T \to T$$

$$ii) \quad T \to U \vdash T \to U \{X/T\}$$

où la notation $U\{X/T\}$ signifie que certaines occurrences de X dans U ont été remplacées par T. Notons $D(T) = \{U | \vdash T \to U\}$.
**Théorème 1 :**

L'ensemble $E(T)$ des termes ayant même point fixe que $T$ est identique à l'ensemble $D(T^*) = \{ U \mid T \to T^* \to U \}$ des termes dérivant de l'élément minimal $T^*$ de $E(T)$.

**Démonstration :**

Bien entendu $E(T) = E(T^*)$. Le fait que $D(T^*) \subseteq E(T^*)$ est déjà connu (par exemple cf. [10]). Montrons maintenant que $E(T^*) \subseteq D(T^*)$ : soit $T$ un terme de longueur minimale appartenant à $E(T^*)$ et non à $D(T^*)$. On a nécessairement $T^* \subset T$ puisque $T^*$ est une forme normale. Donc $T' = T^* \{T_1, \dots, T_k\}$. Comme $T'$ est dans $E(T^*)$, nous avons :

$$Y(t^*) \equiv Y(t') \equiv t'(Y(t')) \equiv t'(Y(t^*)).$$

$$\text{Donc } t^*(Y(t^*)) = t'(Y(t^*)). \blacksquare$$

Par le lemme 3, on en déduit $Y(t^*) = t_i(Y(t^*))$ pour $i \in [1,k]$. Par minimalité puis le lemme 4, on obtient $Y(t_i) = Y(t^*)$. Mais comme les $T_i$ sont plus petits que $T'$ ils sont par hypothèse dans $D(T^*)$. Par suite $T'$ est dans $D(T^*)$. ■

Le théorème 1 implique que la forme normale $T^*$ de $T$ est un sous-terme de $T$, à savoir le plus petit sous-terme $T^*$ tel que $T^* \to T$. Ceci nous donne donc un algorithme de calcul de cette forme normale et un processus de décision de l'équivalence de deux équations au point fixe. Plutôt qu'exposer ces deux algorithmes en plus de détail ici, nous passons maintenant au cas général, celui des systèmes d'équations au point fixe.

## II- SYSTEMES D'EQUATIONS RECURSIVES.

Les résultats obtenus dans la première partie se généralisent au cas des systèmes d'équations au point fixe : à tout sys-
tème, on peut associer un système dit canonique de taille mini-
male (La "taille" d'un système étant la somme des tailles des
équations qui le constituent). On obtient ainsi un algorithme
pour décider de l'équivalence de deux systèmes et l'on peut aussi
calculer un système équivalent ayant un nombre minimum d'équations.
Cependant, ce dernier système n'est pas nécessairement unique.

## 2.1 Syntaxe.

Un **système** est la donnée :

i) d'une famille d'équations au point fixe $X_i \leftarrow T_i$, pour $i = 1,2,...,n$. Les termes $T_i$ sont construits sur les variables $X_i$, $i \in [1,n]$.

ii) d'une variable principale $X_1$.

Un système est dit **connexe** si toutes ses équations sont nécessaires au calcul de $X_1$, avec la définition suivante : l'équation $X_i \leftarrow T_i$ et toutes les équations nécessaires aux variables de $T_i$ sont nécessaires au calcul de $X_i$. La **taille** du système $S = \{X_i \leftarrow T_i | i \in [1,n]\}$ est définie par $||S|| = \sum^n ||T_i||$ et un système est dit **uniforme** si pour tout $i, ||T_i|| = 1$ autrement dit si les $T_i$ ne comportent qu'un seul symbole de fonction.

## 2.2 Sémantique.

Si l'on interprète les termes comme au § 1.2 sur un domaine $\mathcal{B}$, à l'ensemble $\{T_i | i \in [1,n]\}$ se trouve naturellement associée une application de $\mathcal{B}^n$ dans $\mathcal{B}^n$ et donc un point fixe dans $\mathcal{B}^n$.
Nous noterons $Y(x_i)$ la composante de ce vecteur correspondant à la variable $X_i$.

Deux systèmes $S$ et $S'$ sont **équivalents** si, pour toute interprétation $Y(x_1) \equiv Y(x_1')$. La notion d'interprétation canonique se généralise trivialment et le lecteur pourra vérifier que le lemme 2 reste valide.
Un système $\{ X_i \leftarrow T_i \mid i \in [1,n] \}$ sera dit normal s'il n'est équivalent à aucun système $\{ X_j \leftarrow T_j \mid j \in [1,n] \}$ dans lequel les $T_j$ sont des sous-termes des $T_i$ et au moins l'un d'eux est un sous-terme propre.

Un sous-terme propre de T est un sous-terme de T différent de T et de $X_i$ pour tout $i \in [1,n]$.

Dans le cas d'un système comportant une seule équation, ce système est normal si l'équation est en forme normale.

## 2.3 Systèmes cancniques.

Etant donné un système $S = \{ X_i \leftarrow T_i \mid i \in [1,n] \}$ nous commençons par construire un système uniforme $\bar{S}$ qui lui est équivalent. Par exemple :

$$ S = \begin{cases} X_1 \leftarrow F(X_1, G(X_1, X_2)) \\ X_2 \leftarrow H(F(X_1, X_2)) \end{cases} \qquad (\text{variable principale } X_1) $$

$$ \bar{S} = \begin{cases} Y_1 \leftarrow F(Y_1, Y_3) \\ Y_2 \leftarrow H(Y_4) \\ Y_3 \leftarrow G(Y_1, Y_2) \\ Y_3 \leftarrow F(Y_1, Y_2) \end{cases} \qquad (\text{variable principale } Y_1) $$

Formellement, $\bar{S}$ est construit ainsi : appelons $\mathcal{J} = \{\tau_i \mid i \in [1,m]\}$ l'ensemble des sous-termes propres de S (dans le cas de nictre exemple : $\mathcal{J} = \{X_1, X_2, F(X_1, X_2), G(X_1, X_2)\}$. Le système $\bar{S}$ est construit sur les nouvelles variables $Y_i$, $i \in [1,m]$ associées ainsi aux éléments de $\mathcal{J}$ :

1) Si $\tau_i = X_1$ et si $X_1 \leftarrow F(\tau_1, \dots, \tau_{i-1}, \tau_{i+1}, \dots, \tau_{k-1}, \tau_k)$ est une équation de S, alors $Y_i \leftarrow F(Y_1, \dots, Y_{i-1}, Y_{i+1}, \dots, Y_{k-1}, Y_k)$ est une équation de $\bar{S}$.
2) Si $\tau_i = F(\tau_{i1}, \dots, \tau_{ik})$ alors $Y_i \Leftarrow F(Y_{i1}, \dots, Y_{ik})$ est une équation de $\bar{S}$.

3) La variable principale de $\bar{S}$ est la nouvelle variable $Y_l$ associée à $X_l$.

Nous laissons au lecteur le soin de démontrer les lemmes suivants (inspirés des travaux de W.P. de Roever [2]) :

**Lemme 8 :**

$$S \equiv \bar{S}$$

**Lemme 9 :**

Si $S$ est connexe, $\bar{S}$ est connexe. Si $S$ est normal, $\bar{S}$ est normal.

Pour un système uniforme $S = \{ X_i \Leftarrow F_i (X_i, \dots, X_i) \mid i \in I \}$ nous calculons la relation d'équivalence entre ses variables définie par $Y(X_i) \equiv Y(X_j)$ pour toute interprétation, que nous notons $X_i \equiv X_j$. Définissons inductivement une suite croissante de parties de $\Sigma \times \Sigma$, si $\Sigma = \{ X_i \mid i \in I \}$ :

$$1) D_0 = \{ (X_i, X_j) \in \Sigma \times \Sigma \mid F_i \neq F_j \}$$

$$2) D_{n+1} = D_n \cup \{ (X_i, X_j) \in \Sigma \times \Sigma \mid F_j = F_j \wedge \exists m \in [1, k(i)] \text{ tel que } (X_{i_m}, X_{j_m}) \in D_n \}$$

**Lemme 10 :**

i) Il existe un certain $l$ tel que $D_l = \bigcup_{n=0}^{\infty} D_n$

ii) $X_i \equiv X_j$ si et seulement si la paire $(X_i, X_j)$ n'appartient pas à $D_l$.
**Démonstration :**

L'existence de $l$ vient simplement du fait que $\exists$ est fini.
Montrons ii) par induction de Scott (cf. [5]) sur la formule $\Phi$ :

$$ \mathop{\wedge} X_i \equiv X_j \\ (X_i X_j) \notin D_1 $$

Tout d'abord $\mathop{\wedge}\Omega \equiv \Omega$. Par ailleurs, $\Phi$ implique :

$$ \Phi\{T_1/X_1, \dots, T_i/X_i, \dots, T_n/X_n\} $$

puisque $(X_i, X_j) \notin D_1$ entraine $T_i \equiv T_j$ ■

**Théorème 2 :**

L'équivalence de deux systèmes d'équations au point fixe est décidable.

**Démonstration :**

Le lemme 9 permet de se ramener au cas des systèmes unifor-
mes. Si $S = \{X_i \leftarrow T_i \mid i \in I\}$ et $S' = \{X'_i \leftarrow T'_i \mid i \in I'\}$, il est
toujours possible de s'assurer que $\exists = \{X_i \mid i \in I\}$ et $\exists' = \{X'_i \mid i \in I'\}$
sont disjoints et de considérer le système

$$ S'' = \{ X_i \leftarrow T_i \cup X'_j \leftarrow T'_j \mid i \in I, j \in I' \}. $$

L'algorithme du lemme 10 nous dira si $X_1 \equiv X_1'$ ■

**Corollaire 1 :**

L'équivalence $T \equiv T'$, où $T$ et $T'$ sont des termes quelcon-
ques sur les variables de deux systèmes $S$ et $S$ est décidable.
Démonstration :

On rajoute les équations $Z \Leftarrow T$ et $Z' \Leftarrow T'$ et on vérifie si
$Z \equiv Z'$. ■

Théorème 3 :

A tout système S on peut faire correspondre un système équivalent S' qui est normal, dont la taille est au plus la taille de S et qui comporte au plus le même nombre de variables.

Démonstration :

Soit T un sous-terme propre de S, $T \neq X_i$, tel que $X_i \equiv T$.
Cette égalité permet de "réduire" le système S :

- Si T est une variable $X_j$, on remplace partout $X_j$ par $X_i$
et on supprime de S l'équation de définition de $X_j$, $X_j \Leftarrow T_j$. Cette
transformation élimine une variable du système sans acroitre sa
taille. On aurait aussi bien pu éliminer $X_i$ que $X_j$ ; ce degré de
liberté sera exploité plus loin.

- Si T est un sous-terme de taille supérieure ou égale à 1, remplaçons toutes ses occurences dans S par $X_i$. La taille du système ne peut que diminuer et le système obtenu est équivalent au système initial.

Cette construction ne peut être itérée qu'un nombre fini de
fois puisqu'il ne peut y avoir qu'un nombre fini d'équivalences
$X_i \equiv T$. Par définition, le système auquel on aboutit est alors
normal. ■

Exemple :

$$
S_O = \begin{cases}
X \Leftarrow F(F(X,Y),Z) \\
Y \Leftarrow G(X,Z) \\
Z \Leftarrow G(X,G(X,Y))
\end{cases}
$$
On découvre que $Y \equiv Z$. $S_0$ est équivalent à $S_1$ :

$$S_1 = \begin{cases} X \leftarrow F(F(X,Y),Y) \\ Y \leftarrow G(X,Y) \end{cases}$$

Mais $X \equiv F(X,Y)$. $S_1$ est donc équivalent à $S_2$ :

$$S_2 = \begin{cases} X \leftarrow F(X,Y) \\ Y \leftarrow G(X,Y) \end{cases}$$

$S_2$ est normal.

La construction du théorème 3 peut être effectuée plus facilement sur des systèmes uniformes où les seuls sous-termes propres sont des variables.

Le lemme 10 définit une relation d'équivalence entre ces variables et le système normal associé à un système uniforme relation les classes d'équivalence.

### Notations :

Si $S$ est uniforme, nous notons $\tilde{S}$ le système normal qui lui correspond. A tout système $S$, on associe un système $\bar{S}$ uniforme équivalent, puis $\hat{S} = \tilde{S}$, système normal et uniforme.

### Lemme 11 :

Si $S$ et $S'$ sont deux systèmes connexes équivalents, alors $\hat{S} = \hat{S}'$.

### Démonstration :

Bien entendu, l'égalité entre $\hat{S}$ et $\hat{S}'$ s'entend à un renom-
mage près des variables. Montrons d'abord que pour toute varia-
ble $X_i$ de $\bar{S}$ il existe une variable $X'_i$ de $\bar{S}'$ telle que $X_i \equiv X'_j$,
par récurrence. Comme $S \equiv S'$ et $\bar{S} \equiv \bar{S}'$, nous avons bien $X_l \equiv X'_l$.

Si $X_i \equiv X'_j$ et $X_i \leftarrow F(X_i, \dots, X_i)$, $X'_i \leftarrow F(X'_j, \dots, X'_j)$, alors
$X_i = X_j, \dots, X_i = X_j$. Par suite, toutes les variables nécessai-
res à $X_i$ ont un correspondant dans $\bar{S}'$. Comme $\bar{S}$ est connexe, ce
sont toutes les variables de $\bar{S}$. Bien entendu la propriété symé-
trique est vraie :

$$
\forall j \in i \quad X_j' \equiv X_i
$$

Donc il existe une bijection entre les classes d'équiva-
lence des variables de S et S'. Comme par construction les varia-
bles de S et S' respectivement sont indépendantes, nous avons
S = S' à un changement de nom près des variables.■

Le lemme 11 justifie le nom de système canonique donné au
système $\hat{S}$.

Théorème 4 :

Dans l'ensemble des systèmes équivalents à un système donné
S, le système canonique S est de taille minimale.

Démonstration :

De la construction de $\bar{S}$ il est clair que $\| S \| \ge \| \bar{S} \|$.
Comme $\| \bar{S} \| \ge \| \tilde{S} \| = \| \hat{S} \|$ et $\hat{S} = \hat{S}'$ pour tout S' équivalent à S, $\hat{S}$
est de taille minimale. ■

Remarque :

Il peut exister plusieurs systèmes équivalents de taille
minimale, bien qu'un seul soit canonique, comme le montre l'exem-
ple suivant :
$$S_1 = \begin{cases} X \leftarrow F(X,Y) \\ Y \leftarrow G(Z) \\ Z \leftarrow H(X,Y) \end{cases}$$

$$S_2 = \begin{cases} X \leftarrow F(X,Y) \\ Y \leftarrow G(H(X,Y)) \end{cases}$$

Ici, $|| S_1 || = || S_2 ||$, $S_1 \equiv S_2$ et $S_1$ est canonique.

## 2.4 Minimisation du nombre d'équations.

On peut être interessé par la représentation d'un système qui en minimise non pas la taille mais le nombre d'équations au point fixe. L'exemple suivant montre qu'il n'y a pas toujours de système normal minimal (en ce sens) unique :

$$S_1 = \begin{cases} X \leftarrow F(X,Y) \\ Y \leftarrow G(H(X,Y)) \end{cases}$$

$$S_2 = \begin{cases} X' \leftarrow F(X',G(Y')) \\ Y' \leftarrow H(X',G(Y')) \end{cases}$$

$S_1$ et $S_2$ sont équivalents ($X \equiv X'$), normaux et comportent un nombre minimum d'équations. Mais $S_1$ et $S_2$ ne sont pas identiques à un changement près des noms des variables.

Nous montrons maintenant comment construire tous les systèmes normaux et tous les systèmes normaux minimaux.

### Définition :

Soit $S = \{ X_i \leftarrow T_i \mid i \in I \}$ et $C$ un sous-ensemble des variables de $S$, $C = \{ X_k \mid k \in K \}$, contenant $X_1$ et ayant la propriété suivante :

Pour $l \in I \setminus K$, $\exists T(l,C)$, terme ne faisant intervenir que les variables de $C$ tel que $X_1 \equiv T(l,C)^{\dagger}$.

On appelle *coupe de S*, $C(S)$ le système associé à un tel ensemble $C$ :

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

Et par $T(l,C)$ nous désignons dans la suite le plus petit terme permettant de définir $X_1$.
$$
C(S) = \{ X_i \leftarrow T_i' | X_i \in C \}
$$

dans lequel $T_i'$ est obtenu à partir de $T_i$ en remplaçant, pour tout
1 dans $I\setminus K$ $X_l$ par $T(l,C)$. A un $C$ comportant un nombre minimum de
variables correspond une **coupe minimale**.

Théorème 5 :

Les systèmes normaux équivalents à S sont les coupes de $\hat{S}$.

Démonstration :

a) Si $S'$ est une coupe de $\hat{S}$, $S' \equiv_S S$ et $S'$ est normal sinon $\hat{S}$ ne le serait pas.

b) Si $S'$ est normal et $S' \equiv_S S$, alors $\bar{S}'$ est normal donc
$$ \bar{S}' = \hat{S}' = \bar{S}. $$

Mais $S'$ est une coupe de $\hat{S}$ si et seulement si $\bar{S}' = \hat{S}$ et $S'$ est normal. ■

Corollaire 2 :

Les systèmes normaux minimaux équivalents à S sont les coupes minimales de S̄. Comme il n'y a qu'un nombre fini de coupes de S̄, on peut construire effectivement ces systèmes minimaux.

Exemple :

$$
S = \begin{cases} X \leftarrow F(F(X,Y),Y) \\ Y \leftarrow G(H(X,G(Z))) \\ Z \leftarrow H(X,G(Z)) \end{cases}
$$

$$
\hat{S} = \begin{cases} X \leftarrow F(X,Y) \\ Y \leftarrow G(Z) \\ Z \leftarrow H(X,Y) \end{cases}
$$
$$C_1 = \{ X, Y, Z \} \qquad C_1(\hat{S}) = \hat{S}$$

$$C_2 = \{ X, Y \} \qquad C_2(\hat{S}) = \begin{cases} X \leftarrow F(X,Y) \\ Y \leftarrow G(H(X,Y)) \end{cases}$$

$$C_3 = \{ X, Z \} \qquad C_3(\hat{S}) = \begin{cases} X \leftarrow F(X,G(Z)) \\ Z \leftarrow H(X,G(Z)) \end{cases}$$

On retrouve bien les deux formes normales minimales de S.

**Remarque :**

Si l'on part d'une seule équation récursive comme dans la première partie, on doit trouver une seule forme normale minimale, la forme normale de cette équation.

**Exemple :**

$$S = \{ X \leftarrow F(X, G(F(X, G(X, X)), X)) \}$$

$$\hat{S} = \begin{cases} X \leftarrow F(X, X') \\ X' \leftarrow G(X, X) \end{cases}$$

$$C = \{ X \} \qquad C(\hat{S}) = \{ X \leftarrow F(X, G(X, X)) \}.$$
## Conclusion :

Dans l'esprit des auteurs, l'interêt de ce travail ne réside pas tant dans les résultats de décidabilité obtenus (qui peuvent l'être à moindre frais) que dans les méthodes utilisées.

L'objectif est de reconstruire, sur les bases solides de la théorie de Scott [8], une théorie des schémas de programmes. Cette idée a été appliquée par Scott ([9]), et les techniques décrites ici sont appliquées aux programmes récursifs dans [1].

Enfin, il est possible de considérer les résultats obtenus comme des résultats de complétude de sous-théories de la logique LCF (Logic for Computable Functions) étudiée par Milner [5].

## Remerciement :

Une partie des résultats obtenus ici étaient connus de R. Milner, qui a collaboré à ce travail dans sa phase initiale.
REFERENCES BIBLIOGRAPHIQUES.

[1] Courcelle B. et J. Vuillemin (Rapport Laboria - à paraître).

[2] De Roever, W.P. Operational and Mathematical Semantics for first-order Recursive Program Schemas. (Private Communication).

[3] Kahn G. "A preliminary theory for parallel programs". (Rapport Laboria n° 6 - Janvier 1973).

[4] Lewis C.H., Rosen B.K. "Recursively defined data types". IEEE SWAT Symposium (Octobre 1973).

[5] Milner R. "Models of LCF". Stanford Computer Science Department Report. CS-332 (1973).

[6] Milner R., Weyrauch R. "Proving Compiler Correctness in a mechanized logic" in Machine Intelligence 7. Edinburgh University Press (1972).

[7] Nivat M. "Sur l'interprétation des schémas de programmes monodiques". Rapport Laboria n° 1 (Décembre 1972).

[8] Scott D. "Outline of a mathematical theory of computation". Oxford Mono. PRG-2. Oxford University (1970).

[9] Scott D. "The Lattice of Flowdiagrams" in Semantics of Algorithmic Languages. E. Engeler (Ed). Springer Lecture Notes (1970).

[10] Vuillemin J. "Proof techniques for recursive programs". Stanford Computer Science Department. Ph. D. Thesis (1973).