Une procédure algorithmique qui prend un ensemble de règles de réécriture (ou de relations) et un ordre de réduction bien fondé, puis tente d'étendre l'ensemble de règles en ajoutant des conséquences (résolution des paires critiques) afin d'obtenir un système de réécriture confluent (et terminé) qui résout le problème des mots pour l'algèbre présentée lorsque la procédure aboutit.

Principe

Calculer systématiquement les recouvrements (paires critiques) entre règles, orienter les égalités obtenues selon un ordre de termes choisi, et ajouter de nouvelles règles pour résoudre les divergences ; répéter jusqu'à ce qu'il n'y ait plus de paires critiques non résolues ou que le processus n'aboutisse pas.

Démonstration

Pour une présentation finiment engendrée d'un monoïde ou d'un groupe, convertir les relations en règles de réduction orientées avec un ordre de longueur ou lexicographique, calculer les paires critiques issues des recouvrements des membres gauches, ajouter des règles résolutives et simplifier de manière itérative. Si la procédure termine sur un système confluent, deux mots sont égaux dans l'algèbre présentée si et seulement s'ils se réduisent à la même forme normale.

Mauvaise application

Supposer que l'algorithme termine toujours ou qu'il produit toujours la confluence ; choisir un ordre mauvais ou non bien fondé ou ignorer des axiomes équationnels (comme la commutativité) peut empêcher la réussite ou conduire à des conclusions incorrectes sur le problème des mots.

Conséquence

Si elle réussit, la complétion fournit un système de réécriture terminé et confluent et donc une solution en forme normale au problème des mots ; elle met aussi en évidence des conséquences structurelles telles que des représentants canoniques et des procédures de décision pour l'égalité.

Inversion

Le point de vue inverse consiste à introduire délibérément des recouvrements ambigus (en supprimant des règles ou en affaiblissant les ordres) pour produire des systèmes non confluent, ce qui peut être utile pour explorer des présentations alternatives mais fait perdre la décidabilité des formes normales.

Limite

S'applique aux systèmes de réécriture de termes, aux présentations de monoïdes ou de groupes et aux théories équationnelles pour lesquelles existe un ordre bien fondé compatible ; elle n'est pas garantie de réussir pour toutes les présentations et doit être adaptée (ou remplacée) pour les théories avec commutativité incorporée, des contraintes équationnelles d'ordre supérieur, ou lorsque la terminaison ne peut être assurée.

Tension sémantique

Tension avec les techniques de base de Gröbner et la complétion modulo théories : bien que superficiellement similaires, des méthodes distinctes apparaissent dans des cadres algébriques différents (idées polynomiales versus réécriture de termes pour mots), et les utilisateurs confondent parfois les garanties de terminaison/confluence entre ces cadres.

Synthèse

La Complétion Knuth–Bendix est une tentative algorithmique de transformer une présentation en un système de réécriture confluent et terminé en résolvant les recouvrements via l'analyse des paires critiques et des réductions orientées ; le succès fournit des formes normales et une procédure de décision pour l'égalité des mots, mais terminaison et confluence ne sont pas garanties en général.