Talk:Halting problem
![]() | This ![]() It is of interest to the following WikiProjects: | |||||||||||||||||||||||||||
|
This page has archives. Sections older than 90 days may be automatically archived by Lowercase sigmabot III when more than 5 sections are present. |
Misleading sentence?!
[edit]The article states "This proof is significant to *practical computing efforts*, defining a class of applications which no programming invention can possibly perform perfectly." which does not make sense because all practical computing has to be performed with computers that have finite memory.
Later the article correctly states "The halting problem is theoretically decidable for linear bounded automata (LBAs) or deterministic machines with finite memory." and all real computers are linear bounded in this sense.
Of course, the technique to check for reoccurring memory patterns does not make the halting problem tractable, but Turing's theoretical result does, strictly speaking, not apply to "practical computing efforts".
ClassA42 (talk) 13:40, 29 May 2024 (UTC)
I have implemented a correction myself. ClassA42 (talk) 15:56, 31 May 2024 (UTC)
Inconsistency over origin of Halting problem
[edit]The opening paragraph tells us:
Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program–input pairs cannot exist.
Later we read:
"The halting problem was so named (and it appears, first stated) by Martin Davis... (It is often said that Turing stated and proved the halting theorem in 'On Computable Numbers', but strictly this is not true)."
So we have a contradiction (via good references) within this article. Also no mention of Halting by Andrew Hodges etc.
The reason for this is that the article does not discuss what Turing actually proved in 1936 (although Davis has written on this). In fact Turing proved two statements: "the Diagonalisation Argument" (not actually named) and then the "Printing Problem". Later proofs were reduced to this Printing Problem, in the way that nowadays would be reduced to the Halting problem.
However Davis has made the point (and I generally agree) that Turing's Diagonalisation proof is not in the same logical recursion class as the Halting problem: these are slightly different results. This is because Turing's 1936 paper is not exactly the machine model that was later adopted by Davis, Kleene etc.
All this needs to be properly explained, and Wikipedia doesnt do it. RoyMWiki (talk) 17:38, 18 April 2023 (UTC)
- I don't see any contradiction. First we have a general statement, and then a clarification (in the history section) that Turing's presentation of the problem is not the modern one. The modern formulation follows trivially from the first of Turing's proofs that "no computing machine exists that can decide whether or not an arbitrary computing machine (as represented by an integer) is circle-free". The reason it is not "strictly true" that Turing proved it is really just terminology - the modern term "halting problem" and associated program and input formulation was not around in Turing's time. So strictly speaking he didn't write about anything called the halting problem.
- But morally, Turing did prove it. I disagree with you when you say "Davis has made the point (and I generally agree) that Turing's Diagonalisation proof is not in the same logical recursion class as the Halting problem". Davis did not say such a thing in his book, and Turing's first proof and Davis's proof that there exists a Turing machine with unsolvable halting problem are pretty similar. As noted on Turing's proof, his first proof is not a traditional "diagonalization" argument, rather a proof by contradiction of assuming computability and applying the program to itself. Similarly Davis's proof applies the program to itself and achieves a contradiction of computability. Davis's proof uses a Godel numbering, pretty similar to Turing's conversion between symbol strings and integers. They are substantially the same proof. Indeed Davis says in his introduction "Another result (the unsolvability of the halting problem) may be interpreted as implying the impossibility of constructing a program for determining whether or not an arbitrary given program is free of 'loops'." The "loop" term of course is a reference to Turing's original terminology of circle-free. Mathnerd314159 (talk) 21:00, 18 April 2023 (UTC)
- After some searching I found a recent paper on the subject. Apparently the circle-free theorem ("satisfactoriness" in the paper) is actually equivalent to the universal halting problem, and is of higher complexity than the halting problem. But Turing's second "printing problem" is of the same degree of unsolvability as the halting problem. In particular, there is a transformation that takes halting programs to specific-symbol-printing programs and non-halting programs to programs that don't print a specific symbol, and similarly the reverse transformation from specific-symbol to halting. So I got the theorem reference wrong. But the main argument that Turing's proof is morally equivalent to Davis's still applies. I guess there is still some clarification to do in explaining that Turing proved that a variation of the halting problem was undecidable. Mathnerd314159 (talk) 00:22, 19 April 2023 (UTC)
- Thanks for these replies, and for finding that new paper which closely relates to my points. I am new to Wikipedia Editing so only make comments at the moment hoping that someone else would rewrite. An issue this discussion opens is that Wikipedia technical articles need to do two jobs: (1) Introduce the subject matter (e.g. halting, Turing Machine) for a general audience; and (2) make correct encylopedic and hopefully authoritative statements and definitions for a serious audience. Sometimes this cannot be done without doing some (original?) research on the literature.
- So Turing clearly introduced a machine model and the limitation argument on them. Penrose might perhaps argue that the moral origin of that proof technique is with Cantor, but clearly Turing (as opposed to Post, etc) initiated this work for machines. The contradiction that I refer to indicates to me that the author(s) of this (and most Turing Machine) articles were simply unaware of these subtlities reducing the value of these Wikipedia articles. A naive question is: did Turing originate the (textbook) halting proof or didnt he? A mathematical question might be: so what did Turing actually prove and what did the Halting Theorem prove and who proved that theorem? The answer to that question is outlined in your quoted paper - but not in any Wikipedia article I can find. Incidentally I am not clear from a first reading of that paper when the result that SATIS > HALT was first presented. I found (effectively) this result in a footnote to an article by Martin Davis in a 1988 Book "Universal Turing Machine". Hodges 1984, for example, does not explain this as might have been expected from such a detailed technical biography of Turing and his work.
- I put some related remarks online in another forum in 2019 https://cstheory.stackexchange.com/questions/36576/where-does-the-modern-canonical-version-of-the-turing-machine-come-from/42250#42250 .
- Incidentally you might see from my own reference that I would change the emphasis from your quoted paper by saying that Davis and Post had decided by the 1950s to adopt Emil Post's 1947 model, rather than Turing's 1936 model, which is why they and not Turing stated and proved the Halting theorem. RoyMWiki (talk) 10:05, 19 April 2023 (UTC)
- Edit: Davis and Kleene used Post's 1947 model, which now became the definitive model presented in all textbooks under the title "Turing Machine". RoyMWiki (talk) 10:10, 19 April 2023 (UTC)
- So, https://www.google.com/books/edition/What_Can_Be_Computed/p26YDwAAQBAJ says
In his seminal 1936 “On computable numbers” paper, Alan Turing focused on a variant of the halting problem. (pg. 126)
Let’s now debunk a common misconception about Turing’s paper. It’s often stated that Turing proved the undecidability of the halting problem. But Turing never even defined the concept of halting, and he certainly never proved anything about it. What he did prove is a closely related idea: in §8 of the paper, he proves that the question of whether a machine is circle-free is undecidable. Circle-free machines don’t terminate, but some circular machines don’t terminate either. So although there is an easy reduction from the circle-free problem to the halting problem (as described in the previous paragraph), these problems are not the same. Nevertheless, it’s clear that Turing already had a deep understanding of undecidability. For example, Turing does explicitly prove the undecidability of at least one other problem in his §8: this is the question of whether a given machine ever prints a “0”. And Turing’s proof works almost verbatim for proving the undecidability of many other problems. So Turing probably knew that undecidability is a widespread phenomenon. (pg 323-324)
- That seems like neutral phrasing. So my plan is use "a variant of the halting problem" in the lead and then the explanation of the various related problems and the common misconception debunking in the body. Mathnerd314159 (talk) 02:07, 21 April 2023 (UTC)
- Thanks for another new reference. The challenge is to explain all this in a way which is fully comprehensible and correct. I actually have a slight issue with the references to the Printing Problem, but before we get to that I would like to summarise some of the basic logic results using terms from the 2021 paper.
- Problem P is decidable <==> P is in 0 Turing Degree class;
- Problem P is undecidable <==> P is in a higher degree class (e.g. 0', 0" and higher) and P cannot be solved/decided by an algorithm;
- HALT is 0' complete. (Proved by Davis/Kleene).
- SATIS is 0" complete (Earliest known reference Davis 1988, also in the 2021 paper) SATIS is Turing's actual machine limitation result, but not expressed in modern logic terms in 1936. Thus SATIS is undecidable as proved by Turing.
- Davis-PRINT = HALT is again 0';
- Turing-PRINT = SATIS is 0" - so undecidable to a higher degree. Turing did not show that Turing-PRINT was equal to HALT (0') because he had no means to do so, and Davis 1988 does not accept that Turing's Proof is a correct reduction for that proof also.
- Informally the reason why Turing's results belong to this higher degree class is because his prefered outputs are infinite strings, rather than the finite strings output by a terminating (Post) machine. So they demand infinite searches, which bumps the degree level up by one. RoyMWiki (talk) 11:36, 21 April 2023 (UTC)
- I am confused why you say Davis-PRINT and Turing-PRINT have different degrees, and what these decision problems are precisely. Davis 1988 has a "general printing problem" of whether a Turing machine starting with a tape prefilled with some symbols will ever print 0, and similarly David 1958 the phrasing is "determining, of a given instantaneous description a of a Turing machine Z, whether or not, in the course of its “computation” beginning with a, the symbol Si ever appears on the tape of Z". There is also a "blank printing problem" of whether a Turing machine, starting with a blank tape, ever prints a given symbol (e.g., 0) during its (finite or infinite) execution. Salvador 2021 and Davis 1988 both state Turing showed that the blank printing problem cannot be solved by any general algorithm (i.e., is undecidable), hence I would assume that the blank printing problem is Turing-PRINT. But the blank printing problem is Turing degree 0', so this would contradict your statement that Turing-PRINT is 0''. (Incidentally, from what I can tell, the general printing problem is Turing equivalent to the blank printing problem, hence also 0'). I guess what you're saying is that, since Turing in his proof reduced the blank printing problem to SATIS, Turing only showed the printing problem had Turing degree greater than 0 but less than or equal to 0''. This doesn't make the printing problem itself a higher degree of undecidable though, it's still 0'. Mathnerd314159 (talk) 16:01, 21 April 2023 (UTC)
- Good points, this is where the topic becomes a little unreferenced and potentially controversial.
- (1) Davis 1958 proves that the Printing problem for a Terminating machine is 0', by reduction to Halting.
- (2) Davis 1988 is examining Turing 1936 directly. He points out that Turing-PRINT is not reducible to 0", so creates a new diagonal argument to "replace" Turing's faulty argument. Davis generates a contradiction, and concludes that there can be no algorithm for the general printing problem. Has Davis proved (or even stated?) via this argument that General Printing is 0' ?
- (3) So for me there are two novel issues in this Davis 1988 article. First that Turing did not prove the Halting problem itself, because his machine model construction was more general (not discussed anywhere else for many years). Second that Turing "made a mistake" in his Printing Theorem derivation - I have not encountered any claim that any of Turing's 1936 proofs do not work before.
- So Davis does not say explicitly that Turing only proved that Printing was 0", although that is one conclusion from the section. Also did Turing make a mistake here? More simply is there some reason why Turing's 1936 model cannot have a 0' General Printing proof? (Turing might claim that he was simply rephrasing SATIS in a manner more useful for proving the later theorems, not establishing something genuinely different.)
- At first glance for Turing's General Printing problem not to be 0' would seem to contradict Davis's standard proof of Printing. However it indeed is the case that these classes 0, 0', 0" are logically different for a reason. In particular the fact that SATIS is 0" and not 0' means that the Turing 1936 model has more versatility than the later Post-1947 model in our textbooks.
- Now this is rather a large topic which take us to Turing's AI work, and to Limit-Computation (qv) - it takes us ever closer to "original research" questions, like those in Quantum Computation. RoyMWiki (talk) 11:37, 22 April 2023 (UTC)
- I think you are misunderstanding "reducible". By definition of Turing degree, any decision problem is Turing-reducible to any other problem of the same Turing degree or higher. What Davis 1988 states in footnote 5 is that the circle-free problem (SATIS) is of degree 0'' and hence not reducible to either of the printing problems (the blank printing problem Turing-PRINT or the general printing problem Davis-PRINT) as they are of lower degree 0'. But, since the printing problems are of lower degree, the printing problems can be reduced to the circle-free problem without issue, as Turing did in his proof.
- And I see now that you have this idea discussed your SE post that Post's model model differs from Turing's model. But as far as I can tell, there is only one definition of machine model in play here, the Turing machine. It is simply the associated decision problems that are differently posed. A non-halting Turing machine is still a Turing machine.
- I think we've discussed this enough, I'll edit the article in the next few hours. Mathnerd314159 (talk) 17:15, 22 April 2023 (UTC)
- OK. I agree that this discussion is too long, and I have gone off topic. Perhaps it could be archived or eventually deleted?
- I am confused why you say Davis-PRINT and Turing-PRINT have different degrees, and what these decision problems are precisely. Davis 1988 has a "general printing problem" of whether a Turing machine starting with a tape prefilled with some symbols will ever print 0, and similarly David 1958 the phrasing is "determining, of a given instantaneous description a of a Turing machine Z, whether or not, in the course of its “computation” beginning with a, the symbol Si ever appears on the tape of Z". There is also a "blank printing problem" of whether a Turing machine, starting with a blank tape, ever prints a given symbol (e.g., 0) during its (finite or infinite) execution. Salvador 2021 and Davis 1988 both state Turing showed that the blank printing problem cannot be solved by any general algorithm (i.e., is undecidable), hence I would assume that the blank printing problem is Turing-PRINT. But the blank printing problem is Turing degree 0', so this would contradict your statement that Turing-PRINT is 0''. (Incidentally, from what I can tell, the general printing problem is Turing equivalent to the blank printing problem, hence also 0'). I guess what you're saying is that, since Turing in his proof reduced the blank printing problem to SATIS, Turing only showed the printing problem had Turing degree greater than 0 but less than or equal to 0''. This doesn't make the printing problem itself a higher degree of undecidable though, it's still 0'. Mathnerd314159 (talk) 16:01, 21 April 2023 (UTC)
- Edit: Davis and Kleene used Post's 1947 model, which now became the definitive model presented in all textbooks under the title "Turing Machine". RoyMWiki (talk) 10:10, 19 April 2023 (UTC)
- After some searching I found a recent paper on the subject. Apparently the circle-free theorem ("satisfactoriness" in the paper) is actually equivalent to the universal halting problem, and is of higher complexity than the halting problem. But Turing's second "printing problem" is of the same degree of unsolvability as the halting problem. In particular, there is a transformation that takes halting programs to specific-symbol-printing programs and non-halting programs to programs that don't print a specific symbol, and similarly the reverse transformation from specific-symbol to halting. So I got the theorem reference wrong. But the main argument that Turing's proof is morally equivalent to Davis's still applies. I guess there is still some clarification to do in explaining that Turing proved that a variation of the halting problem was undecidable. Mathnerd314159 (talk) 00:22, 19 April 2023 (UTC)
Halting Problem: There's a mathematical concept called the Halting Problem, which proves there's no general way to know if any program will halt (finish) or run forever. However, this doesn't mean true infinite runs exist, just that predicting them is difficult.
[edit]I don't know that i am writing correct or incorrect so sorry if there is any inconvenience with my further response . Ad we all know here problem is about a software program that will run infinitely or it will terminate, according to me any program will run infinitely until unless we provide them enough storage and enough power energy to run. here we can take a ai robot as a refence because in this also anyhow we use program only and we know ai robots work until we don't destroy it or stop it to work. We can take example of an laptop that is developed and manufactured after that just keep it somewhere only after using once but the system , program any operation will work as it was working in using it first time. It will not terminate not terminate itself any how unless we didn't programed it to terminate. (The program which learn and update like an ai tool will never terminate it will run infinitely & the program which do not upgrade by itself will be terminated but it will also run for a long period of time). Deepesh150 (talk) 13:07, 13 March 2024 (UTC)
Moreover, the definition of g is self-referential. A rigorous proof addresses these issues
[edit]Errr, why does this sentence exist? The "rigorous" proof is still self-referential, the self-reference is just passed in through the variable i of e(i), instead of simply being defined as a static self-reference in e. Seems like an unnecessary claim. Dart200 (talk) 04:12, 13 August 2024 (UTC)
- That's exactly the point - in the rigorous proof sketch, the counterexample program (g / e) does not use itself in the body. Whereas in the proof sketch, translating the reference to g in "if halts(g)" requires a lot of theory on how to interpret self-reference. Does this actually make the proof more rigorous? Hard to say, but it certainly makes it more self-contained.
- If you want a really rigorous proof you can look at Lean, there they use the function fixed_point₂ which is a variation of Rogers's fixed-point theorem. Mathnerd314159 (talk) 12:53, 13 August 2024 (UTC)
The halting problem is theoretically decidable for linear bounded automata
[edit]You have correctly argued that in the real world a computer can be in so many states that you can't try all the states because it takes too long. On the other hand, you are very generous in finding an algorithm that has to process an infinite amount of data. You seem to find a single input that cannot be processed by such an algorithm, a simple paradox. What does this say about whether there could be an algorithm for reality that can process a finite subset of this data - the set of all algorithms occurring in reality? NOTHING! The halting problem proves nothing here! On the one hand, you are very strict and complain that a small and a large natural number are being confused here. On the other hand, you are very generous and consider it appropriate to confuse a finite number with an infinite number!