Module `Interval_crlibm.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 (**) : 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.

Sourceval sqrt : t -> t

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

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.

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 log1p : t -> t

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

Sourceval exp : t -> t

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

Sourceval expm1 : t -> t

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

Sourceval log2 : t -> t

log2 is an interval extension of log₂.

Sourceval log10 : t -> t

log10 is an interval extension of log₁₀.

Trigonometric functions

Sourceval cos : t -> t

cos is an interval extension of cos.

Sourceval cospi : t -> t

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

Sourceval sin : t -> t

sin is interval extension of sin.

Sourceval sinpi : t -> t

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

Sourceval tan : t -> t

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

Sourceval tanpi : t -> t

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

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

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

Sourceval atan : t -> t

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

Sourceval atanpi : t -> t

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

Hyperbolic functions

Sourceval cosh : t -> t

cosh extends cosh to interval arithmetic.

Sourceval sinh : t -> t

sinh extends sinh to interval arithmetic.

Sourceval tanh : t -> t

tanh extends tanh to interval arithmetic.

package interval_crlibm

Module Interval_crlibm.ISource