En la reescritura abstracta , un objeto está en forma normal si no se puede reescribir más. Dependiendo del sistema de reescritura y del objeto, pueden existir varias formas normales o ninguna.
Definición
Dicho formalmente, si ( A , →) es un sistema de reescritura abstracta , alguna x ∈ A está en forma normal si no existe y ∈ A tal que x → y .
Por ejemplo, utilizando el término sistema de reescritura con una sola regla g ( x , y ) → x , el término g ( g (4,2), g (3,1)) se puede reescribir de la siguiente manera, aplicando la regla a la aparición más externa [nota 1] de g :
- g ( g (4,2), g (3,1)) → g (4,2) → 4.
Dado que ninguna regla se aplica al último término, 4, no se puede reescribir más y, por lo tanto, es una forma normal del término g ( g (4,2), g (3,1)) con respecto a este sistema de reescritura de términos .
Propiedades de normalización
Los conceptos relacionados se refieren a la posibilidad de reescribir un elemento en forma normal. Se dice que un objeto de un sistema de reescritura abstracto se normaliza débilmente si se puede reescribir de alguna manera en una forma normal, es decir, si alguna secuencia de reescritura a partir de él no se puede extender más. Se dice que un objeto se está normalizando fuertemente si se puede reescribir de alguna manera en una forma normal, es decir, si cada secuencia de reescritura a partir de él finalmente no puede extenderse más. Se dice que un sistema de reescritura abstracto se normaliza débil y fuertemente , o tiene la propiedad de normalización débil y fuerte , si cada uno de sus objetos se normaliza débil y fuertemente, respectivamente.
Por ejemplo, el sistema de regla única anterior se está normalizando fuertemente, ya que cada aplicación de regla disminuye adecuadamente el tamaño del término y, por lo tanto, no puede haber una secuencia de reescritura infinita a partir de cualquier término. En contraste, el sistema de dos reglas { g ( x , y ) → x , g ( x , x ) → g (3, x )} se normaliza débilmente [nota 2] pero no fuertemente [nota 3] , aunque cada el término que no contiene g (3,3) se normaliza fuertemente. [nota 4] El término g (4,4) tiene dos formas normales en este sistema, a saber. g (4,4) → 4 y g (4,4) → g (3,4) → 3, por lo tanto, el sistema no es confluente .
Otro ejemplo: el sistema de una sola regla { r ( x , y ) → r ( y , x )} no tiene propiedades normalizadoras (ni débil ni fuerte), ya que de cualquier término, por ejemplo, r (4,2) una sola secuencia de reescritura comienza, a saber. r (4,2) → r (2,4) → r (4,2) → r (2,4) → ..., que es infinitamente largo.
Normalización y confluencia
El lema de Newman establece que si un sistema de reescritura abstracta A se normaliza fuertemente y es débilmente confluente , entonces A es confluente .
El resultado permite generalizar aún más el lema del par crítico . [ aclaración necesaria ]
Ver también
Notas
- ^ Cada aparición de g donde se aplica la regla se resalta en negrita .
- ^ Dado que cada término que contiene g se puede reescribir mediante un número finito de aplicaciones de la primera regla a un término sin g , que está en forma normal.
- ^ Ya que al término g (3,3), la segunda regla se puede aplicar una y otra vez, sin llegar a ninguna forma normal.
- ^ Para un término dado, dejar que m y n indican el número total de g y de g aplicada a los argumentos idénticos, respectivamente. La aplicación de cualquier regla disminuye adecuadamente el valor de m + n , lo cual es posible solo un número finito de veces.
Referencias
- Baader, Franz ; Nipkow, Tobias (1998). Reescritura de términos y todo eso . Prensa de la Universidad de Cambridge. ISBN 9780521779203.