Misplaced Pages

Revision as of 20:02, 15 October 2009

Mathematics Unassessed High‑priority

This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Misplaced Pages. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics ??? This article has not yet received a rating on Misplaced Pages's content assessment scale. High This article has been rated as High-priority on the project's priority scale.

Archives

Talk:Halting Problem: 2001-2002 Archive 1: 2002–2005 Archive 2: 2006 Archive 3: 2007–2009

Has it been noted?

Formally a Turing machine M is a tuple (Σ,Γ, Q, δ) where Σ,Γ,Q are finite nonempty sets with Σ Ç Γ and b G Γ − Σ. The state set Q contains three special states q0,qaccept,qreject. The transition function δ satisfiesδ : (Q − {qaccept,qreject}) × Γ → Q × Γ × {−1,1}If δ(q, s)=(q ,s ,h) the interpretation is that if M is in state q scanning the symbol s then q is the new state, s is the symbol printed, and the tape head moves left or right one square depending on whether h is -1 or 1.We assume that the sets Q and Γ are disjoint.A configuration of M is a string xqy with x, y G Γ∗, y not the empty string,and q G Q.The interpretation of the configuration xqy is that M is in state q with xy on its tape, with its head scanning the left-most symbol of y.If C and C are configurations, then CM→ C if C = xqsy and δ(q, s) =(q ,s ,h) and one of the following holds:C = xs q y and h = 1 and y is nonempty.

C = xs q b and h = 1 and y is empty.C = x q as y and h = −1 and x = x a for some a G Γ.C = q bs y and h = −1 and x is empty.A configuration xqy is halting if q G {qaccept,qreject}. Note that for each non-halting configuration C there is a unique configuration C such that CM→ C .The computation of M on input w G Σ∗is the unique sequence C0,C1, ... of configurations such that C0 = q0w (or C0 = q0b if w is empty) and CiM→ Ci+1for each i with Ci+1 in the computation, and either the sequence is infinite or it ends in a halting configuration. If the computation is finite, then the number of steps is one less than the number of configurations; otherwise the number of steps is infinite. We say that M accepts w iff the computation is finite and the final configuration contains the state qaccept.

--Musatov

Problematic sentences

Hi,

I find this language a bit problematic:

Given a specific algorithm, one can often show that it must halt for any input, and in fact computer scientists often do just that as part of a correctness proof. But each proof has to be developed specifically for the algorithm at hand; there is no mechanical, general way to determine whether algorithms on a Turing machine halt. However, there are some heuristics that can be used in an automated fashion to attempt to construct a proof, which succeed frequently on typical programs. This field of research is known as automated termination analysis.

Namely, there is a mechanical way to prove the termination for exactly those algorithms that can be proven by such a (finite-length) mathematical proof: Generate all such proofs up to a given length (the limit can be set arbitrarily high, higher than any human could hope to do) and check them for correctness. If a proof has been found, the algorithm does indeed terminate; if not, no such proof exists and could not been found by a human either. Hence a human is not "stronger" in this sense than a purely mechanical Turing machine.

Also WTF does the "See also: Watchdog timer" do here :D --SLi (talk) 21:46, 30 March 2009 (UTC)

The quote simply says, "there is no mechanical, general way to determine whether algorithms on a Turing machine halt". It is true that if the computation does halt you can tell this; but if it does not halt there is no general way to determine so by mechanical means (it may not be provable from a given set of axioms that the program does not halt). The quote above does not say there is no mechanical way to search for a proof that a program halts. — Carl (CBM · talk) 22:04, 30 March 2009 (UTC)

Somehow it seems like it says that there may be a "specific" way of proving some algorithm halts, while my argument is that if there is such a proof that a given Turing machine always halts, it can be found by an entirely general algorithm, not "specific" to the "algorithm at hand" (and certainly not only by a computer scientist). That's what disturbs me in this language. --SLi (talk) 22:27, 30 March 2009 (UTC)

Your argument shows how to find the proof, but the proof that your argument finds will still be specific to the algorithm in question (although this "specificity" may seem trivial). However, when computer scientists actually prove that some algorithm always terminates, they don't use an exhaustive search for a proof, they use some ad hoc argument, maybe involving loop invariants or something like that. Maybe the "has to be" could be changed to "is". — Carl (CBM · talk) 22:35, 30 March 2009 (UTC)

