Deutsch   English   Français   Italiano  
<vqu84v$363tm$1@dont-email.me>

View for Bookmarking (what is this?)
Look up another Usenet article

Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: Every sufficiently competent C programmer knows --- posthumous reviewers
Date: Thu, 13 Mar 2025 11:22:39 +0200
Organization: -
Lines: 144
Message-ID: <vqu84v$363tm$1@dont-email.me>
References: <vqntaq$1jut5$1@dont-email.me> <vqp388$1tvqa$1@dont-email.me> <vqpdv9$202b2$2@dont-email.me> <vqperb$20c9k$2@dont-email.me> <E6mcnWv3nMa66036nZ2dnZfqnPWdnZ2d@brightview.co.uk> <vqpv2u$23vhr$1@dont-email.me> <Ny-dnRlMHcVpA036nZ2dnZfqnPqdnZ2d@brightview.co.uk> <vqrjrn$2h4l2$1@dont-email.me> <nESdnUfJxdhoTkz6nZ2dnZfqnPSdnZ2d@brightview.co.uk> <vqsl7c$2ok91$1@dont-email.me> <f7b6995ae3e79db00fa5070d9be8126b7ea5ae78@i2pn2.org> <vqt99l$2spcd$5@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 13 Mar 2025 10:22:39 +0100 (CET)
Injection-Info: dont-email.me; posting-host="80488b36e9a6425fadc2d3d82bbb0c14";
	logging-data="3346358"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX197ORr9oi/J3H9xUuGSkILc"
User-Agent: Unison/2.2
Cancel-Lock: sha1:WoteAIMiTG95MrgQX0rNnie3gQY=
Bytes: 7463

On 2025-03-13 00:36:04 +0000, olcott said:

> On 3/12/2025 5:47 PM, Richard Damon wrote:
>> On 3/12/25 2:53 PM, olcott wrote:
>>> On 3/12/2025 1:35 PM, Mike Terry wrote:
>>>> 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.]
>>>> 
>>> 
>>> _DDD()
>>> [00002172] 55         push ebp      ; housekeeping
>>> [00002173] 8bec       mov  ebp,esp  ; housekeeping
>>> [00002175] 6872210000 push 00002172 ; push DDD
>>> [0000217a] e853f4ffff call 000015d2 ; call HHH(DDD)
>>> [0000217f] 83c404     add  esp,+04
>>> [00002182] 5d         pop  ebp
>>> [00002183] c3         ret
>>> Size in bytes:(0018) [00002183]
>>> 
>>> When DDD is emulated by HHH according to the semantics
>>> of the above x86 machine language then DDD cannot possibly
>>> reach past its own machine address 0000217a.
>>> 
>>> My posthumous reviewers will notice that my current
>>> reviewers were disingenuous to the extent of dishonesty
>>> on this specific point.
>>> 
>> 
>> But the problem is the HHH that does that never answers,
> 
> So you forgot the details of this context?
> 
> typedef void (*ptr)();
> int HHH(ptr P);
> 
> void Infinite_Loop()
> {
>    HERE: goto HERE;
>    return;
> }
> 
> void Infinite_Recursion()
> {
>    Infinite_Recursion();
>    return;
> }
> 
> void DDD()
> {
>    HHH(DDD);
>    return;
> }
> 
> int DD()
> {
>    int Halt_Status = HHH(DD);
>    if (Halt_Status)
>      HERE: goto HERE;
>    return Halt_Status;
> }
> 
> When HHH correctly emulates N steps of the
> above functions none of them can possibly reach
> their own "return" instruction and terminate normally.

Nevertheless, assuming HHH is a decider, Infinite_Loop and Infinite_Recursion
specify a non-terminating behaviour, DDD specifies a terminating behaviour
and DD only specifies that termination or non-terimination depends on HHH.

-- 
Mikko