package interval_intel

  1. Overview
  2. Docs

Interval library in OCaml. ONLY FOR INTEL PROCESSORS.

All operations use correct rounding.

It is recommended to open this module. It will put into scope the interval type and a module I (see Interval.I) containing interval operations:

open Interval_intel

let x = I.(v 0.5 1. + sin(v 3. 3.125))

When the module I is open, the integer operators (+, -,...) and the floating point ones (+., -.,...) are redefined. If, in the middle of an expression, you need to use the usual operators, locally open the module I.U as in I.(x /. U.(float(n + 1))).

The names symbols for infix operators have been chosen to try to make the standard cases short and the overall expression readable. The rationale is as follows.

  • The integer operators +, -, *, /, ~- and ~+ act on intervals;
  • The float operators +., -., /. take an interval to the left and a float to the right, but *. does the opposite. This is to match the standard presentation of polynomials. Example: I.(3. *. x**2 + 2. *. x +. 4.). WARNING: you should only use these functions when the float argument represent the exact mathematical value (taking into account that the compiler will round literals). For example, 42. is fine while 0.1 is not (because it has an infinite binary representation).
  • Operators +:, -:, *: and /: are as in the previous point but with the interval and float swapped. Note that +: and *: are not really needed because the operations are commutative but are present for consistency.
  • For exponentiation, ** has been chosen for integer exponent because they are the more frequent, **. when the exponent is a float, **: when the base is a float and *** for exponentiation of two intervals.

You do not have to worry about remembering these rules. The type system will enforce them.

It is not mandatory, but still wise, to read the documentation of the Fpu module.

This library has been mainly designed to be used in a branch and bound optimization algorithm. So, some choices have been made:

  • NaN is never used. We either extend functions by pseudo continuity or raise exceptions. For example, {low=2.;high=3.} / {low=0.;high=2.} returns {low=1.;high=Inf}, while {low=2.;high=3.} / {low=0.;high=0.} or {low=0.;high=0.} / {low=0.;high=0.} raises Interval_base.Division_by_zero.
  • Intervals [+Inf,+Inf] or [-Inf,-Inf] are never used and never returned.
  • When using a float in the following operations, it must never be equal to +Inf or -Inf or Nan.
  • Functions such as log, sqrt, acos or asin are restricted to their definition domain but raise an exception rather than returning an empty interval: for example sqrt {low=-4;high=4} returns {low=0;high=2} while sqrt {low=-4;high=-2} will raise an exception.

Another design choice was to have non mutable elements in interval structure, and to maintain an "ordinary" syntax for operations, such as let a = b + c in ... thus mapping interval computation formula on airthmetic formula. We could have instead chosen to have mutable elements, and to write for example (Interval.add a b c) to perform “a ← b + c”. The first choice is, to our point of view, more elegant and easier to use. The second is more efficient, especially when computing functions with many temporary results, which force the GC to create and destroy lot of intervals when using the implementation we chose. Nothing's perfect.

The older deprecated interface is still available.

The library is implemented in x87 assembly mode and is quite efficient (see below).

  • version 1.5

Intervals (for Intel processors)

type t = Interval.t = {
  1. low : float;
    (*

    lower bound, possibly = -∞

    *)
  2. high : float;
    (*

    higher bound, possibly = +∞

    *)
}

The interval type. Be careful however when creating intervals. For example, the following code: let a = {low=1./.3.; high=1./.3.} creates an interval which does NOT contain the mathematical object 1/3.

If you want to create an interval representing 1/3, you have to write let a = I.(inv(v 3. 3.)) because rounding will then be properly handled by I.inv and the resulting interval will indeed contain the exact value of 1/3.

exception Division_by_zero
exception Domain_error of string
module I : sig ... end

Interval operations. Locally open this module — using e.g. I.(...) — to redefine classical arithmetic operators for interval arithmetic.

module Fpu : sig ... end

Access to low level floating point functions. THIS LIBRARY ONLY WORKS FOR INTEL PROCESSORS.

module Low = Fpu.Low
module High = Fpu.High

Old interface (deprecated)

The functions below are the ones of the older versions of Interval. They will soon be removed.

type interval = t
val zero_I : t

Neutral element for addition

  • deprecated Use I.zero instead
