Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: DDD simulated by HHH cannot possibly halt (Halting Problem)
Date: Tue, 8 Apr 2025 10:51:49 +0300
Organization: -
Lines: 98
Message-ID: <vt2kil$1puad$1@dont-email.me>
References: <vsnchj$23nrb$2@dont-email.me> <vso4a5$302lq$1@dont-email.me> <vsqhuu$1hl94$2@dont-email.me> <vsqknb$1ldpa$1@dont-email.me> <vsrmn8$2o2f2$1@dont-email.me> <vstku7$p4u7$1@dont-email.me> <vsu95l$1c5kt$1@dont-email.me> <vt01l0$39kn7$1@dont-email.me> <vt28vk$1fe7a$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 08 Apr 2025 09:51:50 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="bda8ea56dc77aee86178d29b1be67de3";
	logging-data="1898829"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18YOHsAa+x54NsqrignAOb5"
User-Agent: Unison/2.2
Cancel-Lock: sha1:d8ESTBrfN6INrkLEuSgH+bh9hzo=
Bytes: 4369

On 2025-04-08 04:33:57 +0000, olcott said:

> On 4/7/2025 3:16 AM, Mikko wrote:
>> On 2025-04-06 16:12:36 +0000, olcott said:
>> 
>>> On 4/6/2025 5:27 AM, Mikko wrote:
>>>> On 2025-04-05 16:45:28 +0000, olcott said:
>>>> 
>>>>> On 4/5/2025 2:05 AM, Mikko wrote:
>>>>>> On 2025-04-05 06:18:06 +0000, olcott said:
>>>>>> 
>>>>>>> On 4/4/2025 3:12 AM, Mikko wrote:
>>>>>>>> On 2025-04-04 01:27:15 +0000, olcott said:
>>>>>>>> 
>>>>>>>>> void DDD()
>>>>>>>>> {
>>>>>>>>>     HHH(DDD);
>>>>>>>>>     return;
>>>>>>>>> }
>>>>>>>>> 
>>>>>>>>> Do you really think that anyone knowing the C
>>>>>>>>> programming language is too stupid to see that
>>>>>>>>> DDD simulated by HHH cannot possibly return?
>>>>>>>> 
>>>>>>>> Anyone knowing the C language can see that if DDD() does not halt
>>>>>>>> it means that HHH(DDD) does not halt. The knowledge that that
>>>>>>>> means that HHH is not a decider is possible but not required.
>>>>>>>> 
>>>>>>> 
>>>>>>> *Perpetually ignoring this is not any actual rebuttal at all*
>>>>>>> 
>>>>>>> *Simulating termination analyzer Principle*
>>>>>>> It is always correct for any simulating termination
>>>>>>> analyzer to stop simulating and reject any input that
>>>>>>> would otherwise prevent its own termination. The
>>>>>>> only rebuttal to this is rejecting the notion that
>>>>>>> deciders must always halt.
>>>>>> 
>>>>>> Wrong, because a termination analyzer is not required to halt.
>>>>> 
>>>>> Why say things that you know are untrue?
>>>> 
>>>> The term "termination analyzer" is used about programs that do not halt
>>>> on every input. There is no strict derfiniton of the term so there is
>>>> no requirement about halting.
>>>> 
>>>> On the first page of https://www.cs.princeton.edu/~zkincaid/pub/ pldi21.pdf
>>>> in the first parapgraph of Introduction:
>>>> 
>>>>    For example, termination analyzers may themselves fail to terminate on
>>>>    some input programs, or ...
>>>> 
>>>>> A termination analyzer that doesn't halt
>>>>> would flunk every proof of total program correctness.
>>>> 
>>>> There are no total termination analyzers.
>>> 
>>> Total proof of correctness does not require a halt
>>> decider, it only requires a termination analyzer
>>> with inputs in its domain.
>> 
>> Depends on what one wants to prove correct.
>> 
>> Often there is no way to determine whether a pariticular termination
>> analyser can determine about a particular program.
>> 
> 
> typedef void (*ptr)();
> int HHH(ptr P);
> 
> int DD()
> {
>    int Halt_Status = HHH(DD);
>    if (Halt_Status)
>      HERE: goto HERE;
>    return Halt_Status;
> }
> 
> int main()
> {
>    HHH(DD);
> }
> 
> *Simulating termination analyzer Principle*
> It is always correct for any simulating termination
> analyzer to stop simulating and reject any input that
> would otherwise prevent its own termination.
> 
> Rational minds would agree that the above principle
> is correct and directly applies to HHH(DD) rejecting
> its input.

From the meaning of the word "correct" obviously follows that it is
never correct to reject a terminating input as non-terminating.

-- 
Mikko