Automated termination analysis for programs with second-order recursion

Abstract

Many algorithms on data structures such as terms (finitely branching trees) are naturally implemented by second-order recursion: A first-order procedure f passes itself as an argument to a second-order procedure like map, every, foldl, foldr, etc. to recursively apply f to the direct subterms of a term. We present a method for automated termination analysis of such procedures. It extends the approach of argument-bounded functions (i) by inspecting type components and (ii) by adding a facility to take care of second-order recursion. Our method has been implemented and automatically solves the examples considered in the literature. This improves the state of the art of inductive theorem provers, which (without our approach) require user interaction even for termination proofs of simple second-order recursive procedures. © 2010 Springer-Verlag.