En lógica matemática , un par crítico surge en los sistemas de reescritura de términos donde las reglas de reescritura se superponen para producir dos términos diferentes. Más detalladamente, ( t 1 , t 2 ) es un par crítico si hay un término t para el cual dos aplicaciones diferentes de una regla de reescritura (ya sea la misma regla aplicada de manera diferente o dos reglas diferentes) producen los términos t 1 y t 2 .
Por ejemplo, en el sistema de reescritura de términos con reglas
f ( g ( x , y ), z ) → g ( x , z ) g ( x , y ) → x ,
el par sólo es fundamental es ⟨ g ( x , z ), f ( x , z )⟩. Ambos términos se pueden derivar del término f ( g ( x , y ), z ) aplicando una sola regla de reescritura.
Como otro ejemplo, considere el término sistema de reescritura con la regla única
f ( x , y ) → x .
Al aplicar esta regla de dos maneras diferentes al término f ( f ( x , x ), x ), vemos que ( f ( x , x ), f ( x , x )) es un par crítico (trivial).
Cuando ambos lados del par crítico pueden reducirse al mismo término, el par crítico se llama convergente . Cuando un lado del par crítico es idéntico al otro, el par crítico se denomina trivial .
Si el término sistema de reescritura no confluye , es posible que el par crítico no converja, por lo que los pares críticos son fuentes potenciales donde fallará la confluencia. De hecho, el lema del par crítico establece que un sistema de reescritura de términos es débilmente (también conocido como localmente) confluente si todos los pares críticos son convergentes. Por lo tanto, para averiguar si un sistema de reescritura de términos es débilmente confluente, basta con probar todos los pares críticos y ver si son convergentes. Esto permite averiguar algorítmicamente si un sistema de reescritura de términos es débilmente confluente o no, dado que se puede verificar algorítmicamente si dos términos convergen.
Confluencia débil implica claramente pares críticos convergentes: si cualquier par crítico ⟨ un , b ⟩ surge, a continuación, una y b tienen reduct común y por lo tanto el par crítico es convergente.
Ver también
- Compleción de Knuth-Bendix , un algoritmo basado en pares críticos para calcular un sistema de reescritura de términos de terminación y confluencia equivalente a uno dado
enlaces externos
Referencias
- Franz Baader y Tobias Nipkow , Term Rewriting and All That , Cambridge University Press, 1998 (enlace web del libro)
- Terese, Term Rewriting Systems , Cambridge Tracts in Theoretical Computer Science, 2003. (enlace web del libro)