Loop Detection in Term Rewriting Using the Eliminating Unfoldings - Université de La Réunion Accéder directement au contenu
Article Dans Une Revue Theoretical Computer Science Année : 2008

Loop Detection in Term Rewriting Using the Eliminating Unfoldings

Résumé

In this paper, we present a fully automatizable approach to detecting loops in standard term rewriting. Our method is based on semi-unication and an unfolding operation which processes both forwards and backwards and considers variable subterms. We also describe a technique to reduce the explosion of rules caused by the unfolding process. The idea is to eliminate from the set of unfoldings some rules that are estimated as useless for detecting loops. This is done by an approximation which consists in pruning the left-hand or right-hand side of the rules used to unfold. The analyser that we have implemented is able to solve most of the examples from the Termination Competition'07 that do not terminate due to a loop.
Fichier principal
Vignette du fichier
Loop_detection_in_term_rewriting_using_eliminating_unfoldings.pdf (325.28 Ko) Télécharger le fichier
Origine : Accord explicite pour ce dépôt
Loading...

Dates et versions

hal-01186183 , version 1 (08-11-2018)

Identifiants

  • HAL Id : hal-01186183 , version 1

Citer

Etienne Payet. Loop Detection in Term Rewriting Using the Eliminating Unfoldings. Theoretical Computer Science, 2008, 403 (2-3), pp.307-327. ⟨hal-01186183⟩
76 Consultations
142 Téléchargements

Partager

Gmail Facebook X LinkedIn More