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