Groups | Search | Server Info | Login | Register

Groups > comp.software-eng > #3960

Re: Proof theoretic semantics based halt prover correctly rejects its input

From dart200 <user7160@newsgrouper.org.invalid>
Newsgroups comp.theory, sci.logic, sci.math, comp.lang.prolog, sci.lang, comp.software-eng
Subject Re: Proof theoretic semantics based halt prover correctly rejects its input
Date 2026-02-05 18:49 -0800
Organization A noiseless patient Spider
Message-ID <10m3ksm$3mv46$2@dont-email.me> (permalink)
References (10 earlier) <10m10hk$2se5m$1@dont-email.me> <10m10m5$2s99i$3@dont-email.me> <10m11cd$2sl46$1@dont-email.me> <10m2m6c$3dita$2@dont-email.me> <10m2u23$3hft3$1@dont-email.me>

Cross-posted to 6 groups.

Show all headers | View raw

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 <is> 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 perhaps 
>>>> a more optimal one that can do more than just abort it's simulation, 
>>>> but upon doing so recognize the self-reference and perform more in- 
>>>> depth analysis beyond pure simulation.
>>>>
>>>
>>> Like I tell the LLM systems it is a partial halt prover
>>
>> i simple see that a more powerful partial halting recognizer can 
>> return TRUE to the input ND just fine,
>>
> 
> When an input does the opposite of whatever value

bro u didn't read what i posted before, please refer to the definition:

   int ND()
   {
        int Halt_Status = HHH(ND);
        return Halt_Status;
   }

*ND* does not do the oppose of whatever HHH(ND) reports 🫩, it halts 
regardless of what HHH(ND) reports.

yet HHH will still fail to report it's behavior properly because HHH 
will decide that the self-referential recursion implies an infinite 
execution that doesn't actually execute.

> its halt decider returns the only correct choice
> is to reject this input.
> 
> Thanks to LLM systems I now finally have the proper
> conventional terms-of-the-art to say this, we correctly
> reject any input not having:
> 
> *a well-founded justification tree within Proof*
> *theoretic semantics*
> 
> I may have said that same thing not using conventional
> terms-of-the-art as much as 22 years ago. I only had
> the actual algorithm to do that about six years ago.
> 
>> because i can map out the essential steps on paper...
>>
>> furthermore, how do u know ur not losing computational power when 
>> removing all self-referential analysis?
>>
>>> in the same sense that a truth predicate that fails to
>>> correctly determine if this sentence is true or false:
>>>
>>> "What time is it?"  Is a partial truth predicate.
>>>
>>> Then they get it. Once we reject bad data it is a
>>> halt prover that always works.
>>>
>>
>>
> 
> 


-- 
arising us out of the computing dark ages,
please excuse my pseudo-pyscript,
~ nick

Back to comp.software-eng | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-01-31 11:49 -0600
  Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <news.x.richarddamon@xoxy.net> - 2026-02-01 07:11 -0500
    Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 11:35 -0600
      Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 13:31 -0500
        Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 12:36 -0600
          Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 13:48 -0500
      Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 12:41 -0800
        Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 16:15 -0600
          Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 14:19 -0800
            Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 16:27 -0600
              Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 15:43 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 18:00 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 18:42 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 20:50 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 18:52 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 21:04 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 10:06 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 14:20 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 18:49 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 21:11 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 19:23 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 22:08 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 20:15 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 22:31 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 20:36 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 23:01 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 21:22 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 23:26 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 23:42 -0800
                Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-06 08:58 -0600
                Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <news.x.richarddamon@xoxy.net> - 2026-02-06 10:21 -0500
  Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 13:35 -0600
    Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 15:03 -0500
  Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 14:12 -0600
    Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 18:39 -0500
  Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 17:45 -0600
    Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 18:55 -0500
  Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 18:00 -0600
    Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 19:15 -0500
  Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 18:28 -0600
    Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 20:33 -0500

csiph-web