Termination analysis of higher-order functional programs

Abstract

Size-change termination (SCT) automatically identifies termination of first-order functional programs. The SCT principle: a program terminates if every infinite control flow sequence would cause an infinite descent in a well-founded data value (POPL 2001). More recent work (RTA 2004) developed a termination analysis of the pure untyped A-calculus using a similar approach, but an entirely different notion of size was needed to compare higher-order values. Again this is a powerful analysis, even proving termination of certain A-expressions containing the fixpoint combinator Y. However the language analysed is tiny, not even containing constants. These techniques are unified and extended significantly, to yield a termination analyser for higher-order, call-by-value programs as in ML's purely functional core or similar functional languages. Our analyser has been proven correct, and implemented for a substantial subset of OCaml. © Springer-Verlag Berlin Heidelberg 2005.