So far, the works in this area have tried to define suitable properties of non-terminating relations in order to guarantee that the intended infinite term can be reached as the limit of w-converging derivations. The main advantage of these approaches is the generality of the framework with respect to the set of infinite definable terms: no a priori assumption is made on the set of definable infinite data structure. Restrictions instead apply on the kind of infinite derivations they can deal with (top erminating/strongly convergent) and on the term rewriting system, in order to guarantee the reachability of the infinite terms within w-steps. To this respect the restrictions are quite heavy since only left-linear (orthogonal) term rewriting systems can be managed. In this paper we propose a different approach based on the following consideration: in the above mentioned papers the need for considering non-terminating relations is a side effect of the definitional mechanism for infinite terms. That is the only way to deal with infinite terms is by giving the rules for constructing them.

Rational rewriting

1994

Abstract

So far, the works in this area have tried to define suitable properties of non-terminating relations in order to guarantee that the intended infinite term can be reached as the limit of w-converging derivations. The main advantage of these approaches is the generality of the framework with respect to the set of infinite definable terms: no a priori assumption is made on the set of definable infinite data structure. Restrictions instead apply on the kind of infinite derivations they can deal with (top erminating/strongly convergent) and on the term rewriting system, in order to guarantee the reachability of the infinite terms within w-steps. To this respect the restrictions are quite heavy since only left-linear (orthogonal) term rewriting systems can be managed. In this paper we propose a different approach based on the following consideration: in the above mentioned papers the need for considering non-terminating relations is a side effect of the definitional mechanism for infinite terms. That is the only way to deal with infinite terms is by giving the rules for constructing them.
1994
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
Software
Specifying and verifying and reasoning about programs
File in questo prodotto:
File Dimensione Formato  
prod_409280-doc_143848.pdf

solo utenti autorizzati

Descrizione: Rational rewriting
Tipologia: Versione Editoriale (PDF)
Dimensione 1.64 MB
Formato Adobe PDF
1.64 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14243/360138
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? ND
social impact