Yes, the proof is specific to the algorithm, unless you consider it a proof that the Turing machine that computes and checks those proofs terminates when given the algorithm. However if interpreted that way, the second part of "But each proof has to be developed specifically for the algorithm at hand; there is no mechanical, general way to determine whether algorithms on a Turing machine halt" seems, while true, misleading when combined with the first part, since theoretically the developing of the proof can be done entirely mechanically. --SLi (talk) 22:47, 30 March 2009 (UTC)

It's not completely clear to me that an exhaustive search for a proof counts as "developing" the proof. In any case, when people in computer science prove that algorithms terminate, they do not do so by making an exhaustive search for a proof (people don't prove mathematical theorems that way, either). The usual CS way of proving algorithms terminate is to do an ad hoc analysis of the algorithm at hand and write a custom proof for that situation. So if you want to change "has to" to "is", that seems OK.

But I don't believe the current language is actually inaccurate, since it could be argued that the exhaustive search does count as "developing" a proof, and nobody does exhaustive search anyway. And the text does not claim that it is impossible to search for a proof, only that there is no mechanical way to separate halting programs from non-halting programs. — Carl (CBM · talk) 01:39, 31 March 2009 (UTC)

Of course exhaustive search is not how it's done in reality, but then people don't write their algorithms in Turing machines either. Fast or slow is so far removed from the topic of this article, it's mostly just about whether it can be done in finite time by a Turing machine or not (especially since we are talking about the halting problem). The Turing machine model is so far from actual reality that I'm afraid bringing in people proving that an algorithm always halts in such a context only serves to confuse the reader into thinking it's something that a person can do but a Turing machine, as a computational model (not as a concrete machine) cannot.

I'll try to think if I could come up with some less confusing language. --SLi (talk) 01:49, 31 March 2009 (UTC)

The proof is invalid

The halting proof diagnolization argument implies an algorithm that simulates an input machine on it's own encoding. This is the realization of "diagonolization". This algorithm takes one input, copies it, and then gives the original input code the copy as input. It must do so in order to ensure that the program runs only on itself. The article calls this machine G.

Because of the fact that the halting algorithm needs algorithm "code" and input to that code, it is necessary that the halting algorithm traces the input machine to some degree. It must be traced a certain amount in order for it to gain meaningful information. I claim that the amount required ensures it would trace it through the action of copying the input and running H in the case of Machine G.

So, G recieves (G) as input. (G) is the code of G. G copies the (G) and gives (G)(G) to the halting algorithm. The halting algorithm traces G on (G). And we are back where we started - an infinite loop.

This is the reason for the contradiction arrived at, not the existability of a halting algorithm. —Preceding unsigned comment added by 96.32.188.25 (talk) 22:25, 18 May 2009 (UTC)

WRONG again. See refutations of the argument presented by similar anon contributors at Talk:Halting_problem/Archive3#Article_Halting_proof_fails (March 2009), Talk:Halting_problem/Archive3#proof_fails (November 2008). Talk:Halting_problem/Archive3#Proof_is_invalid. (August 2007), Talk:Halting_problem/Archive1#Big_Trouble_in_Proof.3F (2002) — Arthur Rubin (talk) 22:40, 18 May 2009 (UTC)

What if You traced state of variables (not constants, stack ...) at each position (instruction) of program. If that state at certain position repeated You have found infinite program. But only if You can trace these things, otherwise I do not know. But if You can Halting problem is solvable.

Of course running program which never halts and waiting for it to halt is BS ;). You'll wait forever. 84.16.123.194 (talk) 08:53, 26 May 2009 (UTC)

Only question is whether You can create such program that never finishes. Like enumeration of natural numbers, but of course no overflow is considered here. Also program which rewrites itself may be a problem on infinite(!) tape.

i = 1 ; while ( i < INFINITY ) { print i ; i := i + 1 } // if i never overflows => program never halts ; 
// comparing to INFINITY might be problem?
i = 1 ; while ( 0 < i ) { print i ; i := i + 1 } // this'd work ;)

I have seen some "proofs" of tested program call the testing program, WTF is that? Why should tested program know about him? I think that presuming such knowledge is trap.

It may be valid program, but it is quite a special case. Although the other program might be calling arbitrary programs (on arbitrary addresses, so that he may find tester) on a tape IRL and run tested program ...

