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 com-putability 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 checks 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 in-ductive types; the second, a precedence in which some function symbols are smaller than application and abstraction.

Mots clés: recursive path ordering; termination ordering; computability predicates; reducibility candidates; inductive types; Termination criterion; typed lambda calculus; rewriting

Domaines: Logique en informatique [cs.LO]

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio. The computability path ordering . 2015. ⟨hal-01163091v1⟩