# Paire critique

En informatique, plus précisément en théorie de la réécriture, une paire critique$^,$ est une paire de termes qui intervient dans l'étude de la confluence (locale) des systèmes de réécriture. Il s'agit de deux termes obtenus à partir d'un terme t, l'un en appliquant une règle sur t, l'autre en appliquant une règle sur un sous-terme de t. Par exemple, si on dispose des deux règles (u * v) * z → u * (v * z) et x$^2$ * y$^2$ → (x * y)$^2$, et que l'on considère le terme t = (x$^2$ * y$^2$) * z alors :
* si on applique la première règle sur tout le terme t on obtient x$^2$ * (y$^2$ * z)
* si on applique la deuxième règle sur le sous-terme (x$^2$ * y$^2$) on obtient (x * y)$^2$ * z
Les termes x$^2$ * (y$^2$ * z) et (x * y)$^2$ * z forment une paire critique.
L'intérêt des paires critiques est le suivant : si un système de réécriture n'a qu'un nombre fini de règles, le nombre de ses paires critiques est fini et si toutes ses paires critiques sont joignables alors il est localement confluent.

## Présentation intuitive et motivation
### Diminuer le non-déterminisme

Le réécriture est un processus non déterministe, 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 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é 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 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 ».

### Un exemple : l'axiomatisation faible des groupes

À 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.
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. 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.

## Assurer la confluence locale

Un système de réécriture est localement confluent si pour tout terme t, quand t se contracte en t$_1$ et t se contracte en t$_2$, alors t$_1$ et t$_2$ peuvent se réécrire en un même terme. Dans cette section, nous allons étudier d'abord deux configurations où la confluence locale est garantie puis présenter une configuration où la confluence locale n'est pas garantie, ce qui conduira au concept de paire critique. Nous verrons ensuite que la confluence locale dans les systèmes de réécriture se ramène à l'identification des paires critiques.

### Cas où la confluence locale est garantie

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$_1$ et de t vers t$_2$ se font en deux positions disjointes. Deuxièmement, il y a aussi confluence locale si l'une des contractions de t (celle vers t$_1$ ou celle vers t$_2$) 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. |

### Cas où la confluence locale n'est pas garantie

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 :

### Définition d'une paire critique

Considérons deux règles G$_1$ → D$_1$ et G$_2$ → D$_2$ et une position p dans G$_1$ 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$_1$ et du terme G$_2$ (ainsi, la position p correspond à un sous-terme où l'on réécrit en utilisant la règle G$_2$ → D$_2$). La paire formée des termes σ(D$_1$) et σ(G$_1$)[σ(D$_2$)]$_{|p}$ (c'est-à-dire le terme σ(G$_1$) où on a remplacé le sous-terme en position p par σ(D$_2$)) est appelée une paire critique.

### Exemples

Le tableau suivant donne quelques exemples de paires critiques. On précise les deux règles G$_1$ → D$_1$ et G$_2$ → D$_2$, la position p (représentée en gras dans le terme) dans G$_1$ et la substitution principale σ du terme à la position p dans G$_1$ et du terme G$_2$.
| G$_1$ → D$_1$ | G$_2$ → D$_2$ | position p dans G$_1$ | substitution principale σ | Paire critique σ(D$_1$) et σ(G$_1$)[σ(D$_2$)]$_{|p}$ |
| f(g(a, x)) → k(x) | g(y, b) → g(y, c) | f(g(a, x)) | [x := b, y := a] de g(a, x) et g(y, b) | k(b) et f(g(a, c)) |
| (x * y) * z → x * (y * z) | x * x$^{-1}$ → e | (x * y) * z | [y := x$^{-1}$] de x * y et x * x$^{-1}$ | x * (x$^{-1}$ * z) et e * z |
| (x * y) * z → x * (y * z) | f(x) * f(y) → f(x * y) | (x * y) * z → x * (y * z) | [x := f(x), y := f(y)] de x * y et f(x) * f(y) | f(x) * (f(y) * z) et f(x * y) * z |

## Algorithme pour tester la confluence d'un système de réécriture noethérien

On peut montrer que :
Théorème — Un système de réécriture est localement confluent si et seulement si toutes ses paires critiques sont joignables.
De plus, le lemme de Newman dit qu'un système de réécriture noethérien (qui se termine) est localement confluent si et seulement s'il est confluent.
On en déduit donc un algorithme pour tester qu'un système de réécriture noethérien (qui se termine) est confluent : on calcule toutes les paires critiques. Pour chaque paire <s, t>, on calcule les formes irréductibles de s (c'est-à-dire on applique des règles de réécriture sur s jusqu'à épuisement) et les formes irréductibles de t. S'il n'y a pas de formes irréductibles égales pour s et t alors on répond que le système de réécriture n'est pas confluent. Sinon, si pour tout paire, on trouve des formes irréductibles égales, alors le système est confluent.