Opt-in transcendentals for configured binary values #
This module adds deterministic exp, log, sin, cos, sinCos, sinh, cosh, and tanh
approximations, the floating-point power pow, and the MathFunctions instance to
ExecFloat.Binary. The lifting theorems below carry the model results through packing. These
kernels use nearest-even arithmetic and IEEE-style exceptional values. They carry no general
real-error bound.
Certification is an option. exp x (certify := true), and likewise log and pow, refines
rational enclosures of the real function and returns Except Certified.Failure Value: either a
result proved finite and equal to nearest-even rounding of the real function, or the reason
there is none (an unsupported format, a nonfinite input, a domain or range failure, or a search
that did not settle within its budget). Once certification is requested there is no fallback to
the approximation. expMinus1 and logPlus1 exist only in certified form. They form exp x - 1
and log (1 + x) before rounding, retaining small results near zero. The MathFunctions
instance uses the approximation kernels.
ExecFloat.Binary.exp x (certify := true)
ExecFloat.Binary.pow x y (certify := true) (budget := { maxSteps := 32 })
Sine and cosine reduce their arguments by the Payne-Hanek reduction of
Numerics.Enclosure.ArgumentReduction, reading at most 2^21 bits of 2 / pi. In a format with at
most 524,258 fraction bits, every finite argument below 2^(2^20) stays within that limit.
Arguments that would need more bits, such as the largest ones of a 31-bit exponent field, and
reductions whose permitted windows are all rejected give the format's invalid result. These APIs
return no IEEE status flags. The optional Arb adapter supports directed rounding through an
external library.
import FloatLib keeps binary elementary functions opt-in. Certified sqrt and abs, the
MathFunctions class, and its host Float and real instances are available by default.
The exponential eˣ in the configured binary format: by default the deterministic approximation,
and with certify := true a certified nearest-even result or the Certified.Failure that
prevented one, searching within budget.
Instances For
The natural logarithm in the configured binary format: by default the deterministic
approximation, and with certify := true a certified nearest-even result or the
Certified.Failure that prevented one, searching within budget.
Instances For
The power base ^ exponent, by Model.pow by default.
Model.pow gives zeros, infinities, and NaNs their IEEE 754 special cases. For an IEEE
descriptor, a finite result for a nonzero base and an integral exponent is correctly rounded, and
a positive base with any other exponent runs the certified search first. A certified range
failure delivers positive overflow; other failures fall back to exp (exponent * log base). With
certify := true only the certified search runs, for a finite positive base and a finite exponent,
and its failure is returned instead of the fallback.
Instances For
Certify exp x - 1 with one final rounding, preserving signed zero, searching within budget.
There is no uncertified form: the result is a certified nearest-even value or the
Certified.Failure that prevented one.
Instances For
Certify log (1 + x) with one final rounding, preserving signed zero, searching within budget.
There is no uncertified form: the result is a certified nearest-even value or the
Certified.Failure that prevented one.
Instances For
Deterministic approximation to sine in the configured binary format.
Instances For
Deterministic approximation to cosine in the configured binary format.
Instances For
Compute sine and cosine together, sharing argument reduction before repacking both results.
Instances For
Deterministic approximation to hyperbolic sine in the configured binary format.
Instances For
Deterministic approximation to hyperbolic cosine in the configured binary format.
Instances For
Deterministic approximation to hyperbolic tangent in the configured binary format.
Instances For
Representation bridge theorems #
Decoding configured exponential gives the deterministic model kernel.
Decoding configured logarithm gives the deterministic model kernel.
Decoding the configured power gives Model.pow.
Decoding configured sine gives the deterministic model kernel.
Decoding configured cosine gives the deterministic model kernel.
Decoding joint sine/cosine gives both results of the shared model kernel.
Decoding configured hyperbolic sine gives the deterministic model kernel.
Decoding configured hyperbolic cosine gives the deterministic model kernel.
Decoding configured hyperbolic tangent gives the deterministic model kernel.
Configured binary values implement the shared elementary-function interface.
This lets generic programs use MathFunctions.exp, MathFunctions.sin, and the other operations
without knowing the binary descriptor. sqrt and abs here are the certified operations already
on the default import. The remaining fields are the approximations defined above.
Certified results #
Decoding a certified exponential gives the model kernel's result or failure.
Decoding a certified logarithm gives the model kernel's result or failure.
Decoding a certified power gives the model kernel's result or failure.
Decoding expMinus1 gives the model kernel's result or failure.
Decoding logPlus1 gives the model kernel's result or failure.
A certified exponential is finite.
A certified exponential is the nearest-even rounding of the real exponential.
A certified logarithm is finite.
A certified logarithm is the nearest-even rounding of the real logarithm.
A certified power is finite.
A certified power is the nearest-even rounding of the real power toReal base ^ toReal exponent
(Real.rpow, since the base of a certified power is positive).
A certified expMinus1 result is finite.
A certified expMinus1 result is one nearest-even rounding of Real.exp x - 1.
A certified logPlus1 result is finite.
A certified logPlus1 result is one nearest-even rounding of Real.log (1 + x).