Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: H(D,D) cannot even be asked about the behavior of D(D)
Date: Wed, 19 Jun 2024 11:07:15 +0300
Organization: -
Lines: 117
Message-ID: <v4u3jl$1se49$1@dont-email.me>
References: <v45tec$4q15$1@dont-email.me> <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> <v4mnim$1qt6$6@dont-email.me> <v4onga$hjo3$3@dont-email.me> <v4pbg4$ln46$1@dont-email.me> <v4rdtp$18al3$1@dont-email.me> <v4rvil$1boeu$2@dont-email.me> <v4s9hj$1dnm7$1@dont-email.me> <v4sa0h$1dk9i$3@dont-email.me> <v4sci6$1ebce$1@dont-email.me> <v4sd35$1eb2f$5@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 19 Jun 2024 10:07:17 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="d425795ad419ff3204bb64ae5eb2f5d4";
	logging-data="1980553"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+QNigekRMjKyLgxljugh2/"
User-Agent: Unison/2.2
Cancel-Lock: sha1:heY84Nn9JzHfVix365HFpkHUoVw=
Bytes: 7054

On 2024-06-18 16:36:53 +0000, olcott said:

> On 6/18/2024 11:27 AM, Mikko wrote:
>> On 2024-06-18 15:44:16 +0000, olcott said:
>> 
>>> On 6/18/2024 10:36 AM, Mikko wrote:
>>>> On 2024-06-18 12:46:13 +0000, olcott said:
>>>> 
>>>>> On 6/18/2024 2:44 AM, Mikko wrote:
>>>>>> On 2024-06-17 12:51:15 +0000, olcott said:
>>>>>> 
>>>>>>> On 6/17/2024 2:10 AM, Mikko wrote:
>>>>>>>> On 2024-06-16 12:59:02 +0000, olcott said:
>>>>>>>> 
>>>>>>>>> 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.
>>>>>>>> 
>>>>>>>> That would be just an example, not a definition. In particular, it does
>>>>>>>> not tell about another being whether it can be called a "duck".
>>>>>>>> 
>>>>>>>>> *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.
>>>>>>>> 
>>>>>>>> A difference between AProVE and a partial halt decider is that the input
>>>>>>>> to AProVE is only a program but not an input to that program but the
>>>>>>>> input to a partial halt decider contains both.
>>>>>>>> 
>>>>>>>>>>> *AProVE: Non-Termination Witnesses for C Programs*
>>>>>>>>>>> https://link.springer.com/content/pdf/10.1007/978-3-030-99527-0_21.pdf
>>>>>>>> 
>>>>>>> 
>>>>>>> AProVE is a kind of simulating termination analyzer.
>>>>>> 
>>>>>> Not really. It does not simulate.
>>>>>> 
>>>>> 
>>>>> 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*
>>>> 
>>>> I.e., does not simulate.
>>>> 
>>> 
>>> So maybe: *symbolically executes the LLVM program*
>>> means jumping up and down yelling and screaming?
>> 
>> Not a bad guess but not quite right either.
>> 
>>> AProVE does form its non-halting decision on the basis of the
>>> dynamic behavior of its input instead of any static analysis.
>> 
>> It is a kind of static analysis. The important diffrence is that
>> in a simulation there would be a specific input but AProVE considers
>> all possible inputs at the same time.
>> 
> 
> None-the-less it does derive the directly graph of all
> control flows on the basis of
> *symbolically executes the LLVM program*

It is still unclear whether you know what "termination analyzer" means.
Which doesn't matter as nobody believes you anyway.

-- 
Mikko