Re: [isabelle] Rational numbers in Isabelle/ML
On Sat, 2 Apr 2016, Manuel Eberl wrote:
I don't think this is relevant to isabelle-users. Rat is just one of many
auxiliary modules in the implementation.
I have one entry in the AFP already that uses rational numbers in ML,
and another AFP submission is in preparation. I think this is definitely
relevant to some Isabelle users (e.g. for automatically providing
witnesses for certain things; in my case, solutions to linear programs
and adequate interval splittings for Sturm's method).
I have nothing against just one high-quality Rat module in Isabelle/ML,
one that takes all previous experience into account and uses the current
possibilities of Poly/ML and Isabelle/ML.
Looking briefly through the sources raises the following questions:
* Is MyRat based on the existing Rat, or an independent development?
* What is the relation of Integer.lcm/gcd, PolyML.IntInf.lcm/gcd versus
MyRat.gcd? Could it be all based on PolyML.IntInf.lcm/gcd (taking care
about the proper sign)? PolyML.IntInf.lcm/gcd might lead to much
better performance, because it uses GMP operations directly.
* Rat.inv and MyRat.inv look odd to me, but for different reasons. Are
these actually correct?
How about a formally specified and verified implementation? It should be
mostly trivial with all the algebraic tools in Isabelle/HOL.
Some of the authors of the existing rat.ML should get involved.
This archive was generated by a fusion of
Pipermail (Mailman edition) and