A program's run at the register channel

DescriptiveComplexity.Draw.Prog.wideAccept_prog turns a program's run into a yes-instance of DescriptiveComplexity.WideAccept, whose channel writes for every element. This file is the same statement at the register channel, where a program writes for the elements it marks and the file it is handed has one register per such element.

The marking is what a program says about its own channel: Prog.marked is a field, fun _ => True by default, and the two ends of a run read it. At the segment channel the program marks everything and the file is the ruler; at the register channel it marks its argument elements and the file lies in the working region (DescriptiveComplexity.wideRank_wmRegSeg_lt).

theorem DescriptiveComplexity.Draw.Table.wmHasInp_iff_marked {A R P K : Type} {c dd : ℕ} {T : Table A R P K c dd} [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : T.Reads) (x : Univ A R P K dd) : WMHasInp x ↔ T.Marked x

The elements the channel writes for are the ones the table marks: the instance's input relation is the table's, and the table's holds at x exactly when x is marked.

theorem DescriptiveComplexity.Draw.Table.acceptsReg {A R P K : Type} {c dd : ℕ} {T : Table A R P K c dd} [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] (hR : T.Reads) {f : (Univ A R P K dd → Prop) → Univ A R P K dd} (hmark : ∀ (x : Univ A R P K dd), T.Marked x → f (wmRegSeg x) = symElt T.zero (T.markPl x)) (hrest : ∀ (s : Univ A R P K dd → Prop), (∀ (x : Univ A R P K dd), T.Marked x → s ≠ wmRegSeg x) → f s = symElt T.zero T.blankPl) {n : ℕ} {cfg : Config (WPoint (Univ A R P K dd))} (hreach : (wideData (Univ A R P K dd)).ReachesIn n { state := Sum.inr (stateElt T.zero T.startPh T.startPl), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape f (symElt T.zero T.blankPl) } cfg) (hlt : n < 2 ^ Nat.card (Univ A R P K dd)) {p : P} {w : Fin c → A} (hstate : cfg.state = Sum.inr (stateElt T.zero p w)) (ha : T.accept p w) : (wideRegData (Univ A R P K dd)).Accepts

The emitted machine accepts on the clock at the register channel: the reading of DescriptiveComplexity.Draw.Table.accepts whose marks sit on the file of the elements the table writes for.

theorem DescriptiveComplexity.Draw.Table.exists_reachesIn_of_acceptsReg {A R P K : Type} {c dd : ℕ} {T : Table A R P K c dd} [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] (hR : T.Reads) {f : (Univ A R P K dd → Prop) → Univ A R P K dd} (hmark : ∀ (x : Univ A R P K dd), T.Marked x → f (wmRegSeg x) = symElt T.zero (T.markPl x)) (hrest : ∀ (s : Univ A R P K dd → Prop), (∀ (x : Univ A R P K dd), T.Marked x → s ≠ wmRegSeg x) → f s = symElt T.zero T.blankPl) (hwf : (wideRegData (Univ A R P K dd)).WellFormed) (hacc : (wideRegData (Univ A R P K dd)).Accepts) : ∃ (n : ℕ) (cfg : Config (WPoint (Univ A R P K dd))), n < Nat.card { p : WPoint (Univ A R P K dd) // (wideData (Univ A R P K dd)).Posn p } ∧ (wideData (Univ A R P K dd)).StepsIn n { state := Sum.inr (stateElt T.zero T.startPh T.startPl), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape f (symElt T.zero T.blankPl) } cfg ∧ (wideData (Univ A R P K dd)).Acc cfg.state

And backwards: a yes-instance's accepting run starts at the canonical initial configuration – the start state, the empty address, and the tape the channel wrote – because a well-formed machine with one start state has one initial configuration (TMData.isInit_unique). This is where a backward reading of an accepting run gets the run it walks.

noncomputable def DescriptiveComplexity.Draw.Prog.initBackReg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (PR : Prog A R P Q W K dd) : (Univ A R P K dd → Prop) → W → A

The background at time zero, at the register channel: the mark of the element whose cell it is, for the elements the program writes for, and the blank at every other address.

Equations

• PR.initBackReg r s = if h : ∃ (x : DescriptiveComplexity.Draw.Univ A R P K dd), PR.marked x ∧ r = DescriptiveComplexity.wmRegSeg x then PR.mark h.choose s else PR.blank s

theorem DescriptiveComplexity.Draw.Prog.initBackReg_wmRegSeg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype 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} (hlin : IsLinOrd WMLe) (hR : PR.table.Reads) {x : Univ A R P K dd} (hx : PR.marked x) : PR.initBackReg (wmRegSeg x) = PR.mark x

