Algoritmo de completación de Knuth-Bendix

El lema del par crítico establece que un sistema de reescritura de términos es localmente confluente (o débilmente confluente) si y solo si todos sus pares críticos convergen. Además, el lema de Newman establece que si un sistema de reescritura (abstracto) es fuertemente normalizador y débilmente confluente, entonces el sistema de reescritura es confluente. Por lo tanto, si podemos agregar reglas al sistema de reescritura de términos para forzar la convergencia de todos los pares críticos manteniendo la propiedad de fuerte normalización, esto forzará que el sistema de reescritura resultante sea confluente.

Consideremos un monoide finitamente presentado.${\displaystyle M=\langle X\mid R\rangle }$donde X es un conjunto finito de generadores y R es un conjunto de relaciones definitorias en X. Sea X ^* el conjunto de todas las palabras en X (es decir, el monoide libre generado por X). Dado que las relaciones R generan una relación de equivalencia en X*, se pueden considerar los elementos de M como las clases de equivalencia de X ^* bajo R. Para cada clase {w ₁ , w ₂ , ... } es deseable elegir un representante estándar w _k . Este representante se llama forma canónica o normal para cada palabra w _k en la clase. Si existe un método computable para determinar para cada w _k su forma normal w _i entonces el problema de la palabra se resuelve fácilmente. Un sistema de reescritura confluente permite hacer precisamente esto.

Aunque teóricamente la elección de una forma canónica puede hacerse de manera arbitraria, este enfoque generalmente no es computable. (Considérese que una relación de equivalencia en un lenguaje puede producir un número infinito de clases infinitas). Si el lenguaje está bien ordenado, el orden < proporciona un método consistente para definir representantes mínimos; sin embargo, el cálculo de estos representantes aún puede no ser posible. En particular, si se utiliza un sistema de reescritura para calcular representantes mínimos, el orden < también debería tener la propiedad:

A < B → XAY < XBY para todas las palabras A, B, X, Y

Esta propiedad se llama invariancia traslacional . Un orden que es a la vez invariante traslacional y un buen orden se llama orden de reducción .

A partir de la presentación del monoide, es posible definir un sistema de reescritura dado por las relaciones R. Si A x B está en R, entonces A  <  B, en cuyo caso B  →  A es una regla del sistema de reescritura; de lo contrario, A  >  B y A  →  B. Dado que < es un orden de reducción, una palabra dada W puede reducirse a W > W_1 > ... > W_n, donde W_n es irreducible bajo el sistema de reescritura. Sin embargo, dependiendo de las reglas que se apliquen en cada W _i  →  W _i+1, es posible obtener dos reducciones irreducibles diferentes W _n  ≠  W' _m de W. No obstante, si el sistema de reescritura dado por las relaciones se convierte en un sistema de reescritura confluente mediante el algoritmo de Knuth-Bendix, entonces todas las reducciones garantizan la misma palabra irreducible, es decir, la forma normal de esa palabra.

Supongamos que nos dan una presentación${\displaystyle \langle X\mid R\rangle }$, dónde${\displaystyle X}$es un conjunto de generadores y${\displaystyle R}$es un conjunto de relaciones que dan el sistema de reescritura. Supongamos además que tenemos un orden de reducción${\displaystyle <}$entre las palabras generadas por${\displaystyle X}$(p. ej., orden shortlex ). Para cada relación${\displaystyle P_{i}=Q_{i}}$en${\displaystyle R}$, suponer${\displaystyle Q_{i}<P_{i}}$. Así pues, comenzamos con el conjunto de reducciones${\displaystyle P_{i}\rightarrow Q_{i}}$.

Primero, si existe alguna relación${\displaystyle P_{i}=Q_{i}}$se puede reducir, reemplazar${\displaystyle P_{i}}$y${\displaystyle Q_{i}}$con las reducciones.

A continuación, añadimos más reducciones (es decir, reescritura de reglas) para eliminar posibles excepciones de confluencia. Supongamos que${\displaystyle P_{i}}$y${\displaystyle P_{j}}$superposición.

1. Caso 1: o bien el prefijo de${\displaystyle P_{i}}$es igual al sufijo de${\displaystyle P_{j}}$o viceversa. En el primer caso, podemos escribir${\displaystyle P_{i}=BC}$y${\displaystyle P_{j}=AB}$; en este último caso,${\displaystyle P_{i}=AB}$y${\displaystyle P_{j}=BC}$.
2. Caso 2: cualquiera${\displaystyle P_{i}}$está completamente contenido en (rodeado por) ${\displaystyle P_{j}}$o viceversa. En el primer caso, podemos escribir${\displaystyle P_{i}=B}$y${\displaystyle P_{j}=ABC}$; en este último caso,${\displaystyle P_{i}=ABC}$y${\displaystyle P_{j}=B}$.

Reducir la palabra${\displaystyle ABC}$usando${\displaystyle P_{i}}$primero, luego usando${\displaystyle P_{j}}$Primero. Llama a los resultados${\displaystyle r_{1},r_{2}}$, respectivamente. Si${\displaystyle r_{1}\neq r_{2}}$, entonces tenemos un caso en el que la confluencia podría fallar. Por lo tanto, agregue la reducción.${\displaystyle \max r_{1},r_{2}\rightarrow \min r_{1},r_{2}}$a${\displaystyle R}$.

Después de agregar una regla a${\displaystyle R}$, eliminar cualquier regla en${\displaystyle R}$que podrían tener lados izquierdos reducibles (después de comprobar si dichas reglas tienen pares críticos con otras reglas).

Repita el procedimiento hasta que se hayan revisado todos los lados izquierdos superpuestos.