Certified binary exponential, logarithm, and power by enclosure refinement #
Exact input decoding and outward-rounded binary-grid enclosures feed a nearest-even endpoint
check. Refinement increases the Taylor degree while the interval shrinks rapidly, and increases
the working precision when that progress stalls. The cases exp 0 = 1 and log 1 = 0 use point
enclosures.
Exponential uses format-derived rational argument bounds to skip impossible underflow and overflow
checks. Beyond these bounds, total logarithm-based comparisons handle extreme inputs. These
comparisons terminate independently of the options, which bound the direct enclosure search.
Every accepted result has a finite real-rounding certificate. A call that does not certify a result
returns a Failure saying why: an unsupported descriptor, a nonfinite input, an argument outside
the function's domain, a result beyond the finite range, or a search that did not settle.
The power a ^ b of a positive base is exp (b * log a). Writing a = s * 2 ^ e with s near
one, an enclosure of t = b * log a settles underflow and rejects overflow. It also gives an
integer k near t / log 2, from its lower endpoint and a 52-bit approximation of 1 / log 2,
and any integer is sound. Refinement then encloses exp (t - k * log 2) from enclosures of log s
and log 2, and rounds both endpoints times 2 ^ k without forming that power. The
exponential's working precision is independent of |t|, and the argument grid grows only with
the bit lengths of b and b * e, so a result near the end of a very wide exponent range needs
no work proportional to |t|. The logarithms of 2 and of j / 32 come from the shared constants
cache of Numerics.Enclosure.Constants, which keeps the series short. An exact result that is a
rounding boundary generally does not settle and ends inconclusive, but one whose reduced argument
is enclosed exactly, such as binary16 4 ^ -12.5 = 2 ^ -25, can still settle.
Why a certified evaluation returned no result.
An inconclusive result makes no claim about whether more refinement would succeed. The other
cases identify a format, input, domain, or finite-range obstruction.
- unsupportedFormat : Failure
The descriptor is not an IEEE binary format, which the enclosure kernels require.
- nonfiniteInput : Failure
An input is a NaN or an infinity.
- domain : Failure
The input is outside the supported real domain: the logarithm of a number at most zero,
log (1 + x)forx ≤ -1, or a certified power whose base is at most zero. - range : Failure
The exact result rounds beyond the largest finite value of the format.
- inconclusive : Failure
The search stopped without a certificate: its budget ran out, or the exact result lies on or too close to a rounding boundary, or it is a power the search does not settle.
Instances For
Instances For
Try successive enclosures, stopping immediately when the endpoints certify one encoding.
Instances For
The interval from zero to half the least subnormal, including the even tie at zero.
Instances For
First power of two above the normal range, used before direct exponential evaluation.
Instances For
The least rational that nearest-even rounding sends beyond the largest finite value of an IEEE descriptor: the largest finite value plus half its ulp.
Instances For
Argument lower bound that excludes exponential underflow, using log 2 > 1/2.
Instances For
Argument upper bound below the exponential overflow guard on supported descriptors.
Instances For
Accept a certified encoding, or report failure when there is none.
Instances For
The failure of an exhausted exponential search: range when exp argument - shift reaches the
overflow threshold, and inconclusive otherwise. The coarse argument screen avoids constructing
the threshold when overflow is already excluded: an IEEE format has emax ≥ 1, and
exp (emax / 2) < 2^emax lies below its largest finite value.
Instances For
Round the exponential of an exact rational if the enclosure budget certifies a finite result.
Instances For
Certify a finite rounded logarithm of a positive rational, rejecting other arguments.
Instances For
Certify exp argument - 1, subtracting one from the exact rational enclosure before rounding.
This retains small results that would be lost by rounding the exponential to one first.
The same comparison shortcut as expRat handles very negative arguments without constructing
their exponential. Unsupported descriptors, overflow, and an exhausted budget are failures.
Instances For
Certify log (1 + argument), forming the sum exactly before enclosing the logarithm.
In particular, a small nonzero argument is not lost by rounding 1 + argument to one.
Arguments at or below -1 are a domain failure, and the other failures are those of logRat.
Instances For
Real powers #
An upper bound on the number of bits of |value| above the binary point, read from the bit
lengths of its numerator and denominator: |value| < 2 ^ magnitudeBits value.
Instances For
Enclose log value for a positive rational on the grid of precision fractional bits.
With j the integer nearest 32 * value, log value = log (j / 32) + log (32 * value / j): the
first term comes from the cached table BinaryGrid.Internal.logTable, and for value in
[3/4, 3/2) the second argument lies within 1/48 of one, so its series needs about a third of the
terms. Values below 3/4 use the first table entry, since the index saturates at zero. Values from
about 3/2 up, and grids finer than the table's, use BinaryGrid.logUnreduced directly. The
identity holds for every positive j, so the choice affects the work only.
Instances For
Enclose exponent * log s + multiple * log 2 on one grid, from enclosures logScaled of log s
and logTwo of log 2 on that grid.
Instances For
Enclose exp x for every x in argument from one exponential enclosure at its lower end.
For a width w ≤ 1, exp (lo + w) ≤ exp lo * (1 + 2 * w). A wider argument evaluates the
exponential at its upper end as well.
Instances For
Enclose exp r from enclosures reduced grid of r on grids of grid fractional bits.
The argument is taken on the grid of precision + extraBits fractional bits.
Instances For
Round (scaled * 2 ^ binaryExponent) ^ exponent for a positive rational scaled if the
enclosure budget certifies a finite result.
An overflow evident from exponent * binaryExponent alone fails as range before any logarithm.
An enclosure of t = exponent * log (scaled * 2 ^ binaryExponent) on the first grid settles a
result below half the least subnormal as +0, by rounding [0, 1] times
2 ^ (minSubnormalExponent - 1) without forming that power. It fails as range for a result at
least 2 ^ (maxNormalExponent + 1), comparing t with the same grid's enclosure of log 2.
Otherwise refinement encloses exp (t - k * log 2) for an integer k near t / log 2, reusing
the first enclosure of t in its first attempt, and accepts when both endpoints times 2 ^ k
round to the same finite encoding. The options' degree applies to the exponential, while the
logarithm series take their degrees from the grid. Unsupported descriptors, nonpositive scaled,
overflow, and an exhausted budget are failures. A result within a rounding step of the overflow
threshold also ends the search as inconclusive.
Instances For
Round base ^ exponent for exact rationals with a positive base if the enclosure budget
certifies a finite result. Nonpositive bases, unsupported descriptors, overflow, and an exhausted
budget are failures.
Instances For
An integer n with |exponent * log base| < 2 ^ n for a positive dyadic base, read from the
stored fields without forming either rational.
Instances For
An interval around one that contains exp t whenever |t| < 2 ^ -(fracWidth + 4).
Instances For
The failure of a power whose stored exponent field marks an integer exponent too large for the
search: range when the power overflows, a base above one with a positive exponent or below one
with a negative exponent, and inconclusive otherwise.
Instances For
Certify a finite exponential using exact decoding and outward-rounded enclosures.
Instances For
Certify base ^ exponent for a finite positive base and a finite exponent.
Both inputs are decoded exactly as dyadics, and the base's significand alone is split as
scaled * 2 ^ e, so the base's power-of-two scale is never formed. When the stored fields show
|exponent * log base| < 2 ^ -(fracWidth + 4) the result rounds to one without forming the
exponent's rational: in a format with a very wide exponent field its denominator can have billions
of bits. An exponent decoded as a dyadic b with stored binary exponent
b.exponent > fracWidth + expWidth + 8 stops before its rational is formed: it is an integer so
large that only a base of one has a finite nonzero rounded power, and powHugeFailure reports
whether the power overflows. Once these two checks have bounded its size, the general path forms
the exponent's rational. Non-IEEE descriptors, nonpositive or nonfinite bases, nonfinite exponents,
overflow, and an exhausted budget are failures too.