Deutsch English Français Italiano |
<v4mnim$1qt6$6@dont-email.me> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!feeds.phibee-telecom.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: Sun, 16 Jun 2024 07:59:02 -0500 Organization: A noiseless patient Spider Lines: 79 Message-ID: <v4mnim$1qt6$6@dont-email.me> References: <v45tec$4q15$1@dont-email.me> <v4c12r$3oop0$3@i2pn2.org> <v4cjl7$1o4b4$1@dont-email.me> <v4d991$3qbnc$1@i2pn2.org> <v4da12$1sioe$1@dont-email.me> <v4dbmf$3qbnc$3@i2pn2.org> <v4dcd6$1sioe$3@dont-email.me> <v4df0h$3qbnd$1@i2pn2.org> <v4dhf5$1tsdf$2@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> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Sun, 16 Jun 2024 14:59:02 +0200 (CEST) Injection-Info: dont-email.me; posting-host="2f28c05d249972130f2ddc6107b08476"; logging-data="60326"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19uWWK5sE0XnEHHUHXYS5JS" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:sAIUHfsp6qcYP0AaxrYwk5XwlCQ= In-Reply-To: <v4maeo$3vv3f$1@dont-email.me> Content-Language: en-US Bytes: 5333 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. *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. >> *AProVE: Non-Termination Witnesses for C Programs* >> https://link.springer.com/content/pdf/10.1007/978-3-030-99527-0_21.pdf >> >>> The main difference is that a halt decider or partial halt decider takes >>> descriptions of both a Turing machine (or other program) and an input >>> and >>> determines whether that machine halts with that input >> >> H(D,D) is only required to get this one input correctly thus H is >> a halt decider with a domain restricted to D. > > Nevertheless, it takes both the program and its input inputs. > And both the program and its input proves that H(D,D) is not and cannot report on the behavior of the directly executed D(D). -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer