Complétude de systèmes de réécriture d’ordre supérieur

Jacek Chrza_{}szcz

Résumé

Ce travail étend la notion de complétude de systèmes de réécriture sur les systèmes d’ordre supérieur. Comme dans le premier ordre, cette notion est reliée à la complétude de définitions de fonctions. Une procédure de vérification de cette propriété est également présentée. Deux disciplines classiques de types sont étudiées : types simples et types polymorphes. Pour les types simples, plusieurs approches sur le traitement des arguments fonctionnels sont données.

Mémoire de stage de D.E.A. en informatique

Laboratoire de Recherche en Informatique Université de Paris-Sud

Directeur de stage : Jean-Pierre Jouannaud

Orsay, 13 janvier 1998

Complétude de systèmes de réécriture d’ordre supérieur

Jacek Chrza_{}szcz

13 janvier 1998

1 Introduction

La réécriture a des multiples applications dans l’informatique. Par rapport aux équations, utilisées traditionnellement en mathématiques, les règles de réécriture, qui sont tout simplement des équations orientées, sont beaucoup mieux adaptées au calcul symbolique. Elles éliminent une source potentielle de non-déterminisme — le choix d’une direction. L’autre source, le choix d’une sous-expression à réécrire, peut être aussi négligée si la relation de réécriture est confluente. Lorsqu’elle possède la propriété de terminaison, chaque réduction d’un terme donné aboutit à l’issue d’un nombre fini d’étapes à un unique terme irréductible, dit forme normale. Si nous traitons les termes en forme normale comme des valeurs et tous les termes comme des expressions algébriques, notre système de réécriture nous donne un moyen automatique de calculer la valeur d’une expression arbitraire. Si nous voulons nous concentrer sur l’aspect calculatoire de la réécriture, nous pouvons considérer une règle de réécriture, dont le coté gauche a un symbole f en tête, comme un cas de définition par filtrage de la fonction f et, en général, la réécriture comme un moyen d’exécution de programmes fonctionnels.

Étant donné un système de réécriture, nous pouvons en extraire l’ensemble de symboles qui n’apparaissent en tête d’aucun coté gauche. Ces symboles vont être ensuite appelés constructeurs et tous les autres — symboles définis. Remarquons qu’un terme construit uniquement à partir de constructeurs est forcément irréductible, nous avons ainsi trouvé un ensemble des valeurs.

Complétude

Un système de réécriture convergent (qui est confluent et qui termine) est appelé complet si chaque terme sans variables se réécrit en un terme constructeur. Ce fait est essentiel pour faire des preuves inductives de différentes propriétés sémantiques des objets décrits par notre système. Dans le cas d’un système complet, il suffit de démontrer la propriété donnée pour des termes constructeurs, parce que la valeur sémantique de chaque autre terme correspond à la valeur d’un terme constructeur.

La propriété globale de complétude du système est équivalente à une autre propriété plus locale et plus facile à tester automatiquement. Si les définitions de toutes les fonctions du système sont localement complètes, alors le système lui-même est complet. Dans le cadre de la réécriture, la complétude locale de la fonction f donnée signifie que tout terme qui est une application de f à des valeurs est réductible. Cette dernière propriété est appelée aussi la réductibilité close, mais on va utiliser le nom de << complétude locale >> pour la distinguer de la complétude globale du système.

Pour tester la complétude de fonctions définies par des règles de réécriture (et aussi, automatiquement, la complétude globale du système de réécriture) Kounalis [10] a conçu une technique d’arbres de motifs. Cette technique a été ensuite adaptées par Bouhoula dans [1] pour des règles conditionnelles dans le cadre de son système de prototypage de spécifications parametrées SPIKE et par Bouhoula et Jouannaud dans [2] pour un langage de clauses de Horn avec égalité et appartenance, implanté sous le nom de MAUDE [13].

Systèmes de réécriture d’ordre supérieur

Les règles de réécriture constituent souvent un fondement de la sémantique de différents formalismes mathématiques. Par exemple, les études de la sémantique opérationnelle du λ-calcul, basée sur la règle de β-réduction ont beaucoup de points communs avec les études de systèmes de réécriture. On étudie aussi des théories de λ-termes, dont la sémantique est donnée, outre la règle β, par d’autres règles de réécriture.

Un exemple classique d’un tel système est le système T de Gödel (voir par exemple [5]), le λ-calcul des entiers représentés par 0 : nat, succ : nat → nat et une famille de récurseurs, pour chaque type τ une fonction rec_{τ} : τ ×(τ ×nat → τ) × nat → τ, définie par les règles suivantes :

rec_{τ} (u, v, 0) → u
rec_{τ} (u, v, succ(x)) → v(rec_{τ} (u, v, x), x)

Il y a deux moyens de définir la réécriture d’ordre supérieur. Soit on travaille avec des termes en forme β-normale, η-expansée et après chaque application d’une règle de réécriture, on normalise le terme obtenu, soit on permet aux pas de réécriture et de β-réduction de s’entrelacer librement. La façon choisie dépend de l’application et Van de Pol dans [3] montre qu’aucune de deux méthodes n’est plus générale que l’autre. Le système T, mentionné ci-dessus, est habituellement présenté dans ce deuxième cadre.

Les problèmes classique de la réécriture, comme la confluence et la terminaison deviennent plus complexes dans le cas de systèmes d’ordre supérieur. Du point de vue pratique, la situation est encore pire. On ne connaît toujours pas d’algorithme qui résout le problème de filtrage d’ordre supérieur, le mécanisme fondamental de la réécriture. Il est donc possible que ce problème, dans toute sa généralité, soit indécidable, comme le problème d’unification d’ordre supérieur [6], qui lui est très proche.

Comme toujours, quand l’informatique découvre qu’un problème est intraitable (p. ex. NP-difficile), ou même indécidable, on doit chercher des sousclasses de ce problème qui sont plus facilement maniables, mais qui en même temps sont assez grandes pour être utiles en pratique. Dans le cadre de la réécriture d’ordre supérieur, la restriction consiste à limiter la forme des règles. Dans [14] Miller propose une forme particulière de << patterns >> d’ordre supérieur pour lesquels le problème d’unification reste décidable et même quasilinéaire [16].

Grâce à cela l’étude du problème de confluence a pu avancer. Le théorème de Knuth-Bendix, qui réduit la confluence d’un système de réécriture à un simple test de confluence de paires critiques, a été généralisé par Nipkow [15] aux systèmes de réécriture de << patterns >> d’ordre supérieur, d’où décidabilité de cette propriété lorsque la réécriture en question termine.

Pendant les années 90 les premières techniques de preuve de terminaison ont aussi été développées (p. ex. [11]), mais même pour des << patterns >>, l’état de l’art n’est pas comparable avec la multitude de possibilités pour le premier ordre. Seulement récemment une analogie du puissant ordre récursif sur les chemins est apparu [9], mais le théorème de Kruskal qui est très souvent utilisé dans le premier ordre pour démontrer que de nouvelles relations d’ordres sont noetheriennes n’a pas de bonne généralisation connue à l’ordre supérieur.

Complétude de systèmes de réécriture d’ordre supérieur

Ce travail étend la notion de complétude de systèmes de réécriture aux systèmes d’ordre supérieur. Dans ce cadre, la définition de la complétude doit être reformulée. Ce n’est plus raisonnable de demander à certains termes, par exemple λx.f(x), pour un symbole défini f, de se réécrire. Si c’était notre intention, on devrait pouvoir exprimer chaque fonction par un λ-terme constructeur unique, indépendant des arguments. On perdrait donc la possibilité d’avoir un comportement dépendant des valeur des arguments actuels, ce qui est l’essence de la définition par cas et donc des définitions par des règles de réécriture. Pour y remédier on restreint l’ensemble de termes considéré aux seuls termes dont les types sont observables, donc de type de base, qui devront se réécrire en termes constructeurs pour que le système puisse être appelé complet.

Les λ-termes de type supérieur sont donc considérés comme des éléments de l’espace fonctionnel sur l’ensemble de valeurs. Dès qu’on applique une telle fonction à tous les arguments nécessaires, on obtient un terme de type de base, dont la valeur peut être déterminée si le système de règles est complet.

De même, la notion de complétude locale de définition de fonction doit changer. Les fonctions peuvent maintenant prendre des arguments qui sont euxmêmes de type fonctionnel. Étant donné une fonction f, on demande que chaque terme, qui est une application de f à des termes constructeurs à la place des paramètres de type de base et des termes quelconques à la place des paramètres de type fonctionnels, soit réductible. Ce mémoire présente aussi la technique d’arbres de motifs adaptée aux systèmes de réécriture d’ordre supérieur pour tester la complétude locale de définitions de fonctions.

Pour les arguments fonctionnels de la fonction testée trois approches sont étudiées. L’approche classique consiste à traiter les arguments fonctionnels comme des << boîtes noires >>. Ils peuvent être appliqués à quelque chose ou éliminés, mais on ne peut pas modifier la structure interne de la fonction ni faire de récurrence. Dans le cadre de la réécriture cela consiste à limiter la forme des membres gauches de règles utilisées pour définir des fonctions. Les sous-termes de membres gauches qui filtrent les arguments de types fonctionnels doivent être triviaux, la distinction de cas de définitions est donc limitée aux arguments de premier ordre.

Cette approche a un grand avantage : la modularité. Si on ajoute des nouvelles fonctions complètement définies (par des règles appropriées) à un système globalement complet, le nouveau système reste complet. L’inconvénient est l’impossibilité d’utiliser le filtrage d’ordre supérieur ce qui constitue la vraie puissance de la réécriture d’ordre supérieur.

Dans la deuxième approche le filtrage d’ordre supérieur peut être utilisé librement à la seule condition que les cotés gauches des règles soient des << patterns >>. Par exemple considérons la fonction Norm qui calcule la forme normale de fonctions de type bool → bool. Ces deux règles pourrait en faire partie de sa définition :

Norm(λx^{bool}.T ∨ ϕ(x)) → λx^{bool}.T
Norm(λx^{bool}.F ∨ ϕ(x)) → Norm(λx^{bool}.ϕ(x))

Cependant on perd la propriété de modularité : les nouvelles fonctions (même complètement définies), ajoutée à un système complet R peuvent devenir ellesmêmes des arguments des fonction de R. Comme elles ne sont pas considérées par des règles de R, il est possible que le système étendu ne soit plus complet.

La troisième approche non-standard, décrite dans la section 3.8, est un essai d’unifier les avantages des deux premières. On introduit les fonctions à syntaxe limitée, qui sont les fonctions exprimable par des λ-termes utilisant un ensemble spécifié de symboles et qui ont des propriétés similaires aux celles de termes de types de base, sauf qu’elles peuvent être appliquées à des arguments. Les définitions par filtrage sur les arguments fonctionnels de ce nouveau type sont autorisées et la propriété de complétude reste modulaire.

Ce travail présente la problématique de complétude de systèmes d’ordre supérieur dans deux disciplines de types : types simples et types polymorphes. Pour des types simples les trois approches sur le traitement d’arguments fonctionnels sont étudiés dans le cadre de la réécriture de termes normalisés. Dans la discipline de types polymorphes on se restreint à la première approche, la réécriture étant la version où on entrelace librement l’application de règles avec la β-réduction.

Comme dans le premier ordre, la liaison entre la propriété globale de complétude du système et la propriété de complétude locale de définition de fonction est établie par le théorème 2, pour des types simples, et le théorème 4, pour des types polymorphes

L’organisation de ce mémoire est la suivante. Après la présente introductions, la section 2 rappelle d’une façon plus détaillée la problématique de la complétude de systèmes de réécriture de premier ordre. La section 3 décrit l’extension au λ-calcul simplement typé et la section 4 aux types polymorphes. Les conclusions sont données dans la section 5.

2 Premier ordre

La présente section constitue une introduction à la problématique de la complétude de définitions [7, 17, 10]. Les notions de complétude locale, complétude globale ainsi que la procédure de vérification qui seront introduites et expliquées dans cette section, sont assez intuitives dans le cas du premier ordre. Les mêmes notions réapparaîtront dans les sections consacrées à l’ordre supérieur, mais elles seront bien plus complexes et moins intuitives.

2.1 Types et termes

Nous allons travailler avec l’ensemble fini de types de base T. Pour faciliter la présentation, aucun opérateur sur les types ne sera introduit dans cette section.

Pour chaque type τ on a un ensemble dénombrable de variables X_{τ}. La variable x de type τ peut être aussi notée x^{τ}. Les ensembles X_{τ_{1}} et X_{τ_{2}} sont disjoints pour τ_{1} ≠ τ_{2} et l’ensemble de toutes les variables est noté X.

En outre, nous avons aussi besoin d’un ensemble fini de symboles de fonction F. Avec chaque symbole f ∈ F vient une spécification du nombre et des types de ses arguments ainsi que de son type de sortie, ce qui va être noté f : τ_{1} × ⋯ × τ_{n} → τ pour n ≥ 0. Si n = 0, f est une constante et on écrit f : τ.

Les termes bien-typés sont construits selon les règles suivantes :

(var) \overline{x : τ} pour x ∈ X_{τ}

(fun) \frac{u_{1} : τ_{1}, …, u_{n} : τ_{n}}{f(u_{1}, …, u_{n}) : τ} pour \begin{matrix}f ∈ F \\ f : τ_{1} × ⋯ × τ_{n} → τ \end{matrix}

L’ensemble de termes bien-typés, pour X et F donnés, est noté T (F, X). Les termes peuvent être aussi traités comme des arbres étiquetés par des symboles de F ∪ X, on va donc utiliser les suites d’entiers positifs pour symboliser les positions dans les termes ; t|_{p} va signifier un sous-terme de t à la position p et t[u]_{p} un terme t avec un terme u à la place du sous-terme t|_{p}. L’ensemble des variables qui apparaissent dans un terme t est noté FV (t). Une variable est dite linéaire si elle apparaît dans le terme une seule fois. Un terme dont toutes les variables sont linéaire est aussi appelé linéaire. L’ensemble de termes clos (sans variables) est noté T (F).

Les symboles de fonction, qui forment l’ensemble F, sont divisés en deux parties disjointes : l’ensemble des constructeurs C et l’ensemble des symboles définis D. On va toujours supposer que pour tout type τ ∈ T, il existe au moins un terme constructeur t ∈ T (C) tel que t : τ.

Une substitution est une fonction partielle de l’ensemble des variables vers l’ensemble des termes, σ : X → T (F, X), dont le domaine Dom(σ) est fini. D’une façon naturelle cette fonction se prolonge à tout l’ensemble de termes. La fonction étendue (par abus de notation) est toujours notée σ. L’application de la substitution σ à un terme t est notée tσ. Les variables de t qui n’appartiennent pas à Dom(σ) ne changent pas. Une substitution σ de domaine {x_{1}, …, x_{n}} telle que x_{i}σ = t_{i} peut être aussi notée {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}. Si xσ ∈ T (F) pour tout x ∈ Dom(σ), alors σ est appelé une substitution close. D’autres propriétés des termes se prolongent sur les substitutions de la même manière.

2.2 Réécriture du premier ordre

