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 by DescriptiveComplexity.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.

theorem DescriptiveComplexity.Draw.reflTransGen_of_ordLoop {C : Type} {Step : C → C → Prop} {A : Type} [LinearOrder A] [Finite A] {conf : A → C} (hstep : ∀ (w z : A), w < z → (∀ (a : A), ¬(w < a ∧ a < z)) → Relation.ReflTransGen Step (conf w) (conf z)) {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (a : A) : Relation.ReflTransGen Step (conf a₀) (conf a)

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.

theorem DescriptiveComplexity.Draw.reachesIn_of_ordLoop_card {A : Type} [LinearOrder A] [Finite A] {S : Type} {M : TMData S} {conf : A → Config S} {w : ℕ} (hstep : ∀ (x z : A), x < z → (∀ (a : A), ¬(x < a ∧ a < z)) → M.ReachesIn w (conf x) (conf z)) {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (a : A) : M.ReachesIn (w * Nat.card A) (conf a₀) (conf a)

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.

theorem DescriptiveComplexity.Draw.reflTransGen_of_tupLoop {C : Type} {Step : C → C → Prop} {A : Type} [LinearOrder A] [Finite A] {e : ℕ} {conf : (Fin e → A) → C} (hstep : ∀ (v v' : Fin e → A), TupSucc v v' → Relation.ReflTransGen Step (conf v) (conf v')) {v₀ : Fin e → A} (hbot : ∀ (j : Fin e) (a : A), v₀ j ≤ a) (v : Fin e → A) : Relation.ReflTransGen Step (conf v₀) (conf v)

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.