Re: Computability in principle

From: Joe Marshall (jrm_at_ccs.neu.edu)
Date: 11/10/03 

Date: Mon, 10 Nov 2003 16:16:25 -0500

Fergus Henderson <fjh@cs.mu.oz.au> writes:

> Joe Marshall <jrm@ccs.neu.edu> writes:
>
>>Matthias Blume <find@my.address.elsewhere> writes:
>>
>>> Indeed, if you know that there are always satisfying elements, and
>>> that for some of them there is a proof of correctness, then your
>>> technique would work.
>>
>>Yes. I think that this is one of the restrictions on the
>>`M-algorithm' that we were discussing so long ago. It can generate a
>>program within a factor of 5 of optimal from a constructive proof,
>
> Two points. First, don't forget the constant factor -- it's important!

Yeah, yeah. My point is *not* to defend this! This M-algorithm is
cute for the problems that it solves, but it only solves
`well-defined' problems.

> I think you are misremembering. The M-algorithm takes as input an
> algorithm, not a constructive proof.

Here's what the paper says:
  ``Given a formal specification of a problem depending on some
    parameter x (element of X), we are interested in a fast algorithm
    computing solution y (element of Y). This means that we are
    interested in a fast algorithm computing f: X->Y, where f is a
    formal (logical, mathematical, not necessarily algorithmic),
    specification of the problem.''

So f is some formal specification, not necessarily an algorithm, but
necessarily something you could manipulate with a computer.

> No, this is wrong/meaningless. As we discussed already,
> there is no easy way to use the M-algorithm to determine if P=NP.

I *know* that M-algorithm cannot solve P=NP (probably, it could be
that P *does* = NP and that this is provable, but assuming that it
isn't). Given that it *can* solve well-defined problems for which it
can find a proof, then `P=NP' must not be `well-defined' `formal
specification' of the problem.
 

Relevant Pages

  • Re: Computability in principle
    ... >> algorithm, not a constructive proof. ... > ``Given a formal specification of a problem depending on some ... the fastest algorithm computing a solution* ... ...
    (comp.lang.lisp)
  • Re: Python from Wise Guys Viewpoint
    ... > if a putative input/output pair is indeed correct. ... I can render any specification ... a formal system in which the correctness of the fastest algorithm can be ... a constructive proof that P=NP is decidable would be ...
    (comp.lang.lisp)
  • Re: Python from Wise Guys Viewpoint
    ... > that solves the collatz problem? ... just supply the algorithm that solves it. ... Assuming you have a provable formal specification of the collatz ... journal = "International Journal of Foundations of Computer Science", ...
    (comp.lang.lisp)
  • Re: ZFC
    ... there is a long running tradition that constructive proof = ... > constructive proof of an AE-statement yields an algorithm, ... wasting my CPU time. ...
    (comp.theory)
  • Re: symplectic group generators
    ... > is given an arbitrary symplectic matrix, an algorithm to express it in ... This topic should be included in any basic publication on Siegel modular ...
    (sci.math.research)