# Complétude d'un système formel pour prouver l'équivalence de certains schémas récursifs monadiques

Bruno Courcelle, Jean Vuillemin

► To cite this version:

Bruno Courcelle, Jean Vuillemin. Complétude d'un système formel pour prouver l'équivalence de certains schémas récursifs monadiques. [Rapport de recherche] IRIA-RR-063, IRIA. 1974, pp.19. hal-04715972

HAL Id: hal-04715972

https://inria.hal.science/hal-04715972v1

Submitted on 1 Oct 2024

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
RIA
laboria

laboratoire de recherche
en informatique
et automatique

Complétude
d'un système formel
pour prouver l'équivalence
de certains schémas
récursifs monadiques.

B.Courcelle,J.Vuillemin

19p

Institut de Recherche
d'Informatique
et d'Automatique

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

Rapport de Recherche n° 63

mars 1974
COMPLÉTUDE D'UN SYSTEME FORMEL POUR PROUVER
L'ÉQUIVALENCE DE CERTAINS SCHÉMAS RÉCURSIFS MONADIQUES

B. Courcelle, J. Vuillemin

IRIA - LABORIA

**Résumé :**

Dans [3] de Bakker et Scott définissent une classe de schémas de programmes et un système formel permettant de prouver certaines propriétés de ces schémas. Sous le nom de µ-calculus, ce système a été repris par de Bakker [2] qui a montré que le système est complet relativement aux formules exprimant l'équivalence des schémas de Ianov. Nous montrons ici la complétude de ce système pour les schémas récursifs monadiques définis par Ashcroft, Manna et Pnueli [1] (et écrits sans la fonction identité).

**Abstract :**

In [3] de Bakker and Scott introduce a formal system for proving properties of recursive program schemes. This formal system, the µ-calculus has been further studied and improved by de Bakker [2] who showed a completeness result for "regular procedures", which correspond roughly to the Ianov schemes [9]. This completeness result is extended here to recursive schemes without identity, as introduced and studied by Ashcroft, Manna, Pnueli [1].
# 1. Syntaxe et sémantique des schémas récursifs monadiques.

Désignons par S la classe des schémas récursifs monadiques définis par Ashcroft, Manna et Pnueli dans [1].

Un **schéma** S de S, ou **système de procédures récursives monadiques** est défini à l'aide d'un alphabet composé de :

1) Un ensemble $V = \{F_o, ..., F_m\}$ de **variables fonctionnelles**,

2) Un ensemble $F = \{f_1, ..., f_r\}$ de **fonctions de base monadiques**,

3) Un ensemble $P = \{p_1, ..., p_n\}$ de **prédicats monadiques**,

4) Le symbole $\Omega$.

Un **terme standard** est une expression de la forme $\Omega, f_i$ ou $f_i; F_{i1}; ... ; F_{ik}$.

Les **termes conditionnels** (t.c) sont les expressions finies construites inductivement selon les règles :

i) tout terme standard est un t.c,

ii) si $\tau_1$ et $\tau_2$ sont des t.c écrits sans le prédicat $p_i$ alors $(p_i \rightarrow \tau_1 | \tau_2)$ est un t.c. (écrit avec le prédicat $p_i$).

Un **schéma** S est alors un système de **définitions des variables fonctionnelles** :

$$ S \begin{cases} F_o \ <= \ T_o \\ . \\ . \\ . \\ F_m \ <= \ T_m \end{cases} $$

où pour tout $i$, $T_i$ est un t.c, définissant $F_i$.

En fait, en utilisant la notation post-fixée de de Bakker [2] plutôt que celle, préfixée, de Ashcroft, Manna et Pnueli [1] nous avons défini les schémas récursifs monadiques écrits sous forme standard sans la fonction identité de [1].

**Exemple** : $F <= (p_1 \rightarrow f_1 | (p_2 \rightarrow \Omega | f_2 ; F ; F))$ est un schéma de S qui serait écrit dans [1] :

$$ F(X) <= \underset{\text{si } p_1(X) \text{ alors } f_1(X) \text{ sinon } (\text{si } p_2(X) \text{ alors } F_\infty \text{ sinon } FF_{f_2(X)}).}{\text{F}} $$
Les symboles $\Omega$ et $F_\infty$ représentent tous deux la procédure divergente
$\Omega <= \Omega$. Par convention, on omet cette équation dans tout schéma.

Un **terme** (général) est une expression finie construite inductivement selon les règles :

i) $\Omega, f_i^1, F_j^1$ sont des termes,

ii) si $T_1$ et $T_2$ sont des termes et si $p_i$ est un prédicat, $T_1$ ; $T_2$ et $(p_i \rightarrow T_1|T_2)$ sont des termes.

Une _interprétation_ d'un schéma est la donnée $I = <D, p_i^I, f_i^I>$

i) d'un ensemble $D$ ou domaine de $I$,

ii) de prédicats totaux $p_i^I$ sur $D$ pour tout $p_i \in P$,

iii) de fonctions partielles $f_i^I : D \rightarrow D$ pour tout $f_i \in F$.

Le quadruple $<S,I,F_i,\xi>$ où $S$ est un schéma, $I$ une interprétation, $F_i$ une variable fonctionnelle et $\xi$ un élément de $D^I$ est alors un **programme récursif interprété**. Nous prendrons comme règle d'évaluation celle de la sémantique Algol. Le résultat du calcul, si celui-ci termine, est alors noté $Val(F_i,S,I)(\xi)$ ou plus simplement $F_i(\xi)$ lorsqu'il n'y a pas ambiguïté sur $S$ et $I$. De manière analogue on peut définir $Val(T,S,I)(\xi)$, $T$ étant un terme écrit à l'aide des variables de $S$.

Si $T$ et $T'$ sont deux termes écrits avec les variables d'un même schéma $S$, nous dirons que $T$ et $T'$ sont **équivalents par rapport à S** si pour toute interprétation $I, val(T,S,I) = val(T',S,I)$. Cette équivalence sera notée $S \models T \equiv T'$. La **réunion** de deux schémas $S$ et $S'$ dont les ensembles de variables fonctionnelles sont disjoints (c'est-à-dire la réunion de leurs ensembles d'équations) est un schéma qui est noté $SUS'$. Nous écrirons alors $S,S' \models T \equiv T'$ au lieu de $SUS' \models T \equiv T'$.

