Sistema de redução abstrato

Um sistema de redução abstrato (SRA) é uma modelagem matemática que permite o estudo de propriedades sobre sistema de reescrita de termos sem a necessidade de nos preocuparmos com a natureza dos objetos que são reescritos.

Definições

Sistema de Redução Abstrato

Um sistema de redução abstrato (SRA) é um par (A,$\rightarrow$), em que a redução $\rightarrow$ é uma relação binária sobre o conjunto A, isto é, $\rightarrow \,\subseteq$ em A x A.

Redução

Se temos (a,b) $\in$ a $\rightarrow$ para a e b $\in$ A, então escrevemos a $\rightarrow$ b e chamamos b de uma redução de a, ou a uma expansão de b.

Cadeia de redução ou seqüência de redução

Seja o SRA (A,$\rightarrow$), uma cadeia de redução é uma cadeia finita ou infinita da seguintes forma: $a_{0}\,\rightarrow \,a_{1}\,\rightarrow \,a_{2}\,\rightarrow \,a_{3}\,\rightarrow$ … .

n-Redução

Dizemos que $a_{n}$ é uma n-redução de $a_{1}$ se existir uma cadeia $a_{1}\,\rightarrow ,a_{2}\,\rightarrow \,a_{3}\,\rightarrow \,\ldots \rightarrow \,a_{n}$.

Notações

Para o SRA (a,$\rightarrow$) temos as seguintes notações para $\rightarrow$:

• Fecho reflexivo: $\rightarrow ^{=}$.
• Fecho transitivo: $\rightarrow ^{+}$.
• Fecho simétrico: $\leftrightarrow$.
• Fecho transitivo e reflexivo: $\rightarrow ^{*}$.
• Fecho transitivo e simétrico: $\leftrightarrow ^{+}$.
• Fecho transitivo, simétrico e reflexivo: $\leftrightarrow ^{*}$.
• Relação inversa: $\leftarrow$.

Para o SRA (A,$\rightarrow$) e x, y e z $\in$ A dizemos que:

• y é um sucessor direto de x se e somente se x $\rightarrow$ y;
• y é um sucessor de x se e somente se x $\rightarrow ^{+}$ y;
• x e y são ligáveis se e somente se existe um z tal que x $\rightarrow ^{*}$ z $\leftarrow ^{*}$ y.

Bibliografia

• 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.

Ver também

• Sistema de reescrita de termos
• Sistema de redução