Commit 11a74b67 authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent 55796216
module DoubleExtensions.Constants
import DoubleExtensions.Predicates
|||
public export
eps : Double
|||
public export
epsSpec1 : Positive eps
module DoubleExtensions.Operations
{-
Ported from https://github.com/NAMEhzj/IPF_GroundOne/blob/master/Intervals/RoundedArithmetic.lhs
The IEEE standard 754-2008 requires availability of a function nextUp
and similarily nextDown, where nextUp(a) is the least floating-point
number in the format of a that compares greater than a. The function
nextUp thus computes the successor of a floating point number. This
just amounts to adding eta, the smallest subnormal positive number, if
directed rounding is available(as requested by IEEE754). We use this
idea a proposed in the 2009 paper"Computing predecessor and successor
in rounding to the nearest" by Rump, Zimmermann et al. to give
intervals that contain the results of the arithmetic operation. For
add we produce a lower bound and an upper bound with the functions
add_u (upper bound for add) and add_d for the lower bound. Our
procedures will work in any rounding mode, i.e. the result of fl(a°b)
is garanteed to lie between those boundaries provided it is finite,
where fl: Real -> Float denotes rounding to the nearest. The
advantage of the given procedures are that they are fast and efficient
in that they avoid a switching of rounding modes. The disadvantage is
that they do not always yield the tightest possible interval. For
details see the proofs in the above mentioned paper.
-}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment