On 1/31/2024 11:07 AM, immibis wrote:
> On 1/31/24 15:40, olcott wrote:
>> On 1/31/2024 2:19 AM, Mikko wrote:
>>> On 2024-01-30 14:58:21 +0000, olcott said:
>>>
>>>> On 1/30/2024 5:24 AM, Mikko wrote:
>>>>> On 2024-01-29 17:33:56 +0000, olcott said:
>>>>>
>>>>>> On 1/29/2024 11:02 AM, Mikko wrote:
>>>>>>> On 2024-01-29 14:39:58 +0000, olcott said:
>>>>>>>
>>>>>>>> On 1/29/2024 2:03 AM, Mikko wrote:
>>>>>>>>> On 2024-01-28 18:47:03 +0000, olcott said:
>>>>>>>>>
>>>>>>>>>> On 1/28/2024 12:25 PM, Mikko wrote:
>>>>>>>>>>> On 2024-01-28 14:59:06 +0000, immibis said:
>>>>>>>>>>>
>>>>>>>>>>>> On 1/28/24 14:25, Mikko wrote:
>>>>>>>>>>>>> On 2024-01-27 19:22:56 +0000, immibis said:
>>>>>>>>>>>>>> On 1/27/24 20:15, olcott wrote:
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Every H that must abort its simulation of any input D
>>>>>>>>>>>>>>> to prevent its own infinite execution is necessarily
>>>>>>>>>>>>>>> correct to reject D as non-halting.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> The computer science professor who told you that simply
>>>>>>>>>>>>>> misunderstood the question, and yet you continued to
>>>>>>>>>>>>>> parrot the answer to the misunderstood question for years.
>>>>>>>>>>>>>
>>>>>>>>>>>>> The computer science professor did not misundersand anything.
>>>>>>>>>>>>> Olcott misunderstood both the question and the answer.
>>>>>>>>>>>>
>>>>>>>>>>>> Misunderstanding what Olcott meant by a question is still
>>>>>>>>>>>> misunderstanding the question.
>>>>>>>>>>>
>>>>>>>>>>> No, it isn't. The question has a clear meaning from the
>>>>>>>>>>> tradition of
>>>>>>>>>>> English language even if Olcott meant something else.
>>>>>>>>>>>
>>>>>>>>>>> Mikko
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> Professor Sipser is the best selling author of theory of
>>>>>>>>>> computation textbooks.
>>>>>>>>>
>>>>>>>>> That is irrelevant to the question how good he is to interprete
>>>>>>>>> questions,
>>>>>>>>> in particular questions about agreement. However, from other
>>>>>>>>> considerations
>>>>>>>>> I think he probably understood the question in a way that I
>>>>>>>>> would call
>>>>>>>>> correct.
>>>>>>>>>
>>>>>>>>> Mikko
>>>>>>>>
>>>>>>>> Professor Sipser is a qualified expert in the
>>>>>>>> field of the theory of computation.
>>>>>>>>
>>>>>>>> On 10/13/2022 11:46 AM, olcott wrote:
>>>>>>>>  > MIT Professor Michael Sipser has agreed that the following
>>>>>>>>  > verbatim paragraph is correct ...
>>>>>>>>  >
>>>>>>>>  > If simulating halt decider H correctly simulates its input D
>>>>>>>>  > until H correctly determines that its simulated D would never
>>>>>>>>  > stop running unless aborted then H can abort its simulation
>>>>>>>>  > of D and correctly report that D specifies a non-halting
>>>>>>>>  > sequence of configurations.
>>>>>>>>  >
>>>>>>>>
>>>>>>>> This has been extensively reviewed and there never were
>>>>>>>> any alternative readings suggested.
>>>>>>>
>>>>>>> You mean, other than that that is a tautology that does
>>>>>>> not cotradict the fact that there is no halt decider.
>>>>>>>
>>>>>>
>>>>>> *It does contradict the misconception that there is no halt decider*
>>>>>
>>>>> No, it doesn't. A tautology is true even when there is no halt
>>>>> decider.
>>>>>
>>>>
>>>> *The tautology proves that the H on lines 668-691 is correct*
>>>> https://github.com/plolcott/x86utm/blob/master/Halt7.c
>>>
>>> No, it doesn't. It merely indicates what a proof of certain kind
>>> must prove.
>>>
>>
>> *THE FOLLOWING IS A TAUTOLOGY*
>> When one understands that H is always correct to abort any
>> simulation that cannot possibly stop running unless aborted
>>
>> 01 int D(ptr x)  // ptr is pointer to int function
>> 02 {
>> 03   int Halt_Status = H(x, x);
>> 04   if (Halt_Status)
>> 05     HERE: goto HERE;
>> 06   return Halt_Status;
>> 07 }
>> 08
>> 09 void main()
>> 10 {
>> 11   H(D,D);
>> 12 }
>>
>> as every H specified by the above template must do then each
>> and every element of this infinite set is correct to abort
>> its simulation of D and reject its input D as non-halting.
>>
>
> This is saying: If H doesn't abort its simulation then H is correct to
> abort its simulation.

