Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I think the halting problem is not a result regarding computability, but rather expressiveness or restrictiveness. It's like asking a computer to prove $0=1$ or color a planar graph using only $3$ colors. To accommodate this lack of expressiveness, I propose to change the yes-no output options to these two:

  • This program halts and it does not have a crossing structure.
  • This program does not halt or it has a crossing structure.

The key here is that I merged the case "does not halt" and the case "has a crossing structure". And this will stop Rice's theorem from being able to be applied here.

Now, what is a crossing structure? It simply means that the input machine simulates the decider and does the opposite of its verdict.

So much for the definitions. My question is:

Is the halting problem solvable with these two output meanings?

My suspicion is that it's still not solvable, but yet it's consistent with all my test cases.


This is actually a paradox. The question is:

Is there a program with a crossing structure?

First suppose there is. Then this program will simulate me. Suppose I say you don't halt or you have a crossing structure. Then you must, in order to contradict me, halt and at the same time don't possess a crossing structure. Contradiction.

Next suppose there isn't any. Then "halt and don't possess a crossing structure" is equivalent to "halt" and "don't halt or possess a crossing structure" is equivalent to "don't halt". Then it's easy to contradict me, that is, there is a program possessing the crossing structure. Again, contradiction.

share|improve this question
1  
How does Rice's theorem not apply? Are you sure? –  user16697 Nov 6 '11 at 20:15
    
OK, this is the beautiful part of the definition. Rice's idea is to use my separation to solve the halting problem. But this does not work for my definitions. Imagine appending a program $p$ before a program that halts and does not have a crossing structure. I can separate the combined program without giving any indication whether $p$ halts, provided $p$ is the opponent of the halting decider, i.e. $p$ has the crossing structure. So if you turn my program into a halting decider, the opponent will not make a dilemma for the decider. Because it will just be put into the second category. –  Zirui Wang Nov 7 '11 at 7:05
    
As I was saying, it's really an expressiveness problem, not a computability problem. –  Zirui Wang Nov 7 '11 at 7:19
add comment

2 Answers

up vote 3 down vote accepted

It simply means that the input machine simulates the decider and does the opposite of its verdict.

It is not that simple. "Simulating" is extremely vague.

Even if you fix it, there is another issue, with "does the opposite of its verdict".

Suppose you have a decider D for your problem. I give you a program P(X):

  1. Run decider D on X(X)
  2. If D says "not halts or has a crossing sequence", then halt
  3. If D says "halts and does not have crossing sequence", then do some complicated loop

If step 3 contains a finite loop, the program surely halts.

If step 3 contains an infinite loop, then P simulates the decider and does the opposite of its verdict - so it has a crossing a sequence.

Let's ask the decider about P(P).

If the decider says that $P(P)$ halts, then the execution of $P(P)$ must go to step 3, and halt. In other words, the complicated loop is finite.

If the decider says that $P(P)$ does not halt or has a crossing sequence, then there are two cases:

  • $P(P)$ does not halt. This is not possible, since because of D's answer in step 1 the program goes to step 2 and halts.

  • $P(P)$ has a crossing sequence. This means that the program does the opposite of the verdict, so the loop in step 3 is infinite.

So if $D$ existed, you could use it to solve normal halting problem. Therefore the original problem is undecidable.


There is a lot of "partial halting problem deciders" - programs which always say "yes", "no", "don't know" correctly. For example, a program which always says "don't know", or a program which runs P for 100 seconds and says "yes" when halted, and "don't know" otherwise.

I disagree with your philosophy. Halting problem is about uncomputability. It means that we cannot perform general unbounded search over natural numbers. For example, there is no universal tool to prove Goldbach's conjecture, Fermat last theorem, odd perfect number conjecture etc. You have to use number theory to solve such problems. There is no apparent "crossing structure" in a program which searches for odd perfect number conjecture.

Do you remember Cantor's proof of uncountability of reals? There are MUCH more reals than naturals. Any attempt to find a surjection $\mathbb N \to \mathbb R$ will fail miserably - you will miss a LOT of numbers, much more than a single one found by diagonal reasoning. Any attempt to find an algorithm solving halting problem will also fail miserably - any "decider" will be wrong on lot of programs.

share|improve this answer
    
