Deutsch English Français Italiano |
<v4sd35$1eb2f$5@dont-email.me> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!npeer.as286.net!npeer-ng0.as286.net!3.eu.feeder.erje.net!feeder.erje.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: Tue, 18 Jun 2024 11:36:53 -0500 Organization: A noiseless patient Spider Lines: 131 Message-ID: <v4sd35$1eb2f$5@dont-email.me> References: <v45tec$4q15$1@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> <v4pbg4$ln46$1@dont-email.me> <v4rdtp$18al3$1@dont-email.me> <v4rvil$1boeu$2@dont-email.me> <v4s9hj$1dnm7$1@dont-email.me> <v4sa0h$1dk9i$3@dont-email.me> <v4sci6$1ebce$1@dont-email.me> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Tue, 18 Jun 2024 18:36:54 +0200 (CEST) Injection-Info: dont-email.me; posting-host="817dd47f58e869d78494e0bf13c00909"; logging-data="1518671"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18kNTSWct94LSR6Iri2Vq7G" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:3Hyan9yVPsbnXdeayCkY6m+uE00= Content-Language: en-US In-Reply-To: <v4sci6$1ebce$1@dont-email.me> Bytes: 7418 On 6/18/2024 11:27 AM, Mikko wrote: > On 2024-06-18 15:44:16 +0000, olcott said: > >> On 6/18/2024 10:36 AM, Mikko wrote: >>> 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. >>> >> >> So maybe: *symbolically executes the LLVM program* >> means jumping up and down yelling and screaming? > > Not a bad guess but not quite right either. > >> AProVE does form its non-halting decision on the basis of the >> dynamic behavior of its input instead of any static analysis. > > It is a kind of static analysis. The important diffrence is that > in a simulation there would be a specific input but AProVE considers > all possible inputs at the same time. > None-the-less it does derive the directly graph of all control flows on the basis of *symbolically executes the LLVM program* >> *symbolically executes the LLVM program* means dynamic behavior >> and not static analysis. > > It does not reproduce any specific example of the dynamic behaviour. > -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer