Groups | Search | Server Info | Login | Register

Groups > comp.software-eng > #3958

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 10:06 -0800
Organization A noiseless patient Spider
Message-ID <10m2m6c$3dita$2@dont-email.me> (permalink)
References (8 earlier) <10m0mic$2pl45$1@dont-email.me> <10m103g$2s99i$2@dont-email.me> <10m10hk$2se5m$1@dont-email.me> <10m10m5$2s99i$3@dont-email.me> <10m11cd$2sl46$1@dont-email.me>

Cross-posted to 6 groups.

Show all headers | View raw

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,

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