Module Interval_intel.I

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.

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 ) Stdlib.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 : Stdlib.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 ) Stdlib.format -> Stdlib.out_channel -> t -> unit

Same as pr but enables to choose the format.

val pp : Stdlib.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 ) Stdlib.format -> Stdlib.Format.formatter -> t -> unit

Same as pp but enables to choose the format.

val fmt : ( number -> 'b, 'a, 'b ) Stdlib.format -> ( t -> 'c, 'd, 'e, 'c ) Stdlib.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 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.

val high : t -> number

high t returns the higher bound of the interval.

val width_high : t -> number
val width_low : t -> number
module Precision : sig ... end

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

val size : t -> t
val size_high : t -> number
val size_low : t -> number

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.

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

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

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

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

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

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.

  • raises Domain_error

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

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

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

Trigonometric functions

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

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

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

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

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

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

val 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

val cosh : t -> t

cosh is the proper extension of cosh to interval arithmetic.

val sinh : t -> t

sinh is the proper extension of sinh to interval arithmetic.

val tanh : t -> t

tanh is the proper extension of tanh to interval arithmetic.

Arrays of intervals

module Arr : sig ... end

Operations on arrays of intervals.