[isabelle-dev] Alternative approach to »efficient« natural numbers
florian.haftmann at informatik.tu-muenchen.de
Sun Apr 29 15:51:26 CEST 2012
I did an experiment with Flyspeck-Tame (on macbroyXY):
Using the Efficient_Nat theory where Isabelle nat is directly
represented as PolyML int:
> Finished HOL-Flyspeck-Tame (11:50:46 elapsed time, 13:54:35 cpu time, factor 1.17)
Using the Target_Numeral theory where Isabelle nat is an abstract
datatype over PolyML int:
> Finished HOL-Flyspeck-Tame (10:55:49 elapsed time, 13:57:31 cpu time, factor 1.27)
The reason why this has the same magnitude of runtime is that in PolyML
trivial datatypes like
> datatype nat = Nat of int
> fun int_of (Nat k) = k
are optimized away.
This is a proof of concept that it is possible in the future to have
just *one* type which is mapped onto target language numerals by
default, and to refine nat and/or int to use this is implementation if
desired, rather than adhoc code_const setups etc. for nat and int. Cf.
P.S. This his no consequences for the upcoming release.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev