package interval_base

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Usual arithmetic operators

interval_base
- Interval_base
  - DIRECTED
  - I
    
    Precision
    
    U
  - RoundDown
  - RoundUp
  - T

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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

type number = float

Numbers type on which intervals are defined.

type t = 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.