Module supertask 

The run-time half of the supertask engine: the exact operations the statements it writes call, generic over a value model (ValueAlgebra) so the interpreter and a compiled program run one implementation.

The engine resolves a supertask by rewriting the loop into ordinary statements; what those statements cannot express in arithmetic alone lives here, each as a builtin every tier runs the same way.

• trip_count: how many times a loop stepped by a clock runs — an infinite natural when the step is infinitesimal.
• affine_power: Aᴺ·x for an exact matrix whose eigenvalues are roots of unity, at an infinite N. With A^z·(A^p − I)^m = 0 (read off the characteristic polynomial, then checked by multiplying it out), q ↦ A^(z + r + p·q)·x is a polynomial of degree below m in q for each residue r, so m samples and their forward differences give Aᴺ·x = Σ_j C(q, j)·Δʲ exactly, read on each residue class of N.
• polynomial_flow: N Euler steps of a polynomial differential equation, ending on the validated solution’s germ.
• hybrid_flow: N steps of a loop whose state flows by a polynomial Euler step between jumps: the values of the ideal hybrid system it follows (see crate::hybrid), Zeno tails and continuous firing included, each a germ known by its standard part or, where the loop’s own value is exactly it, that value.
• cycle_at: the state at step N of a recorded run that has entered a cycle.
• first_exit: how many passes a loop makes whose guard compares terms linear in a counter it steps — While not (n <= x and x < n + 1):, the floor of Imamura’s Lemma 1 — read where the guard’s truth can change, and on each residue class of the generator where those points depend on it.
• search_candidates: the naturals at which a search over every natural must look. A predicate built from linear terms a·n + b and remainders modulo m is constant between the integers where some a·n + b changes sign and periodic with the period lcm(m) there, so its first witness, if any, lies at a sign change or within one period after one.

Functions

affine_power

Aᴺ·x. See the module documentation.

check_annihilator

The certificate the closed form rests on, checked by multiplying it out: A^z·(A^p − I)^m = 0.

cycle_at

The state at step n of a run recorded as states (the state before each step) up to the step whose state, repeated, had been seen before: the run is eventually periodic from the first occurrence of repeated.

first_exit

How many passes While <guard>: makes when each pass adds step to its counter, from t0: the first natural k at which the guard fails at t0 + k·step. The guard compares terms linear in the counter (the formula Guard::read takes), so its truth can change only where one of them crosses zero and otherwise repeats with the period of its remainders; its first failure lies at a crossing or within one period after one, and is found by evaluating the guard there alone. Where those points depend on the residue of the generator — ⌊1/(2·dt)⌋ — each class is read on its own scale and the count is the infinite integer the classes’ answers make.

hybrid_flow

N steps of a loop whose body is polynomial Euler steps and jumps, as model encodes them: [body, jumps], the body its parts in order — ["flow", field] a run of flow statements as one polynomial update per slot, as for polynomial_flow, ["check", k] the check of jump k — and each jump [guard, block]. A finite N runs the steps themselves. An infinite one, N = T/dt + δ on each residue class, ends on the values of the ideal hybrid system the loop follows for time T (see crate::hybrid): a value the flow moves is a germ known by its standard part, a value the loop holds exactly is that value.

polynomial_flow

N passes of x ← x + dt·f(x) + O(dt²), f polynomial with rational coefficients. A finite N runs the update itself. An infinite one, N = T/dt + δ on each residue class, ends infinitely close to the solution of x' = f(x) from the start’s standard part at time T, a germ known by its standard part; a scalar solution certified to leave every bound before T leaves an unlimited germ.

search_candidates

The naturals a search over every natural must examine, in increasing order; empty when the predicate’s coefficients or periods are not ones this reading decides. See the module documentation.

state_size

The bits a state occupies — a number by its magnitude, text by its length, a list or tuple by its items, an exact value by its canonical encoding — the measure the cycle search stops a growing state by.

trip_count

How many times While t <relation> bound: runs when each step adds step to t, starting from t0: ⌈(bound − t0)/step⌉ for a strict bound, ⌊…⌋ + 1 for an inclusive one, 0 when the guard is false at the start. −1 — not counted, so the loop runs as written — when the clock is not a number, or when a standard step walks away from its bound; a refusal when an infinitesimal step does, since that loop could never end.

Type Aliases

Matrix

A square matrix of values, row by row.