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

Liste des GroupesRevenir à c theory 
Sujet : Re: H(D,D) cannot even be asked about the behavior of D(D)
De : mikko.levanto (at) *nospam* iki.fi (Mikko)
Groupes : comp.theory
Date : 16. Jun 2024, 10:15:04
Autres entêtes
Organisation : -
Message-ID : <v4maeo$3vv3f$1@dont-email.me>
References : 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
User-Agent : Unison/2.2
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.

*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.
Nevertheless, it takes both the program and its input inputs.
--
Mikko

Date Sujet#  Auteur
26 Apr 25 o 

Haut de la page

Les messages affichés proviennent d'usenet.

NewsPortal