The element loop's run #
The run theorem of DescriptiveComplexity.Draw.elemRule, in the kit-discharge
idiom: one hypothesis – the program's rules at an injection of rule names are
the loop's – and the geometry of the working cell, and the machine carries
itself from the loop's entry checkpoint to its exit phase, the control folded
over every tuple of the enumeration.
The shape of the statement follows the loop's shape. The enumeration is
abstract – a finite linear order ι, in practice the lexicographic order
on control-held tuples – and the control's evolution is a family per index:
fsOf a j is the pointer before the j-th read of round a, tied together
by four equations (the entry initializes round a₀, each read stores its bit,
each advance dispatch opens the next round, the last round is recognized by
the exhaustion guard). Every read trip is one
DescriptiveComplexity.Draw.ReadKit discharge; the store, dispatch and
walk-back steps are single DescriptiveComplexity.Draw.Prog.step_move /
step_moveBack steps; the loop closes by
DescriptiveComplexity.Draw.reachesIn_of_ordLoop_card.
The run is proved with its cost (elem_reachesIn): given a width c for
one read trip, a round costs 2 + (c + 2) · nr – the dispatch, the walk back,
and per read the trip, the store and the walk back – and the whole loop that
once per element of the enumeration, plus the round that opens it and the step
that leaves. elem_run is the same run with the budget forgotten, at the width
every trip has anyway: twice the number of addresses. A space-bounded caller
reads that one; a clocked program compares the count with its clock.
Every track the loop touches – the read tracks and a reference track t₀ the
tape is presented along – is backed: its digits are carried by the
background at its own slot, which is what
DescriptiveComplexity.Draw.Data.back provides and what lets consecutive
trips walking different tracks share one tape term
(DescriptiveComplexity.Draw.trackTape_of_back).
What indexes the file is a parameter (DescriptiveComplexity.IxFile): a
track is a set of registers and the cells the reads stop at are registers, so
nothing here asks the file to have one register per element of the universe.
A backed track presents the naked background: a walked track whose digits the background already carries at its own slot adds nothing to the tape. This is what lets one leg's conclusion be the next leg's hypothesis when the two walk different tracks.
Dependency graph
A backed track's pass presentation is the background itself.
Dependency graph
The phase before the k-th read of a round – the fold checkpoint once
the reads are exhausted. DescriptiveComplexity.Draw.elemFirstRd is this at
0, DescriptiveComplexity.Draw.elemNextRd j at j + 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The working cell is nobody's register.
Dependency graph
The element loop's run, on a clock: from the entry checkpoint at the
marker to the exit phase one cell to its right, the control folded over the
whole enumeration – entered with initEl, each round's reads stored by
setFlag, each advance by advEl, the verdict handed to exitSt at the top
index – and the cost is one round's width once per element of the enumeration,
plus the round that opens it and the step that leaves.
Dependency graph
The element loop's run, the budget forgotten: what a space-bounded caller reads. The width of a trip is then the largest of the finitely many the loop takes.