Sciweavers

Share
TACAS
2010
Springer

Automated Termination Analysis for Programs with Second-Order Recursion

10 years 2 months ago
Automated Termination Analysis for Programs with Second-Order Recursion
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 argumentbounded 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.
Markus Aderhold
Added 14 May 2010
Updated 14 May 2010
Type Conference
Year 2010
Where TACAS
Authors Markus Aderhold
Comments (0)
books