Forma normal

Em sistemas de reescrita de termos, dizemos que um termo está na forma normal se não é possível aplicar nenhuma regra do sistema que o reescreva em outro termo.

A partir deste conceito, podemos estudar sistemas de reescrita de termos quanto as características dos seus termos com a relação as formas normais.

Exemplo como Motivação editar

Considere o sistema de reescrita de termos com a seguinte regra de redução 1: f(x,y) $\rightarrow$ x. O termo f(a,b) pode ser reescrito como o termo a aplicando a regra 1. Se tentarmos reduzir a não encontraremos nenhuma regra do sistema que possa ser aplicada, logo a é irredutível e podemos dizer assim que a é um termo em forma normal neste sistema de reescrita de termos.

Teoria editar

Para um sistema de redução abstrato (A, $\rightarrow$ ) e $t_{1},\,t_{2}\,\in$ A, dizemos que $t_{1}$ está em forma normal se é irredutível, isto é, não existe $t_{2}$ tal que $t_{1}\,\rightarrow \,t_{2}$ . Isto é, dado um termo no sistema se não existir uma regra que possa reescrevê-lo então ele está em forma normal.

Dizemos também que $t_{2}$ é uma forma normal de $t_{1}$ se e somente se existe uma cadeia de redução finita iniciada por $t_{1}$ e terminada em $t_{2}$ e $t_{2}$ é uma forma normal do sistema.

Propriedades Relacionadas editar

Para um sistema de redução abstrato (A, $\rightarrow$ ) podemos ter as seguintes propriedades:

Dizemos que um termo a $\in$ A é fracamente normalizante se existe um cadeia de redução finita iniciada por a terminado em b para alguma forma normal b $\in$ A.
Dizemos que a relação $\rightarrow$ é fracamente normalizante se todo a $\in$ A é fracamente normalizante.
Dizemos que a $\in$ A é fortemente normalizante se toda cadeia de redução iniciada por a é finita. Logo, pela definição de forma normal, o último elemento de cada cadeia de redução iniciada por a será uma forma normal de a.
A relação $\rightarrow$ é fortemente normalizante, terminante, ou noetheriana, se cada elemento a $\in$ A é fortemente normalizante.

Fracamente Normalizante x Fortemente Normalizante editar

Figura 1:Sistema de redução abstrato fracamente normalizante, mas não fortemente normalizante

Em geral, quando dizemos que um sistema é normalizante ou terminante, estamos nos referindo à propriedade de fracamente normalizante. Observe que a propriedade de fortemente normalizante é um requisito mais forte que a propriedade fracamente normalizante, portanto ser fortemente normalizante implica fracamente normalizante, mas o contrário não é verdadeiro. Mostraremos isto através de um exemplo.

Com base na definição da propriedade de fracamente normalizante sobre sistemas abstratos de redução, poderíamos pensar que se não existe no sistema uma cadeia de redução iniciada por um termo a em que um dos termos da cadeia, com exceção do inicial, seja a, isto é, não existem no sistema cadeias de redução que formem ciclos de reduções de termos então não existem cadeias de redução infinitas no sistema já que para cada termo existe uma cadeia de redução finita e nenhuma delas pode formar um ciclo. No entanto, esta afirmação é falsa como podemos observar na figura 1.

Na figura 1 temos um sistema abstrato de redução que é fracamente normalizante, pois todo elemento pode ser reduzido ao elemento mais abaixo na figura que por sua vez é está na forma normal, mas não é fortemente normalizante pois existe uma cadeia de redução infinita. Portanto ser fracamente normalizante não implica ser fortemente normalizante.

Convergência editar

Ser fortemente normalizante não garante que os termos do sistema possuam formas normais únicas, isto é, para alguns termos do sistema podemos encontrar mais de uma forma normal. Para garantir isto necessitamos que o sistema além de fortemente normalizante, também seja confluente.

Quando o sistema é fortemente normalizante e confluente dizemos que ele é convergente. Neste caso podemos verificar se dois termos no sistema são equivalentes verificando se suas formas normais são idênticas. Este resultado é importante pois em geral verificar se dois termos, num sistema abstrato de redução, são equivalentes é um problema não decidível. Como o sistema é fortemente normalizante não existe cadeias infinitas no sistema e como é confluente cada termo possui uma forma normal única portanto verificar se dois termos são equivalentes é um problema decidível.

Bibliografia editar

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.