Complétion de Knuth-Bendix

Principe de la complétion de Knuth-Bendix : transformer des équations (ici, en entrée, ce sont les axiomes des groupes) en un système de réécriture confluent et qui termine.

La procédure de complétion de Knuth-Bendix ou complétion de Knuth-Bendix (aussi appelée algorithme de Knuth-Bendix ) transforme, si elle réussit, un ensemble fini d'identités (sur des termes) décrivant une structure algébrique en un système de réécriture de termes confluent et qui termine (dit alors convergent). Le processus de complétion a été inventé par Donald Knuthaidé d'un étudiant, nommé Peter Bendix, pour la mise en œuvre.

En cas de réussite, la complétion donne un moyen effectif de résoudre le problème du mot pour l'algèbre en question, comme cela a été démontré par Gérard Huet. Par exemple, pour la théorie équationnelle des groupes (voir schéma à droite), la complétion fournit un système de réécriture de terme confluent et qui termine. On peut alors décider si une équation t₁ = t₂ est vraie dans tous les groupes (même si décider si une formule du premier ordre est vraie dans tous les groupes est indécidable).

Malheureusement, le problème du mot étant indécidable en général, la procédure de complétion ne se termine pas toujours avec succès. Elle peut soit s'exécuter indéfiniment, soit échouer en rencontrant une identité non-orientable (qu'elle ne peut pas transformer en règle de réécriture sans être sûre de ne pas mettre en danger la terminaison).

Il existe une variante de la procédure de complétion qui n'échoue pas sur les identités non orientables. Elle fournit une procédure de semi-décision pour le problème du mot, autrement dit, elle permet de dire si une identité donnée est déductible des identités qui décrivent l'algèbre en question, dans tous les cas où elle l'est effectivement, mais peut ne jamais terminer.

Ordre de réduction

Pour garantir la terminaison des systèmes de réécriture qui interviennent au cours du processus, mais aussi pour garantir la correction de la méthode, la complétion de Knuth-Bendix prend en entrée un ordre < sur les termes. La relation doit être irréflexive, transitive et bien fondée, close par contexte (si a < b alors x[a]p < x[b]p où x[a]p et x[b]p sont les termes x où on a remplacé le sous-terme en position p par respectivement a et b), close par instanciation (si a < b, alors a[σ] < b[σ] pour toute substitution σ). Une relation qui satisfait ces propriétés est un ordre de réduction.

Exemple : ordre lexicographique sur les chemins

L'ordre lexicographique sur les chemins 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.

Idée générale

Certains ouvrages présentent d'abord la procédure de complétion sous la forme d'une procédure naïve qui est loin d'une implémentation en pratique mais qui permet de comprendre l'idée générale. La procédure de complétion de Knuth-Bendix prend en entrée un ensemble fini d'identités et un ordre de réduction < sur les termes. En sortie, il produit un système de réécriture pour les identités qui est à la fois confluent, qui termine et qui est compatible avec l'ordre. La procédure peut aussi explicitement dire qu'elle ne parvient pas à construire un tel système de réécriture ou alors elle peut diverger.

Initialisation

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)

Boucle de complétion

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

Pseudo-code de la procédure naïve

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

 

Procédure de complétion sous forme de règles

On peut présenter la complétion de manière synthétique à l'aide de règles d'inférence qui transforment à la fois le système d'équations et le système de réécriture. On les écrit sous la forme ${\frac {E_{\text{avant}},\qquad R_{\text{avant}}}{E_{\text{après}},\qquad R_{\text{après}}}}$ où le numérateur donne le système d'équations et le système de réécriture avant l'application de la règle et le dénominateur donne le système d'équations et le système de réécriture après l'application de la règle. En appliquant les règles (dans n'importe quel ordre et tant que c'est possible), on espère transformer l'état initial $(E_{\text{initial}},\emptyset )$ où il y a les équations données en entrée et un système de réécriture vide en un état final $(\emptyset ,R)$ où il n'y a plus d'équations à traiter et un système de réécriture confluent et qui termine.

Règles de base

On donne d'abord un ensemble minimal de règles :

Nom de la règle	Règle	Explication
Orienter une identité	${\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é	${\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	${\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é	${\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.

Règles d'optimisation

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	${\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	${\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.

Exemples

Dans cette section, nous allons exécuter la procédure de Knuth-Bendix sur quelques exemples pour illustrer les cas où la complétion réussit, échoue ou boucle.

Exemple où la complétion réussit

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

Exemple où la complétion échoue

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.

Exemple où la complétion boucle

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.

Variantes et implémentations

Il existe une implémentation de la complétion de Knuth-Bendix à but pédagogique avec une interface graphique. Il existe des variantes de la complétion de Knuth-Bendix où l'ordre de complétion n'est pas donné a priori mais construit au cours du processus de complétion.

Le prouveur Waldmeister est une implémentation de la complétion. Il a remporté les sessions de 1997 à 2011 et la session 2014 de la compétition CASC dans la catégorie UEQ (pour unit-equational first-order logic).

La complétion de Knuth-Bendix est implémentée dans des outils de calculs formels par exemple Magma qui utilise le package kbmag.

Articles connexes

• Combinatoire des mots
• Paire critique
• Algorithme de Buchberger : bien que développé indépendamment, c'est une instantiation de la complétion de Knuth-Bendix pour un idéal polynomial

Lien externe

• Logiciel pédagogique pour tester la complétion de Knuth-Bendix