Termination analysis

In computer science, a termination analysis is program analysis which attempts to determine whether the evaluation of a given program will definitely terminate. Because the halting problem is undecidable, termination analysis cannot be total. The aim is to find the answer "program does terminate" (or "program does not terminate") whenever this is possible. Without success the algorithm (or human) working on the termination analysis may answer with "maybe" or continue working infinitely long.

Termination proof

A termination proof is a type of mathematical proof that plays a critical role in formal verification because total correctness of an algorithm depends on termination.

A simple, general method for constructing termination proofs involves associating a measure with each step of an algorithm. The measure is taken from the domain of a well-founded relation, such as from the ordinal numbers. If the measure "decreases" according to the relation along every possible step of the algorithm, it must terminate, because there are no infinite descending chains with respect to a well-founded relation.

Some types of termination analysis can automatically generate or imply the existence of a termination proof.

Example

An example of a programming language construct which may or may not terminate is a loop, as they can be run repeatedly. Loops implemented using a counter variable as typically found in data processing algorithms will usually terminate, demonstrated by the pseudocode example below:

i := 0
loop until i = SIZE_OF_DATA
   process_data(data[i])) //process the data chunk at position i
   i := i + 1 //move to the next chunk of data to be processed

If the value of SIZE_OF_DATA is non-negative, fixed and finite, the loop will eventually terminate, assuming process_data terminates too.

Some loops can be shown to always terminate or never terminate, through human inspection. For example, even a non-programmer should see that, in theory, the following never stops (but it may halt on physical machines due to arithmetic overflow):

i := 1
loop until i = 0
    i := i + 1

In termination analysis one may also try to determine the termination behaviour of some program depending on some unknown input. The following example illustrates this problem.

i := 1
loop until i = UNKNOWN
    i := i + 1

Here the loop condition is defined using some value UNKNOWN, where the value of UNKNOWN is not known (e.g. defined by the user's input when the program is executed). Here the termination analysis must take into account all possible values of UNKNOWN and find out that in the possible case of UNKNOWN = 0 (as in the original example) the termination cannot be shown.

There is, however, no general procedure for determining whether an expression involving looping instructions will halt, even when humans are tasked with the inspection. The theoretical reason for this is the undecidability of the Halting Problem: there cannot exist some algorithm which determines whether any given program stops after finitely many computation steps.

In practice one fails to show termination (or non-termination) because every algorithm works with a finite set of methods being able to extract relevant information out of a given program. A method might look at how variables change with respect to some loop condition (possibly showing termination for that loop), other methods might try to transform the program's calculation to some mathematical construct and work on that, possibly getting information about the termination behaviour out of some properties of this mathematical model. But because each method is only able to "see" some specific reasons for (non)termination, even through combination of such methods one cannot cover all possible reasons for (non)termination.

Recursive functions and loops are equivalent in expression; any expression involving loops can be written using recursion, and vice versa. Thus the termination of recursive expressions is also undecidable in general. Most recursive expressions found in common usage (i.e. not pathological) can be shown to terminate through various means, usually depending on the definition of the expression itself. As an example, the function argument in the recursive expression for the factorial function below will always decrease by 1; from the well-ordering property on natural numbers, the argument will eventually reach 1 and the recursion will terminate.

function factorial (argument as natural number)
    if argument = 0 or argument = 1
        return 1
    otherwise
        return argument * factorial(argument - 1)

Dependent types

Termination check is very important in dependently typed programming language and theorem proving systems like Coq and Agda. These systems use Curry-Howard isomorphism between programs and proofs. Proofs over inductively defined data types were traditionally described using induction and recursion principles which are in fact, primitive recursion. However, it was found later, that describing a program via a recursively defined function with pattern matching is more natural way of proving than using induction principle directly. Unfortunately, allowing arbitrary, including non terminating definitions, leads to possibility of logical inconsistencies in type theories. That's why Agda and Coq have termination checkers built-in.

Sized types

One of the approaches to termination checking in dependently typed programming languages are sized types. The main idea is to annotate the types over which we can recurse with size annotations and allow recursive calls only on smaller arguments. Sized types are implemented in Agda as a syntactic extension.

Current Research

There are several research teams that work on new methods that can show (non)termination. Many researchers include these methods into programs[1] that try to analyze the termination behavior automatically (so without human interaction). An on-going aspect of research is to allow the existing methods to be used to analyze termination behavior of programs written in "real world" programming languages. For declarative languages like Haskell, Mercury and Prolog, many results exist[2][3][4] (mainly because of the strong mathematical background of these languages). The research community also works on new methods to analyze termination behavior of programs written in imperative languages like C and Java.

Because of the undecidability of the Halting Problem research in this field cannot reach completeness. One can always think of new methods that find new (complicated) reasons for termination.

See also

References

  1. ↑ Tools at termination-portal.org
  2. ↑ Giesl, J. and Swiderski, S. and Schneider-Kamp, P. and Thiemann, R. Pfenning, F., ed. Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages (invited lecture) (postscript). Term Rewriting and Applications, 17th Int. Conf., RTA-06. LNCS. pp. 297–312.
  3. ↑ Compiler options for termination analysis in Mercury
  4. ↑ http://verify.rwth-aachen.de/giesl/papers/lopstr07-distribute.pdf

Research papers on automated program termination analysis include:

System descriptions of automated termination analysis tools include:

External links

This article is issued from Wikipedia - version of the Tuesday, March 22, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.