Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with code generation for the reals

view this post on Zulip Email Gateway (Aug 19 2022 at 10:48):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jesus,

we were trying to generate code
for matrices of real numbers; we had been doing some experiments with
real numbers represented in SML by fractions of elements of type
"IntInf.int", but doing some profiling we detected that most of the
execution time was spent in computing the functions "gcd", "divmod",
"quotrem", "normalize" and so on, instead of on performing the
operations over matrices that were really interesting for us.

We thought that giving a chance to Code_Real_Approx_By_Float could be
worth (even if we read about its potential accuracy matters), just to
see if we could reduce computing times of the arithmetic operations.

Unfortunately, we got some problems with the Library, when generating
code, that we don't know how to avoid.

The sort answer: insert the following snippet at the beginning of your
example theory:

code_const Ratreal (SML)

definition Realfract :: "int ⇒ int ⇒ real"
where
"Realfract p q = of_int p / of_int q"

code_datatype Realfract

code_const Realfract
(SML "Real.fromInt _/ '// Real.fromInt _")

lemma [code]:
"Ratreal r = split Realfract (quotient_of r)"
by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)

lemma [code, code del]:
"(plus :: real ⇒ real ⇒ real) = plus"
..

lemma [code, code del]:
"(times :: real ⇒ real ⇒ real) = times"
..

lemma [code, code del]:
"(divide :: real ⇒ real ⇒ real) = divide"
..

lemma [code]:
fixes r :: real
shows "inverse r = 1 / r"
by (fact inverse_eq_divide)

Code_Real_Approx_By_Float seems indeed to be very approximative since it
cannot handle real numerals. This snippet amends this by a specific
datatype constructor Realfract which is then mapped to a SML expression.

This renders all code equations using the original datatype constructor
Ratreal invalid, and they must be dropped explicitly using the funny
[code, code del] pattern on reflexive equations. I added only the ones
necessary for your examples, their might be more. Inversions seems not
be implemented in Code_Real_Approx_By_Float, but it can be easily
delegated to division on reals which is.

@Johannes: Maybe this stuff should be added to Code_Real_Approx_By_Float?

In the file there can be also found some definitions from the SML
structure "Vector" (or type iarray, in Isabelle); we read your comment
on http://isabelle.in.tum.de/library/HOL/HOL-Library/IArray.html and
thought that the functions might be useful for someone else.

This is indeed work by Tobias. I did not experience any problem with it
in your examples.

To get back to your original observation:

we had been doing some experiments with
real numbers represented in SML by fractions of elements of type
"IntInf.int", but doing some profiling we detected that most of the
execution time was spent in computing the functions "gcd", "divmod",
"quotrem", "normalize" and so on, instead of on performing the
operations over matrices that were really interesting for us.

It is indeed questionable whether it is a good idea to normalize
quotients always. What do others implementations do here (e.g. Ocaml)?
The implementation of rational numbers can be changed in user space
using the usual mechanisms of datatype refinement (see the tutorial on
code generation and the upcoming ITP paper
http://isabelle.in.tum.de/~haftmann/pdf/data_refinement_haftmann_kuncar_krauss_nipkow.pdf).

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 10:49):

From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear all,

