Rational Rewriting

In this paper we introduced rational rewriting to rewrite infinite rational terms as finitely represented by mgrterms. The main advantage of this approach is that it deals with infinite terms by retaining most of the results and tools for finite rewriting avoiding the use of infinitary machinery. The obvious disadvantage is that we can only deal with rational terms. Nevertheless there are significant applications concerning rational terms. In these settings we believe that our approach can be a valid alternative to infinite rewriting. For example, we can define relations among mgrterms. Rules like mgrx.g(x) rarr mgry.f(x) or mgrx.g(x) rarr c, cannot be expressed in the infinite rewriting approaches. Though our setting lacks expressivity, it is more flexible since mgrterms are first class citizens. The other consequence of working in a finitary framework is that we can deal with TRSs that do not need to have the restrictions, like left-linearity or orthogonality, that are necessary to guarantee the ohgr-convergency of the non terminating relations.