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: "Fred. Zwarts" Newsgroups: comp.theory Subject: Re: This function proves that only the outermost HHH examines the execution trace Date: Thu, 1 Aug 2024 14:52:36 +0200 Organization: A noiseless patient Spider Lines: 55 Message-ID: References: <0amdndFJSZSzYD77nZ2dnZfqnPednZ2d@brightview.co.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Thu, 01 Aug 2024 14:52:37 +0200 (CEST) Injection-Info: dont-email.me; posting-host="8c0ac17c3f9e00decd2248743b2f1a16"; logging-data="2259175"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19CJqEG8u9tr4/8P6diSjmy" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:SzigvMXg8tOEB3une4Vxc0GvcSk= In-Reply-To: Content-Language: en-GB Bytes: 3788 Op 01.aug.2024 om 14:03 schreef olcott: > On 8/1/2024 2:52 AM, Mikko wrote: >> On 2024-07-31 17:33:38 +0000, olcott said: >> >>> On 7/31/2024 4:15 AM, Mikko wrote: >>>> On 2024-07-30 23:40:21 +0000, olcott said: >>>> >>>>> On 7/30/2024 2:00 AM, Mikko wrote: >>>>>> On 2024-07-29 16:50:53 +0000, olcott said: >>>>>> >>>>>>> On 7/28/2024 3:59 AM, Mikko wrote: >>>>>>>> On 2024-07-27 20:05:31 +0000, olcott said: >>>>>>>>> If you had sufficient understanding of the x86 language >>>>>>>>> you would know that DDD is correctly emulated by HHH. >>>>>>>> >>>>>>>> If you had suffient understanding of x86 language and correctness >>>>>>>> you would know that DDD is incorrectly emnulated by HHH. >>>>>>> >>>>>>> This is only seems that way because every reviewer makes sure >>>>>>> to ignore one aspect of the basis of another. >>>>>> >>>>>> It is perfectly OK to ignore irrelevant details. A relevant detail >>>>>> is the meaning of the word "emulate" as that determines what is a >>>>>> correct emulation and what is not. >>>>> >>>>> *It is not OK to ignore* >>>>> >>>>> This algorithm is used by all the simulating termination analyzers: >>>>> >>>>>      If simulating halt decider *H correctly simulates its input D* >>>>>      *until H correctly determines that its simulated D would never* >>>>>      *stop running unless aborted* then >>>>> >>>>>      H can abort its simulation of D and correctly report that D >>>>>      specifies a non-halting sequence of configurations. >>>>> >>>>> >>>>> for DDD correctly emulated by HHH until... >>>> >>>> It is as Sipser does not say whether DDD is correctly simulated by HHH >>>> or what would constitute a correct simulation. >>>> >>> >>> This has already been fully established elsewhere. >> >> You have never shown any proof about either "correctly". >> > > When instructions are executed/emulated according to the > semantics of the x86 language then they are executed/emulated > correctly. > But only those instructions. A halting program is simulated correctly if no instructions are skipped.