Termination analysis
Encyclopedia
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 work correctly in all cases. 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.
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 number
s. 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.
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
algorithm
s 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 function
s 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 number
s, 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)
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.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, a termination analysis is program analysis
Program analysis
Program analysis may refer to:* Program analysis , the process of automatically analysing the behavior of computer programs* Program evaluation, a disciplined way of assessing the merit, value, and worth of projects and programs...
which attempts to determine whether the evaluation of a given program
Computer program
A computer program is a sequence of instructions written to perform a specified task with a computer. A computer requires programs to function, typically executing the program's instructions in a central processor. The program has an executable form that the computer can use directly to execute...
will definitely terminate. Because the halting problem
Halting problem
In computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...
is undecidable
Undecidable
Undecidable may refer to:In mathematics and logic* Undecidable problem - a decision problem which no algorithm can decide* "Undecidable" is sometimes used as a synonym of "independent", where a formula in mathematical logic is independent of a logical theory if neither that formula nor its negation...
, termination analysis cannot work correctly in all cases. 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 proofMathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
that plays a critical role in formal verification
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
because total correctness of an algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
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
Well-founded relation
In mathematics, a binary relation, R, is well-founded on a class X if and only if every non-empty subset of X has a minimal element with respect to R; that is, for every non-empty subset S of X, there is an element m of S such that for every element s of S, the pair is not in R:\forall S...
, such as from the ordinal number
Ordinal number
In set theory, an ordinal number, or just ordinal, is the order type of a well-ordered set. They are usually identified with hereditarily transitive sets. Ordinals are an extension of the natural numbers different from integers and from cardinals...
s. 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 languageProgramming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
construct which may or may not terminate is a loop, as they can be run repeatedly. Loops implemented using a counter variable
Counter
In digital logic and computing, a counter is a device which stores the number of times a particular event or process has occurred, often in relationship to a clock signal.- Electronic counters :...
as typically found in data processing
Data processing
Computer data processing is any process that a computer program does to enter data and summarise, analyse or otherwise convert data into usable information. The process may be automated and run on a computer. It involves recording, analysing, sorting, summarising, calculating, disseminating and...
algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
s will usually terminate, demonstrated by the pseudocode
Pseudocode
In computer science and numerical computation, pseudocode is a compact and informal high-level description of the operating principle of a computer program or other algorithm. It uses the structural conventions of a programming language, but is intended for human reading rather than machine reading...
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
Programmer
A programmer, computer programmer or coder is someone who writes computer software. The term computer programmer can refer to a specialist in one area of computer programming or to a generalist who writes code for many kinds of software. One who practices or professes a formal approach to...
should see that, in theory, the following never stops (but it may halt on physical machines due to arithmetic overflow
Arithmetic overflow
The term arithmetic overflow or simply overflow has the following meanings.# In a computer, the condition that occurs when a calculation produces a result that is greater in magnitude than that which a given register or storage location can store or represent.# In a computer, the amount by which a...
):
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 function
Recursive function
Recursive function may refer to:*Recursion , a procedure or subroutine, implemented in a programming language, whose implementation references itself*A total computable function, a function which is defined for all possible inputs...
s 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
Pathological (mathematics)
In mathematics, a pathological phenomenon is one whose properties are considered atypically bad or counterintuitive; the opposite is well-behaved....
) 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
Factorial
In mathematics, the factorial of a non-negative integer n, denoted by n!, is the product of all positive integers less than or equal to n...
function below will always decrease by 1; from the well-ordering property on natural number
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s, 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)
Current Research
There are several research teams that work on new methods that can show (non)termination. Many researchers include these methods into programs 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 and Prolog, many results exist (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.