Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [86 references]  Display  Hide  Download
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Monday, November 16, 2015 - 4:54:27 PM
Last modification on : Saturday, June 25, 2022 - 10:17:56 PM
Long-term archiving on: : Wednesday, February 17, 2016 - 5:50:48 PM


Files produced by the author(s)




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⟩



Record views


Files downloads