Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > comp.lang.c > #392050 > unrolled thread

Proving the: Simulating termination analyzer Principle

Started byolcott <polcott333@gmail.com>
First post2025-04-05 15:52 -0500
Last post2025-04-13 18:26 -0500
Articles 20 on this page of 66 — 8 participants

Back to article view | Back to comp.lang.c


Contents

  Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 15:52 -0500
    Re: Proving the: Simulating termination analyzer Principle dbush <dbush.mobile@gmail.com> - 2025-04-05 17:15 -0400
      Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 16:29 -0500
        Re: Proving the: Simulating termination analyzer Principle dbush <dbush.mobile@gmail.com> - 2025-04-05 17:31 -0400
          Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-05 23:18 +0100
            Re: Proving the: Simulating termination analyzer Principle dbush <dbush.mobile@gmail.com> - 2025-04-05 18:27 -0400
              Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 19:30 -0500
                Re: Proving the: Simulating termination analyzer Principle dbush <dbush.mobile@gmail.com> - 2025-04-05 20:34 -0400
                  Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 19:43 -0500
                    Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 02:21 +0100
                      Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 22:30 -0500
                    Re: Proving the: Simulating termination analyzer Principle dbush <dbush.mobile@gmail.com> - 2025-04-05 21:22 -0400
                Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 01:52 +0100
                  Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 20:22 -0500
                    Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 02:37 +0100
                      Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 20:42 -0500
            Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 18:18 -0500
              Re: Proving the: Simulating termination analyzer Principle dbush <dbush.mobile@gmail.com> - 2025-04-05 19:20 -0400
                Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 19:36 -0500
                  Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 02:03 +0100
                    Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 22:34 -0500
                  Re: Proving the: Simulating termination analyzer Principle dbush <dbush.mobile@gmail.com> - 2025-04-05 21:19 -0400
                    Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 20:49 -0500
              Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 00:45 +0100
              Re: Proving the: Simulating termination analyzer Principle James Kuyper <jameskuyper@alumni.caltech.edu> - 2025-04-05 20:54 -0400
                Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 20:09 -0500
                  Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 02:31 +0100
        Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-05 14:32 -0700
    Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-05 22:58 +0100
      Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 17:20 -0500
        Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-05 23:31 +0100
          Re: Proving the: Simulating termination analyzer Principle Kaz Kylheku <643-408-1753@kylheku.com> - 2025-04-05 22:42 +0000
            Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 00:25 +0100
              Re: Proving the: Simulating termination analyzer Principle Tim Rentsch <tr.17687@z991.linuxsc.com> - 2025-04-06 03:25 -0700
                Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 11:34 +0100
                Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-06 10:37 -0500
                  Re: Proving the: Simulating termination analyzer Principle Tim Rentsch <tr.17687@z991.linuxsc.com> - 2025-04-06 19:37 -0700
                    Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-06 23:23 -0500
                      Re: Proving the: Simulating termination analyzer Principle Tim Rentsch <tr.17687@z991.linuxsc.com> - 2025-04-07 05:46 -0700
                        Re: Proving the: Simulating termination analyzer Principle Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2025-04-07 14:04 -0700
                          Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-07 16:54 -0500
                          Re: Proving the: Simulating termination analyzer Principle Tim Rentsch <tr.17687@z991.linuxsc.com> - 2025-04-08 10:52 -0700
                            Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-08 22:04 -0500
                        Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-07 16:41 -0500
                        Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-08 21:22 -0500
            Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 19:07 -0500
          Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 19:35 -0500
            Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-06 01:59 +0100
              Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-05 22:26 -0500
                Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-08 23:00 -0700
                  Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-09 12:18 -0500
                    Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-09 16:39 -0700
                      Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-09 21:02 -0500
                        Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-09 21:04 -0700
                          Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-09 21:10 -0700
                          Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-10 17:53 -0500
                            Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-10 20:00 -0700
                              Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-11 09:42 -0500
                                Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-11 13:00 -0700
                                  Re: Proving the: Simulating termination analyzer Principle Richard Heathfield <rjh@cpax.org.uk> - 2025-04-11 21:57 +0100
                                    Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-13 07:08 -0500
                                  Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-13 07:03 -0500
                                    Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-13 12:38 -0700
                                      Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-13 14:56 -0500
                                        Re: Proving the: Simulating termination analyzer Principle "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-04-13 14:50 -0700
                                          Re: Proving the: Simulating termination analyzer Principle olcott <polcott333@gmail.com> - 2025-04-13 18:26 -0500

Page 2 of 4 — ← Prev page 1 [2] 3 4  Next page →


#392115

