Complétion de Knuth-Bendix

L'ordre lexicographique sur les chemins[7]^,[8] est un exemple d'ordre de réduction. C'est un ordre pratique car il est uniquement donné à partir d'un ordre sur les symboles de fonctions. Étant donné un ordre sur les symboles de fonctions il est défini par :

• s > x si x est une variable qui apparaît dans s et s ≠ x
• f(s₁, ... s_k) > g(t₁, ... , t_n) si

1. ou bien il existe i où s_i > g(t₁, ... , t_n)
2. ou bien f > g et f(s₁, ... s_k) > t_j pour tout j
3. ou bien f = g et f(s₁, ... s_k) > t_j pour tout j et il existe i tq s₁ = t₁, ..., s_i-1 = t_i-1 et s_i > t_i.

La procédure part d'un système de réécriture obtenu en orientant les identités à l'aide de l'ordre < (s'il existe une règle qui n'est pas orientable avec l'ordre <, alors l'algorithme dit qu'il n'existe pas de tel système de réécriture). Par exemple, si l'entrée du problème est :

1 * x = x     (1 est un élément neutre à gauche)

x^-1 * x = 1     (x^-1 est un inverse à gauche de x)

(x * y) * z = x * (y * z)    (* est associative)

et l'ordre lexicographique sur les chemins comme ordre de réduction > où ^-1 > * > 1, l'algorithme commence avec le système de réécriture suivant :

1 * x → x

x^-1 * x → 1

(x * y) * z → x * (y * z)

Ensuite, la procédure complète le système de réécriture en ajoutant des règles supplémentaires afin d'essayer de rendre le système confluent. La complétion s'appuie sur l'ordre < afin de garantir que le système termine toujours.

Durant la complétion, on considère les paires critiques. Pour chaque paire critique (s, t), on calcule des formes normales s' et t' on ajoute s' → t' ou t' → s' en s'aidant de l'ordre <. Par exemple, 1 * z et x^-1 * (x * z) forment une paire critique non joignable et sont déjà des formes normales. Comme x^-1 * (x * z) > 1 * z, la procédure de complétion ajoute la règle :

x^-1 * (x * z) → 1 * z

Ainsi, la complétion ajoute de nouvelles règles au système de réécriture et donc de nouvelles paires critiques apparaissent. Il faut donc continuer à compléter le système de réécriture. La procédure s'arrête avec succès s'il n'y a plus de nouvelles paires critiques non joignables. La procédure s'arrête avec échec s'il y a une paire critique que l'on ne peut pas rendre joignable avec l'ordre <.

Entrée : un ensemble fini d'équations E
         un ordre <
Sortie : un système de réécriture R qui termine, qui est confluent correspondant à E, et compatible avec l'ordre < s'il en existe un
         "non" ou alors boucle, s'il n'existe pas de tel système de réécriture R

completionKnuthBendixVersionNaïve(E, <)
    si il existe une équation s = t dans E où s ≠ t et ni s < t, ni t < s
                 retourner "non"
    sinon
                 Soit R l'ensemble des règles G → D où G = D ou D = G est une équation de E et D < G

                 répéter
                          pour toute paire critique s, t de R
                                        s' := une R-forme normale de s
                                        t' := une R-forme normale de t

                                        si s' ≠ t'   
                                                 si t' < s'
                                                         ajouter s' → t' à R
                                                 sinon si s' < t'
                                                         ajouter t' → s' à R
                                                 sinon
                                                      retourner "non"
                 tant que R a été modifié par la boucle

                 retourner R

On donne d'abord un ensemble minimal de règles[13]^,[14] :

Nom de la règle	Règle	Explication
Orienter une identité	${\displaystyle {\frac {E\cup \{s=t\},\qquad R}{E,\qquad R\cup \{s\rightarrow t\}}}}$ si s > t	Transforme une identité en une règle en utilisant l'ordre de réduction <
Déduire une identité	${\displaystyle {\frac {E,\qquad R}{E\cup \{s=t\},\qquad R}}}$ s'il existe u qui se réécrit en s et qui se réécrit en t	Ajoute une identité déduite du système de réécriture. La règle donnée ici est très générale. Un cas spécial de la règle consiste à ajouter l'identité s = t pour toute paire critique (s, t) de R.
Supprimer une identité triviale	${\displaystyle {\frac {E\cup \{s=s\},\qquad R}{E,\qquad R}}}$	Supprime une identité triviale où les termes de part et d'autre sont syntaxiquement les mêmes.
Simplifier une identité	${\displaystyle {\frac {E\cup \{s=t\},\qquad R}{E\cup \{s'=t'\},\qquad R}}}$ si s se réécrit en s' ou t se réécrit en t'	Simplifie une identité en utilisant le système de réécriture.

On note l'invariant suivant : l'application d'une règle conserve les égalités que l'on peut démontrer en combinant les égalités de E ou les règles de réécriture de R, le système de réécriture termine toujours. Les transformations ne font que faire croître le système de réécriture R.

Les quatre transformations ci-dessus construisent un système de réécriture où il y a redondance des règles de réécriture et qui, étant donné un ordre de terminaison, n'est pas unique. C'est pourquoi on utilise aussi les deux règles suivantes qui sont des optimisations afin d'obtenir un système de réduction avec moins de règles, qui soit unique pour l'ordre que l'on s'est donné et qui soit plus efficace pour calculer les formes normales.

Composer	${\displaystyle {\frac {E,\qquad R\cup \{s\rightarrow t\}}{E,\qquad R\cup \{s\rightarrow u\}}}}$ si t se réécrit en u	Ajoute une règle au système de réécriture qui compose la réécriture s en t et t en u
Effondrement	${\displaystyle {\frac {E,\qquad R\cup \{s\rightarrow t\}}{E\cup \{u=t\},\qquad R}}}$ si s → u en utilisant une règle G → D où G ne peut pas être réduit par s → t	Supprime une règle dont le membre gauche est simplifiable, sans la faire disparaître complètement

Ces transformations jouent un rôle clés dans la démonstration de la correction de la procédure de complétion[3]^,[5].

Exemple d'exécution qui réussit de la complétion de Knuth-Bendix avec en entrée un système d'identités pour les semi-groupes idempotents.

On cherche un système de réécriture confluent et qui termine pour le système d'identités pour les semi-groupes idempotents donné par :

(x * y) * z = x * (y * z)

x * x = x

La figure à droite donne les applications des règles depuis le système d'identités (et un système de réécriture vide) vers un système d'identités vide et un système de réécriture confluent et qui termine. Il y a deux premières applications des règles d'orientation. Puis une déduction d'une identité car x * z et x * (x * z) sont des paires critiques. Le système de réécriture confluent et qui termine est :

(x * y) * z → x * (y * z)

x * x → x

x * (x * z) → x * z

Si le système d'équations contient :

x * y = y * x

alors la procédure de complétion échoue car elle n'arrive pas à orienter l'équation.

Considérons l'exemple :

a * b = b * a

a * c = c * a = b * d = d * b = 1

Avec l'ordre lexicographique sur les chemins donné par 1 < a < c < b < d, la complétion termine. Mais avec l'ordre lexicographique sur les chemins donné par 1 < a < b < c < d, la complétion ne termine pas.