Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Re: [isabelle] Problems with code generation for the reals
7 views
Skip to first unread message
Florian Haftmann
Apr 27, 2013, 9:15:14 AM4/27/13
to Jesus Aransay, USR Isabelle Mailinglist, Johannes Hoelzl
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
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 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
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Jesus Aransay
Apr 29, 2013, 2:08:00 PM4/29/13
to Florian Haftmann, USR Isabelle Mailinglist
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
On Sat, Apr 27, 2013 at 3:03 PM, Florian Haftmann
<florian....@informatik.tu-muenchen.de> wrote:
> Hi Jesus,
>...
Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-mar...@unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España
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
On Sat, Apr 27, 2013 at 3:03 PM, Florian Haftmann
<florian....@informatik.tu-muenchen.de> wrote:
> Hi Jesus,
>...
>
> 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
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
--
> 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
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-mar...@unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España
Makarius
May 21, 2013, 8:48:21 AM5/21/13
to Jesus Aransay, USR Isabelle Mailinglist
On Mon, 29 Apr 2013, Jesus Aransay wrote:
> 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.
> 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 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):
Just curious: How does that compared to Poly/ML, instead of Mlton? It is
> 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):
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
Jesus Aransay
May 22, 2013, 5:55:00 AM5/22/13
to Makarius, USR Isabelle Mailinglist
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:
- with MLton, 9 seconds to compile the stand-alone executable, 45
seconds of execution;
- with PolyML 5.5 (the version dispatched with Isabelle 2013), 111
seconds of execution;
- just for the record, with PolyML 5.2 (the version packaged for
ubuntu), 350 seconds of execution.
Thanks for your interest,
Jesus
--
Jes�s Mar�a Aransay Azofra
Universidad de La Rioja
Dpto. de Matem�ticas y Computaci�n
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:
- with MLton, 9 seconds to compile the stand-alone executable, 45
seconds of execution;
- with PolyML 5.5 (the version dispatched with Isabelle 2013), 111
seconds of execution;
- just for the record, with PolyML 5.2 (the version packaged for
ubuntu), 350 seconds of execution.
Thanks for your interest,
Jesus
Jes�s Mar�a Aransay Azofra
Universidad de La Rioja
Dpto. de Matem�ticas y Computaci�n
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-mar...@unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logro�o, Espa�a
mail: jesus-mar...@unirioja.es ; web: http://www.unirioja.es/cu/jearansa
0 new messages