Re: [isabelle] Rational numbers in Isabelle/ML
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".
* Is MyRat based on the existing Rat, or an independent development?
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
* 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
about the proper sign)? PolyML.IntInf.lcm/gcd might lead to much
better performance, because it uses GMP operations directly.
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.
* 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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and