Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: DDD correctly emulated by HHH is correctly rejected as non-halting.
Date: Mon, 15 Jul 2024 10:41:06 +0300
Organization: -
Lines: 92
Message-ID: <v72jqi$juvg$1@dont-email.me>
References: <v6m7si$1uq86$2@dont-email.me> <v6mhc7$20hbo$2@dont-email.me> <v6mhr3$20kkr$2@dont-email.me> <v6nts5$2be3m$1@dont-email.me> <v6op4h$2fuva$4@dont-email.me> <v6qo1d$2ugov$1@dont-email.me> <v6rajl$30qtt$7@dont-email.me> <v6tc75$3gidj$1@dont-email.me> <v6tri1$3imib$9@dont-email.me> <v702t1$2lgb$1@dont-email.me> <v70mel$61d8$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 15 Jul 2024 09:41:06 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="eb7bc3c094cc39ab136406329ffd9913";
	logging-data="654320"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/hjGgpQsBEnPImGEjGZlSM"
User-Agent: Unison/2.2
Cancel-Lock: sha1:q9RIleP6YhC0rPlGV97cNnD2KFg=
Bytes: 4461

On 2024-07-14 14:13:41 +0000, olcott said:

> On 7/14/2024 3:40 AM, Mikko wrote:
>> On 2024-07-13 12:22:24 +0000, olcott said:
>> 
>>> On 7/13/2024 3:00 AM, Mikko wrote:
>>>> On 2024-07-12 13:20:53 +0000, olcott said:
>>>> 
>>>>> On 7/12/2024 3:03 AM, Mikko wrote:
>>>>>> On 2024-07-11 14:10:24 +0000, olcott said:
>>>>>> 
>>>>>>> On 7/11/2024 1:25 AM, Mikko wrote:
>>>>>>>> On 2024-07-10 17:53:38 +0000, olcott said:
>>>>>>>> 
>>>>>>>>> On 7/10/2024 12:45 PM, Fred. Zwarts wrote:
>>>>>>>>>> Op 10.jul.2024 om 17:03 schreef olcott:
>>>>>>>>>>> typedef void (*ptr)();
>>>>>>>>>>> int HHH(ptr P);
>>>>>>>>>>> 
>>>>>>>>>>> void DDD()
>>>>>>>>>>> {
>>>>>>>>>>>    HHH(DDD);
>>>>>>>>>>> }
>>>>>>>>>>> 
>>>>>>>>>>> int main()
>>>>>>>>>>> {
>>>>>>>>>>>    HHH(DDD);
>>>>>>>>>>> }
>>>>>>>>>> 
>>>>>>>>>> Unneeded complexity. It is equivalent to:
>>>>>>>>>> 
>>>>>>>>>>        int main()
>>>>>>>>>>        {
>>>>>>>>>>          return HHH(main);
>>>>>>>>>>        }
>>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> Every time any HHH correctly emulates DDD it calls the
>>>>>>>>> x86utm operating system to create a separate process
>>>>>>>>> context with its own memory virtual registers and stack,
>>>>>>>>> thus each recursively emulated DDD is a different instance.
>>>>>>>> 
>>>>>>>> However, each of those instances has the same sequence of instructions
>>>>>>>> that the x86 language specifies the same operational meaning.
>>>>>>>> 
>>>>>>> 
>>>>>>> *That is counter-factual*
>>>>>>> When DDD is correctly emulated by HHH according to the
>>>>>>> semantics of the x86 programming language HHH must abort
>>>>>>> its emulation of DDD or both HHH and DDD never halt.
>>>>>> 
>>>>>> There is not "must" anywhere in the semantics of the programming language.
>>>>>> 
>>>>> 
>>>>> The semantics of the language specifies the behavior of
>>>>> the machine code thus deriving the must.
>>>> 
>>>> How can one derive "must" from the semantics of the machine code?
>>>> 
>>> 
>>> Deciders are required to (thus must) halt.
>> 
>> The semantics of the x86 language does not require that, nor that any of
>> the programs is a decider.
> 
> The subject our our conversion is a simulating termination
> analyzer

No, it is not. As stated on the Subject line, the subject is correctness of
the rejection of DDD as non-halting.

> AKA partial halt decider

That "AKA" is incorrect. The term "termination analyzer" means a program
of a certain kind and the term "partial halt decider" means a program of
a different kind.

> that accepts a finite string of x86 code as specifying halting behavior
> or rejects this finite string. Deciders are required to halt thus must
> abort the emulation of any input that would prevent this.

However, that is not sufficient. The decider must not accpet inputs that
its specification does not specify as acceptable and must not reject inputs
that its specification does not specify as rejectable. As you call your
program a "partial halt decider" you should also specify how it is partial,
i.e., what inputs it is required to answer the same whay as a halt decider
and what it may do with the other inputs.

-- 
Mikko