I feel (=> don't have proof), that making one program call other program, which then calls first one, just for sake of creating recursion is not valid at all.

If I'd create testing program I'd be sure not to let the tested program know about tester, otherwise there's gonna (might => going to :) ) be circle and that is what I do not want.

To me turings "proof" is interesting thing to consider when making testing program, nothing more. AMIRITE?

Also it is quite paranoid because You may not know even IRL whether other program inside tested won't call tester, or whether some machine bug won't do that :). It is quite similar to paranoia in Ken Thompson's lecture ;) . 84.16.123.194 (talk) 09:30, 26 May 2009 (UTC)

Artificial Intelligence and the Halting Problem

I'm surprised that there isn't even a paragraph on the use of the Halting Problem in the philosophy of AI to discriminate (rightly or wrongly) between what computers and humans can/can't do. —Preceding unsigned comment added by 121.45.215.163 (talk) 11:05, 16 July 2009 (UTC)

If there is a reliable, mainstream source that discusses it, then by all means put it into the article. But since neither computers nor humans can solve the halting problem, it doesn't appear initially that the halting problem would separate the two. — Carl (CBM · talk) 11:13, 16 July 2009 (UTC)

Afraid I don't know the precise reference - but I'm pretty sure that Roger Penrose covered it in The Emperor's New Mind - actually, WP discusses it in his article - http://en.wikipedia.org/Roger_Penrose#Physics_and_consciousness - but doesn't give the reference either. —Preceding unsigned comment added by 121.45.215.163 (talk) 12:33, 16 July 2009 (UTC)

We could probably add a sentence pointing to Roger Penrose, but it's important to remember that his theories about mathematical philosophy are somewhat idiosyncratic and don't have broad consensus in the field. So Penrose's opinions need to be attributed directly to him when they are presented. — Carl (CBM · talk) 12:37, 16 July 2009 (UTC)

There has been extensive discussion of the issue in the mainstream philosophical and cognitive-science literature. I believe that Dennett addresses the matter in Kinds of Minds, for example, and does so not as a new issue but as an oh-well-I-suppose-I-have-to-discuss-this-old-chestnut thing. It is my impression that Gödel's incompleteness theorem is more often invoked in this context than are any undecidability results. The section Mechanism_(philosophy)#Gödelian_arguments gives a number of references, some of which probably discuss undecidability results, at least in passing. —Dominus (talk) 13:06, 16 July 2009 (UTC)

Using randomness to solve halting problem

We know for a fact that a deterministic machine cannot solve the halting problem in all cases, but can a probabilistic machine (such as a quantum computer) solve it? I found a paper that states that one can:

http://arxiv.org/pdf/quant-ph/0512248 (If this link goes dead, please update it or at least e-mail me a nasty letter. I hate dead links!)

Joeyadams (talk) 04:34, 30 July 2009 (UTC)

Well, I suppose there are various things you could mean by that, but in the most obvious interpretation, no, it's not possible. The cone of Turing degrees that compute the halting problem has Lebesgue measure zero. (Actually if I remember right, all nontrivial Turing cones are Lebesgue null.)

So suppose you had some program with a slot for a true-random-number generator, and for any input Turing machine, this program would tell you, correctly with probability 1, whether the TM halts or not. Then intersecting the sets of streams from the RNG that work for each particular TM, of which there are only countably many, you get that for almost all random streams, this program witnesses that the halting problem is Turing reducible to that stream. But this is a contradiction. --Trovatore (talk) 07:11, 30 July 2009 (UTC)

Yes, you remember right, for any noncomputable real X the set of reals that compute X is measure 0. This is due to Sacks in the 1960s. — Carl (CBM · talk) 13:14, 30 July 2009 (UTC)

Re Joeyadams: You have to be extremely careful with terminology. First, the thing that is ordinarily called quantum computing is not probabilistic: it is completely deterministic. However, apparently Kieu is not using the standard definition of quantum computing, he is using his own idea for a hypercomputation system and calling it quantum computing. Such misuse of terminology is unfortunately common among the hypercomputation community: they often make up new definitions for standard terms, making it easy to get the wrong impression from scanning their abstracts.

Second, the paper you cited explains that Kieu's system cannot work. Not only does it depend on a false theorem about physics, but even if this could be fixed, the method does not guarantee that the output answer is correct, and so does not actually decide anything. We do list it on our article on hypercomputation, though. — Carl (CBM · talk) 13:03, 30 July 2009 (UTC)

It is widely believed and current work indicates that quantum computers do not alter the notion of computability, and would not solve the halting problem. The deterministic/probabilistic distinction in the first post doesn't impact on the halting problem. There are people working on unphysical models of computation that could solve the problem, but being unphysical they're not very useful practically (the hypercomputation mentioned above). There are merely of theoretical interest. Verbal chat 14:13, 25 September 2009 (UTC)

