home bbs files messages ]

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,383 of 297,461   
   Richard Damon to olcott   
   Re: Proof theoretic semantics based halt   
   01 Feb 26 07:11:22   
   
   XPost: comp.theory, sci.logic, sci.math   
   XPost: comp.lang.prolog, comp.software-eng   
   From: news.x.richarddamon@xoxy.net   
      
   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 correctly determines that DD does not have a well-founded   
   > justification tree within Proof theoretic semantics.   
      
   But only because your DD is not a well-formed program because you fail   
   to include the code for all the program.   
      
   And the reason its behavior isn't "well-founded" is because you failed   
   to include the actual code for HHH. If you do, and that code happens to   
   abort its simulation and returns non-halting, then it is well founded   
   that DD will halt.   
      
   >   
   > When HHH is construed as a proof theoretic halting prover   
   > HHH detects the pathological-self-reference of its input and   
   > rejects DD as non-well-founded on this basis.   
      
   Because your input is just garbage, because you never understood what   
   you were talking abouyt,   
      
   The problem is you think lying is valid logic.   
      
   >   
   > % This sentence is not true.   
   > ?- LP = not(true(LP)).   
   > LP = not(true(LP)).   
   > ?- unify_with_occurs_check(LP, not(true(LP))).   
   > false.   
   >   
   > The Liar Paradox is formally rejected by Prolog   
   > occurs_check for this same reason.   
   >   
   > occurs_check correctly determines that LP does not   
   > have a well-founded justification tree within Proof   
   > theoretic semantics.   
   >   
      
   Which is just irrelevent here, as DD doesn't "call" itself.   
      
   Sorry, you are just proving you are just a pathological liar.   
      
   --- 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