home bbs files messages ]

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,801 of 262,912   
   olcott to All   
   Re: Proof theoretic semantics based halt   
   04 Feb 26 21:04:43   
   
   XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: sci.lang, comp.software-eng   
   From: polcott333@gmail.com   
      
   On 2/4/2026 8:52 PM, dart200 wrote:   
   > On 2/4/26 6:50 PM, olcott wrote:   
   >> On 2/4/2026 8:42 PM, dart200 wrote:   
   >>> On 2/4/26 4:00 PM, olcott wrote:   
   >>>> On 2/4/2026 5:43 PM, dart200 wrote:   
   >>>>> On 2/4/26 2:27 PM, olcott wrote:   
   >>>>>> On 2/4/2026 4:19 PM, dart200 wrote:   
   >>>>>>> On 2/4/26 2:15 PM, olcott wrote:   
   >>>>>>>> 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  a bad input.   
   >>>>>>>>   
   >>>>>>>   
   >>>>>>> so ur just banning self-referential analysis?   
   >>>>>>>   
   >>>>>>   
   >>>>>> When we reject inputs not having   
   >>>>>> *a well-founded justification tree within Proof*   
   >>>>>> *theoretic semantics*   
   >>>>>>   
   >>>>>> Then undecidability utterly ceases to exist.   
   >>>>>   
   >>>>> i agree it's impossible to demonstrated undecidability without   
   >>>>> self- reference,   
   >>>>>   
   >>>>> and filtering out paradoxes is a path to turing complete and fully   
   >>>>> decidable subset of turing machines,   
   >>>>>   
   >>>>> but ND is a halting function, and i don't see a particular reason   
   >>>>> why a more intelligent HHH couldn't return that given a more in-   
   >>>>> depth analysis of how the self-reference interplays with the rest   
   >>>>> of the machine   
   >>>>>   
   >>>>   
   >>>> It cannot do that because that is not what it sees.   
   >>>   
   >>> once it sees the infinite recursion on itself ...   
   >>>   
   >>> why can't it do analysis on the effects of various possible return   
   >>> values for itself ... like what we do when we talk thru it?   
   >>>   
   >>   
   >> The job of a simulating halt prover is to determine   
   >> whether or not it must abort its simulation to prevent   
   >> its own non-termination. If for-any-reason the answer   
   >> is yes then it is always correct to abort and reject   
   >> this input.   
   >>   
   >   
   > it's still a partial recognizer, just with worse power than perhaps a   
   > more optimal one that can do more than just abort it's simulation, but   
   > upon doing so recognize the self-reference and perform more in-depth   
   > analysis beyond pure simulation.   
   >   
      
   Like I tell the LLM systems it is a partial halt prover   
   in the same sense that a truth predicate that fails to   
   correctly determine if this sentence is true or false:   
      
   "What time is it?"  Is a partial truth predicate.   
      
   Then they get it. Once we reject bad data it is a   
   halt prover that always works.   
      
   --   
   Copyright 2026 Olcott

              My 28 year goal has been to make
       "true on the basis of meaning expressed in language"
       reliably computable for the entire body of knowledge.

              This required establishing a new foundation
              --- SoupGate-Win32 v1.05        * Origin: you cannot sedate... all the things you hate (1:229/2)   

[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]


(c) 1994,  bbs@darkrealms.ca