Re: Bob's 'Self-aggrandizing ignorant' Count: Was: What databases have taught me

Bob Badour wrote:

[ snippage ]

> I don't necessarily agree with the statement that some algorithms are
> implicitly imperative or procedural in nature on the basis of possible
> implementations in PROLOG. Even if they are imperative, this does not
> preclude declarative solutions because a language can be both imperative
> and declarative, and one can imagine other non-procedural languages than
> PROLOG.
>

Given that all Turing complete languages compute the same functions, I think this comes down to the fuzzy notion of convenience; some algorithms *might* be "conveniently" described in an imperative manner. But this will vary from programmer to programmer.

[ snippage ]

> These observations naturally lead one to two important questions:
>
> 1) Can one create a pair of languages where the proofs written in one
> language establish the correct outcome and where some other language
> instructs the compiler on how to implement to get the best possible
> performance?
>

Just to be sure I'm reading you correctly; you want to write proofs in language (a). Some other language (b) then provides hints to a compiler for language (a) on optimising proofs for some or other machine architecture (c). (In which case, wouldn't (b) normally just be the optimising stage on a compiler ?) Or would you want to effectively hand-optimise by writing your own optimiser hints for architecture (c) in language (b) for a particular proof in language (a) ? Basically, is a program a pair of (proof in (a), hints in (b)) ?

> 2) Could one create a compiler to translate proofs as above in 1) into
> assembler code with an automated proof that the maximum number of CPU
> cycles consumed in the worst-case situation would not exceed some threshold?
>

The first part sounds like a compiler, with a customisable optimiser. The second part sounds like a job for abstract interpretation & static analysis - just beware of the halting problem & Rice's theorem waiting to pounce.

> These then lead into a third question: Can one combine the above
> features in a single product?
>

Possibly. Partial evaluators sounded bizarre to me until I got my head around them (to some extent, anyway). Received on Fri Jun 30 2006 - 18:20:13 CDT