Path: ...!npeer.as286.net!npeer-ng0.as286.net!weretis.net!feeder8.news.weretis.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: olcott <polcott333@gmail.com>
Newsgroups: comp.theory
Subject: Re: H(D,D) cannot even be asked about the behavior of D(D)
Date: Mon, 17 Jun 2024 07:51:15 -0500
Organization: A noiseless patient Spider
Lines: 85
Message-ID: <v4pbg4$ln46$1@dont-email.me>
References: <v45tec$4q15$1@dont-email.me> <v4d991$3qbnc$1@i2pn2.org>
 <v4da12$1sioe$1@dont-email.me> <v4dbmf$3qbnc$3@i2pn2.org>
 <v4dcd6$1sioe$3@dont-email.me> <v4df0h$3qbnd$1@i2pn2.org>
 <v4dhf5$1tsdf$2@dont-email.me> <v4dja1$3qbnd$5@i2pn2.org>
 <v4djhf$1tsdf$6@dont-email.me> <v4dk7b$3qbnc$8@i2pn2.org>
 <v4dl3b$225kb$1@dont-email.me> <v4dn5u$3qbnd$8@i2pn2.org>
 <v4dop4$22o4a$2@dont-email.me> <v4dq07$3qbnc$12@i2pn2.org>
 <v4dqq0$2353n$1@dont-email.me> <v4el9m$3rsd6$3@i2pn2.org>
 <v4f3ec$2akmh$2@dont-email.me> <v4g65a$3tn6q$1@i2pn2.org>
 <v4g6vr$2ic0g$1@dont-email.me> <v4gc0b$3tn6r$6@i2pn2.org>
 <v4gcjc$2msea$1@dont-email.me> <v4geab$3tn6r$8@i2pn2.org>
 <v4gg0s$2nim8$2@dont-email.me> <v4ha63$3v16r$2@i2pn2.org>
 <v4hfq9$2sdqr$5@dont-email.me> <v4hp3r$3viml$1@i2pn2.org>
 <v4hv85$3021v$1@dont-email.me> <v4ju8f$222a$1@i2pn2.org>
 <v4k1m4$3f99u$1@dont-email.me> <v4k4mt$3fnqu$1@dont-email.me>
 <v4maeo$3vv3f$1@dont-email.me> <v4mnim$1qt6$6@dont-email.me>
 <v4onga$hjo3$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 17 Jun 2024 14:51:16 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="24f2a1964fe8769a85c52084edf5324e";
	logging-data="711814"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18GGmxZIg9TUzC9BR7b/1nl"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:H3YcGpaLS8YfQ9+yA/pmCRzYsIg=
In-Reply-To: <v4onga$hjo3$3@dont-email.me>
Content-Language: en-US
Bytes: 5598

On 6/17/2024 2:10 AM, Mikko wrote:
> On 2024-06-16 12:59:02 +0000, olcott said:
> 
>> On 6/16/2024 4:15 AM, Mikko wrote:
>>> On 2024-06-15 13:24:45 +0000, olcott said:
>>>
>>>> On 6/15/2024 7:33 AM, Mikko wrote:
>>>>> On 2024-06-15 11:34:39 +0000, joes said:
>>>>>
>>>>>> Am Fri, 14 Jun 2024 12:39:15 -0500 schrieb olcott:
>>>>>>> On 6/14/2024 10:54 AM, joes wrote:
>>>>>>>> Am Fri, 14 Jun 2024 08:15:52 -0500 schrieb olcott:
>>>>>>>>> On 6/14/2024 6:39 AM, Richard Damon wrote:
>>>>>>>>>> On 6/14/24 12:13 AM, olcott wrote:
>>>>>>>>>>> On 6/13/2024 10:44 PM, Richard Damon wrote:
>>>>>>>>>>>> On 6/13/24 11:14 PM, olcott wrote:
>>>>>>>>>>>>> On 6/13/2024 10:04 PM, Richard Damon wrote:
>>>>>>>>>>>>>> On 6/13/24 9:39 PM, olcott wrote:
>>>>>>>>>>>>>>> On 6/13/2024 8:24 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>> On 6/13/24 11:32 AM, olcott wrote:
>>>>>>
>>>>>>>>> When H and D have a pathological relationship to each other then
>>>>>>>>> H(D,D) is not being asked about the behavior of D(D). H1(D,D) 
>>>>>>>>> has no
>>>>>>>>> such pathological relationship thus D correctly simulated by H1 
>>>>>>>>> is the
>>>>>>>>> behavior of D(D).
>>>>>> What is H1 asked?
>>>>>>>> H is asked whether its input halts, and by definition should 
>>>>>>>> give the
>>>>>>>> (right) answer for every input.
>>>>>>> If we used that definition of decider then no human ever decided
>>>>>>> anything because every human has made at least one mistake.
>>>>>> Yes. Humans are not machines.
>>>>>>> I use the term "termination analyzer" as a close fit. The term 
>>>>>>> partial
>>>>>>> halt decider is more accurate yet confuses most people.
>>>>>
>>>>> Olcott has used the term "termination analyzer", though whether he 
>>>>> knows
>>>>> what it means is unclear.
>>>>>
>>>>
>>>> To prove (non-)termination of a C program, AProVE uses the Clang 
>>>> compiler [7] to translate it to the intermediate representation of 
>>>> the LLVM framework [15]. Then AProVE symbolically executes the LLVM 
>>>> program and uses abstraction to obtain a finite symbolic execution 
>>>> graph (SEG) containing all possible program runs.
>>>
>>> AProVE is a particular attempt, not a defintion.
>>>
>>
>> If you say: What is a duck? and I point to a duck that
>> *is* what a duck is.
> 
> That would be just an example, not a definition. In particular, it does
> not tell about another being whether it can be called a "duck".
> 
>> *Termination analysis*
>> In computer science, termination analysis is program analysis which
>> attempts to determine whether the evaluation of a given program halts
>> for each input. This means to determine whether the input program
>> computes a total function.
>> https://en.wikipedia.org/wiki/Termination_analysis
>>
>> I pointed out AProVE because it is essentially a simulating
>> halt decider with a limited domain.
> 
> A difference between AProVE and a partial halt decider is that the input
> to AProVE is only a program but not an input to that program but the
> input to a partial halt decider contains both.
> 
>>>> *AProVE: Non-Termination Witnesses for C Programs*
>>>> https://link.springer.com/content/pdf/10.1007/978-3-030-99527-0_21.pdf
> 

AProVE is a kind of simulating termination analyzer.
H is a kind of simulating halt decider with a restricted domain.
[Simulating termination analyzers for dummies] makes these ideas
simpler.

-- 
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer