Talk:Termination analysis

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Computer science  
WikiProject icon This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
 ???  This article has not yet received a rating on the project's quality scale.
 ???  This article has not yet received a rating on the project's importance scale.
 

Applications[edit]

I think this article is missing motivations for performing termination analysis. What are the benefits of finding out whether a program terminates? For example, are there compiler optimizations making use of this fact? Can the information be used to rule out faulty programs? - (Signature supplied from revision history:) 46.5.181.43, 19 June 2015‎

I agree, and try to indicate some motivations, however, yet without sources.
(1) The software controlling an embedded system often has the form of an outer loop which repeatedly executes some inner code to react to actual sensor inputs. in order to react in time, it is essential that the inner code terminates under every circumstances (, and within a guaranteed maximum-time bound). Think of a car driving at 60 mph with the inner code computing the break control getting stuck in an endless loop, thus preventing the following code for computing the steering control from being executed (at all, let alone in time).
(2) A compiler, run on an however weird input, should always terminate.
(3) If a text processing program calls an internal subroutine that doesn't terminate, it won't read any more user input. From the user's point of view, the program is "hanging", and has to be terminated manually via the operating system, often resulting in loss of the more recent unsaved edit operations. - Jochen Burghardt (talk) 18:42, 19 June 2015 (UTC)

Only valid answers?[edit]

The assertion that the only valid answers are "definitely terminates" or "don't know" is patently false and a misinterpretation of the Halting Problem. Consider a simple program:

010 GOTO 010

Trivially, this program will never terminate. What must be true is that any given method must have at least one program that it cannot determine, and so must any union of finitely many methods. Robert A.West (Talk) 00:00, 1 September 2006 (UTC)

This above^ is why we need some knowledgeable folks to fix this "article". I pulled this definition down today (1 Sept 2006) from the FOLDOC and just pasted it in to get something going.

I was bothered by the following statement too:

"For example, evaluation of a constant is bound to terminate."
  1. I don't quite know what "evaluation of" means.
  2. If "evaluation of" means "to determine" as in "to create" a constant such as pi I don't see why the calculation creating pi has to necessarily terminate
  3. And even if "the method" starts to calculate pi (apparently) successfully, will it erroneously terminate, say after calculating only 1,258,433,705 digits? In other words, do we have an "ineffective" algorithm because of premature termination?

Am I missing something obvious here? wvbaileyWvbailey 02:47, 1 September 2006 (UTC)



If someone wants to "unstub" this article feel free to contact me. I am part of the AProVE project (http://aprove.informatik.rwth-aachen.de) and might be able to explain details and important facts. cotto@i2.informatik.rwth-aachen.de —Preceding unsigned comment added by 137.226.108.169 (talk) 22:50, 29 March 2008 (UTC)


Misleading statements[edit]

It's my turn to be bothered, please take a look at these statements:

"Because the Halting Problem is undecidable, termination analysis cannot work correctly in all cases."

"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."

"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."

I think these statements reveal a very common lack of understanding of the Halting Problem. The Halting Problem is only a problem for "imaginary" computers (Turing machines), with infinite memory, which don't exist in real life and never will.

It's theoretically possible to prove whether a program-input pair will terminate, for all programs and inputs, as long as we limit its memory usage. The problem is that the currently known (and naïve) way of doing this requires exponential amounts of memory compared to the original algorithm.

So it's true that currently there is no known practical algorithm that solves this problem for all cases, but that doesn't mean that there never will be one in the future. In other words, there might be an algorithm that could answer "this program will halt with this input" or "this program will not halt with this input" or "this program will exceed 10 TB of memory usage with this input", for any given program-input pair.

So, saying that "termination analysis cannot work correctly in all cases" and "research in this field cannot reach completeness" is a bit misleading, to say the least.

193.126.142.107 (talk) 02:42, 11 September 2008 (UTC)


This is a very interesting comment, but I think you may be missing something. My first guess is that the algorithms in question can actually assume infinite memory -- and usually do. Most programs leave the problem of memory to the operating system -- virtual memory (hard-disk memory swapping) is employed to deal with the memory filling up, but out-of-memory errors can still occur, which means the operating system (or a virtual machine environment like Java) has stepped in from outside an algorithm and stopped it. This kind of behaviour is not part of the algorithm analysis, even though "the algorithm stopped".
The following section from the Halting problem article may be relevant.

The halting problem is, in theory if not in practice, decidable for linear bounded automata (LBAs), or deterministic machines with finite memory [note from Robertbyrne: note that the definition of an LBA gives a technical mathematical meaning to "finite memory" in this case, and it's not a simple number of spaces for symbols]. A machine with finite memory has a finite number of states, and thus any deterministic program on it must eventually either halt or repeat a previous state:

"...any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine..."(italics in original, Minsky 1967, p. 24)

Minsky warns us, however, that machines such as computers with e.g. a million small parts, each with two states, will have on the order of 21,000,000 possible states:

"This is a 1 followed by about three hundred thousand zeroes ... Even if such a machine were to operate at the frequencies of cosmic rays, the aeons of galactic evolution would be as nothing compared to the time of a journey through such a cycle" (Minsky p. 25)

Minsky exhorts the reader to be suspicious -- although a machine may be finite, and finite automata "have a number of theoretical limitations":

"...the magnitudes involved should lead one to suspect that theorems and arguments based chiefly on the mere finiteness [of] the state diagram may not carry a great deal of significance" (ibid).
For more on this issue of "intractability" see the article Busy beaver.


I think the area of model checking is also relevant here. It works well for hardware, where finite space is assumed in the algorithm specification, but is merely one of the many incomplete solutions to general algorithm verification because of the assumption of infinite space.
Robertbyrne (talk) 02:46, 22 September 2008 (UTC)
Right, what you quoted made half of my point. The other half of my point is that this article is misleading (or at least incomplete). Nowhere it says that termination analysis is only applicable to Turing machines.
So my point still stands: the sentences I quoted, such as "termination analysis cannot work correctly in all cases" and "research in this field cannot reach completeness" are incorrect when it comes to termination analysis on deterministic machines with finite memory (i.e. LBAs, or "computers" as I like to call them).
193.126.142.107 (talk) 02:39, 25 September 2008 (UTC)
A decider, given n bits of state, cannot solve the halting problem for an arbitrary program that requires at least n bits of state. ~ Jafetbusinesspleasurevoicemail 11:16, 25 September 2008 (UTC)

missing info[edit]

At what stage of the compilation does termination analysis take place ? Any variation ? --81.84.152.156 (talk) 22:57, 10 May 2010 (UTC)

Strange comment[edit]

"Some types of termination analysis can automatically generate or imply the existence of a termination proof." - a termination analysis tool, by definition, has to be able to generate or imply the existence of either a termination or a non-termination proof (when it succeeds). Hence, I do not understand the point of this sentence. (One could speculate on a tool which "magically" knows a result without even implying a proof for it, but such a tool would not be accepted by the scientific community). Perhaps the writer of this sentence intended to write about certifiable termination provers? AmirOnWiki (talk) 12:54, 4 October 2015 (UTC)