Email Gateway (Aug 22 2022 at 12:02): Email Gateway (Aug 22 2022 at 12:02):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I am looking for bindings of rational numbers to the target languages of the code
generator. Has anyone done something in this direction? E.g., something analogous to
Code_Numeral.integer and Code_Target_Int.thy?
Haskell and OCaml support arbitrary-precision rational numbers in their libraries
(Rational and Num.num) and there is a library for Scala (https://github.com/non/spire),
but I have not found anything for SML. Does anyone know of such a library for SML?
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:03):From: Wenda Li <wl302@cam.ac.uk>
Hi Andreas,
As far as I know, src/Tools/rat.ML is an implementation of rational
number in Isabelle/ML and MetiTarski
(https://bitbucket.org/lcpaulson/metitarski/src) uses another
implementation that is inherited from John Harrison somehow.
I have considered this question before, but considering there is no
standard implementation of rational number in the standard PolyML
library, I thought it is risky to do such binding...
Hope this helps,
Wenda
Email Gateway (Aug 22 2022 at 12:03):From: Michael Norrish <Michael.Norrish@nicta.com.au>
There is an implementation used in HOL4 at
https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/portableML/Arbrat.{sig,sml}
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:03):From: "W. Douglas Maurer" <maurer@email.gwu.edu>
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
Sent from my iPhone
Email Gateway (Aug 22 2022 at 12:03):From: Lochbihler Andreas <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 12:03):From: Manuel Eberl <eberlm@in.tum.de>
My own, perhaps somewhat naïve, thoughts on this: What is the advantage
of using target-language rats? Are they really faster than the code that
Isabelle produces?
Intuitively, I would think that the basic operations on rational numbers
translate to operations on integers very clearly and obviously and that
there is not much room for creativity – except for the question of if
and when to reduce the numerator and denominator.
A FFI-based implementation using the GNU Multiple Precision Arithmetic
Library (GMP) might be faster because it reduces overhead, but even
Haskell (which uses GMP for its integers) does not do that and relies on
‘pure’ rational numbers implemented as a datatype instead.
On the question of normalisation, let me remark that the GMP always
assumes that rats are in canonical form and also brings all results into
canonical form, and the GMP people generally seem know their stuff, so
this is probably a good idea. (I think they also offer ‘raw’ functions
without this normalisation though)
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 12:03):From: Manuel Eberl <eberlm@in.tum.de>
the existing setup for rat with Code_Target_Int in place.
I find that a bit surprising, considering how rats are implemented in
Haskell. One possible explanation that I have is that perhaps the
exported code uses Isabelle's GCD operation on natural numbers, whereas
the Haskell version uses the GCD operation that GMP provides, and which
is probably much faster.
Another possible reason is perhaps some issue with lazyness; Haskell's
"Ratio" datatype is declared with strict fields, whereas Isabelle
probably declares "rat" with the lazy fields. Perhaps this can cause
large unevaluated chunks to hang around longer than they should?
However, the fact that the difference is even more pronounced in OCaml
seems to speak against that. I don't know the OCaml implementation, so I
don't know if the GCD thing might also be an explanation there.
Email Gateway (Aug 22 2022 at 12:03):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
On 18/12/15 09:29, Manuel Eberl wrote:
On 18/12/15 09:01, Lochbihler Andreas wrote:
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.I find that a bit surprising, considering how rats are implemented in
Haskell. One possible explanation that I have is that perhaps the
exported code uses Isabelle's GCD operation on natural numbers, whereas
the Haskell version uses the GCD operation that GMP provides, and which
is probably much faster.
Your guess seems to be right. If I serialise the gcd operation on integer to the target
language implementation, the differences almost vanish.
Another possible reason is perhaps some issue with lazyness; Haskell's
"Ratio" datatype is declared with strict fields, whereas Isabelle
probably declares "rat" with the lazy fields. Perhaps this can cause
large unevaluated chunks to hang around longer than they should?However, the fact that the difference is even more pronounced in OCaml
seems to speak against that. I don't know the OCaml implementation, so I
don't know if the GCD thing might also be an explanation there.It is.
Thanks,
Andreas
Email Gateway (Aug 22 2022 at 12:04):From: Jose Divasón <jose.divasonm@unirioja.es>
Dear all,
in my AFP about the Gauss-Jordan algorithm I worked with rational matrices,
so I serialised the rational numbers from Isabelle to Haskell, see:
http://afp.sourceforge.net/browser_info/current/AFP/Gauss_Jordan/Code_Rational.html
For exporting code to SML, I just used the file Code_Target_Int together
with serialisations from gcd to PolyML.IntInf.gcd and MLton.IntInf.gcd (as
far as I know, there is no gcd implementation in the standard library). I
also serialised the operations div and mod, see
http://afp.sourceforge.net/browser_info/current/AFP/Gauss_Jordan/Code_Generation_IArrays_SML.html.
Without such GCD serialisations, i.e. only using Code_Target_Int, times
were 20 times slower in my case.
Best,
Jose
Email Gateway (Aug 22 2022 at 12:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jose,
Did you measure how much you gained from serialising rat to Haskell's Rational type
(compared with using Code_Target_Int plus an appropriate setup to implement gcd on integer
and int with Prelude.gcd)? In my quick experiment this morning, I could not see a
significant speed-up.
I was also a bit surprised by your comparison of serialisation options for divmod_integer
in Code_Generation_IArrays_SML. In SML, quotRem and divMod behave differently when it
comes to negative numbers. In that respect, quotRem is the wrong choice. For example,
quotRem (~10, 6) evaluates to (~4, ~6) and divMod (~10, 6) to (~2, 2). In Isabelle/HOL,
value [nbe] "divmod_integer (-10, 6)" gives (-2, 2). So the generated code may actually
return a different result than what you have proved. (I do not know whether such negative
numbers can occur in your application).
Given that the generated ML code should work for all ML systems, I think we cannot take
the serialisations of gcd into the distribution by default.
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:04):From: Jose Divasón <jose.divasonm@unirioja.es>
Dear Andreas,
Did you measure how much you gained from serialising rat to Haskell's
Rational type (compared with using Code_Target_Int plus an appropriate
setup to implement gcd on integer and int with Prelude.gcd)? In my quick
experiment this morning, I could not see a significant speed-up.
Yes, I did. I also carried out quick experiments and noticed more or less
the same as you: Haskell's Rational type was just a little bit faster,
almost insignificant.
I was also a bit surprised by your comparison of serialisation options for
divmod_integer in Code_Generation_IArrays_SML. In SML, quotRem and divMod
behave differently when it comes to negative numbers. In that respect,
quotRem is the wrong choice. For example,
quotRem (~10, 6) evaluates to (~4, ~6) and divMod (~10, 6) to (~2, 2). In
Isabelle/HOL,
value [nbe] "divmod_integer (-10, 6)" gives (-2, 2). So the generated code
may actually return a different result than what you have proved. (I do not
know whether such negative numbers can occur in your application).
Good point, let me take a glance at it.
Given that the generated ML code should work for all ML systems, I think
we cannot take the serialisations of gcd into the distribution by default.
Yes, you are completely right. Each time I exported code, I had to decide
which serialisation was going to be used depending on the ML interpreter.
Best,
Jose
Email Gateway (Aug 22 2022 at 12:04):From: Jose Divasón <jose.divasonm@unirioja.es>
I think it works for my concrete case (integer numbers are only used for
representing rational numbers), however for a general integer manipulation
this is not a correct serialisation.
In my exported code, quot is only used when nomalising rational numbers (by
means of the Rat.normalise definition). If I am not wrong, for such a
function it is the same using "div" as using "quot".
So, "-20 div 6" would return different results (as expected), but normalize
(-20,6) the same:
code_printing
constant "op div :: integer => _ => _" ⇀ (SML) "(IntInf.div ((_), (_)))"
| constant "op mod :: integer => _ => _" ⇀ (SML) "(IntInf.mod ((_), (_)))"
value[code] "-20 div 6::int" (Result: - 4)
value[code] "Rat.normalize (-20,6)" (Result: (-10,3) :: "int × int")
code_printing
constant "op div :: integer => _ => _" ⇀ (SML) "(IntInf.quot ((_), (_)))"
| constant "op mod :: integer => _ => _" ⇀ (SML) "(IntInf.rem ((_), (_)))"
value[code] "-20 div 6::int" (Result: - 3 :: "int")
value[code] "Rat.normalize (-20,6)" (Result: (-10,3) :: "int × int")
Then, I took advantage of it and decided to use quot, since it is supposed
to be faster. Nevertheless, I have to study it carefully again because
maybe I am wrong.
Best,
Jose
Email Gateway (Aug 22 2022 at 12:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jose,
Rat.normalise only divides by divisors, so the remainder is always 0 and the problem
should not occur in this case.
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:05):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
concerning division on integers, I also observed some optimization potential, which is save in a way that
it only invokes the divmod on positive numbers. At least
in my application gave a significant speedup, cf.
http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Improved_Code_Equations.html
Cheers,
René
Last updated: Apr 19 2024 at 08:19 UTC