On a register cell the background is that register's mark: two marked elements with the same cell are equal (wmRegSeg_injOn).

theorem DescriptiveComplexity.Draw.Prog.initBackReg_of_not_reg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} {r : Univ A R P K dd → Prop} (hno : ∀ (x : Univ A R P K dd), PR.marked x → r ≠ wmRegSeg x) : PR.initBackReg r = PR.blank

Off the file the background is the blank.

theorem DescriptiveComplexity.Draw.Prog.trackTape_initBackReg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} {t₀ : W} (hmk : ∀ (x : Univ A R P K dd), PR.mark x t₀ = PR.zero) (hb : PR.blank t₀ = PR.zero) : (PR.trackTapeAt wmRegSeg t₀ PR.initBackReg fun (x : Univ A R P K dd) => False) = fun (r : Univ A R P K dd → Prop) => PR.syElt (PR.initBackReg r)

The initial tape is the pass-layer presentation, at the register channel: the walked track is empty, so nothing of the file is read but the cells themselves.

theorem DescriptiveComplexity.Draw.Prog.accepts_progReg {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} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t₀ : W} (hmk : ∀ (x : Univ A R P K dd), PR.mark x t₀ = PR.zero) (hb : PR.blank t₀ = PR.zero) {n : ℕ} {cfg : Config (WPoint (Univ A R P K dd))} (hreach : (wideData (Univ A R P K dd)).ReachesIn n { state := Sum.inr (PR.stElt PR.startPh PR.startSt), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt wmRegSeg t₀ PR.initBackReg fun (x : Univ A R P K dd) => False) (PR.syElt PR.blank) } cfg) (hlt : n < 2 ^ Nat.card (Univ A R P K dd)) {p : P} {fq : Q → A} (hstate : cfg.state = Sum.inr (PR.stElt p fq)) (ha : PR.accept p fq) : (wideRegData (Univ A R P K dd)).Accepts

A program's run accepts on the clock, at the register channel.

theorem DescriptiveComplexity.Draw.Prog.exists_stepsIn_of_wideRegAccept {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} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t₀ : W} (hmk : ∀ (x : Univ A R P K dd), PR.mark x t₀ = PR.zero) (hb : PR.blank t₀ = PR.zero) (hacc : WideRegAccept.Holds (Univ A R P K dd)) : ∃ (n : ℕ) (cfg : Config (WPoint (Univ A R P K dd))), (wideData (Univ A R P K dd)).StepsIn n { state := Sum.inr (PR.stElt PR.startPh PR.startSt), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt wmRegSeg t₀ PR.initBackReg fun (x : Univ A R P K dd) => False) (PR.syElt PR.blank) } cfg ∧ (wideData (Univ A R P K dd)).Acc cfg.state

And backwards, at a program: a yes-instance of DescriptiveComplexity.WideRegAccept gives a run of this program from the configuration it starts in – the state it starts in, the empty address, and the tape the channel wrote. The clock is dropped: a backward reading refutes acceptance by determinism, and for that the length of the run does not matter.

theorem DescriptiveComplexity.Draw.Prog.wideRegAccept_prog {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} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t₀ : W} (hmk : ∀ (x : Univ A R P K dd), PR.mark x t₀ = PR.zero) (hb : PR.blank t₀ = PR.zero) {n : ℕ} {cfg : Config (WPoint (Univ A R P K dd))} (hreach : (wideData (Univ A R P K dd)).ReachesIn n { state := Sum.inr (PR.stElt PR.startPh PR.startSt), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt wmRegSeg t₀ PR.initBackReg fun (x : Univ A R P K dd) => False) (PR.syElt PR.blank) } cfg) (hlt : n < 2 ^ Nat.card (Univ A R P K dd)) {p : P} {fq : Q → A} (hstate : cfg.state = Sum.inr (PR.stElt p fq)) (ha : PR.accept p fq) : WideRegAccept.Holds (Univ A R P K dd)

A program's run makes its instance a yes-instance of DescriptiveComplexity.WideRegAccept: the reading a clocked reduction into the register channel produces.