Re: Python from Wise Guy's Viewpoint

prunesquallor_at_comcast.net
Date: 11/03/03 

Date: Mon, 03 Nov 2003 18:53:47 GMT

gat@jpl.nasa.gov (Erann Gat) writes:

> In article <ptg9zdzk.fsf@comcast.net>, prunesquallor@comcast.net wrote:
>
>> gat@jpl.nasa.gov (Erann Gat) writes:
>>
>> > In article <znfelp34.fsf@comcast.net>, prunesquallor@comcast.net wrote:
>> >
>> >> gat@jpl.nasa.gov (Erann Gat) writes:
>> >>
>> >> >
>> >> > SATISFIES-SPEC is undefined. And would you kindly show me the adaptation
>> >> > that solves the collatz problem? That encrypts text according to the
>> >> > rijndael algorithm? That filters spam?
>> >>
>> >> Certainly. Oh, wait, *you* have to supply the formal specification, I
>> >> just supply the algorithm that solves it.
>> >
>> > Fine, but you still have to write SATISFIES-SPEC first.
>>
>> If the specification is formal, then it can algorithmically decide
>> if a putative input/output pair is indeed correct. So I'll just
>> generate putative outputs and funcall your spec until I get one
>> that matches.
>
> Ah, but now you've added an additional constraint, namely, that my spec be
> funcallable. Not all formal specifications can be rendered as functions.
> For example, "This program terminates" can be formally rendered, but not
> as a program.

I think we're using different definitions of `formal'.

A `formal' spec would consist of a series of algorithmically
verifiable assertions. A termination statement in your spec would not
be algorithmically verifiable.

>> > 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, whether prime factoring
>> > really is hard, etc. etc.
>>
>> It *could*, but you'd have to supply the proof in the specification!
>
> That's not what the abstract says. It only says that you have to provide
> a formal system in which the correctness of the fastest algorithm can be
> proven, not the proof itself. The paper's algorithm purports to do that
> for you. What's more, it purports to do so in time that is within a
> factor of 5 of the fastest algorithm for solving the problem itself plus a
> (presumably very large) constant! If this were true, it would be a
> constructive proof that the question of whether P=NP is tractable, though
> to actally get the answer you'd have to run the program, which could take
> a long time. Still, a constructive proof that P=NP is decidable would be
> big, big news.
>
> E.

Here's the abstract:

    An algorithm M is described that solves any well-defined problem p
    as quickly as the fastest algorithm computing a solution to p,
    save for a factor of 5 and low-order additive terms. M optimally
    distributes resources between the execution of provably correct
    p-solving programs and an enumeration of all proofs, including
    relevant proofs of program correctness and of time bounds on
    program runtimes. M avoids Blum's speed-up theorem by ignoring
    programs without correctness proof. M has broader applicability
    and can be faster than Levin's universal search, the fastest
    method for inverting functions save for a large multiplicative
    constant. An extension of Kolmogorov complexity and two novel
    natural measures of function complexity are used to show that the
    most efficient program computing some function f is also among the
    shortest programs provably computing f.

So it requires that p is a `well defined problem', *and* it only
searches those algorithms that have correctness proofs.

If your problem is undecidable within your formal framework, then it
isn't well-defined, and this algorithm won't help.

Relevant Pages

  • Re: Test Driven Development Sample (Yet Another Pet Example)
    ... If the algorithm is flawed, it is still possible that it ... The key words here are "correct subsequence"...as RDM pointed out, ... Nope...wasn't part of the spec or needed at this time. ... > And you'd have to survive waiting for the results of any conclusive ...
    (comp.object)
  • Re: Blowfish Sign Extension implementation risk
    ... Usual approach is to specify the algorithm in a computer-understandable ... Some people work on proofs of program correctness: ... with more low-level languages like C, ... one could try to design the algorithm ...
    (sci.crypt)
  • Re: JSH: Weird feeling
    ... I recall, back when you claimed to find a polynomial algorithm for TSP, that you gave "proofs" of correctness for your algorithms, algorithms that were later shown to be incorrect. ... My family's too spread out to be killed with a bomb. ... Intelligence services need to note that I have ...
    (sci.math)
  • Re: Hash functions (was: Maximum String size in Java?)
    ... > "Even though a hash table is a fairly wonderful data structure, ... correctness are, which implies simplicity and consistency of the ... It doesn't take long for an Oalgorithm to become unusable, ... the broken "Reply" link at the bottom of the article. ...
    (comp.programming)
  • Re: Proof of Algorithm correctness
    ... >>sort algorithm), but want to see a proof for substantial programs. ... >>prove program correctness in certain cases, ... written in a first order language - then show that the invariant is ... a few first order expressions: one that describes the necessary state ...
    (sci.math.research)