Re: How do simulating termination analyzers work? ---Truth Maker Maximalism FULL_TRACE

On 7/13/25 4:43 PM, olcott wrote:

On 7/7/2025 9:07 AM, Alan Mackenzie wrote:

olcott <polcott333@gmail.com> wrote:

On 7/6/2025 4:23 PM, Alan Mackenzie wrote:

olcott <polcott333@gmail.com> wrote:

On 7/6/2025 12:52 PM, Alan Mackenzie wrote:

olcott <polcott333@gmail.com> wrote:

On 7/6/2025 11:02 AM, Alan Mackenzie wrote:

>

[ .... ]

>

int DD()
{
     int Halt_Status = HHH(DD);
     if (Halt_Status)
       HERE: goto HERE;
     return Halt_Status;
}

>

Then you should know that DD simulated by HHH
according to the semantics of the C programming
language cannot possibly reach its own "return"
statement final halt state.

>

An argument like this is at such a low level of abstraction as to be near
valuless.

>

It is really weird that you are calling a 100% complete
concrete specification "a low level of abstraction".
That HHH(DD) correctly determines that DD simulated by
HHH cannot possibly halt is a proven fact.

>

A complete concrete specification would necessarily include a description
of what you mean by "simulation".

>

I specifically mean that this x86 machine code

[ .... ]

Is emulated by an x86 emulator named HHH.

>
That's no adequate description.  To make it so, you'd have to say what
you mean by an "x86 emulator".  The name you give it is irrelevant
>

  But my point was that rather than
sticking to the abstract nature of the proof, you're chipping tiny pieces
out of it and dealing with those.  The proof you claim to refute has no
notion of simulation, for example; it doesn't need it.

>
>

*Not at all there are two pieces*
(1) HHH(DD) does correctly determine that its input
     specifies non halting behavior.
(2) The directly executed DD() does not contradict this.

>
The word "correctly" is fully redundant there.
>
The proof does not state whether the constructed function returns true or
false, i.e. whether it specifies non halting behaviour.

 The proof is purported to prove THAT DD is an undecidable
input for HHH. This is its counter example refuting the
claim that a universal halt decider can exist.
  

But since your DD by your own admission is a category error for a halt decider, as you have specifically stated it isn't a program as the input doesn't include the code of the specific HHH that it calls, you proof is just invalid.
Sorry, all you proved is that you don't know what you are talking about.