Encyclopedia > Talk:Halting Problem

Article Content

Talk:Halting Problem

I think the material about Chaitin would maybe better fit on the page about Gödel's incompleteness theorem. Does anybody have good references or introductory material about that work? --AxelBoldt

The page was incomprehensible to a non-programmer; it used Scheme code which a non-programmer would have no chance of understanding. It also used unclear and poorly defined terms a lot, such as a "computing system". Some content (Scheme with real numbers) was too advanced for a general-purpose article describing the Halting Problem. I append below stuff from the page as it was before this change which someone might want to salvage and use here or elsewhere. --AV

[... old material deleted ...]

Thanks, the page is so much better now!

I wonder if you think the following trivia would be worth putting on the page: for an actual existing computer with a finite amount of RAM and external storage, the halting problem is of course solvable. If the number of internal states is N, you can just wait for N+1 steps to see if a state returns.

Also, do you know anything about the Chaitin connection? --AxelBoldt

I think it's better to put this somewhere on a page devoted to computability models, which should be written. Maybe I'll give it a shot later. Once it's written, it'd be linked from here, and anyone not sure why one needs unlimited memory could go there and read that.

I do know something about the Chaitin connection, but I question my memory, have been some years. I'll try to check it further, but right now it seems to me that this doesn't belong on this page, this information is not important enough for the general article on the halting problem; it can be relegated to a page on Chaitin and his results. -- AV

I like some of the things in the latest change, that make the description and the proof more clear, and dislike some others. Specifically, I refactored the page and rewrote the proof precisely in order to make it easy for a layman with no mathematical training to understand. There's no real reason to employ notation like H:N->N, or the notion of a partial function and undefined values in the sketch of the proof. Sure, it makes it somewhat more elegant, but accessibility of the idea to someone without a university education in CS or math is lost. Similarly, some redundancy in my version, e.g. stating the problem separately as an algorithm to solve the problem and an algorithm to compute the halting function which embodies the problem, was intentional.

Unless there are objections, I will try to integrate the nice things about the latest change with the easier-to-understand-for-a-nonspecialist version of the proof. --AV

No problem. I already made the proof sketch less formal myself. If you want to change it more, that's fine with. -- JanHidders

I think it is important to have a completely accessible definition of the problem and sketch of the proof; after all, it is one of the major intellectual highlights of the 20th century to see that there are well-defined problems that cannot possibly be solved with an algorithm/program.

But I also think that Turings approach is really important. How about if we restructure the article as follows:

