(HO)RPO Revisited - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2006

(HO)RPO Revisited

Résumé

The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used for strengthening the higher-order recursive path ordering. In the present paper, we study in more details the relations between the computability closure and the (higher-order) recursive path ordering. We show that the first-order recursive path ordering is equal to an ordering naturally defined from the computability closure. In the higher-order case, we get an ordering containing the higher-order recursive path ordering whose well-foundedness relies on the correctness of the computability closure. This provides a simple way to extend the higher-order recursive path ordering to richer type systems.
Fichier principal
Vignette du fichier
RR-5972.pdf (278.8 Ko) Télécharger le fichier

Dates et versions

inria-00090488 , version 1 (31-08-2006)
inria-00090488 , version 2 (06-09-2006)
inria-00090488 , version 3 (06-09-2006)

Identifiants

Citer

Frédéric Blanqui. (HO)RPO Revisited. [Research Report] RR-5972, INRIA. 2006, pp.20. ⟨inria-00090488v3⟩
119 Consultations
33 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More