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

Groups > comp.lang.c > #159303

Re: A small, slightly meta-, question

Show all headers | View raw

Ben Bacarisse <ben.usenet@bsb.me.uk> wrote:
> John Forkosh <forkosh@panix.com> writes:
>> David Brown <david.brown@hesbynett.no> wrote:
>>> Mark Bluemel wrote:
>>>> Is there any value in trying to understand Pete Olcott's posts?
>>> 
>>> No. He is wrong. It's not difficult to prove that the halting problem
>>> cannot be solved, [...]
>>
>> And since this is comp.lang.c, here's a little C program to prove it
>> by contradiction (though it might equally as well be Fortran, etc).
>>    Suppose you claim to have a function  int ishalts(char *filename)
>> that reads a C program from filename and returns 1=the program in
>> filename eventually halts, 0=it never halts, and -1=filename doesn't
>> contain a valid C program (just so ishalts() is a total function
>> from all_possible_strings-->{1,0,-1} rather than a partial function).
> 
> Just because detail often get in the way, it's simpler to make it a
> total function by saying that it returns 1 if the argument is a halting
> C program and 0 otherwise.
> 
>>    And now write the following 5-line C program, save it in doIhalt.c,
>> having it submit itself to ishalts() as follows.
>>    /* save this program in file doIhalt.c */
>>    #include <stdio.h>
>>    int main ( int argc, char *argv[] ) {
>>       int ishalts(char *);
>>       while ( ishalts("doIhalt.c") == 1 ) continue;
>>       exit; }
>>    /* end-of-file */

> exit is a function, not a statement.
Yeah, as mentioned below, I saw this somewhere but (still) can't
recall where. And I was trying to recall it while writing all this,
and seemed to recall the original example was in Fortran
(is that what you also recall seeing???). And I must have been
subconsciously channeling "CALL EXIT" when I wrote that (without
the "()").

> I'd ditch it, the include and the parameters to main:
>     /* save this program in file doIhalt.c */
>     int main(void) {
>        int ishalts(char *);
>        while (ishalts("doIhalt.c") == 1) continue; }
> again, just to remove as much extraneous detail as possible.
> 
>> So the program never halts if ishalts() claims that it eventually halts,
>> and it immediately halts if ishalts() claims it never halts.
>> Thus no such function ishalts() can exist with the claimed functionality.
>> (I saw this example somewhere, but don't recall where.)
> 
> I think I have as well.  The trouble is that using the file name to "tie
> the knot" is really a cheat.  Not a cheat in a bad way (the argument is
> sound and the conclusion is correct) but a student might well wonder if
> halting for C programs is due to the fact that programs can be put into
> named files, and other models, that don't have named files, would not be
> subject to the same argument.

With your repeated interest in students, my original thought about
all this (which I didn't originally mention since, as I did mention,
this is comp.lang.c) is that it's a nice segue to the curry-howard
isomorphism,
   https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
-- 
John Forkosh  ( mailto:  j@f.com  where j=john and f=forkosh )

Back to comp.lang.c | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

A small, slightly meta-, question Mark Bluemel <mark.bluemel@gmail.com> - 2021-03-10 00:18 -0800
  Re: A small, slightly meta-, question Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2021-03-10 00:20 -0800
    Re: A small, slightly meta-, question Jorgen Grahn <grahn+nntp@snipabacken.se> - 2021-03-11 21:24 +0000
      Re: A small, slightly meta-, question om@iki.fi (Otto J. Makela) - 2021-03-15 14:40 +0200
  Re: A small, slightly meta-, question "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2021-03-10 00:30 -0800
  Re: A small, slightly meta-, question David Brown <david.brown@hesbynett.no> - 2021-03-10 10:04 +0100
    Re: A small, slightly meta-, question "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2021-03-10 20:40 -0800
    Re: A small, slightly meta-, question John Forkosh <forkosh@panix.com> - 2021-03-11 06:42 +0000
      Re: A small, slightly meta-, question Ben Bacarisse <ben.usenet@bsb.me.uk> - 2021-03-11 10:48 +0000
        Re: A small, slightly meta-, question Manfred <noname@add.invalid> - 2021-03-11 16:04 +0100
          Re: A small, slightly meta-, question Ben Bacarisse <ben.usenet@bsb.me.uk> - 2021-03-11 21:57 +0000
        Re: A small, slightly meta-, question John Forkosh <forkosh@panix.com> - 2021-03-12 06:29 +0000
  Re: A small, slightly meta-, question Malcolm McLean <malcolm.arthur.mclean@gmail.com> - 2021-03-10 05:51 -0800
    Re: A small, slightly meta-, question David Brown <david.brown@hesbynett.no> - 2021-03-10 16:03 +0100
  Re: A small, slightly meta-, question Bonita Montero <Bonita.Montero@gmail.com> - 2021-03-10 15:50 +0100
    Re: A small, slightly meta-, question Anton Shepelev <anton.txt@g{oogle}mail.com> - 2021-03-10 17:53 +0300
      Re: A small, slightly meta-, question Dolores Filandro <dolfiland8@gmail.com> - 2021-03-13 18:49 -0800
    Re: A small, slightly meta-, question "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2021-03-10 20:41 -0800
  Re: A small, slightly meta-, question Joe Pfeiffer <pfeiffer@cs.nmsu.edu> - 2021-03-10 08:54 -0700
  Re: A small, slightly meta-, question "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2021-03-14 19:33 -0700

csiph-web