Groups | Search | Server Info | Login | Register
Groups > comp.software-eng > #3957
| From | olcott <polcott333@gmail.com> |
|---|---|
| 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-04 21:04 -0600 |
| Organization | A noiseless patient Spider |
| Message-ID | <10m11cd$2sl46$1@dont-email.me> (permalink) |
| References | (7 earlier) <10m0ljq$2ou3d$1@dont-email.me> <10m0mic$2pl45$1@dont-email.me> <10m103g$2s99i$2@dont-email.me> <10m10hk$2se5m$1@dont-email.me> <10m10m5$2s99i$3@dont-email.me> |
Cross-posted to 6 groups.
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
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.
--
Copyright 2026 Olcott<br><br>
My 28 year goal has been to make <br>
"true on the basis of meaning expressed in language"<br>
reliably computable for the entire body of knowledge.<br><br>
This required establishing a new foundation<br>
Back to comp.software-eng | Previous | Next — Previous in thread | Next in thread | Find similar
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