Sujet : Re: Analysis of Flibble’s Latest: Detecting vs. Simulating Infinite Recursion ZFC
De : news.dead.person.stones (at) *nospam* darjeeling.plus.com (Mike Terry)
Groupes : comp.theoryDate : 24. May 2025, 17:35:18
Autres entêtes
Organisation : A noiseless patient Spider
Message-ID : <100ssg5$qc3d$1@dont-email.me>
References : 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
User-Agent : Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Firefox/91.0 SeaMonkey/2.53.18.2
On 24/05/2025 01:36, Keith Thompson wrote:
Ben Bacarisse <ben@bsb.me.uk> writes:
Keith Thompson <Keith.S.Thompson+u@gmail.com> writes:
Ben Bacarisse <ben@bsb.me.uk> writes:
[...]
And the big picture is that this can be done because false is the
correct halting decision for some halting computations. He has said
this explicitly (as I have posted before) but he has also explained it
in words:
>
| When-so-ever a halt decider correctly determines that its input would
| never halt unless forced to halt by this halt decider this halt
| decider has made a correct not-halting determination.
>
Hmm. I don't read that the way you do. Did I miss something?
>
It assumes that the input is a non-halting computation ("its input
would never halt") and asserts that, in certain circumstances,
his mythical halt decider correctly determines that the input
is non-halting.
>
When his mythical halt decider correctly determines that its input
doesn't halt, it has made a correct non-halting determination.
It's just a tautology.
>
It would be a tautology but for the "unless..." part. It does not make
the determination that it does not halt. It determines that it would
not halt were it not for the fact that the decider (a simulation) in
fact halts it.
Right, so the computation itself is non-halting.
No no no, it halts! (Assuming we're discussing the computation DD() with PO's code.)
Ben's wording is as bad as PO's. In fact Ben just copies PO's wording without explaining or clarifying anything.
I feel that the quickest way for you to get everything straight in your head would be to actually trace through yourself (line by line) what computations HHH(DD) and DD() do at a high level (pseudocode, not x86 instructions). That way you'll see for yourself that DD() halts, and HHH(DD) decides non-halting. [I'd guess it might take you 20 minutes, but how long have you already spent posting??] If you're not clear on what you would trace for HHH, ask and I'll concoct some high-level pseudocode for you.
Your interpretation of the statement as a tautology is how everybody but PO reads the statement. Here is what you say:
-----
> If his mythical halt decider correctly determines that its input
> doesn't halt, it has made a correct non-halting determination.
> It's just a tautology.
-----
[Bear in mind that with PO's HHH(DD), it /incorrectly/ determines that its input doesn't halt. But sure, the statement as you're reading it is a tautology. That tautology just doesn't apply to PO's HHH(DD).]
So how does PO's reading differ? The problem is with your phrase "its input doesn't halt". That's fine wording, directly invoking the /definition/ of "halt", which most people understand, but PO CAN'T DO ABSTRACT. In his head he has replaced the definition with something he /can/ cope with - some "concrete" procedure he can imagine performing, involving simulations and amended code. So what exactly is this concrete procedure PO imagines?
PO imagines /changing the code of HHH/ so that it doesn't abort. Then if "DD" would never halt that means HHH is right to decide non-halting. AND FINALLY THE PROBLEM: DD calls HHH, so when PO imagines changing the code of HHH, he is also imagining changing the behaviour of HHH's input (DD) so the new DD calls the new HHH which doesn't abort! In case it needs spelling out, that's wrong, because HHH was asked to decide halting for the specific (fixed) input DD, and the behaviour of that input is to call the specific (fixed) HHH. We may consider how /that input/ might be decided by a modified decider, but if we switch to examining a /new/ input with different behaviour that has no bearing on DD's halting status.
With less words (probably clearer):
- HHH(DD) is asking HHH to decide halting of DD()
HHH and DD are actual programs with fixed code. (and DD halts)
- PO imagines changing HHH to HHH2 which doesn't abort.
This also changes DD behaviour so it calls the new HHH2 instead of HHH.
We'll call this new DD DD2.
- He considers HHH2(DD2) and concludes that HHH2 will never end its simulation of DD2.
[Indeed, computation DD2() does not halt.]
- So based on your/Sipsers wording [but with his own interpretation as above]
he concludes "It is correct for HHH to decide DD never halts".
[In fact DD does halt. It is obviously DD2 that never halts.]
The mythical
"halt decider" is a simulator that, I suppose, can either faithfully
execute the computation (which will take forever if it's non-halting)
*or* partially execute it and stop executing it at some arbitrary
point. (The latter is of course not a correct full emulation of
the computation.) The "forced to halt" step is not part of the
computation.
Perfect.
`int main(void) { while (1); }` is non-halting, at least in the C
abstract machine. The fact that I can kill it by typing Control-C or
pulling the power plug doesn't change that. If I don't immediately
notice the obvious, I can simulate its execution, letting it iterate
a few times, until I realize that it's never going to halt. At that
point I can interrupt my simulation and correctly report that the
program does not halt (something I can do for this program, but not for
all programs).
Perfect.
If you don't assume that this "halt decider" is the impossible
thing that olcott claims it is, but rather is a program that can
simulate another program's execution and report one of "halts",
"does not halt", or "I don't know", it seems to me that olcott's
statement is true and unremarkable (though a little convoluted).
It does not of course refute the validity of the existing proofs
that the Halting Problem is unsolvable.
With your interpretation the statement is indeed true but unremarkable. That is effectively what Sipser agreed to (IMO). We can imagine a correct partial simulating halt decider applying your interpretation to report a tight loop as non-halting.
BUT PO's interpretation of the statement which I've tried to explain above [all the stuff about changing both HHH /and/ its input DD] is what he is using now to justify his claim that his specific HHH correctly decides its corresponding "HP counterexample" input DD. If this latter claim were true, that /would/ refute the validity of the Linz HP proof.
So sure, you can say the statement is a tautology, but PO made that statement and his interpretation of what it means is far from your tautology.
HTH (if only in sending you off on a good night's sleep!)
Mike.