Fromolcott <polcott333@gmail.com>
Date2025-04-05 22:34 -0500
Message-ID<vssso1$d1q$4@dont-email.me>
In reply to#392094
On 4/5/2025 8:03 PM, Richard Heathfield wrote:
> On 06/04/2025 01:36, olcott wrote:
>> On 4/5/2025 6:20 PM, dbush wrote:
>>> On 4/5/2025 7:18 PM, olcott wrote:
>>>> On 4/5/2025 5:18 PM, Richard Heathfield wrote:
>>>>> On 05/04/2025 22:31, dbush wrote:
>>>>>> On 4/5/2025 5:29 PM, olcott wrote:
>>>>>>> On 4/5/2025 4:15 PM, dbush wrote:
>>>>>>>> On 4/5/2025 4:52 PM, olcott wrote:
>>>>>>>>> *Simulating termination analyzer Principle*
>>>>>>>>> It is always correct for any simulating termination
>>>>>>>>> analyzer to stop simulating and reject any input that
>>>>>>>>> would otherwise prevent its own termination.
>>>>>>>>>
>>>>>>>>> void DDD()
>>>>>>>>> {
>>>>>>>>>     HHH(DDD);
>>>>>>>>>     return;
>>>>>>>>> }
>>>>>>>>
>>>>>>>> Except when doing so would change the input, as is the case with 
>>>>>>>> HHH and DDD.
>>>>>>>>
>>>>>>>> Changing the input is not allowed.
>>>>>>>
>>>>>>> You may disagree that the above definition
>>>>>>> of simulating termination analyzer is correct.
>>>>>>>
>>>>>>> It is self-evident that HHH must stop simulating
>>>>>>> DDD to prevent its own non-termination.
>>>>>>>
>>>>>>
>>>>>> Changing the input is not allowed.
>>>>>
>>>>> You're right, but it doesn't matter very much as long as 
>>>>> terminates() *always* gets the answer right for any arbitrary 
>>>>> program tape and any data tape. Mr Olcott's fails to do that.
>>>>>
>>>>
>>>> Termination analyzers are not required to be infallible.
>>>>
>>>
>>>
>>> But they must still generate the required mapping for the input they 
>>> claim to answer correctly:
>>>
>>>
>>> Given any algorithm (i.e. a fixed immutable sequence of instructions) 
>>> X described as <X> with input Y:
>>>
>>> A solution to the halting problem is an algorithm H that computes the 
>>> following mapping:
>>>
>>> (<X>,Y) maps to 1 if and only if X(Y) halts when executed directly
>>> (<X>,Y) maps to 0 if and only if X(Y) does not halt when executed 
>>> directly
>>>
>>
>> Exactly the opposite, they are only allowed to report
>> on what they see.
> 
> A solution is required to take into account all parts of the program 
> that affect its termination status. It is not allowed to guess.
> 

HHH sees that it must stop simulating DDD to prevent its
own non-termination. It doesn't guess most every novice
C programmer can see this too.

-- 
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[toc] | [prev] | [next] | [standalone]


#392097

Fromdbush <dbush.mobile@gmail.com>
Date2025-04-05 21:19 -0400
Message-ID<vsskr5$3mggf$1@dont-email.me>
In reply to#392087
On 4/5/2025 8:36 PM, olcott wrote:
> On 4/5/2025 6:20 PM, dbush wrote:
>> On 4/5/2025 7:18 PM, olcott wrote:
>>> On 4/5/2025 5:18 PM, Richard Heathfield wrote:
>>>> On 05/04/2025 22:31, dbush wrote:
>>>>> On 4/5/2025 5:29 PM, olcott wrote:
>>>>>> On 4/5/2025 4:15 PM, dbush wrote:
>>>>>>> On 4/5/2025 4:52 PM, olcott wrote:
>>>>>>>> *Simulating termination analyzer Principle*
>>>>>>>> It is always correct for any simulating termination
>>>>>>>> analyzer to stop simulating and reject any input that
>>>>>>>> would otherwise prevent its own termination.
>>>>>>>>
>>>>>>>> void DDD()
>>>>>>>> {
>>>>>>>>     HHH(DDD);
>>>>>>>>     return;
>>>>>>>> }
>>>>>>>
>>>>>>> Except when doing so would change the input, as is the case with 
>>>>>>> HHH and DDD.
>>>>>>>
>>>>>>> Changing the input is not allowed.
>>>>>>
>>>>>> You may disagree that the above definition
>>>>>> of simulating termination analyzer is correct.
>>>>>>
>>>>>> It is self-evident that HHH must stop simulating
>>>>>> DDD to prevent its own non-termination.
>>>>>>
>>>>>
>>>>> Changing the input is not allowed.
>>>>
>>>> You're right, but it doesn't matter very much as long as 
>>>> terminates() *always* gets the answer right for any arbitrary 
>>>> program tape and any data tape. Mr Olcott's fails to do that.
>>>>
>>>
>>> Termination analyzers are not required to be infallible.
>>>
>>
>>
>> But they must still generate the required mapping for the input they 
>> claim to answer correctly:
>>
>>
>> Given any algorithm (i.e. a fixed immutable sequence of instructions) 
>> X described as <X> with input Y:
>>
>> A solution to the halting problem is an algorithm H that computes the 
>> following mapping:
>>
>> (<X>,Y) maps to 1 if and only if X(Y) halts when executed directly
>> (<X>,Y) maps to 0 if and only if X(Y) does not halt when executed 
>> directly
>>
> 
> Exactly the opposite, they are only allowed to report
> on what they see.
> 

No, they report what they are programed to report, which is some 
computable function.

And the halting function is not a computable function, as Linz and 
others have proved:


Given any algorithm (i.e. a fixed immutable sequence of instructions) X 
described as <X> with input Y:

A solution to the halting problem is an algorithm H that computes the 
following mapping:

(<X>,Y) maps to 1 if and only if X(Y) halts when executed directly
(<X>,Y) maps to 0 if and only if X(Y) does not halt when executed directly

[toc] | [prev] | [next] | [standalone]


