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

    From olcott@NoOne@NoWhere.com to comp.theory,sci.logic,comp.ai.philosophy on Tue Jul 22 12:00:13 2025
    From Newsgroup: comp.ai.philosophy

    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
    --- Synchronet 3.21a-Linux NewsLink 1.2