Path: ...!feed.opticnetworks.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: "Fred. Zwarts" <F.Zwarts@HetNet.nl>
Newsgroups: comp.theory,sci.logic
Subject: Re: Simulating termination analyzers for dummies
Date: Tue, 18 Jun 2024 17:47:29 +0200
Organization: A noiseless patient Spider
Lines: 249
Message-ID: <v4sa6j$1dcrb$3@dont-email.me>
References: <v4oaqu$f9p5$1@dont-email.me> <v4os9e$i70m$1@dont-email.me>
 <v4p9mb$lavj$1@dont-email.me> <v4pdph$l7lf$1@dont-email.me>
 <v4pepj$ln46$15@dont-email.me> <v4pgk3$l7le$2@dont-email.me>
 <v4phhl$mub6$2@dont-email.me> <v4piea$l7le$5@dont-email.me>
 <v4pmb8$nmvq$1@dont-email.me> <v4rekj$180pg$1@dont-email.me>
 <v4rv45$1blnm$1@dont-email.me> <v4s8k7$1dcrb$1@dont-email.me>
 <v4s9cj$1dk9i$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 18 Jun 2024 17:47:31 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="26f683594679855339d1c38e4ced75da";
	logging-data="1487723"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18p8nHh+3W35Al90YGWI1Rq"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:ttE3uPfDTu7a55+p4xtUX/D1UN4=
In-Reply-To: <v4s9cj$1dk9i$1@dont-email.me>
Content-Language: en-GB
Bytes: 10889