Start with a colloquial description of the problem along the lines of "Find a program/algorithm, which takes as input the description of some other program/algorithm plus some input for that program, and decides whether that program, when fed that input, will ever halt".
State that provably, no such algorithm exists, and give implications (problems that computers can never possibly solve, Entscheidungsproblem)
Then give the colloquial proof sketch without lisp syntax and without Turing machines and without the Halting function
Then describe the formally correct version of the problem, and give the argument that this formalization actually captures the full content of the colloquial description (Church-Turing thesis).
Then comes Turings diagonalization argument
Pointers to generalizations (Rice's theorem)

That way, a reader can stop reading article as soon as the material gets too advanced, and they will still have gotten a for them adequate explanation.

Ok. I gave it a shot. Let me know what you think. I wanted to add some more on how the Halting problem can be formulated as a statement about numbers, but I'm rather time-pressed at the moment. My apologies to Anatoly, because I more or less promised him to leave the article to him. -- JanHidders

Is it correst to say that Turing was first? I always thought it was referred t as the Church-Turing thesis, since it was proven almost simultaneously. I know that Alan Turing's infinately more interresting than Church, but he (and his solution) is left out of the article altogether.

You are right that Church was first. (Turing says so in his own article) But the Church-Turing thesis is not about the Halting problem and I'm not sure I would agree with your statement that Turing is infinitely more interesting than Church. :-) -- JanHidders

It is true that Church was first in solving the Entscheidungsproblem, but I'm not so sure that Church talked about the halting problem at all; after all, in order to even define the Halting problem, you need to have a formal concept of some machine that may or may not halt. Church was using his lambda calculus to solve the Entscheidungsproblem. It certainly is possible to formulate the halting problem in lambda calculus, but did Church actually do it? --AxelBoldt

Hmmm. You may be right. I more or less assumed that Church had shown that the Entscheidungsproblem is undecidable by showing that the problem whether a certain lambda expression when applied to another lambda expression is defined or not, is undecidable. But I am not really sure of this. I will revert my changes and come back when I have found Church's article in the library. -- JanHidders

If you have access to http://www.jstor.org then you can read both of his articles online. The citations are on the Entscheidungsproblem page. The substantial one is the one in the American Journal of Mathematics. Church proves that there is no algorithm (defined via recursive functions) which decides whether two lambda-calculus expressions are equivalent. The proof relies heavily on Kleene's earlier work on the lambda-calculus. --AxelBoldt

Thanks for the enlightenment. Perhaps it should be more clearly defined as Turing's solution to the Entscheidungsproblem. And it's perhaps not so important that he solved the halting problem first, since he proposed it. Man, I'm coming off really anti-Turing today... --Eventi

Well, the article is about the Halting problem, not the Entscheidungsproblem, so I think it is important to mention who proposed it first and who solved it first. --AxelBoldt

Was it seperately proposed and then solved? If so, I agree. But there was no such thing as a halting problem before the Turing machine, so I doubt it. I don't think it's incorrect by any means, only that solving first is too trivial an accomplishment to mention.

Ok, maybe we should say "was proposed and solved in Turing's paper..." --AxelBoldt

I've corrected an important error, vis. the statement that the incompleteness theorem follows directly from the undecidability of the halting problem. I'm not completely satisfied with the way I've done that, however; anyone who can improve the language/clarity - please do it.

One important problem which perhaps isn't unique to this page is that I feel it wrong to talk in Wikipedia about "Goedel's Incompleteness Theorem". There are in fact two theorems, and either of them is sometimes referred to as "Godel's Incompleteness Theorem" (the first more often than the second), creating confusion. I'd prefer to always use "...theorems" or to refer explicitly to the first or to the second.

W.r.t. the particular page, I think it especially unfortunate that it still requires knowledge of a programming language to understand the sketch of the proof. There's no justification of that IMHO. The Pascal version is certainly lighter on the layman than the original Scheme version, but the verbal description of mine in rev. 11 is still better, I think. I'll bring it back and try to make it even simpler and less verbose, as soon as I find some time to work on that - if there're objections, please speak out. --AV

Good to see that you're back! I agree that a non-programming-language version would be desirable. Also, in light of your above comments, I think we should probably remove the paragraph early on talking about Goedel's incompleteness theorem and pack the whole discussion in the corresponding section later on; after all, Goedel's theorem had been proven earlier and the fact that a weaker version of it can be reproven using the Haling problem is not that amazing after all.

I agree. I'll do that when I find time to refactor the page (or anybody should feel free to do that before). In fact, there's an even conceptually simpler proof of Godel's first than with the undecidability of the halting problem - it's the proof via Tarsky's undefinability of truth. One: 1) establishes a coding for formulas and coding for sequences; 2) establishes a formula phi(x,y) which is true in N iff y codes a proof of x using axioms of Q; 3) notes that if Q is sound and complete then "there exists y s.t. phi(x,y)" defines precisely all sentences x which are true in N; 4) this contradicts undefinability of truth in N, which states precisely that a formula defining true sentences does not exist (this is the correct formalisation of the Liar paradox and is proved accordingly). Step 1 is technical and step 2 is very simple, while steps 3 and 4 are immediate observations. --AV

I think we should add something to the Goedel's theorem article about "soundness not required". I'm still not quite clear about the exact requirements that Goedel needs for his proof to go through though. --AxelBoldt

soundness is completely unnecessary for both statement and proof of Godel's theorems; in fact, nothing about truth or falsity is ever used, the theorem is completely proof-theoretic. This very important fact is often overlooked for several reasons, e.g. existence of simpler proofs that require soundness (via halting problem or via Tarski's undefinability theorem); another reason is Goedel's unfortunately worded introduction to his paper where he draws a (largely misguided) parallel with the Liar paradox, which is all about truth and falsity. We should clarify this on the goedel's theorem page.

the requirements for the first theorem are: that a theory Q be recursively axiomatizable; that it extend (or more generally interpret) a certain very weak theory of arithmetic; that it be omega-consistent. The conclusion is that Q is not complete. With Rosser's trick, the requirement of omega-consistence is weakened to consistence. --AV

"extend a very weak theory of arithmetic": does that not mean that the provable arithmetical statements of the weak theory (which are presumably true) are also provable in Q? In other words: Q has to be a little bit sound? --AxelBoldt

nope, that's why in general case we allow "interpreting", not necessarily extending. This means that we may map the axioms of the weak theory to different sentences, which aren't necessarily true at all, in such a way as to preserve proof-theoretic strength. Essentially what we are after is the power of representation that the weak theory has: e.g. given a recursive function f(x), we want there to be phi(x,y) s.t. the theory proves phi(x,y) whenever f(x)=y and proves not(phi(x,y)) whenever f(x)!=y. Now in the original weak theory this phi(y) will just embody whatever way of building the recursive function up from basic building blocks that we choose (e.g. it may embody a Turing machine or a process of defining the function from basic recursive functions, iterations, etc.), so phi(x,y) will actually be true whenever f(x)=y. But we don't really care about that in Goedel's proof, we just need the theory to be strong enough to prove/disprove phi(x,y) according to whether f(x)=y. So the Goedel's theorem will apply to very convoluted and extremely not-sound theories Q as long as there's a way to faithfully map the "real" sound phi(x,y) proved/disproved by the weak theory into some phi'(x,y) proved disproved by Q, without any regard to its truth in N. --AV

