Réécriture (informatique) - Définition et Explications

Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

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 (Un langage de programmation est un langage informatique, permettant à un être humain d'écrire un code source qui sera analysé par une machine, généralement un ordinateur. Le code source subit ensuite une...) ou d’une langue naturelle (analyse syntaxique),
  • exprimer la sémantique d’un langage de programmation (La programmation dans le domaine informatique est l'ensemble des activités qui permettent l'écriture des programmes informatiques. C'est une étape importante de la conception de logiciel (voire de matériel, cf. VHDL).) (sémantique opérationnelle),
  • étudier la structure d’un groupe ou d’un monoïde (algèbre (L'algèbre, mot d'origine arabe al-jabr (الجبر), est la branche des mathématiques qui étudie, d'une façon générale, les structures algébriques.) combinatoire (En mathématiques, la combinatoire, appelée aussi analyse combinatoire, étudie les configurations de collections finies d'objets ou les combinaisons d'ensembles finis, et les...)),
  • expliciter le contenu calculatoire d’une démonstration (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment démontrées à partir de propositions initiales, en...) 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 (En informatique, un logiciel est un ensemble d'informations relatives à des traitements effectués automatiquement par un appareil informatique. Y sont inclus les instructions de traitement, regroupées sous forme de...) sendmail les entêtes de courrier sont manipulées par des systèmes de réécriture) ou l'optimisation de code (En programmation informatique, l'optimisation est la pratique qui consiste généralement à réduire le temps d'exécution d'une fonction, l'espace occupé par les...) dans les compilateurs

Systèmes de réécriture

Un système de réécriture est un ensemble (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui peut être comprise comme un tout », comme...) 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 (De manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois dimensions, qui a une fonction...) 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 (Le vide est ordinairement défini comme l'absence de matière dans une zone spatiale.). Exemple : ab → caa.

Une telle règle s’applique au mot t si celui-ci est de la forme urvu 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 (En mathématiques et en logique, une variable est représentée par un symbole. Elle est utilisée pour marquer un rôle dans une formule, un prédicat ou un algorithme. En statistiques, une variable peut aussi...) 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 (Le lambda-calcul (ou λ-calcul) est un langage de programmation théorique inventé par Alonzo Church dans les années 1930. Ce langage a été le premier utilisé pour...)

  • 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]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é (La théorie de la calculabilité (appelée aussi parfois théorie de la récursion) est une branche de la logique mathématique et de l'informatique théorique....), 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 (La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons naturelles de raisonner). 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.

Page générée en 0.169 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique