Path: ...!weretis.net!feeder9.news.weretis.net!2.eu.feeder.erje.net!feeder.erje.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: Sat, 17 Aug 2024 10:54:25 +0300
Organization: -
Lines: 61
Message-ID: <v9pkvh$1r81e$1@dont-email.me>
References: <v9gv4k$4sc4$1@dont-email.me> <v9hp66$ck4s$1@dont-email.me> <v9ia4j$f16v$1@dont-email.me> <v9kkso$u2rh$1@dont-email.me> <v9l6kj$10ae5$4@dont-email.me> <v9n430$1clc0$1@dont-email.me> <v9nhfe$1dvef$5@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 17 Aug 2024 09:54:25 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="129c142c9cce33919a33ea59b2adcd14";
	logging-data="1941550"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+LCp68EEeYv2a1vw+Hq5ww"
User-Agent: Unison/2.2
Cancel-Lock: sha1:7RhvamtmUCwL1VzzAFLr7lJmK0I=
Bytes: 3357

On 2024-08-16 12:42:22 +0000, olcott said:

> On 8/16/2024 3:53 AM, Mikko wrote:
>> On 2024-08-15 15:25:07 +0000, olcott said:
>> 
>>> On 8/15/2024 5:22 AM, Mikko wrote:
>>>> 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.
>>>> 
>>> 
>>> Wrong. Non-halting only means that when DDD is emulated
>>> according to the semantics of the x86 language and this
>>> emulation is unlimited that DDD would never reach its
>>> own "return" instruction.
>> 
>> If what I said is wrong then what you said is wrong, too,
>> as you say what I said.
>> 
> 
> *You are getting the computer science incorrectly*
> 
> On 8/2/2024 11:32 PM, Jeff Barnett wrote:
>  > ...In some formulations, there are specific states
>  >    defined as "halting states" and the machine only
>  >    halts if either the start state is a halt state...

These formulations have the problem that it is possible that
a computation reaches a state where the computation shall not
halt and cannot be continued. Therefore most authors prefer a
simpler formulation (introduced by Post) where halting simply
means impossibility to continue. For x86 processors the best
definition is that a computation halts when the SP register
gets a value that is greater than its value at the start of
the computation (in x86 processors the stack grows downwards
to smaller addresses).

-- 
Mikko