Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail From: dbush Newsgroups: comp.lang.c Subject: Re: Proving the: Simulating termination analyzer Principle Date: Sat, 5 Apr 2025 19:20:55 -0400 Organization: A noiseless patient Spider Lines: 53 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Sun, 06 Apr 2025 01:20:54 +0200 (CEST) Injection-Info: dont-email.me; posting-host="bdf677863da665303917a0e1a85da663"; logging-data="3417512"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/TGhefrh3n3fwhwPtpP5MU" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:vLNJ6UZuXqYDFms6m6U1DbUYVa4= Content-Language: en-US In-Reply-To: Bytes: 2881 On 4/5/2025 7:18 PM, olcott wrote: > On 4/5/2025 5:18 PM, Richard Heathfield wrote: >> On 05/04/2025 22:31, dbush wrote: >>> On 4/5/2025 5:29 PM, olcott wrote: >>>> On 4/5/2025 4:15 PM, dbush wrote: >>>>> On 4/5/2025 4:52 PM, olcott wrote: >>>>>> *Simulating termination analyzer Principle* >>>>>> It is always correct for any simulating termination >>>>>> analyzer to stop simulating and reject any input that >>>>>> would otherwise prevent its own termination. >>>>>> >>>>>> void DDD() >>>>>> { >>>>>>     HHH(DDD); >>>>>>     return; >>>>>> } >>>>> >>>>> Except when doing so would change the input, as is the case with >>>>> HHH and DDD. >>>>> >>>>> Changing the input is not allowed. >>>> >>>> You may disagree that the above definition >>>> of simulating termination analyzer is correct. >>>> >>>> It is self-evident that HHH must stop simulating >>>> DDD to prevent its own non-termination. >>>> >>> >>> Changing the input is not allowed. >> >> You're right, but it doesn't matter very much as long as terminates() >> *always* gets the answer right for any arbitrary program tape and any >> data tape. Mr Olcott's fails to do that. >> > > Termination analyzers are not required to be infallible. > But they must still generate the required mapping for the input they claim to answer correctly: Given any algorithm (i.e. a fixed immutable sequence of instructions) X described as with input Y: A solution to the halting problem is an algorithm H that computes the following mapping: (,Y) maps to 1 if and only if X(Y) halts when executed directly (,Y) maps to 0 if and only if X(Y) does not halt when executed directly