Module limit_value 

Values at the end of a supertask: what depends on the infinite generator’s residue, the limit rules that turn such a value into one number, and the provisional answer of an unfinished search.

A program’s infinitesimal is dt = 1/H for an infinite natural H the program never fixes. A loop that runs H times can end in a state that depends on H itself — Thomson’s lamp, toggled H times, is on exactly when H is odd. Which residues H may take is all the program knows (Let dt be an infinitesimal whose reciprocal is even.), recorded as a ResidueType: the residues allowed modulo some modulus. In Presburger arithmetic the complete type of an infinite natural is exactly its residue system — an element of the profinite integers — so a residue type is the most a program can say about H without naming it.

A Depends value is the same quantity on every residue class of H, held modulo the smallest modulus that still separates its branches. When the residue type pins a single branch it is an ordinary value; otherwise it prints its dependence (0 when ⌈1/dt⌉ is even, 1 when it is odd) and a LimitRule resolves it: the limit superior or inferior (the extreme branch, the infinite-time Turing machine’s rule at a limit stage), the Cesàro mean (each admitted residue weighted by its density), or the limit itself, which exists only when every branch agrees.

A Converging value is the answer of a search no proof has settled: the current guess, how many cases were checked and how often the guess changed — Shoenfield’s limit lemma made honest.

Structs

Converging

The answer of a search: settled by a certificate, or provisional with its evidence.

Depends

A quantity on every residue class of the generator. See the module documentation.

ResidueType

The residues the infinite generator may take. See the module documentation.

Enums

LimitRule

How a quantity that depends on the generator becomes one value at the limit.

ResidueError

Why a residue system cannot be formed.

Constants

MAX_MODULUS

The most residue classes one value may be split over: the wire’s collection bound, so every value a program holds can travel.