Path: ...!feeds.phibee-telecom.net!news.mixmin.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: Sun, 16 Jun 2024 12:15:04 +0300 Organization: - Lines: 57 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Sun, 16 Jun 2024 11:15:04 +0200 (CEST) Injection-Info: dont-email.me; posting-host="265fa7fef37a78527295c06fc878f4cf"; logging-data="4193391"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/AKJQX/iFxIAgHhHB8Eyvd" User-Agent: Unison/2.2 Cancel-Lock: sha1:BeDmnHzfbmw42bj5fzu3rsaHCgs= Bytes: 4321 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. > *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. -- Mikko