# Forma normal (reescritura abstracta)

En sistema de reescritura de términos, se dice que un término está en forma normal si no es posible aplicar ninguna regla del sistema que lo reescriba en otro término.
A partir de este concepto, podemos estudiar los sistemas de reescritura de términos y las características de sus términos con relación a las formas normales.

## Ejemplo como motivación

Considere del sistema de reescritura de términos con la regla de reducción siguiente 1: f(x,y) $\rightarrow$ x. El término f(a,b) puede ser reescrito como el término a aplicando la regla 1. Si tratamos de reducir a no se encuentra ninguna regla del sistema que pueda ser aplicada, entonces a es irreductible y así podemos decir que a es un término en forma normal en esta sistema de reescritura de términos.

## Teoría

Para un sistema de reducción de abstracto (A,$\rightarrow$) y $t_{1},\,t_{2}\,\in$ A, se dice que t_1 está en forma normal es irreductible, es decir, no existe $t_{2}$ tal que $t_{1}\,\rightarrow \,t_{2}$. Es decir, dado un término en el sistema si existe una regla que puede reescribirlo entonces está en forma normal.
También se puede afirmar que $t_{2}$ es una forma normal de $t_{1}$ si y solamente si hay una cadena de reducción finita iniciada por $t_{1}$ y terminada en $t_{2}$ y $t_{2}$ es una forma normal del sistema.

## Propiedades Relacionadas

Para un sistema de reducción abstracto (A,$\rightarrow$) se pueden tener las siguientes propiedades:
* Decimos que el término a $\in$ A es débilmente normalizante si existe una cadena de reducción finita iniciada por a y terminada en b a alguna forma normal b $\in$ A.
* Decimos que la relación $\rightarrow$ está débilmente normalizante si todo a $\in$ A es débilmente normalizante.
* Decimos que a $\in$ A es fuertemente normalizante si toda cadena de reducción iniciada por la cadena es finita. Por lo tanto, mediante el establecimiento de la manera normal, el elemento final de cada reducción de la cadena a ser iniciada por la forma normal de a.
* La relación $\rightarrow$ es fuertemente normalizante, concluyente, o noetheriana si cada elemento a $\in$ A es fuertemente normalizante.

### Débilmente Normalizado x Fuertemente Normalizado

En general, cuando se dice que un sistema es normalizante o concluyente, se está refiriendo a la propiedad debilidad normalizante. Observe que la propiedad de fuertemente normalizante es un requisito más fuerte que la propiedad francamente normalizante, por tanto, ser fuertemente normalizante implica débilmente normalizante, pero lo contrario no es verdadero. Mostramos esto a través de un ejemplo.
Sobre la base de la definición de débilmente normalizante de los sistemas de reducción abstractos, uno podría pensar que hay una reducción en la cadena del sistema iniciado por un término en el que uno de los términos de la cadena, con excepción del inicial, o bien, esto es, en el sistema no existen cadenas de reducción que formen ciclos de reducciones de términos entonces no existen cadenas de reducción infinitas en el sistema ya que para cada término existe una cadena de reducción finita y ninguna de ellas puede formar un ciclo. Sin embargo, esta declaración es falsa, como puede verse de la figura 1.
En la figura 1 se tiene un sistema de reducción abstracto que es débilmente normalizante porque todo el elemento puede ser reducido al elemento más debajo en la figura que a su vez está en la formal normal, pero no es fuertemente normalizante ya que no es una cadena de reducción infinita. Por lo tanto ser débilmente normalizante no implica ser fuertemente normalizante.

### Convergencia

Ser fuertemente normalizante no garantiza que los términos del sistema posean formas normales únicas, es decir, para algunos términos del sistema se pueden encontrar más de una forma normal. Para asegurar esto se necesita que el sistema, además de fuertemente normalizante, también sea confluente.
Cuando el sistema es fuertemente normalizante y confluente se dice que es convergente. En este caso podemos verificar si dos términos en el sistema son equivalentes verificando si sus formas normales son idénticas. Este resultado es importante porque en general comprueba dos términos, en un sistema de reducción abstracto, son equivalentes es un problema no decidible. Debido a que el sistema está fuertemente normalizando no existen cadenas infinitas en el sistema y como confluente cada término posee una única forma normal, por lo tanto, verificar si dos términos son equivalentes es un problema decidible.

## Bibliografía

* Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003.
* Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998.