Legend:
Library
Module
Module type
Parameter
Class
Class type

The theory of floating-point numbers modulo transcendental functions.

This signature includes several functions that can be expressed in terms of a finite sequence of the operations of addition, multiplication, and root extraction. Despite the fact, that those operation are defined in the Basic Theory of Floating points (Fbasic), operations in this signature couldn't be expressed in terms of Fbasic because the set of floating points is finite. Therefore the operations in this signature are defined in terms of real numbers arithmetic.

For example, the following expression is not true for all x,y,m:

fmul m x (fmul m x x) = pown m x (succ (succ one)),

E.g., when fmul m x x is not denoted with x^2, but the number that is closest to x^2 with respect to the rounding mode m.

The denotation is not defined if x represents zero.

Rounding modes

Many operations in the Theory of Floating-Point numbers are defined using the rounding mode parameter.

The rounding mode gives a precise meaning to the phrase "the closest floating-point number to x", where x is a real number. When x is not representable by the given format, some other number x' is selected based on rules of the rounding mode.

The denotation is the floating-point number nearest to the denoted real number. If the two nearest numbers are equally close, then the one with an even least significant digit shall be selected. The denotation is not defined, if both numbers have an even least significant digit.

The denotation is the floating-point number nearest to the denoted real number. If the two nearest numbers are equally close, then the one with larger magnitude shall be selected.

fsqrt m x returns the closest floating-point number to r, where r is such number that r*r is equal to x.

If x is a negative finite non-zero number, or is nan, or is the negative infinity, then sqrt x is nan. If x is the positive infinity then fsqrt x is the positive infinity.