The two ends of a program's run, at the pass-layer presentation

DescriptiveComplexity.Draw.Table.isInit and DescriptiveComplexity.Draw.Table.acceptsSpace state the two ends of a run at an arbitrary tape function; a program's phases are all stated at the DescriptiveComplexity.Draw.Prog.trackTapeAt presentation. This file joins them.

DescriptiveComplexity.Draw.Prog.initBack is the background at time zero – the mark of the cell's element on the register file, the blank everywhere else – and DescriptiveComplexity.Draw.Prog.trackTape_initBack says the initial tape is the presentation walking any track whose mark and blank digits are clear, with the empty track: which is why the all-blank start needs no initialization sweep. On top of it, DescriptiveComplexity.Draw.Prog.isInit_prog is the initial configuration a program's first phase starts from, and DescriptiveComplexity.Draw.Prog.acceptsSpace_prog / DescriptiveComplexity.Draw.Prog.dwideAcceptSpace_prog are what a finished run delivers – for the latter, together with the separation argument (DescriptiveComplexity.Draw.Prog.sep_of), the two promises of DescriptiveComplexity.DWideAcceptSpace.

The background at time zero

noncomputable def DescriptiveComplexity.Draw.Prog.initBack {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: the mark of the cell's element on the register file, the blank everywhere else.

Equations

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

theorem DescriptiveComplexity.Draw.Prog.initBack_wmSeg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [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) (x : Univ A R P K dd) : PR.initBack (wmSeg x) = PR.mark x

On a register cell the background is the mark.

theorem DescriptiveComplexity.Draw.Prog.initBack_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), r ≠ wmSeg x) : PR.initBack r = PR.blank

Off the register file the background is the blank.

theorem DescriptiveComplexity.Draw.Prog.trackTape_initBack {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 wmSeg t₀ PR.initBack fun (x : Univ A R P K dd) => False) = fun (r : Univ A R P K dd → Prop) => PR.syElt (PR.initBack r)

The initial tape is the pass-layer presentation, walking any track whose mark and blank digits are clear, with the empty track: the all-blank start needs no initialization sweep.

theorem DescriptiveComplexity.Draw.Prog.trackTapeAt_initBack {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} {J : Type} (cell : J → Univ A R P K dd → Prop) {t₀ : W} (hmk : ∀ (x : Univ A R P K dd), PR.mark x t₀ = PR.zero) (hb : PR.blank t₀ = PR.zero) : (PR.trackTapeAt cell t₀ PR.initBack fun (x : J) => False) = fun (r : Univ A R P K dd → Prop) => PR.syElt (PR.initBack r)

The initial tape does not depend on which file presents it: the same statement at an arbitrary file. Nothing of the file is read – the walked track is empty, so the only cell-dependent part of the presentation is a bit that is False wherever the head is – and that is what lets a clocked program, whose file is not the channel's and does not exist yet at time zero, start its opening in the presentation the rest of its run is stated in.

theorem DescriptiveComplexity.Draw.Prog.initBack_of_mark_blank {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} (hmk : ∀ (x : Univ A R P K dd), PR.mark x = PR.blank) (r : Univ A R P K dd → Prop) : PR.initBack r = PR.blank

A program may decline the input channel's marks. What a marked cell carries is the program's own field, so a program that wants a blank tape at time zero takes mark to be the blank, and then the background at time zero is the blank everywhere – no cell of the channel's ruler is distinguishable from any other.

That is what a clocked program does. It cannot afford the ruler (DescriptiveComplexity.Problems.Wide.Marks), it builds its own file low on the tape, and if the channel's marks were still there it would have to say at every step that it has not mistaken one for a register of its own. Declining them removes the question.

The two ends of a run