Modern Proof

Since the original proofs of this involve useless terminology from recursive function theory, and since the proof is trivial, it is a shame to use the terminology. Previous discussions of this subject have been hampered by a lack of consensus about what constitutes original research in scientific articles. I hope the discussion of this can follow the WP:ESCA guidelines.Likebox (talk) 00:33, 15 October 2009 (UTC)

Why isn't recursive function theory "modern"? It's a shame to introduce unusual terminalogy, such as Quineing, to replace perfectly straightforward recursive function theory. — Arthur Rubin (talk) 00:48, 15 October 2009 (UTC)

You are not adressing the input issue. Nobody nowadays states the halting problem the way it is stated here. In particular, the input is a complete red-herring.Likebox (talk) 00:50, 15 October 2009 (UTC)

Input nonsense

The presentation of the halting problem is unfortunate, because it pretends that the input to the program is important in some way. The problem of determining which programs halt with 0 input is just as undecidable as the problem of determining which programs halt with arbitrary input. The only reason the input is mentioned at all is because historically, Turing proved the theorem by putting the program code on the input stream. That's not necessary at all, the program can include its own code internally.Likebox (talk) 00:39, 15 October 2009 (UTC)

That's true, in a sense. But your methodology seems to be to replace simple diagonalization by complex Quining, which doesn't strike me as productive. — Arthur Rubin (talk) 00:50, 15 October 2009 (UTC)

I see. But it's a question: quining can be proved by diagonalization, and diagonalization is equivalent to quining. It's a question of taste. I think that quining makes the proof more self evident, because it doesn't involve the input stream.

I saw someone get awfully confused about proving the following theorem: It is undecidable to show that P halts in polynomial time with arbitrary input. The reason is that the Turing method passes the code on the input stream. It's an awful presentation nowadays.Likebox (talk) 00:52, 15 October 2009 (UTC)

Diagonalization is simpler; even in this context where some coding is required. The term "Quining" is obscure, even with respect to what you call "modern" methodology. In fact, in your "modern proof" section, you note that "quining" is necessarily the correct term. Why not use a method which is correct?

Even if the absence of input is the "correct", "modern" formulation, "Machine R with input T" can be coded as

1. Write "T"
2. Execute "R"

This is clearly computationally equivalent, so that, if the proof is simpler in the input formulation, it can easily be translated. — Arthur Rubin (talk) 01:02, 15 October 2009 (UTC)

Indeed, if you formalize what you just said, you prove that quines can be written. It's a question of whether the self-reference is acheived by diagonalization, or by the quining result, which makes self-reference obvious. It's a matter of taste, and I think that both presentations can be placed side-by-side.Likebox (talk) 01:12, 15 October 2009 (UTC)

Only if modern formulations use the word "quine", and if you can formalize the concept (not the same as "quine") of a program R' which writes the code of "R" and then executes "R" on that input. That's not the same as a "quine", which seems to be a program R which writes its own code. — Arthur Rubin (talk) 01:34, 15 October 2009 (UTC)

We seem no longer to have an article on the concept formerly known as quining; indirect self-reference doesn't seem to actually use the word, other than as a natural language example. It's no longer in the text. The article quine (computing) doesn't really seem applicable, unless modified to include a code of the Turing machine program as source code. — Arthur Rubin (talk) 01:39, 15 October 2009 (UTC)

quine (computing) is Ok. The method of writing quines makes it obvious that a program can print its own code in a subroutine, and then go on to do something else. There is no issue with this particular idea. Modern formulations use the word "fixed point theorem" which is essentially a synonym for quine.Likebox (talk) 01:43, 15 October 2009 (UTC)

Reverting the changes to the intro

If you don't like quining, discuss that. The old intro is ridiculous, because the halting problem is never stated about programs with inputs nowadays. It is always stated about programs without inputs.Likebox (talk) 00:56, 15 October 2009 (UTC)

No, I don't like quining, and I dispute your statement that "the halting problem is never stated about programs with inputs nowadays". Furthermore, even if it were, diagonalization is simpler than quining, and better understood — at least, by everyone other than yourself with whom I've interacted. Please stop adding nonsense to the lede. — Arthur Rubin (talk) 01:02, 15 October 2009 (UTC)

