Interval_base.I
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 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.
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 -> t
Returns 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 -> unit
Print 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 -> unit
Print 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 -> bool
is_singleton x
says whether x
is a ingleton i.e., the two bounds of x
are equal.
val is_bounded : t -> bool
is_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_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
.
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 n
th power according to interval arithmetic. If n=0
then one
is returned.
module U : sig ... end
Module undoing the redeclaration of usual infix operators +
, +.
, etc. in case it is needed locally, while this module is open.