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.

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.

A, se dice que t_1 está en forma normal es irreductible, es decir, no existe

Es decir, dado un término en el sistema si existe una regla que puede reescribirlo entonces está en forma normal.

si y solamente si hay una cadena de reducción finita iniciada por

Mostramos esto a través de un ejemplo.

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.

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.

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.