Re: Title: A Structural Analysis of the Standard Halting Problem Proof --- Alan Mackenzie

On 7/21/2025 3:58 PM, Alan Mackenzie wrote:

In comp.theory olcott <polcott333@gmail.com> wrote:
 

typedef void (*ptr)();
int HHH(ptr P);

 

void DDD()
{
   HHH(DDD);
   return;
}

 

int main()
{
   HHH(DDD);
}

 

Not at all. HHH does emulate the x86 machine code
of DDD pointed to by P. That is does this according
to the semantics of the x86 language conclusively
proves that this emulation is correct.

 That's nauseatingly overstretching things into another lie.  Whatever HHH
might do is far short of sufficient "conclusively to prove" that the
emulation is correct.  To prove that is likely impossible in principle,
that's even assuming you could define "correct" coherently.
 

_DDD()
[00002192] 55             push ebp
[00002193] 8bec           mov ebp,esp
[00002195] 6892210000     push 00002192  // push DDD
[0000219a] e833f4ffff     call 000015d2  // call HHH
[0000219f] 83c404         add esp,+04
[000021a2] 5d             pop ebp
[000021a3] c3             ret
Size in bytes:(0018) [000021a3]
To prove (beyond all possible doubt) that HHH
does emulate DDD correctly only requires that
each instruction of DDD is emulated according
to the meaning of that instruction.
When HHH emulates the instruction at machine address
00002192 and it emulates DDD pushing its own ebp onto
its own stack this is proof that this instruction was
emulated correctly. If instead HHH emulated: "push ebp"
as "jmp 000021a3" that would be an incorrect emulation.
What exactly did you mean by "likely impossible in principle"
(please it all over again using different words).
I could make this proof more detailed by providing
the full state of the DDD virtual machine before
and after each emulated instruction.
line 1444 SaveState() Saves 16 register values
line 1469 LoadState() Loads 16 register values
line 1638 DebugStep()
Switch process context from emulator to emulated
Emulate one slave instruction
Switch process context from emulated back to emulator
https://github.com/plolcott/x86utm/blob/master/x86utm.cpp
--
Copyright 2024 Olcott
"Talent hits a target no one else can hit;
  Genius hits a target no one else can see."
  Arthur Schopenhauer