Talk:Termination analysis

Applications

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?

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

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 2^1,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. ~ Jafet • business • pleasure • voicemail 11:16, 25 September 2008 (UTC)

Adjacent to these concerns about being misleading is the quote "As of 2023, it is still unknown whether this C-program terminates for every input; see Collatz conjecture" when displaying a C-program that implements the function of study in the Collatz conjecture. However, there is a possible source of confusion here as the program takes a single variable of type int. In all C implementation the space of possible ints is finite and so halting can be solved by exhaustion (albeit at great computational expense). If one wants to use the Collatz conjecture as a learning tool may I suggest using a programming language that implements arbitrary sized ints (for example JavaScript) so that the posed halting question is actually equivalent to the Collatz conjecture.

missing info

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

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

"Terminating computation" redirect page

@Jochen Burghardt: I recently added a link to "terminating computation" on this page, but the target of this redirect page seems to be incorrect. Should "terminating computation" be redirected to a different article to avoid this confusion? Jarble (talk) 21:24, 28 January 2019 (UTC)

I think both words are used here in there common sense, so they need not necessarily be explained. Maybe, "terminating" is a foreign (Latin?) word, and could be simplified to "halting" or "finishing" or "coming to an end". There is an article computation that could be linked, but it appears to have a philosophical rather than a computer-science view. I also checked algorithm, but while it uses "run-time" and "execution", it never explains that an algorithm is run (or executed) on a computer, let alone explaining that this process usually should finish with a result, after some reasonable amount of time (to explain this would be the main purpose of adding a link, I think). - On the other hand, termination analysis is an issue of theoretical computer science, so we can expect a reader will known the most basic facts about algorithms and their execution. - Jochen Burghardt (talk) 21:47, 28 January 2019 (UTC)

Reformulation of the introduction

I have reformulated the introduction because
- it is unclear what is meant with "definitely" in formal terms (=> program will definitely terminate) ;
- it is the Totality Problem instead of the Halting Problem which matters here;
- being (not) "total" is a property of functions but not of programs (=> "termination analysis cannot be total");
- there is no evidence about the performance of humans in (dis)proving termination.
Jack Rusell (talk) 16:34, 30 November 2019 (UTC)

Example C program

You should mention bignum is used... because it's easy to work out all 32-bit or 64-bit integer inputs... Maybe using language like Python? — Preceding unsigned comment added by 93.75.21.51 (talk) 02:08, 29 March 2020 (UTC)

done 109.243.1.42 (talk) 11:52, 14 October 2024 (UTC)

Example software

Would it be relevant to have a list, in this page, of known software that does termination analysis? My leading candidates are https://dafny.org/ and https://cacm.acm.org/research/alloy/ and https://en.wikipedia.org/wiki/Coq_(software), but I have no advice to give about chosing between them.

2404:4404:3722:8700:CC11:E02:B0D7:639E (talk) 22:48, 21 November 2024 (UTC)