Un système de réécriture est un ensemble fini de règles R = {l_{i} → r_{i}}, pour les termes l_{i}, r_{i} ∈ T (F, X) de même type, qui satisfont les contraintes suivantes :

– les variables du coté droit apparaissent dans le coté gauche, F V (r_{i}) ⊆ F V (l_{i}),

– le coté gauche n’est pas une variable

– le coté gauche ne commence pas par un constructeur l_{i} ≠ c(t_{1}, …, t_{n})

pour c ∈ C, Étant donné un tel système R, un terme s ∈ T (F, X) se réécrit en un terme t en utilisant la règle l → r à la position p, ce qui va être noté s ⟶_{l→r}^{p} t (où tout simplement s ⟶_{R} t), s’il existe une substitution σ telle que s|_{p} = lσ et t = s[rσ]_{p}. La cloture reflexive et transitive de la relation ⟶_{R} sera notée ⟶_{R}^{∗}.

On va supposer en plus que le système R est linéaire, donc chaque coté gauche l_{i} est un terme linéaire. La propriété de linéarité de règles n’est pas fondamentale pour l’étude de la complétude des définitions, mais facilite les définitions d’une façon non-négligeable.

2.3 Complétude

Le but général de la réécriture, compris comme une manière de définir les fonctions et d’exécuter des programmes fonctionnels, est de transformer toute expression close, utilisant des fonctions, en une valeur, donc (en premier ordre) un terme construit uniquement à partir de constructeurs.

Définition 2.3.1 (complétude globale)

Un système de réécriture R est complet ssi pour tout terme clos t ∈ T (F) il existe un terme s ∈ T (C) tel que t ⟶_{R}^{∗} s.

La notion de complétude globale étant complexe, nous allons introduire une propriété auxiliaire qui sera plus facile à démontrer. La complétude locale de la définition de fonction signifie que l’application de cette fonction à des valeurs donne toujours un terme réductible.

Définition 2.3.2 (complétude locale)

Un système de réécriture R définit une fonction f ∈ D, f : τ_{1} × ⋯ × τ_{n} → τ d’une façon localement complète ssi pour tous termes u_{1}, …, u_{n} ∈ T (C), tels que u_{1} : τ_{1}, …, u_{n} : τ_{n}, le terme f(u_{1}, …, u_{n}) est réductible par R.

La complétude locale de tous les symboles définis implique la complétude globale du système, à condition que le système soit fortement normalisant.

Théorème 1 (théorème de complétude)

Soit R un système de réécriture du premier ordre convergent. R est globalement complet si et seulement si R définit tous les symboles f ∈ D d’une façon localement complète.

Preuve. Il est évident que la complétude globale implique la complétude locale de tous les symboles.

Afin de démontrer la réciproque il suffit de prouver que tout terme clos irréductible est un terme constructeur. Supposons que t soit un terme irréductible qui contient des symboles définis. Nécessairement il existe dans t un sous-terme f(u_{1}, …, u_{n}) qui commence par un symbole défini dont tous les arguments u_{1}, …, u_{n} sont des termes constructeurs. Puisque t est clos, ses sous-termes u_{1}, …, u_{n} le sont aussi et par la complétude locale de f, le terme f(u_{1}, …, u_{n}) est réductible, ce qui contredit l’irréductibilité de t. □

2.4 Procédure de vérification

Par la suite on va présenter une procédure qui, pour une fonction f donnée, vérifie la complétude locale de f. La procédure crée un arbre de motifs, dont la racine est le motif le plus général f(x_{1}, …, x_{n}). Les fils d’un nœud interne sont des motifs plus précis que leur père, mais l’ensemble de termes filtrés par les fils est le même que celui filtré par leur père. Les feuilles de l’arbre sont des motifs réductibles, ou bien ceux dont le développement n’aboutirait jamais à un motif réductible.

Avant d’expliquer comment détecter ces derniers, on doit introduire la notion de variable d’induction :

