El algoritmo de finalización Knuth-Bendix (el nombre de Donald Knuth y Peter Bendix [1] ) es un semi-decisión [2] [3] algoritmo para la transformación de un conjunto de ecuaciones (más términos ) en un confluente sistema de reescritura plazo . Cuando el algoritmo tiene éxito, resuelve eficazmente el problema verbal del álgebra especificada .
El algoritmo de Buchberger para calcular las bases de Gröbner es un algoritmo muy similar. Aunque se desarrolló de forma independiente, también puede verse como la instanciación del algoritmo de Knuth-Bendix en la teoría de anillos polinomiales .
Introducción
Para un conjunto E de ecuaciones, su cierre deductivo () es el conjunto de todas las ecuaciones que se pueden derivar aplicando ecuaciones de E en cualquier orden. Formalmente, E se considera una relación binaria , () es su cierre de reescritura , y () es el cierre de equivalencia de (). Para un conjunto R de reglas de reescritura, su cierre deductivo ( ∘ ) es el conjunto de todas las ecuaciones que se pueden confirmar aplicando reglas de R de izquierda a derecha a ambos lados hasta que sean literalmente iguales. Formalmente, R se ve nuevamente como una relación binaria, () es su cierre de reescritura, () es su inverso , y ( ∘ ) es la composición de relaciones de sus cierres transitivos reflexivos ( y ).
Por ejemplo, si E = {1⋅ x = x , x −1 ⋅ x = 1, ( x ⋅ y ) ⋅ z = x ⋅ ( y ⋅ z )} son los axiomas del grupo , la cadena de derivación
- a −1 ⋅ ( a ⋅ b ) ( a −1 ⋅ a ) ⋅ b 1⋅ b B
demuestra que a −1 ⋅ ( a ⋅ b ) b es un miembro del cierre deductivo de E. Si R = {1⋅ x → x , x −1 ⋅ x → 1, ( x ⋅ y ) ⋅ z → x ⋅ ( y ⋅ z )} es una versión de E de "regla de reescritura" , las cadenas de derivación
- ( a −1 ⋅ a ) ⋅ b 1⋅ b b y b B
demostrar que ( a −1 ⋅ a ) ⋅ b ∘ b es un miembro del cierre deductivo de R. Sin embargo, no hay forma de derivar a −1 ⋅ ( a ⋅ b )∘ b similar al anterior, ya que no se permite una aplicación de derecha a izquierda de la regla ( x ⋅ y ) ⋅ z → x ⋅ ( y ⋅ z ) .
El algoritmo de Knuth-Bendix toma un conjunto E de ecuaciones entre términos , y una orden de reducción (>) en el conjunto de todos los términos, y los intentos de construir un confluente y que termina término reescritura sistema R que tiene el mismo cierre deductivo como E . Si bien probar las consecuencias de E a menudo requiere intuición humana, probar las consecuencias de R no. Para más detalles, ver la confluencia (reescritura abstracto) ejemplos #Motivating , que da una prueba de ejemplo a partir de la teoría de grupos, realizado tanto usando E y el uso de R .
Reglas
Dado un conjunto E de ecuaciones entre términos , las siguientes reglas de inferencia se pueden usar para transformarlo en un sistema de reescritura de términos convergente equivalente (si es posible): [4] [5] Se basan en un orden de reducción dado por el usuario (>) en el conjunto de todos los términos; se eleva a un ordenamiento bien fundado (▻) en el conjunto de reglas de reescritura definiendo ( s → t ) ▻ ( l → r ) si
- s l , o
- s y l son literalmente similares y t > r .
Borrar | ‹ E ∪ { s = s } | , R › | ⊢ | ‹ E | , R › | |
Componer | ‹ E | , R ∪ { s → t } › | ⊢ | ‹ E | , R ∪ { s → u } › | si t tu |
Simplificar | ‹ E ∪ { s = t } | , R › | ⊢ | ‹ E ∪ { s = u } | , R › | si t tu |
Orientar | ‹ E ∪ { s = t } | , R › | ⊢ | ‹ E | , R ∪ { s → t } › | si s > t |
Colapso | ‹ E | , R ∪ { s → t } › | ⊢ | ‹ E ∪ { u = t } | , R › | si s u por l → r con ( s → t ) ▻ ( l → r ) |
Deducir | ‹ E | , R › | ⊢ | ‹ E ∪ { s = t } | , R › | si ( s , t ) es un par crítico de R |
Ejemplo
La siguiente ejecución de ejemplo, obtenida del demostrador del teorema E , calcula la finalización de los axiomas de grupo (aditivos) como en Knuth, Bendix (1970). Se inicia con las tres ecuaciones iniciales para el grupo (elemento neutro 0, elementos inversos, asociatividad), utilizando f(X,Y)
para X + Y , y i(X)
para - X . Las 10 ecuaciones marcadas con "final" representan el sistema de reescritura convergente resultante. "pm" es la abreviatura de " paramodulación ", que implementa deducir . El cálculo de pares críticos es un ejemplo de paramodulación para cláusulas de unidad de ecuaciones. "rw" es reescribir, implementar componer , contraer y simplificar . La orientación de las ecuaciones se realiza de forma implícita y no se registra.
1:: [++ igual (f (X1,0), X1)]: inicial ("GROUP.lop", at_line_9_column_1) 2:: [++ igual (f (X1, i (X1)), 0)]: inicial ("GROUP.lop", at_line_12_column_1) 3:: [++ igual (f (f (X1, X2), X3), f (X1, f (X2, X3)))]: inicial ("GROUP.lop", at_line_15_column_1) 5:: [++ igual (f (X1, X2), f (X1, f (0, X2)))]: pm (3,1) 6:: [++ igual (f (X1, f (X2, i (f (X1, X2)))), 0)]: pm (2,3) 7:: [++ igual (f (0, X2), f (X1, f (i (X1), X2)))]: pm (3,2) 27:: [++ igual (f (X1,0), f (0, i (i (X1))))]: pm (7,2) 36:: [++ igual (X1, f (0, i (i (X1))))]: rw (27,1) 46:: [++ igual (f (X1, X2), f (X1, i (i (X2))))]: pm (5,36) 52:: [++ igual (f (0, X1), X1)]: rw (36,46) 60:: [++ igual (i (0), 0)]: pm (2,52) 63:: [++ igual (i (i (X1)), f (0, X1))]: pm (46,52) 64:: [++ igual (f (X1, f (i (X1), X2)), X2)]: rw (7,52) 67:: [++ igual (i (i (X1)), X1)]: rw (63,52) 74:: [++ igual (f (i (X1), X1), 0)]: pm (2,67) 79:: [++ igual (f (0, X2), f (i (X1), f (X1, X2)))]: pm (3,74) 83:: [++ igual (X2, f (i (X1), f (X1, X2)))]: rw (79,52) 134:: [++ igual (f (i (X1), 0), f (X2, i (f (X1, X2))))]: pm (83,6) 151:: [++ igual (i (X1), f (X2, i (f (X1, X2))))]: rw (134,1) 165:: [++ igual (f (i (X1), i (X2)), i (f (X2, X1)))]: pm (83,151) 239:: [++ igual (f (X1,0), X1)]: 1: 'final' 240:: [++ igual (f (X1, i (X1)), 0)]: 2: 'final' 241:: [++ igual (f (f (X1, X2), X3), f (X1, f (X2, X3)))]: 3: 'final' 242:: [++ igual (f (0, X1), X1)]: 52: 'final' 243:: [++ igual (i (0), 0)]: 60: 'final' 244:: [++ igual (i (i (X1)), X1)]: 67: 'final' 245:: [++ igual (f (i (X1), X1), 0)]: 74: 'final' 246:: [++ igual (f (X1, f (i (X1), X2)), X2)]: 64: 'final' 247:: [++ igual (f (i (X1), f (X1, X2)), X2)]: 83: 'final' 248:: [++ igual (i (f (X1, X2)), f (i (X2), i (X1)))]: 165: 'final'
Consulte también Problema verbal (matemáticas) para ver otra presentación de este ejemplo.
Sistemas de reescritura de cuerdas en la teoría de grupos
Un caso importante en la teoría de grupos computacional son los sistemas de reescritura de cadenas que pueden usarse para dar etiquetas canónicas a elementos o clases sociales de un grupo presentado de forma finita como productos de los generadores . Este caso especial es el tema central de esta sección.
Motivación en la teoría de grupos
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 son convergentes. Además, tenemos el lema de Newman que establece que si un sistema de reescritura (abstracto) se normaliza fuertemente y confluye débilmente, entonces el sistema de reescritura es confluente. Entonces, si podemos agregar reglas al término sistema de reescritura para forzar que todos los pares críticos sean convergentes mientras se mantiene la propiedad de normalización fuerte, entonces esto forzará al sistema de reescritura resultante a ser confluente.
Considere un monoide de presentación finita 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 puede considerar que los elementos de M son las clases de equivalencia de X * bajo R. Para cada clase {w 1 , w 2 , ...} es deseable elegir un estándar representante w k . Este representante se denomina 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 verbal se resuelve fácilmente. Un sistema de reescritura confluente permite hacer precisamente esto.
Aunque la elección de una forma canónica teóricamente se puede hacer de manera arbitraria, este enfoque generalmente no es computable. (Considere que una relación de equivalencia en un lenguaje puede producir un número infinito de clases infinitas). Si el lenguaje está bien ordenado, entonces el orden
- A
Esta propiedad se llama invariancia de traducción . Un orden que es invariante en la traducción y un orden de pozo se denomina 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 y A → B. Dado que
Descripción del algoritmo para monoides presentados de forma finita
Supongamos que nos dan una presentación , dónde es un conjunto de generadores yes un conjunto de relaciones que da el sistema de reescritura. Supongamos además que tenemos un pedido de reducción entre las palabras generadas por (por ejemplo, orden shortlex ). Para cada relación en , suponga . Así comenzamos con el conjunto de reducciones.
Primero, si alguna relación se puede reducir, reemplazar y con las rebajas.
A continuación, agregamos más reducciones (es decir, reescritura de reglas) para eliminar posibles excepciones de confluencia. Suponer que y superposición.
- Caso 1: el prefijo de es igual al sufijo de , o viceversa. En el primer caso, podemos escribir y ; En este último caso, y .
- Caso 2: ya sea está completamente contenido en (rodeado por) , o viceversa. En el primer caso, podemos escribir y ; En este último caso, y .
Reducir la palabra utilizando primero, luego usando primero. Llamar a los resultados, respectivamente. Si, entonces tenemos una instancia en la que la confluencia podría fallar. Por lo tanto, agregue la reducción a .
Después de agregar una regla a , elimine las reglas en que podría tener lados izquierdos reducibles (después de verificar si tales reglas tienen pares críticos con otras reglas).
Repita el procedimiento hasta que se hayan verificado todos los lados izquierdos superpuestos.
Ejemplos de
Un ejemplo final
Considere el monoide:
- .
Usamos la orden shortlex . Este es un monoide infinito pero, sin embargo, el algoritmo de Knuth-Bendix es capaz de resolver el problema verbal.
Nuestras tres reducciones iniciales son por lo tanto
( 1 )
( 2 )
- .
( 3 )
Un sufijo de (a saber ) es un prefijo de , así que considera la palabra . Reduciendo usando ( 1 ), obtenemos. Reduciendo usando ( 3 ), obtenemos. Por lo tanto, obtenemos, dando la regla de reducción
- .
( 4 )
Del mismo modo, usando y reduciendo usando ( 2 ) y ( 3 ), obtenemos. De ahí la reducción
- .
( 5 )
Ambas reglas son obsoletas ( 3 ), por lo que las eliminamos.
A continuación, considere superponiendo ( 1 ) y ( 5 ). Reduciendo obtenemos, entonces agregamos la regla
- .
( 6 )
Considerando superponiendo ( 1 ) y ( 5 ), obtenemos, entonces agregamos la regla
- .
( 7 )
Estas reglas obsoletas ( 4 ) y ( 5 ), entonces las eliminamos.
Ahora, nos quedamos con el sistema de reescritura.
( 1 )
( 2 )
( 6 )
- .
( 7 )
Verificando las superposiciones de estas reglas, no encontramos fallas potenciales de confluencia. Por lo tanto, tenemos un sistema de reescritura confluente y el algoritmo termina con éxito.
Un ejemplo no final
El orden de los generadores puede afectar de manera crucial si termina la terminación Knuth-Bendix. Como ejemplo, considere el grupo abeliano libre por la presentación monoide:
La terminación Knuth-Bendix con respecto al orden lexicográfico termina con un sistema convergente, sin embargo considerando el orden longitud-lexicográfico no termina porque no hay sistemas convergentes finitos compatibles con este último orden. [6]
Generalizaciones
Si Knuth-Bendix no tiene éxito, funcionará para siempre o fallará cuando encuentre una ecuación desorientable (es decir, una ecuación que no puede convertir en una regla de reescritura). La terminación mejorada sin fallas no fallará en ecuaciones desorientables y proporciona un procedimiento de semi-decisión para el problema verbal.
La noción de reescritura registrada discutida en el documento de Heyworth y Wensley que se enumera a continuación permite alguna grabación o registro del proceso de reescritura a medida que avanza. Esto es útil para calcular identidades entre relaciones para presentaciones de grupos.
Referencias
- ^ D. Knuth, "La génesis de las gramáticas de atributos"
- ^ Jacob T. Schwartz; Domenico Cantone; Eugenio G. Omodeo; Martin Davis (2011). Lógica computacional y teoría de conjuntos: aplicación de la lógica formalizada al análisis . Springer Science & Business Media. pag. 200. ISBN 978-0-85729-808-9.
- ^ Hsiang, J .; Rusinowitch, M. (1987). "Sobre problemas verbales en teorías de ecuaciones" (PDF) . Autómatas, lenguajes y programación . Apuntes de conferencias en informática. 267 . pag. 54. doi : 10.1007 / 3-540-18088-5_6 . ISBN 978-3-540-18088-3., pag. 55
- ^ Bachmair, L .; Dershowitz, N .; Hsiang, J. (junio de 1986). "Pedidos para pruebas de ecuaciones". Proc. Simposio IEEE sobre Lógica en Ciencias de la Computación . págs. 346–357.
- ^ N. Dershowitz; J.-P. Jouannaud (1990). Jan van Leeuwen (ed.). Reescribir sistemas . Manual de Informática Teórica. B . Elsevier. págs. 243–320. Aquí: sección 8.1, p.293
- ^ V. Diekert; AJ Duncan; AG Myasnikov (2011). "Pregrupos y sistemas de reescritura geodésica". En Oleg Bogopolski; Inna Bumagin; Olga Kharlampovich; Enric Ventura (eds.). Teoría de grupos combinatoria y geométrica: conferencias de Dortmund y Ottawa-Montreal . Springer Science & Business Media. pag. 62. ISBN 978-3-7643-9911-5.
- D. Knuth; P. Bendix (1970). J. Leech (ed.). Problemas de palabras simples en álgebras universales (PDF) . Pergamon Press. págs. 263-297.
- Gérard Huet (1981). "Una prueba completa de la exactitud del algoritmo de finalización de Knuth-Bendix" (PDF) . J. Comput. Syst. Sci . 23 (1): 11-21. doi : 10.1016 / 0022-0000 (81) 90002-7 .
- C. Sims. "Cálculos con grupos presentados de forma finita". Cambridge, 1994.
- Anne Heyworth y CD Wensley. " Reescritura registrada e identidades entre relatores ". Grupos St. Andrews 2001 en Oxford. Vol. I, 256–276, London Math. Soc. Lecture Note Ser., 304, Cambridge Univ. Prensa, Cambridge, 2003.
enlaces externos
- Weisstein, Eric W. "Algoritmo de finalización de Knuth-Bendix" . MathWorld .