Path: ...!weretis.net!feeder8.news.weretis.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: Proof that DDD specifies non-halting behavior --- point by point
Date: Thu, 15 Aug 2024 11:19:38 +0300
Organization: -
Lines: 78
Message-ID: <v9kdmq$t1s7$1@dont-email.me>
References: <v9gv4k$4sc4$1@dont-email.me> <561f876601b0329c0260bac26f8b6dfb6e28647f@i2pn2.org> <v9h5af$9jn6$1@dont-email.me> <aa4bc24ac5642087e81796fffc31e5022bd8823e@i2pn2.org> <v9h9ec$a0id$1@dont-email.me> <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