Wikipedia: Halting Problem/Talk

I think the material about Chaitin would maybe better fit on the page about Goedels 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