If you think that, just get rid of the quining and we'll discuss it. But please don't revert the intro--- the intro is stating the halting problem, which is stated without inputs. You can keep the intro without inputs, and add a sentence saying "Turing's original formulation was for programs with inputs, so determining whether a program P with input I halts is undecidable". But the modern statement of the problem definitely does not involve inputs in any way, and it is slightly misleading to present it with inputs. The only purpose of doing it this way is to avoid quining.Likebox (talk) 01:07, 15 October 2009 (UTC)

Also, in my experience, everyone I have ever met understands quining better than diagonalization, although in this case both are sufficiently trivial and sufficiently obviously equivalent that they are indistinguishable.Likebox (talk) 01:13, 15 October 2009 (UTC)

It looks like a whole section is also being reverted by Arthur Rubin titled "Modern Proof of Undecidability". It's time for a third party to look into this issue. Varks Spira (talk) 01:15, 15 October 2009 (UTC)

I just added that section--- Arthur Rubin is not reverting any long-standing material. This dispute has happened before, and honesty compels me to admit that consensus swung against "modern proof". I was hoping that the issue can be looked at again, as a test-case for the proposed WP:ESCA guidelines. These allow streamlined modernized proofs in scientific or mathematical articles, in cases where the proofs are correct, and are only designed to illuminate intermediate steps in well-understood sourced arguments.Likebox (talk) 01:19, 15 October 2009 (UTC)

How do the reliable sources state it? We should follow the sources, rather than debate the best way to present it. Finell (Talk) 01:22, 15 October 2009 (UTC)

This is why I brought up WP:ESCA. There are sources, and there are sources. The result is so old by now, that sources discuss it in ten-thousand different ways. In such cases, using verbatim quotes from sources can be misleading at times.

Current textbooks do usually state the halting problem with the input. But they also later prove that the halting problem is equally undecidable without the input. Both theorems are so closely related, that they are both called "the halting problem", but since the no-input result is infinitesimally stronger (whatever that means in this case), the no-input theorem is what people use.

The usual path in mathematics textbooks is to prove the halting problem with input by diagonalization, then to pass to the no-input case by the Kleene fixed-point theorem. The Kleene fixed point theorem is equivalent to the existence of quines, so I just wrote it in this language. According to WP:ESCA, which I agree with, it is not a good idea to only debate in terms of the language in sources, because then you can end up with an illegible mess. Instead, you should consider clarity of explanation and correctness when talking about objective material that fills in intermediate steps in proofs.

But even with WP:ESCA, it's a judgement call. So take the time to think about it, and see how the new material feels.Likebox (talk) 01:29, 15 October 2009 (UTC)

See WT:MATH

See WT:MATH#Halting problem and Likebox. Your input is welcome there, but I doubt the quined proof would be. — Arthur Rubin (talk) 01:18, 15 October 2009 (UTC)

Previous Likebox discussions

Can be found at Talk:Halting problem/Archive3#Formal statement redux, Talk:Halting problem/Archive3#What Is A Rigorous Proof? (November 2007), and Talk:Halting problem/Archive3#Likebox edits (March 2008). I see no indication that anyone agreed with Likebox then, nor do I see any likelyhood that other editors will do so now. — Arthur Rubin (talk) 01:28, 15 October 2009 (UTC)

Things have changed since then, and we have different ideas about how scientific and mathematical articles should be written. To give a good test of the proposed guidelines in WP:ESCA, I am bringing this up again.Likebox (talk) 01:31, 15 October 2009 (UTC)

WP:CONSENSUS can change, but you have provided no evidence that it has, nor that WP:ESCA (even if a guideline, which it appears not to be; and, in fact, you are the only one in support in the poll) would provide a different result. — Arthur Rubin (talk) 01:54, 15 October 2009 (UTC)

I am testing the waters. I am not the only supporter of WP:ESCA, there are also the authors of the proposed guideline. It is important that we get this trivial stuff straight, so that mathematical and scientific articles can be written without the fear of deletion.Likebox (talk) 02:08, 15 October 2009 (UTC)

You have tested the waters before... Regardless what WP:ESCA says, we write all of our articles in a way that agrees with the presentations in the mainstream literature, rather than inventing our own organizational frameworks. — Carl (CBM · talk) 02:29, 15 October 2009 (UTC)

And I will test the waters again, until this is accepted. It is not reasonable that material which is clear and correct, old and well-established, can be removed just because some editors think it sounds to quirky.Likebox (talk) 20:02, 15 October 2009 (UTC)

• Unassessed mathematics articles
• High-priority mathematics articles