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,817 of 262,912   
   dart200 to olcott   
   Re: Proof theoretic semantics based halt   
   05 Feb 26 21:22:05   
   
   XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: sci.lang, comp.software-eng   
   From: user7160@newsgrouper.org.invalid   
      
   On 2/5/26 9:01 PM, olcott wrote:   
   > On 2/5/2026 10:36 PM, dart200 wrote:   
   >> On 2/5/26 8:31 PM, olcott wrote:   
   >>> On 2/5/2026 10:15 PM, dart200 wrote:   
   >>>> On 2/5/26 8:08 PM, olcott wrote:   
   >>>>> On 2/5/2026 9:23 PM, dart200 wrote:   
   >>>>>> On 2/5/26 7:11 PM, olcott wrote:   
   >>>>>>> On 2/5/2026 8:49 PM, dart200 wrote:   
   >>>>>>>> On 2/5/26 12:20 PM, olcott wrote:   
   >>>>>>>>> On 2/5/2026 12:06 PM, dart200 wrote:   
   >>>>>>>>>> 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   
      
   [continued in next message]   
      
   --- 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