Starting a run at the register channel

The two machines an instance describes – DescriptiveComplexity.wideData and DescriptiveComplexity.wideRegData – differ in one field, the channel, and it is read nowhere but in the initial tape: a step reads the transitions, the order and the positions and nothing else. So every run lemma of the library transfers by definition (wideRegData_step, wideRegData_reachesIn), and what has to be redone is the pair of statements at the two ends of a run.

They are the segment channel's own with two changes: the cell of x is wmRegSeg x, and only the elements that carry input have one. Where the segment channel says “every cell holds its element's symbol, every other address is blank”, the register channel says the same of the elements it writes for, and an address that is nobody's cell is blank as before.

theorem DescriptiveComplexity.wideRegData_step {A : Type} [FirstOrder.Language.wide.Structure A] (c c' : Config (WPoint A)) : (wideRegData A).Step c c' ↔ (wideData A).Step c c'

The two machines take the same steps: a step reads the transitions, the order and the positions, and the channel is none of those.

theorem DescriptiveComplexity.wideRegData_stepsIn {A : Type} [FirstOrder.Language.wide.Structure A] (n : ℕ) (c c' : Config (WPoint A)) : (wideRegData A).StepsIn n c c' ↔ (wideData A).StepsIn n c c'

And so they take the same runs.

theorem DescriptiveComplexity.wideRegData_reachesIn {A : Type} [FirstOrder.Language.wide.Structure A] (n : ℕ) (c c' : Config (WPoint A)) : (wideRegData A).ReachesIn n c c' ↔ (wideData A).ReachesIn n c c'

And the same bounded runs.

theorem DescriptiveComplexity.initTape_wmRegSeg {A : Type} [FirstOrder.Language.wide.Structure A] {x a : A} (hinp : WMInp x a) : (wideRegData A).InitTape (Sum.inl (wmRegSeg x)) (Sum.inr a)

A register cell starts holding its element's symbol.

theorem DescriptiveComplexity.initTape_of_not_wmRegSeg {A : Type} [FirstOrder.Language.wide.Structure A] {s : A → Prop} (hno : ∀ (x y : A), WMRegSeg s x → ¬WMInp x y) (a : WPoint A) : (wideRegData A).InitTape (Sum.inl s) a ↔ (wideRegData A).Blank a

Every other address starts blank: one that is no writing element's cell.

theorem DescriptiveComplexity.initTape_of_marksReg {A : Type} [FirstOrder.Language.wide.Structure A] {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMHasInp x → WMInp x (sym x)) {tp : WPoint A → WPoint A} (hmark : ∀ (x : A), WMHasInp x → tp (Sum.inl (wmRegSeg x)) = Sum.inr (sym x)) (hrest : ∀ (p : WPoint A), (∀ (x : A), WMHasInp x → p ≠ Sum.inl (wmRegSeg x)) → tp p = Sum.inr b) (p : WPoint A) : (wideRegData A).InitTape p (tp p)

The initial tape at the register channel: the symbol of x at the cell of x for every element the channel writes for, the blank at every address that is no such element's cell.

theorem DescriptiveComplexity.wideRegData_wellFormed_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] : (wideRegData A).WellFormed ↔ WideWF A

The promise of the register-channel machine is the same promise about the instance: a linear order, a functional input and a unique blank. The channel enters only through the functionality of the input, and there two elements with the same cell that both carry input are equal.

theorem DescriptiveComplexity.isInit_wideReg_marks {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMHasInp x → WMInp x (sym x)) {tp : WPoint A → WPoint A} (hmark : ∀ (x : A), WMHasInp x → tp (Sum.inl (wmRegSeg x)) = Sum.inr (sym x)) (hrest : ∀ (p : WPoint A), (∀ (x : A), WMHasInp x → p ≠ Sum.inl (wmRegSeg x)) → tp p = Sum.inr b) {q₀ : A} (hq : WMStart q₀) : (wideRegData A).IsInit { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := tp }

The initial configuration at the register channel: a start state, the head on the empty address – which is no register's cell, a register's cell holding its own element – and the marked tape.

theorem DescriptiveComplexity.isInit_wideRegTape {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMHasInp x → WMInp x (sym x)) {f : (A → Prop) → A} (hmark : ∀ (x : A), WMHasInp x → f (wmRegSeg x) = sym x) (hrest : ∀ (s : A → Prop), (∀ (x : A), WMHasInp x → s ≠ wmRegSeg x) → f s = b) {q₀ : A} (hq : WMStart q₀) : (wideRegData A).IsInit { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := wideTape f b }

The initial configuration of a program at the register channel, its tape given as a function of the addresses.

theorem DescriptiveComplexity.accepts_of_wideRegTape {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMHasInp x → WMInp x (sym x)) {f : (A → Prop) → A} (hmark : ∀ (x : A), WMHasInp x → f (wmRegSeg x) = sym x) (hrest : ∀ (s : A → Prop), (∀ (x : A), WMHasInp x → s ≠ wmRegSeg x) → f s = b) {q₀ : A} (hq : WMStart q₀) {n : ℕ} {c : Config (WPoint A)} (hreach : (wideData A).ReachesIn n { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := wideTape f b } c) (hlt : n < Nat.card { p : WPoint A // (wideData A).Posn p }) {qa : A} (hstate : c.state = Sum.inr qa) (hacc : WMAcc qa) : (wideRegData A).Accepts

A program at the register channel accepts on its clock: it starts as isInit_wideRegTape says, runs for fewer steps than there are addresses, and ends in an accepting state.

theorem DescriptiveComplexity.accepts_of_wideRegTape_lt_two_pow {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMHasInp x → WMInp x (sym x)) {f : (A → Prop) → A} (hmark : ∀ (x : A), WMHasInp x → f (wmRegSeg x) = sym x) (hrest : ∀ (s : A → Prop), (∀ (x : A), WMHasInp x → s ≠ wmRegSeg x) → f s = b) {q₀ : A} (hq : WMStart q₀) {n : ℕ} {c : Config (WPoint A)} (hreach : (wideData A).ReachesIn n { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := wideTape f b } c) (hlt : n < 2 ^ Nat.card A) {qa : A} (hstate : c.state = Sum.inr qa) (hacc : WMAcc qa) : (wideRegData A).Accepts

The same, with the budget compared against 2 ^ n.