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,822 of 262,912    |
|    Richard Damon to olcott    |
|    Re: Proof theoretic semantics based halt    |
|    06 Feb 26 10:21:15    |
   
   XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: sci.lang, comp.software-eng   
   From: news.x.richarddamon@xoxy.net   
      
   On 2/6/26 9:58 AM, olcott wrote:   
   > On 2/6/2026 1:42 AM, dart200 wrote:   
   >> On 2/5/26 9:26 PM, olcott wrote:   
   >>> On 2/5/2026 11:22 PM, dart200 wrote:   
   >>>> 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
|
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
(c) 1994, bbs@darkrealms.ca