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 com-putability 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 for 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.
Recommendations
- The Computability Path Ordering: The End of a Quest
- scientific article; zbMATH DE number 1405624
- On the complexity of recursive path orderings
- scientific article; zbMATH DE number 1303201
- Ordinal computability
- A complete characterization of the ordering of path-complete methods
- On recursive path ordering
- Order-computable sets
- The first-order theory of lexicographic path orderings is undecidable
- Computably enumerable partial orders
Cited in
(15)- A Lambda-Free Higher-Order Recursive Path Order
- HORPO with Computability Closure: A Reconstruction
- Certified Higher-Order Recursive Path Ordering
- The Computability Path Ordering: The End of a Quest
- Computability Closure: Ten Years Later
- Size-based termination of higher-order rewriting
- scientific article; zbMATH DE number 7566074 (Why is no real title available?)
- Higher-Order Termination: From Kruskal to Computability
- Superposition with lambdas
- Superposition with lambdas
- Superposition for higher-order logic
- A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems
- The computability path order for beta-eta-normal higher-order rewriting
- Coq formalization of the higher-order recursive path ordering
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
This page was built for publication: The computability path ordering
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196359)
