Re: [isabelle] Efficient Lookups in Lists



There is one more solution possibility, you could use the compute oracle in Pure/Tools/compute.ML. It is already included in your Isabelle build (so it is somewhere between the "trusted base" and the rest :-)),
you can invoke it by calling once

Compute.basic_make ....

and then each time you simplify a term by

Compute.rewrite ...

There are two major drawbacks to this method:

1. You can only simplify terms which contain no type variables.
2. You have to configure the rewrite by calling Compute.basic_make and give it ALL the theorems used for rewriting;
   these theorems must not contain type variables, either;

The no-type-variables limitation in 2) is not so bad if you know what types you can possibly have in your terms; you can just instantiate the polymorphic rewrite theorems with all types you need and give these to Compute.basic_make.

I have used above technique successfully for fast matrix multiplication, gaining a speed-up-factor comparable to compilation. It is more trustworthy than compilation, though, because it builds directly on Pure and makes no additional assumptions.


Steven





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