Réécriture (informatique)

Pour les articles homonymes, voir Réécriture.

La réécriture (ou récriture) est un modèle de calcul utilisé en informatique, en algèbre, en logique mathématique et en linguistique. Il s’agit de transformer des objets syntaxiques (mots, termes, lambda-termes, programmes, preuves, graphes, …) en appliquant des règles bien précises. Voici quelques exemples classiques d’utilisation de la réécriture :

• simplifier une expression algébrique (calcul formel),
• définir la grammaire formelle d’un langage de programmation ou d’une langue naturelle (analyse syntaxique),
• exprimer la sémantique d’un langage de programmation (sémantique opérationnelle),
• étudier la structure d’un groupe ou d’un monoïde (algèbre combinatoire),
• expliciter le contenu calculatoire d’une démonstration mathématique par le mécanisme d’élimination des coupures (théorie de la démonstration).

On peut aussi mentionner des applications très pratiques telles que la gestion des courriers électroniques (dans le logiciel sendmail les entêtes de courrier sont manipulées par des systèmes de réécriture) ou l'optimisation de code dans les compilateurs.

Systèmes de réécriture

Un système de réécriture est un ensemble de règles de réécriture de la forme r → r’. Une telle règle s’applique à l’objet syntaxique t si celui-ci contient une instance du membre gauche r, c’est-à-dire un sous-objet que l’on peut identifier à r. L’objet t se réécrit alors en un nouvel objet t’, obtenu en remplaçant l’instance de r par l’instance du membre droit r’ correspondante. Notation : t → t’.

On va expliciter ce principe général dans chacun des trois cadres classiques de la réécriture.

Réécriture de mots

• les objets sont des mots construits à partir d’un alphabet Σ = {a, b, c, …} ;
• une règle r → r’ est constituée de deux mots r et r’. En général, on exige que le membre gauche r soit non vide. Exemple : ab → caa.

Une telle règle s’applique au mot t si celui-ci est de la forme urv où u et v sont des mots quelconques (éventuellement vides). Le mot t se réécrit alors en ur’v. Autrement dit, on applique la règle r → r’ dans le contexte formé du préfixe u et du suffixe v. Exemple : pour u = a et v = bc, on obtient aabbc → acaabc.

Réécriture de termes

• les objets sont des termes du premier ordre, c’est-à-dire des expressions construites à partir d’une signature constituée de constantes et de symboles d’opérations. Exemple : 0,1,+, · (deux constantes et deux opérations binaires, avec la convention habituelle de précédence du produit · sur la somme +). On utilise aussi des variables x, y, z, … ;
• une règle r → r’ est constituée de deux termes r et r’. En général, on exige que le membre gauche r ne soit pas une variable et que toutes les variables de r’ apparaissent déjà dans r. Exemple : x · (y + z) → x · y + x · z.

Une instance du membre gauche est un sous-terme s obtenu en remplaçant les variables de r par des termes quelconques. L’instance correspondante du membre droit s’obtient en remplaçant les variables de r’ par ces mêmes termes. Exemple : (x + 0) · (x + 1) est une instance de x · (y + z) et l’instance correspondante de x · y + x · z est (x + 0) · x + (x + 0) · 1. On a donc (x + 0) · (x + 1) → (x + 0) · x + (x + 0) · 1, et aussi ((x + 0) · (x + 1)) + y → ((x + 0) · x + (x + 0) · 1) + y.

Remarque : si la signature est uniquement constituée de symboles d’opérations unaires, alors chaque règle contient une seule variable, qui apparaît une fois à gauche et une fois à droite. Exemple : a(b(x)) → c(a(a(x))). Ainsi, la réécriture de mots peut être considérée comme un cas particulier de la réécriture de termes.

Lambda-calcul

• les objets sont des expressions construites à partir des variables x, y, z, … en utilisant l’application u v et l’abstraction λx·u (où x est une variable quelconque);
• la règle principale est la β-réduction : (λx·u) v → u[x := v] où u[x := v] est le terme u dans lequel toutes les occurrences de x ont été remplacées par v.

