Re: [isabelle] Numerical Recipes in Isabelle



> this is possible in Isabelle, though it might be a little bit harder and
> cumbersome than you might imagine and the resulting code is not as
> efficient as you would like it to be :-) Recently there has been work on
> computing with floating point numbers in Isabelle, and stuff like
> Taylor-approximation is available now, I think (though I do not know how
> accessibly packaged this is).

Very nicely.

> There is one efficiency problem: To my knowledge sabelle does not
> directly deal with the usual IEEE floats and doubles, but uses a pair of
> arbitrary size integers to encode a float. This and the fact that your
> code will be functional code (as opposed to imperative code) will make
> the compiled code way slower than if coded for example in C.

Generating code with floats and doubles is not an issue. Of course you
need a theory of IEEE 754 to base your verification on. There are some
in HOL (which would not be hard to port to Isabelle).

You avoided machine floats because you wanted to rely on as few trusted
components as possible (which is the Coq/HOL/Isabelle tradition). But
for Numerical Recipes this would be unnatural and would appear esoteric
to that community.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.