Re: Proof that DDD specifies non-halting behavior --- point by point

On 8/15/24 10:58 AM, olcott wrote:

On 8/15/2024 3:19 AM, Mikko wrote:

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.
>

>
There are no deviations. The x86utm operating system is
built from libx86emu that has had decades of development
effort. HHH really does emulate itself emulating DDD.
>

 And then ignores that emulation,