The Computability Path Ordering

Abstract : This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a precedence on function symbols. A first version, core CPO, is essentially obtained from the higher-order recursive path ordering (HORPO) by eliminating type checks from some recursive calls and by incorporating the treatment of bound variables as in the so-called computability closure. The well-foundedness proof shows that core CPO captures the essence of computability arguments à la Tait and Girard, therefore explaining its name. We further show that no more type check can be eliminated from its recursive calls without loosing well-foundedness, but one for which we found no counterexample yet. Two extensions of core CPO are then introduced which allow one to consider: the first, higher-order inductive types; the second, a precedence in which some function symbols are smaller than application and abstraction.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 〈10.2168/LMCS-11(4:3)2015〉
Liste complète des métadonnées

Littérature citée [86 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01163091
Contributeur : Frédéric Blanqui <>
Soumis le : lundi 16 novembre 2015 - 16:54:27
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mercredi 17 février 2016 - 17:50:48

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio. The Computability Path Ordering. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 〈10.2168/LMCS-11(4:3)2015〉. 〈hal-01163091v2〉

Partager

Métriques

Consultations de la notice

376

Téléchargements de fichiers

58