Paire critique

En informatique, plus précisément en théorie de la réécriture, une paire critique^[1]^,^[2] 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² * y² → (x * y)², et que l'on considère le terme t = (x² * y²) * z alors :

si on applique la première règle sur tout le terme t on obtient x² * (y² * z)
si on applique la deuxième règle sur le sous-terme (x² * y²) on obtient (x * y)² * z

Les termes x² * (y² * z) et (x * y)² * 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^[3] alors il est localement confluent.

Présentation intuitive et motivation

Articles détaillés : Réécriture (informatique) et Complétion de Knuth-Bendix.

Diminuer le non-déterminisme

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

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.

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.

Assurer la confluence locale

Un système de réécriture est localement confluent si pour tout terme t, quand t se contracte^[9] en t₁ et t se contracte en t₂, alors t₁ et t₂ 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₁ 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).

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₁ → 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.

Exemples

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

G₁ → D₁	G₂ → D₂	position p dans G₁	substitution principale σ	Paire critique σ(D₁) et σ(G₁)[σ(D₂)]_\|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.

Notes et références

↑ D. Knuth, P. Bendix (1970). J. Leech, ed. Simple Word Problems in Universal Algebras. Pergamon Press. pp. 263–297. Voir aussi Franz Baader et Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1^er janvier 1998, 301 p. (ISBN 0-521-45520-0, lire en ligne).
↑ Franz Baader et Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1^er janvier 1998, 301 p. (ISBN 0-521-45520-0, lire en ligne).
↑ Une paire de termes est joignable si les deux termes qui la constituent se réécrivent en le même terme.
↑ Dans ce cas, on parle de non-déterminisme « on ne sait pas », en anglais don't know non determinsm, pour dire qu'on ne sait pas a priori le résultat du calcul.
↑ Dans ce cas, on parle de non-déterminisme « on s'en moque », en anglais don't care non determinsm, pour dire qu'on ne cherche pas à savoir comment l'unique résultat est obtenu.
↑ Plus de non-déterminisme « on ne sait pas ».
↑ qui prouve les mêmes égalités, si les règles, qui servent d'égalités de base, sont prises dans les deux sens.
↑ On parle alors de démonstration par normalisation, qui est une démonstration d'une égalité par réduction à la même forme normale du membre gauche et du membre droit de l'égalité.
↑ On dira que t se contracte en t' si t se réécrit en t' en une étape de réécriture.

[1] D. Knuth, P. Bendix (1970). J. Leech, ed. Simple Word Problems in Universal Algebras. Pergamon Press. pp. 263–297. Voir aussi Franz Baader et Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1^er janvier 1998, 301 p. (ISBN 0-521-45520-0, lire en ligne).

[2] Franz Baader et Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1^er janvier 1998, 301 p. (ISBN 0-521-45520-0, lire en ligne).

[3] Une paire de termes est joignable si les deux termes qui la constituent se réécrivent en le même terme.

[4] Dans ce cas, on parle de non-déterminisme « on ne sait pas », en anglais don't know non determinsm, pour dire qu'on ne sait pas a priori le résultat du calcul.

[5] Dans ce cas, on parle de non-déterminisme « on s'en moque », en anglais don't care non determinsm, pour dire qu'on ne cherche pas à savoir comment l'unique résultat est obtenu.

[6] Plus de non-déterminisme « on ne sait pas ».

[7] qui prouve les mêmes égalités, si les règles, qui servent d'égalités de base, sont prises dans les deux sens.

[8] On parle alors de démonstration par normalisation, qui est une démonstration d'une égalité par réduction à la même forme normale du membre gauche et du membre droit de l'égalité.

[9] On dira que t se contracte en t' si t se réécrit en t' en une étape de réécriture.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]