Définition 2.4.1 (variable d'induction)

Soit f ∈ D, soit t = f(t_{1}, …, t_{n}) un terme linéaire, où t_{1}, …, t_{n} ∈ T (C, X). Soit p une position dans t telle que t|_{p} = x soit une variable. La variable x est une variable d’induction dans t s’il existe une règle l_{i} → r_{i} ∈ R telle que t et l_{i} soient unifiables et que p soit une position dans l_{i} telle que l_{i}|p ne soit pas une variable.

Exemple 1. On définit le système suivant dont le type de base est << mots binaires >> :

T = {bin}

        C = {ϵ : bin, 0 : bin → bin, 1 : bin → bin}
        D = {g : bin × bin → bin, h : bin × bin × bin → bin}

avec le système de règles R suivant :

\begin{aligned}1 : & g( 1(x), y) & → & 0(ϵ) \\ 2 : & g( 0(ϵ), y) & → & 1(ϵ) \\ 3 : & g( x, ϵ) & → & x \\ 4 : & h(ϵ, y, z) & → & g(y, z) \\ 5 : & h(0(x), y, z) & → & x \\ 6 : & h(1(x), y, z) & → & x \end{aligned}

Dans le terme g(x, y), x et y sont des variables d’induction, mais dans g(1(x), y), seulement y. Le terme g(0(x), 1(y)) a une seule variable d’induction x, qui est aussi la seule variable d’induction de h(x, y, z).

Ce sont bien évidemment des motifs possédant des variables d’induction qui vont être développés au cours de la construction de l’arbre de motifs. Les autres motifs sont ou bien réductibles, ou bien leur développement ne donne plus aucun espoir pour la réductibilité. Une variable d’induction de type ι peut être remplacé par :

Définition 2.4.2 (ensemble couvrant)

Soit t = f(u_{1}, …, u_{n}) pour f ∈ D et u_{1}, …, u_{n} ∈ T (C, X). Soit p une position de variable d’induction x^{ι} dans t. Un ensemble fini de termes non-variables CS est un ensemble couvrant de x^{ι} dans t ssi pour toute substitution σ telle que yσ ∈ T (C) si y ∈ FV (t), il existe un terme u ∈ CS et une substitution σ̂ tels que tσ = t[u]_{p}σ̂.

Dans le cas du premier ordre un bon candidat pour un ensemble couvrant est un ensemble de tous les constructeurs du type donné :

Proposition 2.4.3 (ensemble couvrant simple)

Soit CS_{∅}(ι) un ensemble de tous les termes de la forme c(x_{1}^{ι_{1}}, …, x_{m}^{ι_{m}}) pour x_{i}^{ι_{i}} nouvelles et distinctes, où c : ι_{1} × ⋯ × ι_{m} → ι est un constructeur. CS_{∅}(ι) est un ensemble couvrant de toute variable d’induction de type ι. □

Le nom d’ensemble couvrant << simple >>, ainsi que l’indice ∅ viennent du fait que le même ensemble sera utilisé également à l’ordre supérieur, à coté des autres ensembles couvrants dont la construction dépendra du contexte de la variable d’induction remplacée. Ces derniers seront décorés par l’information venant du contexte et leur nom figurera les endroits potentiels d’utilisation.

Maintenant on peut présenter la procédure de vérification, qui développe un arbre de motifs. Elle travaille sur des triplets d’ensembles : nœuds de travail (N_{T}), feuilles réductibles (F_{r}) et feuilles irréductibles (F_{ir}).

(succès) \frac{(∅, F_{r}, ∅)}{succès}

(échec) \frac{(∅, F_{r}, F_{ir})}{F_{ir}}

(décompose) \frac{(N_{T} ∪ \{u\}, F_{r}, F_{ir})}{(N_{T} ∪ \{u[v_{i}]_{p}\}_{i∈I}, F_{r}, F_{ir})}
si \{ \begin{matrix}u n’est pas réductible par R \\ u|_{p} = x est une variable d’induction de u \end{matrix}
où \{ \begin{matrix}\{v_{i}\}_{i∈I} est un ensemble couvrant de u|_{p} \\ les variables libres de \{v_{i}\}_{i∈I} sont nouvelles \end{matrix}

(feuille-réd) \frac{(N_{T} ∪ \{u\}, F_{r}, F_{ir})}{(N_{T} , F_{r} ∪ \{u\}, F_{ir})}

si u est réductible par R

(feuille-irréd) \frac{(N_{T} ∪ \{u\}, F_{r}, F_{ir})}{(N_{T} , F_{r}, F_{ir} ∪ \{u\})}
si \{ \begin{matrix}u est irréductible par R \\ u n’a pas de variables d’induction \end{matrix}

Pour tester la complétude locale de définition d’une fonction f ∈ F, où f : ι_{1} × ⋯ × ι_{n} → ι il suffit de lancer la procédure ci-dessus avec le triplet suivant :

({f(x_{1}^{ι_{1}}, …, x_{n}^{ι_{n}})}, ∅, ∅)

Pendant le déroulement de la procédure la structure complète de l’arbre n’est pas mémorisée. Une fois un nœud développé (par la règle (décompose)) seuls ses fils restent dans l’ensemble N_{T}. Donc à tout instant N_{T} ∪F_{r} ∪F_{ir} représente une << frontière >> de l’arbre en cours de construction.

Lorsque la construction de l’arbre est terminée et toutes les feuilles classées << réductible >> ou << irréductible >>, l’une des deux premières règles est déclenchée. Le succès signifie que tous les motifs sont réductibles, et sinon la procédure retourne l’ensemble de cas pour lesquels la fonction f n’est pas définie.

Exemple 1 (suite). On reprend l’exemple de la page 7. Voici la construction de l’arbre de motifs de la fonction g. Les variables d’induction sont indiquées par un caractère gros.

g(x, y) g(x, ϵ) réductible par 3 g(x, 0(y))

g(ϵ, 0(y)) irréductible

g(0(x), 0(y))

g(0(ϵ), 0(y)) réductible par 2 g(0(0(x)), 0(y)) irréductible g(0(1(x)), 0(y)) irréductible g(1(x), 0(y)) réductible par 1

g(x, 1(y))

g(ϵ, 1(y)) irréductible

g(0(x), 1(y))

g(0(ϵ), 1(y)) réductible par 2 g(0(0(x)), 1(y)) irréductible g(0(1(x)), 1(y)) irréductible g(1(x), 1(y)) réductible par 1

Feuilles irréductibles : g(ϵ, 0(y)), g(0(0(x)), 0(y)), g(0(1(x)), 0(y)) g(ϵ, 1(y)), g(0(0(x)), 1(y)), g(0(1(x)), 1(y))

Remarquons que le choix de la variable d’induction y dans la première ligne est arbitraire. Le choix complémentaire créerait un arbre différent, mais le résultat de la procédure serait toujours le même. Cependant il est possible d’avoir á chaque fois un ensemble de motifs irréductibles différents (s’il y avait une seule règle g(ϵ, ϵ) → ϵ par exemple), mais dernière règle utilisée, (succès) ou (échec) est toujours la même.

La vérification de la fonction h est beaucoup plus simple et retourne un succès :

h(x, y, z) h(ϵ, y, z) réductible par 4 h(0(x), y, z) réductible par 5 h(1(x), y, z) réductible par 6

Toutes les feuilles réductibles : succès

2.5 Correction de la procédure de vérification

On va maintenant démontrer la correction de la procédure. Le premier lemme explique la signification de la réponse succès. Lemme 2.5.1 Soit f ∈ D. Si la procédure de vérification lancée pour f retourne un succès, alors le système R définit f d’une façon localement complète. Preuve. Soit Arg(f) l’ensemble de toutes les instances constructeurs closes de f(x_{1}^{ι_{1}}, …, x_{n}^{ι_{n}}), donc des termes f(u_{1}, …, u_{n}) pour u_{1}, …, u_{n} ∈ T (C). Vue la définition 2.4.2 de l’ensemble couvrant, l’utilisation de la règle (décompose) ne diminue pas l’ensemble des instances constructeurs de tous les termes N_{T}. Comme la règle (feuille-réd) ne change pas l’ensemble N_{T} ∪ F_{r} ∪ F_{ir}, donc pendant tout déroulement de la procédure, l’invariant suivant est satisfait :

tout terme t ∈ Arg(f) est une instance d’un terme t̂∈ N_{T} ∪ F_{r} ∪ F_{ir}

Donc si la règle (succès) est déclenchée, alors tout terme de l’ensemble Arg(f) est réductible et donc la définition de f est localement complète. □

La correction de la réponse négative est expliquée par le lemme suivante :

Lemme 2.5.2 Soit f ∈ D. Si la procédure de vérification lancée pour f, utilisant des ensembles couvrants simples CS_{∅} retourne un ensemble de feuilles irréductibles F_{ir}, alors la définition de f n’est pas localement complète.

Preuve. Soit t ∈ F_{ir}. La condition sur la règle (feuille-irréd) dit qu’il n’y a pas de variables d’induction dans t. Montrons que t n’unifie avec aucun coté gauche de R. Par contradiction, supposons que l_{i} soit unifiable avec t. D’après la définition 2.4.1 de variable d’induction, il y a deux possibilités :

– t est clos,

– la position de chaque variable x ∈ F V (t) n’est pas une position stricte

de l_{i}. Puisque le terme l_{i} est linéaire, dans les deux cas t est une instance de l_{i}, alors t est réductible, contradiction. Donc chaque instance constructeur close de t est irréductible. Comme il existe des termes constructeurs clos de chaque type et vu la définitions de CS_{∅} (voir Proposition 2.4.3), il y a des instances closes de t de la forme f(u_{1}, …, u_{n}) pour u_{1}, …, u_{n} ∈ T (C) qui ne sont pas réductibles. □

Pour finir la preuve de correction de la procédure de vérification on doit encore démontrer sa terminaison.

Lemme 2.5.3 La procédure de vérification lancée pour un symbole de fonction f donné termine.

Preuve. Les règles (succès) et (échec) ne peuvent être utilisées qu’une fois. Les règles (feuille-irréd) et (feuille-réd) diminuent l’ensemble N_{T} et seule la règle (décompose) pourrait éventuellement boucler. Mais comme un ensemble couvrant est composé de termes non-variables, la règle (décompose) fait grossir les termes dans N_{T}. Comme la position d’une variable d’induction a une profondeur bornée par celle des règles, les termes dans N_{T} ne peuvent grossir à l’infini. Alors, comme l’ensemble N_{T} est toujours fini, par le lemme de König, tout déroulement de la procédure doit être fini. □

Grâce au théorème 1 ainsi qu’aux lemmes 2.5.1, 2.5.2 et 2.5.3, afin de vérifier la complétude globale d’un système R linéaire fortement normalisant, il suffit de lancer la procédure de vérification pour tous les symboles définis. Le système est complet si et seulement si la procédure retourne un succès pour tous les symboles. Le cas échéant, elle nous fournit pour chaque symbole un ensemble de motifs non-spécifiés.

3 Ordre supérieur : types simples

Dans le cas de termes d’ordre supérieur, la situation est un peu plus complexe. Maintenant des fonctions peuvent prendre des arguments qui, eux aussi, sont des fonctions. Donc pour vérifier que la fonction donnée est définie pour tous ses arguments potentiels, il faut trouver un moyen de décrire d’une façon finie non seulement l’ensemble des arguments de type de base mais aussi les arguments fonctionnels.

3.1 Types et termes

Étant donné un ensemble fini de sortes B, on définit l’ensemble de types simples T par la grammaire suivante :

T ::= B | T → T

Au cas d’ambiguïté on va écrire T (B) pour l’ensemble de type simples construit à partir d’un ensemble de sortes B donné. Les types ι ∈ T, qui ne contiennent aucun symbole →, pour ι ∈ B (puisque B ⊆ T), vont être appelés types de base. Le symbole → est associatif à droite, donc on va écrire τ_{1} → τ_{2} → ⋯ → τ_{n} → τ pour τ_{1} → (τ_{2} → ⋯ → (τ_{n} → τ) …), et τ va être appelé type de sortie si τ ∈ B. Dans ce cas on va représenter ce type aussi par τ_{1} × ⋯ × τ_{n} → τ.

Les termes sont construits à partir d’un ensemble de variables X, un ensemble de symbole de fonction F, l’opérateur d’application -(-) et d’abstraction λ.

Comme dans la section précédente l’ensemble des variables est la somme disjointe des ensembles de variables de chaque type X = ⋃_{τ∈T} X_{τ}. Remarquons qu’une variable peut désormais avoir un type d’ordre supérieur, par exemple

bin → bin.

Les symboles de fonctions dans l’ensemble fini F sont aussi équipés d’un type, f : τ_{1} × ⋯ × τ_{n} → ι. On va supposer toujours que ι ∈ B, mais τ_{1}, …, τ_{n} peuvent être arbitraires.

On va travailler dans cette section avec des λ-termes algébriques, alors suivant la convention de [8], les éléments de F ne vont pas être tout simplement traités comme des constantes d’ordre supérieur. Dans des λ-termes algébriques un symbole n-aire f est toujours suivi de ses n-arguments. Le langage des termes est défini par la grammaire suivante :

Λ ::= X | Λ(Λ) | λX .Λ | F(Λ, …, Λ)

On ne regarde pas l’arité de symboles de fonction pour l’instant, parce que cela est pris en charge par les règles de typage qui limitent l’ensemble Λ aux termes bien-typés. Afin de suivre la convention de termes algébriques, on va souvent écrire u(v_{1}, …, v_{n}) pour u(v_{1}) … (v_{n}). Pour éviter la confusion on peut toujours supposer que les variables libres et liées sont disjointes, et par conséquent, que les variables libres du terme u restent libres dans t{x ↦ u}. Les positions dans les λ-termes sont aussi des suites d’entiers positifs, la construction λx étant considéré comme un symbole unaire pour tout x ∈ X.

Les règles qui associent des types simples à certains termes sont les suivantes :

(var) \overline{x^{τ} : τ}

(fun) \frac{u_{1} : τ_{1}, …, u_{n} : τ_{n}}{f(u_{1}, …, u_{n}) : τ} pour \begin{matrix}f ∈ F \\ f : τ_{1} × ⋯ × τ_{n} → τ \end{matrix}
(abs) \frac{u : ρ}{λx^{τ} .u : τ → ρ}
(app) \frac{u : τ → ρ v : τ}{u(v) : ρ}

L’ensemble de tous les termes bien-typés, pour F et X donnés est (comme auparavant) noté T (F, X). Les termes clos sont maintenant les termes qui ne contiennent pas de variables libres, mais ils peuvent contenir des variables liées (par exemple λx^{τ} .x^{τ} est un terme clos de type τ → τ), les termes clos, bientypés sont toujours noté T (F).

Comme dans la section précédente, l’ensemble de symboles F est divisé en deux parties disjointes : les constructeurs C et les symboles définis D. Maintenant on met une condition supplémentaire sur les constructeurs. Leurs types doivent être du premier ordre, donc si c : τ_{1} × ⋯ × τ_{n} → τ est un constructeur, alors τ_{1}, …, τ_{n}, τ ∈ B. Comme dans la section précédente l’ensemble de termes constructeurs clos bien-typés est noté T (C) et on suppose toujours que pour chaque type de base ι ∈ B il existe un terme constructeur t ∈ T (C) tel que t : ι.

3.2 Forme β-normale η-expansée

On va travailler presque uniquement sur les termes en forme β-normale η-expansée. Pour calculer cette forme on va utiliser les règles :

(λx^{τ} .v)(u) ⟶_{β} u{x^{τ} ↦ v}
C[u]_{p} ⟶_{η} C[λx^{τ} .u(x^{τ})]_{p} pour x^{τ} ∉ F V (u)

La règle de η-expansion ne pourra s’appliquer que sous les conditions suivantes : – u : τ → σ

– u n’est pas une abstraction

– C[u]|_{q} n’est pas une application pour p = q · 1 On va noter u↕_{β}^{η} la forme normale de u, et si on est sûr que la normalisation n’utilise que la règle η (notamment pour des variables d’ordre supérieur) on écrira u↑^{η}; T (F, X) ↕_{β}^{η} va signifier l’ensemble de termes bien-typés en forme normale.

A cause de confluence de règles β et η on obtient le lemme suivant : Lemme 3.2.1 Si u est un terme en forme β-normale η-expansée, de type τ_{1} × ⋯×τ_{m} → ι pour m ≥ 0, ι ∈ B, alors u = λx_{1}^{τ_{1}} … x_{m}^{τ_{m}}.ϕ(u_{1}, …, u_{n}), ϕ ∈ F ∪X, ϕ : ρ_{1} × ⋯ × ρ_{n} → ι et les termes u_{1}, … u_{n} sont eux aussi en forme normale. Corollaire 3.2.2 Soient s, t deux termes en forme normale tels que s|_{p} et t soient de même type. Alors s[t]_{p} est aussi en forme normale.

3.3 Réécriture d’ordre supérieur de termes normalisés

La définition d’un système de réécriture reste la même que celle de premier ordre. Un système de réécriture d’ordre supérieur est donc un ensemble fini de règles {l_{i} → r_{i}}, où l_{i}, r_{i} sont des termes d’ordre supérieur, normalisés. Outre des conditions nécessaires (l_{i} et r_{i} de même type, F V (r_{i}) ⊆ F V (l_{i}), l_{i} ∉ X, l_{i} ≠ c(u_{1}, …, u_{n}) pour c ∈ C), qui ont été déjà introduites dans la section précédente, on va restreindre la forme du coté gauche aux patterns. Définition 3.3.1 (pattern) Un terme normalisé t est un pattern ssi pour tout sous-terme s de t, si s = Y (u_{1}, …, u_{n}) pour Y ∈ F V (t), la suite u_{1}, …, u_{n} est η-équivalente à une suite de variables liées distinctes. Voici quelque exemples de << patterns >> : λx.Y (λz.x(z)), λx.c(λz.Y (z, x)), Y, λx.c(x) et quelque termes qui ne le sont pas : λx.Y (x, x), λxy.Y (x, c), λx.Y (Z(x)), Y (d). Les << patterns >> ont toutes les bonnes propriétés de décidabilité des termes de premier ordre, l’unification peut être calculée en temps quasi-linéaire [16], et cette classe de termes est assez large pour la plupart des application.

La définition de la relation de réécriture associée à un système de règles donné est une simple généralisation de celle de premier ordre. Un terme normalisé s ∈ T (F, X) se réécrit en un terme t en utilisant la règle l → r à la position p, ce qui va être noté s ⟶_{l→r}^{p} t (où tout simplement s ⟶ t), s’il existe

une substitution σ telle que s|_{p} =_{βη} lσ et t = s[rσ↕_{β}^{η}]_{p}. La différence se manifeste seulement par le fait que le coté gauche de la règle doit être égal à un sous-terme approprié modulo les règles β et η, et qu’on normalise le coté droit substitué, avant de le mettre dans le terme réécrit. D’après le corollaire 3.2.2, le terme t est normalisé.

3.4 Complétude

La notion de complétude globale diffère légèrement de celle de premier ordre. Comme on a dit dans l’introduction, on ne va plus exiger des termes fonctionnels (λx.f(x), pour f ∈ D, par exemple) de se réécrire en termes constructeurs. Seuls les termes de type de base doivent avoir une forme normale dans l’ensemble de valeurs du premier ordre T (C).

Définition 3.4.1 (complétude globale)

Un système de réécriture R est complet ssi pour tout terme clos t ∈ T (F) de type de base il existe un terme s ∈ T (C) tel que t ⟶_{R}^{∗} s. De même que dans le premier ordre on va introduire une notion de complétude locale de définition d’une fonction, mais ici on doit également faire un petit changement. Dans le premier ordre on a défini la complétude locale d’une fonction f, comme la réductibilité des tous les termes f(u_{1}, …, u_{n}) pour u_{1}, …, u_{n} construits à partir de constructeurs. Ici on permet aux arguments fonctionnels d’être arbitraires. Cette nouvelle définition vient du même raisonnement que celle de complétude globale.

Définition 3.4.2 (f-terme canonique)

Soit f : τ_{1} × ⋯ × τ_{n} → ι où ι ∈ B. Un terme normalisé u = f(u_{1}, …, u_{n}) va être appelé f-terme canonique si pour tout i = 1 … n, u_{i} une des conditions suivantes est satisfaite :

– u_{i} a un type fonctionnel

– u_{i} a un type de base et u_{i} ∈ T (C, X)

Les arguments u_{1}, …, u_{n} de f construit comme dans la définition du f-terme canonique vont être appelés arguments canoniques.

Pour un terme avec variables libres v = f(v_{1}, …, v_{n}), une substitution σ telle que vσ ↕_{β}^{η} soit un f-terme canonique, va être appelée une substitution canonique de v.

La complétude locale signifie bien sûr la réductibilité de tous les f-termes canoniques clos :

Définition 3.4.3 (complétude locale)

Un système de réécriture R définit une fonction f ∈ D, f : τ_{1} × ⋯ × τ_{n} → ι d’une façon localement complète ssi tout f-terme canonique clos est réductible par R.

Heureusement à l’ordre supérieur le rapport entre la complétude locale de définition de tous les symboles et la complétude globale du système fortement normalisant reste le même qu’au premier ordre :

Théorème 2 (théorème de complétude)

Soit R un système de réécriture d’ordre supérieur convergent. R est globalement complet si et seulement si R définit tous les symboles f ∈ D d’une façon localement complète. Preuve. Comme dans la section précédente la difficulté existe seulement dans un sens. On va utiliser la recurrence sur l’union de l’ordre de sous-terme et de l’ordre de réduction, impliqué par la relation noetherienne ⟶_{R}. Le fait que cette union est bien-fondée peut être trouvé dans [4]. On va montrer que pour chaque terme de type de base t, il existe un terme t′ ∈ T (C) tel que t ⟶_{R}^{∗} t′, si tous les symboles sont localement complets.

Soit t un terme clos de type de base. Si t=c(s_{1}, …, s_{n}), pour c ∈ C, alors les sous-termes s_{1}, …, s_{n} de t sont aussi de type de base. Par hypothèse de récurrence, il existe des termes s′_{1}, …, s′_{n} ∈ T (C) tels que pour tous i, s_{i} ⟶_{R}^{∗} s′_{i}. Donc t′ = c(s′_{1}, …, s′_{n}) et bien évidemment t′ ∈ T (C) et t ⟶_{R}^{∗} t′.

Si t = f(s_{1}, …, s_{n}), pour f ∈ D, f : τ_{1} × ⋯ × τ_{n} → ι, alors pour tout i tel que τ_{i} ∈ B (par hypothèse de récurrence) il existe des termes s′_{i} ∈ T (C) tels que s_{i} ⟶_{R}^{∗} s′_{i}. Pour les autres i on pose s′_{i} = s_{i}. Soit t_{1} = f(s′_{1}, …, s′_{n}). Comme f est localement complète, t_{1} est réductible, disons t_{1} ⟶_{R} t_{2}. Comme t_{2} est strictement plus petit que t dans l’ordre de réduction (puisque t ⟶_{R}^{∗} t_{1} ⟶_{R} t_{2}), par hypothèse de récurrence, il existe un terme t_{3} ∈ T (C) tel que t_{2} ⟶_{R}^{∗} t_{3}. Donc comme t ⟶_{R}^{∗} t_{2} ⟶_{R}^{∗} t_{3}, on obtient le résultat.

Le cas de base est un terme irréductible sans sous-termes, donc une constante qui appartient à C. □

3.5 Procédure de vérification

Cette section présente une adaptation de la procédure de vérification de la complétude locale pour la réécriture d’ordre supérieur. On va d’abord définir une notion auxiliaire :

Définition 3.5.1 (sous-terme transparent)

Soit u un terme normalisé, et p une position dans u. On va appelle u|_{p} un sousterme transparent de u s’il n’y a pas de variables libres sur le chemin entre la racine et le sous-terme u|_{p} et si u|_{p} = X(x_{1}↑^{η}, …, x_{n}↑^{η}) où X : τ_{1} × ⋯ × τ_{n} → ι, pour ι ∈ B, est une variable libre linéaire dans u et x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}} sont des variables liées distinctes.

On redéfinit maintenant quelque notions de la section précédente.

Définition 3.5.2 (variable d'induction)

Soit f ∈ D. Étant donné un f-terme normalisé u et une position p, tels que u|_{p} =_{η} X(x_{1}, …, x_{n}) soit un sous-terme transparent, on appelle X variable d’induction s’il existe une règle l_{i} → r_{i} dans R, telle que u soit unifiable avec l_{i} et l_{i}|p ne soit pas un sous-terme transparent de la forme (η-égale à) Y (y_{1}, …, y_{n}), pour Y libre et y_{1}, …, y_{n} liées.

Au cours de la construction de l’arbre de motifs, les sous-termes transparents dont le symbole de tête est une variables d’induction vont être remplacés par des ensembles couvrants. Mais la définition d’ensemble couvrant doit être adaptée à la notion de f-terme canonique.

Définition 3.5.3 (ensemble couvrant)

Soit f : τ_{1} ×⋯×τ_{n} → ι où ι ∈ B. Soit u = f(u_{1}, …, u_{n}) un f-terme canonique et p une position dans u, telle que u|_{p} soit un sous-terme transparent. L’ensemble fini CS de termes linéaires normalisés va être appelé ensemble couvrant de u|_{p}, ssi pour toute substitution canonique close σ de u il existe un terme v ∈ CS et une substitution σ̂ telle que uσ ↕_{β}^{η}= u[v]_{p}σ̂ ↕_{β}^{η}.

La procédure de vérification de la section 2 (dans la page 8) n’est presque pas modifiée. Ce qui change est la définition de variable d’induction et donc la règle (décompose) qui l’utilise, ainsi que les définitions des ensembles couvrants qui vont être étudiés dans les sous-sections qui suivent, pour les différentes approches traitant les arguments fonctionnels.

(succès) \frac{(∅, F_{R}, ∅)}{succès}

(échec) \frac{(∅, F_{R}, F_{I})}{F_{I}}

(décompose) \frac{(N_{T} ∪ \{u\}, F_{R}, F_{I})}{(N_{T} ∪ \{u[v_{i}]_{p}\}_{i∈I}, F_{R}, F_{I})}

si \{ \begin{matrix}u n’est pas réductible par R \\ u|_{p} = X(x_{1}↑^{η}, …, x_{n}↑^{η}) est un sous-terme transparent \\ X est une variable d’induction de u \end{matrix}

où \{ \begin{matrix}\{v_{i}\}_{i∈I} est un ensemble couvrant de u|_{p} \\ les variables libres de \{v_{i}\}_{i∈I} sont nouvelles \end{matrix}

(feuille-réd) \frac{(N_{T} ∪ \{u\}, F_{R}, F_{I})}{(N_{T} , F_{R} ∪ \{u\}, F_{I})}

si u est réductible par R

(feuille-irréd) \frac{(N_{T} ∪ \{u\}, F_{R}, F_{I})}{(N_{T} , F_{R}, F_{I} ∪ \{u\})}
si \{ \begin{matrix}u est irréductible par R \\ u n’a pas de variables d’induction \end{matrix}

Comme auparavant, pour tester la complétude locale de la définition de la fonction f ∈ D, f : τ_{1} × ⋯ × τ_{n} → ι, on lance la procédure avec le triplet initial :

{(f(x_{1}^{τ_{1}}↑^{η}, …, x_{n}^{τ_{n}}↑^{η}), ∅, ∅)}

La correction de la réponse positive de la procédure peut être démontrée maintenant, avant de présenter les ensembles couvrants utilisés. L’argumentation reste la même que dans le cas de premier ordre.

Lemme 3.5.4 Soit f ∈ D. Si la procédure de vérification lancée pour f retourne un succès, alors le système R définit f d’une façon localement complète.

Preuve. On va montrer que l’application successive des règles (décompose) et (feuille-réd) ne viole pas l’invariant suivant :

tout f-terme canonique clos t est une instance d’un terme t̂∈ N_{T} ∪ F_{r} ∪ F_{ir}

Pour la règle (feuille-réd) c’est évident puisqu’elle ne change pas l’ensemble N_{T} ∪ F_{r} ∪ F_{ir}.

La règle (décompose) change l’ensemble N_{T}, mais vu la définition 3.5.3 de l’ensemble couvrant, ne diminue pas l’ensemble de f-termes canoniques qui sont instances de N_{T}.

Chaque déroulement de la procédure qui résulte en un succès est une suite d’applications des règles (décompose) et (feuille-réd) suivi par (succès). La règle (feuille-irréd) ne peut pas être appliquée puisque à la fin on a F_{ir} = ∅, pour déclencher la règle (succès).

Comme tout terme canonique clos est un instance du terme initiale, l’invariant est satisfait et toutes les feuilles sont réductibles, donc chaque f-terme canonique clos est réductible. □

3.6 Approche classique sur les arguments fonctionnels

Cette sous-section va considérer l’approche classique qui est utilisé dans des langages fonctionnels existants. Il n’est pas permis de regarder la structure interne des arguments fonctionnels qui sont traités comme des << boîtes noires >> et la pleine puissance du filtrage d’ordre supérieur n’est pas utilisée.

Définition 3.6.1 Un système de réécriture R = {l_{i} → r_{i}} est appelé classique si toutes les règles satisfont la condition suivante : si l_{i} = f(u_{1}, …, u_{n}) pour f : τ_{1} × ⋯ × τ_{n} → ι alors tous les sous-termes u_{j} tels que τ_{j} ∉ B sont (ηéquivalents à) des variables linéaires.

On va montrer que dans ce cas toutes les variables d’induction sont du premier ordre et qu’on peut utiliser l’ensemble couvrant simple CS_{∅} (de la proposition 2.4.3) dans la procédure de vérification.

Lemme 3.6.2 Soit R un système de réécriture classique, soit f ∈ D, f : τ_{1} × ⋯ × τ_{n} → ι pour ι ∈ B et u un f-terme canonique. Soit p une position d’un sous-terme transparent dans u avec une variable d’induction X en tête. Alors, le type de X est un type de base.

Preuve. Soit u = f(u_{1}, …, u_{n}) et l_{j} le coté gauche (d’une règle de R) qui s’unifie avec u. Puisque p n’est pas la position de la racine, donc p = i · q pour i ∈ 1 … n. Supposons que τ_{i} ne soit pas de type de base, τ_{i} = ρ_{1} ×⋯×ρ_{m} → ρ, pour ρ ∈ B. Le symbole de tête de l_{j} est f et alors l_{j} = f(t_{1}, …, t_{n}), où t_{i} = λx_{1}^{ρ_{1}} … x_{m}^{ρ_{m}}.Y (x_{1}, …, x_{m}) pour une variable Y : τ_{i} linéaire dans l_{j}. Comme u_{i} est normalisé, alors u_{i} = λx_{1}^{ρ_{1}} … x_{m}^{ρ_{m}}.u′_{i}. Donc la position q dans u_{i} doit être au moins aussi profonde que la position du sous-terme transparent Y (x_{1}, …, x_{m}) dans t_{i}, contradiction.

Donc τ_{i} est un type de base. Puisque les constructeurs ont des types du premier ordre, il n’y a pas de λ sur le chemin de la racine vers p. Donc u|_{p} = X, parce qu’il n’y a pas de variables liées qui peuvent être arguments de X. □

Alors la procédure de vérification utilisée pour tester les fonctions définies par des systèmes de réécriture classique n’est pas différente de celle pour le premier ordre. Nous avons donc gratuitement les lemmes manquants (2.5.2 correction de l’échec et 2.5.3 terminaison) pour prouver la correction de la procédure pour des systèmes classiques linéaires.

La bonne propriété des systèmes classiques, mentionnée dans l’introduction, c’est la modularité.

Lemme 3.6.3 Soit R_{1} et R_{2} deux systèmes classiques convergeants, sur le même ensemble de types T sur les signatures F_{1} et F_{2} respectivement, tels que F_{1} ∩ F_{2} = C_{1} = C_{2}. Si R_{1} et R_{2} sont complets et R_{1} ∪ R_{2} termine, alors R_{1} ∪ R_{2} est aussi complet.

Preuve. Soit R = R_{1} ∪ R_{2}, F = F_{1} ∪ F_{2}. On va prouver par contradiction que chaque terme de type de base clos irréductible est un terme constructeur. Soit t un terme irréductible, qui contient des symboles non-constructeurs, minimal dans le sens de sous-terme, donc tel que tous ses sous-termes immédiat de premier ordre sont constructeurs. On a donc t = f(t_{1}, …, t_{n}) pour f ∈ D_{1} (par exemple), f : τ_{1} × ⋯ × τ_{n} → ι pour ι ∈ B. Pour tout i, tel que τ_{i} ∈ B, on a t_{i} ∈ T (C) et donc on pose s_{i} = t_{i}. Pour les autres i, s_{i} est un terme arbitraire (de type fonctionnel) clos, irréductible, mais s_{i} ∈ T (F_{1}). Comme R_{1} est complet, il y a une règle l_{j} → r_{j} qui réduit le terme s = f(s_{1}, …, s_{n}) et elle peut être appliquée seulement en tête. Mais R_{1} est un système classique et ne fait pas de filtrage sur les arguments fonctionnels. Donc l_{j} doit filtrer aussi le terme t. Contradiction. □

3.7 Approche moins restrictive

Dans cette approche, on ne met aucune condition supplémentaire sur la forme des règles (sauf celle que les membres gauches doivent être des << patterns >>), donc pour les arguments de type fonctionnel on a besoin de l’ensemble couvrant suivant, qui remplace un sous-terme transparent X(x_{1}^{τ_{1}} ↑^{η} , …, x_{n}^{τ_{n}} ↑^{η}) : ι.

Définition 3.7.1 (grand ensemble couvrant)

Le grand ensemble couvrant, CS_{x_{1}^{τ_{1}} ,...,x_{n}^{τn}} (ι) contient tous les termes de la forme

f(X_{1}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}})↑^{η}, …, X_{m}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}})↑^{η})

