Zero-dependency Standard ML library for interval arithmetic with conservative outward rounding.
signature INTERVAL =
sig
type ivl = { lo : real, hi : real }
exception Divide
val make : real * real -> ivl
val singleton : real -> ivl
val width : ivl -> real
val mid : ivl -> real
val contains : ivl -> real -> bool
val hull : ivl -> ivl -> ivl
val intersect : ivl -> ivl -> ivl option
val add : ivl -> ivl -> ivl
val sub : ivl -> ivl -> ivl
val mul : ivl -> ivl -> ivl
val divide : ivl -> ivl -> ivl (* raises Divide if rhs contains 0 *)
val neg : ivl -> ivl
val abs_ : ivl -> ivl
val sqr : ivl -> ivl
val sqrt_ : ivl -> ivl
val exp_ : ivl -> ivl
val ln_ : ivl -> ivl
val sin_ : ivl -> ivl
val cos_ : ivl -> ivl
val intervalNewton : {f: ivl -> ivl, fPrime: ivl -> ivl, x0: ivl, tol: real}
-> ivl list
end(* Bound sqrt(2) using interval Newton *)
fun f x = Interval.sub (Interval.sqr x) (Interval.singleton 2.0)
fun fp x = Interval.mul (Interval.singleton 2.0) x
val roots = Interval.intervalNewton
{f=f, fPrime=fp, x0=Interval.make(1.0, 2.0), tol=1e~10}
(* roots contains an interval [a,b] with |a-b| < 1e-10 enclosing sqrt(2) *)
(* Range of sin on [0, pi] *)
val range = Interval.sin_ (Interval.make (0.0, Math.pi))
(* range = [-eps, 1+eps] where eps is a tiny outward-rounding bound *)- Outward rounding uses a small relative nudge (≈1e-14) rather than true directed rounding, so enclosures are conservative but not guaranteed tight.
sin_andcos_check for critical points within the interval; for wide intervals (>2π) they return [-1, 1].- The interval Newton method is a simple fixed-point iteration; convergence is not guaranteed for all inputs.
- Does not support extended intervals, interval matrices, or multi-dimensional arithmetic.
Requires MLton and Poly/ML in PATH.
make all-tests