All halt deciders must predict what the behavior of their
input would be.

*PREMISE* (self evident truth)
*When one understands that simulating termination analyzer H*
*is always correct to abort any simulation that cannot possibly*
*stop running unless aborted*

01 int D(ptr x) // ptr is pointer to int function
02 {
03 int Halt_Status = H(x, x);
04 if (Halt_Status)
05 HERE: goto HERE;
06 return Halt_Status;
07 }
08
09 void main()
10 {
11 H(D,D);
12 }

*IS LOGICALLY ENTAILED FROM PREMISE*
Then every simulating termination analyzer H specified by
the above template correctly aborts its simulation of D
and correctly rejects D as non-halting.

Pages 661 to 696 of Halt7.c specify the H that does this
https://github.com/plolcott/x86utm/blob/master/Halt7.c

This is true because halt deciders are requires to report on
the behavior that their input finite string specifies and
are not allowed to report on any other behavior.

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

On 31/01/24 18:11, olcott wrote:
> On 1/31/2024 11:07 AM, immibis wrote:
>> This is saying: If H doesn't abort its simulation then H is correct to
>> abort its simulation.
>
> All halt deciders must predict what the behavior of their
> input would be.

And yours predicts wrong.

On 02/05/2024 01:00 PM, immibis wrote:
> On 31/01/24 18:11, olcott wrote:
>> On 1/31/2024 11:07 AM, immibis wrote:
>>> This is saying: If H doesn't abort its simulation then H is correct
>>> to abort its simulation.
>>
>> All halt deciders must predict what the behavior of their
>> input would be.
>
> And yours predicts wrong.

One thing you're getting into is "quantifier disambiguation".

That is, for a given decider, there are undecideable inputs,
but, there exists a different decider, for which the same input's
decideable.

I.e., "for-any for-any" and "for-any for-all" and "for-all for-any"
and "for-all for-all", are four different disambiguations reflecting
quantifier application to the transfer principle or to that "for-each is
for-all", about breaking the quantifier down to at least

for-any <- at least one?
for-each <- going through?
for-every <- gone through?
for-all <- all as one?

that these sort of reflect why the universal quantifier suffers usual
quantifier ambiguities or the impredicative what with regards to
Feferman and quantifier disambiguation helps provide greater concrete
framings for the halting or traveling or branching or Entsheidungs.

This doesn't necessarily so help PO "validate his decider" but it does
illustrate that there are various concrete framings of what's otherwise
let out about static analysis generally, that specifically, there are
always approaches for static analysis to proceed, then as with respect
to existence proofs vis-a-vis demonstrations, and of course the very
notion of "completions", in logic and mathematics, of the "incomplete",
at all.

So, for things like the Sorites or Heap, quantifier disambiguation
doesn't go without saying, for such notions of predicativity and
impredicativity and even just "framing it in the second order" or
"under the conditions where the tape admits an arithmetization,
algebraization, or geometrization".

For tautology and identity and sameness and intensionality and
extensionality and such things, it's a lot about what things are,
"equal", as when, "almost", or the infinite or continuum limit,
vis-a-vis usually ordering theory.

Then, the usual idea that "the world of deciders is too big to find the
right one for an arbitrary input", still has that static analysis finds
most of the easy grapes, and, that the world of deciders is big enough
to include the input's own very one.

Not that it's very general, ....

So, it is a common misconclusion that "there exists an inscrutable input
for this decider" means "there exists inputs inscrutable any decider",
it's a usual error after impredicativity of quantifier ambiguity, where
logic sort of just has "next-higher-order" for these kinds of things,
and all sorts usual forms of concrete static analysis.

--
https://www.youtube.com/@rossfinlayson <- a "podcasts" or "vlog"