1
$\begingroup$

I've read the definition for Rice's Theorem, here's the one from Wikipedia:

In computability theory, Rice's theorem states that all non-trivial, semantic properties of programs are undecidable.

The classical proof for proving Rice's Theorem is on Wikipedia, which is similar to other sources.

However, I have a problem with this proof, made clear (hopefully) in the paragraphs following.

This proof goes like this:

if we had an oracle for deciding these properties of program behavior, we would be able to use it to solve the Halting Problem, but the Halting Problem is undecidable, so an oracle for deciding these properties cannot exist either.

However, as far as I know, the impossibility of the Halting Program only occurs if the program checking whether something halts or not is trying to prove the hypothetical does_it_halt(a, i) wrong by using self-referencing tricks. But, in this proof, the oracle that is trying to decide the property is not trying to do that. So, it should be able to do its job without solving the Halting Problem.

I had some hope at the beginning that this proof may be wrong, but since it is apparently the "classical" proof for proving Rice's Theorem, I must be missing something. What is it that I am missing ?

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ Do you know what is the meaning of DECIDEing a problem using Turing machine? $\endgroup$ – Doralisa Jun 14 '18 at 14:08
  • 1
    $\begingroup$ @DsD I think I know. Care to elaborate ? $\endgroup$ – doubleOrt Jun 14 '18 at 14:09
  • 1
    $\begingroup$ If you look precisely on its definition you'll find it there is no Turing machine for halting problem accept yes inputs and reject no inputs. Which means there can't be something (that computes) deciding Halting problem. $\endgroup$ – Doralisa Jun 14 '18 at 14:18
  • 1
    $\begingroup$ @DsD Could you elaborate further ? I don't see your point yet. If you are talking about that does_it_halt(a, i) function, it's a hypothetical function, not actual. $\endgroup$ – doubleOrt Jun 14 '18 at 14:22
  • 2
    $\begingroup$ It seems someone wrote an answer sooner than me which you've accepted. I just suggest you read relation of halting problem and incompleteness of Godel for further reading and finding out why you can't decide halting problem. $\endgroup$ – Doralisa Jun 15 '18 at 14:04
1
$\begingroup$

However, as far as I know, the impossibility of the Halting [Problem] only occurs if the program checking whether something halts or not is trying to prove the hypothetical does_it_halt(a, i) wrong by using self-referencing tricks. But, in this proof, the oracle that is trying to decide the property is not trying to do that. So, it should be able to do its job without solving the Halting Problem.

The proof shows that, if we had a machine $M$ to decide a nontrivial semantic property, we can craft another machine $N$ to solve the Halting problem.

With "$N$ solves the Halting problem" we mean that $N$ can decide the termination of absolutely any other Turing machine, including those using "self-referencing tricks" -- no exceptions.

In a nutshell, "for all" means "for all". If we show that a machine decides a problem, then it must always do its job on all inputs. The mentioned proof crafts a machine $N$ which does not "decide the Halting problem, except for self-referencing cases" (whatever that might actually mean in formal terms). $N$ is proved to work "for all" inputs.

By the way, it's a common misconception to think that we actually detect when a program is "self-referencing", and that we could work around the impossibility of deciding the halting problem by weakening the goal to "decide whether $T$ halts on input $x$, as long as there is no self-referencing". What actually happens is that there are infinitely many machines $U$ equivalent to $T$ we could use for the "self-referencing", and (by Rice!) deciding whether $T$ and an arbitrary $U$ are equivalent or not is impossible. No algorithmic "syntactic inspection" on two programs can hope to decide whether they are equivalent on all cases.

Indeed, at first the self-referencing trick looks as a quite unsatisfactory negative proof, making one think that it could be worked around easily by just excluding that case. However, it is far more general than it looks at first.

|cite|improve this answer
$\endgroup$
  • 1
    $\begingroup$ Thanks for answering! But in this line The mentioned proof crafts a machine N which does not "decide the Halting problem, except for self-referencing cases" Did you mean which does ? $\endgroup$ – doubleOrt Jun 15 '18 at 11:57
  • 1
    $\begingroup$ What actually happens is that there are infinitely many machines U equivalent to T we could use for the "self-referencing" Could you elaborate or/and provide an example ? $\endgroup$ – doubleOrt Jun 15 '18 at 12:05
  • 1
    $\begingroup$ @doubleOrt No, i mean "which does not (only) ..." $\endgroup$ – chi Jun 15 '18 at 12:05
  • 1
    $\begingroup$ However, it is far more general than it looks at first. As in, more general cases of self-referencing, or other ways other than self-referencing, which make the Halting Problem impossible to decide ? I would be thankful if you could elaborate :) $\endgroup$ – doubleOrt Jun 15 '18 at 12:08
  • 1
    $\begingroup$ @doubleOrt Given program $T$, you can generate a program $U$ which on input $n$ (natural) first checks if there is a counterexample to some complex theorem, say, Fermat Last Theorem with numbers $<n$. If there is one, the program behaves differently from $U(n)$, otherwise it behaves exactly as $U(n)$. Proving that $U$ is equivalent to $T$ requires proving that no counterexamples exist to the Fermat Last Theorem, i.e. proving the theorem itself. You can generate other examples replacing FLT with your theorem of choice. $\endgroup$ – chi Jun 15 '18 at 12:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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