Path: ...!weretis.net!feeder8.news.weretis.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: olcott Newsgroups: comp.theory Subject: Re: Categorically exhaustive reasoning applied to the decision to abort Date: Wed, 3 Apr 2024 09:53:14 -0500 Organization: A noiseless patient Spider Lines: 210 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 14:53:14 +0200 (CEST) Injection-Info: dont-email.me; posting-host="bfbe230f41d733c8e8d14e4fa12c421a"; logging-data="932"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19VUCrts7JBhwtz/dvFJZ0/" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:CxrahRYJ1rJif7TzB99I820juZI= Content-Language: en-US In-Reply-To: Bytes: 10918 On 4/3/2024 3:06 AM, Mikko wrote: > 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. ========== REMAINDER OF ARTICLE TRUNCATED ==========