Path: ...!2.eu.feeder.erje.net!feeder.erje.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: Sat, 15 Jun 2024 08:24:45 -0500 Organization: A noiseless patient Spider Lines: 65 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Sat, 15 Jun 2024 15:24:45 +0200 (CEST) Injection-Info: dont-email.me; posting-host="020d44455d70acf7231aebb6a85d124b"; logging-data="3661662"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18YPh/cUjv7en9A0bQ6+lSP" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:/YqICFubdiOpFMXO2N12FL3yjRc= In-Reply-To: Content-Language: en-US Bytes: 4840 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: 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. > but a termination > analyzer takes only the dexcription of a Turing machine (or other program) > and attempts to determine whether that machine halts with every input. > The term "analyzer" instead "decider" indicates that it may fail to > determine on some inputs Yes that is the distinction that I intend. > and that it may produce additional information > that may be useful. The intent is to create termination analyzers that > are useful for practical purposes. > -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer