# 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.
Makarius

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