| Deutsch English Français Italiano |
|
<v50d8k$2e51s$1@dont-email.me> View for Bookmarking (what is this?) Look up another Usenet article |
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 <mikko.levanto@iki.fi> Newsgroups: comp.theory Subject: Re: H(D,D) cannot even be asked about the behavior of D(D) Date: Thu, 20 Jun 2024 08:04:20 +0300 Organization: - Lines: 145 Message-ID: <v50d8k$2e51s$1@dont-email.me> References: <v45tec$4q15$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> <v4sd35$1eb2f$5@dont-email.me> <v4u3jl$1se49$1@dont-email.me> <v4umvh$1vpm0$7@dont-email.me> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Thu, 20 Jun 2024 07:04:21 +0200 (CEST) Injection-Info: dont-email.me; posting-host="f2c5be32a8e18ed9d3dcb1608f59dff0"; logging-data="2561084"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/IDpJQFfjluRoRUa21ACPc" User-Agent: Unison/2.2 Cancel-Lock: sha1:K7chYmYPJJHGeQoImFhjD++u7YQ= Bytes: 8214 On 2024-06-19 13:37:53 +0000, olcott said: > On 6/19/2024 3:07 AM, Mikko wrote: >> On 2024-06-18 16:36:53 +0000, olcott said: >> >>> 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* >> >> It is still unclear whether you know what "termination analyzer" means. >> Which doesn't matter as nobody believes you anyway. >> > > It is dishonest to dismiss my reasoning out-of-hand without > finding an actual error. So many of your errors have been found and analyzed that one more or less makes no difference. > For my first three examples that have no input H0 is a termination > analyzer. Sitll inclear whether you know what "termination analyzer" means. > For my next example that has an input there is no existing > term of the art that exactly fits besides halt decider with a limited > domain or partial halt decider. The latter is better. > This is too confusing to my software engineer reviewers. The cause of confusion is that you use common words in a way that is not compatible with their common meanings. If one cannot trust that you know what your words mean one cannot understand what you are trying to say. -- Mikko