Termination analysis
void f(int n) {
while (n > 1)
if (n % 2 == 0)
n = n / 2;
else
n = 3 * n + 1;
}
|
As of 2024[update], it is still unknown whether this C-program terminates for every input; see Collatz conjecture. |
In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.
It is closely related to the
Now as the question whether a computable function is total is not semi-decidable,[1] 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
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
Some types of termination analysis can automatically generate or imply the existence of a termination proof.
Example
An example of a
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
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.[citation needed]
function factorial (argument as natural number) if argument = 0 or argument = 1return1 otherwise return argument * factorial(argument - 1)
Dependent types
Termination check is very important 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 (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.
See also
- Complexity analysis— 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
- ISBN 0-262-68052-1.
- ^ Tools at termination-portal.org
- ^ Giesl, J.; Swiderski, S.; Schneider-Kamp, P.; 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. Vol. 4098. pp. 297–312. (link: springerlink.com).
- ^ Compiler options for termination analysis in Mercury
- ^ http://verify.rwth-aachen.de/giesl/papers/lopstr07-distribute.pdf [bare URL PDF]
Research papers on automated program termination analysis include:
- Christoph Walther (1988). "Argument-Bounded Algorithms as a Basis for Automated Termination Proofs". Proc. 9th Conference on Automated Deduction. LNAI. Vol. 310. Springer. pp. 602–621.
- Christoph Walther (1991). "On Proving the Termination of Algorithms by Machine". Artificial Intelligence. 70 (1).
- Xi, Hongwei (1998). "Towards Automated Termination Proofs through Freezing" (PDF). In Rewriting Techniques and Applications, 9th Int. Conf., RTA-98. LNCS. Vol. 1379. Springer. pp. 271–285.
- Jürgen Giesl; Christoph Walther; Jürgen Brauburger (1998). "Termination Analysis for Functional Programs". In W. Bibel; P. Schmitt (eds.). Automated Deduction - A Basis for Applications (postscript). Vol. 3. Dordrecht: Kluwer Academic Publishers. pp. 135–164.
- Christoph Walther (2000). "Criteria for Termination". In S. Hölldobler (ed.). Intellectics and Computational Logic (postscript). Dordrecht: Kluwer Academic Publishers. pp. 361–386.
- Christoph Walther; Stephan Schweitzer (2005). "Automated Termination Analysis for Incompletely Defined Programs" (PDF). In Franz Baader; Andrei Voronkov (eds.). Proc. 11th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). LNAI. Vol. 3452. Springer. pp. 332–346.
- Adam Koprowski; Johannes Waldmann (2008). "Arctic Termination ...Below Zero". In Andrei Voronkov (ed.). Rewriting Techniques and Applications, 19th Int. Conf., RTA-08 (PDF). Lecture Notes in Computer Science. Vol. 5117. Springer. pp. 202–216. ISBN 978-3-540-70588-8.
System descriptions of automated termination analysis tools include:
- Giesl, J. (1995). "Generating Polynomial Orderings for Termination Proofs (system description)". In Hsiang, Jieh (ed.). Rewriting Techniques and Applications, 6th Int. Conf., RTA-95 (postscript). LNCS. Vol. 914. Springer. pp. 426–431.
- Ohlebusch, E.; Claves, C.; Marché, C. (2000). "TALP: A Tool for the Termination Analysis of Logic Programs (system description)". In Bachmair, Leo (ed.). Rewriting Techniques and Applications, 11th Int. Conf., RTA-00 (compressed postscript). LNCS. Vol. 1833. Springer. pp. 270–273.
- Hirokawa, N.; Middeldorp, A. (2003). "Tsukuba Termination Tool (system description)". In Nieuwenhuis, R. (ed.). Rewriting Techniques and Applications, 14th Int. Conf., RTA-03 (PDF). LNCS. Vol. 2706. Springer. pp. 311–320.
- Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S. (2004). "Automated Termination Proofs with AProVE (system description)". In van Oostrom, V. (ed.). Rewriting Techniques and Applications, 15th Int. Conf., RTA-04 (PDF). LNCS. Vol. 3091. Springer. pp. 210–220. ISBN 3-540-22153-0.
- Hirokawa, N.; Middeldorp, A. (2005). "Tyrolean Termination Tool (system description)". In Giesl, J. (ed.). Term Rewriting and Applications, 16th Int. Conf., RTA-05. LNCS. Vol. 3467. Springer. pp. 175–184. ISBN 978-3-540-25596-3.
- Koprowski, A. (2006). "TPA: Termination Proved Automatically (system description)". In Pfenning, F. (ed.). Term Rewriting and Applications, 17th Int. Conf., RTA-06. LNCS. Vol. 4098. Springer. pp. 257–266.
- Marché, C.; Zantema, H. (2007). "The Termination Competition (system description)". In Baader, F. (ed.). Term Rewriting and Applications, 18th Int. Conf., RTA-07 (PDF). LNCS. Vol. 4533. Springer. pp. 303–313.
External links
- Termination Analysis of Higher-Order Functional Programs
- Termination Tools mailing list
- Termination Competition — see Marché, Zantema (2007) for a description
- Termination Portal