Module `Interval_intel.I`Source

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

include module type of Interval_base.I

include Interval_base.T
  with type number = float
   and type t = Interval_base.interval

Sourcetype number = float

Numbers type on which intervals are defined.

Sourcetype t = Interval_base.interval

The type of intervals.

Sourceval zero : t

Neutral element for addition.

Sourceval one : t

Neutral element for multiplication.

Sourceval pi : t

π with bounds properly rounded.

Sourceval two_pi : t

2π with bounds properly rounded.

Sourceval half_pi : t

π/2 with bounds properly rounded.

Sourceval euler : t

Euler's constant with bounds properly rounded.

since 1.6

Sourceval entire : t

The entire set of numbers.

since 1.5

Sourceval v : number -> number -> t

v a b returns the interval [a, b]. BEWARE that, unless you take care, if you use v a b with literal values for a and/or b, the resulting interval may not contain these values because the compiler will round them to binary numbers before passing them to v.

raises Invalid_argument
if the interval [a, b] is equal to [-∞,-∞] or [+∞,+∞] or one of the bounds is NaN.

Sourceval inf : t -> number

inf t returns the lower bound of the interval.

since 1.6

Sourceval sup : t -> number

sup t returns the higher bound of the interval.

since 1.6

Sourceval singleton : number -> t

singleton x returns the same as {!v} x x except that checks on x are only performed once and infinite values of x work according to the specification of intervals.

since 1.6

Sourceval of_int : int -> t

Returns the interval containing the conversion of an integer to the number type.