pour f ∈ F, f : ρ_{1} × … × ρ_{m} → ι et X_{j} : τ_{1} → ⋯ → τ_{n} → ρ_{i} distinctes. Il contient également tous les termes de la forme :

x_{i}^{τ_{i}}(X_{1}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}})↑^{η}, …, X_{m}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}})↑^{η})

pour x_{i} variable liée de type τ_{i} = ρ_{1} × … × ρ_{m} → ι (X_{1}, …, X_{m} comme avant).

Sa correction (vis-à-vis la définition 3.5.3) est démontrée par la proposition suivante :

Proposition 3.7.2 Soit f : ξ_{1} × ⋯ × ξ_{n} → ξ où ξ ∈ B. Soit u = f(u_{1}, …, u_{k}) un f-terme canonique et p une position dans u, telle que p = i · q pour ξ_{i} ∉ B, et telle que u|_{p} est un sous-terme transparent η-égale à X(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}}), pour X : τ_{1}×⋯×τ_{n} → ι, ι ∈ B. L’ensemble CS_{x_{1}^{τ_{1}} ,...,x_{n}^{τn}} (ι) est un ensemble couvrant de u|_{p}.

Preuve. Soit σ une substitution canonique close de u. D’après le lemme 3.2.1, Xσ↕_{β}^{η}= λy_{1}^{τ_{1}} … y_{n}^{τ_{n}}.ϕ(t_{1}, …, t_{n}) pour ϕ ∈ F ∪X. La substitution est close, donc il y a deux possibilités :

– ϕ est une variable liée, ϕ = y_{j}^{τ_{j}} et dans ce cas τ_{j} = ρ_{1} × ⋯ × ρ_{m} → ι on prend v = x_{j}^{τ_{i}}(X_{1}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}})↑^{η}, …, X_{m}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}})↑^{η})

– ϕ est un symbole de fonction, ϕ = g pour g : ρ_{1} × ⋯ × ρ_{m} → ι et on

prend v = g(X_{1}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}})↑^{η}, …, X_{m}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}})↑^{η}) Dans les deux cas, on pose

X_{1}σ̂ = λy_{1}^{τ_{1}} … y_{n}^{τ_{n}}.t_{1}
⋮
X_{m}σ̂ = λy_{1}^{τ_{1}} … y_{n}^{τ_{n}}.t_{m}

Pour les Y ∈ Dom(σ) tels que Y ≠ X on pose Y σ̂ = Y σ. Il est évident que uσ ↕_{β}^{η}= u[v]_{p}σ̂ ↕_{β}^{η}. □

La terminaison de la procédure est établie par le lemme suivant, dont la preuve est presque identique à celle du premier ordre.

Lemme 3.7.3 La procédure de vérification, qui utilise les ensembles couvrants CS_{∅} et CS\overline{x} , lancée pour un symbole de fonction f donné, termine.

Preuve. Comme les ensembles couvrants CS_{∅} et CS\overline{x} sont composés de termes non-transparents, la règle (décompose) fait grossir les termes dans N_{T}, dans le sens que le multi-ensemble de distances de la racine de sous-termes transparents dans les termes introduits dans N_{T} est plus grand que celui du terme supprimé. Comme la position d’un sous-terme transparent dominé par une variable d’induction a une profondeur bornée par celle des règles, les termes dans N_{T} ne peuvent grossir à l’infini. Comme l’ensemble N_{T} est toujours fini, par le lemme de König, toute suite d’applications de la règle (décompose) doit être fini. Puisque toute déroulement éventuel infini de la procédure doit comprendre une infinité d’applications de la règle (décompose), on obtient le résultat. □

Malheureusement, dans cette approche on n’a pas de lemme de correction de la réponse négative. Il se peut que la procédure retourne des termes irréductibles, mais qu’il n’existe aucun f-terme canonique clos irréductible. Cependant, si un tel terme existe, il est forcément une instance d’un terme retourné par la procédure. La procédure peut donc être vue, comme un outil de preuve semiautomatique. Elle fait tout le travail mécanique et laisse seulement des cas plus difficiles pour l’utilisateur.

Exemple 2. Supposons avoir les définitions suivantes : \begin{aligned}B_{2} & = & \{α, β, γ\} \\ C_{2} & = & \{a, b, c\} \\ D_{2} & = & \{f, g\} \end{aligned}  \begin{aligned}a & : & β → α \\ b & : & β \\ f & : & (β → β) → γ \\ g & : & α → β \\ c & : & γ \end{aligned}

Considérons maintenant le système de règles suivant :

\begin{aligned}1 : & g(a(x)) & → & b \\ 2 : & f(λx^{β}.x) & → & c \\ 3 : & f(λx^{β}.b) & → & c \end{aligned}

et procédons à la verification de complètude de définition de f.

f(λx^{β}.X(x))
f(λx^{β}.x)  réd. par 2
f(λx^{β}.b)  réd. par 3
f(λx^{β}.g(Y (x))) irréd.

La procédure retourne le terme f(λx^{β}.g(Y (x))) qui est irréductible par notre système de règles. Mais la seule possibilité d’avoir une instance close du terme rétourné est de mettre à la place de Y (x) le terme a(…), puisque l’argument de g doit être de type α et a seul possède un tel type de sortie. Dans ce cas :

f(λx^{β}.g(a(X(x)))) ⟶_{1} f(λx^{β}.b) ⟶_{3} c

et on s’apperçoit que f est tout de même complètement définie.

Quand même pour un système linéaire, si dans un des termes retournés par la procédure toutes les variables libres sont de type de base, on peut trouver un f-terme canonique clos irréductible. L’argument est le même que dans la preuve du lemme 2.5.2 de la section 2.

Comme l’on a dit dans l’introduction la complétude des systèmes sans restriction n’est pas une propriété modulaire.

Exemple 3. On définit un système R_{1} des entiers avec la fonction Biz de type d’ordre supérieur (intuitivement Biz(f) ⟶^{∗} f(1), mais ce n’est pas du tout important dans cet exemple) :

T = {nat}
C = {0 : nat, succ : bin → bin}
D_{1} = {Biz : (nat → nat) → nat}

avec les règles :

