[r6rs-discuss] Re: Plausible list problems

From: William D Clinger <will>
Date: Wed Oct 4 08:42:25 2006

I am posting this as an individual member of the Scheme
community. I am not speaking for the R6RS editors.

Andre van Tonder wrote:
> An undecidable question cannot be proved false in a sound
> proof system, so are you allowing unsound proofs, and if so,
> which ones?

You are being silly.

Let P(m) be the proposition that states that Turing
machine m does *not* halt when started with a blank
tape. If m0 is a Turing machine that *does* halt
when started with a blank tape, then "not P(m0)" can
be proved by exhibiting the calculation of m0 upon
a blank tape.

For the higher order procedures that are described
in the draft R6RS, it is impossible to prove that
their list arguments are *not* plausible lists. On
the other hand, the algorithms used by list? and
length suffice to prove that they *are* plausible
lists in all cases for which, in my opinion, the
draft R6RS intends for the higher order procedures
not to raise an exception.

As I have stated several times now, the draft R6RS,
perhaps through obsession with the circumstances in
which procedures are required to raise an exception,
fails to state the circumstances in which the higher
order procedures are required *not* to raise an
exception. As I have stated several times now, the
circumstances in which these procedures are required
to raise an exception, together with the circumstances
in which these procedures are required not to raise
an exception, do not cover all cases; there remmains
a gap between the two, which corresponds to the
is-an-error situations of the R5RS. The draft R6RS
must be revised to acknowledge the is-an-error
situations.

Will
Received on Wed Oct 04 2006 - 08:42:19 UTC