Réécriture (informatique)

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[4] 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[5].
• 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[5].
• 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.

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.

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.

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.

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${\displaystyle {}_{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${\displaystyle {}_{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${\displaystyle {}_{3}}$(M) est de type fini, mais la réciproque n’est pas vraie.

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.

Le premier langage fondé sur la réécriture est Hope, dû à Burstall, McQueen et Sanella[6], quoiqu'on puisse lui trouver deux ancêtres dans les travaux de Burge[7] et d'O'Donnell[8]. 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, 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.

• 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)