## Schémas équivalents

Luckham, Park et Paterson ont introduit dans [8] une classe particulière d'interprétations, les _interprétations libres_ définies par les conditions suivantes :

1) $D^I = F^*$ (dont le mot vide sera désigné par $\xi_0$),

2) pour tout $d \in D^I$, tout $f \in F$, $f^I(d) = df$.
**Proposition 1** : S ≡ Fᵢ ≡ Fⱼ ssi pour toute interprétation libre
Fᵢ(ξ₀) = Fⱼ(ξ₀). (Voir [8] et [5]).

Soit I une interprétation libre telle que Fᵢ(ξ₀) = m ∈ F*.
Soit n le nombre de prédicats du schéma et Σ = {0,1}ⁿ x F ; associons à m
le mot m̄ ∈ Σ*, m̄ = (η₀, fᵢ₀)(η₁, fᵢ₁) ... (ηₖ, fᵢₖ) où

$$
(1) m = f_{i_o} \dots f_{i_k}
$$

(2) η₀(resp. ηⱼ) représente la valeur des n prédicats sur
ξ₀(resp. fᵢ₀ ... fᵢⱼ-₁). Remarquons qu'au cours du calcul de Fᵢ(ξ₀), les
seuls tests effectués sont ceux dont on a "enregistré" la valeur sur le
mot m̄. Donc, pour toute interprétation libre I telle que m̄ = (η₀, fᵢ₀) ... (ηₖ, fᵢₖ)
satisfait la condition (2) ci-dessus, Fᵢ(ξ₀) = fᵢ₀ ... fᵢₖ.

Appelons *trace* de Fᵢ le langage sur Σ constitué des mots m associés
à toutes les interprétations libres. (Ce langage est noté Tr(Fᵢ)). Ceci
montre la

**Proposition 2** :

(i) $\underline{\mathrm{Tr}(F_i)} = \emptyset$ ssi $F_i \equiv \Omega$.

(ii) $\underline{\mathrm{Tr}(F_i)} = \mathrm{Tr}(F_j)$ ssi $F_i \equiv F_j$.

Nous venons donc de ramener l'équivalence de deux schémas à l'égalité
de deux langages que nous allons définir par des grammaires algébriques
("context-free" en anglais). Prenons V comme ensemble de non-terminaux.
A toute variable fonctionnelle F, à tout n-uple η de 0 et de 1 (représen-
tant les valeurs des n prédicats) est associé par la définition de F un
certain terme standard T(F,η) correspondant aux valeurs des prédicats
spécifiéespar η. Définissons la grammaire G en prenant comme productions :

$$
\begin{align*}
F &\rightarrow (\eta, f) \quad \text{ssi } T(F, \eta) = f \\
F &\rightarrow (\eta, f) \ F_j \dots F_k \quad \text{ssi } T(F, \eta) = f \ ; \ F_j \ ; \dots \ ; \ F_k
\end{align*}
$$

Il est clair que pour tout F ∈ V,L(G,F) = Tr(F) et que cette
grammaire est simple déterministe [4] . L'équivalence des schémas
récursifs monadiques se ramène donc à celle des langages simples
étudiée par Hopcroft et Korenjak [7] et Courcelle [4].
**Remarque :** On définit de même $\text{Tr}(F_j; F_{j_2}; \dots; F_{j_k})$. Et nous avons
$$ \text{Tr}(F_{j_1}; \dots; F_{j_k}) = \text{L}(G, F_{j_1} \dots F_{j_k}). $$ Il en résulte la

**Proposition 3 :** Pour tout schéma S, pour tous termes $T_1$ et $T_2$ on peut décider si $S \models T_1 \equiv T_2$.

**Démonstration :** Quitte à introduire de nouvelles variables, on peut ramener $S \models T_1 \equiv T_2$ à $S' \models F_{i_1}; \dots; F_{i_k} \equiv F_{j_1}; \dots; F_{j_k}$ et donc à $\text{Tr}(F_{i_1}; \dots; F_{i_k}) = \text{Tr}(F_{j_1}; \dots; F_{j_k})$. Cette dernière équivalence est décidable ([4] et [7]).

## 2 Schémas normaux

En utilisant essentiellement les méthodes de Courcelle [4] sur les grammaires simples, nous allons montrer que tout schéma S sur $V$ peut être réduit en un schéma équivalent dont l'ensemble des variables fonctionnelles est $V' \subseteq V$ et tel que $|V'|$ soit minimal.

**Définitions :**

1) Une variable fonctionnelle $F$ d'un schéma est dite **active** si elle est non-divergente (c'est-à-dire $F \not\models \Omega$) et si elle figure dans l'un au moins des membres de droite des équations de définition de S.

2) Un schéma S est dit **normal** si, pour toutes variables actives $F_{i_1}, \dots, F_{i_k}, \dots; F_{j_1}, \dots, F_{j_k}$ l'équivalence $F_{i_1}; \dots; F_{i_k} \equiv F_{j_1}; \dots; F_{j_k}$ implique $k=1$ et $i_1 = j_1, \dots, i_k = j_k$.

3) Nous étendrons (légèrement) la définition des schémas en autorisant une variable inactive $F$ à être définie par un terme de la forme $F_{i_1}; \dots; F_{i_k}$ (les $F_{i_j}$ étant des variables actives) ou $\Omega$.

**Proposition 4 :** Pour tout schéma S on peut construire un schéma $\overline{S}$ normal et équivalent à S.

**Notations :** Un schéma S étant donné, dont les variables fonctionnelles sont $F, F', F''_i$, etc, $m, m', m'_i$ désigneront des termes de la forme $F_{i_1}; \dots; F_{i_k}$.
**Lemme 1 :** Soit S un schéma, F, F', m et m' tous non divergents. Si S ⊢ F ; m ≡ F' ; m', on peut trouver m'' tel que l'une des trois conditions suivantes :

