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



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

Attachment: signature.asc
Description: OpenPGP digital signature



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