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: Mon, 7 Apr 2025 11:16:32 +0300
Organization: -
Lines: 66
Message-ID: <vt01l0$39kn7$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 07 Apr 2025 10:16:33 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="8ae89a7175d590b824f758ddcfef81d4";
	logging-data="3461863"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19YSMrtI600teFnKkb+APyE"
User-Agent: Unison/2.2
Cancel-Lock: sha1:PzeBG+UJZhoxfKz30J1B36TFZmI=
Bytes: 3386

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.

-- 
Mikko