Paire critique

Le réécriture est un processus non déterministe[4], autrement dit un même terme peut se réécrire de plusieurs façons différentes ; parler de « la » forme irréductible d'un terme est donc ambigu et on doit plutôt parler d'« une » forme irréductible. Or on aimerait que le résultat de la réécriture soit unique[5] et que l'on puisse parler de « la » forme irréductible, appelée aussi forme normale, d'un terme, ce qui signifierait qu'il n'y ait qu'une forme irréductible d'un terme et que le résultat de la réécriture ne dépende pas de la manière dont les réécritures ont été activées ; c'est-à-dire qu'en partant d'un terme et en le récrivant de façon quelconque on arrive tôt ou tard au même terme. Un système de réécriture où il n'y a plus d'ambiguïté[6] dans la réécriture est dit confluent.

Donald Knuth a eu l'idée suivante : si on part d'un système de réécriture non confluent, on doit pouvoir mécaniquement le transformer en un système de réécriture équivalent[7] et confluent (voir procédure de complétion de Knuth-Bendix). L'idée repose sur la recherche d'« ambiguïtés minimales » que l'on appelle « paires critiques ».

À titre d'exemple, considérons les trois égalités, qui définissent les groupes et où * est la loi de composition interne, e est l'élément neutre et i(x) est l'inverse de x :

• x * e = x     (e est un élément neutre à droite) ;
• x * i(x) = e     (i(x) est un inverse à droite de x) ;
• (x * y) * z = x * (y * z)    (* est associative).

On peut naïvement les orienter en règle de réécriture :

• x * e → x ;
• x * i(x) → e ;
• (x * y) * z → x * (y * z).

mais on perd en pouvoir de démonstration des égalités. En particulier, on sait que l'on peut montrer à partir des axiomes égalitaires ci-dessus que e est un élément neutre à gauche (voir la démonstration ci-dessous) et que i(x) est un inverse à gauche de x, mais avec les trois règles ci-dessus on ne peut pas le démontrer par réécriture.

Schéma de la démonstration de x = e * x.

Pour démontrer x = e * x, qui dit que e est un élément neutre à gauche, on a besoin d'utiliser les trois égalités ci-dessus tantôt de gauche à droite tantôt de droite à gauche. Les trois termes (x * i(x)) * i(i(x)), (e * e) * i(i(x)) et e * (x * (i(x) * i(i(x)))) jouent un rôle particulier dans cette démonstration. Ce sont les trois termes qui se réécrivent de deux façons différentes. Ils correspondent à des configurations qu'il faut identifier. Mais ces configurations ne sont pas minimales. Les configurations minimales sont appelées des superpositions et sont calculées à partir du système de réécriture par unification de sous-termes des membres gauches de règles. Plus précisément :

• (x * i(x)) * i(i(x)) correspond à la superposition (x * i(x)) * y ;
• (e * e) * i(i(x)) correspond à la superposition (x * e) * y ;
• e * (x * (i(x) * i(i(x)))) correspond à la superposition x * (y * i(y)).

À partir de ces superpositions, on peut calculer des paires de termes :

• de la superposition (x * i(x)) * y, on obtient la paire <e * y, x * (i(x) * y)> ;
• de la superposition (x * e) * y, on obtient la paire <x * y, x * (e * y)> ;
• de la superposition x * (y * i(y)), on obtient la paire <(x * y) * i(y), x * e>.

Pour « compléter » un système de réécriture non convergent en un système de réécriture convergent, on peut ajouter des règles de réécriture pour rendre joignables les paires critiques, par exemple, les règles :

• x * (i(x) * y) → e * y ;
• x * (e * y) → x * y ;
• (x * y) * i(y) → x.

Mais l'introduction de nouvelles règles introduit de nouvelles paires critiques. On voit qu'avec les six règles que nous avons (trois au départ et trois nouvelles), on ne peut pas encore démontrer x = e * x par de simples réécritures[8]. D'autre part, rien ne garantit l'arrêt du processus de complétion. Autrement dit, rien ne garantit qu'en calculant des paires critiques et en orientant les paires critiques pour en faire des règles de réécriture, le processus va s'arrêter. Néanmoins, les paires critiques jouent un rôle clé dans l'obtention ou la démonstration de la confluence, comme cela est expliqué dans la section qui suit.

Dans cette section nous allons nous placer dans la réécriture de termes et raisonner essentiellement sur des dessins pour chercher les différentes configurations où le problème de la confluence locale peut se poser. Deux configurations simples se présentent tout d'abord.

Premièrement, il y a confluence locale lorsque les contractions de t vers t₁ et de t vers t₂ se font en deux positions disjointes. Deuxièmement, il y a aussi confluence locale si l'une des contractions de t (celle vers t₁ ou celle vers t₂) s'effectue dans la partie substituée du membre gauche de l'autre contraction (cf. dessins ci-dessous).

Exemple où il y a confluence locale parce qu'on réécrit en deux positions disjointes.

Exemple où il y a confluence locale parce que la première réécriture réécrit dans la partie substituée du membre gauche de la première réécriture.

Il se peut qu'il n'y ait pas confluence locale si les sous-termes réécrits (appelés redex pour reducible expressions) se superposent, autrement dit si l'une des contractions se fait dans la partie non substituée de l'autre. Par exemple :

Exemple où la confluence locale n'est pas garantie.

Considérons deux règles G₁ → D₁ et G₂ → D₂ et une position p dans G₁ qui n'est pas la position d'une variable. Considérons aussi une substitution principale σ (voir l'article sur l'unification) du terme à la position p dans G₁ et du terme G₂ (ainsi, la position p correspond à un sous-terme où l'on réécrit en utilisant la règle G₂ → D₂). La paire formée des termes σ(D₁) et σ(G₁)[σ(D₂)]_|p (c'est-à-dire le terme σ(G₁) où on a remplacé le sous-terme en position p par σ(D₂)) est appelée une paire critique.

Le tableau suivant donne quelques exemples de paires critiques. On précise les deux règles G₁ → D₁ et G₂ → D₂, la position p (représentée en gras dans le terme) dans G₁ et la substitution principale σ du terme à la position p dans G₁ et du terme G₂.