Scanning to a cell recognized by its tracks

DescriptiveComplexity.Problems.Wide.DrawPass navigates to cells marked by a single slot – the two ends of the register file, the working-cell marker. The atom subroutines of the EXPSPACE program navigate differently: they scan for the register cell whose name slots – the mark a canonically padded cell carries its own coordinates in – match a tuple the machine holds in its control. That stopping condition reads several slots at once, so the scans are restated here with an arbitrary guard on the tracks:

• DescriptiveComplexity.Draw.Prog.reaches_scanStop / reaches_scanStopBack – scan to the first cell whose tracks satisfy the guard, learning on arrival that no cell passed did;
• DescriptiveComplexity.Draw.Prog.reaches_toCell / reaches_toCellBack – the same when the caller knows which cell that is, because the guard identifies it uniquely: arrival at the named cell exactly.

As everywhere in the pass layer, the caller supplies rules (Prog.HasRight / Prog.HasLeft families), the symbols are computed for it, and the tape is the Prog.trackTapeAt presentation, so a program never mentions FirstOrder.Language.wide.

theorem DescriptiveComplexity.Draw.Prog.reaches_scanStop {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {rest : (Univ A R P K dd → Prop) → W → A} {StopG : (W → A) → Prop} {p : P} {f : Q → A} {m : I → Prop} (hgo : ∀ (g : W → A), ¬StopG g → PR.HasRight p f g p f g) {s : Univ A R P K dd → Prop} (hex : ∃ (r : Univ A R P K dd → Prop), StopG (PR.passTracksAt cell t rest m r) ∧ WMSetLe WMLe s r) : ∃ (r : Univ A R P K dd → Prop), StopG (PR.passTracksAt cell t rest m r) ∧ WMSetLe WMLe s r ∧ (∀ (r' : Univ A R P K dd → Prop), WMSetLe WMLe s r' → WMSetLt WMLe r' r → ¬StopG (PR.passTracksAt cell t rest m r')) ∧ Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl r, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

Scanning right to the first cell whose tracks satisfy a guard, the budget forgotten.

theorem DescriptiveComplexity.Draw.Prog.reaches_toCell {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {rest : (Univ A R P K dd → Prop) → W → A} {StopG : (W → A) → Prop} {p : P} {f : Q → A} {m : I → Prop} (hgo : ∀ (g : W → A), ¬StopG g → PR.HasRight p f g p f g) {s u : Univ A R P K dd → Prop} (hstop : StopG (PR.passTracksAt cell t rest m u)) (hle : WMSetLe WMLe s u) (huniq : ∀ (r : Univ A R P K dd → Prop), WMSetLe WMLe s r → StopG (PR.passTracksAt cell t rest m r) → r = u) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl u, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

Scanning right to a cell the guard identifies uniquely, the budget forgotten.

theorem DescriptiveComplexity.Draw.Prog.reaches_toCellBackC {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {rest : (Univ A R P K dd → Prop) → W → A} {StopG : (W → A) → Prop} {p : P} {f : Q → A} {m : I → Prop} {s u : Univ A R P K dd → Prop} (hgo : ∀ (r : Univ A R P K dd → Prop), WMSetLe WMLe r s → ¬StopG (PR.passTracksAt cell t rest m r) → PR.HasLeft p f (PR.passTracksAt cell t rest m r) p f (PR.passTracksAt cell t rest m r)) (hstop : StopG (PR.passTracksAt cell t rest m u)) (hle : WMSetLe WMLe u s) (huniq : ∀ (r : Univ A R P K dd → Prop), WMSetLe WMLe r s → StopG (PR.passTracksAt cell t rest m r) → r = u) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl u, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

Scanning right to a cell the guard identifies uniquely, the budget forgotten.

Re-presenting the tape between passes

A register pass walks one track and carries the rest of the tape as its background. Two consecutive passes walk different tracks, so the after-tape of one has to be read as the before-tape of the other: the walked track moves into the background and a background slot becomes the walked track. That is one equality of presentations, provable once – the only condition being that the slot about to be walked satisfies the register discipline, i.e., is the DescriptiveComplexity.bitAtOf of some track (set nowhere off the register file).