Re: Foundation for a Formal Refutation of the Original Halting Problem?

From: Owen Jacobson (angstrom_at_lionsanctuary.net)
Date: 08/04/04 

Date: Wed, 04 Aug 2004 05:00:47 GMT

Note: Peter uses "WillHalt", I use Halt. We mean the same function, but
the extra keystrokes of following Peter's naming conventions aren't worth
the effort to me.

Fun fact: in the course of writing this, I typed the word 'Halt' enough
times that it stopped looking like a word.

On Wed, 04 Aug 2004 02:15:00 +0000, Peter Olcott wrote:

> "Simon G Best" <s.g.best@btopenworld.com> wrote in message
> news:410F33D0.1040608@btopenworld.com...
>> Peter Olcott wrote:
>> [...]
>> >
>> > I have thought about this quite extensively over the past few days. I
>> > have come to the conclusion that it is correct to say that an
>> > identical method with identical input must produce identical results.
>>
>> Well done! :-D
>>
>> [...]
>>
>> > In this case we have identical methods. It is not even an identical
>> > copy of the same method. It is the very same method.
>>
>> Correct.
>>
>> > What we do not have is identical data.
>>
>> Incorrect. The data is identical in both cases. In Turing's proof, the
>> data is identical in both cases.
>
> I am running out of time for today.
> I will post a breif point here:
> it is something like this.
>
> WillHalt(LoopIfHalts, LoopIfHalts)
> WillHalt(WillHalt(LoopIfHalts, LoopIfHalts))

Just to refresh our collective memories, let's review the properties of
a function to determine if programs and their inputs halt.

Halt (M, x) is a program that accepts an encoding of a program, M, and an
encoding of M's input, x, and provides, as an output, a symbol that can be
interpreted as either saying that M(x) (M, evaluated with inputs x) halts
or that M(x) does not halt. These are the only two possible outputs;
furthermore, Halt(M, x) must be able to correctly analyze any program M
with any input x that M would accept.

We can cast this into C++ reasonably correctly:

bool Halt (string M, string x);

Returning true if M(x) halts, and false if M(x) does not halt.

The following properties must be true, for Halt (M, x) to satisfy this
defintion.

First, Halt (M, x) must itself always halt. Therefore, Halt (Halt, x)
outputs the symbol meaning "Halt (x) will halt" for any x (where x is a
valid encoding Halt's inputs -- I.E., a program and that program's
input). A program Halt(M, x) that can fail to halt can fail
to produce output. This is clearly not acceptable.

Second, Halt (M, x) must always output a symbol meaning "M(x) does halt"
or "M(x) doesn't halt". The specific symbols aren't overly relevant; in
the C++ example it is natural to use 'true' and 'false'. No other outputs
are possible.

Third, Halt (M, x), being a Turing machine, must therefore be
deterministic. For any given input (M, x), Halt (M, x) must always
produce the same output.

Finally, Halt (M, x) must do these things for *every* *possible* input (M,
x). A program Halt (M, x) that can compute whether M(x) halts in all case
but one is not acceptable.

Are we agreed on the fundamental definition of the Halt program?

So, let's return to Peter's post:

> WillHalt(WillHalt(LoopIfHalts, LoopIfHalts))

The second example is clearly incorrect as it provides no correct inputs
to Halt, but I strongly suspect he means Halt (Halt, (LoopIfHalts,
LoopIfHalts)) (where (LIH, LIH) is an encoding of the parameters to Halt).

>From the above rules for the behaviour of Halt (M, x) we know that this
will always output the symbol meaning "Halt (LoopIfHalts, LoopIfHalts)
will halt," because Halt itself must halt. However, this case is never
evaluated in Peter's own example program:

Peter Olcott, Message-ID:
<UiAPc.166937$OB3.76613@bgtnsc05-news.ops.worldnet.att.net>
> 08) void LoopIfHalts(string SourceCode, string DataInput)
> 09) {
> 10) if (WillHalt(SourceCode, DataInput))
> 11) while(true)
> 12) ;
> 13) else
> 14) return;
> 15) }

