Path: ...!weretis.net!feeder8.news.weretis.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: Mikko Newsgroups: comp.theory Subject: Re: Proof that DDD specifies non-halting behavior --- point by point Date: Thu, 15 Aug 2024 11:19:38 +0300 Organization: - Lines: 78 Message-ID: References: <561f876601b0329c0260bac26f8b6dfb6e28647f@i2pn2.org> <190847da05ab48555c036a799e768f555461eb43@i2pn2.org> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Thu, 15 Aug 2024 10:19:39 +0200 (CEST) Injection-Info: dont-email.me; posting-host="869077aac8cbf110e80701f4c3f6428a"; logging-data="952199"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/W2+Iv22j1ArlA4tYLjLwE" User-Agent: Unison/2.2 Cancel-Lock: sha1:7+V84VPbsbmTU0J/xgb0E5SS6dE= Bytes: 3742 On 2024-08-14 04:04:23 +0000, Richard Damon said: > On 8/13/24 11:48 PM, olcott wrote: >> On 8/13/2024 10:21 PM, Richard Damon wrote: >>> On 8/13/24 10:38 PM, olcott wrote: >>>> On 8/13/2024 9:29 PM, Richard Damon wrote: >>>>> On 8/13/24 8:52 PM, olcott wrote: >>>>>> void DDD() >>>>>> { >>>>>>    HHH(DDD); >>>>>>    return; >>>>>> } >>>>>> >>>>>> _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] >>>>>> >>>>>> A simulation of N instructions of DDD by HHH according to >>>>>> the semantics of the x86 language is necessarily correct. >>>>>> >>>>> >>>>> Nope, it is just the correct PARTIAL emulation of the first N >>>>> instructions of DDD, and not of all of DDD, >>>> >>>> That is what I said dufuss. >>> >>> Nope. You didn't. I added clairifying words, pointing out why you claim >>> is incorrect. >>> >>> For an emulation to be "correct" it must be complete, as partial >>> emulations are only partially correct, so without the partial modifier, >>> they are not correct. >>> >> >> A complete emulation of one instruction is >> a complete emulation of one instruction > > > >> >>>> >>>>> >>>>>> A correct simulation of N instructions of DDD by HHH is >>>>>> sufficient to correctly predict the behavior of an unlimited >>>>>> simulation. >>>>> >>>>> Nope, if a HHH returns to its caller, >>>> >>>> *Try to show exactly how DDD emulated by HHH returns to its caller* >>>> (the first one doesn't even have a caller) >>>> Use the above machine language instructions to show this. >>>> >>> >>> Remember how English works: >>> >>> When you ask "How DDD emulated by HHH returns to its callers". >> >> Show the exact machine code trace of how DDD emulated >> by HHH (according to the semantics of the x86 language) >> reaches its own machine address 00002183 > > No. The trace is to long, and since you HHH doesn't meet your > requirements (since it isn't a pure function) you can't give me a > compldte input to trace. The trace is regular enough that we could define a formal language for the trace and construct an analyzer program to detect deviations from x86 semnatics and hidden inputs. -- Mikko