Réécriture (informatique) - Définition

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

• 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 preuve 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.

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éressent 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.