Sistema de redução abstrato
# 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.