The first topic we’re going to look at on QA9 is termination analyses for type theories. What is a termination analysis and why should we be interested? A termination analysis is a static analysis that attempts to show some piece of code is terminating — that is, will not execute forever — or even more interestingly, show that some function is uniformly terminating — that is, will terminate for all inputs to the function. Uniformly terminating functions are also called total functions. Functions which the termination analysis cannot determine are total are called possibly partial. These functions might or might not be total, but the termination analysis simply cannot tell.
We know from recursion theory that it is not possible to have a sound and complete termination analysis. We definitely want a sound analysis: if it says a term is terminating or a function is total, then that should really be the case. So we will have to give up on completeness. In this context, completeness means that if the term is terminating the analysis can definitely show that it is, and if the function is total then the analysis can definitely show that it is. So we will have to live with a situation where our termination analysis might report that some function is possibly partial, when it is really total.
In practice, the kind of functions that fall outside customary termination analyses are highly complex in the sense of complexity theory. Even very simple termination analyses can handle, for example, functions significantly more complex than Ackermann’s function, which takes more steps to compute an output, for natural number inputs on the order of 4 or 5, than there are atoms in the known universe. Mostly for Computer Science applications, the only interesting functions complex enough to pose problems for termination analyses are interpreters for languages where a termination analysis has ensured that all terms are terminating. In that case, an even stronger termination analysis must be used to confirm that the interpreter is itself a total function.
So we have answered the “what”: termination analyses are algorithms for certifying that terms are terminating and functions are total. Now how about the “why”? I will answer that in my next post.