Expand description
Hyperreal numbers generated by the program’s infinitesimal dt — exact, ordered, decidable.
A program that declares Let dt be an infinitesimal. gets a positive number smaller than every
positive standard number. Every hyperreal value built from dt with the field operations is a
rational function of dt with real algebraic coefficients, N(dt)/D(dt), and that is how a
Hyperreal is held: reduced (gcd(N, D) = 1) with D comonic (its lowest-order nonzero
coefficient is 1), so equal values are structurally equal.
The order is decided exactly by the transfer principle for real closed fields: a rational
function of dt has, for every small enough positive standard t, the sign of its
lowest-order coefficient — so x > 0 exactly when the lowest-order coefficient of N is
positive (D being comonic). From the same expansion come the standard notions:
- the valuation
v(x) = ord N − ord D— positive for an infinitesimal, negative for an infinite value, zero for an appreciable one; - the standard part — the leading coefficient when
v = 0, zero whenv > 0, and none at all (the value is not limited) whenv < 0; x ≈ y—x − yis infinitesimal.
A value prints as the exact rational function in the infinitesimal’s name (3 + 2·dt, 1/dt,
(1 + dt)/(2 - dt)), with rational coefficients scaled to integers when that is possible.
Structs§
- Hyperreal
- A hyperreal number generated by the infinitesimal. See the module documentation.
Enums§
- Power
Error - Why a power is refused.
Constants§
- MAX_
POWER_ DEGREE - The highest degree one power may reach, so a single operation’s work stays bounded.