Interval_base.TBasic signature for interval arithmetic packages.
val zero : tNeutral element for addition.
val one : tNeutral element for multiplication.
val pi : tπ with bounds properly rounded.
val two_pi : t2π with bounds properly rounded.
val half_pi : tπ/2 with bounds properly rounded.
val euler : tEuler's constant with bounds properly rounded.
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.
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.
val of_int : int -> tReturns the interval containing the conversion of an integer to the number type.
to_string i return a string representation of the interval i.
val pr : Stdlib.out_channel -> t -> unitPrint the interval to the channel. To be used with Printf format "%a".
Same as pr but enables to choose the format.
val pp : Stdlib.Format.formatter -> t -> unitPrint the interval to the formatter. To be used with Format format "%a".
Same as pp but enables to choose the format.
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.
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 is_singleton : t -> boolis_singleton x says whether x is a ingleton i.e., the two bounds of x are equal.
val is_bounded : t -> boolis_bounded x says whether the interval is bounded, i.e., -∞ < inf(x) and sup(x) < ∞.
x <= y says whether x is weakly less than y i.e., ∀ξ ∈ x, ∃η ∈ y, ξ ≤ η and ∀η ∈ y, ∃ξ ∈ x, ξ ≤ η.
x >= y says whether x is weakly greater than y i.e., ∀ξ ∈ x, ∃η ∈ y, ξ ≥ η and ∀η ∈ y, ∃ξ ∈ x, ξ ≥ η.
interior x y returns true if x is interior to y in the topological sense. For example interior entire entire is true.
x < y says whether x is strictly weakly less than y i.e., ∀ξ ∈ x, ∃η ∈ y, ξ < η and ∀η ∈ y, ∃ξ ∈ x, ξ < η.
strict_precedes x y returns true iff x is to the left and does not touch y.
size a returns an interval containing the true width of the interval sup a - inf a.
dist x y is the Hausdorff distance between x and y. It is equal to max{ |inf x - inf y|, |sup x - sup y| }.
dist_up x y is the Hausdorff distance between x and y, rounded up. (This satisfies the triangular inequality for a rounded up +..)
mid x returns a finite number belonging to x which is close to the midpoint of x. If is_entire x, zero is returned.
sgn a returns the sign of each bound, e.g., for floats [float (compare (inf a) 0.), float (compare (sup a) 0.)].
truncate a returns the integer interval containing a, that is [floor(inf a), ceil(sup a)].
abs a returns the absolute value of the interval, that is
a if inf a ≥ 0.,~- a if sup a ≤ 0., andmax (- inf a) (sup a)] otherwise.hull a b returns the smallest interval containing a and b, that is [min (inf a) (inf b), max (sup a) (sup b)].
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.
max a b returns the "maximum" of the intervals a and b, that is [max (inf a) (inf b), max (sup a) (sup b)].
min a b returns the "minimum" of the intervals a and b, that is [min (inf a) (inf b), min (sup a) (sup b)].
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.
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.
a *. x multiplies a by x according to interval arithmetic and returns the proper result. If x=0. then zero is returned.
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.
a /. x divides a by x according to interval arithmetic and returns the proper result. Raise Interval.Division_by_zero if x=0.0.
x /: a divides x by a according to interval arithmetic and returns the result. Raise Interval.Division_by_zero if a=zero.
inv a returns 1. /: a but is more efficient. Raise Interval.Division_by_zero if a=zero.
val invx : t -> t one_or_twoinvx 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.
cancelminus x y returns the tightest interval z such that x ⊆ z + y. If no such z exists, it returns entire.
cancelplus x y returns the tightest interval z such that x ⊆ z - y. If no such z exists, it returns entire.
a**n returns interval a raised to nth power according to interval arithmetic. If n=0 then one is returned.