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 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: References: 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: 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