From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 10db24,77f71d0bde4c5bb4
X-Google-Attributes: gid10db24,public
X-Google-Thread: 103376,86fd56abf3579c34
X-Google-Attributes: gid103376,public
From: dewar@cs.nyu.edu (Robert Dewar)
Subject: Re: What good is halting prob?
Date: 1995/04/20
Message-ID: <dewar.798381929@gnat>#1/1
X-Deja-AN: 101283209
references: <3kaksj$iur@isnews.calpoly.edu> <3mve9b$gaj@news.cais.com>
 <cppD7880n.32B@netcom.com> <3n285v$9vl@news.cais.com>
 <cppD7BMpM.39p@netcom.com>
organization: Courant Institute of Mathematical Sciences
newsgroups: comp.lang.ada,comp.edu
Date: 1995-04-20T00:00:00+00:00
List-Id: <comp.lang.ada>

Robin is certainly right to point out that a program on its own cannot
usefully be said to be correct or incorrect, there must be an accompanying
specification. Still I don't see that this means that correctness is
subjective. Not at all, it is an objective function

    Correct (P : Program; S : Specification) return Boolean;

of course the halting problem says that we cannot provide a full
implementation of correct.

But that brings up another point. Of course correctness is (pretty
trivially) equivalent to the halting problem, and thus is undecidable.

But Robin, don't make the mistake of assuming that because a problem is
undecidable it is impossible to write a program that decides it in 
most or some cases.

For any given instance of the halting problem, there is of course an answer.
Either the program halts or it does not halt. Furthermore there is a trivial
program, for a particular instance of the halting problem, that gives the
right answer (it is one of the following:

    return True
or
    return False

of course it may be hard to tell which of these two giving the right answer!

Suppose now we go back to our correctness function:

    program x spec => boolean

obviously we can't write this program in a way that it always works, but
we could write a program which would do one of three things:

   result in true
   result in false
   go into an infinite loop

in fact it is not hard to write this program, we just enumerate proofs till
we find one that proves correctness or incorrectness (at least I should say
not hard conceptually, the mechanics of this program would of course be
formidable).

So that's an important lesson, just because something is equivalent tto the
halting problem does not mean that we can't write a program for it, it just
means that the program can't possibly work in all cases.

So it would be a good idea to change the spec of our correctness procedure
to return a type

  type result is (correct, incorrect, cannot_tell)

instead of boolean.

and expect it to generate a proof along with correct, a counter-example
along with incorrect.

then our task as a programmer is simply to avoid the cannot_tell cases
in our programs if we are interested in correct programs. We may have
to discard some perfectly good and correct programs, but a correct program
that you cannot convince anyone else is correct is a dubious beast.