(HO)RPO Revisited

Frédéric Blanqui 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Type de document :
Rapport
[Research Report] RR-5972, INRIA. 2006, pp.20
Liste complète des métadonnées

https://hal.inria.fr/inria-00090488
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 6 septembre 2006 - 17:47:14
Dernière modification le : jeudi 8 février 2018 - 11:32:01
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 15:32:03

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. (HO)RPO Revisited. [Research Report] RR-5972, INRIA. 2006, pp.20. 〈inria-00090488v3〉

Partager

Métriques

Consultations de la notice

170

Téléchargements de fichiers

57