The Computability Path Ordering

Frédéric Blanqui (1) , Jean-Pierre Jouannaud (2, 3) , Albert Rubio (4)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 UP11 - Université Paris-Sud - Paris 11
4 UPC - Universitat Politècnica de Catalunya = Université polytechnique de Catalogne [Barcelona]

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.

Mots clés: termination; path order; rewriting; lambda-calculus; reducibility; inductive types

Domaines: Logique en informatique [cs.LO]

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio. The Computability Path Ordering. Logical Methods in Computer Science, 2015, ⟨10.2168/LMCS-11(4:3)2015⟩. ⟨hal-01163091v2⟩