Re: Python from Wise Guy's Viewpoint

From: Erann Gat (gat_at_jpl.nasa.gov)
Date: 11/03/03 

Date: Mon, 03 Nov 2003 08:25:32 -0800

In article <3fa5e76b$1@news.unimelb.edu.au>, Fergus Henderson
<fjh@cs.mu.oz.au> wrote:

> gat@jpl.nasa.gov (Erann Gat) writes:
>
> >prunesquallor@comcast.net wrote:
> >
> >> the following paper discusses a technique finds an algorithm
> >> that is within a factor of 5 of the fastest algorithm that provably
> >> implements the formal spec.
> >
> >That is a truly remarkable result. I have taken only a brief look at this
> >paper and it doesn't come acros as immediately bogus, but I have a hard
> >time believing that it is true because if it were it seems to me that it
> >would provide the answer to, e.g. whether P=NP,
>
> It doesn't. What it does do is this: given a formal system F, it produces
> an algorithm A for solving NP-complete problems such that A is in P iff P=NP
> is provable in F. However, we don't know if A is actually in P or not,
> and finding out whether A is in P is no easier than finding out whether
> P=NP is provable in F.

That my well be, but according to what the abstract says (and what you
have said) I don't actually have to provide the proof that P=NP, the
algorithm will find that for me. So I'll give it the Peano axioms and ask
it to solve the traveling salesman problem. If it does so in polynomial
time (which can be determined empirically) then P=NP. If not, then we
have proof that P=NP is not provable in PA. Either way it's a major
breakthrough in mathetmatics, and the fact that it hasn't made the papers
indicates that it doesn't really do what the short description says it
does.

E.