Réécriture (informatique)

En informatique théorique, la réécriture (ou récriture[1]) 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.

Pour les articles homonymes, voir Réécriture.

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[2]) ou la génération et l'optimisation de code dans les compilateurs[3].

Exemples

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

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 t0 → t1 → t2 → ··· → tn, on écrit t0 →* tn. 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 t0 → t1 → t2 → ··· → tn → ···

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(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é :

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[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.

Références
  1. Pour une discussion voir Éric Bordas, « Récriture, Réécriture », in Le Dictionnaire du littéraire pp. 519-520 et Yuko Rokukawa Écriture de la pureté dans l'œuvre d'Anatole France, note 1363, p. 211. et Magdalena Wandzioch (dir.), Quelques aspects de la réécriture, Wydawnictwo Uniwersytetu Ślą1skiego, (lire en ligne)
  2. (en) « Linux Network Administrator's Guide, 2nd Edition Linux Network Administrator's Guide, 2nd Edition. Chapter 18ː Sendmail. »
  3. Alexander Meduna Elements of Compiler Design, Auerbach Publications (2007), p. 15
  4. Alexander Meduna Elements of Compiler Design, Auerbach Publications (2007), p. 23
  5. (en) Terese, Term rewriting systems
  6. Rod M. Burstall, David B. MacQueen, Donald Sannella, HOPE: An Experimental Applicative Language, 136-143, The 1980 LISP Conference.
  7. W. Burge, Recursive Programming Techniques, Addison Wesley 1975.
  8. 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 et Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1998 (ISBN 0521779200)
  • (en) Nachum Dershowitz et Jean-Pierre Jouannaud Rewrite systems, publié dans Handbook of theoretical computer science (vol. B) Pages 243 - 320 MIT Press Cambridge, MA, USA ©1990 (ISBN 0-444-88074-7)
  • (en) 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, no 6,‎ , p. 433-452.
  • Michel Latteux et Yves Roos, « On prefixal one-rule string rewrite systems », Theoretical Computer Science, vol. 795,‎ , p. 240–256 (ISSN 0304-3975, DOI 10.1016/j.tcs.2019.07.004).

Voir aussi

Articles connexes

Liens externes

(en) Rewriting Home Page

  • Portail des mathématiques
  • Portail de la logique
  • Portail de l’informatique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.