Module tower 

The exact real types in a program’s value model: real algebraic numbers, computable reals, the program’s infinitesimal and the hyperreals it generates, infinite integers, ordinals, and the values a supertask leaves.

Each type lives in its own module of this crate; this module decides how they mix with the numeric tower and with each other, once, for every value model that holds them. A value model (the interpreter’s runtime value, a compiled program’s value) implements TowerValue: how to see one of its values as an exact type or a standard number, and how to build one. Everything here is generic over it, so every tier computes, compares and prints these values identically.

• an integer, rational or float operand is lifted exactly (a float is the dyadic rational it denotes, never a rounding of the other side) into the exact type it meets;
• real algebraic numbers sit below computable reals; the hyperreals are generated by the infinitesimal over the algebraic numbers, exactly as rational functions of dt; a value a flow leaves, or a computable transcendental meeting the infinitesimal, is a germ — known by its series in dt with exact coefficients, compared by the sign of its first nonzero one;
• an infinite integer meets a standard integer as an infinite integer (+ − ×, floor division and remainder keep integer meaning) and anything fractional as a hyperreal;
• a value that depends on the residue of 1/dt lifts every operation branch by branch, and a comparison of infinite integers can itself depend on that residue;
• an ordinal meets only ordinals and naturals.

Every result is held in its smallest exact form — a hyperreal with no infinitesimal part is its standard value, a hyperreal that is an integer for every admitted ⌈1/dt⌉ is that infinite integer, an algebraic number that is rational is a rational — so a value has one representation whatever route produced it, exactly as the tower downsizes BigInt to Int.

Structs

Branch

One branch of a residue-dependent value, compared by value.

DependsValue

A value that depends on the residue of ⌈1/dt⌉.

HyperValue

A hyperreal value with the infinitesimal it is written in.

NaturalValue

An infinite integer with the infinitesimal whose reciprocal generates it.

Scale

An infinitesimal of the program: the name it was declared under, what is known about the residues of its reciprocal, the infinite natural ⌈1/dt⌉, and where it stands among the others.

Enums

ExactRef

A value of a value model seen as one of the types this module governs.

HyperForm

A hyperreal’s representations: an exact rational function of dt; a real algebraic Puiseux series that is none, a root of one (crate::puiseux); the germ a flow leaves, known by its series in dt; or a value of several ordered infinitesimals (Multi). A Puiseux series compares and hashes by its value, a germ by its canonical encoding.

Op

The arithmetic operators the exact types take.

RealFn

A function of the reals the exact types take: the square root, the exponential, the natural logarithm.

Rel

The relational operators the exact types answer.

Rounding

How an integer part rounds: down, up, or to the nearest integer with ties away from zero (the tower’s round).

Shape

A value’s structure, as far as the supertask runtime reads it: the scalar kinds it treats apart, and the items of a list or a tuple.

Traits

TowerValue

A value model that holds the exact types: how to see a value as one of them or as a standard number, and how to build one. The interpreter’s runtime value and a compiled program’s value each implement it; every operation in this module is generic over it.

ValueAlgebra

A value model’s whole arithmetic and its lists: what the supertask runtime computes with. Each operation is the language’s own on that model, exact types and standard numbers alike.

Functions

apply_limit

Resolve a residue-dependent value under a limit rule; a value that does not depend on the residue is its own limit under every rule. A value that depends on the residues of several generators resolves each branch’s finer dependence first: the residues of different generators are independent, so the rule over every pair of classes is the rule over the coarser generator’s classes of the rule over the finer one’s.

arith

Apply op when either operand is an exact type; None when neither is (the tower handles it), and for + with a Text operand, which joins the other value as it prints by the value model’s own rule for every value. recurse is the value model’s full arithmetic, used to lift an operation over residue branches and through provisional values.

carry_evidence

v carrying the evidence a provisional or settled answer c carries. An answer never holds another: when v carries evidence of its own, the two join into one (Converging::joined).

depends_from_parts

A residue-dependent value rebuilt from its scale, modulus and per-class values.

display

How an exact value prints; None for any other value.

euler

e, exactly.

exact_bytes

An algebraic number (0), computable real (1) or ordinal (2) as its canonical bytes; None for any other value, and for a real built from a function a program defines, which stays with the program.

exact_power

base ** exponent for an exponent that is an exact number — what ** and pow are when their exponent is one: a fraction p/q takes the real q-th root and raises it to p (2 ** (1/2) is √2, dt ** (1/2) is √dt, an even root of a negative number refused), and any other exponent is the language’s own **, a float on either side the float power. A residue-dependent or provisional operand is followed branch by branch.

from_algebraic

The canonical value of an algebraic number: a rational is an Int/BigInt/Rational.

from_closed

The canonical value of a value of the real closure: a rational function of dt is that hyperreal, in its own smallest form.

from_depends

The canonical value of a residue-dependent value: a branch that itself depends on the residue is read on its own class, a single branch is that value, and a dependence whose every branch is an integer polynomial in 1/dt on its class is that infinite integer.

from_exact_bytes

The value exact_bytes wrote; None for a forged or non-canonical encoding.