val one_I : t

Neutral element for multiplication

  • deprecated Use I.one instead
val pi_I : t

pi with bounds properly rounded

  • deprecated Use I.pi instead
val e_I : t

e with bounds properly rounded

  • deprecated Use I.e instead
val printf_I : (float -> string, unit, string) format -> t -> unit

Prints an interval with the same format applied to both endpoints. Formats follow the same specification than the one used for the regular printf function

  • deprecated Use I.pr or I.fmt instead
val fprintf_I : out_channel -> (float -> string, unit, string) format -> t -> unit

Prints an interval into an out_channel with the same format applied to both endpoints

  • deprecated Use I.pr ot I.fmt instead
val sprintf_I : (float -> string, unit, string) format -> t -> string

Returns a string holding the interval printed with the same format applied to both endpoints

  • deprecated Use I.to_string instead
val float_i : int -> t

Returns the interval containing the float conversion of an integer

  • deprecated Use I.of_int instead
val compare_I_f : t -> float -> int

compare_I_f a x returns 1 if a.high<x, 0 if a.low<=x<=a.high and -1 if x<a.low

  • deprecated Use I.compare_f instead
val size_I : t -> float

size_I a returns a.high-a.low

  • deprecated Use I.size_high instead
val sgn_I : t -> t

sgn a returns {low=float (compare a.low 0.);high=float (compare a.high 0.)}

  • deprecated Use I.sgn instead
val truncate_I : t -> t

truncate_I a returns {low=floor a.low;high=ceil a.high}

  • deprecated Use I.truncate instead
val abs_I : t -> t

abs_I a returns {low=a.low;high=a.high} if a.low>=0., {low=-a.high;high=-a.low} if a.high<=0., and {low=0.;high=max -a.low a.high} otherwise

  • deprecated Use I.abs instead
val union_I_I : t -> t -> t

union_I_I a b returns {low=min a.low b.low; high=max a.high b.high}

  • deprecated Use I.hull instead
val max_I_I : t -> t -> t

max_I_I a b returns {low=max a.low b.low; high=max a.high b.high}

  • deprecated Use I.max instead
val min_I_I : t -> t -> t

min_I_I a b returns {low=min a.low b.low; high=min a.high b.high}

  • deprecated Use I.min instead
val (+$) : t -> t -> t

a +$ b returns {low=a.low+.b.low;high=a.high+.b.high}

  • deprecated Use I.( + ) instead
val (+$.) : t -> float -> t

a +$. x returns {low=a.low+.x;high=a.high+.x}

  • deprecated Use I.( +. ) instead
val (+.$) : float -> t -> t

x +.$ a returns {low=a.low+.x;high=a.high+.x}

  • deprecated Use I.( +: ) instead
val (-$) : t -> t -> t

a -$ b returns {low=a.low-.b.high;high=a.high-.b.low}

  • deprecated Use I.( - ) instead
val (-$.) : t -> float -> t

a -$. x returns {low=a.low-.x;high=a.high-.x}

  • deprecated Use I.( -. ) instead
val (-.$) : float -> t -> t

x -.$ a returns {low=x-.a.high;high=x-.a.low}

  • deprecated Use I.( -: ) instead
val (~-$) : t -> t

~-$ a returns {low=-a.high;high=-a.low}

  • deprecated Use I.( ~- ) instead
val (*$.) : t -> float -> t

a *$. x multiplies a by x according to interval arithmetic and returns the proper result. If x=0. then zero_I is returned

  • deprecated Use I.( *: ) instead
val (*.$) : float -> t -> t

x *$. a multiplies a by x according to interval arithmetic and returns the proper result. If x=0. then zero_I is returned.

  • deprecated Use I.( *. ) instead
val (*$) : t -> t -> t

a *$ b multiplies a by b according to interval arithmetic and returns the proper result. If a=zero_I or b=zero_I then zero_I is returned

  • deprecated Use I.( * ) instead
val (/$.) : t -> float -> t

a /$. x divides a by x according to interval arithmetic and returns the proper result. Raise Failure "/$." if x=0.

  • deprecated Use I.( /. ) instead and adjust exn
val (/.$) : float -> t -> t