All I'm saying is that I changed the output meaning. It's not longer "halt" or "don't halt". It's "halt and do not have a crossing structure" and "don't halt or have the crossing structure". I'm not deciding whether the machine halts; this is clearly impossible. I'm asking whether I can separate the programs into the two categories defined by my new meanings. Yes, it can be complicated but that's not the same as saying it's impossible. –  Zirui Wang Nov 7 '11 at 6:46
    
@Zirui Wang: I have shown that distinguishing "halt and do not have a crossing structure" and "don't halt or have the crossing structure" is not decidable. –  sdcvvc Nov 7 '11 at 6:49
    
The unsolvability, or better non-recursiveness, of the halting problem relies on the crossing structure. So it doesn't mean that you can't figure out whether a loop if finite or infinite. I'm suggesting that without the crossing structure, it is possible to discern which programs halt. But I'm not saying that it's possible to figure out whether a program has the crossing structure. I'm merely saying that we can figure out whether it does not halt or it has the crossing structure. Note the difference. –  Zirui Wang Nov 7 '11 at 6:52
    
But my $D$ will never say "halt" or "do not halt". Can you point out where you showed my new meanings are not decidable please? –  Zirui Wang Nov 7 '11 at 6:55
    
Your $D$ will either say "halt and do not have crossing structure" (in this case loop in step 3 is finite), or "does not halt or has crossing structure" (in this case loop in step 3 is infinite). So if you had a machine $D$ you could use it to solve normal halting problem. –  sdcvvc Nov 7 '11 at 6:58
show 4 more comments

It will not be possible to define "has a crossing structure" broadly or precisely enough to make the halting problem be computably solvable.

For example, it is known that the following function is not computable: given a first-order sentence $\phi$, return $1$ if $\phi$ is provable and $0$ if $\phi$ is not provable, where "provable" means in one of the standard effective proof systems for first-order logic. This function can be shown to be noncomputable without already knowing that the halting problem is noncomputable, using the incompleteness theorems. (If this function was computable, we could use it to make a computable, complete extension of Robinson arithmetic, which cannot exist.)

Now for each $\phi$ we can make a program $e_\phi$ that simply searches for a proof of $\phi$, and halts if and only if $\phi$ does have a proof. None of these programs directly simulates another program - these programs just search for proofs, and in fact except for the particular formula being tested all of these programs have the same code. But it is not possible to computably solve even the special case of the halting problem for programs of this form.

We could try to define broader and broader notions of "crossing pattern", but these become vaguer and vaguer as they become more general. In particular, it is difficult to see how to make a precise definition of "crossing pattern" that would cover the example of the programs I gave above.

share|improve this answer
    
I thought the first incompleteness theorem says that there is a $\varphi$ such that neither $\varphi$ nor $\lnot\varphi$ is provable. I don't see how to prove that the problem you defined is uncomputable. I mean, certainly either $\varphi$ is provable or it's not provable. Why can't this be decided by a program? Even when there are true but unprovable formulas, it's not a problem. The decidability of this problem does not mean the theory used is complete, does it? I need some clarification of the undecidability of this problem. Thanks in advance. :) –  Zirui Wang Nov 7 '11 at 6:33
    
I'm mainly thinking of using Hoare logic to prove the existence of a crossing structure. And I just need partial correctness and hence avoid the undecidability/unprovability. –  Zirui Wang Nov 7 '11 at 8:55
1  
If you take the correctness of the second paragraph as a lemma, the key point is the third paragraph. These programs do not have an obvious "crossing structure" but their halting problem is still undecidable. –  Carl Mummert Nov 7 '11 at 12:17
1  
As for the proof, see theorem 5 in: [phil.cam.ac.uk/teaching_staff/Smith/blogstuff/GWT02.pdf]. Although that proof in theorem 4 uses diagonalization, there is a different proof of theorem 4 that doesn't. Namely, if the set of theorems of Robinson arithmetic $Q$ was decidable, we could use this to make a stronger, complete, consistent theory extending $Q$. That theory cannot exist by the incompleteness theorem. The proof takes all the formulas, enumerates them in some order, and selects each one if and only if it is not disprovable from the ones that have previously been selected. –  Carl Mummert Nov 7 '11 at 12:22
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.