Module exact_real 

Exact real numbers: every computable real, to any precision, with equality decided wherever a theorem decides it.

An ExactReal is one of four forms. Three are exact forms whose equality is decidable:

• an Algebraic number (rationals included);
• an exponential-algebraic sum Σ aₖ·e^{βₖ} with complex algebraic aₖ, βₖ — what exp, sin and cos of algebraic arguments produce, and what linear differential equations integrate to. By the Lindemann–Weierstrass theorem the e^{βₖ} for distinct algebraic βₖ are linearly independent over the algebraic numbers, so a sum is zero exactly when every coefficient is zero after like exponents are merged: equality is a finite symbolic check;
• a Laurent polynomial in π Σ aₖ·πᵏ with algebraic aₖ — zero exactly when every coefficient is, because π is transcendental.

Everything else — a mix of π with exponentials, a logarithm, an exponential of a transcendental, a number a program defines by a function (ExactReal::defined) — is a general computable real: an expression DAG that encloses its value in a dyadic interval at any requested working precision. Equality of general reals is undecidable (it contains the halting problem), so compare refines until the values separate and reports a typed RealError::Inseparable when a budget runs out first; compare_within is total. There is deliberately no PartialEq: numeric equality is compare, which answers Equal only when an exact form proves it.

Evaluation is fixed-point dyadic arithmetic (m·2^e, no gcds): π by Machin’s formula (cached at the highest precision computed), ln 2 = 2·atanh(1/3), exp by argument halving, Taylor and repeated squaring, log by atanh, sin/cos by reduction modulo 2π, Taylor and the double-angle formulas, square roots by integer Newton. Every primitive returns a rigorous enclosure with its truncation errors counted, so every printed digit is certain.

Structs

ExactReal

A computable real number. See the module documentation.

Enums

Closeness

The answer of a comparison within a tolerance: which side, or within the tolerance.

Definition

How a program’s function gives its real number.

RealError

Why an exact real could not answer.

Constants

DEFAULT_BUDGET

The precision budget, in bits, of a comparison whose budget the caller does not state.

DISPLAY_DIGITS

Significant digits a general computable real prints with.

STAYS_WITH_ITS_PROGRAM

What a real number built from a function a program defines is, where a task, a channel or the wire refuses it: it stays with the program that defines it.

Traits

Approximant

A program’s function a real number is defined by, as the tier running the program calls it from inside a refinement. The tier evaluates the function in a context of its own, so a call made in the middle of another computation changes nothing the program can see.

Functions

not_a_rational_answer

The refusal of a function’s answer at n that is a value of type_name, not a rational.

not_sendable

The sentence a program stops with when it hands a task, or sends through a channel, a value that holds a real number a function of the program defines.