Procédure appliquée à un système de réécriture présenté qui tente de produire un système de réécriture confluent (complet) en orientant les relations en règles de réécriture selon un ordre de réduction choisi et en ajoutant les conséquences issues des recouvrements critiques jusqu'à ce qu'il ne reste plus de paires critiques non résolues ou que le processus diverge.

Principe

Choisir un ordre bien fondé compatible avec la réduction sur les termes ou mots, orienter les relations de manière cohérente en règles de réécriture, calculer les paires critiques (recouvrements des parties gauches), et ajouter les conséquences appropriées comme nouvelles règles ; itérer jusqu'à obtention de la confluence ou à non-terminaison de la génération de règles.

Démonstration

Partir d'une présentation d'un monoïde avec générateurs et relations définissantes ; orienter les relations selon un ordre lexicographique ou longueur-plus-lexique, calculer les recouvrements entre règles pour trouver des paires critiques, réduire ces paires et introduire de nouvelles règles lorsque les réductions diffèrent ; dans des cas simples ceci produit un système confluent fini donnant des formes normales uniques pour les mots.

Mauvaise application

Supposer que la complétion termine toujours ou que le système de réécriture obtenu soit minimal ; pour de nombreuses présentations non triviales l'algorithme peut tourner indéfiniment, dépendre du choix d'ordre ou produire des ensembles de règles redondants ou inefficaces sans élagage.

Conséquence

Lorsqu'elle réussit, la complétion Knuth–Bendix fournit un système de réécriture confluent et donc une procédure de décision pratique pour le problème des mots dans la structure présentée en réduisant les mots à des formes normales uniques ; elle met aussi en évidence des conséquences algébriques des relations sous une forme calculable.

Inversion

Plutôt que d'ajouter des conséquences pour forcer la confluence, on peut retirer ou affaiblir des relations pour obtenir plus facilement un système terminant ; cela inverse l'objectif de complétion en approximation ou simplification conservative, au prix de la fidélité à la présentation d'origine.

Limite

La portée dépend de la classe des présentations, du choix de l'ordre sur les termes et de l'acceptation de la non-terminaison ; les résultats sont sensibles aux cadres non commutatifs versus commutatifs et à la présence d'identités générant une infinité de paires critiques.

Tension sémantique

Complétion Knuth–Bendix versus méthodes de bases de Gröbner : les deux réduisent la redondance en transformant des générateurs de relations en formes canoniques, mais opèrent dans des cadres algébriques différents (systèmes de réécriture contre idéaux polynomiaux) et présentent des différences de terminaison et de choix d'ordre.

Synthèse

La complétion Knuth–Bendix oriente itérativement des relations en règles de réécriture et résout les recouvrements pour construire un système confluent ; en tant que pont algorithmique entre présentation et formes normales canoniques, elle fournit soit une procédure de décision effective pour l'égalité des mots, soit révèle les limites de cette réduction par la non-terminaison ou la dépendance à l'ordre.