$$
(i) \mathcal{S} \vdash F \equiv F', m \equiv m'
$$

$$
(ii) S \vdash F \equiv F' ; m'', m'' ; m \equiv m'
$$

$$
(iii) S \vdash F' \equiv F ; m, m'' ; m' \equiv m.
$$

soit satisfaite.

**Démonstration** : En utilisant le langage trace ce lemme peut se reformuler en termes de grammaires simples déterministes. Il figure alors comme corollaire 1 bis dans [4] et nous renvoyons le lecteur à ce travail.

Introduisons pour tout $m \in V^*$ l'entier $\delta(m) = \inf\{|W|/W \in \text{Tr}(m)\}$. Il est clair alors que $\delta(m_1;m_2) = \delta(m_1) + \delta(m_2)$. En utilisant la grammaire algébrique engendrant $\text{Tr}(F_i)$ et les algorithmes classiques de théorie des langages, on peut calculer $\delta(F)$ pour tout $F \in V$. Remarquons que l'on peut prendre $\delta(\Omega) = \infty$. On a encore $\delta(\Omega;m) = \delta(\Omega) + \delta(m)$.

Démonstration de la Proposition 4.

1) Puisque l'on sait décider si une grammaire engendre un langage vide, on peut décider (grâce à la Proposition 2) si une variable est divergente. Le schéma S' obtenu en remplaçant par Ω tout terme standard d'une définition d'une variable de S où figure une variable divergente F et tout terme de la forme (p → Ω|Ω) par Ω est équivalent à S.

2) Si S' est normal, on prend $\bar{S} = S'$ et la preuve est finie.
Sinon, d'après le Lemme 1 il existe m et F tels que m ≠ F et m ≡ F. Remarquons
que F ne figure pas dans m, sinon m = m₀;F;m₁ et δ(m) = δ(m₀) + δ(F) + δ(m₁);
mais δ(F) = δ(m) donc δ(m₀) = δ(m₁) = 0. Donc m₀ et m₁ sont des "termes
vides" soit m = F contrairement à l'hypothèse.

On peut donc utiliser toute équation de la forme F ≡ m (et m ≠ F)
pour éliminer F, c'est-à-dire la rendre inactive : il suffit de remplacer
F par m dans tout membre de droite, définition d'une variable de S' et de
remplacer F <= T par F <= m. On obtient un schéma S<sub>1</sub> équivalent à S' ayant
une variable active de moins. Cette construction ne pourra être itérée
qu'un nombre fini de fois puisque l'on réduit à chaque pas le nombre de
variables actives et qu'un schéma doit comporter au moins une variable
active. D'autre part, cette construction est effective puisque l'on peut
savoir quelles équations $F \equiv m$ sont satisfaites : il y en a a priori un nombre fini car $F \equiv F_i \pmod{F_i}$ implique $\delta(F) = \delta(F_i) + \dots + \delta(F_i)$ et chacune d'elles est décidable.

**Exemple :**

$$ S \left\{ \begin{array}{l} F_o \triangleq (p \to f; F_2 | (q \to f|f; F_o; F_1)) \\ F_1 \triangleq (p \to \Omega | (q \to f; F_o|f; F_1; F_1)) \\ F_2 \triangleq (p \to f; F_2|f; F_2; F_2) \end{array} \right. $$

On remarque tout d'abord que $F_2 \equiv \Omega$. D'où $S'$ :

$$ S' \left\{ \begin{array}{l} F_o \triangleq (p \to \Omega | (q \to f|f; F_o; F_1)) \\ F_1 \triangleq (p \to \Omega | (q \to f; F_o|f; F_1; F_1)) \\ F_2 \triangleq \Omega \end{array} \right. $$

On s'aperçoit ensuite que $F_1 \equiv F_o;F_o$. D'où $\overline{S}$.

Le lecteur vérifiera que $\overline{S}$ est normal et équivalent à $S$ :

$$ \overline{S} \left\{ \begin{array}{l} F_o \triangleq (p \to \Omega | (q \to f|f; F_o; F_o; F_o)) \\ F_1 \triangleq F_o; F_o \\ F_2 \triangleq \Omega \end{array} \right. $$

**Remarques :**

1) Soient $S_1$ et $S_2$ deux schémas normaux équivalents à un schéma donné $S$. Ils sont **isomorphes** : il existe une bijection $\rho$ de $V_1$ sur $V_2$ telle que :

$$ 1) [F \triangleq \Omega] \in S_1 \quad \text{ssi } [\rho(F) \triangleq \Omega] \in S_2 $$

$$ 2) [F \triangleq m] \in S_1 \quad \text{ssi } [\rho(F) \triangleq m] \in S_2 $$

3) Si $F$ est une variable de $S_1$ définie par $F \triangleq T$ (et soit $\rho(T) = T\{\rho(F_i)/F_i\}^*$) alors $\rho(F)$ est une variable active de $S_2$ définie par $\rho(F) \triangleq T'$ et $\rho(T)$ et $T'$ sont des termes conditionnels qui ne diffèrent que par l'ordre des tests. Nous ne démontrerons pas ce fait car il ne nous servira pas pour la preuve de complétude.

<footnote>* $T\{\rho(F_i)/F_i\}$ est obtenu en substituant dans $T \rho(F_i)$ à $F_i$ pour tout $i$.</footnote>
2) Le système normal $\overline{S}$ est donc "unique" par rapport à un système donné, mais non par rapport à une variable particulière $F_0$: par exemple, soient

$$ S \quad \begin{cases} F_0 \le (p \to f | f ; F_1 ; F_2) \\ F_1 \le (q \to f ; F_1 | f) \\ F_2 \le (r \to f | f ; F_2) \end{cases} $$

et

$$ S' \quad \begin{cases} G_0 \le (p \to f | f ; G_1) \\ G_1 \le (q \to f ; G_1 | f ; G_2) \\ G_2 \le (r \to f | f ; G_2) \end{cases} $$

Il est facile de voir que S, $S' \vdash F_0 \equiv G_0$, $F_1 ; F_2 \equiv G_1$, $F_2 \equiv G_2$, et que chacun des schémas S et $S'$ est normal mais qu'ils ne sont pas isomorphes bien que $F_0 \equiv G_0$.

