Forums before death by AOL, social media and spammers... "We can't have nice things"
|    sci.logic    |    Logic -- math, philosophy & computationa    |    262,912 messages    |
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
|    Message 262,791 of 262,912    |
|    olcott to All    |
|    Re: Proof theoretic semantics based halt    |
|    04 Feb 26 16:15:42    |
   
   XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: sci.lang, comp.software-eng   
   From: polcott333@gmail.com   
      
   On 2/4/2026 2:41 PM, dart200 wrote:   
   > On 2/1/26 9:35 AM, olcott wrote:   
   >> On 2/1/2026 6:11 AM, Richard Damon wrote:   
   >>> On 1/31/26 12:49 PM, olcott wrote:   
   >>>> Source code of fully operational system   
   >>>> https://github.com/plolcott/x86utm/blob/master/Halt7.c   
   >>>>   
   >>>> int DD()   
   >>>> {   
   >>>> int Halt_Status = HHH(DD);   
   >>>> if (Halt_Status)   
   >>>> HERE: goto HERE;   
   >>>> return Halt_Status;   
   >>>> }   
   >>>>   
   >>>> HHH simulates DD step-by-step according to   
   >>>> the semantics of the C programming language.   
   >>>   
   >>> IT CAN'T, as you have been told, as your above program, without the C   
   >>> CODE for HHH, has undefined behavior by the semantics of the C   
   >>> programming language.   
   >>>   
   >   
   > HHH as executed by polcott is exhibiting a classifier interface i'm   
   > calling a *partial recognizer*   
   >   
   > (machine) -> {   
   > TRUE iff machine HALTS and DECIDABLE,   
   > FALSE iff machine LOOPS or UNDECIDABLE,   
   > }   
   >   
   > it doesn't do so quite so intelligently, but HHH(DD) needs to return   
   > FALSE because DD is an UNDECIDABLE input to HHH   
   >   
   > polcott does this by detecting the infinite recursion and returning   
   > FALSE because of that   
   >   
   > this approach of returning FALSE upon encountering an infinite recursion   
   > on self (which i believe all paradoxes will involve) will either be   
   > accurate or inaccurate in regards to actually halting/not... but it   
   > doesn't matter because returning FALSE for halting yet UNDECIDABLE input   
   > is acceptable for a *partial recognizer*   
   >   
   > where this wouldn't work is:   
   >   
   > int ND()   
   > {   
   > int Halt_Status = HHH(ND);   
   > return Halt_Status;   
   > }   
   >   
   > HHH(ND) -> FALSE because HHH(ND) will recognize the infinite recursion   
   > and return FALSE ... but that's not an acceptable response for a   
   > *partial recognizer* for ND because ND is not an UNDECIDABLE input, and   
   > it clearly should HALT   
   >   
   > sorry polcott   
   >   
      
   That is merely a text message that has not been updated.   
      
   See my other post:   
   When halt provers are allowed to reject bad   
   inputs the remaining domain is decidable   
      
   A bad input is any input that does not have   
   *a well-founded justification tree within Proof*   
   *theoretic semantics*   
      
   For a simulating halt prover as soon as it detects   
   that its simulated input cannot possibly reach its   
   own simulated final halt state for any reason   
   what-so-ever then this input
|
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
(c) 1994, bbs@darkrealms.ca