Path: ...!3.eu.feeder.erje.net!feeder.erje.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: Mikko Newsgroups: comp.theory Subject: Re: Overview of proof that the input to HHH(DDD) specifies non-halting behavior --- Mike Date: Fri, 16 Aug 2024 11:07:01 +0300 Organization: - Lines: 77 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 16 Aug 2024 10:07:02 +0200 (CEST) Injection-Info: dont-email.me; posting-host="a261f81d360d8a0d1650f1befa0eb23e"; logging-data="1451091"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX199Lv/24G5BUpzxN6foEaey" User-Agent: Unison/2.2 Cancel-Lock: sha1:wMIo+TTaKSi6+PhJluxq237wx+o= Bytes: 3907 On 2024-08-15 15:07:11 +0000, olcott said: > On 8/15/2024 3:13 AM, Mikko wrote: >> On 2024-08-14 13:49:28 +0000, olcott said: >> >>> On 8/14/2024 3:09 AM, Mikko wrote: >>>> On 2024-08-13 13:04:17 +0000, olcott said: >>>> >>>>> On 8/13/2024 5:57 AM, Mikko wrote: >>>>>> On 2024-08-13 01:43:49 +0000, olcott said: >>>>>> >>>>>>> We prove that the simulation is correct. >>>>>>> Then we prove that this simulation cannot possibly >>>>>>> reach its final halt state / ever stop running without being aborted. >>>>>>> The semantics of the x86 language conclusive proves this is true. >>>>>>> >>>>>>> Thus when we measure the behavior specified by this finite >>>>>>> string by DDD correctly simulated/emulated by HHH it specifies >>>>>>> non-halting behavior. >>>>>>> >>>>>>> https://www.researchgate.net/ >>>>>>> publication/369971402_Simulating_Termination_Analyzer_H_is_Not_Fooled_by_Pathological_Input_D >>>>>>> >>>>>> >>>>>> Input to HHH(DDD) is DDD. If there is any other input then the proof is >>>>>> not interesting. >>>>>> >>>>>> The behviour specified by DDD on the first page of the linked article >>>>>> is halting if HHH(DDD) halts. Otherwise HHH is not interesting. >>>>>> >>>>>> Any proof of the false statement that "the input to HHH(DDD) specifies >>>>>> non-halting behaviour" is either uninteresting or unsound. >>>>>> >>>>> >>>>> void DDD() >>>>> { >>>>>    HHH(DDD); >>>>>    return; >>>>> } >>>>> >>>>> It is true that DDD correctly emulated by any HHH cannot >>>>> possibly reach its own "return" instruction final halt state. >>>> >>>> If DDD does not halt then HHH does not halt. >>>> >>> >>> _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] >>> >>> The impossibility of DDD emulated by HHH >>> (according to the semantics of the x86 language) >>> to reach its own machine address [00002183] is >>> complete proof that DDD never halts. >>> >>> This has nothing to do with whether or not HHH >>> halts. >> >> Everone who understands either C or x86 machine code can see that >> the next thing DDD does after the return from HHH (if HHH ever >> returns) is that DDD returns. > > It is 100% impossible for the first emulated instance > of DDD to return because it is never called. Whether the first emulated instance is called or not does not affect the behaviour that DDD specifies. -- Mikko