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, the following loop will, in theory, never stop. However, it may halt when executed on a physical machine due to
arithmetic overflow: either leading to an
exception or causing the counter to wrap to a negative value and enabling the loop condition to be fulfilled. 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; by the
well-ordering property of
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 ==