> 16) cout << WillHalt(LoopIfHalts, LoopIfHalts);

Let's evaulate Halt (LoopIfHalts, LoopIfHalts) ourselves. It must
determine if the call LoopIfHalts (LoopIfHalts) halts. This is clearly
impossible, as Peter's LoopIfHalts function accepts two strings
(representing, I assume from context, encodings of programs) as input, not
a single string. So, once again, we'll take the liberty of "correcting"
Peter's function to something consistent, both with the apparent intent
above and with existing Halting proofs:

void LoopIfHalts (string Program) {
  if (Halt (Program, Program))
    while (true) ;

  else
    return;
}

Now, back to the question of what Halt (LoopIfHalts, LoopIfHalts) outputs.
It's evaluating the invocation LoopIfHalts (LoopIfHalts). Therefore, we
can expand the variable Program in the above source to LoopIfHalts (for
this invocation):

void LoopIfHalts (string Program = LoopIfHalts) {
  if (Halt (LoopIfHalts, LoopIfHalts)) // Not a literal invocation, merely
                                       // an input
    while (true) ;

  else
    return;
}

That contains our original program: Halt (LoopIfHalts, LoopIfHalts).
THIS IS A CRITICAL POINT: by simple variable expansion we can show that
both the original invocation and the invocation contained in LoopIfHalts
are identical.

Obviously, if we keep following this method and expanding LoopIfHalts,
we'll end up recursing a very long ways. Fortunately, we don't have to
assume Halt (M, x) recursively evaluates LoopIfHalts (LoopIfHalts) at all,
because we know that Halt (M, x) == Halt (M, x) from the third property of
Halt (M, x) above, and, seeing as there are only two possible outputs for
Halt (M, x), we can search them exhaustively by hand.

Let's assume Halt (LoopIfHalts, LoopIfHalts) outputs our symbol meaning
"true, this invocation does halt." Therefore, we can replace the function
call above with 'true':

void LoopIfHalts (string Program = LoopIfHalts) {
  if (true) // Not a literal 'true', merely an output
    while (true) ;

  else
    return;
}

But wait, now we have a function that, obviously, does not halt. So Halt
(LoopIfHalts, LoopIfHalts) can't determine that LoopIfHalts (LoopIfHalts)
*will* halt. So, what about the only other option,
"LoopIfHalts(LoopIfHalts) will not halt"? We can do the same expansion:

void LoopIfHalts (string Program = LoopIfHalts) {
  if (false) // Not a literal 'false', merely an output
    while (true) ;

  else
    return;
}

Ah, but now LoopIfHalts halts, which still contradicts the output of Halt
(LoopIfHalts, LoopIfHalts). So, Halt (LoopIfHalts, LoopIfHalts) cannot
determine that LoopIfHalts (LoopIfHalts) *does not* halt, either. We've
exhausted all possible outputs for Halt (LoopIfHalt, LoopIfHalt), too.

The only remaining way for Halt (LoopIfHalts, LoopIfHalts) to satisfy any
of the requirements is to break one -- either that it must always output
one of two values, that it must halt, or that it must always produce the
same output from the same inputs. Since, in order to satisfy the
definition of a program that can determine if arbitrary programs and their
inputs halt, none of these requirements may be ignores, we can conclude
that no program can exist to satisfy all of these requirements.

Note that LoopIfHalts is clearly a perverse case designed specifically to
thwart Halt (M, x). This does not excuse Halt (M, x); one of the
requirements (the last one, in my list) is that Halt (M, x) must be able
to analyze any program and its input.

This is Turing's proof, with examples expressed in C++ for ease of
reading. I invite all and sundry to highly errors, by quoting them and
then describing, as precisely as possible, the error. Saying "this does
not follow" is not a precise description of the error; "this does not
follow because X" might be, if X can be clearly shown. Show your X. Show
how you arrived there. 

-- 
Some say the Wired doesn't have political borders like the real world,
but there are far too many nonsense-spouting anarchists or idiots who
think that pranks are a revolution.

Relevant Pages
Loading