x /.$ a divides x by a according to interval arithmetic and returns the result. Raise Failure "/.$" if a=zero_I

  • deprecated Use I.( /: ) instead and adjust exn
val (/$) : t -> t -> t

a /$ b divides the first interval by the second according to interval arithmetic and returns the proper result. Raise Failure "/$" if b=zero_I

  • deprecated Use I.( / ) instead and adjust exn
val mod_I_f : t -> float -> t

mod_I_f a f returns a mod f according to interval arithmetic et OCaml mod_float definition. Raise Failure "mod_I_f" if f=0.

  • deprecated Use I.mod_f instead and adjust exn
val inv_I : t -> t

inv_I a returns 1. /.$ a. Raise Failure "inv_I" if a=zero_I

  • deprecated Use I.inv instead and adjust exn
val sqrt_I : t -> t

sqrt_I a returns {low=sqrt a;high=sqrt b} if a>=0., {low=0.;high=sqrt b} if a<0.<=b. Raise Failure "sqrt_I" if b<0.

  • deprecated Use I.sqrt instead and adjust exn
val pow_I_i : t -> int -> t

Pow_I_i a n with n integer returns interval a raised to nth power according to interval arithmetic. If n=0 then {low=1.;high=1.} is returned. Raise Failure "pow_I_f" if n<=0 and a=zero_I. Computed with exp-log in base2.

  • deprecated Use I.( ** ) instead and adjust exn
val (**$.) : t -> float -> t

a **$. f returns interval a raised to f power according to interval arithmetic. If f=0. then {low=1.;high=1.} is returned. Raise Failure "**$." if f<=0. and a=zero_I or if f is not an integer value and a.high<0.. Computed with exp-log in base2.

  • deprecated Use I.( **. ) instead and adjust exn
val (**$) : t -> t -> t

a **$ b returns interval a raised to b power according to interval arithmetic, considering the restriction of x power y to x >= 0. Raise Failure "**$" if a.high < 0 or (a.high=0. and b.high<=0.)

  • deprecated Use I.( *** ) instead and adjust exn
val (**.$) : float -> t -> t

x **.$ a returns float x raised to interval a power according to interval arithmetic, considering the restiction of x power y to x >= 0. Raise Failure "**.$" if x < 0 and a.high <= 0

  • deprecated Use I.( **: ) instead and adjust exn
val log_I : t -> t

log_I a returns {low=log a.low; high=log a.high} if a.low>0., {low=neg_infinity; high=log a.high} if a.low<0<=a.high. Raise Failure "log_I" if a.high<=0.

  • deprecated Use I.log instead and adjust exn
val exp_I : t -> t

exp_I a returns {low=exp a.high;high=exp b.high}

  • deprecated Use I.exp instead
val cos_I : t -> t

cos_I a returns the proper extension of cos to arithmetic interval Returns [-1,1] if one of the bounds is greater or lower than +/-2**53

  • deprecated Use I.cos instead
val sin_I : t -> t

sin_I a returns the proper extension of sin to arithmetic interval Returns [-1,1] if one of the bounds is greater or lower than +/-2**53

  • deprecated Use I.sin instead
val tan_I : t -> t

tan_I a returns the proper extension of tan to arithmetic interval Returns [-Inf,Inf] if one of the bounds is greater or lower than +/-2**53

  • deprecated Use I.tan instead
val acos_I : t -> t

acos_I a raise Failure "acos_I" if a.low>1. or a.high<-1., else returns {low=if a.high<1. then acos a.high else 0; high=if a.low>-1. then acos a.low else pi}. All values are in [0,pi].

  • deprecated Use I.acos instead and adjust exn
val asin_I : t -> t

asin_I a raise Failure "asin_I" if a.low>1. or a.high<-1. else returns {low=if a.low>-1. then asin a.low else -pi/2; high=if a.low<1. then asin a.high else pi/2}. All values are in [-pi/2,pi/2].

  • deprecated Use I.asin instead and adjust exn
val atan_I : t -> t

atan_I a returns {low=atan a.low;high=atan a.high}

  • deprecated Use I.atan instead
val atan2mod_I_I : t -> t -> t

