Re: [isabelle] Target language bindings for rat



Dear Wenda, Michael and Mr. Douglas Maurer,

Thanks for your input.

The libraries for rational numbers in Isabelle and HOL4 are very similar, so I guess that it makes sense to add binding to Isabelle's implementation in the Eval target of the code generator (because Eval runs in the namespace of Isabelle, so everything is available. I still have to check whether this improves evaluation times at all (compared to using Code_Target_Int), because the code in rat.ML is in principle quite similar to what would be executed if we use the existing code setup for rat.

Meanwhile, I have started to setup bindings to Haskell and OCaml, and there I noticed a nice speedup (ca. 3X for Haskell and 10X for OCaml) over the existing setup for rat with Code_Target_Int in place.

As for the normalisation business, the current setup always reduces rational numbers to lowest terms. This is also what happens in the implementations in rat.ML and in HOL4. The Haskell standard library also does that (http://hackage.haskell.org/package/base-4.8.1.0/docs/src/GHC.Real.html#line-372). In OCaml's library Num, the user can set a flag whether rationals should be kept in lowest terms. It seems as if this is set to false by default. The Spire library for Scala also always reduces rationals (https://github.com/non/spire/blob/32345c24a598369388763abf7e5aed8621af1d15/core/shared/src/main/scala/spire/math/Rational.scala#L377).

For the target language bindings, we do not have to commit to any strategy, as long as the rationals are only manipulated by the target language library. Only when we convert them back into nominator and denominator in Isabelle, normalisation makes a difference. And it seems as if in this case (I guess a rather rare case) we can normalise if necessary.

Best,
Andreas

________________________________________
Von: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk]" im Auftrag von "W. Douglas Maurer [maurer at email.gwu.edu]
Gesendet: Freitag, 18. Dezember 2015 03:24
An: cl-isabelle-users at lists.cam.ac.uk
Betreff: Re: [isabelle] Target language bindings for rat

The main problem with standard treatments of rational numbers, as I see it, is: how often do you reduce to lowest terms? For example: (1/3+1/6)+1/2 -- do you reduce 1/3+1/6 to 1/2 immediately, and then add 1/2 to get 2/2, reducing to 1? Or do you leave 1/3+1/6 as 9/18 and then add 1/2 to get 36/36, reducing only at the end? The problem is that reducing to lowest terms is slow, in the worst case. You can ask the user when to reduce, potentially saving time, but would users necessarily know the best times to reduce? Is anyone aware of a good general solution to this problem? -WDMaurer





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