Il est montré dans [4] que l'on peut définir un schéma canonique par rapport à une variable fonctionnelle.

### 3. Description du µ-calculus.

Nous reprenons pour l'essentiel le µ-calculus étudié par de Bakker [2] en y apportant les modifications suivantes :

1) L'axiomatisation des conditionnelles tient compte de ce que dans toute interprétation les prédicats sont totaux, alors que dans [2] ils ne le sont pas.

2) Nous introduisons la **borne inférieure** de deux termes $\min(T_1, T_2)$.

3) Nous ne lions pas les variables par l'opérateur $\mu$. Les assertions sont de la forme $S, \Phi \vdash \Psi$, S étant un schéma définissant les variables fonctionnelles apparaissant dans $\Phi$ et $\Psi$. Cette astuce technique permet d'éviter l'élimination de la récursion multiple (ce problème est résolu pour le µ-calculus de de Bakker par exemple par Hitchcock et Park [6]).

Afin de rappeler son origine, nous continuerons à appeler ce système le µ-calculus bien qu'il ne comporte pas de µ-termes.
## Syntaxe.

Définissons la syntaxe en notation B.N.F :

<terme> ::= Ω | $f \in F$ | $F \in V$ | (p → <terme> | <terme>) | <terme>; <terme>|<terme>
min(<terme>, <terme>)

Remarquons que les termes introduits au §1 sont exactement les termes du u-calculus écrits sans min.

<formule atomique> ::= <terme> ⊑ <terme>

<formule> ::= <formule atomique> | <formule>, <formule>

<assertion> ::= <schéma>, <formule> ↦ <formule> | <formule> ↦ <formule>.

Nous utiliserons aussi quelques abréviations :

1) S,S', Φ ↦ Ψ pour SUS', Φ ↦ Ψ (Rappelons que SUS' est un schéma si $V(S) \cap V(S') = \emptyset$).

2) T ≡ T' pour T ⊑ T', T' ⊑ T

3) $\bigwedge_{o \le i \le m} \varphi_i$ pour $\varphi_0, \varphi_1, \dots, \varphi_m$, (les $\varphi_i$ étant des formules atomiques).

Une variable fonctionnelle qui n'appartient pas à $V(S)$ est dite libre dans l'assertion S, Φ ↦ Ψ. Sinon elle est liée.

## Sémantique :

Pour tout ensemble D, désignons par $[D \to D]$ l'ensemble des fonctions partielles $D \to D$. Il est ordonné par la relation de moindre définition ; $f \subseteq G$ ssi $\forall d \forall d' \in D f(d) = d' \Rightarrow g(d) = d'$.

Deux éléments quelconques f et g admettent une borne inférieure notée $min(f,g)$ et définie par $min(f,g)(d) = d'$ ssi $f(d) = g(d) = d'$.

La composition, $f ; g$ est définie par $(f;g)(d) = d'$ ssi il existe $d''$ tel que $d'' = f(d)$ et $d' = g(d)$.

L'opération de sélection est définie pour tout prédicat $p$ sur $D$ et tous $f,g$ par : $(p \to f|g)(d) = d'$ ssi $p(d)$ est vrai et $f(d) = d'$ ou bien $p(d)$ est faux et $g(d) = d'$.

Soit $T$ un terme dont les variables fonctionnelles sont $F_1, \dots, F_m$. Au couple $<I, \vec{\phi}>$ constitué d'une interprétation $I = <D^I, p^I, f^I>$ et d'un m-uple $\vec{\phi} = <\phi_1, \dots, \phi_m>$ d'éléments de $[D^I \to D^I]$, on peut associer l'interprétation $I(T,I, \vec{\phi})$ de $T$ ; c'est un élément de $[D^I \to D^I]$ défini par :
1) $I(\Omega, I, \phi) = \Omega_D$, la fonction définie pour aucun $d \in D^I$,

2) $I(f, I, \phi) = f^I$,

3) $I(F_i, I, \phi) = \phi_i$,

4) $I(T; T', I, \phi) = I(T, I, \phi) ; I(T', I, \phi)$,

5) $I((p \to T|T'), I, \phi) = (p^I \to I(T, I, \phi) | I(T', I, \phi))$

6) $I(\min(T, T'), I, \phi) = \min(I(T, I, \phi), I(T', I, \phi)).$

L'interprétation d'une formule atomique $T_1 \subseteq T_2$ est alors _vrai_ si $I(T_1, I, \phi) \subseteq I(T_2, I, \phi)$ et _faux_ sinon.

Une *formule* est vraie si et seulement si toute formule atomique qui la constitue est vraie. On note encore $I(\phi, I, \phi) \in \{\text{vrai}, \text{faux}\}$ l'interprétation d'une formule.

Soit $A = S, \Phi \vdash \Psi$ une assertion dont les variables libres sont $F_1, \dots, F_1$ et les variables liées (c'est-à-dire les variables fonctionnelles de $S$) sont $F_{1+1}, \dots, F_m$. Alors

$I(A, I, \langle \varphi_1, \dots, \varphi_l \rangle) = I(\Phi \Rightarrow \Psi, I, \langle \varphi_1, \dots, \varphi_l, \varphi_{l+1}, \dots, \varphi_m \rangle)$ où pour $1+l \le i \le m$, $\varphi_i = \text{val}(S, F_i, I)$.

L'assertion A est _valide_ si elle est vraie pour tout $\langle I, \langle \varphi_1, \dots, \varphi_l \rangle \rangle$.

Exemples :

1) $\vdash (p \to f|(q \to f;F|G)) \equiv (q \to (p \to f|f;F)|(p \to f|G))$ est une assertion valide.

2) Si $S \vdash F_0 \equiv F_1;F_2$ alors $S \vdash F_0 \equiv F_1;F_2$ est une assertion valide.
Nous noterons $S, \Phi \vdash \Psi$ les assertions valides. Cette notation est cohérente avec celle introduite au §1 pour exprimer l'équivalence des schémas.