regarding the mail I sent to Florian, I just wanted to add some
figures about the performance of our algorithm computing the reduced
row echelon form of a matrix; the algorithm is refined to "iarrays"
(http://isabelle.in.tum.de/library/HOL/HOL-Library/IArray.html) to
represent matrices. We implemented the algorithm over fields, and
generated the ML code associated to the algorithm. We used MLton to
compile the code and execute it over some instances of matrices; the
results obtained when profiling are the following ones.

The following example is a randomly generated matrix of dimension
70*70 matrix with entries in the field "Z / 2Z"; these elements are
generated to "0::IntInf.int" and "1::IntInf.int", and the field
operations are defined by means of ad - hoc "fun" definitions
(execution time is 0.02 seconds).

(*
0.02 seconds of CPU time (0.00 seconds GC)
function cur raw

Sequence.tabulate 50.0% (0.01s)
example_70_x_70_Z2.plus_z2a 50.0% (0.01s)
*)

The following are the results obtained for the very same matrix as in
the previous example, but now the elements are labelled as being of
type "real"; following the standard setup for code generation of reals
they are generated in SML to fractions of "IntInf.int" (execution
time gets multiplied by 100, most of the time is spent in computing
quotients and remainders):

(*
2.46 seconds of CPU time (0.03 seconds GC)
function cur raw

Primitive.IntInf.bigQuot 28.1% (0.70s)
Primitive.IntInf.bigRem 28.1% (0.70s)
Primitive.IntInf.bigDivMod 12.4% (0.31s)
Primitive.IntInf.make 12.0% (0.30s)
example_70_x_70_binary_rat.abs_int 5.2% (0.13s)
example_70_x_70_binary_rat.sgn_int 3.6% (0.09s)
example_70_x_70_binary_rat.gcd_int 2.8% (0.07s)
example_70_x_70_binary_rat.divmod_int 2.0% (0.05s)
example_70_x_70_binary_rat.mod_int 1.6% (0.04s)
<gc> 1.2% (0.03s)
Sequence.tabulate 1.2% (0.03s)
example_70_x_70_binary_rat.div_int 0.4% (0.01s)
example_70_x_70_binary_rat.divmod_int.fn 0.4% (0.01s)
example_70_x_70_binary_rat.apsnd 0.4% (0.01s)
example_70_x_70_binary_rat.mult_iarray.fn.fn 0.4% (0.01s)
*)

Finally, this third example is the result of applying the algorithm to
a randomly generated "70*70" matrix, but in this case of real numbers
between 0 and 1000; they are again generated in SML to fractions of
"IntInf.int":

(*
46.14 seconds of CPU time (1.19 seconds GC)
function cur raw

Primitive.IntInf.bigRem 32.5% (15.37s)
Primitive.IntInf.bigQuot 24.2% (11.46s)
Primitive.IntInf.make 11.3% (5.37s)
Primitive.IntInf.bigDivMod 9.5% (4.51s)
example_70_x_70_rat.sgn_int 7.6% (3.62s)
example_70_x_70_rat.abs_int 6.1% (2.87s)
example_70_x_70_rat.divmod_int 2.9% (1.35s)
<gc> 2.5% (1.19s)
example_70_x_70_rat.gcd_int 1.4% (0.65s)
example_70_x_70_rat.mod_int 0.9% (0.43s)
example_70_x_70_rat.divmod_int.fn 0.7% (0.34s)
example_70_x_70_rat.apsnd 0.3% (0.12s)
Sequence.sub 0.0% (0.01s)
example_70_x_70_rat.plus_rata 0.0% (0.01s)
example_70_x_70_rat.uminus_rata 0.0% (0.01s)
example_70_x_70_rat.div_int 0.0% (0.01s)
Primitive.IntInf.extdFromWord32 0.0% (0.01s)
*)

We thought that, in order to increase performance, it could be a good
idea to try to use the SML "Real" type (as proposed in
http://isabelle.in.tum.de/library/HOL/HOL-Library/Code_Real_Approx_By_Float.html),
instead of fractions of "IntInf.int". Any other ideas would be also
warmly welcome.

Any suggestions are welcome,

Jesus

view this post on Zulip Email Gateway (Aug 19 2022 at 11:08):

From: Makarius <makarius@sketis.net>
Just curious: How does that compared to Poly/ML, instead of Mlton? It is
important here to distinguish Poly/ML with GNU MP and without. (The
version that is shipped with Isabelle2013 includes libgmp only for Linux,
and it should work for Windows/Cygwin as well, but not for Mac OS X -- I
did not know how to compile that in a portable manner.)

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 11:10):

From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Hi Makarius,

the times compare as follows; a matrix of dimension 70 * 70 of real
numbers (randomly generated, with entries between 0 and 1000) mapped
to fractions of "IntInf.int" elements takes:

Thanks for your interest,

Jesus

Last updated: Apr 25 2024 at 04:18 UTC