Path: ...!3.eu.feeder.erje.net!feeder.erje.net!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: Sun, 31 Mar 2024 12:04:03 +0300
Organization: -
Lines: 106
Message-ID: <uub8u3$1k9b3$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 31 Mar 2024 09:04:03 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="9512f205df1ed007a04f4b5f52c0d4cb";
	logging-data="1713507"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18yQX9O7YGDNx/ZsN/ieUpr"
User-Agent: Unison/2.2
Cancel-Lock: sha1:IGaX76AdE3du7Y0MDFn90Rk0prM=
Bytes: 5911

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.

-- 
Mikko