Path: ...!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: Categorically exhaustive reasoning applied to the decision to abort
Date: Wed, 3 Apr 2024 11:06:41 +0300
Organization: -
Lines: 178
Message-ID: <uuj2mh$3q6u1$1@dont-email.me>
References: <utlf69$39fl1$1@dont-email.me> <utlff5$3997r$3@dont-email.me> <utlgg1$2o1am$20@i2pn2.org> <utlirq$3dsl2$2@dont-email.me> <utmo5e$2plc2$8@i2pn2.org> <utmqu6$3msk5$1@dont-email.me> <utnmqm$3tjdn$1@dont-email.me> <utnoks$3ttm3$2@dont-email.me> <utns99$2rkld$3@i2pn2.org> <uto24n$3vtt8$2@dont-email.me> <utpd7m$dibu$1@dont-email.me> <utsv72$1bgkl$6@dont-email.me> <utu29i$1n8qn$1@dont-email.me> <utumq5$1rsiu$5@dont-email.me> <uu0p2r$2opup$1@dont-email.me> <uu1911$2seum$2@dont-email.me> <uu3vod$3krqk$1@dont-email.me> <uu42t0$3ldlj$3@dont-email.me> <uu67j1$8ksq$1@dont-email.me> <uu6j3a$b6gs$2@dont-email.me> <uu8dr3$rukj$1@dont-email.me> <uu950v$114hv$2@dont-email.me> <uub8u3$1k9b3$1@dont-email.me> <uubrp1$1r54k$1@dont-email.me> <uuc1pf$1skhe$1@dont-email.me> <uuc2as$1smok$1@dont-email.me> <uuc30i$1smok$2@dont-email.me> <uudqfu$2ckr5$1@dont-email.me> <uueho9$2hsd5$1@dont-email.me> <uugdun$339t7$1@dont-email.me> <uuh58o$38mcp$1@dont-email.me>
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