Termination checking without using an ordering relation
Aytekin Vargun · International Conference on Software Engineering · 2007
One approach to mechanizing proofs of termination is to require that each new recursive function definition be accompanied by an ordering relation. The main disadvantage of this methodology is to determine an ordering relation first and prove the termination based on it. This paper describes an alternative approach that does not require a separate order relation. The proof of termination is constructed as a proof by induction that mirrors the recursion structure in the axioms. We generate for each new function being defined a termination condition (TC), and from each axiom of the function's definition we generate a corresponding termination axiom. Using the resulting set of termination axioms, we construct a proof of the TC. Both TC and termination axioms are generated automatically by applying a simple tool called TCGen. If the termination is proved, another tool called CodeGen can be applied to the axioms to construct a recursive function.