interval_crlibm 1.6 (latest)

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

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

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

type number = float

Numbers type on which intervals are defined.

type t = Interval_base.interval

The type of intervals.

val zero : t

Neutral element for addition.

val one : t

Neutral element for multiplication.

val pi : t

π with bounds properly rounded.

val two_pi : t

2π with bounds properly rounded.

val half_pi : t

π/2 with bounds properly rounded.

val euler : t

Euler's constant with bounds properly rounded.

since 1.6

val entire : t

The entire set of numbers.

since 1.5

val 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.

val inf : t -> number

inf t returns the lower bound of the interval.

since 1.6

val sup : t -> number

sup t returns the higher bound of the interval.

since 1.6

val 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

val of_int : int -> t

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

val 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.

val pr : out_channel -> t -> unit

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

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

Same as pr but enables to choose the format.

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

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

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

Same as pp but enables to choose the format.

val 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

val 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).

val belong : number -> t -> bool

belong x a returns whether x ∈ a.

val 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

val is_bounded : t -> bool

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

since 1.5

val is_entire : t -> bool

is_entire x says whether x is the entire interval.

since 1.5

val equal : t -> t -> bool

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

since 1.5

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

Synonym for equal.

since 1.5

val subset : t -> t -> bool

subset x y returns true iff x ⊆ y.

since 1.5

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

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

since 1.5

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

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

since 1.5

val precedes : t -> t -> bool

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

since 1.5

val 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

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

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

since 1.5

val (>) : t -> t -> bool

x > y iff y < x.

since 1.5

val 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

val disjoint : t -> t -> bool

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

since 1.5

Operations

val width : t -> t

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

val width_up : t -> number

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

val width_dw : t -> number

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

val diam : t -> number

Alias for width_up (page 64 of IEEE1788).

val 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

val 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 +..)

val mag : t -> number

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

val mig : t -> number

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

val 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.

val 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.)].

val truncate : t -> t

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

val floor : t -> t

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

val ceil : t -> t

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

val 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.

val 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)].

val 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

val 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

val 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)].

val 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)].

val (+) : t -> t -> t

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

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

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

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

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

val (-) : t -> t -> t

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

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

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

val (-:) : number -> t -> t

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

val (~-) : t -> t

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

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

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

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

val (/) : 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.

val (/.) : 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.

val (/:) : 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.

val inv : t -> t

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

type 'a one_or_two =

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

val 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.

val 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

val 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

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

a**n returns interval a raised to nth power according to interval arithmetic. If n=0 then one is returned.

raises Domain_error
if n < 0 and a=zero.

val sqrt : t -> t

sqrt x returns an enclosure for the square root of x.

val hypot : t -> t -> t

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

val low : t -> number

low t returns the lower bound of the interval.

deprecated Use I.inf

val high : t -> number

high t returns the higher bound of the interval.

deprecated Use I.sup

val width_high : t -> number

deprecated Use I.width_up

val width_low : t -> number

deprecated Use I.width_dw

module Precision : sig ... end

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

val size : t -> t

deprecated Use I.width

val size_high : t -> number

deprecated Use I.width_up

val size_low : t -> number

deprecated Use I.width_dw

Usual arithmetic operators

module U : sig ... end

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

Logarithmic and exponential functions

val 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.

val log1p : t -> t

log1p a returns an enclosure of {log(1 + x) | x ∈ a}. Raise Domain_error if a.high ≤ -1.

val exp : t -> t

exp a returns an enclosure of {eˣ | x ∈ a}.

val expm1 : t -> t

expm1 a returns an enclosure of {eˣ-1 | x ∈ a}.

val log2 : t -> t

log2 is an interval extension of log₂.

val log10 : t -> t

log10 is an interval extension of log₁₀.

Trigonometric functions

val cos : t -> t

cos is an interval extension of cos.

val cospi : t -> t

cospi a is an interval extension of x ↦ cos(π·x).

val sin : t -> t

sin is interval extension of sin.

val sinpi : t -> t

sinpi is an interval extension of x ↦ sin(π·x).

val tan : t -> t

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

val tanpi : t -> t

tanpi is an interval extension of x ↦ tan(π·x).

val 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.

val acospi : t -> t

acospi a returns an enclosure of {acos(x)/π | x ∈ a}. All values are in [0,1].

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

val 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.

val asinpi : t -> t

asinpi a returns an enclosure of {asin(x)/π | x ∈ a}. All values are in [-1/2, 1/2].

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

val atan : t -> t

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

val atanpi : t -> t

atanpi a returns an enclosure of {atan(x)/π | x ∈ a}. All values are in [-1/2, 1/2].

Hyperbolic functions

val cosh : t -> t

cosh extends cosh to interval arithmetic.

val sinh : t -> t

sinh extends sinh to interval arithmetic.

val tanh : t -> t

tanh extends tanh to interval arithmetic.