The computability path ordering

TL;DR

This paper introduces the computability path ordering (CPO), a recursive relation for automatic termination proofs in simply typed higher-order calculi, extending previous orderings with new features and proving its well-foundedness.

Contribution

The paper presents the CPO, a novel recursive ordering for termination proofs, extending HORPO and incorporating new features like higher-order inductive types and precedence modifications.

Findings

Core CPO captures computability arguments similar to Tait and Girard.

No further type check elimination possible without losing well-foundedness, except for one case.

Extensions enable handling of higher-order inductive types and precedence adjustments.

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.