Sourceval to_string : ?fmt:(number -> 'b, 'a, 'b) format -> t -> string

to_string i return a string representation of the interval i.

parameter fmt
is the format used to print the two bounds of i. Default: "%g" for float numbers.

Sourceval pr : out_channel -> t -> unit

Print the interval to the channel. To be used with Printf format "%a".

Sourceval pr_fmt : ?fmt:(number -> 'b, 'a, 'b) format -> out_channel -> t -> unit

Same as pr but enables to choose the format.

Sourceval pp : Format.formatter -> t -> unit

Print the interval to the formatter. To be used with Format format "%a".

Source

val pp_fmt : 
  ?fmt:(number -> 'b, 'a, 'b) format ->
  Format.formatter ->
  t ->
  unit

Same as pp but enables to choose the format.

Sourceval fmt : (number -> 'b, 'a, 'b) format -> (t -> 'c, 'd, 'e, 'c) format4

fmt number_fmt returns a format to print intervals where each component is printed with number_fmt.

Example: Printf.printf ("%s = " ^^ fmt "%.10f" ^^ "\n") name i.

Boolean functions

Sourceval compare_f : t -> number -> int

compare_f a x returns

1 if sup(a) < x,
0 if inf(a) ≤ x ≤ sup(a), i.e., if x ∈ a, and
-1 if x < inf(a).

Sourceval belong : number -> t -> bool

belong x a returns whether x ∈ a.

Sourceval is_singleton : t -> bool

is_singleton x says whether x is a ingleton i.e., the two bounds of x are equal.

since 1.6

Sourceval is_bounded : t -> bool

is_bounded x says whether the interval is bounded, i.e., -∞ < inf(x) and sup(x) < ∞.

since 1.5

Sourceval is_entire : t -> bool

is_entire x says whether x is the entire interval.

since 1.5

Sourceval equal : t -> t -> bool

equal a b says whether the two intervals are the same.

since 1.5

Sourceval (=) : t -> t -> bool

Synonym for equal.

since 1.5

Sourceval subset : t -> t -> bool

subset x y returns true iff x ⊆ y.

since 1.5

Sourceval (<=) : t -> t -> bool

x <= y says whether x is weakly less than y i.e., ∀ξ ∈ x, ∃η ∈ y, ξ ≤ η and ∀η ∈ y, ∃ξ ∈ x, ξ ≤ η.

since 1.5

Sourceval (>=) : t -> t -> bool

x >= y says whether x is weakly greater than y i.e., ∀ξ ∈ x, ∃η ∈ y, ξ ≥ η and ∀η ∈ y, ∃ξ ∈ x, ξ ≥ η.

since 1.5

Sourceval precedes : t -> t -> bool

precedes x y returns true iff x is to the left but may touch y.

since 1.5

Sourceval interior : t -> t -> bool

interior x y returns true if x is interior to y in the topological sense. For example interior entire entire is true.

since 1.5

Sourceval (<) : t -> t -> bool

x < y says whether x is strictly weakly less than y i.e., ∀ξ ∈ x, ∃η ∈ y, ξ < η and ∀η ∈ y, ∃ξ ∈ x, ξ < η.

since 1.5

Sourceval (>) : t -> t -> bool

x > y iff y < x.

since 1.5

Sourceval strict_precedes : t -> t -> bool

strict_precedes x y returns true iff x is to the left and does not touch y.

since 1.5

Sourceval disjoint : t -> t -> bool

disjoint x y returns true iff x ∩ y = ∅.

since 1.5

Operations

Sourceval width : t -> t

size a returns an interval containing the true width of the interval sup a - inf a.

Sourceval width_up : t -> number

width_up a returns the width of the interval sup a - inf a rounded up.

Sourceval width_dw : t -> number

width_dw a returns the width of the interval sup a - inf a rounded down.

Sourceval diam : t -> number

Alias for width_up (page 64 of IEEE1788).

Sourceval dist : t -> t -> t

dist x y is the Hausdorff distance between x and y. It is equal to max{ |inf x - inf y|, |sup x - sup y| }.

since 1.6

Sourceval dist_up : t -> t -> number

dist_up x y is the Hausdorff distance between x and y, rounded up. (This satisfies the triangular inequality for a rounded up +..)

Sourceval mag : t -> number

mag x returns the magnitude of x, that is sup{ |x| : x ∈ x }.

Sourceval mig : t -> number

mig x returns the mignitude of x, that is inf{ |x| : x ∈ x }.

Sourceval mid : t -> number

mid x returns a finite number belonging to x which is close to the midpoint of x. If is_entire x, zero is returned.

Sourceval sgn : t -> t

sgn a returns the sign of each bound, e.g., for floats [float (compare (inf a) 0.), float (compare (sup a) 0.)].

Sourceval truncate : t -> t

truncate a returns the integer interval containing a, that is [floor(inf a), ceil(sup a)].

Sourceval floor : t -> t

floor a returns the floor of a, that is [floor(inf a), floor(sup a)].

Sourceval ceil : t -> t

ceil a returns the ceil of a, that is [ceil(inf a), ceil(sup a)].

Sourceval abs : t -> t

abs a returns the absolute value of the interval, that is

a if inf a ≥ 0.,
~- a if sup a ≤ 0., and
[0, max (- inf a) (sup a)] otherwise.

Sourceval hull : t -> t -> t

hull a b returns the smallest interval containing a and b, that is [min (inf a) (inf b), max (sup a) (sup b)].

Sourceval inter_exn : t -> t -> t

inter_exn x y returns the intersection of x and y.

raises Domain_error
if the intersection is empty.

since 1.5

Sourceval inter : t -> t -> t option

inter_exn x y returns Some z where z is the intersection of x and y if it is not empty and None if the intersection is empty.

since 1.5

Sourceval max : t -> t -> t

max a b returns the "maximum" of the intervals a and b, that is [max (inf a) (inf b), max (sup a) (sup b)].

Sourceval min : t -> t -> t

min a b returns the "minimum" of the intervals a and b, that is [min (inf a) (inf b), min (sup a) (sup b)].

Sourceval (+) : t -> t -> t

a + b returns [inf a +. inf b, sup a +. sup b] properly rounded.

Sourceval (+.) : t -> number -> t

a +. x returns [inf a +. x, sup a +. x] properly rounded.

Sourceval (+:) : number -> t -> t

x +: a returns [a +. inf a, x +. sup a] properly rounded.

Sourceval (-) : t -> t -> t

a - b returns [inf a -. sup b, sup a -. inf b] properly rounded.

Sourceval (-.) : t -> number -> t

a -. x returns [inf a -. x, sup a -. x] properly rounded.

Sourceval (-:) : number -> t -> t

x -: a returns [x -. sup a, x -. inf a] properly rounded.

Sourceval (~-) : t -> t

~- a is the unary negation, it returns [-sup a, -inf a].

Sourceval (*) : t -> t -> t

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

Sourceval (*.) : number -> t -> t

x *. a returns the multiplication of a by x according to interval arithmetic. If x=0. then zero is returned.

Note that the scalar comes first in this “dotted operator” (as opposed to other ones) because it is customary in mathematics to place scalars first in products and last in sums. Example: 3. *. x**2 + 2. *. x +. 1.

Sourceval (*:) : t -> number -> t

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

Sourceval (/) : t -> t -> t

a / b divides the first interval by the second according to interval arithmetic and returns the proper result. Raise Interval.Division_by_zero if b=zero.

Sourceval (/.) : t -> number -> t

a /. x divides a by x according to interval arithmetic and returns the proper result. Raise Interval.Division_by_zero if x=0.0.

Sourceval (/:) : number -> t -> t

x /: a divides x by a according to interval arithmetic and returns the result. Raise Interval.Division_by_zero if a=zero.

Sourceval inv : t -> t

inv a returns 1. /: a but is more efficient. Raise Interval.Division_by_zero if a=zero.

Sourcetype 'a one_or_two =

| One of 'a
| Two of 'a * 'a

Sourceval invx : t -> t one_or_two

invx a is the extended division. When 0 ∉ a, the result is One(inv a). If 0 ∈ a, then the two natural intervals (properly rounded) Two([-∞, 1/(inf a)], [1/(sup a), +∞]) are returned. Raise Interval.Division_by_zero if a=zero.

Sourceval cancelminus : t -> t -> t

cancelminus x y returns the tightest interval z such that x ⊆ z + y. If no such z exists, it returns entire.

since 1.5

Sourceval cancelplus : t -> t -> t

cancelplus x y returns the tightest interval z such that x ⊆ z - y. If no such z exists, it returns entire.

since 1.5

Sourceval hypot : t -> t -> t

hypot x y returns an enclosure of sqrt(x *. x + y *. y).

Sourceval low : t -> number

low t returns the lower bound of the interval.

deprecated Use I.inf

Sourceval high : t -> number

high t returns the higher bound of the interval.

deprecated Use I.sup

Sourceval width_high : t -> number

deprecated Use I.width_up

Sourceval width_low : t -> number

deprecated Use I.width_dw

Sourcemodule Precision : sig ... end

Global precision for the functions I.pr and I.pp.

Sourceval size : t -> t

deprecated Use I.width

Sourceval size_high : t -> number

deprecated Use I.width_up

Sourceval size_low : t -> number

deprecated Use I.width_dw

Usual arithmetic operators

Sourcemodule U : sig ... end

Module undoing the redeclaration of usual infix operators +, +., etc. in case it is needed locally, while this module is open.

Sourceval mod_f : t -> float -> t

mod_f a f returns a mod f according to interval arithmetic and OCaml mod_float definition. Raise Interval.Division_by_zero if f=0.0.

Sourceval sqrt : t -> t

sqrt x returns

{low=sqrt x.low; high=sqrt x.high} (properly rounded) if x.low ≥ 0.,
{low=0.; high=sqrt x.high} if x.low < 0 ≤ x.high.

raises Domain_error
if x.high < 0.0.

Sourceval (**) : t -> int -> t

a**n returns interval a raised to nth power according to interval arithmetic. If n=0 then one is returned. Computed with exp-log in base2.

raises Domain_error
if n <= 0 and a=zero.

Sourceval (**.) : t -> float -> t

a **. f returns interval a raised to f power according to interval arithmetic. If f=0. then one is returned. Computed with exp-log in base2.

raises Domain_error
if f <= 0. and a=zero or if f is not an integer value and a.high < 0..

Sourceval (**:) : float -> t -> t

x **: a returns float x raised to interval a power according to interval arithmetic, considering the restiction of x to x >= 0.

raises Domain_error
if x < 0. and a.high <= 0.0.

Sourceval (***) : 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.

raises Domain_error
if a.high < 0 or (a.high = 0. and b.high <= 0.).

Logarithmic and exponential functions

Sourceval log : t -> t

log a returns, properly rounded,

{low=log a.low; high=log a.high} if a.low>0., and
{low=neg_infinity; high=log a.high} if a.low<0<=a.high.

Raise Domain_error if a.high ≤ 0.

Sourceval exp : t -> t

exp a returns {low=exp a.high; high=exp b.high}, properly rounded.

Trigonometric functions

Sourceval cos : t -> t

cos a returns the proper extension of cos to interval arithmetic. Returns [-1,1] if one of the bounds is greater or lower than ±2⁵³.

Sourceval sin : t -> t

sin a returns the proper extension of sin to interval arithmetic. Returns [-1,1] if one of the bounds is greater or lower than ±2⁵³.

Sourceval tan : t -> t

tan a returns the proper extension of tan to interval arithmetic. Returns [-∞,∞] if one of the bounds is greater or lower than ±2⁵³.

Sourceval acos : t -> t

acos a 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,π].

raises Domain_error
if a.low > 1. or a.high < -1.

Sourceval asin : t -> t

asin a 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 [-π/2,π/2].

raises Domain_error
if a.low > 1. or a.high < -1.

Sourceval atan : t -> t

atan a returns {low=atan a.low; high=atan a.high} properly rounded.

Sourceval atan2mod : t -> t -> t

atan2mod y x returns the proper extension of interval arithmetic to atan2 but with values in [-π, 2π] instead of [-π, π]. 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π}. This preserves the best inclusion function possible but is not compatible with the standard definition of atan2.

Sourceval atan2 : t -> t -> t

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

Hyperbolic functions

Sourceval cosh : t -> t

cosh is the proper extension of cosh to interval arithmetic.

Sourceval sinh : t -> t

sinh is the proper extension of sinh to interval arithmetic.

Sourceval tanh : t -> t

tanh is the proper extension of tanh to interval arithmetic.

Arrays of intervals

Sourcemodule Arr : sig ... end

Operations on arrays of intervals.

package interval_intel

Module Interval_intel.ISource