Re: Python from Wise Guy's Viewpoint

prunesquallor_at_comcast.net
Date: 11/03/03 

Date: Mon, 03 Nov 2003 15:08:33 GMT

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.

>> Assuming you have a provable formal specification of the collatz
>> problem,
>
> I'm not sure what you mean by a "provable" specification. The Collatz
> problem is extremely simple. See
> http://mathworld.wolfram.com/CollatzProblem.html

Yep, I'm familiar with it.

The problem with a `provable' specification is that it has shifted all
the correctness burden on the specification rather than the program.
So the program I write really doesn't have to do anything clever but
systematically look for answers and ask the specification if they are
correct. If the specification is provably correct, then the program
is.

>> 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, whether prime factoring
> really is hard, etc. etc.

It *could*, but you'd have to supply the proof in the specification!

There are a couple of `loopholes' in the paper. It requires a formal
specification, and there's the usual asymptotic and constant factor
stuff, but the big one is that it ignores those programs that are
correct, but for which a proof that they implement the specification
doesn't exist within the proof framework. (If it could find those,
then you'd be able to prove statements like `this statement is true
but not provable'.)

Relevant Pages

  • Re: Python from Wise Guys Viewpoint
    ... >> 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. ...
    (comp.lang.lisp)
  • Re: Computability in principle
    ... Fergus Henderson writes: ... >>If the formal spec is undecidable, then algorithms derived from it are ... > conforming to it are undecidable"? ... By `undecidable algorithm' I meant that the algorithm is equivalent to ...
    (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)