Le lambda-calcul est à la fois un modèle de la calculabilité, le prototype de tous les langages de programmation fonctionnels, et la version non typée de l’élimination des coupures pour la déduction naturelle. En fait, c’est un cas particulier de réécriture de termes du second ordre. La principale différence avec le cadre précédent est que les termes contiennent des variables liées qui rendent le mécanisme de substitution plus subtil.

Terminaison

Article détaillé : Terminaison d'un système de réécriture.

Notation : si t₀ → t₁ → t₂ → ··· → t_n, on écrit t₀ →* t_n. Autrement dit, →* est la clôture réflexive et transitive de →.

Définition : si aucune règle ne s’applique à t, on dit que t est irréductible ou en forme normale, et si t →* u où u est en forme normale, on dit que u est une forme normale de t.

On dit qu’un système de réécriture est noetherien, ou qu’il satisfait la propriété de terminaison, s’il n’existe aucune chaîne infinie t₀ → t₁ → t₂ → ··· → t_n → ···

Exemples (réécriture de mots) :

• le système formé de l’unique règle a → ab n’est pas noetherien, car il existe une chaîne infinie a → ab → abb → abbb → ··· ;
• le système formé des deux règles a → b et b → a n’est pas noetherien, car il existe une chaîne infinie a → b → a → b → ··· ;
• le système formé de l’unique règle ab → a est noetherien, car la longueur d’un mot diminue à chaque étape de réécriture ;
• le système formé de l’unique règle ab → caa est noetherien, car le nombre d’occurrences de b diminue à chaque étape.

En général, la propriété de terminaison se démontre en construisant un ordre de terminaison, c’est-à-dire un ordre strict bien fondé < tel que t → t’ implique t > t’.

Dans le cas noetherien, tout objet a une forme normale. De plus, on a un principe de récurrence noetherienne : si pour tout t, on peut démontrer la propriété P(t) en supposant P(t’) pour tout t’ tel que t → t’, alors on a P(t) pour tout t.

Remarque : la propriété de terminaison pour un système (fini) de réécriture de mots est un problème indécidable. Il est de même pour l'absence de cycles.

Terminologie : La terminaison est parfois aussi appelée forte normalisation en lambda calcul par exemple.

Confluence

La nature non-déterministe de la réécriture fait qu’on peut appliquer plusieurs règles au même objet, obtenant ainsi plusieurs résultats différents.

Pour un système de réécriture donné, la propriété de confluence, aussi appelée propriété du diamant, s’énonce ainsi : si t →* u et t →* v, alors il existe w tel que u →* w et v →* w. Elle équivaut à la propriété de Church-Rosser.

Exemples (réécriture de mots) :

• le système formé des deux règles ab → a et ba → b n’est pas confluent, car on a aba → aa et aba → ab → a, et les mots aa et a sont en forme normale ;
• le système formé des deux règles ab → ε et ba → ε (où ε est le mot vide) est confluent (voir ci-dessous).

Dans le cas noetherien, la propriété de confluence équivaut à la propriété de confluence locale, aussi appelée confluence faible : si t → u et t → v, alors il existe w tel que u →* w et v →* w.

Un système de réécriture qui vérifie à la fois la propriété de terminaison et la propriété de confluence est dit convergent. Dans ce cas, on a l’existence et l’unicité de la forme normale, si bien que le problème du mot est décidable, du moins si le système est fini.

Remarque : dans le cas noetherien, la propriété de confluence pour un système (fini) de réécriture de mots ou de termes est un problème décidable. Il suffit en effet de tester la confluence d’un nombre fini de configurations appelées paires critiques. Par exemple, dans le cas du système formé des deux règles ab → ε et ba → ε, il suffit de vérifier la propriété de confluence locale pour les mots aba et bab. Ces paires critiques sont analogues aux bases de Gröbner utilisées en algèbre commutative.

Si un système de réécriture est noetherien, mais pas confluent, on essaie de le rendre convergent en utilisant l’algorithme de complétion de Knuth-Bendix.

Invariants homologiques

