Path: ...!2.eu.feeder.erje.net!feeder.erje.net!news.swapon.de!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: This function proves that only the outermost HHH examines the execution trace
Date: Tue, 30 Jul 2024 10:11:35 +0300
Organization: -
Lines: 56
Message-ID: <v8a3n7$ub6i$1@dont-email.me>
References: <v80h07$2su8m$3@dont-email.me> <v82bi4$39v6n$4@dont-email.me> <v82tr5$3dftr$2@dont-email.me> <v82vtl$3dq41$2@dont-email.me> <v830hg$3dftr$9@dont-email.me> <v83des$2nhr$1@news.muc.de> <v83dp3$3g9s7$1@dont-email.me> <v852m1$3sfas$1@dont-email.me> <v86loe$54o5$1@dont-email.me> <v87g9h$d073$1@dont-email.me> <v883of$g39i$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 30 Jul 2024 09:11:35 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="329af3d797696bf444d9a1dc8986292a";
	logging-data="994514"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18v1MS1QTCCiIOAH7VQTxPW"
User-Agent: Unison/2.2
Cancel-Lock: sha1:mDr7n39EqKYEpaduqwi8lxNivqc=
Bytes: 3528

On 2024-07-29 12:59:59 +0000, olcott said:

> On 7/29/2024 2:27 AM, Mikko wrote:
>> On 2024-07-28 23:54:54 +0000, olcott said:
>> 
>>> On 7/28/2024 4:23 AM, Mikko wrote:
>>>> On 2024-07-27 18:20:19 +0000, olcott said:
>>>> 
>>>>> On 7/27/2024 1:14 PM, Alan Mackenzie wrote:
>>>>>> olcott <polcott333@gmail.com> wrote:
>>>>>> 
>>>>>>> Stopping running is not the same as halting.
>>>>>>> DDD emulated by HHH stops running when its emulation has been aborted.
>>>>>>> This is not the same as reaching its ret instruction and terminating
>>>>>>> normally (AKA halting).
>>>>>> 
>>>>>> I think you're wrong, here.  All your C programs are a stand in for
>>>>>> turing machines.  A turing machine is either running or halted.  There is
>>>>>> no third state "aborted".
>>>>> 
>>>>> Until you take the conventional ideas of
>>>>> (a) UTM
>>>>> (b) TM Description
>>>>> (c) Decider
>>>>> and combine them together to become a simulating partial halt decider.
>>>> 
>>>> You also need the conventional ideas of halting and halt decider.
>>>> The latter is largely a combination of the conventional ideas of
>>>> decider and halting but also involves the conventional of
>>>> prediction, so you need that, too.
>>>> 
>>>> Although the conventional idea of testing is not relevant to the 
>>>> construction of a simulating partial halt decider it is helpful to 
>>>> presentation of the
>>>> result, especially if your target audience contains software engineers. 
>>>> If your target audience is mainly mathematicians the convnetional idea 
>>>> of proofs is more useful because in that case most of your presentation 
>>>> must be proofs.
>>> 
>>> My ideas must be anchored in fully specified running software
>>> otherwise the false assumptions made by computer science people
>>> remain hidden.
>> 
>> There is no "must" there. You may present your ideas whichever way you
>> think is the best for your purposes.
> 
> Even when I make my ideas 100% concrete people still deny
> the verified facts.

Perhaps you should add a pointer to the verification report when you
call smoething a "verified fact". Otherwise the lack of verification
of the verification is sufficient suspect your "verified facts".

-- 
Mikko