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,805 of 262,912   
   dart200 to olcott   
   Re: Proof theoretic semantics based halt   
   05 Feb 26 10:06:04   
   
   XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: sci.lang, comp.software-eng   
   From: user7160@newsgrouper.org.invalid   
      
   On 2/4/26 7:04 PM, olcott wrote:   
   > 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   
      
   i simple see that a more powerful partial halting recognizer can return   
   TRUE to the input ND just fine,   
      
   because i can map out the essential steps on paper...   
      
   furthermore, how do u know ur not losing computational power when   
   removing all self-referential analysis?   
      
   > 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.   
   >   
      
      
   --   
   arising us out of the computing dark ages,   
   please excuse my pseudo-pyscript,   
   ~ nick   
      
   --- 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