Re: H(D,D) cannot even be asked about the behavior of D(D)

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*

and uses abstraction to obtain a finite symbolic execution graph (SEG)
 

H is a kind of simulating halt decider with a restricted domain.
[Simulating termination analyzers for dummies] makes these ideas
simpler.