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

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.

*symbolically executes the LLVM program* means dynamic behavior
and not static analysis.

It does not reproduce any specific example of the dynamic behaviour.
--
Mikko