#392109

Fromolcott <polcott333@gmail.com>
Date2025-04-05 20:49 -0500
Message-ID<vssmir$3m0q1$6@dont-email.me>
In reply to#392097
On 4/5/2025 8:19 PM, dbush wrote:
> On 4/5/2025 8:36 PM, olcott wrote:
>> On 4/5/2025 6:20 PM, dbush wrote:
>>> On 4/5/2025 7:18 PM, olcott wrote:
>>>> On 4/5/2025 5:18 PM, Richard Heathfield wrote:
>>>>> On 05/04/2025 22:31, dbush wrote:
>>>>>> On 4/5/2025 5:29 PM, olcott wrote:
>>>>>>> On 4/5/2025 4:15 PM, dbush wrote:
>>>>>>>> On 4/5/2025 4:52 PM, olcott wrote:
>>>>>>>>> *Simulating termination analyzer Principle*
>>>>>>>>> It is always correct for any simulating termination
>>>>>>>>> analyzer to stop simulating and reject any input that
>>>>>>>>> would otherwise prevent its own termination.
>>>>>>>>>
>>>>>>>>> void DDD()
>>>>>>>>> {
>>>>>>>>>     HHH(DDD);
>>>>>>>>>     return;
>>>>>>>>> }
>>>>>>>>
>>>>>>>> Except when doing so would change the input, as is the case with 
>>>>>>>> HHH and DDD.
>>>>>>>>
>>>>>>>> Changing the input is not allowed.
>>>>>>>
>>>>>>> You may disagree that the above definition
>>>>>>> of simulating termination analyzer is correct.
>>>>>>>
>>>>>>> It is self-evident that HHH must stop simulating
>>>>>>> DDD to prevent its own non-termination.
>>>>>>>
>>>>>>
>>>>>> Changing the input is not allowed.
>>>>>
>>>>> You're right, but it doesn't matter very much as long as 
>>>>> terminates() *always* gets the answer right for any arbitrary 
>>>>> program tape and any data tape. Mr Olcott's fails to do that.
>>>>>
>>>>
>>>> Termination analyzers are not required to be infallible.
>>>>
>>>
>>>
>>> But they must still generate the required mapping for the input they 
>>> claim to answer correctly:
>>>
>>>
>>> Given any algorithm (i.e. a fixed immutable sequence of instructions) 
>>> X described as <X> with input Y:
>>>
>>> A solution to the halting problem is an algorithm H that computes the 
>>> following mapping:
>>>
>>> (<X>,Y) maps to 1 if and only if X(Y) halts when executed directly
>>> (<X>,Y) maps to 0 if and only if X(Y) does not halt when executed 
>>> directly
>>>
>>
>> Exactly the opposite, they are only allowed to report
>> on what they see.
>>
> 
> No, they report what they are programed to report, which is some then
> computable function.
> 

If its a Turing computable function then it must
transform an input finite string into an output
according to some algorithm (defined sequence of steps).


-- 
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[toc] | [prev] | [next] | [standalone]


#392081

FromRichard Heathfield <rjh@cpax.org.uk>
Date2025-04-06 00:45 +0100
Message-ID<vssfa2$3gd7d$2@dont-email.me>
In reply to#392077
On 06/04/2025 00:18, olcott wrote:
> On 4/5/2025 5:18 PM, Richard Heathfield wrote:
>> On 05/04/2025 22:31, dbush wrote:
<snip>
>>>
>>> Changing the input is not allowed.
>>
>> You're right, but it doesn't matter very much as long as 
>> terminates() *always* gets the answer right for any arbitrary 
>> program tape and any data tape. Mr Olcott's fails to do that.
>>
> 
> Termination analyzers are not required to be infallible.

Then why all the fuss? Writing a program that doesn't have to 
work is not exactly difficult.

int terminates(void (*prg)(), void *data)
{
   return 1; /* job done */
}

"Termination analyzers are not required to be infallible." - 
Peter Olcott

-- 
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within

[toc] | [prev] | [next] | [standalone]


#392092

FromJames Kuyper <jameskuyper@alumni.caltech.edu>
Date2025-04-05 20:54 -0400
Message-ID<vssjcu$3l5ki$1@dont-email.me>
In reply to#392077
On 06/04/2025 00:18, olcott wrote:
...
> Termination analyzers are not required to be infallible.

The Halting Problem refers to the impossibility of an infallible
termination analyzer. Fallible termination analyzers are trivially
possible - the question's not worth thinking about.

[toc] | [prev] | [next] | [standalone]


#392096

Fromolcott <polcott333@gmail.com>
Date2025-04-05 20:09 -0500
Message-ID<vssk8p$3m0q1$1@dont-email.me>
In reply to#392092
On 4/5/2025 7:54 PM, James Kuyper wrote:
> On 06/04/2025 00:18, olcott wrote:
> ...
>> Termination analyzers are not required to be infallible.
> 
> The Halting Problem refers to the impossibility of an infallible
> termination analyzer. Fallible termination analyzers are trivially
> possible - the question's not worth thinking about.

typedef void (*ptr)();
int HHH(ptr P);

int DD()
{
   int Halt_Status = HHH(DD);
   if (Halt_Status)
     HERE: goto HERE;
   return Halt_Status;
}

