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. 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ù x2 = 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.