Nous allons maintenant _axiomatiser_ certains ensembles d'assertions valides.

**Notation** : Etant donné un terme $T$ écrit sur les variables fonctionnelles $F_0, \dots, F_m$ et $T_i$ des termes quelconques pour $0 \le i \le m$, $T\{T_i/F_i\}$ désigne le terme obtenu en substituant $T_i$ à chaque occurrence de $F_i$ pour tout $0 \le i \le m$.
Dans la liste suivante, de schémas d'axiomes et de règles d'inférence S, S' désignent des schémas (définis au §1), Φ, ψ, ... des formules ; les assertions écrites sont toujours supposées bien formées.

### Axiomes et règles "purement logiques".

$$AO: \quad \Phi \vdash \Phi$$

$$R1: \quad \frac{S, \Phi \vdash \psi, \psi'}{S, S', \Phi, \Phi' \vdash \psi} \qquad (\text{Affaiblissement})$$

$$R2: \quad \frac{S, \Phi \vdash \psi \quad S', \Phi' \vdash \psi'}{S, S', \Phi, \Phi' \vdash \psi, \psi'} \qquad (\text{Conjonction})$$

$$R3: \quad \frac{S, \Phi \vdash \psi \quad S, \psi \vdash \chi}{S, \Phi \vdash \chi} \qquad (\text{Modus Ponens})$$

$$R4: \quad \frac{S, \Phi \vdash \psi}{S', \Phi' \vdash \psi'} \qquad \begin{array}{l} \text{si la deuxième assertion se déduit de la première} \\ \text{par un changement de nom des variables liées.} \end{array}$$

### Axiomes et règles "non logiques" (c'est-à-dire exprimant les propriétés da ⊑ , ; etc).

1) Axiomes relatifs à ⊑

$$A1: \quad \vdash T \subseteq T$$

$$A2: \quad T_1 \subseteq T_2, \ T_2 \subseteq T_3 \quad \vdash T_1 \subseteq T_3$$

$$A3: \quad \vdash \Omega \subseteq T$$

2) Axiomes relatifs à ⊂ ;

$$A4: \quad T_1 \subseteq T_2, \ T_3 \subseteq T_4 \quad \vdash T_1 ; T_2 \subseteq T_3 ; T_4$$

$$A5: \quad \vdash T_1 ; (T_2 ; T_3) \equiv (T_1 ; T_2) ; T_3$$

$$A6: \quad \vdash T ; \Omega \equiv \Omega ; T \equiv \Omega$$

3) Axiomes relatifs à min

$$A7: \quad T_1 \subseteq T_2, \ T_1 \subseteq T_3 \quad \vdash T_1 \subseteq \min(T_2, T_3)$$

$$A8: \quad \vdash \min(T_1, T_2) \equiv \min(T_2, T_1) \subseteq T_1$$
### 4) Axiomes relatifs aux conditionnelles

$$A9 : \vdash (p \rightarrow T|T) \equiv T$$

$$A10 : \vdash (p \rightarrow (p \rightarrow T_1|T_2)|T_3) \equiv (p \rightarrow T_1|T_3)$$

$$A11 : \vdash (q \rightarrow (p \rightarrow T_1|T_2)|T_3) \equiv (p \rightarrow (q \rightarrow T_1|T_3)|(q \rightarrow T_2|T_3))$$

ainsi que les axiomes analogues obtenus en échangeant dans A10 et A11 $T_3$ et $(p \rightarrow T_1|T_2)$.

$$A12 : \vdash (p \rightarrow T_1|T_2) ; T_3 \equiv (p \rightarrow T_1 ; T_3|T_2 ; T_3)$$

### 5) Axiome du point fixe

A13 : $S \vdash \bigwedge_{0 \le i \le m} F_i \equiv T_i$ ($\{F_o, \dots, F_m\}$ étant l'ensemble des variables du schéma S et pour tout $i, T_i$ est la définition de $F_i$).

### 6) Règle "d'induction de Scott"

R5 : Soit S un schéma $\prec <F_i \leq T_i / o \leq i \leq m>$ . Alors,

$$S', \Phi \vdash \Psi \{\Omega/F_i\} \qquad S', \Phi, \Psi \vdash \Psi \{T_i/F_i\}$$

$$S, S', \Phi \vdash \Psi$$

à condition que les $F_i$ soient libres dans $S'$, $\Phi \vdash \Psi$.

De ce même système d'axiomes et de règles, on peut dériver la règle suivante :

R6 Avec les mêmes notations que plus haut,

$$S', \Phi \vdash \bigwedge_{0 \le j \le m} T_j \{T'_i / F_i\} \subseteq T'_j$$

$$S, S', \Phi \vdash \bigwedge_{0 \le j \le m} F_j \subseteq T'_j$$

Une **preuve** est une suite d'assertions obtenues chacune par substitution de termes et de schémas dans un axiome ou par application d'une règle d'inférence à des assertions précédentes de la suite. Un **théorème** est la dernière assertion d'une preuve. Nous écrivons $S, \Phi \vdash * \Psi$ comme abréviation de : "$S, \Phi \vdash \Psi$ est un théorème".

**Théorème 1** : Le μ-calculus est valide. Autrement dit, si $S, \Phi \vdash * \Psi$ alors $S, \Phi \vdash \Psi$.

Le lecteur le démontrera ou consultera [2].
Si A est un ensemble d'assertions, nous disons que le µ-calculus est _A-complet_ si, pour toute assertion S, $\phi \vdash \Psi$ de A, $S, \phi \models \Psi$ équivaut à $S, \phi^* \vdash \Psi$. Il est _A-incomplet_ sinon.

Soit $A_0$ l'ensemble des assertions écrites sans _min_; $A_1$ l'ensemble des assertions de la forme $S \vdash T \equiv T'$ ; $A_2 = A_0 \cap A_1$ ; $A_3$ est l'ensemble des assertions de la forme $S \vdash T \subseteq T'$ écrites sans _min_.

**Proposition 5** : Le µ-calculus est $A_0$-incomplet et $A_1$-incomplet.

**Démonstration** : Ce résultat pour $A_0$ est classique ([3]).

