(HO)RPO Revisited - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2006

(HO)RPO Revisited


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 and versions

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



Frédéric Blanqui. (HO)RPO Revisited. [Research Report] RR-5972, INRIA. 2006, pp.20. ⟨inria-00090488v3⟩
111 View
32 Download



Gmail Facebook Twitter LinkedIn More