Path: ...!weretis.net!feeder8.news.weretis.net!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: Proof that DDD specifies non-halting behavior --- point by point
Date: Thu, 15 Aug 2024 13:22:16 +0300
Organization: -
Lines: 28
Message-ID: <v9kkso$u2rh$1@dont-email.me>
References: <v9gv4k$4sc4$1@dont-email.me> <v9hp66$ck4s$1@dont-email.me> <v9ia4j$f16v$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 15 Aug 2024 12:22:17 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="12fc9c697b40d6367e6f93c8d12f250c";
	logging-data="985969"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19R1y77vaYI4+vasEDvDOmf"
User-Agent: Unison/2.2
Cancel-Lock: sha1:Km9cluBwMw+omy7VDIC5eAhOoFM=
Bytes: 1782

On 2024-08-14 13:06:27 +0000, olcott said:

> On 8/14/2024 3:17 AM, Mikko wrote:
>> On 2024-08-14 00:52:36 +0000, olcott said:
>> 
>>> void DDD()
>>> {
>>>    HHH(DDD);
>>>    return;
>>> }
>> 
>> In order to prove that the above specifies a non-halting behavour
>> you must prove that HHH(DDD) does not terminate.
> 
> Wrong.

At least the proof that DDD does not terminate also proves as an
intermedate result or an obvious corollary that HHH does not halt.

Non-halting means that an infinite number of instructions can be
executed without halting. That means that at least one instruction
is executed infinitely many times as there are only finitely many
instructions. But not instrunctions of DDD outside HHH is executed
infinitely many times.

-- 
Mikko