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 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 t = Interval_base.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 : 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.
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
.
module U : sig ... end
Module undoing the redeclaration of usual infix operators +
, +.
, etc. in case it is needed locally, while this module is open.
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
.
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
.a**n
returns interval a
raised to n
th power according to interval arithmetic. If n=0
then one
is returned. Computed with exp-log in base2.
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.
x **: a
returns float x
raised to interval a
power according to interval arithmetic, considering the restiction of x
to x >= 0.
a *** b
returns interval a
raised to b
power according to interval arithmetic, considering the restriction of "x power y" to x >= 0.
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.
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⁵³.
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⁵³.
tan a
returns the proper extension of tan to interval arithmetic. Returns [-∞,∞] if one of the bounds is greater or lower than ±2⁵³.
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,π].
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].
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
.
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.
module Arr : sig ... end
Operations on arrays of intervals.