Il suffit de démontrer que le µ-calculus est B-incomplet où
$B = \{S \vdash \underline{min}(T,T') \equiv \Omega\}$ pour démontrer la deuxième partie de la proposition.
Or $S \models \underline{min}(T,T') \equiv \Omega$ ssi $\mathrm{Tr}(T) \cap \mathrm{Tr}(T') = \emptyset$. $\mathrm{Tr}(T)$ et $\mathrm{Tr}(T')$ sont des
langages simples, et en utilisant les techniques classiques, on peut
associer à tout problème de correspondance de Post deux termes T et T'
tels que $\mathrm{Tr}(T) \cap \mathrm{Tr}(T') \neq \emptyset$ ssi le problème a une solution. Autrement
dit $\{S \vdash \underline{min}(T,T') \equiv \Omega\}$ n'est pas récursif. On montre facilement que
son complémentaire est récursivement énumérable. Puisque l'ensemble des
théorèmes de B est récursivement énumérable, il ne peut coïncider avec
$\{S \vdash \underline{min}(T,T') \equiv \Omega\}$ sinon ce dernier ensemble serait récursif.

**Question** : Le µ-calculus est-il $A_3$-complet ? S'il l'était il en résulterait que l'inclusion de deux langages simples est décidable et ce dernier problème est ouvert.

Nous démontrons au §4 le résultat principal de cet article :

**Théorème 2** : Le µ-calculus est $A_2$-complet.

4. **Compléture du µ-calculus pour les formules exprimant l'équivalence des schémas.**

Rappelons (§2) qu'à tout schéma S sur $\{F_o, ..., F_m\}$ nous savons
associer un schéma S' sur $\{F'_o, ..., F'_m\}$, normal, tel que pour tout i
$F'_i \equiv F_i$.

On peut supposer que la numérotation des variables est telle que
{$F'_o, ..., F'_1$} est l'ensemble des variables actives et que S' est de
la forme :
<figure><img src="image_2.png" /></figure>

**Proposition 6** : Avec ces notations, $S,S' \stackrel{*}{\leftarrow} \bigwedge_{0 \le i \le m} F_i \equiv F'_i$.

**Remarque préliminaire** : Soient $T$ et $T'$ deux termes conditionnels sur $P \cup F \cup \{F'_0, \dots, F'_1\}$ tels que $S' \models T \equiv T'$. Alors $S' \stackrel{*}{\leftarrow} T \equiv T'$. En effet, pour tout $\eta \in \{0,1\}^n$ $S' \models T(\eta) \equiv T'(\eta)$. Or $T(\eta)$ et $T'(\eta) \in F'\{F'_0, \dots, F'_1\}^*$ et donc, puisque $S'$ est normal $T(\eta) = T'(\eta)$ donc $\stackrel{*}{\models} T(\eta) \equiv T'(\eta)$. (La notion $T(\eta)$ a été introduite à la fin du §1).

Il reste à montrer que deux termes conditionnels ne différant que par l'ordre des tests peuvent être prouvés équivalents dans le µ calculus. Or on peut (par les axiomes A10 et A11) mettre les deux termes sous une forme commune testant tous les prédicats dans l'ordre $p_1, p_2, \dots, p_n$. Par exemple, on transformera $T_1 = (p_2 \rightarrow (p_1 \rightarrow A|B)|C)$ en $T_2 = (p_1 \rightarrow (p_2 \rightarrow A|C)|(p_2 \rightarrow B|C))$ il est clair que $\stackrel{*}{\models} T_1 \equiv T_2$.

Autrement dit, le fait que $S'$ soit normal implique que deux termes sur $\{F'_0, \dots, F'_1\}$ équivalents sont suffisamment semblables pour que l'on puisse prouver leur équivalence.

**Démonstration:**

$$ \text{lère Partie : } S,S' \stackrel{*}{\leftarrow} \bigwedge_{0 \le i \le m} F_i \equiv F'_i $$

Remarquons tout d'abord que $S' \stackrel{*}{\leftarrow} F'_i \equiv m'_i$ et que
$$ S' \stackrel{*}{\leftarrow} \bigwedge_{k+1 \le i \le m} F'_i \equiv \Omega \text{ (Axiome du point fixe A13).} $$

Pour tout $i$ soit $T''_i$ le résultat de la substitution dans $T_i$ de $F'_j$ à $F_j$ pour $0 \le j \le 1$, de $m'_j$ à $F_j$ pour $1 \le j \le k$ et de $\Omega$ à $F_j$ pour $k+1 \le j \le m$.

Afin d'utiliser la règle R6 qui conduit à la conclusion souhaitée, il suffit de montrer que :
a) $S' \stackrel{*}{\vdash} T''_i \equiv F'_i$ pour $0 \le i \le 1$,

b) $S' \stackrel{*}{\vdash} T''_i \equiv m'_i$ pour $1+1 \le i \le k$,

c) $S' \stackrel{*}{\vdash} T''_i \equiv \Omega$ pour $k+1 \le i \le m$.

a) L'application de A13 fournit $S' \vdash F'_i \equiv T'_i$. Soit d'autre part $T'''_i$ le terme obtenu en remplaçant dans $T''_i$ chaque $u_1 ; \Omega$ ; $u_2$ par $\Omega$. Il est clair alors que $\stackrel{*}{\vdash} T''_i \equiv T'''_i$. D'autre part $S' \vdash T'''_i \equiv T'_i$ parce que $S$ et $S'$ sont équivalents donc $S' \stackrel{*}{\vdash} T'''_i \equiv T'_i$ par la remarque préliminaire.

b) La preuve est semblable : posons $m'_i = F'_i r'_i ; q'_i$. Alors $S' \vdash m'_i \equiv T'_i r'_i ; q'_i$. En utilisant A12 on met ce dernier terme sous forme d'un terme conditionnel et on achève la preuve comme en a) avec la remarque préliminaire.

c) Si $F_i \equiv \Omega$, alors pour tout $\eta \in \{0,1\}^n$, $T(F_i, \eta)$ est de la forme $u_1 ; F_j ; u_2$ où $F_j \equiv \Omega$. Il en résulte que $S' \stackrel{*}{\vdash} T''_i \equiv \Omega$ par application de A6 puis A9.

$$ \underline{2ème Partie} : S,S' \stackrel{*}{\vdash} \bigwedge_{0 \le i \le m} F'_i \subseteq F_i. $$

Nous abordons la partie difficile de la démonstration, qui recquiert, croyons nous, l'utilisation de *min*. Posons pour $1+1 \le i \le k$ : $m_i = F'_i r'_i ; q'_i$, $q'_i$ étant éventuellement réduit au mot vide.

$$ \text{Tout revient à montrer que } S,S' \stackrel{*}{\vdash} \bigwedge_{0 \le i \le 1} F'_i \subseteq F_i, \bigwedge_{1+1 \le i \le k} F'_i \subseteq F_i. $$

Introduisons les notations suivantes : pour tout $m' \in \{F'_o, ..., F'_l\}^*$ soit $\Sigma(m') = \{m \in \{F'_o, ..., F'_m\}^* / S,S' \vdash m \equiv m'\}$. Cet ensemble est fini et calculable. Soit alors $\sigma(m') = \min(\Sigma(m'))$. (Il est clair que $\min(\{A,B,C, ... \}) = \min(A,\min(B, ...))$).

