Module hybrid 

Hybrid flows: loops of infinitesimal steps whose state flows between jumps — a bouncing ball, a thermostat — run exactly, as the ideal hybrid system their steps follow to within an infinitesimal.

A loop stepping its clock by dt whose body is an Euler step x ← x + dt·f(x) of a polynomial field and one or more jumps If guard: … stays, between jumps, within an infinitesimal of the flow of x' = f(x), and a jump whose guard the flow crosses fires within an infinitesimal of the crossing. Every value the loop leaves is therefore infinitely close to the value the ideal hybrid system leaves, and that value is what run computes, exactly, in real algebraic numbers:

• flights: a field whose Lie series terminates flows along polynomials in time, so a flight is a polynomial in the time since it began;
• events: a guard’s atoms along a flight are polynomials in time. Their real roots cut the flight into intervals on which every atom keeps one sign, and the guard fires at the first root after which it holds. A guard that only touches its boundary, two guards that fire at once, or a jump in the loop’s last step depend on which infinitesimal dt is, and are refused by name;
• jumps: the jump’s statements run on the state at the crossing in three-valued logic. Two values infinitely close to each other are told apart only by what is known of their difference: that the run holds both exactly, or a sign the guard or a reset implies;
• Zeno tails: when one jump’s events follow each other by a scaling — every quantity the guards read scaled by s^wᵢ and the time between events by s^q, under weights for which the field, the guards and the resets are homogeneous (check_scaling) — every later event is the scaled copy of the one before, every value at event k is a polynomial in z = sᵏ (plus a multiple of k for a count), and for s < 1 the events accumulate at the sum of a geometric series. The values there are those polynomials at z = 0;
• continuous firing: a jump whose guard holds again within an infinitesimal of its firing fires infinitely often in every standard interval — the ball at rest after its Zeno time. The state it writes stays where the jump holds it, the rest flows, and a value the jump records takes its value at the last firing where its condition holds.

Each value the run leaves says whether the loop’s own value is exactly it or only infinitely close to it.

Structs

Jump

If guard: block.

MPoly

A polynomial over the run’s slots with real algebraic coefficients: each monomial by its exponents, listed once, in order, none with a zero coefficient.

Model

A loop’s flow and jumps over its slots: its body in order, and the flow of a whole step — each slot’s rate, and whether a step leaves it exactly unchanged.

Scaling

A scaling certificate: from one round of the firings in cycle to the next, every slot in slots is multiplied by s^w (its weight w), and each time between firings by s^q.

Term

A polynomial over the slots whose coefficients are the standard parts of the program’s, with whether they are the program’s coefficients exactly.

UPoly

A polynomial in one variable with real algebraic coefficients, lowest power first, with no trailing zero: a coordinate of a flight in the time since it began, an atom along a flight, a value along a tail in z.

Enums

Cell

What a slot holds in the ideal run.

Cond

A condition of a guard or of a jump’s statements.

Item

One part of a loop’s body, in its order: a run of flow statements — each slot’s rate, the coefficient of dt in its Euler step, and whether the run leaves it exactly unchanged — or the check of a jump.

Rel

left − right compared with zero.

Stmt

Value

What a jump assigns: a polynomial over the slots, or a value no polynomial reads.

Constants

EVENT_BUDGET

The most firings a run follows one by one before the rest must be read off a scaling. Each firing’s values are exact numbers that grow as the firings go on, so the budget bounds the work as well as the count.

MAX_LIE_ORDER

The highest Lie derivative a field may need before its flow is taken not to be a polynomial in time.

Traits

Ring

What a polynomial over the slots evaluates in: algebraic numbers, polynomials in one variable, polynomials over the slots, values along a tail.

Functions

check_scaling

The certificate a tail rests on, checked on its own: the slots are closed under what feeds them, the field, the guards and the cycle’s statements setting them are homogeneous for the weights, after is the scaling’s image of before, and each flight of the round after is s^q times the same flight of the round before. A run whose state the scaling maps to its state a round later is then, round after round, the scaled copy of the round before. A scaling by one is the identity, which every model is homogeneous for: its certificate is that the state repeats.

real_roots

The distinct real roots of p, ascending; none for a constant.

run

The values a loop of infinitesimal steps leaves after span of its time, starting from start: each infinitely close to what the loop leaves, and exactly it where the cell says so.

scaled_slots

The slots a scaling of a cycle covers: every slot a guard reads, closed under what feeds them — the slots their rates read, and the slots a statement of the cycle setting one of them, or a condition it runs under, reads.

Type Aliases

Step

One firing of a cycle: which jump fires, and the branch each condition it meets takes.