Name
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 a 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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.2168/LMCS-11(4:3)2015 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | DocType | Volume |
termination,path order,rewriting,lambda-calculus,reducibility,inductive types | Journal | 11 |
Issue | ISSN | Citations |
4 | 1860-5974 | 9 |
PageRank | References | Authors |
0.52 | 32 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frédéric Blanqui | 1 | 290 | 17.96 |
| Jean-Pierre Jouannaud | 2 | 1921 | 227.43 |
| Albert Rubio | 3 | 228 | 19.44 |