Réécriture (informatique) - Définition

Introduction

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ême 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.