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.I
Interval operations. Locally open this module — using e.g. I.(...)
— to redefine classical arithmetic operators for interval arithmetic.
include Interval.T with type number = float and type t = Interval.t
type t = Interval.t
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 e : t
e
(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
.
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 pp : Format.formatter -> t -> unit
Print the interval to the formatter. To be used with Format
format "%a".
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 high(a) < x
,0
if low(a)
≤ x
≤ high(a)
, i.e., if x
∈ a
, and-1
if x < low(a)
.val is_bounded : t -> bool
is_bounded x
says whether the interval is bounded, i.e., -∞ < low(x)
and high(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 high a - low a
.
size_high a
returns the width of the interval high a - low a
rounded up.
size_low a
returns the width of the interval high a - low a
rounded down.
sgn a
returns the sign of each bound, e.g., for floats [float (compare (low a) 0.)
, float (compare (high a) 0.)
].
truncate a
returns the integer interval containing a
, that is [floor(low a)
, ceil(high a)
].
abs a
returns the absolute value of the interval, that is
a
if low a
≥ 0.
,~- a
if high a
≤ 0.
, andmax (- low a) (high a)
] otherwise.hull a b
returns the smallest interval containing a
and b
, that is [min (low a) (low b)
, max (high a) (high 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 (low a) (low b)
, max (high a) (high b)
].
min a b
returns the "minimum" of the intervals a
and b
, that is [min (low a) (low b)
, min (high a) (high 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
multiplies a
by x
according to interval arithmetic and returns the proper result. If x=0.
then zero
is returned.
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/(low a)], [1/(high 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.
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.
log1p a
returns an enclosure of {log(1 + x) | x ∈ a
}. Raise Domain_error
if a.high
≤ -1.
tan
is an interval extension of tan. 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].
asinpi a
returns an enclosure of {asin(x)/π | x ∈ a
}. All values are in [-1/2, 1/2].
atanpi a
returns an enclosure of {atan(x)/π | x ∈ a
}. All values are in [-1/2, 1/2].