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,${\displaystyle \rightarrow }$), em que a redução ${\displaystyle \rightarrow }$ é uma relação binária sobre o conjunto A, isto é, ${\displaystyle \rightarrow \,\subseteq }$ em A x A.

Redução

Se temos (a,b) ${\displaystyle \in }$ a ${\displaystyle \rightarrow }$ para a e b ${\displaystyle \in }$ A, então escrevemos a ${\displaystyle \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,${\displaystyle \rightarrow }$), uma cadeia de redução é uma cadeia finita ou infinita da seguintes forma: ${\displaystyle a_{0}\,\rightarrow \,a_{1}\,\rightarrow \,a_{2}\,\rightarrow \,a_{3}\,\rightarrow }$ … .

n-Redução

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

Notações

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

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

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

• y é um sucessor direto de x se e somente se x ${\displaystyle \rightarrow }$ y;
• y é um sucessor de x se e somente se x ${\displaystyle \rightarrow ^{+}}$ y;
• x e y são ligáveis se e somente se existe um z tal que x ${\displaystyle \rightarrow ^{*}}$ z ${\displaystyle \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