Op 18.jun.2024 om 17:33 schreef olcott:
> On 6/18/2024 10:20 AM, Fred. Zwarts wrote:
>> Op 18.jun.2024 om 14:38 schreef olcott:
>>> On 6/18/2024 2:57 AM, Fred. Zwarts wrote:
>>>> Op 17.jun.2024 om 17:56 schreef olcott:
>>>>> On 6/17/2024 9:49 AM, Fred. Zwarts wrote:
>>>>>> Op 17.jun.2024 om 16:34 schreef olcott:
>>>>>>> On 6/17/2024 9:18 AM, Fred. Zwarts wrote:
>>>>>>>> Op 17.jun.2024 om 15:47 schreef olcott:
>>>>>>>>> On 6/17/2024 8:30 AM, Fred. Zwarts wrote:
>>>>>>>>>> Op 17.jun.2024 om 14:20 schreef olcott:
>>>>>>>>>>> On 6/17/2024 3:31 AM, Fred. Zwarts wrote:
>>>>>>>>>>>> Op 17.jun.2024 om 05:33 schreef olcott:
>>>>>>>>>>>>> To understand this analysis requires a sufficient knowledge of
>>>>>>>>>>>>> the C programming language and what an x86 emulator does.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Unless every single detail is made 100% explicit false 
>>>>>>>>>>>>> assumptions
>>>>>>>>>>>>> always slip though the cracks. This is why it must be 
>>>>>>>>>>>>> examined at
>>>>>>>>>>>>> the C level before it is examined at the Turing Machine level.
>>>>>>>>>>>>>
>>>>>>>>>>>>> typedef void (*ptr)();
>>>>>>>>>>>>> int H0(ptr P);
>>>>>>>>>>>>>
>>>>>>>>>>>>> void Infinite_Loop()
>>>>>>>>>>>>> {
>>>>>>>>>>>>>    HERE: goto HERE;
>>>>>>>>>>>>> }
>>>>>>>>>>>>>
>>>>>>>>>>>>> void Infinite_Recursion()
>>>>>>>>>>>>> {
>>>>>>>>>>>>>    Infinite_Recursion();
>>>>>>>>>>>>> }
>>>>>>>>>>>>>
>>>>>>>>>>>>> void DDD()
>>>>>>>>>>>>> {
>>>>>>>>>>>>>    H0(DDD);
>>>>>>>>>>>>>    return;
>>>>>>>>>>>>> }
>>>>>>>>>>>>>
>>>>>>>>>>>>> int main()
>>>>>>>>>>>>> {
>>>>>>>>>>>>>    H0(Infinite_Loop);
>>>>>>>>>>>>>    H0(Infinite_Recursion);
>>>>>>>>>>>>>    H0(DDD);
>>>>>>>>>>>>> }
>>>>>>>>>>>>>
>>>>>>>>>>>>> Every C programmer that knows what an x86 emulator is knows 
>>>>>>>>>>>>> that when H0
>>>>>>>>>>>>> emulates the machine language of Infinite_Loop, 
>>>>>>>>>>>>> Infinite_Recursion, and
>>>>>>>>>>>>> DDD that it must abort these emulations so that itself can 
>>>>>>>>>>>>> terminate
>>>>>>>>>>>>> normally.
>>>>>>>>>>>>>
>>>>>>>>>>>>> When this is construed as non-halting criteria then simulating
>>>>>>>>>>>>> termination analyzer H0 is correct to reject these inputs 
>>>>>>>>>>>>> as non-
>>>>>>>>>>>>> halting.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> For Infinite_Loop and Infinite_Recursion that might be true, 
>>>>>>>>>>>> because there the simulator processes the whole input.
>>>>>>>>>>>>
>>>>>>>>>>>> The H0 case is very different. For H0 there is indeed a 
>>>>>>>>>>>> false assumption, as you mentioned. Here H0 needs to 
>>>>>>>>>>>> simulate itself, but the simulation is never able to reach 
>>>>>>>>>>>> the final state of the simulated self. The abort is always 
>>>>>>>>>>>> one cycle too early, so that the simulating H0 misses the 
>>>>>>>>>>>> abort. Therefore this results in a false negative.
>>>>>>>>>>>> (Note that H0 should process its input, which includes the 
>>>>>>>>>>>> H0 that aborts, not a non-input with an H that does not abort.)
>>>>>>>>>>>>
>>>>>>>>>>>> This results in a impossible dilemma for the programmer. It 
>>>>>>>>>>>> he creates a H that does not abort, it will not terminate. 
>>>>>>>>>>>
>>>>>>>>>>> *Therefore what I said is correct*
>>>>>>>>>>
>>>>>>>>>> No, that is not a logical conclusion. 
>>>>>>>>>
>>>>>>>>> Every C programmer that knows what an x86 emulator is knows
>>>>>>>>> that when H0 emulates the machine language of Infinite_Loop, 
>>>>>>>>> Infinite_Recursion, and DDD that it must abort these emulations
>>>>>>>>> so that itself can terminate normally.
>>>>>>>>
>>>>>>>> That might be correct.
>>>>>>>>>
>>>>>>>>> When this is construed as non-halting criteria then simulating
>>>>>>>>> termination analyzer H0 is correct to reject these inputs as non-
>>>>>>>>> halting.
>>>>>>>>
>>>>>>>> That is wrong. It only shows that H0 is unable to simulate 
>>>>>>>> itself. It tells nothing about the halting of the input.
>>>>>>>>
>>>>>>>>>
>>>>>>>>> *Too late you have already affirmed the words above*
>>>>>>>>> Affirming the first part necessitates the second part.
>>>>>>>>>
>>>>>>>> That is not logical. If a non-aborting program is wrong, it does 
>>>>>>>> not follow that a program that aborts is correct.
>>>>>>>> Please, think before you reply.
>>>>>>>>
>>>>>>>> So, I repeat:
>>>>>>>> The logical conclusion if both aborting and not aborting result 
>>>>>>>> in errors, is: a halt-decider cannot be based on such a simulation.
>>>>>>>
>>>>>>> Your view here is merely ignorant of the fact that deciders
>>>>>>> must report on the behavior specified by their inputs.
>>>>>>>
>>>>>>
>>>>>> It is incorrect to assume that a failing simulation is able to 
>>>>>> report about its input.
>>>>>> The simulation fails, because H0 is unable to simulate itself.
>>>>>>
>>>>>
>>>>> There is no possible way for the call to H0 by DDD
>>>>> correctly simulated by any H0 to return to its caller.
>>>>
>>>> We have not seen a proof for this claim and since H0 has 
>>>> contradictory requirements nobody else has ever provided a proof.
>>>> But OK, lets assume your are right. Simulated H0 is unable to 
>>>> simulate itself op to its final state and return to its caller, 
>>>> because it was aborted one cycle before it would return to its caller.
>>>>
>>>>>
>>>>> _DDD()
>>>>> [00001fd2] 55               push ebp
>>>>> [00001fd3] 8bec             mov ebp,esp
>>>>> [00001fd5] 68d21f0000       push 00001fd2 ; push address of DDD
>>>>> [00001fda] e8f3f9ffff       call 000019d2 ; call  H0
>>>>> [00001fdf] 83c404           add esp,+04
>>>>> [00001fe2] 5d               pop ebp
>>>>> [00001fe3] c3               ret
>>>>> Size in bytes:(0018) [00001fe3]
>>>>>
>>>>> *THAT THIS IS OVER YOUR HEAD DOES NOT MEAN THAT I AM INCORRECT*
>>>>> DDD correctly simulated by H0 *is* the behavior that
>>>>> the finite string of x86 machine code of DDD specifies.
>>>>>
>>>>
>>>> It is such a simple fact that H0 cannot possibly correct. 
>>>
>>> Are you pretending to be incompetent about the semantics of the
>>> x86 language or you you actually incompetent?
>>
>> I understand x86, but I am afraid you don't. Because you assume 
>> results that are not there.
>>
>>>
>>> The C people already agreed that I am correct about this:
>>
>> No serious C people have agreed. They can't, because your H0 has 
>> contradictory requirements.
>>
> 
> It is a verified fact that serious C people have recently
> agreed to the following verbatim statement in the C group.
> You either lack this degree of skill in C or are only
> interested in playing head games.

I have seen the response. It was most certainly not a serious reply.
But you know apparently to little of C to understand that.
Probably, because you are unable to escape from rebuttal mode, even if 
the truth is obvious.

It was your own proof that showed that in

        int main()
        {
          return H(main);
        }

========== REMAINDER OF ARTICLE TRUNCATED ==========