# Talk:Termination analysis

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)

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)