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: H(D,D) cannot even be asked about the behavior of D(D) Date: Tue, 18 Jun 2024 07:46:13 -0500 Organization: A noiseless patient Spider Lines: 98 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Tue, 18 Jun 2024 14:46:14 +0200 (CEST) Injection-Info: dont-email.me; posting-host="817dd47f58e869d78494e0bf13c00909"; logging-data="1434078"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+sO/Qjr77IoshhjRmiDTLv" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:1T4g0m2BHFOkSHEQKezwjRwQRLo= Content-Language: en-US In-Reply-To: Bytes: 6150 On 6/18/2024 2:44 AM, Mikko wrote: > On 2024-06-17 12:51:15 +0000, olcott said: > >> 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. > > Not really. It does not simulate. > 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) >> 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