atan2mod_I_I y x returns the proper extension of interval arithmetic to atan2 but with values in [-pi,2 pi] instead of [-pi,pi]. This can happen when y.low<0 and y.high>0 and x.high<0: then the returned interval is {low=atan2 y.high x.high;high=(atan2 y.low x.high)+2 pi}. This preserves the best inclusion function possible but is not compatible with the standard definition of atan2

  • deprecated Use I.atan2mod instead
val atan2_I_I : t -> t -> t

Same function as above but when y.low<0 and y.high>0 and x.high<0 the returned interval is [-pi,pi]. This does not preserve the best inclusion function but is compatible with the atan2 regular definition

  • deprecated Use I.atan2 instead
val cosh_I : t -> t

cosh_I is the proper extension of interval arithmetic to cosh

  • deprecated Use I.cosh instead
val sinh_I : t -> t

sinh_I is the proper extension of interval arithmetic to sinh

  • deprecated Use I.sinh instead
val tanh_I : t -> t

tanh_I is the proper extension of interval arithmetic to tanh

  • deprecated Use I.tanh instead
val size_max_X : t array -> float

Computes the size of the largest interval of the interval vector

  • deprecated Use I.Arr.size_max instead
val size_mean_X : t array -> float

Computes the mean of the size of intervals of the interval vector

  • deprecated Use I.Arr.size_mean instead
val printf_X : (float -> string, unit, string) format -> t array -> unit

Prints an interval vector with the same format applied to all endpoints.

  • deprecated Use I.Arr.pr or I.Arr.fmt instead
val fprintf_X : out_channel -> (float -> string, unit, string) format -> t array -> unit

Prints an interval vector into an out_channel with the same format applied to all endpoints

  • deprecated Use I.Arr.pr or I.Arr.fmt instead
val sprintf_X : (float -> string, unit, string) format -> t array -> string

Returns a string holding the interval vector printed with the same format applied to all endpoints

  • deprecated Use I.Arr.to_string instead
val print_X : t array -> unit

Deprecated

  • deprecated Use I.Arr.pr instead
val print_I : t -> unit

Deprecated

  • deprecated Use I.pr instead
val size_X : t array -> float

Deprecated

  • deprecated Use I.Arr.size_max instead
val size2_X : t array -> float

Deprecated

  • deprecated Use I.Arr.size_mean instead
val (<$.) : t -> float -> int

Deprecated

  • deprecated Use I.compare_f instead
val pow_I_f : t -> float -> t

Deprecated

  • deprecated Use I.( **. ) instead
val pow_I_I : t -> t -> t

Deprecated

  • deprecated Use I.( *** ) instead

Performance

Intel Atom 230 Linux 32 bits:

  • ftan speed (10000000 calls): 2.528158
  • fcos speed (10000000 calls): 2.076129
  • fsin speed (10000000 calls): 1.972123
  • I.tan speed (10000000 calls): 4.416276
  • I.cos speed (10000000 calls): 4.936308
  • I.sin speed (10000000 calls): 5.396338
  • fadd speed (10000000 calls): 0.980062
  • fsub speed (10000000 calls): 0.980061
  • fmul speed (10000000 calls): 0.980061
  • fdiv speed (10000000 calls): 1.424089
  • I.( + ) speed (10000000 calls): 1.656103
  • I.( - ) speed (10000000 calls): 1.636103
  • I.( * ) speed (10000000 calls): 4.568285
  • I.( / ) speed (10000000 calls): 4.552285

Intel 980X Linux 64 bits:

  • ftan speed (10000000 calls): 0.472029
  • fcos speed (10000000 calls): 0.400025
  • fsin speed (10000000 calls): 0.400025
  • I.tan speed (10000000 calls): 0.752047
  • I.cos speed (10000000 calls): 1.036065
  • I.sin speed (10000000 calls): 1.104069
  • fadd speed (10000000 calls): 0.124008
  • fsub speed (10000000 calls): 0.120008
  • fmul speed (10000000 calls): 0.128008
  • fdiv speed (10000000 calls): 0.156010
  • I.( + ) speed (10000000 calls): 0.340021
  • I.( - ) speed (10000000 calls): 0.332021
  • I.( * ) speed (10000000 calls): 0.556035
  • I.( / ) speed (10000000 calls): 0.468029
OCaml

Innovation. Community. Security.