theorem DescriptiveComplexity.Draw.Prog.isInit_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) (hall : ∀ (x : Univ A R P K dd), PR.marked x) {t₀ : W} (hmk : ∀ (x : Univ A R P K dd), PR.mark x t₀ = PR.zero) (hb : PR.blank t₀ = PR.zero) : (wideData (Univ A R P K dd)).IsInit { 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 wmSeg t₀ PR.initBack fun (x : Univ A R P K dd) => False) (PR.syElt PR.blank) }

The initial configuration of a program: its start phase and pointer, the head on the empty address, the tape presenting the marks with any clear track walked.

theorem DescriptiveComplexity.Draw.Prog.accept_table {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] {PR : Prog A R P Q W K dd} {p : P} {f : Q → A} (h : PR.accept p f) : PR.table.accept p (stPl PR.zero f)

A program's accepting states are the table's.

theorem DescriptiveComplexity.Draw.Prog.accept_of_isAcc {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] {PR : Prog A R P Q W K dd} {p : P} {f : Q → A} (h : PR.table.IsAcc (PR.stElt p f)) : PR.accept p f

And conversely: a state the table accepts is one the program accepts. The pointer is recovered from the payload by the same equation, which is what a backward reading needs – it is handed an accepting configuration and has to say what the program decided.

theorem DescriptiveComplexity.Draw.Prog.acceptsSpace_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) (hall : ∀ (x : Univ A R P K dd), PR.marked x) {t₀ : W} (hmk : ∀ (x : Univ A R P K dd), PR.mark x t₀ = PR.zero) (hb : PR.blank t₀ = PR.zero) {cfg : Config (WPoint (Univ A R P K dd))} (hreach : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { 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 wmSeg t₀ PR.initBack fun (x : Univ A R P K dd) => False) (PR.syElt PR.blank) } cfg) {p : P} {fq : Q → A} (hstate : cfg.state = Sum.inr (PR.stElt p fq)) (ha : PR.accept p fq) : (wideData (Univ A R P K dd)).AcceptsSpace

A program's run accepts in bounded space: start as DescriptiveComplexity.Draw.Prog.isInit_prog says, roam, and end in a phase and pointer the program accepts.

theorem DescriptiveComplexity.Draw.Prog.accepts_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) (hall : ∀ (x : Univ A R P K dd), PR.marked x) {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 wmSeg t₀ PR.initBack 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) : (wideData (Univ A R P K dd)).Accepts

A program's run accepts on the clock: start as DescriptiveComplexity.Draw.Prog.isInit_prog says, run for fewer steps than there are addresses, and end in a phase and pointer the program accepts.

theorem DescriptiveComplexity.Draw.Prog.wideAccept_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) (hall : ∀ (x : Univ A R P K dd), PR.marked x) {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 wmSeg t₀ PR.initBack 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) : WideAccept.Holds (Univ A R P K dd)

A program's run makes its instance a yes-instance of DescriptiveComplexity.WideAccept: well-formedness, which is free, and an accepting run within the clock. A program that guesses produces this and not DescriptiveComplexity.Draw.Prog.dwideAcceptSpace_prog, which asks for determinism.

theorem DescriptiveComplexity.Draw.Prog.dwideAcceptSpace_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) (hall : ∀ (x : Univ A R P K dd), PR.marked x) (hsep : ∀ (r r' : R) (f : Q → A) (g : W → A), (PR.rules r).guard f g → (PR.rules r').guard f g → (PR.rules r).srcPh = (PR.rules r').srcPh → r = r') (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) {cfg : Config (WPoint (Univ A R P K dd))} (hreach : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { 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 wmSeg t₀ PR.initBack fun (x : Univ A R P K dd) => False) (PR.syElt PR.blank) } cfg) {p : P} {fq : Q → A} (hstate : cfg.state = Sum.inr (PR.stElt p fq)) (ha : PR.accept p fq) : DWideAcceptSpace.Holds (Univ A R P K dd)

A program's run makes its instance a yes-instance of DescriptiveComplexity.DWideAcceptSpace: the two promises – well-formedness for free, determinism from the separation argument – and the accepting run.