Termination analysis

From Wikipedia, the free encyclopedia

In computer science, termination analysis is a program analysis technique which attempts to determine whether the evaluation of a given expression will definitely terminate. The study of this problem has led to several interesting results in computer science and mathematics; for example the solution to the Halting problem.

Some expressions are trivially observed to terminate, like "2 * 4"; a sequence of terminating expressions will also terminate. Loops may or may not terminate, as they can be run repeatedly; however loops implemented using a counter variable as typically found in data processing algorithms will usually terminate, demonstrated by the pseudocode example below:

i := 1
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 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

There is, however, no general procedure for determining whether an expression involving looping instructions will halt, even when humans are tasked with the inspection. To see why, we can construct a simple loop to verify Goldbach's Conjecture as follows:

t := 4
loop
    if there does not exist x, y where is_prime(x) and is_prime(y) and x + y = t
        //counterexample found
        print "Goldbach's Conjecture is false for the number " + t
        exit loop
    otherwise
        t := t + 2
        continue loop

To know whether this expression will halt, it is necessary to know whether Goldbach's Conjecture is true or false, which is still an unsolved mathematics problem.

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 are also undecidable in general. Most recursive expressions found in common usage (ie. 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 1
        return 1
    otherwise
        return argument * factorial(argument - 1)