Nous allons appliquer la règle R5 à l'assertion $S,S' \vdash \Phi(X_o, ..., X_l)$ où $\Phi$ est la formule $\bigwedge_{0 \le i \le 1} X_i \subseteq F_i, \bigwedge_{1+1 \le i \le k} X_i \supseteq F_i$. Il est clair que $S,S' \stackrel{*}{\vdash} \Phi(\Omega, \dots, \Omega)$ (par A3 et A6).

Il reste à montrer que $S,S',\Phi \stackrel{*}{\vdash} \Phi\{T'_i(X_o, ..., X_l)/X_i\}$. Or (par A13) $S \vdash F_i \equiv T_i$. Il suffit donc de prouver que $S,S', \Phi \stackrel{*}{\vdash} \bigwedge_{0 \le i \le 1} T'_i(X_o, ..., X_l) \subseteq T_i, \bigwedge_{1+1 \le i \le k} T'_i(X_o, ..., X_l) ; \sigma(q'_i) \subseteq T_i$.
Tout revient, après avoir utilisé A11 et A12, à prouver un nombre fini d'assertions S, S', $\Phi \vdash X_i$ ; ... ; $X_i$ ; $\sigma(m') \subseteq m$ pour lesquelles S, S' $\vdash F_i$ ; ... ; $F_i$ ; $m' \equiv m$. Chacune d'elles est un théorème du μ-calculus comme le montre le :

**Lemme 2** : Si $S \vdash F_j$ ; ... ; $F_j \equiv F_i$ ; ... ; $F_i$ et si pour tout $1 \le i \le r$ : $o \le j_1 \le 1$ (c'est-à-dire $F_j$ est une variable active du système normal S') alors (avec les notations et définitions de la preuve) : $S, S', \Phi \stackrel{*}{\vdash} X_j$ ; ... ; $X_j$ ; $\sigma(F_j ; ... ; F_j) \subseteq F_i$ ; ... ; $F_i$ si $1 \le s \le r$.

**Démonstration** : Nous raisonnons par induction sur $\delta(F_i_1 ; ... ; F_i_k)$ sans traiter le cas $\delta(F_i_1 ; ... ; F_i_k) = 1$ qui est prouvé avec le cas général.

Il résulte des propriétés des variables $F_i$ pour $0 \le i \le 1$ (voir §2) que pour un certain $t$, $1 \le t \le r$, S $\vdash F_{i_1} \equiv F_{j_1}$ ; ... ; $F_{j_t}$.

Distinguons deux cas :

Le cas : $t \le s$ : montrons d'abord que

(1) S, S' $\Phi \vdash X_j$ ; ... ; $X_j \subseteq F_i$ est un théorème. Or, pour tout m équivalent à $F_{j_2}$ ; ... ; $F_{j_t}$, S, S', $\Phi \stackrel{*}{\vdash} X_{j_2}$ ; ... ; $X_{j_t} \subseteq m$ donc par application répétée de A7 et par définition de $\sigma$ :

(2) S, S', $\Phi \stackrel{*}{\vdash} X_{j_2}$ ; ... ; $X_{j_t} \subseteq \sigma(F_{j_2} ; ... ; F_{j_t})$. Comme d'autre part la formule $X_{j_1}$ ; $\sigma(F_{j_2} ; ... ; F_{j_t}) \subseteq F_{i_1}$ figure dans $\Phi$, en utilisant AO et R1 :

S, S', $\Phi \stackrel{*}{\vdash} X_{j_1}$ ; $\sigma(F_{j_2} ; ... ; F_{j_t}) \subseteq F_{i_1}$ et avec (2), A2 et A4, (1) est bien un théorème.

Toujours par hypothèse d'induction,

(3) S, S', $\Phi \stackrel{*}{\vdash} X_{j_{t+1}}$ ; ... ; $X_{j_s}$ ; $\sigma(F_{j_{s+1}} ; ... ; F_{j_r}) \subseteq F_{i_2}$ ; ... ; $F_{i_k}$.

Donc A4 appliqué à (1) et (3) fournit le résultat.
### 2ème cas : s < t

Remarquons tout d'abord que $\Sigma(m_1m_2) \supseteq \Sigma(m_1) \Sigma(m_2)$ pour tous $m_1, m_2$. Donc (1) : $\sigma(m_1m_2) \le \sigma(m_1) \sigma(m_2)$. L'assertion (2) :

$S, S', \Phi \vdash X_j ; \dots ; X_j ; \sigma(F_{j+s+1} ; \dots ; F_j) \subseteq F_i$ est un théorème (par hypothèse d'induction).

D'autre part, $F_{i_2} ; \dots ; F_{i_k} \in \Sigma(F_{j_t+1} ; \dots ; F_j)$ et donc (3) $S, S', \Phi \stackrel{*}{\vdash} \sigma(F_{j_{t+1}} ; \dots ; F_j) \subseteq F_{i_2} ; \dots ; F_{i_k}$.