1 :  Biz(λx^{nat}.x) → succ(0)
2 :  Biz(λx^{nat}.0) → 0
3 :  Biz(λx^{nat}.succ(Y (x))) → succ(Biz(λx^{nat}.Y (x)))
4 : Biz(λx^{nat}.Biz(λy^{nat}.Y (y, x)) → Biz(λy^{nat}.Y (y, succ(0)))

Le système R_{1} est complet, puisque sa seule fonction est localement complète. Examinons la construction de l’arbre de motifs :

Biz(λx^{nat}.Z(x))
Biz(λx^{nat}.0)  réd. par 2
Biz(λx^{nat}.succ(Y (x)))  réd. par 3
Biz(λx^{nat}.Biz(λy^{nat}.Z(x, y)) réd. par 4
Biz(λx^{nat}.x)  réd. par 1

Utilisant une fois la règle (décompose) pour remplacer le sous-terme transparent Z(x) par l’ensemble couvrant CS_{x} (nat), plusieurs fois la règle (feuille-réd) et une fois la règle (succès), on a montré la complétude locale de la définition de Biz et donc (par le théorème 2) la complétude globale de R_{1}.

Maintenant on prend un autre système complet R_{2}, sur le même ensemble de types et de constructeurs, avec la fonction + :

                   D_{2} = {+ : nat × nat → nat}

avec les règles bien connues :

\begin{aligned}5 : & x + 0 & → & x \\ 6 : & x + succ(y) & → & succ(x + y) \end{aligned}

La somme de deux systèmes R = R_{1} ∪ R_{2} n’est pas complète puisque le terme de type nat, Biz(λx^{nat}.x + x), est une forme normale.

3.8 Nouvelle approche : << fonctions à syntaxe limitée >>

La troisième approche est un essai de joindre les avantage des deux premières. On permet l’utilisation du filtrage d’ordre supérieur, mais seulement pour les arguments de certains types fonctionnels. Pour chaqun de ces types on pré-définit l’ensemble de symboles qui peuvent être utilisés.

3.8.1 Extension du système de types

On va maintenant considérer l’ensemble de types simples construit à partir de l’ensemble de sortes B = SPEC ∪ BASE, SPEC ∩ BASE = ∅, pour un ensemble BASE de types de base et l’ensemble SPEC de nouveaux types fonctionnels. On peut distinguer maintenant les ensembles de types

T_{→BASE} = {τ | τ = ρ_{1} × ⋯ × ρ_{n} → ι pour ι ∈ BASE}
T_{→SPEC} = {τ | τ = ρ_{1} × ⋯ × ρ_{n} → s pour s ∈ BASE}

D’une façon similaire on définit les ensembles X_{→BASE} et X_{→SPEC} (ainsi que F_{→BASE} et F_{→SPEC} ), comme ensembles de variables (symboles) de types T_{→BASE} et T_{→SPEC} respectivement.

A chaque type s ∈ SPEC on va associer un vrai type fonctionnel Type(s) ∈ T (BASE), construit uniquement à partir de types de base et un ensemble de symboles symb(s). Intuitivement les λ-termes de type Type(s), construits à partir des symb(s) vont avoir un type s. On va exiger que Type(s) ainsi que le type de tout symbole h ∈ symb(s) soient du premier ordre, donc de la forme ι_{1} × ⋯ × ι_{n} → ι pour ι_{1}, …, ι_{n}, ι ∈ BASE, comme les types des constructeurs.

Pour indiquer le type d’une fonction f ∈ F_{→SPEC} on va écrire à l’occasion f : τ_{1} × ⋯ × τ_{n} → [ι_{1} × ⋯ × ι_{m} → ι]_{s} si f : τ_{1} × ⋯ × τ_{n} → s et Type(s) = ι_{1} × ⋯ × ι_{m} → ι. Si un tel symbole f est suivi de tous ses n + m arguments (ce qui va être souvent le cas), on va le noter f(u_{1}, …, u_{n})(v_{1}, …, v_{m}).

Exemple 4. Supposons avoir les définitions suivantes :

BASE_{4} = {nat}_{C_{4} = {0, s}}_{D_{4} = {+, ∗}} 0 : nat

                                     s : nat → nat
                                  +, ∗ : nat × nat → nat

On introduit un type spécial Lin — les fonctions linéaires d’une variable. On pose :

SPEC_{4} = {Lin}

                      Type(Lin) = nat → nat

symb(Lin) = {0, s, +}

Les termes λx^{nat}.0, λx^{nat}.s(x) et λx^{nat}.x+s(x+s(s(0))) (on utilise une notation infixe pour + et ∗) ont un type Lin, mais le terme λx^{nat}.x ∗ x utilise le symbole interdit ∗.

Étant donné un ensemble de symboles F, avec des types de T (BASE ∪ SPEC ) associés à chaque symbole, en utilisant l’extension évidente de la fonction Type, on peut leur associer des types de T (BASE) de la manière suivante (on va utiliser le signe \overline{:} ) :

Si f : τ_{1} × ⋯ × τ_{n} → τ alors f \overline{:} \overline{Type}(τ_{1}) × ⋯ × \overline{Type}(τ_{n}) → \overline{Type}(τ)

où \overline{Type} est une extension de Type sur T (BASE ∪SPEC ) dans T (BASE) définie inductivement comme suit :

\overline{Type}(ι) = ι  pour ι ∈ BASE
\overline{Type}(s) = Type(s) pour s ∈ SPEC
\overline{Type}(τ_{1} → τ_{2}) = \overline{Type}(τ_{1}) → \overline{Type}(τ_{2})

3.8.2 Nouvelles règles de typage

Afin de déterminer les λ-termes qui ont un type s ∈ SPEC donné, on a besoin d’un prédicat qui vérifie la bonne construction des termes. Pour chaque type s ∈ SPEC on définit un prédicat BON_{s} :

Définition 3.8.1 (prédicat de construction)

Soit s ∈ SPEC , où Type(s) = ι_{1} ×⋯×ι_{m} → ι. Un terme normalisé u ∈ BON_{s} si et seulement si une des conditions suivantes est vraie :

1. u = x^{ι} où, x^{ι} ∈ X, ι ∈ BASE,

2. u = c(u_{1}, …, u_{n}) pour c ∈ symb(s), si u_{1}, …, u_{n} ∈ BON_{s},

3. u = f(u_{1}, …, u_{n})(v_{1}, …, v_{m}) pour f ∈ F, si f : τ_{1} × ⋯ × τ_{n} → s et v_{1}, …, v_{m} ∈ BON_{s}, (u_{1}, …, u_{n} arbitraires)

4. u = x(u_{1}, …, u_{n})(v_{1}, …, v_{m}) pour x^{τ_{1}×···×τ_{n}→s} ∈ X, si u_{i} ∈ BON_{s} pour tout i, où τ_{i} ∈ T_{→BASE} et v_{j} ∈ BON_{s}

5. u = λx^{τ} .u′ si u′ ∈ BON_{s} Remarquons que des termes de différents types peuvent appartenir à BON_{s} pour un type s donné. Maintenant on est prêt à présenter les règles de typage des termes dans la forme β-normale η-expansée (au sens de \overline{:} ), prenant en compte les types fonctionnels à syntaxe limitée.

(fun-base) \frac{u_{1} :_{↦} τ_{1}, …, u_{n} :_{↦} τ_{n}}{ϕ(u_{1}, …, u_{n}) :_{↦} ι}
si \{ \begin{matrix}ϕ ∈ F_{→BASE} ∪ X_{→BASE} , \\ ϕ : τ_{1} × ⋯ × τ_{n} → ι \end{matrix}
(fun-spec) \frac{u_{1} :_{↦} τ_{1}, …, u_{n} :_{↦} τ_{n}, v_{1} :_{↦} ι_{1}, …, v_{m} :_{↦} ι_{m}}{ϕ(u_{1}, …, u_{n})(v_{1}, …, v_{m}) :_{↦} ι}

si \{ \begin{matrix}ϕ ∈ F_{→SPEC} ∪ X_{→SPEC} , \\ ϕ : τ_{1} × ⋯ × τ_{n} → s, \\ Type(s) = ι_{1} × ⋯ × ι_{m} → ι \end{matrix}

(lambda) \frac{u :_{↦} σ}{λx^{τ} .u :_{↦} τ → u}

(spec) \frac{u :_{↦} Type(s)}{u :_{↦} xs} pour s ∈ SPEC si u ∈ BON_{s}

L’axiome x^{τ} : τ, qu’on peut trouver dans chaque système de typage, est ici caché dans la règle (fun-base). Voici quelques exemples de termes typables par le nouveau système :

Exemple 5. Afin de montrer le fonctionnement du système de typage, on va enrichir l’exemple précédent de nouvelles fonctions définies, qui travaillent sur des types spéciaux. On a donc :

BASE_{5} = BASE_{4} = {nat}
SPEC_{5} = SPEC_{4} = {Lin}
C_{5} = {0, s}
D_{5} = {+, ∗, A, M}

                                      A : nat → Lin
                                      M : Lin → Lin

Les termes u_{1} = λx^{nat}.A(0)(x + 0), u_{2} = λy^{nat}.M(λx^{nat}.A(s(0))(x))(y) et u_{3} = λx^{nat}.x^{nat} + A(x ∗ s(0))(x) ont tous le type Lin. Remarquons que le mauvais symbole ∗ apparaît dans u_{3} dans le premier argument de la fonction A, mais selon la condition 3 de la définition du prédicat BON_{s}, on doit seulement assurer la bonne construction de la deuxième liste d’arguments.

Par contre les termes v_{1} = λx^{nat}.A(0)(x ∗ x), v_{2} = λx^{nat}.A(0, 0) ∗ x et v_{3} = λy^{nat}.M(λx^{nat}.A(0)(x ∗ y))(y) n’ont pas de type Lin. Les termes v_{1} et v_{2} ont uniquement le type nat → nat, mais le terme v_{3} n’est pas du tout typable par notre système.

3.8.3 Complétude

Dans cette section on va étudier la complétude de systèmes de réécriture qui peuvent utiliser le filtrage d’ordre supérieur, mais seulement dans les arguments de types fonctionnels à syntaxe limitée.

Définition 3.8.2 Un système de réécriture R = {l_{i} → r_{i}} est appelé limité si toutes les règles sont de type de base et satisfont les conditions suivantes :

– si l_{i} = f(u_{1}, …, u_{n}) pour f : τ_{1} × ⋯ × τ_{n} → τ, alors tous les sous-termes u_{j} tels que τ_{j} ∉ BASE ∪ SPEC sont (η-égaux à) des variables linéaires

– si l_{i} = f(u_{1}, …, u_{n})(v_{1}, …, v_{m}) pour f : τ_{1} × ⋯ × τ_{n} → s, s ∈ SPEC , alors les sous-termes v_{1}, …, v_{m} sont des variables linéaires.

Il faut encore faire la remarque que les deux conditions ne s’excluent pas. Donc, si on prendre les types de l’exemple précédent, le membre gauche d’une règle qui définit la fonction f : (nat → nat) × Lin × nat → Lin doit être de la forme f(λx^{nat}.Y (x), u, v)(z), pour Y et z libres. Par contre les termes u et v peuvent être plus détaillés.

La notion de complétude, qu’on va présenter ici pour des systèmes limités, est plus forte que celle pour des systèmes standard. Comme on l’a dit dans l’introduction, les nouveaux types fonctionnels ont beaucoup de points communs avec les types de base. Une similarité est le fait qu’on va demander, que les termes clos d’un type s ∈ SPEC donné aient une forme construit uniquement à partir de symboles pré-définis symb(s). On pourrait donc écrire un terme compliqué de type s, faire le calcul au niveau de la fonction, le simplifier jusqu’à la forme normale construit de symb(s), et ensuite appliquer la forme simple à des arguments, peut-être plusieurs fois, sans recalculer la fonction de nouveau.

Un des inconvénients de cette approche est le fait que la propriété essentielle de préservation de types par réécriture, qui est normalement assurée par la simple condition que le membre gauche et le membre droit de chaque règle aient le même type, devient non-triviale dans le cadre de types fonctionnels à syntaxe limitée. De plus il y a une autre condition sur les termes qui doit être préservée par le système. Définition 3.8.3 (condition VAR) Un terme normalisé t :_{↦} τ satisfait la condition VAR si les conditions suivantes sont satisfaites :

1. si u est un sous-terme de t et u :_{↦} s pour s ∈ SPEC , alors F V (u) ⊆ X_{→SPEC}

2. si f(u_{1}, …, u_{n})(v_{1}, …, v_{m}) est un sous-terme de t, pour f : τ_{1}×⋯×τ_{n} → [ι_{1} × ⋯ × ι_{m} → ι]_{s}, s ∈ SPEC , alors F V (u_{1}, …, u_{n}) ⊆ X_{→SPEC}

On donnera quelques outils de preuve de préservation de typabilité et la condition VAR par des règles de réécriture dans 3.8.5. Pour l’instant on peut présenter la nouvelle version de la notion de complétude.

Définition 3.8.4 (complétude globale)

Soit R un système de réécriture sur la signature contenant des types fonctionnels à syntaxe limitée. On dit que R est globalement complet si pour tout terme clos t, qui satisfait la condition VAR,

– si t :_{↦} ι pour ι ∈ BASE alors il existe t′ ∈ T (C) tel que t ⟶_{R}^{∗} t′

– si t :_{↦} s pour s ∈ BASE alors il existe t′ ∈ T (symb(s)) tel que t ⟶_{R}^{∗} t′

La condition VAR sert en principe à éliminer les termes de nouveaux types fonctionnels qui sont de la mauvaise forme. Si le système de réécriture est limité, un terme clos λx^{nat}.A(x)(x) qui a le type Lin peut être réduit uniquement par une règle dont le membre gauche est de la forme A(y)(z), qui filtre tout autre terme avec A en tête. Si on demande la réductibilité de ce terme, on perd la possibilité de distinction de cas.

Le changement de la notion de complétude globale nécessite la modification correspondante de la complétude locale. On commence par la nouvelle définition de f-terme canonique.

Définition 3.8.5 (f-terme canonique)

Soit f : τ_{1}×⋯×τ_{n} → τ où τ ∈ BASE (respectivement τ ∈ SPEC et Type(τ) = ι_{1} ×⋯×ι_{m} → ι). Un terme u = f(u_{1}, …, u_{n}) (resp. u = f(u_{1}, …, u_{n})(⊥_{1}, …, ⊥_{m})) va être appelé f-terme canonique si pour tout i = 1 … n, u_{i} est clos et l’une des conditions suivantes est satisfaite dans u :

– u_{i} a un type fonctionnel

– u_{i} a un type de base et u_{i} ∈ T (C, X)

– u_{i} a un type s ∈ SPEC et u_{i} ∈ T (symb(s), X) (les symboles ⊥_{1}, …, ⊥_{m} sont des nouvelles constantes de types appropriés qui n’appartiennent pas à F)

La complétude locale (voir la définition 3.4.3) de f est comme toujours la réductibilité de tout f-terme canonique clos.

Comme les systèmes de réécriture considérés ici sont des systèmes limités, la complétude locale d’un symbole de fonction f dont le type de sortie s appartient à SPEC (Type(s) = ι_{1} ×⋯×ι_{m} → ι), garantit aussi la réductibilité des termes λx_{1}^{ι_{1}} … x_{m}^{ι_{m}}.f(u_{1}, …, u_{n})(x_{1}, …, x_{m}) pour u_{1}, …, u_{n} clos ainsi que de tous les termes f(u_{1}, …, u_{n})(v_{1}, …, v_{m}) pour u_{1}, …, u_{n} clos et v_{1}, …, v_{m} quelconques.

Afin de prouver l’équivalence entre complétude locale de tout les symboles et complétude globale du système, on a besoin d’un lemme encore plus fort, pour pouvoir faire la preuve par récurrence.

Lemme 3.8.6 Soit R un système de réécriture limité convergent, qui préserve la typabilité au sens de :_{↦} et la condition VAR. Si R définit tous les symboles f ∈ D d’une façon localement complète, alors pour un terme normalisé t qui satisfait VAR, les trois conditions suivantes sont satisfaites :

1. si t :_{↦} ι pour ι ∈ BASE et t est clos, alors il existe t′ ∈ T (C) tel que t ⟶_{R}^{∗} t′

2. si t :_{↦} s pour s ∈ SPEC et t clos, alors il existe t′ ∈ T (symb(s)) tel que t ⟶_{R}^{∗} t′

3. si t :_{↦} ι pour ι ∈ BASE et t ∈ BON_{s} pour un s ∈ SPEC donné tel que Type(s) = τ_{1} × ⋯ × τ_{m} → τ et si F V (t) ⊆ {x_{1}^{τ_{1}}, …, x_{m}^{τ_{m}}}, alors il existe t′ ∈ T (symb(s), X) tel que t ⟶_{R}^{∗} t′

Preuve. On prouve le lemme par récurrence sur l’union d’ordre de sous-terme et d’ordre de réduction (impliqué par la relation noetherienne ⟶_{R}). Soit R et t comme dans le lemme.

1. si t :_{↦} ι pour ι ∈ BASE et t est clos, alors il y a trois possibilités selon le

symbole de tête de t (qui n’est pas une variable puisque t est clos) :

– t = c(t_{1}, …, t_{n}) pour c ∈ C. Les sous-terme t_{1}, …, t_{n} de t sont clos du premier ordre et alors, par hypothèse de récurrence, il existe des termes t′_{1}, …, t′_{n} ∈ T (C) tels que pour tout i, t_{i} ⟶_{R}^{∗} t′_{i}. Dans ce cas t ⟶_{R}^{∗} c(t′_{1}, …, t′_{n}).

– t = f(t_{1}, …, t_{n}) pour f ∈ D, f : τ_{1} × ⋯ × τ_{n} → ι, ι ∈ BASE.

– t = f(t_{1}, …, t_{n})(u_{1}, …, u_{m}) pour f ∈ D, f : τ_{1} × ⋯ × τ_{n} →

[ι_{1} × ⋯ × ι_{m} → ι]_{s}, s ∈ SPEC . Dans les deux derniers cas on calcule par récurrence les formes normales t′_{i} pour les i où τ_{i} ∈ BASE ∪SPEC , pour les autres on pose t′_{i} = t_{i}. Le terme t′ = f(t′_{1}, …, t′_{n}) (ou bien t′ = f(t′_{1}, …, t′_{n})(u_{1}, …, u_{m})) est réductible. Disons que t′ ⟶_{R} t′′. On a donc t ⟶_{R}^{∗} t′ ⟶_{R} t′′ et par récurrence sur ⟶_{R} on peut trouver dans T (C) la forme normale de t′′.

2. si t :_{↦} s pour s ∈ SPEC , Type(s) = ι_{1} × ⋯ × ι_{m} → ι et t clos, alors t = λx_{1}^{ι_{1}} … x_{m}^{ι_{m}}.t_{1}, pour t_{1} :_{↦} ι et t_{1} ∈ BON_{s}. Alors par récurrence (le point 3), t_{1} ⟶_{R}^{∗} t′_{1} pour t′_{1} ∈ T (symb(s), X). Donc t ⟶_{R}^{∗} λx_{1}^{ι_{1}} … x_{m}^{ι_{m}}.t′_{1} où ce dernier terme est clos.

3. si t :_{↦} ι pour ι ∈ BASE et t ∈ BON_{s} pour un s ∈ SPEC donné tel que Type(s) = τ_{1} × ⋯ × τ_{m} → τ et si F V (t) ⊆ {x_{1}^{τ_{1}}, …, x_{m}^{τ_{m}}} alors on a les possibilités suivantes :

– t ∈ X. Donc forcément t = x_{i}^{τ_{i}} pour un i.

– t = c(t_{1}, …, t_{n}) pour c ∈ symb(s). Les types de t_{i} sont dans BASE et donc par récurrence, on a les formes souhaitées t′_{i} ∈ T (symb(s), X) et alors t ⟶_{R}^{∗} c(t′_{1}, … t′_{n})

– t = f(t_{1}, …, t_{n})(u_{1}, …, u_{m}) pour f : τ_{1} ×⋯×τ_{n} → s. Comme t satisfait la condition VAR, les termes t_{1}, …, t_{n} sont clos. Par hypothèse de récurrence, on obtient les formes normales t′_{i} souhaitées pour les i où τ_{i} ∈ BASE ∪ SPEC . Pour les autres i on pose t′_{i} = t_{i}. On a donc t = f(t′_{1}, …, t′_{n})(u_{1}, …, u_{m}), où t ⟶_{R}^{∗} t′. Par complétude locale, t′ se réduit à t′′. Donc on peut utiliser l’hypothèse de récurrence pour t′′.

Le terme t ne peut pas avoir un autre symbole en tête puisque t ∈ BON_{s}. □ On peut maintenant prouver immédiatement le théorème de complétude pour des systèmes utilisant les types fonctionnels à syntaxe limitée.

Théorème 3 Soit R un système de réécriture limité convergent, qui préserve la typabilité au sens de :_{↦} et la condition VAR. Le système R est globalement complet si et seulement si R définit tous les symboles f ∈ D d’une façon localement complète.

Preuve. L’implication dans un sens est une simple conséquence du lemme précédent, et dans l’autre, comme toujours, est évidente. □

3.8.4 Vérification de complétude

Pour vérifier la complétude locale d’un symbole f donné, on peut utiliser la procédure de la page 16. Pour un symbole f ∈ F_{→SPEC} on va utiliser le triplet initial suivant :

({f(X_{1}^{τ_{1}}↑^{η}, …, X_{n}^{τ_{n}}↑^{η})(⊥_{1}, …, ⊥_{m})}, ∅, ∅)

pour f : τ_{1} × ⋯ × τ_{n} → [ι_{1} × ⋯ × ι_{m} → ι]_{s}. Il faut encore définir l’ensemble couvrant à utiliser pour des arguments d’un type s ∈ SPEC donné, pour remplacer un sous-terme transparent X(x_{1}^{ι_{1}}, …, x_{n}^{ι_{n}}) de type ι. Sa construction est très similaire à celle du grand ensemble couvrant, sauf que dans ce dernier on prenait en compte tous les symboles de la signature (de type de sortie approprié) et maintenant seulement les symboles autorisés de l’ensemble symb(s).

Définition 3.8.7 (ensemble couvrant limité)

L’ensemble couvrant limité, s-CS_{x_{1}^{ι_{1}},...,x_{n}^{ιn}} (ι), (pour ι_{1}, …, ι_{n} ∈ BASE) contient tous les termes de la forme

f(X_{1}(x_{1}^{ι_{1}}, …, x_{n}^{ι_{n}}), …, X_{m}(x_{1}^{ι_{1}}, …, x_{n}^{ι_{n}}))

où f ∈ symb(s) et f : τ_{1} ×⋯×τ_{m} → ι, X_{1}, …, X_{n} sont des nouvelles variables libres de type X_{i} : ι_{1} × ⋯ × ι_{n} → τ_{i}.

De plus, l’ensemble s-CS_{x_{1}^{ι_{1}},...,x_{n}^{ιn}} (ι) contient toutes les variables liées parmi x_{1}^{ι_{1}}, …, x_{n}^{ι_{n}} pour lesquelles ι_{i} = ι.

La preuve de correction (vis-à-vis la définition 3.5.3) est très similaire à celle du grand ensemble couvrant :

Proposition 3.8.8 Soit f : ξ_{1} × ⋯ × ξ_{n} → ξ où ξ ∈ BASE (respectivement ξ ∈ SPEC et Type(ξ) = ι_{1} × ⋯ × ι_{m} → ι). Soit u = f(u_{1}, …, u_{k}) (resp. u = f(u_{1}, …, u_{k})(⊥_{1}, …, ⊥_{m})) un f-terme canonique et p une position dans u, telle que p = i·q pour ξ_{i} ∈ SPEC , et telle que u|_{p} est un sous-terme transparent η-égale à X(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}}), pour X : τ_{1} × ⋯ × τ_{n} → τ, τ_{1}, …, τ_{n}, τ ∈ BASE. L’ensemble CS_{x_{1}^{τ_{1}} ,...,x_{n}^{τn}} (ι) est un ensemble couvrant de u|_{p}.

Preuve. Soit σ une substitution canonique close de u. D’après le lemme 3.2.1, Xσ↕_{β}^{η}= λy_{1}^{τ_{1}} … y_{n}^{τ_{n}}.ϕ(t_{1}, …, t_{n}) pour ϕ ∈ F ∪X. La substitution est close, donc il y a deux possibilité :

– ϕ est une variable liée, ϕ = y_{j}^{τ_{j}} et dans ce cas m = 0, parce que τ_{j} ∈ BASE, donc on prend v = x_{j}

– ϕ est un symbole de fonction, ϕ = g pour g : ρ_{1} × ⋯ × ρ_{m} → ι. Comme uσ ↕_{β}^{η} est un terme canonique, alors g ∈ symb(s) et on peut prendre v = g(X_{1}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}}), …, X_{m}(x_{1}^{τ_{1}}, …, x_{n}^{τ_{n}}))

