Re: Every sufficiently competent C programmer knows

On 12/03/2025 09:24, Fred. Zwarts wrote:

Op 11.mrt.2025 om 21:37 schreef Mike Terry:

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.
>
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.
>
[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).
>
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 seems that he does not understand that the these conditions (that indicate non-termination behaviour), form exactly the halting problem.
PO claims that simulation is the solution, but he only shifts the problem of non-termination detection to the detection of these 'special conditions'.
When we realise that, we understand that a finite or infinite simulation is not very relevant. The discussion should address these conditions. But PO carefully avoids discussions about the detection of these conditions, although they are the heart of the problem.

I completely agree.
We could create a (partial) simulating halt decider (PSHD) that works by simulating the steps of its input computation, and looking for patterns in the resulting trace indicating halting or non-halting behaviour.  If these patterns were /*sound*/, meaning that matching guarantees the computation behaviour is indeed halting/non-halting as the test claims, then the PSHD could abort the simulation and decide halting behaviour correctly on that basis.  [This much is obvious, and is basically what Sipser means in his "agreement" statement that PO often quotes, although PO has his own differing interpretation of what that means.]
If H is such a PSHD, H might correctly decide many inputs, and moreover if it does manage to decide a particular input it will do so correctly, since its patterns are assumed sound.  E.g. we could define a sound pattern matching tight loops, and computations entering such a tight loop would be correctly identified as non-halting.
But such an H cannot detect /all/ non-halting conditions, and in particular cannot decide the behaviour of its corresponding H^(H^) computation.  When H simulates H^(H^), none of its tests will ever match against the trace of H^(H^), and the computation will never terminate, so H would just run forever, never deciding the input.  (We said H was only a partial decider, so no problem.) Every PSHD suffers this same flaw, no matter how many different (sound) tests it incorporates.
The logic of the Linz proof proves this behaviour (non-halting of H when given input (<H^>,<H^>), so PO's claim to have built such an H would be a problem for the Linz proof if correct.  Obviously his claim was not correct, and the problem here is that PO's "Infinite Recursive Simulation" pattern is clearly NOT sound!  [So PO's H is not a PSHD by the above definition.]
I pointed this out to PO years ago and suggested that to proceed he will have to provide a proof that his test is sound.  That was slightly tongue-in-cheek, as it's clear PO lacks the ability to construct a proof of just about anything, let alone something that's clearly false.  Sure enough PO has never seriously attempted such a proof!  [He did make an attempt once, which started with PO introducing an Axiom saying that the test was sound.  No, I'm not kidding, that really happened.]
I do find it strange that PO makes so little reference to the test and its details, since in the end it underpins PO's belief that his H is correct to decide non-halting for H^(H^), even though that computation demonstrably halts.  All he ever says about this is that H is correct because the input "exhibits non-terminating behaviour" when simulated by H.
Well that's totally vague, right?, but clearly what PO is saying is that his "Infinite Recursive Simulation" pattern matches, and so H^(H^) /really is non-halting/ !  He has an almost religious fervour in his intuition that his test is sound, despite having absolutely no proof or valid reasoning to back it up...  The belief is so strong that even direct empirical evidence to the contrary [H^(H^) halting when run under his own x86utm.exe] is rejected and must be "explained away" with further bizarre and unsupported claims about pathelogical self reference etc..
Regards,
Mike.