int main()
{
   HHH(DD);
}

They are not trivially possible for the above input.

*Simulating termination analyzer Principle*
It is always correct for any simulating termination
analyzer to stop simulating and reject any input that
would otherwise prevent its own termination.

-- 
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[toc] | [prev] | [next] | [standalone]


#392104

FromRichard Heathfield <rjh@cpax.org.uk>
Date2025-04-06 02:31 +0100
Message-ID<vssli0$3gd7d$8@dont-email.me>
In reply to#392096
On 06/04/2025 02:09, olcott wrote:
> On 4/5/2025 7:54 PM, James Kuyper wrote:
>> On 06/04/2025 00:18, olcott wrote:
>> ...
>>> Termination analyzers are not required to be infallible.
>>
>> The Halting Problem refers to the impossibility of an infallible
>> termination analyzer. Fallible termination analyzers are trivially
>> possible - the question's not worth thinking about.
> 
> typedef void (*ptr)();
> int HHH(ptr P);
> 
> int DD()
> {
>    int Halt_Status = HHH(DD);
>    if (Halt_Status)
>      HERE: goto HERE;
>    return Halt_Status;
> }
> 
> int main()
> {
>    HHH(DD);
> }
> 
> They are not trivially possible for the above input.


Sure they are.

unsigned hhh(ptr P)
{
   unsigned r = rand();
   return r * (unsigned)P;
}

Getting it wrong is a walk in the park. Nobody disputes your 
claim that you can write broken code.

-- 
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within

[toc] | [prev] | [next] | [standalone]


#392057

From"Chris M. Thomasson" <chris.m.thomasson.1@gmail.com>
Date2025-04-05 14:32 -0700
Message-ID<vss7gq$39cob$1@dont-email.me>
In reply to#392055
On 4/5/2025 2:29 PM, olcott wrote:
[...]
> It is self-evident that HHH must stop simulating
> DDD to prevent its own non-termination.

Yawn.

[toc] | [prev] | [next] | [standalone]


#392063

FromRichard Heathfield <rjh@cpax.org.uk>
Date2025-04-05 22:58 +0100
Message-ID<vss91c$3b1no$1@dont-email.me>
In reply to#392050
On 05/04/2025 21:52, olcott wrote:
> *Simulating termination analyzer Principle*
> It is always correct for any simulating termination
> analyzer to stop simulating and reject any input that
> would otherwise prevent its own termination.

*Halting Problem Principle*
Let us call the function that will
determine whether the program terminates
"terminates (f, x)," and let us further sup-
pose that it gives the answer true if the com-
putation f(x) will eventually (in theory)
terminate, and the answer false if it will
never terminate. Of course, the function
"terminates" itself should be designed
always to terminate; otherwise its general
usefulness would be seriously impaired.
CAR Hoare AND DCS Allison, "Incomputability", 1972.

So a "termination analyzer" (as you call it) is /required/ to 
terminate (with the correct answer).

Because it must terminate, it cannot be allowed to depend on 
running programs to completion to see if they terminate, lest 
they don't. They must be cleverer than that.

Fortunately we don't need to be too clever just to reason about 
terminates(). We can use pseudo-code to show how to call it and 
wave our way past its guts.

We will assume that terminates() correctly echoes either "Does 
halt" or "Never halts" to the output device, ))))however((((( it 
arrives at the result, because whether it determines the answer 
by simulation or by parsing the source is /irrelevant/ as long as 
it gets the answer right.

hp(arg candidate, arg testdata)
{
   if(terminates(candidate(testdata)))
   {
     while(forever);
   }
   else
   {
     halt;
   }
}

We then invoke the program:

hp(hp, hp)

and try to predict what terminates() will report, and of course 
the answer is that we don't know, because neither does 
terminates(). The function cannot be written.

-- 
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within

[toc] | [prev] | [next] | [standalone]


#392070

