Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: "Fred. Zwarts" Newsgroups: comp.theory Subject: Re: Deciders are ONLY accountable for their actual inputs --- Date: Mon, 3 Jun 2024 22:15:56 +0200 Organization: A noiseless patient Spider Lines: 156 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Mon, 03 Jun 2024 22:15:57 +0200 (CEST) Injection-Info: dont-email.me; posting-host="4aa76005a7c4778429e99a66774e7ab2"; logging-data="36249"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18eUMbnBN7lceh6roUQ+Zl8" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:eBY8VfifUq/+4B6Q8xZ7v+u7UHk= Content-Language: en-GB In-Reply-To: Bytes: 7747 Op 03.jun.2024 om 14:52 schreef olcott: > On 6/3/2024 3:35 AM, Mikko wrote: >> On 2024-06-02 13:46:30 +0000, olcott said: >> >>> On 6/2/2024 2:56 AM, Mikko wrote: >>>> On 2024-06-01 14:44:50 +0000, olcott said: >>>> >>>>> On 6/1/2024 2:56 AM, Mikko wrote: >>>>>> On 2024-05-31 14:25:40 +0000, olcott said: >>>>>> >>>>>>> On 5/31/2024 2:50 AM, Fred. Zwarts wrote: >>>>>>>> Op 31.mei.2024 om 00:01 schreef olcott: >>>>>>>>> On 5/30/2024 4:54 PM, joes wrote: >>>>>>>>>> Am Thu, 30 May 2024 09:55:24 -0500 schrieb olcott: >>>>>>>>>> >>>>>>>>>>> typedef int (*ptr)();  // ptr is pointer to int function in C >>>>>>>>>>> 00       int H(ptr p, ptr i); >>>>>>>>>>> 01       int D(ptr p) >>>>>>>>>>> 02       { >>>>>>>>>>> 03         int Halt_Status = H(p, p); >>>>>>>>>>> 04         if (Halt_Status) >>>>>>>>>>> 05           HERE: goto HERE; >>>>>>>>>>> 06         return Halt_Status; >>>>>>>>>>> 07       } >>>>>>>>>>> 08 >>>>>>>>>>> 09       int main() >>>>>>>>>>> 10       { >>>>>>>>>>> 11         H(D,D); >>>>>>>>>>> 12         return 0; >>>>>>>>>>> 13       } >>>>>>>>>>> >>>>>>>>>>> The left hand-side are line numbers of correct C code. >>>>>>>>>>> This code does compile and does conform to c17. >>>>>>>>>>> >>>>>>>>>>> Everyone with sufficient knowledge of C can easily determine >>>>>>>>>>> that D >>>>>>>>>>> correctly emulated by any *pure function* H (using an x86 >>>>>>>>>>> emulator) >>>>>>>>>>> cannot possibly reach its own simulated final state at line >>>>>>>>>>> 06 and halt. >>>>>>>>>> Yeah, of course not, if H doesn’t halt. >>>>>>>>>> >>>>>>>>> >>>>>>>>> To actually understand my words (as in an actual honest dialogue) >>>>>>>>> you must pay careful attention to every single word. Maybe you >>>>>>>>> had no idea that *pure functions* must always halt. >>>>>>>>> >>>>>>>>> Or maybe you did not know that every computation that never >>>>>>>>> reaches >>>>>>>>> its own final state *DOES NOT HALT* even if it stops running >>>>>>>>> because >>>>>>>>> it is no longer simulated. >>>>>>>> >>>>>>>> Since the claim is that H is also a computation, it holds for H, >>>>>>>> as well. That means that H *DOES NOT HALT* even if it stops >>>>>>>> running because it is no longer simulated. >>>>>>>> >>>>>>> >>>>>>> *pure function H definitely halts you are confused* >>>>>> >>>>>> A pure function does not halt (in C that means that a pure function >>>>>> does not call exit). A pure function returns. >>>>>> >>>>> >>>>> When a pure function returns this is the equivalent of the theory >>>>> of computation halting. >>>> >>>> In ceratin sense, yes. But the term "pure function" is mainly used >>>> in a different context where the word "halting" has a more specific >>>> meaning. >>>> >>> >>> I need to maintain a constant mapping between theory of computation >>> terminology and software engineering terminology. >> >> You need to keep your own terminology consistent and well defined. >> If possible try to avoid terms that have different meanings in >> the two areas. >> >>> Computable Function(comp sci) Pure function(SE) >>> I want it to be easy for software engineers to understand my proof. >> >> If you want to write to software engineers you need to define all >> terms that are not software engneers terms or do not mean what >> they mean in oftware engineering or do not have the same meaning >> to all software engineers. Software engineers borrow terms from >> their application areas and tool providers which result term >> conflicts as application areas and tool providers are not the same >> for all software engineers. >> >>> Only software engineers will understand that DD correctly simulated >>> by HH had different behavior than DD(DD). Comp Sci people allow Comp Sci >>> dogma to overrule verified facts. >> >> A relevant dogma always overrides an irrelevant fact. >> > > Nothing can override any fact without lying. > >>> When I pinned Richard down on this he simply said that he does not >>> care that DD correctly simulated by HH has different behavior than >>> DD(DD). >> >> Those behaviour are obiously different as only the latter has >> a specified input. But why would anybody care? >> > > The input to HH(DD,DD) specifies non-halting behavior. > You can lie about it what you can't do is show that it is not true. > >>> It turns out that DD correctly simulated by HH the behavior that >>> the input to HH(DD,DD) specifies. Deciders are ONLY accountable for >>> their actual inputs. Deciders compute the mapping FROM THEIR INPUTS... >> >> It does not turn out. Input does not specify. Problem statements specify. >> Specifications and contracts specify or at least try to specify. Inputs >> are something that can mentioned and considered in specifications. >> > > DD correctly emulated by any HH that can possibly exist DOES NOT HALT > DD correctly emulated by any HH that can possibly exist DOES NOT HALT > DD correctly emulated by any HH that can possibly exist DOES NOT HALT Only because *HH* emulated by any HH that can possibly exist DOES NOT HALT > > typedef int (*ptr)();  // ptr is pointer to int function in C > 00       int HH(ptr p, ptr i); > 01       int DD(ptr p) > 02       { > 03         int Halt_Status = HH(p, p); > 04         if (Halt_Status) > 05           HERE: goto HERE; > 06         return Halt_Status; > 07       } > > _DD() > [00001c22] 55         push ebp > [00001c23] 8bec       mov ebp,esp > [00001c25] 51         push ecx > [00001c26] 8b4508     mov eax,[ebp+08] > [00001c29] 50         push eax        ; push DD 1c22 > [00001c2a] 8b4d08     mov ecx,[ebp+08] > [00001c2d] 51         push ecx        ; push DD 1c22 > [00001c2e] e80ff7ffff call 00001342   ; call HH > [00001c33] 83c408     add esp,+08 > [00001c36] 8945fc     mov [ebp-04],eax > [00001c39] 837dfc00   cmp dword [ebp-04],+00 > [00001c3d] 7402       jz 00001c41 > [00001c3f] ebfe       jmp 00001c3f > [00001c41] 8b45fc     mov eax,[ebp-04] > [00001c44] 8be5       mov esp,ebp > [00001c46] 5d         pop ebp > [00001c47] c3         ret > Size in bytes:(0038) [00001c47] >