Dans le cas de la réécriture de mots, un système de réécriture définit une présentation par générateurs et relations d‘un monoïde. Ce monoïde est le quotient Σ*/↔*, où Σ* est le monoide libre engendré par l’alphabet Σ et ↔* est la congruence engendrée par les règles de réécriture, c’est-à-dire la clôture réflexive, symétrique et transitive de →. Exemple : Z = Σ*/↔* où Σ = {a, b} avec les deux règles ab → ε et ba → ε (groupe libre à un générateur).

Comme un monoïde M a beaucoup de présentations, on s’intéressent aux invariants, c’est-à-dire aux propriétés intrinsèques du monoïde M, qui ne dépendent pas du choix de la présentation. Exemple : la décidabilité du problème du mot pour M.

Un monoïde finiment présentable M peut avoir un problème du mot décidable, mais aucune présentation par un système de réécriture convergent fini. En effet, s’il existe un tel système, le groupe d’homologie H₃(M) est de type fini. Or on peut construire un monoïde finiment présentable dont le problème du mot est décidable et tel que le groupe H₃(M) n’est pas de type fini.

En fait, ce groupe est engendré par les paires critiques, et plus généralement, un système de réécriture convergent permet de calculer l’homologie du monoïde en toute dimension. Il y a aussi des invariants homotopiques : s’il existe un système de réécriture convergent pour un monoïde, on montre que celui-ci a un type de dérivation fini. Il s’agit à nouveau d’une propriété qui se définit à partir d’une présentation (finie), mais qui ne dépend pas du choix de cette présentation. Cette propriété implique que le groupe H₃(M) est de type fini, mais la réciproque n’est pas vraie.

Dimension supérieure

Un mot tel que aabbc peut être interprété comme un chemin dans le graphe composé d’un seul sommet, avec une arête pour chaque symbole a, b, c. Si on part d’un graphe quelconque, on obtient une catégorie plutôt qu’un monoïde. Un calcul tel que aabbc → acaabc → acacaac peut alors être interprété comme un chemin entre chemins, aussi appelé 2-chemin :

Cette remarque suggère une généralisation de la réécriture de mots où les objets sont des 2-chemins, que l’on peut aussi représenter par des diagrammes planaires :

Il se trouve que la réécriture de termes peut se traduire dans un tel système, à condition d’introduire des opérations explicites de duplication, d’effacement et d’échange (analogues aux règles structurelles du calcul des séquents) :

Mais cette approche est bien plus générale que la réécriture de termes. Voici quelques domaines où un tel formalisme peut être utilisé :

• circuits booléens classiques et quantiques ;
• théorie des tresses et des nœuds ;
• diagrammes de Feynman et diagrammes de Penrose ;
• algèbres de Hopf et groupes quantiques ;
• réseaux de preuve de la logique linéaire et réseaux d’interaction.

Enfin, on peut considérer la réécriture de n-chemins, qui consiste à construire des n+1-chemins. Pour cela, on utilise la théorie des catégories et des polygraphes (aussi appelés computades), qui établit un pont entre la théorie du calcul et la topologie algébrique.

Implantation

Le premier langage fondé sur la réécriture est Hope, dû à Burstall, McQueen et Sanella^[1], quoiqu'on puisse lui trouver deux ancêtres dans les travaux de Burge^[2] et d'O'Donnell^[3]. Depuis, plusieurs langages de programmation ont pris pour mécanisme interne la réécriture, parmi lesquels ASF+SDF, ELAN, Maude, Stratego et Tom. Ce dernier est intéressant parce qu'il mélange des constructions venant de la réécriture avec le langage Java.
Bien qu'appartenant à la catégorie des langages fonctionnels, Objective Caml repose également sur un principe de base de la réécriture : le filtrage de motif.

Références

1. ↑ Rod M. Burstall, David B. MacQueen, Donald Sannella: HOPE: An Experimental Applicative Language. 136-143, The 1980 LISP Conference
2. ↑ W. Burge. Recursive Programming Techniques. Addison Wesley 1975.
3. ↑ Michael J. O'Donnell: Computing in Systems Described by Equations, Springer 1977.

Bibliographie

• (en) Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, 2003 (ISBN 0521391156)
• (en) Franz Baader and Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1998 (ISBN 0521779200)

Liens externes

• (en) The rewriting homepage