Re: Simulating termination analyzers for dummies

Am Wed, 19 Jun 2024 21:25:31 -0500 schrieb olcott:

On 6/19/2024 9:17 PM, Richard Damon wrote:

On 6/19/24 10:02 PM, olcott wrote:

On 6/19/2024 8:39 PM, Richard Damon wrote:

On 6/19/24 8:44 PM, olcott wrote:

On 6/19/2024 7:23 PM, Richard Damon wrote:

On 6/19/24 9:00 AM, olcott wrote:

On 6/19/2024 3:08 AM, Fred. Zwarts wrote:

Op 18.jun.2024 om 18:26 schreef olcott:

On 6/18/2024 10:47 AM, Fred. Zwarts wrote:

Op 18.jun.2024 om 17:33 schreef olcott:

On 6/18/2024 10:20 AM, Fred. Zwarts wrote:

It is easier to understand because a print statement was added.
You proved that it halts, but H0 reports non-halting.
So, it produces a false negative.
So, now it has been proved that H, H0, etc produce false
negatives, when used to determine halting behaviour, please, stop
to call them halt-deciders, or termination-deciders.
They might be "simulation deciders". When returning true, the
simulation was correct, when false, the full simulation was not
possible.

Why does H0 NEED to be able to simulate its input?

Yeah, why? That just adds a contradictory requirement. Not that it were
possible otherwise.

Decider must compute the mapping from their finite string input to
the actual behavior that this finite string specifies.

If possible.

They are not free to imagine the behavior that the authors of
textbooks expect.

Nor crackpots.

The finite string input does not communicate the behavior that the
textbook authors expect it to communicate.

Bullshit. Your neither-decider-nor-simulator just can't handle it.
The direct execution of DDD is the measure of things. A simulation
must behave identically. Of course you may be able to do analysis
on whether it halts, but that's different. Simulation is dumb.

The finite string certainly DOES communicate what is needed to
determine the behavior, or it wasn't a correct representation.

Deflection follows:

There is no sequence of truth preserving operations from the finite
string machine code of DDD that can correctly ignore the pathological
relationship between H0 and DDD as an aspect of the behavior that this
finite string specifies.

Many other simulators or deciders work correctly with DDD, just not the
one it calls. But they each get a different one wrong.
What do you mean with "ignore the relationship"?

No one has noticed this before because no one ever thought to make every
single detail 100% concrete, thus leaving huge gaps in all prior
reasoning.

We have a proof.

--
Man kann mit dunklen Zahlen nicht rechnen. Für die eigentliche Mathematik
sind sie vollkommen nutzlos. --Wolfgang Mückenheim