Abstract

Termination analysis for functional programs is a challenging problem with applications in program verification, as well as theorem proving in which it is essential to prove termination of functions for soundness. Building on the size-change termination framework proposed by Lee, Jones and Ben-Amram, we introduce termination analysis for higher-order functional programs, based on a simple but effective termination criterion.

The analysis and verification of higher-order programs raises the issue of control-flow analysis for higher-order languages. The problem of constructing an accurate call graph for a higher-order program has been the topic of extensive research, and the precision of the call graph crucially determines the precision of the resulting analysis. Our termination framework allows the call graph construction technique to be varied, and we present three constructions varying in precision and complexity.

There is to date little theoretical understanding of the precision of control-flow analyses. We use the expressiveness of termination analysis for each call graph to compare our control-flow analysis, and show that precise relationships between the classes of programs recognised as terminating by the same termination criterion over different call graph analyses. This provides a stepping stone to a better understanding of flow analyses for higher-order programs.