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

editar

Sistema de Redução Abstrato

editar

Um sistema de redução abstrato (SRA) é um par (A, ), em que a redução   é uma relação binária sobre o conjunto A, isto é,   em A x A.

Redução

editar

Se temos (a,b)   a   para a e b   A, então escrevemos a   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

editar

Seja o SRA (A, ), uma cadeia de redução é uma cadeia finita ou infinita da seguintes forma:   … .

n-Redução

editar

Dizemos que   é uma n-redução de   se existir uma cadeia  .

Notações

editar

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

  • Fecho reflexivo:  .
  • Fecho transitivo:  .
  • Fecho simétrico:  .
  • Fecho transitivo e reflexivo:  .
  • Fecho transitivo e simétrico:  .
  • Fecho transitivo, simétrico e reflexivo:  .
  • Relação inversa:  .

Para o SRA (A, ) e x, y e z   A dizemos que:

  • y é um sucessor direto de x se e somente se x   y;
  • y é um sucessor de x se e somente se x   y;
  • x e y são ligáveis se e somente se existe um z tal que x   z   y.

Bibliografia

editar
  • 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

editar