Ok.

But really, you should use ZArith, which is much more modern, faster and well-maintained than Big_int.

On 10/25/2016 06:58 PM, Tung Vu Xuan wrote:
Hi, 

Thanks for suggestions. Since I am using a library for interval arithmetic [1], your idea becomes easier for me.

let intv_of_big_int bi = 
    let n = Big_int.num_bits_big_int bi in
    if n <= 53 then 
      let bi_float = Big_int.float_of_big_int bi in
      {low=bi_float;high=bi_float}
    else begin
      let n = n - 53 in
      (* Extract top 53 bits of x *)
      let top = Big_int.shift_right_big_int bi n in

      let top_float = Big_int.float_of_big_int top in
      (* interval [2, 2] *)
      let two_I = {low=2.;high=2.} in
      (* interval: [2, 2]**n *)
      let two_I_to_n = pow_I_i two_I n in

      (* compute upper bound of mantissa, represented as an intv *)
      (* interval arithmetic is needed because rounding error might occur *)
      let mantissa_upper_bound_intv = {low=top_float;high=top_float} +$ one_I in

      (* intv of mantissa *)
      let mantissa_intv = {low=top_float; high=mantissa_upper_bound_intv.high} in
      
      (* compute final interval *)
      mantissa_intv *$ two_I_to_n
    end

[1] Alliot, J.M., Gotteland, J.B., Vanaret, C., Durand, N., Gianazza, D.: Implementing an interval computation library for OCaml on x86/amd64 architectures. In: ICFP. ACM (2012)

Thanks again,
Tung.

On Tue, Oct 25, 2016 at 5:28 PM, Soegtrop, Michael <michael.soegtrop@intel.com> wrote:

Dear Jacques-Henri,

 

if the number is cut off after n digits, the upper and lower bounds I suggested are the (truncated integer)*10^(#cut-off-digits) and (truncated integer+1)*10^(#cut-off-digits). The true number is obviously between these two. Since the integer has higher precision than the mantissa in the case of cut off, this is only a fraction of a mantissa bit. The errors you get by multiplying with the powers of 10 is likely larger in most cases.

 

In the case you mentioned, 2^70=1180591620717411303424 and 32 bit one would truncate after

 

1180591620 * 10^12

 

Maxima gives

 

is(1180591620 * 10^12 <= 2^70);

true

 

is(1180591621 * 10^12 >= 2^70);

true

 

As I said, this method doesn’t give the tightest bounds possible, but it gives you true upper and lower bounds without multi precision arithmetic. It gives 0 intervals e.g. for integers which fit in the mantissa, but not for large exact powers of 2.

 

> Moreover, it is not possible to implement interval arithmetic with OCaml, since you cannot change the rounding mode without a bit of C...

 

It should be possible to make the powers of 10 tables such that this works even with round to nearest, but it would likely be easier to make a C library for this.

 

Of cause it is a good question if I/O is the right place to save performance and waste precision. On the other hand you lose only 2 or 3 bits and you know what the precision is. I would think most applications are such that the required precision is not exactly an IEEE precision, so that these 2 or 3 bits are ok. I used this method once in an embedded platform, where multi precision arithmetic was not an option, and this was a good compromise.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928




--
Tung Vu Xuan,
Japan Advanced Institute of Science and Technology,
Mobile: (+81) 080 4259 9135 -  (+84) 01689934381
Hometown: Bac Ninh