Re: [isabelle] Rational numbers in Isabelle/ML




  * Is MyRat based on the existing Rat, or an independent development?
It's independent; I only found out that there was one in Isabelle after I'd written my own. I didn't think to look in "src/Tools".

  * 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.
Probably. I didn't know Poly/ML already had GMP bindings; in that case, one could probably use GMP rationals directly, which might increase performance further. This is probably something that we could suggest to David Matthews.



  * Rat.inv and MyRat.inv look odd to me, but for different reasons.  Are
    these actually correct?
There is a ~ missing in MyRat.inv. That code should definitely receive a thorough review before it goes anywhere. Rat.inv looks fine to me.

How about a formally specified and verified implementation? It should be mostly trivial with all the algebraic tools in Isabelle/HOL.
Well, we have a rational number type in Isabelle/HOL with working code equations. If I recall correctly, the performance was almost as good as Haskell's (unverified) rational number implementation. (modulo using the unverified gcd operation from GMP). However, I would imagine that the exported could would be quite ugly.


Manuel




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