Réécriture (informatique) - Définition

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, aussi appelée propriété du diamant, 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 noetherien, la propriété de confluence équivaut à la propriété de 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 vérifie à la fois la propriété de terminaison et la propriété de confluence 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 noetherien, 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 noetherien, mais pas confluent, on essaie de le rendre convergent en utilisant l’algorithme de complétion de Knuth-Bendix.

Terminaison

Notation : si t₀ → t₁ → t₂ → ··· → t_n, on écrit t₀ →* t_n. Autrement dit, →* est la clôture réflexive et 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 noetherien, ou qu’il satisfait la propriété de terminaison, s’il n’existe aucune chaîne infinie t₀ → t₁ → t₂ → ··· → t_n → ···

Exemples (réécriture de mots) :

• le système formé de l’unique règle a → ab n’est pas noetherien, 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 noetherien, car il existe une chaîne infinie a → b → a → b → ··· ;
• le système formé de l’unique règle ab → a est noetherien, car la longueur d’un mot diminue à chaque étape de réécriture ;
• le système formé de l’unique règle ab → caa est noetherien, 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 noetherien, tout objet a une forme normale. De plus, on a un principe de récurrence noetherienne : si pour tout t, on peut démontrer la propriété P(t) en supposant P(t’) pour tout t’ tel que t → t’, alors on a P(t) 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.