I did my homework and read again some of Penrose's writings connected with the halting problem. Penrose presents the core of his arguments connecting the halting problem and related ideas to conscious understanding in section 2.5, pages 72 to 77, of ?Shadows of the Mind?. The following summarizes his approach:

Although by Godel?s arguments no Turing machine can answer the general halting question, we could speculate on the existence of a Turing machine that does as well as possible in the sense that it captures all the methods that conscious being could possibly use.

Does he say this machine is correct (for those instances where it returns an answer, the answer will be right)? Does he say we can know that it is correct? I understand he goes on to prove it can't exist. I mean what's the initial assumption at the start of the proof? --LC

Penrose requires that the machine is always correct whenever it concludes that an algorithm does not stop (i.e., the machine is "sound"). Penrose describes an algorithm that we know will not stop, but that stumps the machine; so, the machine fails to capture all of our reasoning powers. This argument seems to assume that we are "sound"; one objection to Penrose is the contention that we are all unavoidably inconsistent. In which case I don't have to be embarrassed that I may be writing nonsense.

Thanks. How about the second question I asked? If someone hands me this machine (which happens to be sound), does he assume I'll look at it and know it's sound? --LC

Applying Cantor?s diagonal construction, Penrose shows that no such machine exists: for any Turing machine that addresses the halting problem, there is an algorithm that conscious being know will not stop but that stumps the Turing machine. This does not mean that the particular algorithm in question will stump all Turing machines, it only means that no single machine exists that will succeed on all algorithms that conscious being can analyze.

Penrose does not claim that conscious beings can answer the halting question for all algorithms, he is not even claiming that there are algorithms that only conscious beings can analyze; he is just saying that for any given Turing machine there is an algorithm that we can analyze that stumps that particular machine (another machine might succeed). The implication, Penrose maintains, is that the reasoning power of a mathematician cannot be captured by a (single) computer. A possible objection is that, if one computer will not do the job, then use many. Penrose addresses this type of objection and many others in ?Shadows?.

I don't see this implication at all. For a given Turning machine, there is an algorithm that it can't analyze. So what? For a given mathematician there are a lot of algorithms that it can't analyze.

The implication seems plausible to me because the argument shows that every Turing machine falls short of accomplishing all that a mathematician can do: for each such machine there is at least one halting problem the mathematician can solve that the machine cannot. So, it does not seem possible to model the mathematician as a machine. (Admittedly, my paraphrase of the argument is very informal and imprecise). The fact that machines can solve many problems that stump the mathematician is not relevant to the argument.

I'm still trying to find time to put these thoughts into an article that won't make me blush. I have collected a bunch of reviews and commentary on these issues. --srwenner

If we say that most mathematicians disagree with Penrose, then we should name some critics and present their objections, either in this article, the Penrose article or the Incompleteness Theorem article. The last time I looked, I did not see such specifics.

The electronic journal Psyche published a symposium on ?Shadows of the Mind?, with articles by many scholars and a reply by Penrose: ([[:http://psyche.csse.monash.edu.au/psyche-index-v2|http://psyche.csse.monash.edu.au/psyche-index-v2]]). Perhaps we could summarize the key objections and Penrose?s rejoinders in the Penrose article. I could take a stab at this, if you wish (I hesitate to edit others? work without their blessing). SRWenner[?]

This is interesting stuff. I'd prefer to have a separate article like "Philosophical implications of the halting problem" or similar, link to that article from here and from Penrose, and explain arguments and counterarguments there. That article could then also get the paragraph about "humans and the halting problem" that's currently still in this article (and in light of your explanation above now seems pretty pointless). The reason that I'd prefer a separate article is that it can easily grow into a quite sizable article whose topic is somewhat removed from the halting problem proper that computer scientists are interested in. --AxelBoldt

For an amusing illustration of the basic flaw in the Penrose/Lucas argument have a look at http://www.frc.ri.cmu.edu/~hpm/project.archive/general.articles/1994/941219.penrose.2.review -- Derek Ross

Perhaps it's interesting to mention that the undecidability of the PHS property follows trivially from Rice's theorem. -- JanHidders

All Wikipedia text is available under the terms of the GNU Free Documentation License

Search Encyclopedia

Search over one million articles, find something about almost anything!