Loops in the control: runs indexed by a finite linear order #
The element loops of the EXPSPACE program enumerate tuples of source elements
in the machine's control, one lexicographic successor per round. The register
loops have their induction principle already
(DescriptiveComplexity.reaches_of_wideRounds, driven by the address rank);
the control loops get theirs here, driven by
DescriptiveComplexity.order_induction:
DescriptiveComplexity.Draw.reflTransGen_of_ordLoop– a run per immediate successor of a finite linear order carries the machine from the bottom to anywhere;DescriptiveComplexity.Draw.reflTransGen_of_tupLoop– the same over tuples in the lexicographic order, the rounds indexed byDescriptiveComplexity.TupSucc, which is the shape of the guards the advancing rules read (DescriptiveComplexity.succTupF).
Both are stated for an arbitrary relation on an arbitrary configuration type:
nothing here is about wide machines, and the reachability they produce is fed
to Relation.ReflTransGen.trans like any other phase.
Both also have a budgeted form – reachesIn_of_ordLoop and
reachesIn_of_tupLoop, with reachesIn_of_ordLoop_card for the crude bound –
which keeps the count a clocked program has to compare with its clock: one
round's budget, once per element of the enumeration. A space-bounded program
throws the count away and uses the two above.
A loop over a finite linear order: one run per immediate successor carries the machine from the configuration of the bottom element to the configuration of any element.
Dependency graph
A loop over a finite linear order, on a clock: one budgeted run per
immediate successor, and the machine reaches the configuration of any element
paying that budget once per element it crossed. The count is orank, the
number of elements strictly below the target, so a whole loop costs
w · (card − 1) and a clocked program can compare it with its clock.
This is DescriptiveComplexity.Draw.reflTransGen_of_ordLoop with the budget
kept, and it is what turns every element and tag loop of the evaluation into a
cost.
Dependency graph
A loop over a finite linear order, at the crude bound: the whole loop costs at most the budget of one round times the number of elements. What a clock is compared with.
Dependency graph
A loop over tuples in the lexicographic order: one run per
coordinatewise successor (DescriptiveComplexity.TupSucc, the shape the
advancing guards read) carries the machine from the all-minimal tuple to any
tuple.
Dependency graph
A loop over tuples in the lexicographic order, on a clock: one budgeted run per coordinatewise successor, and the whole enumeration costs that budget once per tuple. This is the cost of every coordinate loop of the evaluation.