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

olcott <NoOne@nowhere.com> wrote:

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

[ Followup-To: set ]

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

On 7/21/2025 10:52 AM, Alan Mackenzie wrote:

[ .... ]

You will have a get out clause from the vagueness of your language, which
could be construed to mean practically anything.

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.

[00002192] 55             push ebp
[00002193] 8bec           mov ebp,esp
[00002195] 6892210000     push 00002192
[0000219a] e833f4ffff     call 000015d2  // call HHH
[0000219f] 83c404         add esp,+04
[000021a2] 5d             pop ebp
[000021a3] c3             ret
Size in bytes:(0018) [000021a3]

x86utm is a multi-tasking operating system (that I wrote)
that allows any C function to execute any other C function
in debug step mode. HHH and DDD have their own virtual
registers and stack.

When HHH emulates the first instruction of DDD it
emulates pushing the DDD ebp base pointer onto the
DDD stack.

*That is a 100% concrete example of correct emulation*

Which appears to be beside the point.

Exactly how is it that you could have construed this
as impossible in principle?

You seem to be "proving" the correctness of your emulation by giving one
example of its execution and saying "because it works for this particular
case, it works in general".

It is as though you are testing a multiplication program and give it the
inputs 3.0 and 1.5, you get the answer 4.5 "therefore" it works properly.
Actually, what you were testing turned out to be an addition program.

You can never prove a program is correct just by getting correct results
from a single run of it, or even correct results from several or many
runs.  This is impossible in principle.  And as I wrote earlier, that
even supposes that you can define "correct" coherently and usefully.

--
Copyright 2024 Olcott

2024???

"Talent hits a target no one else can hit;
 Genius hits a target no one else can see."
 Arthur Schopenhauer

--
Alan Mackenzie (Nuremberg, Germany).