Réécriture (informatique)

En informatique théorique, la réécriture (ou récriture) est un modèle de calcul dans lequel il s’agit de transformer des objets syntaxiques (mots, termes, lambda-termes, programmes, preuves, graphes, etc.) en appliquant des règles bien précises.

La réécriture est utilisée en informatique, en algèbre, en logique mathématique et en linguistique. La réécriture est utilisée en pratique pour 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 la génération et l'optimisation de code dans les compilateurs.

Exemples

Voici quelques exemples classiques d’utilisation de la réécriture :

• simplifier une expression algébrique (calcul formel) ; x+1+x+1 → x+x+1+1 → 2x+ 1+1→ 2x+ 2
• une grammaire formelle d’un langage de programmation ou d’une langue naturelle est un système de réécriture ; PHRASE → SUJET VERBE → DETERMINANT NOM VERBE → Le NOM VERBE → Le chat VERBE → Le chat dort
• exprimer la sémantique d’un langage de programmation (sémantique opérationnelle) ;
• étudier la structure d’un groupe ou d’un monoïde (combinatoire algébrique) ;
• en théorie des automates, l'exécution d'un automate (automate fini, automate à pile, machine de Turing) sur un mot d'entrée peut être vue comme une réécriture. Par exemple, Alexander Meduna présente les automates comme des systèmes de réécriture ;
• expliciter le contenu calculatoire d’une démonstration mathématique par le mécanisme d’élimination des coupures (théorie de la démonstration) ;
• en théorie des nœuds, les mouvements de Reidemeister sont des règles de réécriture pour dénouer un nœud.
• en logique propositionnelle classique, une formule est une tautologie si elle peut se réécrire en le terme 1 avec des règles de réécriture qui exploitent l'équivalence entre algèbre booléennes et anneaux où x² = x.
• en biologie, les systèmes de Lindenmayer modélisent l'évolution de plantes, de bactéries, etc.
• pour expliquer la théorie des fonctions avec le minimum de concepts, c'est la logique combinatoire.

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 libres de x ont été remplacées par des occurrences de 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

Notation : si t₀ → t₁ → t₂ → ··· → t_n, on écrit t₀ →* t_n. Autrement dit, →* est la clôture réflexive 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 noethérien, ou qu’il satisfait la propriété de terminaison, s’il n’existe aucune suite 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 noethérien, 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 noethérien, car il existe une chaîne infinie a → b → a → b → ··· ;
• le système formé de l’unique règle ab → a est noethérien, car la longueur d’un mot diminue à chaque étape de réécriture ;
• le système formé de l’unique règle ab → caa est noethérien, 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 noethérien, tout objet a une forme normale. De plus, on a un principe de récurrence noethérienne : si pour tout t, la propriété P(t) est vraie chaque fois qu'on a P(t’) pour tous les t’ tels que t → t’, alors P(t) est vraie 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 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 noethérien, par le lemme de Newman, la confluence équivaut à la 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 se termine et est confluent 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 noethérien, 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 noethérien, mais pas confluent, on essaie de le rendre convergent en utilisant la procédure 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éresse 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${}_{3}$(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${}_{3}$(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${}_{3}$(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 preuves 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, quoiqu'on puisse lui trouver deux ancêtres dans les travaux de Burge et d'O'Donnell. 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 a l'intérêt de mélanger des constructions venant de la réécriture avec le langage Java.

Bien qu'appartenant à la catégorie des langages fonctionnels, Haskell et OCaml reposent également sur un principe de base de la réécriture : le filtrage de motif.

Le langage Wolfram, bien que permettant divers paradigmes de programmation, est fondamentalement un système de réécriture.

Bibliographie

• Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, 2003 (ISBN 0521391156)
• Franz Baader et Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1998 (ISBN 0521779200)
• Nachum Dershowitz et Jean-Pierre Jouannaud, « Rewrite systems », Handbook of theoretical computer science (vol. B), pages 243 - 320 MIT Press Cambridge, MA, USA ©1990 (ISBN 0-444-88074-7)
• Gérard Huet et Derek Oppen, Equations and Rewrite Rules, A Survey (1980) Stanford Verification Group, Report N° 15 Computer Science Department Report N° STAN-CS-80-785
• Jean-Pierre Jouannaud et Pierre Lescanne, « La Réécriture », Technique et Science Informatiques, vol. 5, n^o 6,‎ 1986, p. 433-452.

Articles récents

• Michel Latteux et Yves Roos, « On prefixal one-rule string rewrite systems », Theoretical Computer Science, vol. 795,‎ 2019, p. 240–256 (ISSN 0304-3975, DOI 10.1016/j.tcs.2019.07.004).
• Michel Latteux et Yves Roos, « On rationally controlled one-rule insertion systems », RAIRO - Theoretical Informatics and Applications, vol. 56,‎ 2022, article n^o 8 (31 pages) (DOI 10.1051/ita/2022008, lire en ligne)

Voir aussi

Articles connexes

• Grammaire générative et transformationnelle
• substitution explicite
• Système de Post
• Système de Thue
• Règles de réécriture

Liens externes

(en) Rewriting Home Page