One-cell writes, and tests the tracks can decide

Two corrections to the pass interface, found by trying to discharge it.

A single-cell write is a step, not a pass. Prog.reaches_write asks for rules writing m' u at every pair of a symbol and a cell, which only a cell-independent m' can supply – a rule computes its written symbol from the tracks it reads, and at a decoupled pair the tracks say nothing about the cell. Writing one named bit therefore goes: navigate to the cell (DescriptiveComplexity.Draw.Prog.reaches_toCell), then one step (DescriptiveComplexity.Draw.Prog.step_writeCell and its rightward twin): the walked track changes at that cell and nowhere else, which is the coherence condition DescriptiveComplexity.Draw.Prog.trackTape_coh discharges. DescriptiveComplexity.Draw.Prog.passTracks_update_cell is the equation the rule's written symbol is checked against. (A single-cell read needs nothing new at all: it is DescriptiveComplexity.Draw.Prog.step_move or its twin with an unchanged background, the phase branching on the digit the rule reads.)

A file test must be decided by the tracks. Prog.reaches_test takes its question as a predicate of the cell, quantified independently of the symbol, so a deterministic table cannot serve both its pass and its fail hypotheses. DescriptiveComplexity.Draw.Prog.reaches_fileTestG restates it with the question a predicate TestG of the tracks, tied to the cell-level question by one compatibility hypothesis – which is how the machine actually asks it: MIRROR = TARGET is one slot against another, a well-shapedness check is the name marks, and so on.

What indexes the register file is a parameter throughout, as it is from DescriptiveComplexity.IxFile upwards: a program on a clock cannot give every element of the universe a register, and none of these passes care which does. A track is a predicate on the index and an address is a predicate on the universe; at the file a space-bounded program uses the two are the same type, which is why the diagonal reads as it does.

Updating a track at one cell

theorem DescriptiveComplexity.Draw.Prog.passTracks_update_cell {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {I : Type} {ile : I → I → Prop} {PR : Prog A R P Q W K dd} (F : IxFile (Univ A R P K dd) I ile) (hix : IsLinOrd ile) {t : W} {rest : (Univ A R P K dd → Prop) → W → A} (m : I → Prop) {b : Prop} (u : I) : PR.passTracksAt F.cell t rest (fun (v : I) => v = u ∧ b ∨ v ≠ u ∧ m v) (F.cell u) = Function.update (PR.passTracksAt F.cell t rest m (F.cell u)) t (bitVal PR.zero PR.one b)

The tracks at a cell whose walked track was updated there: the update of the tracks. This is the equation a writing rule's symbol is checked against.

theorem DescriptiveComplexity.Draw.Prog.step_writeCell {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] {I : Type} {ile : I → I → Prop} {PR : Prog A R P Q W K dd} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {u : I} {v' : Univ A R P K dd → Prop} (hi : WMIncr WMLe v' (F.cell u)) {t : W} {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {b : Prop} {p p' : P} {f f' : Q → A} (hrule : PR.HasLeft p f (PR.passTracksAt F.cell t rest m (F.cell u)) p' f' (Function.update (PR.passTracksAt F.cell t rest m (F.cell u)) t (bitVal PR.zero PR.one b))) : (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl (F.cell u), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p' f'), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell t rest fun (v : I) => v = u ∧ b ∨ v ≠ u ∧ m v) (PR.syElt PR.blank) }

One step writing the walked track at a register cell, moving left: the program stands on the cell, one rule rewrites the track's digit there – to b, whatever it read – and the head steps to the predecessor. The rest of the track and every other track ride along.

A file test the tracks decide

theorem DescriptiveComplexity.Draw.Prog.reaches_fileTestG {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] {I : Type} [Finite I] {ile : I → I → Prop} {PR : Prog A R P Q W K dd} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {Test : I → Prop} {TestG : (W → A) → Prop} {m : I → Prop} {t rg : W} (hne : t ≠ rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrest : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hcompat : ∀ (u : I), TestG (PR.passTracksAt F.cell t rest m (F.cell u)) ↔ Test u) {py pn : P} {f : Q → A} (hpass : ∀ (g : W → A), TestG g → g rg = PR.one → PR.HasLeft py f g py f g) (hfail : ∀ (g : W → A), ¬TestG g → g rg = PR.one → PR.HasLeft py f g pn f g) (hheld : ∀ (g : W → A), g rg = PR.one → PR.HasLeft pn f g pn f g) (hwalkY : ∀ (r : Univ A R P K dd → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → PR.HasLeft py f (PR.passTracksAt F.cell t rest m r) py f (PR.passTracksAt F.cell t rest m r)) (hwalkN : ∀ (r : Univ A R P K dd → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → PR.HasLeft pn f (PR.passTracksAt F.cell t rest m r) pn f (PR.passTracksAt F.cell t rest m r)) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (q : Univ A R P K dd → Prop), WMIncr WMLe q (F.cell bot) ∧ Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt py f), head := Sum.inl (F.cell top), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (accStateAfter ile Test (PR.stElt py f) (PR.stElt pn f) bot), head := Sum.inl q, tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }

A program tests its register file by a question of the tracks, the budget forgotten.

Whole-track writes the tracks can decide

The two whole-track writes the program needs – clearing a register and copying one register into another – have their written value computable from the symbol under the head (a constant, or another slot of the same cell), which is exactly what a deterministic rule can do. They are DescriptiveComplexity.reaches_fileWrite with the coupling supplied.

theorem DescriptiveComplexity.Draw.Prog.reaches_fileMapTrack {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] {I : Type} [Finite I] {ile : I → I → Prop} {PR : Prog A R P Q W K dd} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {t rg : W} (hne : t ≠ rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrest : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) {Fb : (W → A) → Prop} (hFb : ∀ (g g' : W → A), (∀ (s : W), s ≠ t → g s = g' s) → (Fb g ↔ Fb g')) {m : I → Prop} {p : P} {f : Q → A} (hput : ∀ (g : W → A), g rg = PR.one → PR.HasLeft p f g p f (Function.update g t (bitVal PR.zero PR.one (Fb g)))) (hwalk : ∀ (k : I → Prop) (r : Univ A R P K dd → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → PR.HasLeft p f (PR.passTracksAt F.cell t rest k r) p f (PR.passTracksAt F.cell t rest k r)) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (q : Univ A R P K dd → Prop), WMIncr WMLe q (F.cell bot) ∧ Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl (F.cell top), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl q, tape := wideTape (PR.trackTapeAt F.cell t rest fun (u : I) => Fb (PR.passTracksAt F.cell t rest m (F.cell u))) (PR.syElt PR.blank) }

Rewriting a track by a function of the other tracks, the budget forgotten.