Path: ...!news.misty.com!weretis.net!feeder9.news.weretis.net!i2pn.org!i2pn2.org!.POSTED!not-for-mail
From: Richard Damon <richard@damon-family.org>
Newsgroups: comp.theory
Subject: Re: H(D,D) cannot even be asked about the behavior of D(D)
Date: Sat, 15 Jun 2024 09:51:55 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <v4k69r$2218$5@i2pn2.org>
References: <v45tec$4q15$1@dont-email.me> <v4b50m$1f89t$5@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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 15 Jun 2024 13:51:55 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="67624"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
X-Spam-Checker-Version: SpamAssassin 4.0.0
Content-Language: en-US
In-Reply-To: <v4k4mt$3fnqu$1@dont-email.me>
Bytes: 5062
Lines: 75

On 6/15/24 9:24 AM, olcott wrote:
> 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.
> 

And since it gets the one answer it is resposible for wrong, it fails.

Since H(D,D) returns 0, it can be proven that D(D) will halt, which *IS* 
the behavior a "Halt Decider" (even a limited halt decider) is 
responsible for answering about, so H(D,D) is just WRONG.


>> 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.

But it fails on the one machine you want it to answer about.

> 
>> and that it may produce additional information
>> that may be useful. The intent is to create termination analyzers that
>> are useful for practical purposes.
>>
>