Sistema de redução
# Sistema de redução

Em matemática um sistema de redução é um sistema onde termos podem ser reescritos usando uma lista finita, ou infinita, de regras de reescrita
Exemplos de sistemas de redução incluem sistemas de reescrita de cadeias de caractere, sistemas de reescrita de termos, cálculo lambda sob conversão lambda e sistemas de redução combinatória.
Quando nenhuma regra de redução pode ser aplicada para uma determinada expressão, é dito que esta está na Forma Normal.

## Visão geral

Um sistema de liguagem formal que pode ser transformado de acordo com um conjunto finito de regras de reescrita é chamado de sistema de redução. Enquanto sistemas de redução também são conhecidos como sistemas de reescrita de strings ou Sistema de reescrita de termos, o termo sistemas de redução é mais geral.
Cálculo lambda, como já foi dito, é um exemplo de sistema de redução com regras conversões lambda, constituindo assim as regras de reescrita.

## Exemplo

Se nenhuma das regras de reescrita de um sistema de redução é aplicada a Expressão E, então E está em forma normal para um sistema de redução.
Um par de expressões (x,y) é chamado juntável (joinable), se ambos, x e y, podem ser reduzidos para a mesma expressão em zero ou mais passos de redução (exemplo, a aplicação de regras de redução).
Se x é reduzido para y em um passo, isso é indicado por $x\rightarrow y$. Se Se x é reduzido para y em zero ou mais passos, isso é indicado por $x\rightarrow ^{*}y$.

### 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.
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 \,...\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.