In
computer science, termination analysis is
program analysis
In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness.
Program analysis focuses on two major areas: program op ...
which attempts to determine whether the evaluation of a given
program
Program, programme, programmer, or programming may refer to:
Business and management
* Program management, the process of managing several related projects
* Time management
* Program, a part of planning
Arts and entertainment Audio
* Programm ...
halts for ''each'' input. This means to determine whether the input program computes a ''total'' function.
It is closely related to the
halting problem
In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a g ...
, which is to determine whether a given program halts for a ''given'' input and which is
undecidable. The termination analysis is even more difficult than the Halting problem: the termination analysis in the model of
Turing machines as the model of programs implementing computable functions would have the goal of deciding whether a given Turing machine is a
total Turing machine, and this problem is at level
of the
arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
and thus is strictly more difficult than the Halting problem.
Now as the question whether a computable function is total is not
semi-decidable, each ''sound'' termination analyzer (i.e. an affirmative answer is never given for a non-terminating program) is ''incomplete'', i.e. must fail in determining termination for infinitely many terminating programs, either by running forever or halting with an indefinite answer.
Termination proof
A ''termination proof'' is a type of
mathematical proof
A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proo ...
that plays a critical role in
formal verification because
total correctness
Total may refer to:
Mathematics
* Total, the summation of a set of numbers
* Total order, a partial order without incomparable pairs
* Total relation, which may also mean
** connected relation (a binary relation in which any two elements are compa ...
of an
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
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
In set theory, an ordinal number, or ordinal, is a generalization of ordinal numerals (first, second, th, etc.) aimed to extend enumeration to infinite sets.
A finite set can be enumerated by successively labeling each element with the least ...
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
In mathematics, a total or linear order is a partial order in which any two elements are comparable. That is, a total order is a binary relation \leq on some set X, which satisfies the following for all a, b and c in X:
# a \leq a ( reflexiv ...
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
Data processing is the collection and manipulation of digital data to produce meaningful information.
Data processing is a form of ''information processing'', which is the modification (processing) of information in any manner detectable by a ...
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
s will usually terminate, demonstrated by the
pseudocode
In computer science, pseudocode is a plain language description of the steps in an algorithm or another system. Pseudocode often uses structural conventions of a normal programming language, but is intended for human reading rather than machine re ...
example below:
i := 0
loop until i = SIZE_OF_DATA
process_data(data
)
// 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
Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers—addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th c ...
: 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
Pathology is the study of the causes and effects of disease or injury. The word ''pathology'' also refers to the study of disease in general, incorporating a wide range of biology research fields and medical practices. However, when used in th ...
) 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
In mathematics, the factorial of a non-negative denoted is the product of all positive integers less than or equal The factorial also equals the product of n with the next smaller factorial:
\begin
n! &= n \times (n-1) \times (n-2) ...
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
Return may refer to:
In business, economics, and finance
* Return on investment (ROI), the financial gain after an expense.
* Rate of return, the financial term for the profit or loss derived from an investment
* Tax return, a blank document or t ...
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
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...
and
Agda. These systems use
Curry-Howard isomorphism between programs and proofs. Proofs over inductively defined data types were traditionally described using induction principles. However, it was found later that describing a program via a recursively defined function with pattern matching is a more natural way of proving than using induction principles directly. Unfortunately, allowing non-terminating definitions leads to logical inconsistency in type theories, which is why
Agda and
Coq
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...
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 that try to analyze the termination behavior automatically (so without human interaction). An ongoing 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
Prolog is a logic programming language associated with artificial intelligence and computational linguistics.
Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
, many results exist
[http://verify.rwth-aachen.de/giesl/papers/lopstr07-distribute.pdf ] (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
*
Complexity analysis
In computer science, the analysis of algorithms is the process of finding the computational complexity of algorithms—the amount of time, storage, or other resources needed to execute them. Usually, this involves determining a function that ...
— the problem of estimating the time needed to terminate
*
Loop variant
*
Total functional programming — a programming paradigm that restricts the range of programs to those that are provably terminating
*
Walther recursion
References
Research papers on automated program termination analysis include:
*
*
*
*
*
*
*
System descriptions of automated termination analysis tools include:
*
*
*
*
*
*
* {{cite book , author=Marché, C. , author2= Zantema, H. , author2-link= Hans Zantema , contribution=The Termination Competition (system description) , pages=303–313 , year=2007 , editor=Baader, F. , title=Term Rewriting and Applications, 18th Int. Conf., RTA-07 , series=LNCS , volume=4533 , publisher=Springer , url=https://www.lri.fr/~marche/marche07rta.pdf
External links
Termination Analysis of Higher-Order Functional ProgramsTermination Tools mailing listTermination Competition— see Marché,
Zantema (2007) for a description
Termination Portal
Static program analysis