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

Redução

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

n-Redução

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

Notações

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

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

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

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

Índice

Definições