Fromolcott <polcott333@gmail.com>
Date2025-04-05 17:20 -0500
Message-ID<vssabb$3aqnp$2@dont-email.me>
In reply to#392063
On 4/5/2025 4:58 PM, Richard Heathfield wrote:
> On 05/04/2025 21:52, olcott wrote:
>> *Simulating termination analyzer Principle*
>> It is always correct for any simulating termination
>> analyzer to stop simulating and reject any input that
>> would otherwise prevent its own termination.
> 
> *Halting Problem Principle*
> Let us call the function that will
> determine whether the program terminates
> "terminates (f, x)," and let us further sup-
> pose that it gives the answer true if the com-
> putation f(x) will eventually (in theory)
> terminate, and the answer false if it will
> never terminate. Of course, the function
> "terminates" itself should be designed
> always to terminate; otherwise its general
> usefulness would be seriously impaired.
> CAR Hoare AND DCS Allison, "Incomputability", 1972.
> 
> So a "termination analyzer" (as you call it) is /required/ to terminate 
> (with the correct answer).
> 
> Because it must terminate, it cannot be allowed to depend on running 
> programs to completion to see if they terminate, lest they don't. They 
> must be cleverer than that.
> 
> Fortunately we don't need to be too clever just to reason about 
> terminates(). We can use pseudo-code to show how to call it and wave our 
> way past its guts.
> 
> We will assume that terminates() correctly echoes either "Does halt" or 
> "Never halts" to the output device, ))))however((((( it arrives at the 
> result, because whether it determines the answer by simulation or by 
> parsing the source is /irrelevant/ as long as it gets the answer right.
> 
> hp(arg candidate, arg testdata)
> {
>    if(terminates(candidate(testdata)))
>    {
>      while(forever);
>    }
>    else
>    {
>      halt;
>    }
> }
> 
> We then invoke the program:
> 
> hp(hp, hp)
> 
> and try to predict what terminates() will report, and of course the 
> answer is that we don't know, because neither does terminates(). The 
> function cannot be written.
> 

Understanding my simpler example was a mandatory
prerequisite to complex examples such as this:

typedef void (*ptr)();
int HHH(ptr P);

int DD()
{
   int Halt_Status = HHH(DD);
   if (Halt_Status)
     HERE: goto HERE;
   return Halt_Status;
}

Please go back and try again so that many levels
of quotation do not make this key essence more
difficult to see.

-- 
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[toc] | [prev] | [next] | [standalone]


#392072

FromRichard Heathfield <rjh@cpax.org.uk>
Date2025-04-05 23:31 +0100
Message-ID<vssavl$3b2j0$3@dont-email.me>
In reply to#392070
On 05/04/2025 23:20, olcott wrote:
> On 4/5/2025 4:58 PM, Richard Heathfield wrote:

<snip>

>> hp(arg candidate, arg testdata)
>> {
>>    if(terminates(candidate(testdata)))
>>    {
>>      while(forever);
>>    }
>>    else
>>    {
>>      halt;
>>    }
>> }
>>
>> We then invoke the program:
>>
>> hp(hp, hp)
>>
>> and try to predict what terminates() will report, and of course 
>> the answer is that we don't know, because neither does 
>> terminates(). The function cannot be written.
>>
> 
> Understanding my simpler example was a mandatory
> prerequisite

No, it wasn't.

Understanding my example isn't mandatory either, which is just as 
well where you're concerned.

> int DD()
> {
>    int Halt_Status = HHH(DD);
>    if (Halt_Status)
>      HERE: goto HERE;
>    return Halt_Status;
> }

That's fine, but it does beg the HHH() question. You are 
handwaving it for the same reason I am, which is that it can't be 
written. The difference between us is that I know it and you don't.

-- 
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within

[toc] | [prev] | [next] | [standalone]


#392073

FromKaz Kylheku <643-408-1753@kylheku.com>
Date2025-04-05 22:42 +0000
Message-ID<20250405153728.395@kylheku.com>
In reply to#392072
On 2025-04-05, Richard Heathfield <rjh@cpax.org.uk> wrote:
> On 05/04/2025 23:20, olcott wrote:
> > ...
> The difference between us is that I know it and you don't.

Olcott resides in a fortress he built out of bricks that were
specially ordered from Dunning and Kruger's website.
You're not getting through.

-- 
TXR Programming Language: http://nongnu.org/txr
Cygnal: Cygwin Native Application Library: http://kylheku.com/cygnal
Mastodon: @Kazinator@mstdn.ca

[toc] | [prev] | [next] | [standalone]


#392079

FromRichard Heathfield <rjh@cpax.org.uk>
Date2025-04-06 00:25 +0100
Message-ID<vsse5t$3gbj1$1@dont-email.me>
In reply to#392073
On 05/04/2025 23:42, Kaz Kylheku wrote:
> On 2025-04-05, Richard Heathfield <rjh@cpax.org.uk> wrote:
>> On 05/04/2025 23:20, olcott wrote:
>>> ...
>> The difference between us is that I know it and you don't.
> 
> Olcott resides in a fortress he built out of bricks that were
> specially ordered from Dunning and Kruger's website.
> You're not getting through.

Well, no. On the other hand, the discussion has in places driven
me to the literature and has thus in its own way been
educational. For example, I was surprised to discover that
although Turing's 1936 paper does deal with the Halting Problem,
he doesn't actually use that term, which didn't surface until
1952. I also stumbled on a 1972 paper on incomputability by Tony
Hoare and Donald Allison - well worth the read, and I was amused
by its somewhat prescient opening paragraph: "[...] programmers
have been known to attempt solutions to problems which are
probably unsolvable; the existence of such problems should be of
interest to all programmers." Clearly, 53 years ago, they already
had Olcott nailed.

-- 
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within

[toc] | [prev] | [next] | [standalone]


#392120

FromTim Rentsch <tr.17687@z991.linuxsc.com>
Date2025-04-06 03:25 -0700
Message-ID<86tt71fuxh.fsf@linuxsc.com>
In reply to#392079
Richard Heathfield <rjh@cpax.org.uk> writes:

> On 05/04/2025 23:42, Kaz Kylheku wrote:
>
>> On 2025-04-05, Richard Heathfield <rjh@cpax.org.uk> wrote:
>>
>>> On 05/04/2025 23:20, olcott wrote:
>>>
>>>> ...
>>>
>>> The difference between us is that I know it and you don't.
>>
>> Olcott resides in a fortress he built out of bricks that were
>> specially ordered from Dunning and Kruger's website.
>> You're not getting through.
>
> Well, no.  On the other hand, the discussion has in places driven
> me to the literature and has thus in its own way been
> educational.  For example, I was surprised to discover that
> although Turing's 1936 paper does deal with the Halting Problem,
> he doesn't actually use that term, which didn't surface until
> 1952.  I also stumbled on a 1972 paper on incomputability by Tony
> Hoare and Donald Allison - well worth the read, and I was amused
> by its somewhat prescient opening paragraph: "[...] programmers
> have been known to attempt solutions to problems which are
> probably unsolvable;  the existence of such problems should be of
> interest to all programmers."  Clearly, 53 years ago, they already
> had Olcott nailed.

I agree these discoveries are interesting, but the subject still
isn't one that is suitable for comp.lang.c.  A good way to avoid
these long pointless discussions is not to respond to postings
that are not suitable to comp.lang.c, except to point out that
they are not suitable to comp.lang.c.  And for any given poster,
don't respond to unsuitable postings more often than once a month.

[toc] | [prev] | [next] | [standalone]


#392122

FromRichard Heathfield <rjh@cpax.org.uk>
Date2025-04-06 11:34 +0100
Message-ID<vstlc7$n9gi$1@dont-email.me>
In reply to#392120
On 06/04/2025 11:25, Tim Rentsch wrote:
> Richard Heathfield <rjh@cpax.org.uk> writes:
> 
>> On 05/04/2025 23:42, Kaz Kylheku wrote:
>>
>>> On 2025-04-05, Richard Heathfield <rjh@cpax.org.uk> wrote:
>>>
>>>> On 05/04/2025 23:20, olcott wrote:
>>>>
>>>>> ...
>>>>
>>>> The difference between us is that I know it and you don't.
>>>
>>> Olcott resides in a fortress he built out of bricks that were
>>> specially ordered from Dunning and Kruger's website.
>>> You're not getting through.
>>
>> Well, no.  On the other hand, the discussion has in places driven
>> me to the literature and has thus in its own way been
>> educational.  For example, I was surprised to discover that
>> although Turing's 1936 paper does deal with the Halting Problem,
>> he doesn't actually use that term, which didn't surface until
>> 1952.  I also stumbled on a 1972 paper on incomputability by Tony
>> Hoare and Donald Allison - well worth the read, and I was amused
>> by its somewhat prescient opening paragraph: "[...] programmers
>> have been known to attempt solutions to problems which are
>> probably unsolvable;  the existence of such problems should be of
>> interest to all programmers."  Clearly, 53 years ago, they already
>> had Olcott nailed.
> 
> I agree these discoveries are interesting, but the subject still
> isn't one that is suitable for comp.lang.c.

Agreed. (On re-reading my Hoare quote, I can see that it might be 
interpreted as an attempt to establish topicality! That was most 
certainly not my intent.)

-- 
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within

[toc] | [prev] | [next] | [standalone]


#392135

Fromolcott <polcott333@gmail.com>
Date2025-04-06 10:37 -0500
Message-ID<vsu73b$1b0t8$1@dont-email.me>
In reply to#392120
On 4/6/2025 5:25 AM, Tim Rentsch wrote:
> Richard Heathfield <rjh@cpax.org.uk> writes:
> 
>> On 05/04/2025 23:42, Kaz Kylheku wrote:
>>
>>> On 2025-04-05, Richard Heathfield <rjh@cpax.org.uk> wrote:
>>>
>>>> On 05/04/2025 23:20, olcott wrote:
>>>>
>>>>> ...
>>>>
>>>> The difference between us is that I know it and you don't.
>>>
>>> Olcott resides in a fortress he built out of bricks that were
>>> specially ordered from Dunning and Kruger's website.
>>> You're not getting through.
>>
>> Well, no.  On the other hand, the discussion has in places driven
>> me to the literature and has thus in its own way been
>> educational.  For example, I was surprised to discover that
>> although Turing's 1936 paper does deal with the Halting Problem,
>> he doesn't actually use that term, which didn't surface until
>> 1952.  I also stumbled on a 1972 paper on incomputability by Tony
>> Hoare and Donald Allison - well worth the read, and I was amused
>> by its somewhat prescient opening paragraph: "[...] programmers
>> have been known to attempt solutions to problems which are
>> probably unsolvable;  the existence of such problems should be of
>> interest to all programmers."  Clearly, 53 years ago, they already
>> had Olcott nailed.
> 
> I agree these discoveries are interesting, but the subject still
> isn't one that is suitable for comp.lang.c.  A good way to avoid
> these long pointless discussions is not to respond to postings
> that are not suitable to comp.lang.c, except to point out that
> they are not suitable to comp.lang.c.  And for any given poster,
> don't respond to unsuitable postings more often than once a month.

My intent was to focus on the semantics of a pair of C functions.
Digression into computer science seems inappropriate and never
was my intent. The comp.theory people refused to consider the
semantics of C aspects of these functions.


-- 
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[toc] | [prev] | [next] | [standalone]


#392141

FromTim Rentsch <tr.17687@z991.linuxsc.com>
Date2025-04-06 19:37 -0700
Message-ID<86y0wcelxp.fsf@linuxsc.com>
In reply to#392135
olcott <polcott333@gmail.com> writes:

> On 4/6/2025 5:25 AM, Tim Rentsch wrote:
>
>> Richard Heathfield <rjh@cpax.org.uk> writes:
>>
>>> On 05/04/2025 23:42, Kaz Kylheku wrote:
>>>
>>>> On 2025-04-05, Richard Heathfield <rjh@cpax.org.uk> wrote:
>>>>
>>>>> On 05/04/2025 23:20, olcott wrote:
>>>>>
>>>>>> ...
>>>>>
>>>>> The difference between us is that I know it and you don't.
>>>>
>>>> Olcott resides in a fortress he built out of bricks that were
>>>> specially ordered from Dunning and Kruger's website.
>>>> You're not getting through.
>>>
>>> Well, no.  On the other hand, the discussion has in places driven
>>> me to the literature and has thus in its own way been
>>> educational.  For example, I was surprised to discover that
>>> although Turing's 1936 paper does deal with the Halting Problem,
>>> he doesn't actually use that term, which didn't surface until
>>> 1952.  I also stumbled on a 1972 paper on incomputability by Tony
>>> Hoare and Donald Allison - well worth the read, and I was amused
>>> by its somewhat prescient opening paragraph: "[...] programmers
>>> have been known to attempt solutions to problems which are
>>> probably unsolvable;  the existence of such problems should be of
>>> interest to all programmers."  Clearly, 53 years ago, they already
>>> had Olcott nailed.
>>
>> I agree these discoveries are interesting, but the subject still
>> isn't one that is suitable for comp.lang.c.  A good way to avoid
>> these long pointless discussions is not to respond to postings
>> that are not suitable to comp.lang.c, except to point out that
>> they are not suitable to comp.lang.c.  And for any given poster,
>> don't respond to unsuitable postings more often than once a month.
>
> My intent was to focus on the semantics of a pair of C functions.
> Digression into computer science seems inappropriate and never
> was my intent.  The comp.theory people refused to consider the
> semantics of C aspects of these functions.

It seems the people who are responding to you have the impression
that you are convinced you have a solution to the halting problem,
and that your questions about code are in effect asking people to
convince you that you don't (or alternatively that you are offering
an argument that you have solved the halting problem).

If indeed your interest is only about how C defines the semantics of
some particular functions written in C, and having nothing to do
with solving the halting problem, then the burden is on you to
express that question well enough so that other people realize that.
So far it appears that you haven't succeeded with anyone who has
responded to your postings.

[toc] | [prev] | [next] | [standalone]


#392144

Fromolcott <polcott333@gmail.com>
Date2025-04-06 23:23 -0500
Message-ID<vsvk08$2r125$1@dont-email.me>
In reply to#392141
On 4/6/2025 9:37 PM, Tim Rentsch wrote:
> olcott <polcott333@gmail.com> writes:
> 
>> On 4/6/2025 5:25 AM, Tim Rentsch wrote:
>>
>>> Richard Heathfield <rjh@cpax.org.uk> writes:
>>>
>>>> On 05/04/2025 23:42, Kaz Kylheku wrote:
>>>>
>>>>> On 2025-04-05, Richard Heathfield <rjh@cpax.org.uk> wrote:
>>>>>
>>>>>> On 05/04/2025 23:20, olcott wrote:
>>>>>>
>>>>>>> ...
>>>>>>
>>>>>> The difference between us is that I know it and you don't.
>>>>>
>>>>> Olcott resides in a fortress he built out of bricks that were
>>>>> specially ordered from Dunning and Kruger's website.
>>>>> You're not getting through.
>>>>
>>>> Well, no.  On the other hand, the discussion has in places driven
>>>> me to the literature and has thus in its own way been
>>>> educational.  For example, I was surprised to discover that
>>>> although Turing's 1936 paper does deal with the Halting Problem,
>>>> he doesn't actually use that term, which didn't surface until
>>>> 1952.  I also stumbled on a 1972 paper on incomputability by Tony
>>>> Hoare and Donald Allison - well worth the read, and I was amused
>>>> by its somewhat prescient opening paragraph: "[...] programmers
>>>> have been known to attempt solutions to problems which are
>>>> probably unsolvable;  the existence of such problems should be of
>>>> interest to all programmers."  Clearly, 53 years ago, they already
>>>> had Olcott nailed.
>>>
>>> I agree these discoveries are interesting, but the subject still
>>> isn't one that is suitable for comp.lang.c.  A good way to avoid
>>> these long pointless discussions is not to respond to postings
>>> that are not suitable to comp.lang.c, except to point out that
>>> they are not suitable to comp.lang.c.  And for any given poster,
>>> don't respond to unsuitable postings more often than once a month.
>>
>> My intent was to focus on the semantics of a pair of C functions.
>> Digression into computer science seems inappropriate and never
>> was my intent.  The comp.theory people refused to consider the
>> semantics of C aspects of these functions.
> 
> It seems the people who are responding to you have the impression
> that you are convinced you have a solution to the halting problem,
> and that your questions about code are in effect asking people to
> convince you that you don't (or alternatively that you are offering
> an argument that you have solved the halting problem).
> 
> If indeed your interest is only about how C defines the semantics of
> some particular functions written in C, and having nothing to do
> with solving the halting problem, then the burden is on you to
> express that question well enough so that other people realize that.
> So far it appears that you haven't succeeded with anyone who has
> responded to your postings.

int DD()
{
   int Halt_Status = HHH(DD);
   if (Halt_Status)
     HERE: goto HERE;
   return Halt_Status;
}

The people responding to my posts have consistently
stonewalled my every attempt to:
(a) Show that DD correctly simulated by HHH could
     never reach its own "return" instruction.

(b) We never got to (b) because of endless stonewalling.

The end goal (in this forum) that is empirically proven
by this fully operational code:

https://github.com/plolcott/x86utm/blob/master/Halt7.c

is to show that HHH is a correct termination analyzer for DD.

-- 
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[toc] | [prev] | [next] | [standalone]


#392149

FromTim Rentsch <tr.17687@z991.linuxsc.com>
Date2025-04-07 05:46 -0700
Message-ID<86ldscdtqw.fsf@linuxsc.com>
In reply to#392144
olcott <polcott333@gmail.com> writes:

> On 4/6/2025 9:37 PM, Tim Rentsch wrote:
>
>> olcott <polcott333@gmail.com> writes:
>>
>>> On 4/6/2025 5:25 AM, Tim Rentsch wrote:
>>>
>>>> Richard Heathfield <rjh@cpax.org.uk> writes:
>>>>
>>>>> On 05/04/2025 23:42, Kaz Kylheku wrote:
>>>>>
>>>>>> On 2025-04-05, Richard Heathfield <rjh@cpax.org.uk> wrote:
>>>>>>
>>>>>>> On 05/04/2025 23:20, olcott wrote:
>>>>>>>
>>>>>>>> ...
>>>>>>>
>>>>>>> The difference between us is that I know it and you don't.
>>>>>>
>>>>>> Olcott resides in a fortress he built out of bricks that were
>>>>>> specially ordered from Dunning and Kruger's website.
>>>>>> You're not getting through.
>>>>>
>>>>> Well, no.  On the other hand, the discussion has in places driven
>>>>> me to the literature and has thus in its own way been
>>>>> educational.  For example, I was surprised to discover that
>>>>> although Turing's 1936 paper does deal with the Halting Problem,
>>>>> he doesn't actually use that term, which didn't surface until
>>>>> 1952.  I also stumbled on a 1972 paper on incomputability by Tony
>>>>> Hoare and Donald Allison - well worth the read, and I was amused
>>>>> by its somewhat prescient opening paragraph: "[...] programmers
>>>>> have been known to attempt solutions to problems which are
>>>>> probably unsolvable;  the existence of such problems should be of
>>>>> interest to all programmers."  Clearly, 53 years ago, they already
>>>>> had Olcott nailed.
>>>>
>>>> I agree these discoveries are interesting, but the subject still
>>>> isn't one that is suitable for comp.lang.c.  A good way to avoid
>>>> these long pointless discussions is not to respond to postings
>>>> that are not suitable to comp.lang.c, except to point out that
>>>> they are not suitable to comp.lang.c.  And for any given poster,
>>>> don't respond to unsuitable postings more often than once a month.
>>>
>>> My intent was to focus on the semantics of a pair of C functions.
>>> Digression into computer science seems inappropriate and never
>>> was my intent.  The comp.theory people refused to consider the
>>> semantics of C aspects of these functions.
>>
>> It seems the people who are responding to you have the impression
>> that you are convinced you have a solution to the halting problem,
>> and that your questions about code are in effect asking people to
>> convince you that you don't (or alternatively that you are offering
>> an argument that you have solved the halting problem).
>>
>> If indeed your interest is only about how C defines the semantics of
>> some particular functions written in C, and having nothing to do
>> with solving the halting problem, then the burden is on you to
>> express that question well enough so that other people realize that.
>> So far it appears that you haven't succeeded with anyone who has
>> responded to your postings.
>
> int DD()
> {
>   int Halt_Status = HHH(DD);
>   if (Halt_Status)
>     HERE: goto HERE;
>   return Halt_Status;
> }
>
> The people responding to my posts have consistently
> stonewalled my every attempt to:
> (a) Show that DD correctly simulated by HHH could
>     never reach its own "return" instruction.
>
> (b) We never got to (b) because of endless stonewalling.
>
> The end goal (in this forum) that is empirically proven
> by this fully operational code:
>
> https://github.com/plolcott/x86utm/blob/master/Halt7.c
>
> is to show that HHH is a correct termination analyzer for DD.

I'm sorry my comments weren't more helpful for you.

[toc] | [prev] | [next] | [standalone]


#392169

FromKeith Thompson <Keith.S.Thompson+u@gmail.com>
Date2025-04-07 14:04 -0700
Message-ID<87ecy3d6ob.fsf@nosuchdomain.example.com>
In reply to#392149
Tim Rentsch <tr.17687@z991.linuxsc.com> writes:
> olcott <polcott333@gmail.com> writes:
[82 lines deleted]
>
> I'm sorry my comments weren't more helpful for you.

Tim, *please* trim quoted text that isn't relevant to your followup.
(And please consider whether olcott is worth any attention at all.)

-- 
Keith Thompson (The_Other_Keith) Keith.S.Thompson+u@gmail.com
void Void(void) { Void(); } /* The recursive call of the void */

[toc] | [prev] | [next] | [standalone]


Page 2 of 4 — ← Prev page 1 [2] 3 4  Next page →

Back to top | Article view | comp.lang.c


csiph-web