Rational terms (possibly infinite terms with finitely many subterms) can be represented in a finite way via mu-terms, that is, terms over a signature extended with self-instantiation operators. For example, f(omega) = f(f(f(...))) can be represented as mu(x).f(x) (or also as mu(x).f(f(x)), f(mu x.f(x)),...). Now, if we reduce a mu-term t to s via a rewriting rule using standard notions of the theory of Term Rewriting Systems, how are the rational terms corresponding to t and to s related? We answer to this question in a satisfactory way, resorting to the definition of infinite parallel rewriting proposed by Corradini. We also provide a simple, algebraic description of mu-term rewriting through a variation of Meseguer's Rewriting Logic formalism.
Rational Term Rewriting
CORRADINI, ANDREA;GADDUCCI, FABIO
1998-01-01
Abstract
Rational terms (possibly infinite terms with finitely many subterms) can be represented in a finite way via mu-terms, that is, terms over a signature extended with self-instantiation operators. For example, f(omega) = f(f(f(...))) can be represented as mu(x).f(x) (or also as mu(x).f(f(x)), f(mu x.f(x)),...). Now, if we reduce a mu-term t to s via a rewriting rule using standard notions of the theory of Term Rewriting Systems, how are the rational terms corresponding to t and to s related? We answer to this question in a satisfactory way, resorting to the definition of infinite parallel rewriting proposed by Corradini. We also provide a simple, algebraic description of mu-term rewriting through a variation of Meseguer's Rewriting Logic formalism.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
