We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
THE COMPUTABILITY PATH ORDERING.
- Authors
BLANQUI, FRÉDÉRIC; JOUANNAUD, JEAN-PIERRE; RUBIO, ALBERT
- Abstract
This paper aims at carrying out termination proofs for simply typed higherorder 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 further type check can be eliminated from its recursive calls without loosing well-foundedness, but one for which we found no counter-example 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.
- Subjects
COMPUTABILITY logic; MATHEMATICAL proofs; RECURSIVE functions; MATHEMATICAL bounds; MATHEMATICAL variables
- Publication
Logical Methods in Computer Science (LMCS), 2015, Vol 11, Issue 4, p1
- ISSN
1860-5974
- Publication type
Article
- DOI
10.2168/LMCS-11(4:3)2015