Forums before death by AOL, social media and spammers... "We can't have nice things"
|    sci.lang    |    Natural languages, communication, etc    |    297,461 messages    |
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
|    Message 297,421 of 297,461    |
|    olcott to All    |
|    Re: Proof theoretic semantics based halt    |
|    05 Feb 26 22:31:39    |
   
   XPost: comp.theory, sci.logic, sci.math   
   XPost: comp.lang.prolog, comp.software-eng   
   From: polcott333@gmail.com   
      
   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
|
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
(c) 1994, bbs@darkrealms.ca