Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: olcott Newsgroups: comp.theory Subject: Re: DDD correctly emulated by HHH is correctly rejected as non-halting V2 Date: Thu, 1 Aug 2024 06:56:31 -0500 Organization: A noiseless patient Spider Lines: 118 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Thu, 01 Aug 2024 13:56:32 +0200 (CEST) Injection-Info: dont-email.me; posting-host="3121e7e48560b53e45601f59b50fa691"; logging-data="2256545"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+/3mXCJz7Wk0PdyTmEvdFE" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:QbnF8PmvkATRWI4YgOG9xte0llI= In-Reply-To: Content-Language: en-US Bytes: 6003 On 8/1/2024 2:49 AM, Mikko wrote: > On 2024-07-31 17:28:38 +0000, olcott said: > >> On 7/31/2024 2:36 AM, Mikko wrote: >>> On 2024-07-16 18:18:07 +0000, olcott said: >>> >>>> On 7/16/2024 2:57 AM, Mikko wrote: >>>>> On 2024-07-15 13:43:34 +0000, olcott said: >>>>> >>>>>> On 7/15/2024 3:17 AM, Mikko wrote: >>>>>>> On 2024-07-14 14:50:47 +0000, olcott said: >>>>>>> >>>>>>>> On 7/14/2024 5:09 AM, Mikko wrote: >>>>>>>>> On 2024-07-12 14:56:05 +0000, olcott said: >>>>>>>>> >>>>>>>>>> We stipulate that the only measure of a correct emulation is the >>>>>>>>>> semantics of the x86 programming language. >>>>>>>>>> >>>>>>>>>> _DDD() >>>>>>>>>> [00002163] 55         push ebp      ; housekeeping >>>>>>>>>> [00002164] 8bec       mov ebp,esp   ; housekeeping >>>>>>>>>> [00002166] 6863210000 push 00002163 ; push DDD >>>>>>>>>> [0000216b] e853f4ffff call 000015c3 ; call HHH(DDD) >>>>>>>>>> [00002170] 83c404     add esp,+04 >>>>>>>>>> [00002173] 5d         pop ebp >>>>>>>>>> [00002174] c3         ret >>>>>>>>>> Size in bytes:(0018) [00002174] >>>>>>>>>> >>>>>>>>>> When N steps of DDD are emulated by HHH according to the >>>>>>>>>> semantics of the x86 language then N steps are emulated >>>>>>>>>> correctly. >>>>>>>>>> >>>>>>>>>> When we examine the infinite set of every HHH/DDD pair such that: >>>>>>>>>> HHH₁ one step of DDD is correctly emulated by HHH. >>>>>>>>>> HHH₂ two steps of DDD are correctly emulated by HHH. >>>>>>>>>> HHH₃ three steps of DDD are correctly emulated by HHH. >>>>>>>>>> ... >>>>>>>>>> HHH∞ The emulation of DDD by HHH never stops running. >>>>>>>>>> >>>>>>>>>> The above specifies the infinite set of every HHH/DDD pair >>>>>>>>>> where 1 to infinity steps of DDD are correctly emulated by HHH. >>>>>>>>> >>>>>>>>> You should use the indices here, too, e.g., "where 1 to >>>>>>>>> infinity steps of >>>>>>>>> DDD₁ are correctly emulated by HHH₃" or whatever you mean. >>>>>>>>> >>>>>>>> >>>>>>>> DDD is the exact same fixed constant finite string that >>>>>>>> always calls HHH at the same fixed constant machine >>>>>>>> address. >>>>>>> >>>>>>> If the function called by DDD is not part of the input then the >>>>>>> input does >>>>>>> not specify a behaviour and the question whether DDD halts is >>>>>>> ill-posed. >>>>>>> >>>>>> >>>>>> We don't care about whether HHH halts. We know that >>>>>> HHH halts or fails to meet its design spec. >>>>>> >>>>>> We are only seeing if DDD correctly emulated by HHH >>>>>> can can possibly reach its own final state. >>>>> >>>>> HHH does not see even that. It only sees whther that it does not >>>>> emulate >>>>> DDD to its final state. >>>> >>>> No. HHH is not judging whether or not itself is a correct >>>> emulator. The semantics of the x86 instructions that emulates >>>> prove that its emulation is correct. >>> >>> Semantics of x86 language alone doesn't prove anything. Only a detailed >>> comparison of the emulator code to the x86 semantics may prove that. >> >> A proof is any sequence of steps such that the conclusion >> is a necessary consequence of its basis. > > Only if every "step" is a sentence. > Not at all. My proof is the tautology that proves it is correct. > Your traces are not such sequences. > >> Proving that DDD correctly emulated by HHH matches the >> infinite recursion behavior pattern. >> (a) The semantics of the x86 language. >> (b) the design of HHH provided below. >> (c) The definition of infinite recursion provided below. >> >> *Infinite recursion behavior pattern* >> An emulated sequence of instructions that has no conditional >> branch instructions in this sequence is exactly repeated when >> it calls the same function with the same parameters again. >> As long as the called function can be determined to never >> return this proves infinite recursion. > > The recursive simulation does not satisfy the "no conditional branch" > requirement so does not match the pattern. > 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. It freaking meets the above highlighted criteria. -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer