Re: Every sufficiently competent C programmer knows

On 11/03/2025 21:10, Richard Heathfield wrote:

On 11/03/2025 20:37, Mike Terry wrote:

On 11/03/2025 18:23, Richard Heathfield wrote:

On 11/03/2025 17:42, Mike Terry wrote:

Finally, if you really want to see the actual HHH code, its in the halt7.c file (along with DDD) that PO provides links to from time to time.  However it's not very illuminating due to bugs/design errors/misunderstandings which only serve to obfuscate PO's errors in thinking.

>
[I've now seen the code. Oh deary deary me.]

>
:)
>

>
Thank you for a spirited attempt to be cogent - or at least as cogent as it is possible to be in the circumstances!
>
I think PO's first step must be to demonstrate that HHH() correctly diagnoses some easy functions, such as these:

>
Not really necessary - PO is not trying or claiming to have a (full) halt decider.

 In which case he has nothing. And I'll stipulate that, so he can't even argue back.
 

>
Originally his claim was that he had a program which worked for the counter-example TM used in the common (e.g. Linz book) proof.  Such a program is impossible, as Linz and others prove, so having a program H and its corresponding "counter-example" D, such that H correctly decides D, would certainly show that the Linz proof is wrong.  His claim was always that he had "refuted the HP proof", or sometimes that he had refuted the HP theorem itself although he's been told dozens of times that there are many alternative proofs for the result.

 He's beginning to remind me of a few other Usenet characters.
 

>
[As it turned out, PO's D(D) halted when run under his x86utm environment, while H(D,D) which is required to return the halting status of computation D(D) returned 0 (=non-halting).  That is exactly what the Linz proofs claim!]
>
Anyhow, his decider only /has/ to correctly decide the one input, which is the D constructed from H by the usual method (basically D calls H to see what H claims is the halting behaviour, then does the opposite - I'm not sure if you're familiar with the proof, but imagine you would be given your background).

 It's in GEB, so I first read it roughly a thousand years ago.
 I would take issue with one thing though - if his decider doesn't handle arbitrary programs as input and correctly diagnose them, he is addressing an entirely different problem.
 

>
His decider H works (subject to design errors/bugs and so on) by single-stepping a simulation of its input computation, and monitoring for conditions that PO believes indicate non-termination.  He tests a couple of conditions, and when one of those matches H aborts and returns non-halting. Alternatively if the simulation halts normally, H returns halting.  The problem is (at least) one of his non-halting-behaviour tests is invalid, matching during the simulation of DDD, which is a halting computation.
>
It is true that sometimes his tests match and the input is indeed non-halting.  PO quotes this as evidence that his tests "work", so when the decided non-halting for a halting computation they must be correct and the halting computation in fact is non-halting because it "exhibited non-halting behaviour"!

 Did he pay out a ball of twine behind him?
 

int rha(unsigned int i)
{
   while(--i > 0)while(--i > 0);
   return 0;
}
>
int rhb(unsigned int i)
{
   if(i > 0)
   {
     rhb(i/10);
   }
   return putchar(i + '0');
}
>
int rhc(unsigned int i)
{
   typedef int(*pf)(unsigned int);
   pf arr[3] = {rha, rhb, rhc};
   return arr[i % 3];
}
>
and other such obvious tests.
>
HHH(), the procedure that decides whether a program halts, is required to work for all programs and all inputs. Does it work on those cited above? I'm guessing it doesn't.
>

>
I would have to think a bit about your examples - or more likely just try them out (which I'm not motivated to do).

 I knew you were smart. :-)
 

PO's non-halting tests involve observing loops and conditional branches in some combination.  The major problem for his HHH/DDD is with the simulation aspect - the tests can match when the same code address is reached but across completely different simulation levels.  PO does not appreciate that tests which /might/ work in a non-simulation setting, could go horribly wrong when simulation is involved...  (so your tests aren't especially relevant for PO's code logic - and as I said there is only the one case that he really has to handle.)

 I must disagree. HP is about detecting whether an ***arbitrary*** program (and to show willing I'll buy 'function' for 'program') will terminate. Special cases need not apply.
 If his decision procedure cannot handle arbitrary functions, he isn't addressing HP.

Sure - if PO wants to prove that HP theorem is false, a clear way for him to do that would be to produce a halt decider, and like you say, such a HD must decide /every/ input correctly.
Then again, if his claim is only that Linz HP proof is invalid, he could just attack the /proof/ presented in Linz.
Linz proof high level summary:
[I use <P> notation to denote "TM tape encoding of P", where P is a TM or TM input.]
1)  Suppose H is a halt decider, taking inputs (<P>,<I>) where
     <P>:  a TM description, suitably encoded
     <I>:  a TM tape, suitably encoded
2)  ..then from H we can construct a new TM H^ by modifying H in the following manner:
     a)  H^ is basically a wrapped version of H, with additional pre/post processing
         steps
     b)  pre-processing:  H^ duplicates the input on its tape, [its single input
                          parameter becoming the two input parameters for wrapped H]
     c)  post-processing: if wrapped_H decided HALTS, enter infinite loop
                          else if it decided DOESNT_HALT, halt straight away
3)  With H^ so constructed, it is easily shown that
     if H^(<H^>) halts, then H(<H^>,<H^>) decides DOESNT_HALT,  and
     if H^(<H^>) doesn't halt, then H(<H^>,<H^>) decides HALTS.
4)  Either way, H fails to decide the specific input (<H^>,<H^>) correctly,
     contrary to assumption (1).  Hence no halt decider exists.
While the proof assumes H is a (full) halt decider (deciding ALL inputs correctly), the logic of the proof can be applied to any H meeting the much weaker requirement that H simply decides (correctly or incorrectly) the one particular input (<H^>,<H^>).  Applied with this weaker requirent, the proof shows such an H must decide that specific input /incorrectly/.  [The proof never talks about the behaviour of H for any input other than (<H^>,<H^>), so still applies even if H gets other inputs wrong or even fails to halt for other inputs...]
PO claimed he had an actual example of such an H which decides input (H^,H^) /correctly/.  If this were true, the proof logic (1)-(4) would clearly be incorrect somewhere, and PO would have "refuted the Linz proof of HP".  *It would not matter that his H is not a full halt decider* - the proof would still be refuted.
Of course, it turned out that his H /incorrectly/ decided the critical input exactly as Linz claims, so that should have been the end of things!  But PO just doubles down, claiming that his H was correct to decide DOESNT_HALT even though his H^(H^) demonstrably halts.  All his subsequent posts are efforts to explain why Wrong is Right for whatever reason.
So... your remark was fair if PO claims HP theorem is false, not so much if he merely claims to have refuted one specific proof of the theorem.

 Those functions I rattled off weren't intended to be particularly hard exercises - just opportunities for a proof of concept. I don't expect him to avail himself of that opportunity because I don't believe him to be arguing in good faith.
 

He won't be interested in your cases.  In the end he is just interested in the one input case which he feels "refutes the Linz proof".
Regards,
Mike.