from_exact_real

The canonical value of a computable real: an algebraic one is an algebraic number.

from_germ

The canonical value of a germ: one built as a rational function of dt is that hyperreal.

from_hyper

The canonical value of a hyperreal: a standard value is its standard part, and a polynomial in 1/dt that is an integer for every admitted ⌈1/dt⌉ is that infinite integer.

from_multi

The canonical value of a value of several infinitesimals: a standard number is that number, and a value of one infinitesimal is that infinitesimal’s own.

from_natural

The canonical value of an infinite integer: a standard one is an Int/BigInt, and one whose branches are standard but differ is a residue-dependent integer.

from_ordinal

A finite ordinal is a natural number.

from_scaled_bytes

The value scaled_bytes wrote; None for a forged or non-canonical encoding.

generator_of

The infinite natural ⌈1/dt⌉ generated by an infinitesimal value.

germ_of

A number as a germ: a standard number as a constant, a hyperreal by its series or as the germ it is, an infinite integer that does not depend on the residue by its series; None otherwise.

integer_part

The integer part of an exact value under mode; None when v is not one (the tower handles it). recurse is the builtin itself, for the standard values inside a dependence or a provisional answer.

is_exact_value

True for a value of one of the types this module governs.

is_infinitesimal

x ≈ 0: zero or an infinitesimal.

is_infinitesimal_relative

Zero, or smaller than every positive value of at and of the infinitesimals larger than it.

is_limited

Bounded by a standard number.

is_limited_relative

Bounded by a value of at and of the infinitesimals larger than it.

limit_rule

A limit rule by its English name.

map_depends

f on every branch of a residue-dependent value, or the first error a branch raises.

new_infinitesimal

The program’s infinitesimal: Let <name> be an infinitesimal …, its reciprocal’s residues modulo modulus limited to allowed (the parser has already intersected the stated facts), or the contradiction refused when nothing is allowed.

new_ordered_infinitesimal

Let <name> be an infinitesimal much smaller than <larger> [and much larger than <smaller>] …: an infinitesimal below larger and above smaller, each an infinitesimal itself or nothing, with its reciprocal’s residues as new_infinitesimal reads them. Refused when a bound is no infinitesimal, when the two bounds are not already ordered, and when the name is one an infinitesimal it would be ordered with already has.

not

not lifted over residue branches and through provisional values; None for any other value.

omega

ω, the first infinite ordinal.

pi

π, exactly.

provisional

A provisional answer: the current guess after steps cases with revisions changes. A guess that is already an answer joins this evidence to its own.

real_fn

f of v, exactly. A standard number goes in as the rational it denotes (a float as its dyadic rational), an algebraic number or a computable real as itself, and the answer is held in its smallest exact form: sqrt(4) is 2, sqrt(2) is √2, exp(0) is 1, ln(e) is 1. The square root of a hyperreal or an infinite integer is its root in the real closure (crate::puiseux): sqrt(dt) is √dt. Every other function of a value of the infinitesimal is the germ of it (Germ): exp(dt) is 1 + dt + O(dt^2), ln(1 + dt) is dt - (1/2)·dt^2 + O(dt^3), and the root of a germ is a germ. What is no germ is refused by name: the exponential of an infinite value, beyond every power of dt, and the logarithm of a positive infinitesimal or an infinite value, which carries ln(dt). A residue-dependent value is mapped branch by branch and a provisional one keeps its evidence; a function of an ordinal has no exact form.

relation

Apply rel when either operand is an exact type; None when neither is. The answer is a Bool, or a residue-dependent Bool when it depends on ⌈1/dt⌉; a comparison no theorem decides within the budget is a loud error.

scale_from_parts

The scale scale_parts wrote.

scale_parts

The infinitesimal’s name and its declaration’s bytes (Scale::to_bytes): its reciprocal’s residue facts, and where it stands among the others.

scaled_bytes

A hyperreal (0), infinite integer (1), germ (2), root of a hyperreal (3), exact value of several infinitesimals (4), germ of several (5) or infinite integer of several (6) as its scale and canonical bytes — the scale of a value of several its smallest infinitesimal, the bytes naming every one it involves; None for any other value, and for a germ holding a real built from a function a program defines.

standard_part

The standard part: a hyperreal’s standard value, branch by branch for a residue-dependent value; a standard value is its own. An infinite value has none.

standard_part_relative

The standard part relative to the infinitesimal at: what v is infinitely close to among the values of at and the infinitesimals larger than it, every smaller infinitesimal read at zero — the inner limit with at held fixed. the standard part of dt + dx relative to dt is dt.

structurally_equal

Structural equality for collections and hashing: exact forms by value, a general computable real by the formula that built it; None when neither value is an exact type.

transmissible

Whether a value of the exact types can travel as data — to a task, through a channel, over the wire: every value but one holding a real built from a function a program defines, in itself, in a germ, in a branch of a residue-dependent value or as a provisional answer. A value model’s own lists are its own to walk.

undecided_branch

Why a value cannot decide a branch — a residue-dependent answer, or a provisional one no proof settled — or None for any other value. Every tier refuses such a branch with this sentence.