Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: Mikko Newsgroups: comp.theory Subject: Re: Categorically exhaustive reasoning applied to the decision to abort Date: Wed, 3 Apr 2024 11:06:41 +0300 Organization: - Lines: 178 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Wed, 03 Apr 2024 08:06:41 +0200 (CEST) Injection-Info: dont-email.me; posting-host="e095f4988d60901f7ed2cc6f78ba192d"; logging-data="4004801"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1869fGP9zM81AKzMMF+7Ipx" User-Agent: Unison/2.2 Cancel-Lock: sha1:D9mEhUAaVrB7G5wnPEklUroYfkQ= Bytes: 9794 On 2024-04-02 14:38:16 +0000, olcott said: > On 4/2/2024 3:00 AM, Mikko wrote: >> On 2024-04-01 14:52:57 +0000, olcott said: >> >>> On 4/1/2024 3:15 AM, Mikko wrote: >>>> On 2024-03-31 16:29:06 +0000, olcott said: >>>> >>>>> On 3/31/2024 11:17 AM, olcott wrote: >>>>>> On 3/31/2024 11:08 AM, Mikko wrote: >>>>>>> On 2024-03-31 14:25:37 +0000, olcott said: >>>>>>> >>>>>>>> On 3/31/2024 4:04 AM, Mikko wrote: >>>>>>>>> On 2024-03-30 13:45:03 +0000, olcott said: >>>>>>>>> >>>>>>>>>> On 3/30/2024 2:09 AM, Mikko wrote: >>>>>>>>>>> On 2024-03-29 14:26:50 +0000, olcott said: >>>>>>>>>>> >>>>>>>>>>>> On 3/29/2024 6:10 AM, Mikko wrote: >>>>>>>>>>>>> On 2024-03-28 15:38:08 +0000, olcott said: >>>>>>>>>>>>> >>>>>>>>>>>>>> On 3/28/2024 9:44 AM, Mikko wrote: >>>>>>>>>>>>>>> On 2024-03-27 14:04:17 +0000, olcott said: >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> On 3/27/2024 4:32 AM, Mikko wrote: >>>>>>>>>>>>>>>>> On 2024-03-26 14:41:08 +0000, olcott said: >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> On 3/26/2024 3:50 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>> On 2024-03-25 22:52:18 +0000, olcott said: >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> On 3/24/2024 9:27 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>> On 2024-03-24 02:11:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> On 3/23/2024 7:31 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>> On 3/23/24 7:29 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 3/23/2024 5:58 PM, immibis wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 23/03/24 16:02, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> (b) H(D,D) that DOES abort its simulation is correct >>>>>>>>>>>>>>>>>>>>>>>>>>      (ABOUT THIS ABORT DECISION) >>>>>>>>>>>>>>>>>>>>>>>>>>      because it would halt and all deciders must always halt. >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> To be a decider it has to give an answer. >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> To be a halt decider it has to give an answer that is the same as >>>>>>>>>>>>>>>>>>>>>>>>> whether the direct execution of its input would halt. >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> That would entail that H must report on different behavior >>>>>>>>>>>>>>>>>>>>>>>> than the behavior that H actually sees thus violate the >>>>>>>>>>>>>>>>>>>>>>>> definition of a decider that must compute the mapping from >>>>>>>>>>>>>>>>>>>>>>>> its inputs... >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> Nope. >>>>>>>>>>>>>>>>>>>>>>> You are just showing yourself to be a stupid liar. >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> Where in the DEFINITION of Compute the Mapping of the Input to the >>>>>>>>>>>>>>>>>>>>>>> Mapped Output does it say that the decider has to be able to "see" that >>>>>>>>>>>>>>>>>>>>>>> property of the input? >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> In order to compute the mapping from an input there must be >>>>>>>>>>>>>>>>>>>>>> some basis that is directly provided by this input. >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> If no such basis is in the input the problem has no soution. >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> int sum(int x, int y){ return x + y; } >>>>>>>>>>>>>>>>>>>> sum(3,4) is not allowed to report on the sum of 5 + 6 >>>>>>>>>>>>>>>>>>>> even if you really really believe that it should. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> Your and my beliefs don't matter. Testers call the function with >>>>>>>>>>>>>>>>>>> various pairs of inputs and compare the result to the specification. >>>>>>>>>>>>>>>>>>> If the result is not what the specification requires then the function >>>>>>>>>>>>>>>>>>> is wrong and needs be fixed or rejected. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> There is enough information for sum(3,4) to compute the sum of 3+4. >>>>>>>>>>>>>>>>>> There is NOT enough information for sum(3,4) to compute the sum of 5+6. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> There is enough information for H1(D,D) to compute Halts(D,D). >>>>>>>>>>>>>>>>>> There is NOT enough information for H(D,D) to compute Halts(D,D). >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> There is enough information to determine whether the result is as >>>>>>>>>>>>>>>>> required by the specification. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> This specification only requires a mapping from H(D,D) >>>>>>>>>>>>>>>> to Halts(Simulated_by_H(D,D)) and it gets that one correctly. >>>>>>>>>>>>>>>> D(D) does not halt from the POV of H. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> What "this pecification"? This means the one you refer or point to >>>>>>>>>>>>>>> but you didn't. >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> Every implementation of H(D,D) that simulates its input must abort >>>>>>>>>>>>>> this simulation or never itself halt. >>>>>>>>>>>>>> >>>>>>>>>>>>>> int main() { D(D); }   is not a D simulated by H. >>>>>>>>>>>>>> int main() { H(D,D); } is a D simulated by H. >>>>>>>>>>>>> >>>>>>>>>>>>> Does not answer what "this specification" means above. >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> *THIS SPECIFICATION* >>>>>>>>>>>> Every implementation of H(D,D) that simulates its input must abort >>>>>>>>>>>> this simulation or never itself halt. >>>>>>>>>>> >>>>>>>>>>> Are you sure you want to allow that H(D,D) may run un a loop and never >>>>>>>>>>> halt and never continue the simulation? >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> So you didn't understand the: *must abort this simulation* part ? >>>>>>>>> >>>>>>>>> I did. I asked whether whether you really mean all that "never iself >>>>>>>>> halt" means. >>>>>>>>> >>>>>>>> >>>>>>>> 01 void D(ptr x) // ptr is pointer to void function >>>>>>>> 02 { >>>>>>>> 03   H(x, x); >>>>>>>> 04   return; >>>>>>>> 05 } >>>>>>>> 06 >>>>>>>> 07 void main() >>>>>>>> 08 { >>>>>>>> 09   H(D,D); >>>>>>>> 10 } >>>>>>>> >>>>>>>> *Execution Trace* >>>>>>>> Line 09: main() invokes H(D,D); >>>>>>>> >>>>>>>> *keeps repeating* (unless aborted) >>>>>>>> Line 03: simulated D(D) invokes simulated H(D,D) that simulates D(D) >>>>>>>> >>>>>>>> *Simulation invariant* >>>>>>>> D correctly simulated by H cannot possibly reach past its own line 03. >>>>>>>> >>>>>>>> As soon as line 03 would be simulated  H sees that D would call >>>>>>>> itself with its same input, then H aborts D. >>>>>>> >>>>>>> Looks like you don't know whether you really want to allow that H(D,D) >>>>>>> may run in a loop and never halt and never continue the simulation. >>>>>>> >>>>>> >>>>>> H(D,D) must halt or it cannot be any kind of decider. My other >>>>>> reviewers consistently and perpetually lie about whether or >>>>>> not H(D,D) is correct to abort its simulation. >>>>>> >>>>> >>>>> When I refer to H I am referring to every element of the set of >>>>> implementations H that simulate their input. >>>> >>>> I.e., every element of the set on implementations of oevery element >>>> of the sent of implementataions of .... >>>> >>> >>> Every element of the set of implementations of H(D,D) that simulates its >>> input either aborts this simulation or is wrong. >>> >>> It also must be the first directly executed element that performs >>> the abort or none of them do because all of the H elements in a >>> recursive simulation chain have the exact same machine code. >> >> You seem to agree that "this pecification" is nomen nuduum. > nomen nudum: a proposed taxonomic name that is invalid because > the group designated is not described or illustrated sufficiently > for recognition... > https://www.merriam-webster.com/dictionary/nomen%20nudum The formal definitions are for taxonomists and outside these areas the term is rarely used. However, the phenomenon is more general: people sometimes say something that does not mean anything, either because they forget to define or in order to deceive. -- Mikko