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 Newsgroups: comp.theory Subject: Re: H(D,D) cannot even be asked about the behavior of D(D) Date: Tue, 18 Jun 2024 18:36:19 +0300 Organization: - Lines: 96 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Tue, 18 Jun 2024 17:36:19 +0200 (CEST) Injection-Info: dont-email.me; posting-host="c2afa6234aeec1e0d396e626c474e4c1"; logging-data="1498823"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/reZ/dASEncPiMwNEuGQGJ" User-Agent: Unison/2.2 Cancel-Lock: sha1:KSSnAzWj/uVk5p1IdWaX9V2QEBw= Bytes: 6014 On 2024-06-18 12:46:13 +0000, olcott said: > 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* I.e., does not simulate. > 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. -- Mikko