Talk:Halting problem/Archive 2
This is an archive of past discussions about Halting problem. Do not edit the contents of this page. If you wish to start a new discussion or revive an old one, please do so on the current talk page. |
Archive 1 | Archive 2 | Archive 3 | Archive 4 | Archive 5 |
Formal Statement
This definition is not explicit enough. For example, you speak of a Gödel numbering yet later you have a symbol . What does the subscript mean? Also, what are i and x ? Based on the definition of the Cantor Paring Function, i and x are natural numbers. Yet the Gödel numbering of the computable functions, by definition, I presume is a funtion whose domain is the computable functions. Yet i and x are not "functions" based on how the Cantor Pairing Function is defined. Please clarify and make the defintion make mathematical sense. Otherwise, I can't figure out what you mean!
Importance and Consequences
Is this really that important? All these undecidable problems seem to rely on being able to use pathological cases where calculating the answer relies on already knowing the answer (passing the halting decider to itself as an argument)? Is this of any use to non-pathological cases?
- Yes. Rice's Theorem, which follows from the Halting theorem, says that almost no properties of a program can be deduced from static analysis. So, to pick one of many examples, you cannot tell just from looking at the source code of programs whether they will perform out-of-bounds array accesses, or raise exceptions. -- Dominus 06:17, 30 May 2007 (UTC)
Note that this theorem holds for the function defined by the algorithm and not the algorithm itself. It is, for example, quite possible to decide if an algorithm will halt within 100 steps, but this is not a statement about the function that is defined by the algorithm.
Sorry, what? Interested layman here -- "this is not a statement about the function that is defined by the algorithm?" I'm not contesting this, just saying a little more explanation or a reference to something explaining it would be nice. Seems on the surface that the function defined by an algorithm and the algorithm should be pretty similar.
The last few sentences of the first paragraph, where the general method of proving a language is undecidable is explained, are not clear enough. A possible clarification may be identifying what exactly "new problem" and "old problem" refer to.
Cantor pairing function
does (i, x) have to be the Cantor pairing function or just a pairing function, and why? If it has to be the Cantor function, the question of why would be useful to readers of the article.
A simpler presentation? And add a useful reference.
A presentation of Cantor's "pair" at the very beginning is pretty daunting. Why not just describe Turing's original argument? Although he uses what looks like a diagonalization process, Turing himself rejected diagonalization as a good demonstration of his proof. What he ended up with is a mechanistic demonstration that doesn’t require knowing hardly any math at all. Other authors have struggled to present his proof in different ways, including Minsky, who states that “The result of the simple but delicate argument … is perhaps the most important conclusion in this book. It should be contemplated until perfectly understood.” He goes on to observe that it is similar to “Russell’s paradox. “It is also related to the argument of Cantor, that one cannot “count” the real numbers. In fact the unsolvability of the halting problem is usually demonstrated by a form of Cantor’s ‘diagonal method.’ We prefer the present form because it suppresses the ‘enumeration’ required for the diagonal method.” (page 149, Minsky, Marvin L. Computation Finite and Infinite Machines, 1967, Prentice-Hall, NJ). Minsky uses a different argument, somewhat like Turings.
Turing himself didn’t mention “halting”; this must have come later. In fact he wants his machines do quite the opposite. For clarity and cleverness, Turing’s original proof is where I always return when I am confronted with “the halting problem.” It can be found reprinted (along with papers by Godel, Rosser, Kellene and Post) in "The Undecidable, Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions", edited by Martin Davis, Raven Press, N.Y. 1965.
Turing’s proof begins with a definition of a number as “computable if its decimal can be written down by a machine.” Turing then describes a typewriter-like mechanical device consisting of a table of instructions (what we now call a finite state machine) operating on a paper tape that can move left or right one square at a time. At each “square”, the table can “scan” (read, observe) a symbol or a blank and either write a symbol or erase a symbol. Turing calls the symbols 1 and 0 “symbols of the first kind” and others—e.g. letters, other numerals, etc— “symbols of the second kind”. He calls a machine that prints on its tape only a left-hand decimal-point and 1’s and 0’s, a “computing machine”. Finally he defines as “circular” a machine that (i) “never writes down more than a finite number of symbols of the first kind” (1’s and 0’s), (ii) reaches a state (what he calls a “configuration”) from which there is no “move”, or (iii) it goes on moving and perhaps printing symbols of the second kind but no more 1’s and 0’s.
Note this odd definition indicates that a circle-free machine is one that goes on printing 1’s and 0’s forever (!) Turing goes on to show how to reduce a table of instructions to an Arabic numeral, and this he calls the “description number” of a machine M. He defines as “satisfactory s” such a number that results in a circle-free machine—it goes on calculating the decimal forever— and “unsatisfactory u” such a number that results in a circle.
Turing then demonstrates the existence of a so-called "universal" machine "U", that is, a single table of instructions that can "run" the description number of any machine M present on its tape and compute the same sequences as M. [Note how close Turing was to the modern concept of a computer.] By various arguments and demonstrations, Turing takes great pains to show that all these premises and definitions to be reasonable and true.
The proof is of the form: “the assertion that H exists and is true and H implies “u” or “s” but not both, but in reality “not u” and “not s”” implies H is not true: [H & (H -> (u XOR s)) & (~ u & ~ s)] -> ~H
Turing begins with an assertion of "H" (made of universal machine U and the number equivalent to a machine D) that can test any integer N on the tape and determine whether or not N represents a “circle free” machine. This H marks the number-under-test with “u” (unsatisfactory) or “s” (satisfactory) and keeps a tally “R” of how many numbers have been satisfactory. He then asserts H itself to be "circle-free"—that is, it prints a decimal point and continues to print 1’s and 0’s ad infinitum.
What is this number computed by H? It is easiest to see with an example: Suppose H has tested numbers 1 through 1326, and so far 17 of them have been “successful”. Then if the next number, e.g. 1327, is successful, the tally R becomes “18” and H will print the 18th “figure” (i.e. 1 or 0) computed by this "successful" number. Then H continues to the next number 1328. In all cases H, either (i) delivers the verdict “u” that the number-under-test is unsatisfactory or (ii) delivers the verdict that the number-under-test is satisfactory and printing the Rth figure, and always (iii) continues onward to the next number.
But what happens when H encounters its own description number K? Machine H must yield a verdict of "u" or "s" in a finite number of steps. It cannot yield “u” (unsatisfactory) because of our accepted assertion that H is circle-free— that is, it always goes on computing and printing the “figures” of a decimal number ad infinitum. Thus K must be satisfactory. But is it? What happens when H tests K? H must observe as “the machine known as K” does what H has been doing, i.e. testing numbers 1 through K-1. But eventually H observes that “the machine known as K” arrives at K again, and again it must proceed to test the numbers 1 through K-1, AND AGAIN ... Poor H never gets to write down the R(K)-th figure. It is in a circle, and by definition H is unsatisfactory. But this contradicts our assertion, and the proof has shown that no such H actually exists.
This proof is very subtle. It requires some time to assimilate. Don't blow it off as "archaic" because it doesn’t mention “halting”. The proof has nothing whatever to do with "halting", as in "when M arrives at the HALT instruction all machine motion ceases." Turing never mentions "HALT", at least that I can find in the original paper. “So what?” you wonder? Well, how can a machine looking for HALTs not halt when it hits one?? Are authors' reinterpretations of Turing theorem as a "halting problem" actually good proofs? Suppose the machine M testing for "HALT" runs into a HALT? It must HALT. It’s just a machine. It does what it is told. It will not recover. There's no UN-HALT instruction. No watch-dog timer will knock it out of its HALT state. No uber-observer-machine will keep it going.
Turing cannot allow his machines to “halt”; they must either get into a “tight loop” or not. So he describes machines that have only the following instructions, and no others: “R” (move tape right one square), “L” (move tape left one square), “Ps” (print symbol s in the observed tape-square), “E” (erase symbol in the observed square), “jump to instruction p if symbol s is in the observed square”, “jump to instruction q if no symbol is in observed square”, “jump to instruction r if any symbol is in observed square.” More often than not he puts two or three instructions on the same "line" together with the multiple-branch structure of a finite-state machine.
We have to remember that this Turing machine is supposed to be a real machine. Some authors describe super-simple versions of the Turing machine somethimes called POST machines [after Emil POST's description in an important paper of Turing’s era; see similar descriptions in Penrose's Emporer's New Mind, and Martin Davis's little paper 'What is a Computation 'found in Mathematics Today, Vintage Books, 1980.] Years ago I constructed an actual, real low-power CMOS-based POST machine that used only "mark" and "blank" as symbols and only the instructions RIGHT, LEFT, PRINT, ERASE, JUMP-IF-BLANK-to-instruction-aaa-ELSE-next-instruction, JUMP-IF-MARKED-to-instruction-aaa-ELSE-next-instruction, the unnecessary but useful "JUMP-to-instruction-aaa" ... but no HALT. My machine merely achieved HALT by creating a "circle" such as "instruction #37: JUMP-to-instruction 37." This was an interesting exercise, and I was able to write and actually test the universal machine on a simple little "number" that I put on the tape. wvbaileyWvbailey 16:50, 6 January 2006 (UTC)
This page is, in general, pretty much impossible to understand for the layperson. somewildthingsgo 13:19, 8 August 2006
Data dump removal...
This contains a lot of useful information but needs a lot of cleanup before adding to the article. --Robert Merkel 22:04, 5 January 2006 (UTC)
To Mr. Merkel: The whole article is suspect. Read Turing's proof. Actually read it and understand it. Try to find the word "halting." Then go ahead and improve on the various submissions. But don't dump them. And cite your sources. wvbaileyWvbailey 01:36, 6 January 2006 (UTC)
- For your information, I have read Turing's paper. The reason why I copied your material to the talk page is that it obscures the forest for the trees. Think of your readers and try to give them readable context instead of just core dumping every single thing you know about the halting problem, please. --Robert Merkel 04:29, 6 January 2006 (UTC)
- I agree that the above text has some big problems. For one, it's extremely verbose. There's nothing wrong with a detailed description of Turing's proof, but I'm sure we could condense it down using modern terminology and notation to something much more managable. The style of the above is also rather grating, especially the highly informal language, the first-person anecdotal references, and the not-so-widely-accepted need to claim that Turing was not really describing a "halting problem". Deco 04:44, 6 January 2006 (UTC)
- Just to clarify, the present discussion is in reference to the material below. --Robert Merkel 04:47, 6 January 2006 (UTC)
- Oops. That's quite a bit nicer and briefer, but definitely needs some cleanup. Maybe we can add it to the end of the article in a nonprominent position and let it stabilize for a while? Deco 04:55, 6 January 2006 (UTC)
The whole "Halting" entry is suspect. Turing didn't solve "the Halting Problem", he solved the Enscheidungsproblem. What we should be writing here is an encyclopedia entry, not this off-line fussing. You should think about your readers. They come to this site, all ages and experiences, me included, looking for a good exposition on Turing's proof (and certainly, so far, this is the wrong place) and find dreck. It's not accurate. "Verifiable" is the word. So to the entry I add a bunch of references, some actual verifiable historical information, actually tie it to Principia Mathematica and "vicious circles" (gee I wonder why Turing was so interested in "circles"?) and then some thoughts on this page. And somebody strips it out. What I suggest is for some other folks to get constructive and do some work. Like: edit the entry to make it better. Like: tell us what the Turing proof is all about, in their own words, since they've read it.
Deco is right, that is my stuff and it was a first cut. It belongs where it is, on a discussion page. But the comment that the diagonal-proof presentation is "daunting" still stands. What we need is a really good exposition re Turing's first proof written to emphasize the mechanistic bent he brought to it, so an interested young mathematically immature layman can understand it. I've got a really nice analogy/interpretation of it, but why should I submit it to this bullying? wvbaileyWvbailey 07:20, 6 January 2006 (UTC)
Last suggestions: (1) I came to this wiki page with the question: Why is Turing's odd, highly-mechanistic (mechanism-based), fussily-detailed proof so different from all the others I've seen. Is it really? It feels different to an old engineer who’s pretty tuned to this feeling: something is odd here. I didn’t find the answer at this site, nor any references here to help me; the page failed me. And I know enough about TMs to know some it is rubbish. Because I couldn't find the info I wanted on this site I just “deconstructed” the proof myself. But this is not attributable, verifiable work. So I'm not going to put it here. And it didn’t answer my question anyway. I still have that “something’s odd here” feeling. Turing was a brainy guy, and his first proof is too damn sophisticated for no reason.
(2) If you want, just pull the “Simpler Presentation” thing off and trash it. It’s not verifiable to a source anyway. And if wiki-readers don’t have the patience to get through that kind of stuff, then why bother?
(3) Just like any other worthy pursuit we can be proud of we want historical accuracy. Who exactly coined the phrase "halting problem?" Was it Turing? When did it happen? Was it just a confluence of thought between e.g. Turing, Post, Kleene? I bet it was Kleene. He wrote a book (referenced by Booth) called “Introduction to Metamathematics. D. Van Nostrand Company, Princeton N.J., 1952. In the reference I cited he juxtaposed "terminating algorithms" right before his “Church-Turing Thesis.” Post probably put the idea in his head.
(4) Strangely, in the PM reference I cited, in the “Vicious-Circle Principle” sub-chapter, there’s an interesting discussion of the requirement that, to quote “a set has no ‘total,’ we mean, primarily, that no significant statement can be made about ‘all its members.’” (PM, p. 37). Sure sounds like the Rice Theorem to me, also Turing’s muddled discussion immediately following his second theorem. Are these related?
(5) As I've said the introduction of Godel numbers and Cantor pairing functions right at the beginning is off-putting, to say the least. (No wonder people walk away from mathematicians at parties. “Hi, I’m Sam. Let me tell you about my favorite Godel number”) We don’t want to be intimidating our poor readers. Besides I rather doubt that particular formula is “the” formal expression of the halting problem, anyway (who’s the little god who says so?). It may be "a" formal expression. But did help this reader? Not a chance. The halting problem is just what it says: Can a computing machine, algorithm, mechanism, person-as-algorithm, whatever, decide if any old computing machine will halt or not? And the answer is NO, not unless it’s really, really teensy (i.e. dinky finite tape and dinky FSM)… cf Busy Beaver Problems: Cf Booth’s problem #396 “show that the Busy beaver problem is unsolvable…for all values of n[-state machines].”
(6) And the C-geek-speak examples… jeez…. A lot of us can’t speak C. And we don’t want to either, to decipher an entry that doesn't need it (either that, or we know enough to know we hate it). Some of us speak, or used to speak, Basic or Fortran or assembly code (that’s me) or maybe Excel macros on a bad day. The standard formulation (description, model) of “Turing Machines for the masses” can be found most of the references, best of all in the Martin Davis book. The instruction set for “the machine for the masses” is: “L, R, E, P, Jb,instruction_address, Jm,instruction_address, and maybe H.” To remember that “b” is “blank” and “m” is mark (or whatever), and to encode in unary/tally marks, is about all that our dear reader need know and use to understand a Turing Machine-(equivalent). She can "play machine", to demonstrate “halting”, and “circles”, and “machine algorithms”, with some beads and a couple pieces of paper. And this is verifiable/attributable to a zillion sources.
(7) Which brings me to “busy beavers”: something fun for those masses. Maybe a demonstrable example of an unsolvable problem.
(8) And speaking of “The theory of Logical Types” what about transfinite answers to the “Halting Problem?” Turing wrote a paper about this (and “oracles”) which baffles me, although I suspect it has to do with attaching new “truths” to the previous axioms. There seems to be a debate at the wiki entry re “Hilbert’s Problems” whether or not Hilbert’s Problem #2 is solved. Some folks think it’s been solved by transfinite induction. (Hilbert and Kleene, anyway). There’s a discussion of this in Nagel and Newman, page 97 (especially the footnotes). wvbaileyWvbailey 16:51, 6 January 2006 (UTC)
History
- 1900: Hilbert's 17 questions. "Of these, the second was that of proving the cosistency of the 'Peano axioms' on which, as he had shown the rigour of mathematics depended" (Hodges, p.83).
- 1913, 1927: The work of Alfred North Whitehead and Bertrand Russell, published as Principia Mathematica (first edition in 1913 and second edition in 1927), a thoroughly axiomatized logic and arithmetic. To answer the serious problem called "The Vicious Circle Principle" (p. 38 ff) or "Vicious-circle fallacies" (p. 63ff, ibid) they offered up their "Theory of Logical Types" (p. 38ff). It is here that we see perhaps the first, (maybe not the very first — see their footnote p. 37, ibid) of what would, in a few years, become known as "the halting problem." They wrote, famously, that "Whatever involves all of a collection must not be one of the collection" (p. 37, ibid).
- 1930: Godel's theorem
- 1933: Hilbert's 2nd problem is taken up by the young Alan Turing, a doctoral candidate at Cambridge, England (cf Hodges, p. 86).
- 1935: Alonzo Church's paper "An Unsolvable Prolem of Elementary Number theory" presented to the American Mathematical Society, April 19, 1935 (cf the reprinted paper in The Undecidable, p. 89ff).
- 1936: Turing's proof in 1936 -- "On Computable Numbers, with an Application to the Entscheidunsproblem" (reprinted in The Undecidable, p.115)-- answered with three theorems the "Entscheidungsproblem"-- the "Decision Problem": "I shall show that there is no general method which tells whether a given formula U is provable in K [Principia Mathematica], or what comes to the same, whether the system consisting of K with -U adjoined as an extra axiom is consistent" (p. 145, ibid).
- His demonstration proceeded from a detailed proof of the first theorem: that no "computing machine" exists that can decide whether or not a "computing machine" is "circle-free" (i.e. goes on printing its number in binary ad infinitum): "...we have no general process for doing this in a finite number of steps" (p. 132, ibid).
- 1936: Probably the first usage of the word "termination" i.e. "halt" or "stop" applied to "the problem" appeared in Emil Post's brief paper ("Finite Combinatory Process. Formulation I", reprinted on pp. 289-291 in The Undecidable, from The Journal of Symbolic Logic, vol.1,(1936) pp. 103-105). Post was unaware of Turing's work and visa versa (cf Martin Davis's commentary on p. 288 of The Undecidable, ibid).
- In this paper Post describes a "formulation" (i.e. process, not a machine) consisting of "a worker" who follows a "set of instructions" (that, as it turned out, are virtually identical to those of Turing's machines). But Post adds another instruction "(C)Stop". Thus "...This process will terminate when and only when it comes to the direction of type (C)." He called such a process "type 1 ... if the process it determines terminates for each specific problem." He went on to remove the "Stop" instruction when evaluating "symbolic logics"; in this case "a deterministic process will be set up which is unending"[his italics, ibid).
- 1943: In his 1943 paper Stephen C. Kleene discusses "algorithmic theories" ("Recursive Predicates and Quantifiers", reprinted in Undecidable pp. 255ff, reprinted from American Mathematical Society, 1943: Transactions, Volume 53, No. 1, pages 41-73). He states that "In setting up a complete algorithmic theory, what we do is describe a procedure ... which procedure necessarily terminates and in such manner that from the outcome we can read a definite answer, "Yes" or "No," to the question, "Is the predicate value true?" (p. 273, ibid).
Since then a plethora of authors have offered up various demonstrations of the proof of the "Halting problem" (see Davis's "What is a computation?", Minsky, Penrose, and others).
On the history section
While there is some merit to the pont that the article should not jump right into Gödel numbers, a long history section as the first numbered section is even worse. This is an article about mathematics, not about history. The history section should be heavily edited (with a view to, say, halving its length) and moved later in the article. A sentence or two giving historical context at the start of the first numbered section, or even in the lead section, would not be out of place, and the informal description could profitably be expanded before formalities are introduced. --Trovatore 17:44, 7 January 2006 (UTC)
- I've moved the section to the end. The first major edit that comes to mind would be cutting down, or perhaps removing entirely, the long digression on Hilbert's second problem, which is not obviously relevant, except as a problem on which similar methods have been used (code up an appropriate amount of self-reference and diagonalize). Hilbert's second is about whether the consistency of arithmetic can be proved. ("Proved" in what sense? Hilbert doesn't really say; from this translation of his speech it's very unclear what he would or would not have accepted as a proof.) Trovatore
- Now I'm really confused: I've read the 2nd problem from the above link and I read: "But above all I wish to designate the following as the most important among the numerous questions which can be asked with regard to the axioms: to prove that they are not contradictory, that is, that a definite number of logical steps based upon them can never lead to contradictory results".
- What I read here is: (1) the test must decide that the axioms are not contradictory, that is if we tested any well-formed combination of "sentences" of them we would get ...what?.. no (U & ~U) on the left side of the equation. (Am having a hard time parroting this back in my own words): Thus if U is a test and K is any sentence in the axioms and either s or ~s but not both then (U&K) cannot co-exist: (U&K->s) xor (U&K->~s) <-> ~(U&K), correct?, and (2) this has to be done in a finite number of steps (e.g. a Turing machine). All's Turing needed to do was produce one example, and he produced it. My reading of Turing's words indicates to me that Turing himself believed he proved something different than Godel. "...what I prove is quite different from the well-known results of Godel." About Godel's results, Turing says: "It is shown that no proof of consistency of Principia Mathematica (or of K) can be given within that formalism." About Turing's results: "I shall show that there is no general method which tells whether a given formula U is provable in K... etc". RE Godel I'm unsure what he thought he proved. But isn't this what Hilbert wanted to see?
- A proof of the consistency of arithmetic would not necessarily lead to a solution of the halting problem; a solution of the halting problem would lead to a proof of the consistency of arithmetic only if one could in fact prove that it were a solution. But the halting problem is not about whether there's an algorithm that provably decides whether TMs halt, just about whether there's an algorithm that correctly decides it, whether that can be proved or not.
- What did Turing himself say he proved? I quote: "I shall show that there is no general method which tells whether a given formula U is proveable in K [Principia Mathematica], or, what comes to the same, whether the system consisting of K with -U adjoined as an extra axiom is consistent. // If the negation of what Godel has shown had been proved, i.e. if, for each U either U or -U is proveable, then we should have an immediate solution of the Entsheidunsproblem. For we can invent a machine K will prove consecutively all provable formulae. Sooner or later K will reach either U or -U. If it reaches U then we know that U is provable. If it reaches -U, then, since K is consistent (Hilbert and ackermann, p. 65) we know that U is not provable" (Undecidable, p. 145). This reasoning sounds like this: [(K&U -> s)&(K&U)-> ~s] -> ~U which I believe is true. And see the dialog with Trovatore below re the quote from Hodges, p. 111.
wvbaileyWvbailey 03:02, 8 January 2006 (UTC)
- The "1930" section of the history section, on Gödel's famous paper, contains another serious non-sequitur. Reasonable people can disagree on whether Gödel's second incompleteness theorem (roughly, a consistent theory cannot prove its own consistency) resolves Hilbert's second problem, but there's no obvious reason that a proof of the consistency of arithmetic would entail that Zermelo-Fraenkel set theory, or the system of Principia Mathematica, decide all arithmetical statements. --Trovatore 19:05, 7 January 2006 (UTC)
Good stuff above. Note that the Godel quote is in Godel's own words! I agree with the move to the end. I've added more info, but attempted to cut to more succint entries. Will look at Hilbert issue. I moved the periphera out and put into "footnotes". Including quote from Godel's paper. wvbaileyWvbailey 22:14, 7 January 2006 (UTC)
- The Gödel quote is in Gödel's own words, but I don't see that it has any relevance at all to the point it's alleged to address (Hilbert's second problem). Please explain your reasoning. --Trovatore 22:19, 7 January 2006 (UTC)
- You know, my paragraph above sounds sort of ungracious; sorry about that. You've said you'll "look at [the] Hilbert issue", so I should give you a chance to do that. I'm still curious what you might have had in mind originally, though. --Trovatore 02:45, 8 January 2006 (UTC)
- my god this is the second time I've lost my stuff! wvbaileyWvbailey 02:57, 8 January 2006 (UTC)
- In the following I'll try to address the Godel issue and the Hilbert-connection and the question of "length" and use of "history"...
- FYI I have all these sources before me, real books are all over my desk. I am quoting from real texts, paper and ink, not links. So all editing here is matters of style, not matters of attributable sources or "truth". The sources are "facts." Whether we agree with the "truth" of their content is not the issue.
- Re "length", especially until the article is factual, is not a matter worthy of discourse. Some Britannica articles are enormously long. And no, I don't give a rat's hiney if the typical wiki-reader has the attention span of a gnat. We can structure an article so the gnats get their little bite and then move on...
- Re "history", encyclopedia entries do and are about "history" (in fact on my planet everything is history).
- What I'm trying to do is find a quote in the authors' own words to summarize their significant result(s). If I have my choice, I want to see/hear the real thing. Second best is a good historian. And the Godel quote is 'the real thing' unless of course the translation is bogus. If you have a better one I'm game. Or I suppose I could move the quote to 'footnotes' if it's causing too much anxiety. Lemme know.
- What I care about more is the accuracy of the entry after 1934,5 -- Turing. This, at last, explains "wvbailey's first question" cf the first entry in the previous "dump removed" section. This is a precis-plus-direct-quote from Hodges (again, I'm after attributable, verifiable information so his words are "the facts"), and I want to get the precis right. It explains why Turing used the "diagonal method" (sort of) and then why "the diagonal method" in this particular context of a specific machine is insufficient (right word, insufficient?). The machine cannot calculate it. I was stunned when I finally got the concept (only thanks to Hodges, the historian). All of a sudden all this stuff tied together. Which brings me to another question that you kind of hint at...
- Are Turing's work -- to answer the 2nd problem of Hilbert-- and "the Halting problem" addressing two different issues? The historical context shows that Turing was after an answer to Hilbert's 2nd question, but Church beat him to it.
- I figured out my confusion: apparently Hilbert proposed at a "congress" in 1928 three questions, the third of which has become known as "Hilbert's Entscheidungsproblem" (German for Decision Problem). (cf discussion in Hodges p. 91). Apparently this is what Gödel, Turing and Church were trying to answer, not Hilbert's 2nd problem. There's got to a gonnection (my apologies to F. Scott Fitzergald cf The Great Gatsby) wvbaileyWvbailey 18:07, 10 January 2006 (UTC)
- Cf Hodges again p. 111: "Almost on the same day that Alan announced his discovery to Newman, someone else completed a demonstration that the Hilbert Entsceidungsproblem was unsolvable. It was at Princeton, where the American logician Alonzo Church had finished his argument for publication on 15 April 1936. Church's essential idea, showing the existence of an 'unsolvable problem', had been announced a year earlier, but only a this point did he put it exactly in the form of answering Hilbert's question. // A new idea had found its way into two human minds simultaneously and independently. At first, this was not known at Cambridge" These are Hodges exact words, page 111.
- If they are two separate issues then Turing doesn't deserve the credit. In other words, maybe someone else proposed "the Halting problem" and somone else answered it, using proofs and theorems from Godel and/or Turing and/or Church and/or Post (Rosser, whoever...). So who was it? Who did it first? Or is this Halting Proof an actual different animal altogether that doesn't derive from any other previous work? My guess is "the Halting Problem" is directly derivable from Turing's first theorem, much as the second is derived from the first. But I haven't seen such a definition.
- One thing I do know from writing a zillion lines of code is: a decision doesn't necessarily lead to a halt. In fact the type of real-time embedded programs I did had no halts in them. Horrible things, halts. Unless you have a watch-dog keeping an eye on things. If not, never use a halt. The issue of "circles" is far more serious. (e.g. write a busy beaver without a halt. Send the machine into a tight loop. Have a watchdog look for the locked state. Halts are an artifact).
wvbaileyWvbailey 02:58, 8 January 2006 (UTC)
- On length and other style issues: You're new here. You should poke around other articles, see how they're structured. You can't just breeze in and expect all your content to be kept, regardless of what it does to readability, even if it's correct.
- Kind of resent the tone here. Who are you, the page manager? Do you own this page, what the hell is going on? I have seen how a few are structured, and they have not been very useful to me. Overly complicated, for highly-focused specialists. The references in particular suck, if there are any. E.G. the busy beaver site. No reference to Rado's original paper fer chrissake. So I added it. On this site I add some references, a little different content, and catch shit for it. Sure makes ya want to contribute more, all the positive feedback. wvbaileyWvbailey 23:08, 8 January 2006 (UTC)
- On history: No, this is a math article; it's about math. History should be included to the extent that it helps with the understanding of the math, and perhaps just a wee bit more, but if you want to go on about history at length, that should probably be a separate article.
- History is fun, it gives context, it's useful. We have a fundamental disagreement here. To carry this one on any further will not be useful. I'm fine with the history where it is. You moved it. I trimmed it, moved stuff to footnotes. Of course it can be trimmed. Of course it needs work. But make some suggestions to improve it fer chrissake. All people are doing here is lifting their legs on each others work, I don't see much contribution going on, or attempts to make things better. If you just can't stand the history, move it to a new page. Just lemme know where it went. wvbaileyWvbailey 23:08, 8 January 2006 (UTC)
- On the Gödel quote (please use the umlaut; "Godel" is a flat-out misspelling):
- This nit-pick criticism is unworthy of a serious academic. It's bullying. Give us all a break. My son is a post doc and he's experienced this same sort of shit. But I agree it's not "correct". How do you get the umlaut on the o? Thanks. wvbailey
- I'm not disputing its authenticity, just its relevance, which you still haven't explained. Moreover you seem to be conflating the Entscheidungsproblem with Hilbert's second problem; they are quite different. If you don't understand the difference, ask! Or if you see a connection the rest of us don't, then explain it. --Trovatore 07:06, 8 January 2006 (UTC)
- You could well be correct, I'm pretty confused. So the Entscheidungsproblem is not Hilbert's 2nd problem? Didn't Hilbert coin the word Entscheidungsproblem? This is from the site that quotes Hilbert's 2nd problem verbatim:
- "But above all I wish to designate the following as the most important among the numerous questions which can be asked with regard to the axioms: to prove that they are not contradictory, that is, that a definite number of logical steps based upon them can never lead to contradictory results". Hell I thought the connection was this: Hilbert asked the questions in 1900. Russel and Whitehead carried out their work partly in response to it. Then Go[umlat]del and Church and Post and Turing all started working on it using PM and ZF axioms as their base.
- Cf Hodges again p. 111: "Almost on the same day that Alan announced his discovery to Newman, someone else completed a demonstration that the Hilbert Entsceidungsproblem was unsolvable."
- I read that Hilbert believed he had a set of axioms related to his geometry, but he needed a proof of consistency of arithmetic as a premise for his proof.... is this it? Explain the difference to me, or send me to a reference. thanks. wvbaileyWvbailey 23:08, 8 January 2006 (UTC)
- On length and other style issues: You're new here. You should poke around other articles, see how they're structured. You can't just breeze in and expect all your content to be kept, regardless of what it does to readability, even if it's correct.
- On the umlaut: When you edit a page, look under the "Save page" etc buttons; there's a box that says "Insert:" and has a whole bunch of characters.
- No, the Entscheidungsproblem is not Hilbert's second problem. Whether Hilbert coined the word or not I don't know. The Entscheidungsproblem asks, is there an algorithm that infallibly distinguishes between universally valid first-order sentences, and those that aren't? The 2nd problem asks, is it possible to prove that arithmetic is consistent?
- Those are quite separate issues.
- I'm going to think about this. There is an interesting commentary by Davis in "Undecidable", p. 108 re this issue. What were Hilbert's and Ackermann's "rules"? Is this what it's saying: we can show how to well-form a sentence from "the axioms", but not the converse. i.e. IF(Axioms --> Sentence) but not proveable (decidable?) that IF(Sentence-->Axioms). wvbaileyWvbailey 15:26, 9 January 2006 (UTC)
- Now, it's true that the question of the consistency of arithmetic can be reduced to a question about whether a particular first-order sentence is universally valid (at least I have the outline in my head of an argument to show that; I could possibly have made a mistake) so if you had a machine that tells you whether sentences are universally valid, you could feed it that sentence and it would tell you (presumably) that arithmetic is consistent. But it's still not the same issue, because Hilbert's second problem asks for a proof that arithmetic is consistent, and to get that from the above scenario, you would need not only the machine, but also a proof that the machine works. Hope it's clearer now. --Trovatore 04:40, 9 January 2006 (UTC)
- Not so clear as it should be, that's for sure. I'll do this, I'll change the entries simply to reflect that Turing takes up the question of "The Entscheidungsproblem" rather than "Hilbert's second". Wouldn't it make sense to define these somewhere for the reader, as you did? Very few readers will have enough knowledge to see any distinction. I'm still confused, but this dialog is helping me. But for now I'll leave the entry re "Hilbert's 17 questions" because, again it's historical context. Whether or not they (Gödel, Church, Turing) were poking around at Hilbert's 2nd too is now unclear to me. Who was poking around at Hilbert's 2nd? Gentzen, correct? Others? And yeah what is the connection between Hilbert's 2nd and the "Ent..."? And more germane: the historical thread to the Halting Problem? wvbaileyWvbailey 15:26, 9 January 2006 (UTC)
New topic: Julia Robinson is known for a proof of something re the halting problem. Do you know anything about this? We have Chaitin as “deep” contributors, are there others? wvbaileyWvbailey 15:26, 9 January 2006 (UTC)
- There is no direct connection between Hilbert's second problem and the Entscheidungsproblem, or between Hilbert's second problem and the halting problem. (The Entscheidungsproblem and the halting problem, on the other hand, work out to be essentially the same problem, though this fact uses deep theorems.)
- Can you tell me something about these theorems, where to find them? this is confirming what I suspected. see my last comment. I have not seen a good demo of how to get from Turing's first proof to "the halting problem". In Minsky there's the reverse (I think).wvbaileyWvbailey 16:29, 9 January 2006 (UTC)
- Yes, a definition of the Entscheidungsproblem might well make sense in this article. I would omit Hilbert's second entirely; it's not directly on point to anything in the article.
- Gentzen proved the consistency of arithmetic using transfinite induction. Whether he saw this as a solution to Hilbert's second problem, I don't know, and whether Hilbert would have accepted it as a proof, I also don't know. Not directly related to the halting problem.
- Your historical timeline contains lots of stuff that's related only tangentially to the halting problem, though many of the issues are susceptible to similar techniques, and it is kind of interesting to see it all together. An idea might be to move it to an article called History of limitative results in mathematical logic or some such. Then it could be expanded to include things like Russell's paradox and the independence of the continuum hypothesis.
- I agree to the "tangentiality" problem. And it has become pretty long. In the interest of precision and brevity, which entries would you cut? I do want to have some historical perspective in this article, because "the halting problem" theorems as in "this program terminates" and Turing's circle-tester theorem are not quite the same animals. As to a new page, I dunno, I've been mulling something like this over, with a detailed deconstruction of Turing's 1st proof, and more about Post-Turing machines as neat little demonstration devices of various issues. For instance, even a 5-line little machine with a HALT in it can give a graphic demonstration of how horrid the problem of "will this machine halt" and "circle-hunting" really is (it seems to increase on the order of N*2^N where N is the number of instructions, at least from my first look at it).wvbaileyWvbailey 16:29, 9 January 2006 (UTC)
- I'm afraid I don't know that much about J. Robinson's work (I'm a set theorist, not a recursion theorist). Chaitin has done important work, but in his case it's always a good idea to give careful scrutiny to claims that a particular result of his is groundbreaking or revolutionary. There are a lot of sources that describe his contributions in breathless terms that they don't necessarily merit. --Trovatore 15:56, 9 January 2006 (UTC)
- I'll leave Gentzen and Robinson off. Can we agree that some unknown must have coined the "halting problem" from Post's "Stop"-instruction and Turing's machine? Or, any ideas where the phrase "halting problem" comes from, historically?wvbaileyWvbailey 16:29, 9 January 2006 (UTC)
- I'd prefer not to add speculation about where the term must have come from. If you can find out for sure where it came from, it would be of interest to add it to the article. But if you can't, I don't see that it's any great loss to just not attribute its origin.
- I agree that until attribution is known for sure to leave it out.
- As for Turing's original criterion about "tight loops", as you report it, again that's kind of interesting, but not central to the article. This illustrates one of the major problems with an excessively historical approach to mathematical exposition; namely, that the original sources are always version 1.0 of the notation and proof, and version 1.0 almost always has bugs. Typically the concepts are substantially polished and tightened in later analysis, and that's what seems to have happened here, because the "halting" criterion is much easier to understand, analyze, and apply, than the "tight loops" one. --Trovatore 06:44, 10 January 2006 (UTC)
- I agree that, for most folks, the "halting proof" is probably easier to grab than the "circle/tight-loops" one. Because I'm an engineer I find Turing's mechanical proof much easier and the antonimy-version harder (this I swear has to do with "brain/mind oscillations", due to the delay inherent in the antonimy). [And I'd like to see how to derive the halting proof from Turing's proof...] One thought is to create a section (page? I don't like the new-page thing if the topic is the same... But if so what would the title be?) that describes "alternate proofs and demonstrations", to wit:
- I'd prefer not to add speculation about where the term must have come from. If you can find out for sure where it came from, it would be of interest to add it to the article. But if you can't, I don't see that it's any great loss to just not attribute its origin.
- I'll leave Gentzen and Robinson off. Can we agree that some unknown must have coined the "halting problem" from Post's "Stop"-instruction and Turing's machine? Or, any ideas where the phrase "halting problem" comes from, historically?wvbaileyWvbailey 16:29, 9 January 2006 (UTC)
- One is the Turing mechanistic version that I've sort of given above (but I recognize this isn't the halting proof, and I don't have this extension froms Turings first and maybe second, proof); my guess is the Halting proof falls out easily, and
- Another (proof? demonstration?) would derive from Minsky's comment in his chapter 8. "The Halting Problem" that "the bleak fact is that no computable function can grow so large so fast!" And my take on this is: A circle-hunting heuristic machine must eventually "run" the machine-under-test to verify that a (found) halt-instruction will actually "be executed"; because there are so many circles that can possibly lock the testing/simulating machine, even pattern-recognition heuristics won't help (always a new possibility, even for an adaptive machine). But since no circle-finder is possible for an arbitrary machine, the question "will this finite machine halt?" is effectively undecidable.) I find this fascinating in its own right, brings the reader to "NP-Complete problems. This new section would allow me to move the Turing footnote and history comment out of there to the new section. Comments? Thanks.
- To trim the history section I need some input about what to cut. Thanks.
- RE: About the coining of the word "Entsheidungsproblem" Hodges has this to say: "Alan had been stimulated by Hilbert's decision problem, or the Entscheidungsproblem...." (p. 107). I'm still having a mental block re connections between "the Engscheidungsproblem" and "Hilbert's 2nd Problem". I guess I need a book about Hilbert.
- I'm slowly moving some of my less-germane points over to the Turing Machine page, and trying to cross-reference them. Eventually they may disappear from this page. Comments? Thanks. wvbaileyWvbailey 16:43, 10 January 2006 (UTC)
- The "machine" vs "Gödel number" style is orthogonal to "halting" versus "loops". The former is just an issue of expository style; the latter is, I think, a distinction between two essentially different problems. If you give me an oracle for finding loops, I can easily use it to solve the halting problem: Given a program that I want to know whether it halts, I simulate it in such a way that every step produces output, except that I replace all the "halt" instructions with "tight loops". Now I ask the oracle whether the modified program gets into any tight loops. I don't see any obvious way, though, to check for "tight loops" with just an oracle for halting. So I suspect that "tight loops" is a strictly harder problem, probably of Turing degree 0'', whereas the halting problem itself has Turing degree just 0'.
- You're confirming what I sensed. Tell me more about Turing degree 0 and 0'. Is this in a text somewhere?
- Please don't drag in P vs NP; that's a much finer distinction. All NP decision problems, including the NP-complete ones, are decidable (it just might take a while). From the coarse point of view of this article, all decidable problems are the same.
- Okay. Is there any room here for discussions of failure-to-decide because it will take "forever"?
- As to what Gödel, Church, and Turing were "trying to do"—well, many things, I would say. Just because two problems are addressed by the same workers in the same time frame using similar methods, does not make them the same problem. --Trovatore 19:34, 10 January 2006 (UTC)
- Quite right. Gödel was working on Hilbert Problem 2, Turing and Church on "the Entscheidunsproblem." I have (I hope) finally figured out the historial sequence, ie. where the 'Entscheidungsproblem came from: 1928 conference where Hilbert asked "three questions"-- (1)Complete? (2) Consistent? (3)Decidable? According to Hodges the historian, in 1930 Hilbert was still asserting his "Positivist" philosophy that all is solvable. But at some meeting where he made the statement "that there is no such thing as an unsolvable problem," Gödel announed his results [cf Hodges p. 92], and the first two questions were considered "answered". Thus, by the time Church and Turing were working on the problem in the mid-30's, they were onto this 3rd question. This is Hodges interpretation of events, and he's a mathematician. Whether or not its "true" I don't know. But it is (apparently-- I haven't done this yet) verifiable back to Constance Reid's biography of Hilbert, whom Hodges quotes and uses extensively re Hilbert. So this is the best I have, unless you know more, or know of someone who knows more. As to the source of the moniker "halting"... that may take a trip to the Dartmouth library.
Still need guidance on trimming the history... wvbaileyWvbailey 21:24, 10 January 2006 (UTC)
A lot of the stuff in the history more properly belongs in an article about negative proofs or proofs of nonexistence which would reference halting problem.
- I agree, because the history lead-up is more complex than I would have thought. Can you suggest a good title? wvbaileyWvbailey
- How about proof of impossibility? This already has a modest 500 Google hits in appropriate contexts. A possible intro could go, "A proof of impossibility is a proof demonstrating that a particular problem cannot be solved, or cannot be solved in general. Often proofs of impossibility have put to rest decades or centuries of work attempting to find a solution." It could go on to talk about how such proofs are usually expressible as universal propositions in logic, and how techniques like relativization (see oracle machine) provide "weak" proofs of impossibility excluding certain proof techniques. Deco 08:35, 13 January 2006 (UTC)
- I like it. The deed [a stub anyway] is done. I'll use your words. I don't think I have the expertise to add the subtlety you've added (e.g. weak proofs etc.) I just want to get the longer history somewhere. Thanks, wvbaileyWvbailey 18:03, 13 January 2006 (UTC)
- How about proof of impossibility? This already has a modest 500 Google hits in appropriate contexts. A possible intro could go, "A proof of impossibility is a proof demonstrating that a particular problem cannot be solved, or cannot be solved in general. Often proofs of impossibility have put to rest decades or centuries of work attempting to find a solution." It could go on to talk about how such proofs are usually expressible as universal propositions in logic, and how techniques like relativization (see oracle machine) provide "weak" proofs of impossibility excluding certain proof techniques. Deco 08:35, 13 January 2006 (UTC)
The halting problem isn't the most special or important negative proof in the world - let's keep it to events that are directly relevant. Deco 05:41, 12 January 2006 (UTC)
- I'm going to remove the stuff leading up to 1900, at least for a start. And some of the footnotes. And put the stuff here for time being. If I get convinced that Hilbert's question #? (whatever correct number it is.. 2 or 10) is not germane then we can (maybe) remove that too. For sure the historians (Penrose, Reid, and Hodges) agree he re-worded his question at the 1928 conference. When in late 1930 Godel's proof took care of Q's 1 and 2, Turing and Church got to working on #3. So it could start there. I've ordered a cc of Reid (Hilbert bio).
- Still need an answer: Who coined the phrase "halting problem?" Where did it first appear? Then I'm done with this.wvbaileyWvbailey 13:01, 12 January 2006 (UTC)
Characterization of Entscheidungsproblem still problematic
The article now presents the following question:
- #3: Was mathematics decidable? (Hodges p. 91). The third question is known as the Entscheidungsproblem (Decision Problem) (Hodges p.91, Penrose p.34)
But according to the article Entscheidungsproblem, the Entscheidungsproblem does not ask for a decision procedure for mathematics, but only for (presumably first-order) logical validity. That is, it asks for a mechanical procedure that will decide whether a statement is true in every interpretation; this quite a different matter from asking whether it's true in the intended interpretation, which is what would be required to give a decision procedure for mathematics.
- I don't understand the difference. If I don't probably others won't either. What you wrote sounds as it it is pretty subtle. What exactly does "valid" mean? Provable? Couldn't the "intended" and the "every" be the same, because if we could "validate" (decide? prove?) them all we could then search a catalog of "every" proof (e.g. all 437.78 trillion valid proofs, or even an infinite number) for "the intended" one? My (rudimentary) understanding of the "Entscheidungsproblem" is whether or not we can build a machine (write an algorithm) to decide whether or not an arbitrary "theorem" (string of symbols of a certain type) is "derivable" i.e. "provable" (comes from applications of "the rules" and "the axioms" of the "formal system"). And basically, the "halting problem" asks exactly the same question. Is this a correct understanding? Is "the formal system" "mathematics-as-we-know-it" (i.e. "numbers" -- ZFC set theory -- and Peano arithmetic and formal logic, is there more mathematics now-a-days... am confused... this stuff is damn subtle, and I can't be the only confused one...)Wvbailey 17:55, 7 February 2006 (UTC)wvbailey
Now it is possible, I suppose, that this distinction was not clear at the time. If so, that needs to be made clear in the article(s); right now there is a bit of a disconnect between halting problem and Entscheidungsproblem that could lead the reader to the conclusion that a decision procedure for validities is the same thing as a decision procedure for mathematics. --Trovatore 20:08, 5 February 2006 (UTC)
- I am confused, and wish I could get to the bottom of what "the Entscheidungsproblem" means from a historical perspective. The following comes from book Hilbert by Constance Reid (p. 151):
- "That September [1917] Hilbert returned to Zurich to deliver a lecture before the Swiss Mathematical Society....
- "... it was also in the course of this talk that he [Hilbert]brought up certain questions which revealed for the first time since 1904 in public utterance his continued interest in the subject of the foundations of his science:
- " The problem of the solvability in principle of every mathematical question.
- " The problem of finding a standard of simplicity for mathematical proof.
- " The problem of the relation of content and formalism in mathematics.
- " The problem of the decidability of a mathematical question by a finite procedure.
- "To investigate these questions -- he pointed out -- it would be necessary first to examine the concepts of mathematical proof.
- "But he himself was still not ready ... there were problems at home ..."
- I don't read German so I can't get to the bottom of this by looking at minutes (if they are even available) but I wonder if this is the first time when the Entscheidungsproblem was formally stated, i.e. the last of the four "problems" above [?]. There is also the question of what happened at the later "Bologna Congress" in 1928, whether this was discussed then. Or whether the "problem" was formulated between Ackermann and Bernays and Hilbert and von Neumann, and when this was publically stated. (Constance Reid is apparently the sister of Julia Robinson). Wvbailey 22:47, 6 February 2006 (UTC)wvbailey
- From what I can gather (mostly confusion at this point, see reference to Franzen, below), Gödel produced a proof of "completeness" of "first order predicate logic" in his Ph.D. thesis. But results from Ackermann's PhD thesis and von Neumann's PhD thesis [?] were the first cracks in the Hilbert program because both Ackermann and von Neumann had to use "restriction systems" to get their completeness [? consistency?] proofs to "work" (summarized from Reid's book). So Hilbert and Ackermann continued their quest...
- Turing believed he proved something different than Gödel's first proof (but Franzen seems to blur this distinction). Turing himself refers the reader of his 3rd proof to a text by Hilbert and Ackermann as follows:
- "... to show that the Hilbert Entscheidungsproblem can have no solution... For the formulation of this problem I must refer the reader to Hilbert and Ackermann's Grundzüge der Theoretishen Logic (Berlin, 1931), chapter 3" (Turing's paper in The Undecidable, p. 145).
- Perhaps the thinking was evolving, but I don't think so... the more I read the more I realize that Turing had a good handle on Gödel's proof, and that Turing's proofs are still "current" (i.e. their cleverness and use of their terminology still holds). I'm trying to cut my way through the thicket of "completeness" and "consistent" and "undecidable" and "provable" etc. as defined by Torkel Franzen in his Gödel's Theorem, A.K. Peters: Wellesley Mass, 2005. This book draws two distinctions between the (current) use of the words "decidable" and "undecidable" (p. 65). And, re the use of words "halting", "termination", etc. Franzen states that "(An alternative terminology [for "algorithm"] is also used in the literature, in which an algorithm is a mechanical procedure that does not necessarily terminate)" (p. 64). It's as if the "decision problem" (infinitely-operating algorithm gets trapped in a circle while diagonalizing) and "the halting problem" (algorithm to detect algorithm-halting can't both halt and not-halt when applied to itself) are one and the same, (perhaps) only "cast" and then proved differently (but they both have to do with provability in mathematics "as a whole" (e.g. Principia Mathematica, Peano+Logic, Ackermann's K))Wvbailey 16:11, 7 February 2006 (UTC)wvbailey
Some distinctions
This is in response to wvbailey's paragraph above that starts "I don't understand the difference".
First, let's agree that a "statement of arithmetic" is a first-order sentence in the language of arithmetic, so it has numerals (at least, numerals for zero and one), addition, multiplication, and the less-than relation, and you can quantify over natural numbers but not sets of them. So the following is a statement of arithmetic:
The content of the above statement is "every natural number has a square root"; it is of course false, as 2 does not have a square root in the natural numbers.
Now a statement of arithmetic is true in the intended interpretation if it's true when the variables are allowed to range over the real natural numbers. The negation of the above statement,
is true in the intended interpretation.
By contrast, a statement of arithmetic is universally valid if it's true no matter what sort of objects you allow the variables to range over, or how you interpret the symbols zero, one, plus, times, less than. So the (second) statement, though true in the intended interpretation, is not universally valid, because (for example) it's false if you allow the variables to range over the nonnegative real numbers. An example of a universally valid statement of arithmetic is
Provability is a separate concept, distinct from both truth and validity, and requires that you specify from which formal theory you're accepting proofs. One possibility is Peano arithmetic or PA. There is a statement of arithmetic that formalizes the claim "PA is consistent"; we'll denote that statement of arithmetic by Con(PA). Then Con(PA) is (presumably) true in the intended interpretation, but not universally valid and not provable in PA. However the second formal statement in the section (the one that says "there is a natural number with no square root), is provable in PA but is not universally valid.
So we wind up with four decision problems being considered:
- Given an arbitrary Turing machine, does it halt?
- Given an arbitrary statement of arithmetic, is it universally valid?
- Given an arbitrary statement of arithmetic, is it provable in PA?
- Given an arbitrary statement of arithmetic, is it true (in the intended interpretation)?
The first three questions are all mutually Turing equivalent; that is, given an oracle for any one, you can solve the other two. The fourth one is much harder. --Trovatore 18:18, 7 February 2006 (UTC)
- I now agree with you that (1) "... this distincition was not clear at the time." The worry, of course is (2) it was/still-is/always-was (crystal-) clear (to logicians and set theorists) from the get-go but sort of assumed true without need to discuss. In my readings I have not encountered your subtle distinctions. I've just encountered "natural numbers" used more-or-less as indices or mere "symbols" (e.g. Turing mapping his Standard.Descriptions into his Discription.Numbers, Gödel's natural numbers rasied to primes, etc.) This leads me to (2), that what you're pointing out is so subtle that it has been missed by "all of us" (i.e. all who are not up on the current logic-of-mathematics literature). Presumably your point is established in "the literature", preferably a college text somewhere. Can you point me to one? Thanks.
- I thought your example was pretty good (admittedly had to read it about 4 times to get it), except my confusion re numbers (see below). I suggest it belongs with "halting problem" as an evolved concept from "Entscheidungsproblem", but if so then "Ent" needs some major work, see below.
- I'd recommend that you point me to how to clean up the entries if you believe they need cleaning. Maybe the Entscheidungsproblem entry should present more of the historical context, and the "halting problem" entry maintain more of a "modern" context (but keeping my grumble that Turing did not coin the "halting problem", but more likely it was Davis). E.g. I still believe, and all the history points to the fact that, (although I think you guys disagree) that "the Entscheidungsproblem" was implicit (buried, hidden, unclear) in his #2 and #10 problems of 1900 when he first presented them, but that all the "fine distinctions" (problems, worries, cracks, PhD theses, Russell's paradox, Richard's antinomy) began to emerge (because he asked the questions). Then during and after WWI e.g. the 1917 conference, the 1928 Congress, his retirement address in 1930, and finally as he worked with Ackermann and von Neumann and Bernays in the early 1930's, Hilbert's thinking evolved. Reid says he was angry and horrified when presented with Gödel's proof. Really, some of this history stuff probably belongs with the Entscheidungsproblem. The "Halting Problem" clearly evolved (somehow) from "Ent" (starting with Gödel then Church, Turing, Post). Maybe here's a way to handle this: to put more historical stuff in "Ent" and the more modern stuff, e.g. with your distinctions, in "Halting problem" cast as the "evolved Ent". Or do you think they're different problems? Comments? I mean, do mathematicians still work on the "Entscheidungsproblem?"
- The other problem here, I think, is a "wikipedia problem" . The question always is: who is the article for? Kids? Professors? All? I remember reading re some kids, some high-school girls in Mexico, wanting help with a "Turing machine" (its in the talk section, I believe). I've had a senior-in-college math student write me a comment re "Proof of Impossibility" (he liked it). When I read your entry above I sat with a dictionary to make sure I had clear the distinctions: natural number, integer, whole number, counting number. So I recommend "thoughtful popular" writing i.e. like Scientific American writing (e.g. I liked your explanation above, the example really helped) i.e. write as if directed to a college freshman, maybe in physics or engineering, but not a math student, and definitely not a computer science student (i.e. no C-like programs in the text).Wvbailey 17:12, 8 February 2006 (UTC)wvbailey
Responses:
- Textbook: I never learned this stuff from texts with ISBNs, so I'm not sure what to recommend. A lot of folks like Enderton, which probably has it.
- Enderton, Herbert B. (2000). A Mathematical Introduction to Logic. Academic Press. ISBN 0122384520.
- Cleanup: I don't really have time to figure this out right now. It's plausible that Hilbert thought there was a connection with Hilbert's second problem, but it's clear by now that they are quite separate.
- No, I don't think mathematicians work on the Entscheidungsproblem per se; it's known, not only that it's unsolvable, but exactly how unsolvable (that is, its precise Turing degree). It could be, for all I know, that there is continuing research on variants of it.
- Writing style: I see WP as a scholarly reference work; articles should start at the level of Brittanica, but should not be limited to content that could be presented to a general audience. Some articles are about subject matter too inherently technical to be made as accessible as Brittanica, but much of this article can be that accessible and should be. --Trovatore 01:11, 10 February 2006 (UTC)
problem with trouble() proof
The premise is supposedly that this function ...
function trouble(string s) if halt(s, s) == false return true else loop forever
... doesn't work, thus disproving the possibility of halt().
But consider, instead of halt, a function verify; like halt, it takes in a string representing a program, but instead of dealing with the difficult halting problem, all it does is discern whether a program returns true or false (If the program returns something else, or runs forever, um... I don't care. Let's just say it throws an exception :P ). So, if you have a similar trouble2 function:
function trouble2(string s) if verify(s, s) == false return true else return false
and s is a string representing trouble2, you run into the same sort of contradiction that you did with the halting proof. Are we to assume, then, that it is impossible to predict the outcome of a program at all? If so, why does Turing seem to focus on halting specifically? ~ Booyabazooka 23:49, 21 May 2006 (UTC)
- You are on to what is called "Rice's Theorem", which Turing actually pre-[discovered? what's the word? --- discovered, mentioned, but just blew off as a trivial outcome] -- at the end of his proof #2. But first to clear up confusion relative to a historical fact: Turing's proofs had nothing whatever to do with "halting"; his paper contained three proofs: his first proof, upon which he based his second and third proofs, had to do with whether or not a procedure/algorithm could determine if another procedure/algorithm (that calculates the decimal part of a number) would end up in a "circle" -- a never-ending loop, and thereby fail to calculate its number. Nowhere does Turing's paper mention "halting". The word is never used by Turing. The so-called "halting" proofs seem to trace back to Martin Davis, and through him to his teacher Emil Post whose paper did mention a HALT instruction. The various halting proofs are very different from Turing's "circle" proof -- the Turing proof is very "constructive" and hence very convincing but a bit harder to understand than the simple antinomy that the "halting" proof relies upon. But it's impossible to convince anyone of this who has not read the actual Turing paper. So the myth is perpetuated about "Turing's Halting Proof". There is no such thing. wvbaileyWvbailey 21:30, 22 May 2006 (UTC)
Conversations with Martin Davis: he is the source of the phrase "halting problem", Kleene may the source of the halting/antinomy version, Turing's and the antinomy versions are indeed of different degrees of complexity
Davis has given me permission to quote him. Lambiam set me on to his e-mail address, etc.
- >I've been trying to find the source of the phrase 'the halting problem" and I traced it down to you in a proof you published in the mid- to late-1950's. Truly, is this correct? A proof that you provided... in your book ... used that phrase; you provided an antinomy-based proof similar to the one I've also found in Minsky's text. I found your book in the Dartmouth stacks. Very clearly your proof was much different than Turing's and you referred to it as the halting proof.
- >This is of no little consequence, this attribution to you. If it's yours you deserve the credit, damn it. In a recent Scientific American article Chaitin attributes proof of "the Halting Problem" to Turing. Utter bullshit-as-rubbish-- Turing's proofs do not mention "halting" at all. His 1st proof is entirely different than the antinomy proof you and Minsky offer. I see the word "HALT" in Post's paper and the words "terminating" in Kleene and Church, but not in Turing. Yet Turing gets the credit.
- >I challenged Chaitin via a letter to the editors of Scientific American. But I haven't heard a word from them or him.
Here is Davis's first response [sic = "as written"]
- Thanks for writing.
- My book "Computability & Unsolvability" served to bring the subject to the attention of the brand new (not yet named) computer science community. I supplied I [sic] smooth easy-to-follow development, but there was almost nothing new in it. I combined ideas and results from Turing, Gödel, Post, and Kleene. With the halting problem, I contributed the name - that's all. Despite appearances, the proof is really there in Turing's paper. You'll find it also in Kleene's book "Intro to Metamathematics" published 6 years before my book. But Kleene doesn't even label it as a theorem. It's just one sentence in a long complicated paragraph.
- I hope this helps.
- Martin Davis
The following is the pertainent piece of my second inquiry:
- >I've read the papers you have cited (from your Undecidable -- I bought a cc way back in the 1980's-- thanks for doing that, it's been an invaluable compilation). I quoted from them on the Wikipedia article Halting Problem. In particular Church states that "any sequence of reductions of the formula must (if continued) terminate in the normal form" (p. 92, Theorem II) and he later discusses algorithms that "terminate" (p. 100 Undecidable). While I do agree that the ideas are there it would seem that you (or perhaps Kleene?) synthesized them into a much easier (more compact) form of proof than Turing's. I'll research Kleene's book too, this reference has appeared a couple times in my investigations.
- You'll find it buried in the first paragraph on p. 382.
- Dartmouth library had its cc checked out until end of 2006, ferchrisake. I remember lookin' for it the last time I was up there, and it was out then. I've ordered a cc. Cost me a freakin' hundred bucks, used.wvbaileyWvbailey 13:43, 20 June 2006 (UTC)
- >Let me ask you another question re Turing's paper. Have you ever encountered an "exposition" of his proofs, much as writers have done for Godel's proof(s)? I started a page called "Turing's Proof" on Wikipedia, and I more or less made it through the 1st and 2nd proofs but fell into a snarl with the 3rd.
- Post's paper on "a problem of Thue" has a long critical discussion of Turing's paper including discussion of a very serious bug in his universal machine. In particular,because of Turing's decision to use his machines to compute the digits of a real number, Post points out that Turing's version of what I called the "halting" problem is of a higher degree of unsolvability than what was wanted for Post's purposes. (In later terminology it is 0 [the original is actually written as O prime-prime] complete.)
Davis's last comment echoes correspondent Trovatore's opinion -- see below where I pasted a cc of his response to me. Lambiam observes that wiki-policy won't allow e-mail quotes (i.e. private correspondences) because they are unverifiable. But here I assert we finally have hard evidence of the source of the phrase "halting problem". And we now have confirmation that Turing's first proof and "the halting problem" are not the same animal.
I can now go to my grave a peaceful man.wvbaileyWvbailey 17:05, 4 June 2006 (UTC)
The following is Trovatore's response to my question about why the Turing and antinomy-version of the Halting problem are so different. It confirms Trovatore's suspicion that Turing's formualtion is 0-prime-prime, a "harder problem" than the "halting problem":
- The "machine" vs "Gödel number" style is orthogonal to "halting" versus "loops". The former is just an issue of expository style; the latter is, I think, a distinction between two essentially different problems. If you give me an oracle for finding loops, I can easily use it to solve the halting problem: Given a program that I want to know whether it halts, I simulate it in such a way that every step produces output, except that I replace all the "halt" instructions with "tight loops". Now I ask the oracle whether the modified program gets into any tight loops. I don't see any obvious way, though, to check for "tight loops" with just an oracle for halting. So I suspect that "tight loops" is a strictly harder problem, probably of Turing degree 0 [this is actually written by Travatore as zero-prime-prime], whereas the halting problem itself has Turing degree just 0' [zero-prime].
Origin of Halting Problem?: a proof by S. C. Kleene (1952) and so named by Martin Davis
As I noted above, Martin Davis said in his e-mail to me that he coined the name "halting problem" but he added that in fact the first expression of the notion of an algorithm that could detect if a machine would stop was on p. 382 of S.C, Kleene's book of 1952, first paragraph "buried half way down":
- S. C. Kleene, Introduction to Metamathematics, North-Holland Publishing Company, Amsterdam NY, first published 1952, Tenth impression 1991.
As this book may be hard to find I will quote the entire paragraph:
The proof appears in immediately after § 70 Turing's Thesis:
- § 71 The word problem for semigroups
- "Church's original example of a decision problem which, on the basis of his thesis, is unsolvable was constructed in therms of λ-definability (1936). The corresponding example given above (Theorem XII §60) is constructed in terms of general recursivenss (following Kleene 1936, 1943). Turing 1936-37 gave examples constructed in terms of computability. This can be done e.g. as follows. A machine M is determined by its table, containing (j+1)k entries. We can set up a Gödel numbering of the tables, and thus of the machines. Then the function ξ defined as follows is not computable: ξ(x) = 0, if x is the Gōdel number of a machine Mx, and the partial function φ(x) of one variable which Mx computes has 1 as value for x as argument and ξ(x) = 1 otherwise. So by Turing's thesis (or via the equivalence of general recursivenss and computability by Church's thesis) there is no algorithm for deciding whether any given number x is the Gōdel number of a machine which, when started scanning x in standard position with the tape elsewhere blank, eventually stops scanning x, 1 in standard position. As another example there is no algorithm for deciding whether any given machine, when started from any given initial situation, eventually stops. [boldface added] For if there were, then, given any number x, we could first decide whether x is the Gödel number of a machine Mx, and if so whether Mx started scanning x in standard position with the tape elsewhere blank eventaully stops, and if so finally whether x, 1 is scanned in standard postion in the terminal situation." (p. 382, Computable Functions, CH. XIII)
A question for Trovatore and CMummert: is this version of "the halting problem" just a recasting of the "circle problem" or the "antinomy version" on the article page, or what? It seems like a third form because it seems to be going from Turing machine to Godel numbering of the table, which is something Turing did in his third proof of his 1936-1937 paper. Thanks wvbaileyWvbailey 20:36, 26 June 2006 (UTC)
- Would you clearly (and briefly) define exactly what you mean by the circle problem and the antimony version regarding the halting problem? I don't understand what you mean. Kleene's statement in bold above is exactly what most people would say the phrase halting problem refers to. CMummert 02:58, 28 June 2006 (UTC)
- What I should have written is: Is the proof he offers just another "antinomy version", or is it a form of the "circle problem" or is it a form of the "diagonal-argument version" or what? It seems different.
- By antinomy version I mean the simple proof on the article page. A better presentation appears in Minsky (1967), Computation: Finite and Infinite Machines, Chapter 8.2 Unsolvability of the Halting Problem. After his one-page presentation he states: "We have only the deepest sympathy for those readers who have not encountered this type of simple yet mind-boggling argument before. It resembles the argument in 'Russell's paradox'... the unsolvability of the halting problem is usually demonstrated by a from of Cantor's 'diagonal method.' We prefer the present form because it suppresses the 'enumeration' required for the diagonal method. We will have to use the Cantor form of the argument in the next chapter."(p. 149)
- By diagonal-argument version I mean appeals to "Cantor's diagonal method". Minsky (1967) offers his version on page 159 (which I don't think I can summarize succinctly).
- By circle problem I mean the question Turing asked of his machines (or we would ask of a computer program): Does this machine/program have in it "a circle", or is it "circle-free"? (e.g. the tightest of all fatal "circles" is the following):
- 1003 GO_TO 1003
- When the machine/computer enters this "circle/loop" it becomes incapable of finishing its computation, and hence its "number" is "unsatisfactory".
- By circle problem I mean the question Turing asked of his machines (or we would ask of a computer program): Does this machine/program have in it "a circle", or is it "circle-free"? (e.g. the tightest of all fatal "circles" is the following):
- Trovatore believes that the "order" of the "circle problem" is different (his opinion appears somewhere above). In other words we could use a proof of "the unsolvability of the circle problem" to prove the "unsolvability of the halting problem" but not vice versa [correct ?].
- The canard in the article is that "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." What I propose we should be saying is that:
- "the Halting Problem was first stated and proved by Stephen C. Kleene (1952), and so named by Martin Davis in his proof of (1957); the first known "antinomy version" is a proof by Minsky (1967). Alan Turing's proof (1936) was with regards to a "strictly harder problem" -- the impossibilty of a "general process" to "find out whether a given number is the D.N. of a circle-free machine". [then provide a link to "circle problem", or "circle-free machine" or "loop-problem" or whatever; his proof is fascinating in its own right, and much different.]
- [I will eventually correct the history section to better-reflect the history of "the halting problem".]
- The canard in the article is that "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." What I propose we should be saying is that:
wvbaileyWvbailey 19:07, 28 June 2006 (UTC)
- Turing, in his Computable Numbers article, does state explicitly an unsolvable problem that is the same degree as the Halting problem. I quote Turing (his emphasis):
We can show further that there can be no machine E which, when supplied with the S.D. of an arbitrary machine M, will determine whether M ever prints a given symbol (0 say).
- The quote is from p. 134 of The Undecidable edited by Davis. By S.D. Turing means an index of the machine. From a modern point of view, the standard proofs of the unsolvability can be modified in a straightforward way to show that the question of whether a Turing machine ever prints 0 (that is, has 0 in the range of the partial function it computes) is Σ01 complete and so is of the same difficulty as the halting problem. Turing shows that the quoted problem is unsolvable by showing that it if it is computable then there is a Turing machine which computes a solution to the problem of determining whether a Turing machine is circle free (in modern parlance, whether it computes a total function).
- The conclusion I draw is that in 1936 Turing stated a problem equivalent to the Halting problem (although he did not have the modern terminology at hand) and proved it to be undecidable.
- The circle free problem is at a higher degree of unsolvability than the Halting problem. The former is Π02 complete and the latter is Σ01 complete.
- I do not think that the difference between various proofs of the undecidability of the halting problem is of widespread interest. The key fact is that it is undecidable.
- CMummert 21:35, 28 June 2006 (UTC)
I agree with what you have written -- I see your argument that Turing's 2nd proof is essentially the same as "the halting problem": had he put "halt" into his collection of instructions and hunted for "halt" instead of "print 0" he would have proven the unsolvability of "the halting problem". This was the key I was looking for. I agree that the various proofs are of not too much interest. I'll just figure out a way to modify the history section to be accurate as to its long journey through many minds. (You would definitely be a good editor for the Turing Proof article!) Thanks. wvbaileyWvbailey 22:40, 28 June 2006 (UTC)
- My original post was wrong (I have corrected it; you can look at the history to see my misstatement). Turing's second proof is actually very interesting. Essentially, he shows that if 0′ is computable then 0′′ is computable. I missed that on my first reading of the proof. CMummert 23:02, 28 June 2006 (UTC)
- (I'll need to get one of your recommended texts to undertand what you've written above.) I too find Turing's Proof #2 very interesting. There is something at the very end of the page, very ambiguous... I've read it a bunch of times and am left confused: "For each of these 'general process' problems can be expressed as a problem concerning a general process for determining whether a given integer n has a property G(n)..., and this is equivalent to computing a number whose n-th figure is 1 if G(n) is true and 0 if it is false."(p. 134 U). Perhaps if he had gone just one step further... added just one more sentence... he would have stated "Rice's Theorem"[?]. wvbaileyWvbailey 23:55, 28 June 2006 (UTC)
I don't know if this might be useful, but Jack Copeland's The Essential Turing (OUP, 2004) states (chapter 12, pp40)
The halting problem was so named (and, it appears, first stated) by Martin Davis.
There is a reference to a footnote, which reads
See M. Davis, Computability and Unsolvability (New York: McGraw-Hill, 1958), 70. Davis thinks it likely that he first used the term 'halting problem' in a series of lectures that he gave at the Control Systems Laboratory at the University of Illinois in 1952 (letter from Davies to Copeland, 12 Dec. 2001).
--Randomguy3 19:47, 6 October 2006 (UTC)
- Yes, randomguy3, you cannot believe how much this helps! I am (far) away from my books & library right now but when i return I will verify/double check -- This is exactly the in-print "proof" -- i.e. verifiable source in literature -- that I need to fix the page and put this to rest -- until now we have only my e-mails from Davis, and these are not "admittable as evidence" in the "court of wikipedia." Thanks very much. wvbaileyWvbailey
Reference needed
From the article:
Gregory Chaitin has given an undecidable problem in algorithmic information theory which does not depend on the halting problem.
What is the result that this sentence alludes to? A reference is necessary for such a vague claim. (I am afraid that the original author of that sentence mistook the problem of determing the Kolmogorov complexity of binary strings as “not depending on the halting problem”, when this problem is completely equivalent to the halting problem.) CMummert 12:03, 20 June 2006 (UTC)
- "When in doubt, cut it out" (and paste it here) until someone can verify it.wvbaileyWvbailey 13:46, 20 June 2006 (UTC)
I have now removed the sentence from the main article. It is archived above for future reference. CMummert 12:40, 21 June 2006 (UTC)
- I have a question for CMummert: as you maybe can see above discussions I've been trying to drill down to the ultimate (true) historical source of the "halting problem". Early this year I first came to Wikipedia with this question: why does Turing's "circle proof" seem so different than the "halting proof"? I finally went to the Dartmouth library and drilled down as far as I could go. The trail stopped at Martin Davis and perhaps Kleene in the mid-1950's (I've ordered his book). Davis in his e-mails to me references the Post paper on "Recursive Unsolvability of a Problem of Thue" (1947); this paper refers to "the same degree of unsolvability" on p. 299 (Undecidable) (last paragraph, right before the "Appendix"), So this notion of "degree" must have "been around" at least in his head, in the late 1940's. Davis told me, and another correspondent proposed (see above), that the Halting Problem's degree of unsolvability [if I said that correctly...] is less than Turing's original "circle problem" of his first proof (0-prime versus 0-prime-prime ...). I'm not familiar with the unsolvability degrees (I assume it has to do with oracles ... in fact is it O-prime (as in "Oracle-") or zero-prime? -- Davis used O not zero). Do you agree that the two (Halting versus Circle) are of different degrees of unsolvability? (Or is there something even deeper going on?) If we can back up with published evidence I believe the article needs some rework.Thanks.wvbaileyWvbailey 13:25, 21 June 2006 (UTC)
possible illustration
The above and following are derived from Minsky's proof (1967) but it is similar to the one on the article page. Some readers may find this easier to follow -- there does seem to be a lot of fiddling with the page example. If anyone thinks such a drawing is a good thing and would want me to modify or otherwise can suggest improvements lemme know and I can rework it, split it into pieces (see example below) so they're easier to see, whatever. If anyone is worried about copyright issues -- I did not cc exactly, and attribution to Minsky should be provided. If all think its a bad idea or a waste of time, lemme know and I'll just leave it here; this is easy to do once you get the hang of it. Click on the images to see better. wvbaileyWvbailey 16:13, 30 June 2006 (UTC)
Also, I found a virtually-identical version to Minsky (1967) -- but words only, no drawings -- on pages 171-172 in Edward Beltrami, What is Random: Chance and Order in Mathematics and Life, Springer-Verlag, NY, 1999. wvbaileyWvbailey 17:11, 30 June 2006 (UTC)
Undecidability of group presentations
Given two general presentation of a group, the problem of determining if they give the same group is undecidable, in the Godelian sense. Viz there is no algorithm or Turing machine that can systematically explore presentations and determine whether they specify the same group in a finite amount of time (in general -- in any particular case, you just might be able to work it out). This is isomorphic to the halting problem. Do we have an article on this?
(There is an intuitive way to look at this: for any given presentation, you can try to write out every possible string that it generates; the problem is one of trying to compare all possible strings to determine if the same set was generated. Finitely-presented groups are kind-of-like context-free grammars, so one has a similar problem there: do two different grammars generate the same set of sentences? The CFG article does briefly get into the undecidability issue.) linas 14:48, 25 July 2006 (UTC)
- This presentation-of-a-groups-stuff is way too abstract for shlepps such as meself. A google search ... any hits? Modify search until sure of your new article title. Then: BE BOLD and create your own article. Have fun! But always remember us little guys (folk without the capacity for deep abstraction -- when I read the link me eyes rolled back in me little head, yikes! where's the snooze button? ;-) wvbaileyWvbailey 01:56, 27 July 2006 (UTC)
Look at Word problem for groups, which is closely related. CMummert 02:11, 27 July 2006 (UTC)
Let me just raise one little quibble here: When you say
- the problem of determining if they give the same group is undecidable, in the Godelian sense
that's not a particularly appropriate word choice. It's important to distinguish between two quite different senses of "undecidable"; one means "undecidable as a decision problem" (that's the one you mean); the other means "independent of some fixed formal theory". The latter is the one more usually associated with Gödel, and though I prefer to use the word "independent" for that notion, Gödel himself did use the word "undecidable" in his famous paper. --Trovatore 04:18, 27 July 2006 (UTC)
Stuntz edit
"I asked for a citation a week ago, and none was forthcoming. I personally believe this is wrong. If you add it back, please include a citation."
- I agree with this edit. The first part of the paragraph seemed okay but then came the assertion under consideration. At least with regards to a Turing machine, folks are confused about what it means to "know the state of a computation". A very naive proposal for a "unproductive loop detector" would be to observe the "current instruction" -- i.e. the contents of the "state register" ("register" that holds the current instruction, Turing's "record" of a "desultory computation") -- to see if it "keeps repeating". This is obviously wrong: the TM might be in a useful loop. The less naive but still incorrect proposal would be to look at the tape's contents and see if it is repeating. Similar problem: the "state register" (instruction register) may not be repeating -- the state register can be used to "save information" (e.g. Hopcroft and Ullman 1979 p. 153, "storage in the finite control").
- A particular Turing machine in the process of a computation passes through a sequence of "complete configurations" (each representing "the total system state" at that instant). This includes (i) a list of the entire tape's contents, (ii) the location of the scanned symbol, and (iii) the current instruction's identification. Only if one were to observe all of this repeating would one suspect that the machine is trapped in a "circle" aka "unproductive loop".
- Real computers are much "worse" for such a proposal than Turing machines: they have (usually inaccessible) registers galore, and all of them would need to be 'watched' as well as the entire modifiable memory. This might be possible, but such a proposal needs to be referenced as to its source.wvbaileyWvbailey 18:30, 8 August 2006 (UTC)
The image of a 3-state busy beaver "run" implies that a string of symbols corresponding to the entries of the far right column would have to be created (i.e. all total-configuration entries concatenated into a string) and then somehow a comparison would have to be made between this evolving string (it would be evolving because it isn't halting) and all substrings to see if a substring somewhere along the (evolving) string repeats. This strikes me as either undecidable (is this a "word problem"?) or not too easy (i.e. virtually impossible). wvbaileyWvbailey 12:41, 10 August 2006 (UTC)
- When you drop down to the microcode level, registers, and even machine states, are just memory by another name, and are really few in number compared to other forms of memory. A real computer with a terabit of storage available will have, maybe, a few tens of kilobits of registers, including state registers. That's a rounding error. Now, 21,000,000,000,000 is a really huge number, but it is finite, so the problem is not formally undecidable for a finite-state machine of that size. It might not even be intractable if we simulated a PDP-8 (4K, one accumulator, one state register) on current hardware. Robert A.West (Talk) 23:24, 10 August 2006 (UTC)
- Registers are just memory, yes, but "real computers" frequently have features like truly random number generators, standard on most higher-end Intel CPUs, which cannot be treated as memory. That's an example of why I'm suggesting a very precise statement of what can be solved rather than a generalization. --Craig Stuntz 15:17, 22 August 2006 (UTC)
- This is interesting ... I'm curious. How are they creating the random numbers? Using a zener diode's noise? This is an old classic, but it must be A-to-D converted and the pulses must be filtered and held long enough to do the conversion ... it probably makes pink rather than white noise. I thought that Excel got its rand() seed from the time and date. Lemme know what you know. Thanks, wvbaileyWvbailey 17:07, 22 August 2006 (UTC)
- It's been a while since I looked, but IIRC they start with electical noise and then are selective about which bits they take. No idea about Excel. --Craig Stuntz 03:12, 23 August 2006 (UTC)
I secretly know that the following string is all 13 of the 3-state busy beaver's "complete configurations" concatenated, the concatenation repeated 5 times (shown with and without a dot between them, am not sure whether the dot is "fair" or not). Can you honestly believe that you-as-algorithm can look at something like this and reliably give me a "yes-will-halt" or "no-will-not-halt? And this is just a silly ole teeny-weeny baby busy beaver. Even to reliably examine the most wimpy of cases such as this, such a person-machine would be quite accomplished .
- A0B011A111C0111B01111A0111B1111B1111B1111B11111B0111111A1111111C111A0B011A111C0111B01111A0111B1111B1111B1111B11111B0111111A1111111C111A0B011A111C0111B01111A0111B1111B1111B1111B11111B0111111A1111111C111A0B011A111C0111B01111A0111B1111B1111B1111B11111B0111111A1111111C111A0B011A111C0111B01111A0111B1111B1111B1111B11111B0111111A1111111C111... etc.
- A0.B01.1A1.11C0.111B0.1111A0.111B11.11B111.1B1111.B11111.B011111.1A11111.A0.B01.1A111C0.111B0.1111A0.111B11.11B111.1B1111.B11111.B011111.1A11111.A0.B01.1A1.11C0.111B0.1111A0.111B11.11B111.1B1111.B11111.B011111.1A11111.A0.B01.1A1.11C0.111B0.1111A0.111B1.11B111.1B1111.B11111.B011111.1A11111.A0.B01.1A1.11C0.111B0.1111A0.111B11.11B111.1B1111.B11111.B011111.1A11111....etc.
There's something like 340 symbols shown here (approx 68 per each of 5 strings, but this secret fact is only known to me). Each symbol can be one of 5 { 0, 1, A, B, C }. (What the heck is the log-base-2 of 5? approx 2.2 lets pretend.) Anyway, 340x~2.2 is what about 700, so we have 2^700, a pretty big number of possible strings (5.26 x 10^210 or something like this). But I speculate that there's a permutation-combination issue that amplifies this by orders of orders of magnitude, re busy beavers. All strings 1 to 340 (and up to ad infinitum as the number of symbols grows) have to be compared to our evolving big number above as our machine looks for "circles" (repeating unproductive loops). The same huge numbers explain why no one has been able to solve the 6 or 7-state or 8-state busy beavers. We're talking calculations going on to the ends of this universe and all other universes known and unknown. If that's the case then our "string" cannot be decoded to demonstrate whether it is from a machine trapped in a loop -- the universe and all others will die and wither away long before a definite answer is known. All matter of these universes will be involved in the computation ... and we have just gone from mathematics to an argument of philosophy -- what does "infinite" mean/signify? I have my opinions. Stuntz is right to demand a source for what appeared to be speculation.wvbaileyWvbailey 01:24, 11 August 2006 (UTC)
- The log-base-2 of 2 is by definition 1. The issue of what "infinite" means in this context is not a matter of opinion, Cantor and others did the work long ago. In this case, there are clearly locations in the memory of a Turing machine, and locations in the memory of any real computer. for all k,N. Finite numbers that exceed the age of the universe in picoseconds are still finite and a problem can be computationally intractable without being formally undecidable. Robert A.West (Talk) 04:17, 11 August 2006 (UTC)
- BTW, no dispute that the statement should be sourced — I just remark that it happens to be true, and that the maddening difficulty with sourcing it is going to be its very obviousness. It is more likely to appear in a textbook as an exercise or "question for discussion" than in the main text. Robert A.West (Talk) 04:20, 11 August 2006 (UTC)
- Robert and I discussed this on my talk page, where I commented that I have no objection to the more precise statement he made there. --Craig Stuntz 12:35, 11 August 2006 (UTC)
- And where you remarked that termination analysis needs writing, and that the quantitative issue of tractability should be addressed there. Robert A.West (Talk) 16:23, 11 August 2006 (UTC)+
- I have made an edit to algorithm that references termination analysis. But I don't have the background/experience to write an article on it. The edit does reference Halting problem. Anybody out there with the requisite knowledge? It sorely needs an article. Nah, in the spirit of WP:BE BOLD, here's what I'll do. I'll create the page, cut and paste a definition that I found via google. Then other more knowledgeable folks can flesh it out.wvbaileyWvbailey 15:30, 31 August 2006 (UTC)
Silly me. I meant log-base-2 of 5 not 2, above (now corrected). All this infinity stuff may be obvious to you, but to me it's debatable [non-obvious] because I'm not a Platonist, but rather (I'm evolving into) a strict constructivist: If you can't build it (demonstrate it, produce it), then as far as I'm concerned, it doesn't exist. And since you can't build your machine -- the problem is "intractable" -- such a hypothetical machine doesn't exist for a constructivist as an arguing point. But, if we agree to adopt a Platonist stance then I do agree that we just add on more "memory" or more time, (ad infinitum in the Platonist sense) until our tester-machine makes its determination. As you suggest this discussion could go elsewhere.wvbaileyWvbailey 18:11, 11 August 2006 (UTC)
Error?
At the end of the 2nd paragraph in "Common Pitfalls", shouldn't the text be:
...that repeats a previous state, is known to “halt”.
instead of:
...that repeats a previous state, is known to “not halt”.
62.195.243.191 15:40, 12 August 2006 (UTC)
- No, the article text is correct. If it repeats a previous state, then the continuing execution will follow the same path as before, leading to a repeat of that state again and again, in a never-halting infinite loop. -- Four Dog Night 17:59, 12 August 2006 (UTC)
Assumption that trouble is a program
What is the grounds for assuming that trouble is a program? For example, a listing with unreachable code is not a program even if the reachable parts are. What are the cases a string must satisfy for it to be a program?Hackwrench 08:54, 31 August 2006 (UTC)
- Regarding whether "trouble" contains unreachable code:
- If "halt" has a constant result, then it can't be a solution to the halting problem because some programs halt and some don't.
- If "halt" is not constant, then nothing in "trouble" is a priori unreachable, because the only branch depends on external input.
- In most languages and systems it is quite easy to put obviously unreachable code in a valid program. But even if unreachable code recognition is imagined to be perfect, the proof still works, and then it is clear that recognition can never be perfect.
- Gazpacho 08:37, 27 September 2006 (UTC)
- Except, it seems to me that in order for "trouble" to be a valid program, halt cannot be considered external to it, and since the string "passed" to "trouble" is essentially trouble itself, then trouble has no external input, for that would be saying that trouble is external to itself which is nonsensical. I am using the definition that a program is only a program once all dependencies are linked in, the dependencies then part of the constitution of the program and that's one of the problems I have with this article is that no rigorous definition of "program" is applied. Hackwrench 10:09, 27 September 2006 (UTC)
No formal definition of "program" is applied because the purpose of the sketch is to explain how the proof works without obscuring and entangling it with a particular formalism. The statement of the problem presupposes that you have a scheme for representing programs as strings, one that enables you to analyze the string to make conclusions about the program. That scheme determines which strings represent programs. All that you need to get "trouble" from "halt" is a way to sequence programs and a way to conditionally branch; any interesting programming language has these.
The sketch doesn't say that "halt" is 'external' to "trouble"; you can imagine the source code of "halt" appearing inline in the source code for "trouble if you want. As for "trouble" being 'external to itself', I don't know what you mean. It isn't the case that "trouble" has no external input, it has one input that can be the source code of "trouble" if you choose. Gazpacho 20:41, 5 October 2006 (UTC)
Cognition level
At a certain level of cognition, Trouble is the same function whether it is calling Halt or it's counter function DoesNotHalt. Only once you get to the point where you have the cognitive ability to make an association with the inputs to certain properties that they are expected to express. If Halt only receives Trouble, it has no way of knowing that the symbol halt refers to itself and thus cannot trace into itself. I have a problem with that being the case, and I don't know why. Perhaps it has to do with the fact that if you were to pass both Trouble and a linkage table, it seems the argument changes? Hackwrench 09:58, 27 September 2006 (UTC)
There's no requirement that "halt" needs to be able to recognize itself in its input, and nothing says that "halt" may receive only the source code of "trouble". In fact, it was claimed to be able to take any program in the world, regardless of how it was constructed, and decide the halting problem for it. One counterexample is enough to refute that, and the sketch merely describes how to find such a counterexample.
If your complaint is that there has to be some reason that "halt" can't do what it has to do, well, that's the whole point of the proof, to show that there does have to be a reason. Gazpacho 19:22, 5 October 2006 (UTC)
Separation of function and algorithm
The article would also be more useful with a clarification of what is meant by the separation of function and algorithm and why that separation serves any purpose. Hackwrench 10:17, 27 September 2006 (UTC)
Formalization of the halting problem
The section "Formalization of the halting problem" talks only about the formalization of the concept of an algorithm and is at best incomplete. Hackwrench 10:22, 27 September 2006 (UTC)
Comment 2006-9-27
I looked through the article this morning, and made a few minor edits. Here is a list of things that I noticed when looking through:
- The section on "importance" overlaps with the section on "Godel's theorem".
- The section on "common pitfalls" is not as clear as it could be.
- The section on "formalization of algorithms" could be made more clear.
- In the section on Godel's theorem: neither this page nor the page axiomatization says that an axiomatization must be r.e. This is most likely the fault of the page axiomatization, but it could be clarified here. Also, I think the meaning of the word "sound" here is not the standard one. What is intended is: the set of true formulas for the standard model of natural numbers is not r.e., and thus there is no complete sound effective axiomatization of the theory of the standard natural numbers.
This article is currently 35KB, while the recommended limit is 32KB, so some cutting is required.
- The section on history could be made into two or three paragraphs instead of a long list.
- The notes section could be shortened.
I plan to work on these over time; I am listing them here to remind myself and to share the work.
Feel free to use the <del> tag to strikethrough completed ones. CMummert 13:02, 27 September 2006 (UTC)
- The 32K "limit" is an out-of-date concession to obsolete and buggy browsers, nothing more. Many featured articles greatly exceed that threshold. Arbitrarily chopping up an article to be less than 32K is IMO a bad idea. Robert A.West (Talk) 16:29, 8 October 2006 (UTC)
- The technical reasons for an exact 32K cutoff are not convincing, but it's still a pretty good rule of thumb, I think. Overly long articles are hard to navigate for readers and hard to maintain for editors, and while I'm generally opposed to structuring articles for the convenience of editors, if editors find them hard to maintain, then readers will eventually suffer.
- An article could profitably be much longer, if the writing were tight and well-organized. But how is it going to stay that way, in a long article? What's going to happen in practice is that editors are going to keep adding material in random locations, stuff that isn't obviously wrong (so not likely to be reverted), but that over time turns a coherent presentation into a long, chatty ramble. --Trovatore 18:00, 8 October 2006 (UTC)
- I've discussed with CMummert re a trim: As soon as I can get back to my books (in a week or so) and I can verify the quote re Davis as source of the name "Halting problem", etc., I will trim the history. Most of the history can now be found at algorithm. I should be able to trim the footnotes as well. This should help, a bit. wvbaileyWvbailey 19:05, 8 October 2006 (UTC)
the halting problem is partially decidable, not undecidable
It seems that nobody has remarked a complaint about the *semidecidebility* of the problem. Please, make a distinction between problems that are
- decidable (recursive)
- partially decidable (eventually solvable)
- non decidable (any algorithm never stop)
—The preceding unsigned comment was added by 131.114.250.34 (talk • contribs) 09:58, 8 October 2006 (UTC)
- I just added that in the past week under "pitfalls." Perhaps it's not as prominent as it needs to be, but I think that's part of broader problem. Gazpacho 00:37, 10 October 2006 (UTC)
Um, a problem that's not decidable is by definition undecidable. Even if it's semidecidable. 131.114.250.34, what do you mean by "eventually solvable"? There's an obvious algorithm that, given a Turing machine, will eventually decide if it halts, in the case that it does halt, but not in the case that it doesn't. That doesn't sound like an "eventual solution" to me. --Trovatore 00:59, 10 October 2006 (UTC)
Sorry, I mean that the algorithm eventually stops, as you said. But "undecidable" (or "not decidable") and "partially decidable" (or "semi-decidable") are not the same thing, and this difference should be stated clear. My name is Alessandro. —The preceding unsigned comment was added by 131.114.250.34 (talk • contribs) 17:35, 19 October 2006 (UTC)
- Ciao, Alessandro, e benvenuto. Ma non vorrai farti un account?
- There's nothing deep here; this is just a matter of definition. If a problem isn't decidable, it's undecidable, period. Now it may also be semi-decidable, but that doesn't stop it from being undecidable. (By the way, semi-decidable doesn't imply that it isn't decidable; if you want to be specific you have to say something like "undecidable and semi-decidable". A decidable problem is automatically semi-decidable, as semi-decidability is a weaker condition.)
- Now it's not clear to me whether you have some deeper misunderstanding here than the one purely about the words. What do you mean by "the algorithm eventually stops"? Which algorithm, the input one, or the one that tries to decide whether the input algorithm terminates? --Trovatore 19:50, 19 October 2006 (UTC)
- There may be something a bit deeper here having to do with observers standing outside a system. Kleene (1952) allowed this possibility: that a test-algorithm emits "u" for "I haven't decided yet, work is still in progress . . .". The test-algorithm continues to (periodically) emit "u" until it arrives at its decision: "This particular input-algorithm (the algorithm-under-test) will halt (or not halt)." As observers may be tempted to feel a bit of (but just a little bit of) confidence that the testing-algorithm itself hasn't become locked up in a "tight loop emitting u" perniciously brought about by the very input-algorithm it is testing (e.g. our test-algorithm has become infected with a deadly virus). But given this isn't the case (how can we be sure?), our "u"-emitting test-algorithm in no way solves the halting problem -- it may just go on and on emitting "u", never arriving at its decision. Thus at any time we observers have to consider (at least) eight possible outcomes (perhaps displayed by 3 signal-lights: "H", "~H", "u") -- (i) H: halts, (ii) ~H: doesn't halt, (iii) blinking u: don't know--work is still in progress, (iv) blinking u: don't know-- test-algorithm is caught in a tricky-but-pernicious loop, (v) u is blank: woops something is very wrong--test-algorithm has stopped emitting "u", (vi) stuck u: woops, something has locked up the test-algorithm, (vii) stuck "H" and "~H" simultaneously: test-algorithm is locked, (viii) stuck "H" and "~H" and "u": test algorithm is locked. Most of these are decidable by us onlookers. But we onlookers are faced with a quandry regarding (iii) and (iv): as long as a "u" is presented the matter remains undecided in two ways. wvbaileyWvbailey 14:45, 13 June 2007 (UTC)