The element loop: a sub-fold over control-held tuples

The remaining atom subroutines of the EXPSPACE program are all one shape: enumerate a tuple of elements in the control's loop-variable slots, per tuple run a fixed sequence of named single-bit read trips – the ρ-bit leaves – and fold the leaf's value into the sub-fold accumulators. The expansion atoms run it over the defining sentence's prefix with one read per block atom of its matrix; a point equality or order atom runs it over the coordinate tuples with two reads, one per compared block; the domain gate runs it for X.dom.

The sites: an entry checkpoint (initializing the loop variables and accumulators), the read trips chained head to tail – each verdict exit stores its bit and enters the next – and a fold checkpoint whose advance dispatch folds and re-enters the first read, its exhaustion dispatch folds and leaves. The base-structure atoms of a leaf – L-atoms and order atoms on the control-held elements – need no tape at all: a guard or a dstSt is any function of the pointer, and the reduction, which writes the transition table by formulas, may evaluate them there. As everywhere, the semantic parameters stay abstract.

The shapes

inductive DescriptiveComplexity.Draw.ElemPh (nr : ℕ) : Type

The phases of an element loop: the entry checkpoint, the read trips, the fold checkpoint.

• e0 {nr : ℕ} : ElemPh nr

  The entry checkpoint.

• rdP {nr : ℕ} : Fin nr → ReadPh → ElemPh nr

  The j-th read trip of the current tuple.

• e1 {nr : ℕ} : ElemPh nr

  The fold checkpoint.

inductive DescriptiveComplexity.Draw.ElemSite (nr : ℕ) : Type

The sites of an element loop.

• e0 {nr : ℕ} : ElemSite nr

  The entry checkpoint.

• rd {nr : ℕ} : Fin nr → ElemSite nr

  A read trip.

• e1 {nr : ℕ} : ElemSite nr

  The fold checkpoint.

def DescriptiveComplexity.Draw.ElemSh (nr : ℕ) : ElemSite nr → Type

The rule shape of each site.

Equations

• DescriptiveComplexity.Draw.ElemSh nr DescriptiveComplexity.Draw.ElemSite.e0 = DescriptiveComplexity.Draw.EvalChkRule
• DescriptiveComplexity.Draw.ElemSh nr (DescriptiveComplexity.Draw.ElemSite.rd a) = (DescriptiveComplexity.Draw.ReadRule ⊕ Bool)
• DescriptiveComplexity.Draw.ElemSh nr DescriptiveComplexity.Draw.ElemSite.e1 = DescriptiveComplexity.Draw.EvalChkRule

def DescriptiveComplexity.Draw.elemOwn {nr : ℕ} : ElemPh nr → ElemSite nr

The owner of each phase of an element loop.

Equations

• DescriptiveComplexity.Draw.elemOwn DescriptiveComplexity.Draw.ElemPh.e0 = DescriptiveComplexity.Draw.ElemSite.e0
• DescriptiveComplexity.Draw.elemOwn (DescriptiveComplexity.Draw.ElemPh.rdP j a) = DescriptiveComplexity.Draw.ElemSite.rd j
• DescriptiveComplexity.Draw.elemOwn DescriptiveComplexity.Draw.ElemPh.e1 = DescriptiveComplexity.Draw.ElemSite.e1

def DescriptiveComplexity.Draw.elemFirstRd {P : Type} {nr : ℕ} (emb : ElemPh nr → P) : P

The first read's entry, or the fold checkpoint when there is no read.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.Draw.elemNextRd {P : Type} {nr : ℕ} (emb : ElemPh nr → P) (j : Fin nr) : P

The phase after the j-th read.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.Draw.elemRule {A Q W P : Type} {nr : ℕ} (one : A) (wk rg : W) (emb : ElemPh nr → P) (rdTrack : Fin nr → W) (MatchOf : Fin nr → (Q → A) → (W → A) → Prop) (setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : (Q → A) → (W → A) → Q → A) (IsMaxEl : (Q → A) → Prop) (exitPh : P) (i : ElemSite nr) : ElemSh nr i → Rule A Q W P

The rules of an element loop.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.elemRule_dstPh {A Q W P : Type} {nr : ℕ} (one : A) (wk rg : W) {emb : ElemPh nr → P} (rdTrack : Fin nr → W) (MatchOf : Fin nr → (Q → A) → (W → A) → Prop) (setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : (Q → A) → (W → A) → Q → A) (IsMaxEl : (Q → A) → Prop) (exitPh : P) (i : ElemSite nr) (ρ : ElemSh nr i) : (∃ (p : ElemPh nr), (elemRule one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ).dstPh = emb p) ∨ (elemRule one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ).dstPh = exitPh

An element loop leaves only into its own phases or its exit: the reads' trips stay inside the loop's phases (DescriptiveComplexity.Draw.ReadKit.dstPh_emb), the dispatches land at the next read or the fold checkpoint, and the last one leaves. This is what a caller reads off a stage to know the phases the machine can be in.

theorem DescriptiveComplexity.Draw.elemRule_dstIn {A Q W P : Type} {nr : ℕ} (one : A) (wk rg : W) {emb : ElemPh nr → P} (rdTrack : Fin nr → W) (MatchOf : Fin nr → (Q → A) → (W → A) → Prop) (setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : (Q → A) → (W → A) → Q → A) (IsMaxEl : (Q → A) → Prop) (exitPh : P) {S : P → Prop} (hemb : ∀ (p : ElemPh nr), S (emb p)) (hexit : S exitPh) (i : ElemSite nr) (ρ : ElemSh nr i) : S (elemRule one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ).dstPh

A property of a loop's phases and its exit holds of every phase it can move to. This is the form a caller uses: give the property, check it of the loop's own phases and of the exit, and every rule respects it.

theorem DescriptiveComplexity.Draw.elemHosrc {A Q W P : Type} {nr : ℕ} (one : A) (wk rg : W) {emb : ElemPh nr → P} (rdTrack : Fin nr → W) (MatchOf : Fin nr → (Q → A) → (W → A) → Prop) (setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : (Q → A) → (W → A) → Q → A) (IsMaxEl : (Q → A) → Prop) (exitPh : P) (i : ElemSite nr) (ρ : ElemSh nr i) : ∃ (p : ElemPh nr), (elemRule one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ).srcPh = emb p ∧ elemOwn p = i

Every rule of an element loop fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.elemSep {A Q W P : Type} {nr : ℕ} (one : A) (wk rg : W) {emb : ElemPh nr → P} (rdTrack : Fin nr → W) (MatchOf : Fin nr → (Q → A) → (W → A) → Prop) (setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : (Q → A) → (W → A) → Q → A) (IsMaxEl : (Q → A) → Prop) (exitPh : P) (hemb : Function.Injective emb) (i : ElemSite nr) (ρ ρ' : ElemSh nr i) (f : Q → A) (g : W → A) : (elemRule one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ).guard f g → (elemRule one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ').guard f g → (elemRule one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ).srcPh = (elemRule one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ').srcPh → ρ = ρ'

An element loop separates in-shape.