Dans le deuxième cas, on pose

X_{1}σ̂ = λy_{1}^{τ_{1}} … y_{n}^{τ_{n}}.t_{1}
⋮
X_{m}σ̂ = λy_{1}^{τ_{1}} … y_{n}^{τ_{n}}.t_{m}

Pour les Y ∈ Dom(σ) tels que Y ≠ X on pose Y σ̂ = Y σ. Il est évident que uσ ↕_{β}^{η}= u[v]_{p}σ̂ ↕_{β}^{η}. □

Remarquons que dans le triplet initial, à la position d’un argument du type s ∈ SPEC donné, il y a toujours un terme λx_{1}^{ι_{1}} … x_{m}^{ι_{m}}.X(x_{1}, …, x_{m}) pour Type(s) = ι_{1} ×⋯×ι_{m} → ι. Alors le premier sous-terme transparent dans cette position est de la forme décrite dans la proposition (des types ι_{1}, …, ι_{m} ∈ BASE et comme la construction de s − CS_{x_{1}^{ι_{1}} ...x_{m}^{ιm}} ne le change pas, à chaque fois que l’on veut déclencher la règle (décompose) pour un sous-terme transparent d’un argument de type fonctionnel à syntaxe limitée, on peut utiliser un ensemble couvrant limité approprié.

La preuve de terminaison de la procédure de vérification peut être directement copiée du lemme 3.7.3, parce que l’utilisation des ensembles couvrants limités éloigne les variables libres de la racine de la même façon que l’utilisation des grands ensembles couvrants. Donc on peut se servir du même argument dans la preuve.

Comme pour l’approche précédente, il est aussi facile de trouver un exemple de fonction dont la définition est localement complète, mais pour laquelle la fonction retourne des f-termes canoniques irréductibles. Reprenons l’exemple 3 de la page 20. On introduit un type fonctionnel à syntaxe limité S par :

SPEC_{2} = {S}
Type(S) = β → β
symb(S) = {a, b, g}

et on change légèrement le type de la fonction f : S → γ. Le test de la fonction f se déroule d’une façon identique et l’exemple irréductible retourné par la procédure est inductivement réductible pour la même raison.

Mais par contre la propriété de complétude de systèmes limités est à nouveau modulaire.

Lemme 3.8.9 Soient R_{1} et R_{2} deux systèmes limités convergents, préservant la typabilité et la condition VAR, utilisant le même ensemble de types T et les signatures F_{1} et F_{2} respectivement, tels que F_{1} ∩ F_{2} = C_{1} = C_{2} et que les spécifications de tous les types s ∈ SPEC soient les mêmes. Si R_{1} et R_{2} sont complets et R_{1} ∪ R_{2} termine et préserve typabilité et VAR, alors R_{1} ∪ R_{2} est aussi complet.

Preuve. Soit R = R_{1} ∪ R_{2}, F = F_{1} ∪ F_{2}. On va montrer par contradiction que chaque symbole f ∈ F est complètement défini par R. Supposons qu’il y ait un f-terme canonique u ∈ T (F) clos irréductible, pour f ∈ D_{1}, f : τ_{1} × ⋯ × τ_{n} → τ. Si τ ∈ BASE, alors u = f(u_{1}, …, u_{n}) et si τ ∈ SPEC , alors u = f(u_{1}, …, u_{n})(⊥_{1}, …, ⊥_{m}). On échange maintenant tous les arguments u_{i} de types τ_{i} ∉ BASE ∪SPEC pour des termes u′_{i} ∈ T (F_{∞}) (de types appropriés). Soit u′ le terme après le changement. Le système R_{1} est complet, u est réductible par une règle l_{j} → r_{j}. Mais comme R_{1} est un système limité, l_{j} = f(t_{1}, …, t_{n}) (où l_{j} = f(t_{1}, …, t_{n})(x_{1}, …, x_{m}) pour f ∈ F_{→SPEC} ) pour t_{i} = Y ↑^{η} si τ_{i} ∉ BASE ∪ SPEC . Or si l_{j} filtre u′, il filtre également le terme u. Contradiction. □

La preuve était essentiellement identique à celle de la modularité de la complétude des systèmes classiques (lemme 3.6.3).

3.8.5 Conditions sur des règles de réécriture

On va donner quelque conseils pour prouver qu’un système de règles donné préserve la typabilité au sens de :_{↦} et la condition VAR. Pour préserver la typabilité, il faut absolument que le système préserve le prédicat BON_{s} pour tout s ∈ SPEC . Pour prouver la préservation de typabilité, voici quelque remarques :

– pour des règles de premier ordre, si les symboles du membre gauche appartiennent à symb(s) il faut que les symboles du membre droit y appartiennent aussi.

– pour des règles d’ordre supérieur, si le membre gauche commence par un symbole d’ordre supérieur f ∈ F_{→BASE} , le membre gauche ne satisfait de prédicat BON_{s} pour aucun s.

– pour des règles d’ordre supérieur, si le membre gauche commence par un symbole f ∈ F_{→SPEC} , avec le type de sortie s ∈ SPEC , le membre gauche peut éventuellement satisfaire le prédicat BON_{s}, donc il faut vérifier cela dans le membre droit. Un tel membre droit ne satisfait pas de prédicat BON_{s′} pour les autres types s′ ∈ SPEC .

Le lemme suivant pourrait aider aussi à prouver la préservation de ces propriétés par le système de réécriture.

Lemme 3.8.10 Soit t un terme normalisé typable, qui satisfait VAR et σ une substitution normalisée typable qui satisfait VAR. Le terme tσ↕_{β}^{η} satisfait VAR. De plus si t ∈ BON_{s}, pour un s ∈ SPEC donné, et pour tout x ∈ X_{→BASE} , tel que x ∈ Dom(σ), xσ ∈ BON_{s}, alors tσ↕_{β}^{η}∈ BON_{s}.

Preuve. Puisque t et σ sont typables, ils sont également typables au sens de \overline{:} (voir la page 22) et donc tσ est un terme typable du λ-calcul simplement typé, alors il est fortement normalisant. On prouve par récurrence sur le nombre de β-réductions nécessaires pour obtenir tσ↕_{β}^{η} à partir de tσ. On fait également la récurrence interne sur la construction de t.

– t = x, c’est trivial

– t = λx.t′. Comme t satisfait VAR et BON_{s}, alors t′ aussi, donc on prouve le résultat par récurrence.

– t = f(t_{1}, …, t_{n}), f - de premier ordre. Les sous-termes satisfont VAR et BON_{s}. Si f ∈ F base d’ordre supérieur, t ∉ BON_{s}, mais les sous-termes satisfont VAR. On obtient donc le résultat par récurrence.

– t = f(t_{1}, …, t_{n})(u_{1}, …, u_{m}) pour f ∈ F_{→SPEC} . Les sous-termes t_{1}, …, t_{n} n’ont pas de variables dans X_{→BASE} et les termes substitués par σ non plus. Les u_{1}, …, u_{m} satisfont VAR par récurrence. Si le type de sortie de f est s alors on a u_{1}, …, u_{m} ∈ BON_{s} et on conclut par récurrence. Si le type de sortie de f est un autre type dans SPEC , alors t ∉ BON_{s}.

– t = X(t_{1}, …, t_{n}). Si X ∈ X_{→BASE} alors t ∉ BON_{s}. Si X ∈ X_{→SPEC} , et type de sortie de X est s, tous les termes t_{i} de type T_{→BASE} sont BON_{s}. Par hypothèse de récurrence, t_{i}σ↕_{β}^{η} sont BON_{s} aussi. Maintenant on peut appliquer la récurrence sur le nombre de β-réductions. Xσ = λx_{1} … x_{n}.t′, on peut construire un terme normalisé t′ et une substitution normalisée σ′ = {x_{i} ↦ t_{i}σ ↕_{β}^{η}}. Comme t′σ′ est obtenu de tσ par n β-réductions nécessaires, le nombre de β-réductions pour normaliser t′σ′ et plus petit que celui pour normaliser tσ, on peut utiliser la récurrence. □

L’étude de systèmes avec types fonctionnels à syntaxe limitée est donc très compliquée. Cette approche constitue un intermédiaire entre l’approche classique et l’approche sans restrictions. On essaie de joindre les avantages de ces deux approches, mais les difficultés qui apparaissent sont très grandes. On doit mettre plusieurs conditions non-triviales sur les règles de réécriture, le typage est non-standard et peu clair, les résultats de complétude s’appliquent uniquement à des certains termes. On voit donc que cette approche est trop complexe pour être utilisée en pratique.

4 Ordre supérieur : types polymorphes

Cette section est consacrée à l’étude de la problématique de complétude de systèmes de réécriture d’ordre supérieur dans le cadre de types polymorphes. Les types polymorphes sont dans ce travail équipés d’opérateurs algébriques, comme dans l’article [8], par exemple l’opérateur list(·), qui pour un type quelconque τ donne le type list(τ) de listes d’éléments de type τ.

Même si ces opérateurs, et leurs constructeurs appropriés, peuvent être représentés directement par des types et des termes du système F pur (sans constantes de types et de termes), leur codage est très compliqué et peu intuitif. Par exemple l’ouvrage [5] propose la traduction suivante de l’opérateur list(·) et de ses constructeur Nil_{τ} : list(τ) (liste vide) et Cons_{τ} : τ × list(τ) → list(τ) (tête) :

list(τ) = ∀α.α → (τ → α → α) → α
Nil_{τ} = Λα.λx^{α}.λy^{τ→α→α}.x
Cons_{τ} (h, t) = Λα.λx^{α}.λy^{τ→α→α}.y(h, tα(x, y))

4.1 Types polymorphes

Étant donné un ensemble dénombrable de variables de types Φ, ainsi qu’un ensemble fini d’opérateurs de sortes S = ⋃_{n≥0} S_{n}, on définit l’ensemble de types T_{∀}, comme suit :

T_{∀} ::= Φ | S_{n}(T_{∀}^{n}) | T_{∀} → T_{∀} | ∀Φ.T_{∀}

L’ensemble d’opérateurs de sortes d’arité 0, S_{0} prend la place de l’ensemble de sortes B de la section précédente. Dans le cadre de types polymorphes, les types de base sont tous les types construits uniquement à partir d’opérateurs de sortes. On va aussi écrire qu’un type τ est de premier ordre, τ ∈ T (S, Φ), s’il est construit à partir d’opérateurs de sortes et de variables de types Φ. La convention sur l’utilisation du symbole →, reste la même que dans la section précédente.

Le nouveau symbole ∀ lie des variables de type de la même façon que l’opérateur λ lie des variables de terme dans les termes du λ-calcul, on peut donc définir analogiquement la notion de variable de type libre et liée ainsi que la substitution de type. Le quantificateur signifie intuitivement qu’un terme qui a le type ∀α.τ a tous les types τ{α ↦ ρ} pour tous les ρ possible.

4.2 Termes du λ-calcul polymorphe

On va utiliser un ensemble dénombrable de variables X qui est, comme avant, une somme disjointe de variables de chaque type. L’ensemble de toutes les variables dont le type commence par un opérateur de sortes s ∈ S, va être noté par le symbole X_{S}. On va avoir également un ensemble fini de symboles de fonction

F = ⋃_{τ_{1},...,τ_{n},τ} F_{τ_{1}×···×τ_{n}→τ}

où l’ensemble F_{τ_{1}×···×τ_{n}→τ} contient tout les symboles algébriques dont les types des arguments sont τ_{1}, …, τ_{n} et le type de sortie τ. Remarquons que dans la section précédente le type de sortie de chaque fonction était le type de base. Maintenant le type de sortie peut être arbitraire. Comme avant, F = C ∪ D où C est un ensemble de constructeurs. Pour chaque opérateur de sorte s ∈ S_{n} on a un nombre fini de constructeurs

c : τ_{1} × ⋯ × τ_{m} → s(α_{1}, …, α_{n}) pour τ_{1}, …, τ_{m} ∈ T (S, {α_{1}, …, α_{n}})

À partir de X et F on va construire l’ensemble des termes algébriques du λ-calcul polymorphe. En outre d’opérateurs d’abstraction et d’application les termes vont aussi utiliser l’opérateur d’abstraction de type et d’application de type.

T ::= X | λX .T | T (T ) | F(T , …, T ) | ΛΦ.T | T T_{∀}

L’ensemble de variables de type libre dans un terme t donné va être noté F V T (t). L’ensemble de termes typables, noté toujours T (F, X), est calculé en utilisant les règles de typage suivantes :

(var) \overline{x^{τ} : τ}

(fun) \frac{u_{1} : τ_{1}, …, u_{n} : τ_{n}}{f(u_{1}, …, u_{n}) : τ} pour \begin{matrix}f ∈ F \\ f : τ_{1} × ⋯ × τ_{n} → τ \end{matrix}
(abs-terme) \frac{u : ρ}{λx^{τ} .u : τ → ρ}
(app-terme) \frac{u : τ → ρ v : τ}{u(v) : ρ}
(abs-type) \frac{u : ρ}{Λα.u : ∀α.ρ} si α n’est pas libre dans les types de F V (u)

(app-type) \frac{u : ∀α.ρ}{uτ : ρ\{α ↦ τ\}}

On va supposer que pour tout type de premier ordre il y a des termes constructeurs de ce type et l’ensemble de termes constructeurs typables clos va être noté T (C).

La sémantique du λ calcul polymorphe, en plus de la règle β (voir 3.2) est donné aussi par la règle T β suivante :

(Λα.u)τ ⟶_{T β} u{α ↦ τ}

4.3 Réécriture

Comme on l’a dit dans l’introduction, dans cette section on ne va plus considérer la réécriture de termes normalisés, mais la version ou les réductions par des règles du système et les β-réductions peuvent s’entrelacer arbitrairement. Étant donné un système de règles R = {l_{i} → r_{i}} qui satisfont les conditions de la section 2.2, un terme u ∈ T (F, X) se réécrit à un terme t à la position p en utilisant la règle l_{i} → r_{i} ce qui va être noté s ⟶_{l→r}^{p} t (où tout simplement s ⟶ t), s’il existe une substitution de type σ_{T} et une substitution σ telle que s|_{p} = lσ_{T} σ et t = s[rσ_{T} σ]_{p}.

On va se restreindre par contre aux systèmes algébriques, où tous les membres gauches sont de la forme f(u_{1}, …, u_{n}) pour f ∈ D.

On va dire que R est convergent si la relation ⟶_{Rβ} = ⟶_{R} ∪ ⟶_{β} ∪ ⟶_{T β} est convergente. Les propriétés de tels systèmes mixtes sont étudiées entre autres dans l’article [8].

4.4 Complétude

La notion de complétude de systèmes de réécriture dans le cadre de types polymorphes ne diffère pas beaucoup de celle de la section précédente :

Définition 4.4.1 (complétude globale)

Un système R convergent est appelé globalement complet si pour tout terme t clos, dont le type est clos de premier ordre, il existe un terme s ∈ T (C) tel que t ⟶_{Rβ} s.

La notion de complétude locale nécessite une modification dans le cadre de types polymorphes. La fonction localement complète doit être définie pour les arguments clos qui sont construits à partir de constructeurs jusqu’aux soustermes qui ne sont pas de premier ordre.

Définition 4.4.2 (complétude locale)

Un système R définit une fonction f ∈ D pour f : τ_{1} × ⋯ × τ_{n} → τ d’une façon localement complète si tout terme f(t_{1}, …, t_{n}) est réductible pour une substitution de types σ_{T} et si pour tout i, t_{i} : τ_{i}σ_{T}, t_{i} = t′_{i}γ_{i} pour une substitution close γ_{i} et t′_{i} ∈ T (C, X) et F V (t′_{i}) ∩ X_{S} = ∅.

Afin de démontrer le théorème de complétude, on doit prouver la proposition suivante :

Proposition 4.4.3 Soit t un terme typable clos. Si t = t_{1}(t_{2}) ou bien t = t_{1}τ, alors t contient un β-redex, un T β-redex ou un sous-terme clos de la forme f(u_{1}, …, u_{n}) pour f ∈ D

Preuve. Par récurrence sur la construction de t_{1}, qui ne peut pas commencer par un constructeur ni par une variable.

– Si t = t_{1}(t_{2}) alors t_{1} : τ_{1} → τ_{2}. Donc on a quatre possibilités : 1. t_{1} = f(u_{1}, …, u_{n}) pour f ∈ D,

2. t_{1} = λx.t′_{1} donc t est un redex,

3. t_{1} = t_{3}(t_{4}) pour t_{3} : τ_{4} → (τ_{1} → τ_{2}), par hypothèse de récurrence on trouve un sous-terme voulu dans t_{1},

4. t_{1} = t_{3}ρ pour t_{3} : ∀α.τ′_{1} → τ′_{2}, par hypothèse de récurrence, t_{1}

contient un sous-terme cherché.

– Si t = t_{1}τ alors t_{1} : ∀α.τ′ et on a les possibilités suivantes : 1. t_{1} = f(u_{1}, …, u_{n}) pour f ∈ D, 2. t_{1} = Λα.t′, donc t est un redex,

3. t_{1} = t_{3}(t_{4}) pour t_{3} : τ_{4} → ∀α.τ′, par hypothèse de récurrence, on trouve un sous-terme voulu dans t_{1},

4. t_{1} = t_{3}ρ pour t_{3} : ∀β.τ′_{3} — par hypothèse de récurrence, t_{1} contient un sous-terme expecté. □

Maintenant on va prouver un lemme qui implique directement le théorème de complétude. Mais avant de faire cela on a besoin de quelques notions auxiliaires.

Définition 4.4.4 Soit τ un type polymorphe. Il existe un type de premier ordre ρ et une substitution de types σ_{T} tels que τ = ρσ_{T}, ρ ∈ T (S, Φ) et pour toute α ∈ F V T (ρ), ασ_{T} ≠ s(ξ_{1}, …, ξ_{n}) pour s ∈ S. Alors le chapeau de τ, noté cap(τ), est égal à ρ et l’ensemble de ses aliens aliens(τ) = {ασ_{T} | α ∈ FVT (τ)}

On a donc, intuitivement introduit une partition d’un type τ donné en un chapeau d’opérateurs de sortes et le reste — l’ensemble des aliens — les soustermes (de type) qui ne commence pas par un opérateur de sortes. Pour un type de premier ordre clos ρ ∈ T (S), cap(ρ) = ρ et aliens(ρ) = ∅.

Le lemme qui suit montre que dans une partition pareille de chaque terme clos t : τ en forme normale — en chapeau maximale de constructeurs et les autres sous-termes — les types de ces derniers appartiennent dans aliens(τ). Pour faciliter la formulation, on va écrire Types(A) pour dénoter l’ensemble des types des termes d’un ensemble A donné.

Lemme 4.4.5 Soit R un système de réécriture, qui définit tout ses symboles d’une façon localement complète. Soit t un terme clos de type τ. Si t est une forme normale, alors il existe un terme t′ et une substitution γ tels que t = t′γ pour t′ ∈ T (C, X), Types(FV (t′)) ⊆ aliens(τ).

Preuve. Par récurrence sur la construction de t :

– Si τ ne commence pas par un opérateur de sorte, alors cap(τ) = α, aliens(τ) = {τ}, et alors t = x^{τ} {x ↦ t}.

– Si τ commence par un opérateur de sorte, alors τ = s(\overline{τ}), pour s ∈ S. Alors t ne contient pas de sous-terme clos f(t_{1}, …, t_{m}) pour f ∈ D, parce que vue la condition de complétude locale de f et le fait que t_{1}, …, t_{m} sont dans la forme normale, chaque sous-terme de cette forme serait réductible. Si t = t_{1}(t_{2}) ou t = t_{1}τ′, alors par la proposition 4.4.3 et la dernière remarque, t contient un redex, ce qui est impossible. Donc forcément t = c(t_{1}, …, t_{m}) pour c ∈ C, c : ρ_{1}(\overline{α}) × ⋯ × ρ_{m}(\overline{α}) → s(\overline{α}). Les sous-termes t_{i} ont des types ρ_{i}(\overline{τ}) et comme ρ_{i} ∈ T (S, Φ), alors aliens(ρ_{i}(\overline{τ})) ⊆ aliens(s(\overline{τ})) = aliens(τ). Donc puisque les t_{i} sont en la forme normale, on a t_{i} = t′_{i}γ_{i} pour Types(FV (t′_{i})) ⊆ aliens(ρ_{i}(\overline{τ})). Soit maintenant t′ = c(t′_{1}, …, t′_{m}), γ = γ_{1} ∪ … ∪ γ_{n} (on renomme les variables libres dans t′_{i} en cas de conflit), et t = t′γ pour Types(FV (t′)) ⊆ aliens(τ), donc on obtient le résultat. □

On prouve maintenant facilement le théorème de complétude de systèmes convergents.

Théorème 4 (théorème de complétude)

Soit R un système de réécriture d’ordre supérieur convergent. R définit tous les symboles f ∈ D d’une façon localement complète si et seulement si R est globalement complet.

Preuve. La preuve dans un sens est, comme toujours, évidente, et dans l’autre sens est une simple conséquence du lemme précédent, puisque pour un terme t de type de base τ, aliens(τ) = ∅ et alors t = t′ et la substitution γ est une fonction vide. Donc comme chaque terme possède une forme normale, et comme cette forme normale est un terme constructeur, on prouve le théorème. □

4.5 Vérification de complétude

Pour les types polymorphes on va étudier seulement l’approche classique sur les arguments fonctionnels. Le deuxième type d’arguments dont on ne trouve pas dans la discipline de types simples, les arguments de types universellement quantifiés, vont être traités de la même manière.

Définition 4.5.1 (système classique)

Le système de réécriture algébrique R = {l_{i} → r_{i}} de termes polymorphes est classique si les membres gauches l_{i} sont de la forme f(t_{1}, …, t_{n}) pour f ∈ D, f : τ_{1} × ⋯ × τ_{n} → τ, les termes t_{i} : τ_{i} et si s : ρ est un sous-terme d’un t_{i} (pas nécessairement propre) tel que ρ ≠ s(\overline{ρ}) pour aucun s ∈ S, alors s est une variable linéaire.

À cause de cette restriction sur le système de règles, on peut utiliser la définition 2.4.1 de la variable d’induction présenté dans la section consacrée au premier ordre. L’unification qui apparaît dans cette définition doit prendre en compte aussi les types qui doivent s’unifier.

Puisque les sous-termes des membres gauches d’autres types sont des variable linéaires, seules les variables dont les types commencent par un symbole s ∈ S peuvent être des variables d’induction. Il suffit donc la définition de l’ensemble couvrant suivant

Définition 4.5.2 (ensemble couvrant)

Soit t = f(u_{1}, …, u_{n}) pour f ∈ D, f : τ_{1}×⋯×τ_{n} → τ et u_{1}, …, u_{n} ∈ T (C, X), u_{i} : τ_{i} Soit p une position de variable d’induction x^{τ} dans t. Un ensemble fini de termes non-variables CS est un ensemble couvrant de x^{τ} dans t ssi pour toute substitution σ telle que u_{i}σ ∈ T (C, X), u_{i}σ : τ_{i} et F V (u_{i}σ) ∩ X_{S} = ∅, il existe un terme v ∈ CS et une substitution σ̂ tels que tσ = t[v]_{p}σ̂.

Dans la procédure de vérification on va utiliser l’ensemble couvrant qui est une légère généralisation du petit ensemble couvrant. Pour une variable d’induction de type s(\overline{τ}), on définit

Proposition 4.5.3 (ensemble couvrant polymorphe)

Un ensemble couvrant polymorphe CS_{∀}(s(\overline{τ})) contient tous les termes de la forme

c(x_{1}, …, x_{m}) pour c : ρ_{1}(\overline{α}) × ⋯ × ρ_{m}(\overline{α}) → s(\overline{α})

ou les variables x_{1}, …, x_{m} sont des nouvelles variables de types x_{i} : ρ_{i}(\overline{τ}). CS_{∀}(s(\overline{τ})) est un ensemble couvrant d’une variable d’induction x : s(\overline{τ}).

Preuve. Soient t et σ comme dans la définition de l’ensemble couvrant et p une position dans t d’une variable d’induction x : s(\overline{τ}). Le terme tσ doit être de la forme c(t_{1}, …, t_{m}) pour c constructeur de type de sortie s(\overline{τ}), qui est élément de CS_{∀}(s(\overline{τ})). On pose x_{i}σ̂ = t_{i} et pour les autres variables yσ̂ = yσ. On a certainement tσ = t[c(x_{1}, …, x_{m}]_{p}σ̂. □

La preuve de correction de la réponse positive de la procédure nécessite une proposition supplémentaire, qui dit qu’un terme de type τ = ρσ_{T} qui a des constructeurs jusqu’aux sous-termes qui ne sont pas du premier ordre est une instance de type et de terme d’un terme de type ρ qui, lui aussi, a des constructeurs le plus loin possible.

Proposition 4.5.4 Soit t un terme de type τ = ρσ_{T} pour une substitution de type σ_{T}. Si t = t′σ pour une substitution σ, t′ ∈ T (C, X) avec F V (t′) ∩ X_{S} = ∅, alors il existe un terme t′′ : ρ tel que t′′ ∈ T (C, X), F V (t′′) ∩ X_{S} = ∅ et une substitution γ tels que t = t′′σ_{T} γ.

Preuve. On procède par récurrence sur la construction de t. Si ρ = α est une variable de type ou bien ρ = ρ_{1} → ρ_{2} ou bien ρ = ∀α.ρ′ alors on pose t′′ = x^{ρ}, γ = {x^{τ} ↦ t}, et on obtient t′′σ_{T} γ = x^{ρ}γ = t, {x^{ρ}}∩X_{S} = ∅, pour t′′ ∈ T (C, X).

Si ρ = s(\overline{ξ}), pour s ∈ S, alors τ = s(\overline{ξσ_{T}}), et t = c(t_{1}, …, t_{m}) pour un constructeur c : ι_{1}(\overline{α}) × ⋯ × ι_{m}(\overline{α}) → s(\overline{α}). Certainement t_{i} : ι_{i}(\overline{ξ})σ_{T}, t_{i} = t′_{i}σ_{i} pour t′_{i} ∈ T (C, X), F V (t′_{i}) ∩ X_{S} = ∅.

Donc par hypothèse de récurrence t_{i} = t′′_{i}σ_{T} γ_{i} pour t′′_{i} ∈ T (C, X), t′′_{i} : ι_{i}(\overline{ξ}), F V (t′′_{i}) ∩ X_{S} = ∅. Si on prend t′′ = c(t′′_{1}, …, t′′_{m}), γ = γ_{1} ∪ … ∪ γ_{m} (en cas de conflit on change des noms de variables dans t′′_{i}), on obtient t′′ : s(\overline{ξ}) = ρ, t′′ ∈ T (C, X), F V (t′′) ∩ X_{S} = ∅ et t′′σ_{T} γ = c(t′′_{1}, …, t′′_{m})σ_{T} γ = c(t′′_{1}σ_{T} γ, …, t′′_{m}σ_{T} γ) = t. □

On peut maintenant prouver la correction de la procédure de vérification.

Lemme 4.5.5 Soit R un système classique. Si la procédure, lancée pour un symbole f ∈ D donné, f : τ_{1} × ⋯ × τ_{n} → τ retourne un succès, alors R définit f d’une façon localement complète.

Preuve. D’après la définition de l’ensemble couvrant et la réductibilité de toutes les feuilles par la procédure, tout terme de la forme f(t_{1}, … t_{n}) pour t_{i} : τ_{i}, t_{i} ∈ T (C, X), F V (t_{i}) ∩ X_{S} est réductible par R.

Soit f(u_{1}, …, u_{n}) une instance close de f(x_{1}, …, x_{m}) telle que pour tout i, u_{i} : τ_{i}σ_{T} pour une substitution de types σ_{T}, u_{i} = u′_{i}σ_{i} pour u′_{i} ∈ T (C, X), F V (u′_{i}) ∩ X_{S} = ∅, comme dans la définition de la complétude locale.

Selon le lemme précédent pour chaque i, il existe un terme u′′_{i} tel que u′′_{i} ∈ T (C, X), F V (u′′_{i}) ∩ X_{S} = ∅ et une substitution γ_{i} tels que u_{i} = u′′_{i}σ_{T} γ_{i}. Soit γ = γ_{1} ∪ … ∪ γ_{n} (au cas de conflit on change des noms de variables dans u′′_{i}). Alors le terme f(u_{1}, …, u_{n}) est une instance du terme f(u′′_{1}, …, u′′_{n}) avec les substitutions σ_{T} γ, donc c’est une instance d’un terme réductible. □

La preuve de terminaison de la procédure de vérification peut être faite de la même façon que d’habitude, puisque chaque utilisation de l’ensemble couvrant polymorphe par la règle (décompose), remplace un terme de l’ensemble de nœuds par des autres où il y a un constructeur ajouté dans chaque terme. On a donc, grâce au théorème 4, un outil de preuve de complétude de systèmes de réécriture classiques.

5 Conclusions

On a présenté dans ce travail une adaptation de la notion de complétude de systèmes de réécriture à des systèmes d’ordre supérieur. Les systèmes considérés utilisent une signature divisée en deux parties disjointes : l’ensemble de constructeurs libres du premier ordre et l’ensemble des fonctions définies. On décrit une procédure qui, pour un symbole de fonction donné, vérifie si sa définition par des règles de réécriture couvre l’ensemble de tous ses arguments possibles. On démontre que lorsque cette dernière propriété est vraie pour toutes les fonctions du système, le système lui même est complet.

Deux disciplines de types sont étudiées dans ce travail : les types simples et les types polymorphes. La problématique de complétude de la réécriture typée par d’autres système de typage, par exemple les types dépendants ou le calcul de construction, nécessite un travail supplémentaire.

Pour les types simples, on présente trois approches de traitement des arguments fonctionnels. L’approche non-standard, étudiée dans la section 3.8, constitue un essai de permettre dans les définitions de fonctions l’utilisation du filtrage d’ordre supérieur pour les arguments de certains types fonctionnels, tout en préservant la modularité de la complétude du système. Ces types fonctionnels sont décrits d’une façon syntaxique ce qui provoque de multiples complications. On peut espérer que dans une discipline de types plus riche, on puisse trouver un moyen sémantique de décrire les types fonctionnels, pour lesquels l’utilisation du filtrage d’ordre supérieur n’empêcherait pas la modularité de la complétude.

Une autre extension possible de ce travail consiste à considérer les systèmes où les constructeurs ne sont pas libres, comme par exemple dans la spécification des entiers relatifs, pred(succ(x)) → x. Les notions de complétude présentées dans ce mémoire peuvent être facilement généralisées pour ce type de systèmes. Par contre la généralisation devient plus compliquée si on enlève la condition que les constructeurs soient du premier ordre. Un exemple pratique où les constructeurs ont les types d’ordre supérieur est le système qui décrit les formules logiques de premier ordre, avec des constructeurs ∀, ∃ : (terme → formule) → formule, où la formule ∀x.Φ(x) est représentée par le terme ∀(λx.Φ(x)).

La technique utilisée pour tester la complétude de définitions de fonctions est celle des arbres de motifs, adaptée de [1, 2]. Une généralisation très intéressante, du point de vue de l’application de la réécriture comme moyen de spécifier des systèmes informatiques, serait de considérer les règles conditionnelles d’ordre supérieur. On pourrait également considérer l’utilisation d’autres moyens de preuve de réductibilité close, par exemple la technique d’automates d’arbres, ou la technique de la résolution de formules quantifiées sur le λ-termes étudiés par Lugiez [12] dans le cadre de types simples.

Références

[1] Adel Bouhoula. Using Induction and Rewriting to Verify and Complete Parameterized Specifications. Theoretical Computer Science, 170, 1996. To appear.

[2] Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. Technical report, SRI-CSL, 1996. http ://www.loria.fr/ bouhoula.html, //www.lri.fr/people/jouannau.html.

[3] Jaco Van de Pol. Termination of Higher-Order Rewrite Systems. Phd thesis, Utrecht University, Utrecht, Netherlands, 1996.

[4] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.

[5] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[6] Warren D. Goldfarb. Note on the undecidability of the second-order unification problem. In Theoretical Computer Science, pages 225–230, 1981.

[7] John V. Guttag and James J. Horning. The algebraic specification of abstract data types. Acta Informatica, 10(1), 1978.

[8] Jean-Pierre Jouannaud and Mitsuhiro Okada. Abstract data type systems. Theoretical Computer Science, 173(2) :349–391, February 1997.

[9] Jean-Pierre Jouannaud and Albert Rubio. A recursive path ordering for higher-order terms in η-long β-normal form. In Ganzinger H., editor, Proc. 7th Rewriting Techniques and Applications, New-Jersey, LNCS 1103. Springer-Verlag, 1996.

[10] Emmanuel Kounalis. Completeness in data type specifications. In Proc. EUROCAL 85, Linz, LNCS 204, pages 348–362. Springer-Verlag, April 1985.

[11] C. Loría-Sáenz and J. Steinbach. Termination of combined (rewrite and λ-calculus) systems. In Proc. 3rd Int. Workshop on Conditional Term Rewriting Systems, Pont-à-Mousson, LNCS 656, volume 656 of Lecture Notes in Computer Science, pages 143–147. Springer-Verlag, 1992.

[12] D. Lugiez. Positive and negative results for higher-order disunification. Journal of Symbolic Computation, 20 :431–470, 1995.

[13] P. Lincoln M. Clavel, S. Eker and J. Meseguer. Principles of maude. In J. Meseguer, editor, Proceedings of the 1st International Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science 4, 1996.

[14] D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In P. Schroeder-Heister, editor, Extensions of Logic Programming. LNCS 475, Springer Verlag, 1991.

[15] T. Nipkow. Higher order critical pairs. In Proc. IEEE Symp. on Logic in Comp. Science, Amsterdam, 1991.

[16] Zhenyu Qian. Linear unification of higher-order patterns. In TAP-SOFT’93 : Theory and Practice of Software Development, volume 668 of Lecture Notes in Computer Science, pages 391–405. Springer-Verlag, 1993.

[17] J.-J. Thiel. Stop loosing sleep over incomplete specifications. In Proc. 11th ACM Symp. on Principles of Programming Languages, Salt Lake City, 1984.

Table des matières

1 Introduction 1 Complétude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Systèmes de réécriture d’ordre supérieur . . . . . . . . . . . . . . 2 Complétude de systèmes de réécriture d’ordre supérieur . . . . . 3

2 Premier ordre 5 2.1 Types et termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Réécriture du premier ordre . . . . . . . . . . . . . . . . . . . . . 6 2.3 Complétude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.4 Procédure de vérification . . . . . . . . . . . . . . . . . . . . . . . 7 2.5 Correction de la procédure de vérification . . . . . . . . . . . . . 10

3 Ordre supérieur : types simples 12 3.1 Types et termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.2 Forme β-normale η-expansée . . . . . . . . . . . . . . . . . . . . 13 3.3 Réécriture d’ordre supérieur de termes normalisés . . . . . . . . . 14 3.4 Complétude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.5 Procédure de vérification . . . . . . . . . . . . . . . . . . . . . . . 16 3.6 Approche classique sur les arguments fonctionnels . . . . . . . . 17 3.7 Approche moins restrictive . . . . . . . . . . . . . . . . . . . . . 19 3.8 Nouvelle approche : << fonctions à syntaxe limitée >> . . . . . 21

3.8.1 Extension du système de types . . . . . . . . . . . . . . . 22 3.8.2 Nouvelles règles de typage . . . . . . . . . . . . . . . . . . 23 3.8.3 Complétude . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.8.4 Vérification de complétude . . . . . . . . . . . . . . . . . 27 3.8.5 Conditions sur des règles de réécriture . . . . . . . . . . . 29

4 Ordre supérieur : types polymorphes 31 4.1 Types polymorphes . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4.2 Termes du λ-calcul polymorphe . . . . . . . . . . . . . . . . . . . 31 4.3 Réécriture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4.4 Complétude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 4.5 Vérification de complétude . . . . . . . . . . . . . . . . . . . . . . 35

5 Conclusions 38