Procedimiento aplicado a un sistema de reescritura presentado que intenta producir un sistema de reescritura confluyente (completo) orientando relaciones en reglas de reescritura bajo un orden de reducción elegido y añadiendo consecuencias obtenidas de solapamientos críticos hasta que no queden pares críticos sin resolver o el proceso diverja.

Principio

Elegir un orden bien fundado compatible con la reducción en términos o palabras, orientar las relaciones de manera consistente en reglas de reescritura, calcular pares críticos (solapamientos de lados izquierdos) y añadir las consecuencias apropiadas como nuevas reglas; iterar hasta lograr confluencia o hasta que la generación de reglas no termine.

Demostración

A partir de una presentación de un monoide con generadores y relaciones definitorias, orientar las relaciones por un orden lexicográfico o de longitud más lex, calcular los solapamientos entre reglas para hallar pares críticos, reducir esos pares e introducir nuevas reglas cuando las reducciones difieran; en casos simples esto produce un sistema confluyente finito que da formas normales únicas para las palabras.

Aplicación incorrecta

Suponer que la completación siempre termina o que el sistema de reescritura producido es mínimo; en muchas presentaciones no triviales el algoritmo puede ejecutarse indefinidamente, depender de la elección del orden o producir conjuntos de reglas redundantes o ineficientes si no se podan.

Consecuencia

Cuando tiene éxito, la completación Knuth–Bendix proporciona un sistema de reescritura confluyente y, por tanto, un procedimiento de decisión práctico para el problema de la palabra en la estructura presentada, al reducir palabras a formas normales únicas; además expone consecuencias algebraicas de las relaciones en forma calculable.

Inversión

En lugar de añadir consecuencias para forzar la confluencia, se pueden eliminar o debilitar relaciones para obtener más fácilmente un sistema terminante; esto invierte el objetivo de completación hacia la aproximación o simplificación conservadora, a costa de la fidelidad respecto de la presentación original.

Límite

La aplicabilidad depende de la clase de presentaciones, de la elección del orden de términos y de la aceptación de la no terminación; los resultados son sensibles a escenarios no conmutativos frente a conmutativos y a la presencia de identidades que generan infinitos pares críticos.

Tensión semántica

Completación Knuth–Bendix frente a métodos de bases de Gröbner: ambos eliminan redundancia convirtiendo generadores de relaciones en formas canónicas, pero operan en marcos algebraicos distintos (sistemas de reescritura frente a ideales polinómicos) y tienen diferentes cuestiones de terminación y ordenación.

Síntesis

La completación Knuth–Bendix orienta iterativamente relaciones en reglas de reescritura y resuelve solapamientos para construir un sistema confluyente; como puente algorítmico desde la presentación a formas normales canónicas, proporciona o bien un procedimiento de decisión efectivo para la igualdad de palabras o bien revela los límites de dicha reducción mediante la no terminación o la dependencia del orden.