Blanqui, Frédéric and Jouannaud, Jean-Pierre and Rubio, Albert - The computability path ordering

lmcs:1604 - Logical Methods in Computer Science, October 26, 2015, Volume 11, Issue 4
The computability path ordering

Authors: Blanqui, Frédéric and Jouannaud, Jean-Pierre and Rubio, Albert

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 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.


Source : oai:arXiv.org:1506.03943
DOI : 10.2168/LMCS-11(4:3)2015
Volume: Volume 11, Issue 4
Published on: October 26, 2015
Submitted on: March 6, 2014
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 128 times.
This article's PDF has been downloaded 37 times.