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,798 of 262,912    |
|    dart200 to olcott    |
|    Re: Proof theoretic semantics based halt    |
|    04 Feb 26 18:42:56    |
   
   XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: sci.lang, comp.software-eng   
   From: user7160@newsgrouper.org.invalid   
      
   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
|
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
(c) 1994, bbs@darkrealms.ca