Deutsch English Français Italiano |
<v9kdbd$t0ee$1@dont-email.me> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: Mikko <mikko.levanto@iki.fi> Newsgroups: comp.theory Subject: Re: Overview of proof that the input to HHH(DDD) specifies non-halting behavior --- Mike Date: Thu, 15 Aug 2024 11:13:33 +0300 Organization: - Lines: 70 Message-ID: <v9kdbd$t0ee$1@dont-email.me> References: <v9edol$3metk$1@dont-email.me> <v9fe61$3rqao$1@dont-email.me> <v9flkh$3se8c$3@dont-email.me> <v9hooa$chqn$1@dont-email.me> <v9icl8$f16v$8@dont-email.me> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Thu, 15 Aug 2024 10:13:33 +0200 (CEST) Injection-Info: dont-email.me; posting-host="869077aac8cbf110e80701f4c3f6428a"; logging-data="950734"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX192b+EaNfk/VGeokKG6jTG+" User-Agent: Unison/2.2 Cancel-Lock: sha1:1w4Zfam8WMU3Bncj8H2KgV07RW8= Bytes: 3496 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. There is no conditional code that could cause anything else. Therefore, if DDD does not return the inference that HHH does not return is correct. -- Mikko