En utilisant (1), (2) et (3) ainsi que A2 et A4, on montre que $S, S', \Phi \vdash X_j ; \dots ; X_j ; \sigma(F_{j+s+1}) ; \dots ; F_j) \subseteq F_i, \dots, F_i_k$ est un théorème.

Les conditions d'application de la règle R6 étant réunies, on obtient $S, S' \stackrel{*}{\vdash} \bigwedge_{0 \le i \le 1} F'_i \subseteq F_i, \bigwedge_{1+l \le i \le k} F'_r_i ; \sigma(q'_i) \subseteq F_i$.

Il en résulte avec les résultats de la première partie que $S, S' \stackrel{*}{\vdash} \bigwedge_{0 \le i \le 1} F'_i \equiv F_i$. En procédant par ordre de $\delta$ croissants on peut montrer que pour tout $1+l \le i \le k$, $S, S' \stackrel{*}{\vdash} F'_i \equiv F_i$.

Il suffit en fait que $S, S' \stackrel{*}{\vdash} F_i \equiv m'_i$. Or si $\sigma(q'_i)$ est réduit au terme vide, $F'_{r_i} = F_i$ et $S, S' \stackrel{*}{\vdash} F'_i \equiv F_i$. Sinon, par hypothèse d'induction, pour tout $m \in \Sigma(q'_i)$, $S, S' \stackrel{*}{\vdash} m \equiv q'_i$ et donc $S, S' \stackrel{*}{\vdash} \sigma(q'_i) \equiv q'_i$. Il en résulte que $S, S' \stackrel{*}{\vdash} F'_{r_i} ; q'_i \equiv F_i$. CQFD.

**Théorème** : Soient S un schéma, T et T' des termes sans min écrits avec les variables fonctionnelles de S. Alors $S \vdash T \equiv T'$ si et seulement si $S \stackrel{*}{\vdash} T \equiv T'$.

**Démonstration** : Quitte à introduire de nouvelles variables, on peut faire en sorte que $S_1 \stackrel{*}{\vdash} T \equiv F_i ; \dots ; F_{i_k} \text{ et } S_1 \stackrel{*}{\vdash} T' \equiv F_j ; \dots ; F_{j_1}, S_1$ étant un schéma "contenant" S.

Il reste donc à montrer que $S_1 \stackrel{*}{\vdash} F_i ; \dots ; F_{i_k} \equiv F_j ; \dots ; F_{j_1}$ sachant que cette assertion est valide. Soit $S'_i$ le système normal associé à $S_i$. D'après la proposition 6 $S_i, S'_i \stackrel{*}{\vdash} F_i \equiv m'_i, \dots F_j \equiv m_j$ où les $m_i$ sont des mots sur les variables actives de $S_i$. D'après les propriétés des systèmes normaux, $m_i ; m_{i_2} ; \dots ; m_{i_k} = m_j ; \dots ; m_{j_1}$ donc
* mᵢ₁; mᵢ₂ ... mᵢₖ ≡ mⱼ₁; ... ; mⱼₙ et S₁,S₁* Fᵢ₁;...; Fᵢₖ ≡ Fⱼ₁;...;Fⱼₙ
qui restait à prouver en résulte. CQFD.

**Conclusion** : Ce travail peut être prolongé dans plusieurs directions :

1) Par souci de simplicité, nous avons choisi de nous limiter aux interprétations $\mathcal{T}$ où les prédicats $p_i^I$ sont totaux. Les résultats auraient été les mêmes pour la notion d'équivalence attachée à la classe des interprétations où les prédicats sont partiellement définis. Nous aurions alors défini la trace sur l'alphabet $\{0,1,\perp\}^n \times \mathcal{F}$, un prédicat $p_i$ pouvant être sur une valeur de $D^I$ _faux_, _vrai_ ou _non-testé_ au cours d'un calcul qui se termine. Les axiomes A9, A11 auraient alors été remplacés par les axiomes suivants (voir [2]):

$$A9 \quad \vdash (p \to T|T) \subseteq T$$

$$A11 \quad \vdash (p \to (q \to T_1|T_2) | (q \to T_3|T_4)) \equiv (q \to (p \to T_1|T_3) | (p \to T_2|T_4))$$

2) Définir $S$ comme étant exactement la classe des schémas récursifs monadiques de [1] et prouver formellement que le schéma standard associé à un schéma donné lui est équivalent.

3) Plus difficile, sans doute est de décider si _min_ est indispensable à la preuve de complétude.

4) Il faudrait encore étendre la preuve de complétude aux schémas libres de [1], ce que nous n'avons pas réussi à faire faute de savoir définir un schéma normal équivalent à un schéma libre donné. Nous pensons que c'est possible car les traces des schémas libres sont des langages "très proches" des langages simples.
Références :

[1] E. Ashcroft, Z. Manna, A. Pnueli "Decidable Properties of Monadic Functional Schemes " in Theory of Machines and Computations (Eds: Kohavi and Paz), New York 1971, 3-17.

[2] J.W. de Bakker "Recursive Procedures", Mathematical Center Tract n°24, Amsterdam 1971.

[3] J.W. de Bakker, D. Scott "A Theory of Programs", 1969, Unpublished.

[4] B. Courcelle "Grammaires canoniques des Langages simples", Revue de l'Association pour l'Informatique et la Recherche Opérationnelle, 1974, n°1.

[5] F.G. Cousineau, J.M. Rifflet "Schémas de Programme : Problèmes d'Equivalence et Complexité", Thèse de 3ème cycle, Paris 1974.

[6] P. Hitchcok, D. Park "Induction Rules and Termination Proofs" Automata, Languages and Programming pp 225-252, 1973. (Colloque IRIA 1972).

[7] J.E. Hopcroft, A.J. Korenjak "Simple Deterministic Languages", IEEE 7th Annual Symposium on Switching and Automata Theory pp 36-46.

[8] D. Luckham, D. Park, M. Paterson "On Formalized Computer Programs" J.C.S.S. vol 4, pp 220-249.