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 MHonArc.