Re: What is the Result from Invoking this Halt Function?

From: Mitch Harris (harrisq_at_tcs.inf.tu-dresden.de)
Date: 08/10/04 

Date: Tue, 10 Aug 2004 10:20:57 +0200

Peter Olcott wrote:
>
> It looks like Turing's proof may be erroneously applied to the
> Halting Problem. It looks like Turing might have assumed that
> the Halt function must always return a result to all callers.

I think you misunderstood how a proof by contradiction
works. The main outline of Turing's proof goes like this:

1. -assume- a correct halt analyzer Halt(M, w) (M is a TM
and w is a word on its tape). You don't actually have the
specs for such a TM, you just have a name for a hypothetical
TM with the property that it can correctly determine
whether M halts on w or not (i.e. it has outputs yes or no,
and that's it. this is just an assumption).

2. using Halt(M,w) construct (using accepted notions of
constructing a TM) a TM Diag(M) (details elsewhere).

3. Diag(Diag), can logically be shown to both halt and not
halt, a contradiction.

4. Therefore some hypothesis was wrong. Since everything in
the construction is sort of "off limits" (they are
true/accepted before the proof is begun) then the hypothesis
that must be wrong is the existence of a correct Halt(M,w).

> I
> don't think that the diagonalization process has the facility to
> operate otherwise.

"has the facility"? It was constructed to do what it does on
purpose. You can construct all sorts of other things but
that doesn't mean that the diagonalization process cannot be
  constructed. If it can be done, that's enough.

Now if you prevent it from being done, there still could be
another proof.

> It does not allow a choice to be made
> whether or not to derive a result. Its more like a multiplication
> table. So tentatively it looks just like what I have been saying
> all along.
>
> Quick Summary:
> Alan Turing conclusively proved is that it is impossible to construct a halt
> analyzer that always returns a correct result back to the program being
> analyzed.

I agree with everything before the "that".

> Since returning the result back to the program being analyzed is not the
> only way to construct a halt analyzer,

I, at the moment, cannot think of another way to do it. So
maybe it -is- the only way (modulo meaningless variations,
for sufficiently small concept of meaningless).
It doesn't matter how the construction worked (as long as it
is acceptable). If you can make one contradiction (out of a
multitude of individual truths), then that's enough.

If you don't think it is acceptable, then you're talking
about something other than what is normally referred to as a TM.

> his proof did not show that
> constructing a halt analyzer that works correctly for all input is impossible.

Sure it did. It must be that you just disagree with how TM's
are defined. That's a different matter.

mea culpa for the deja vu all over again. just for the
record, the latecomers, and perpetual skeptics. 

-- 
Mitch Harris
(remove q to reply)

Relevant Pages

  • Re: proof of undecidability of halting problem
    ... however, the contradiction is introduced by using a second function, ... a function like halt can't? ... Turing proved it could be done. ... How can a high level language prove theorems ...
    (sci.logic)
  • Re: Proving a negative is hard
    ... > LoopIfHalts uses a generic halt analyzer, ... > contradiction. ...
    (sci.logic)
  • Re: What is the Result from Invoking this Halt Function?
    ... > the Halt function must always return a result to all callers. ... I think you misunderstood how a proof by contradiction ... -assume- a correct halt analyzer Halt ... > Alan Turing conclusively proved is that it is impossible to construct a halt ...
    (sci.logic)
  • Re: What is the Result from Invoking this Halt Function?
    ... And, obviously, it's NOT an analytical impossibility, ... LoofIfHalts would always halt in each and every instance. ... it is natural to call this TM a halt analyzer. ... > TM itself but A STRING, THE SOURCE CODE FOR, or some other string DESCRIPTION ...
    (comp.theory)
  • Re: What is the Result from Invoking this Halt Function?
    ... And, obviously, it's NOT an analytical impossibility, ... LoofIfHalts would always halt in each and every instance. ... it is natural to call this TM a halt analyzer. ... > TM itself but A STRING, THE SOURCE CODE FOR, or some other string DESCRIPTION ...
    (sci.logic)