A program's tape is a function of the address

DescriptiveComplexity.TMData takes the tape to be a function on the whole universe of the machine, WPoint A → WPoint A. A program's tape is never that general: the control points are not cells, so they keep the blank they started with for ever, and every real cell holds a symbol – an element of the instance. So a program's tape is a function

f : (A → Prop) → A, a symbol for each address,

and DescriptiveComplexity.wideTape is the machine's tape it presents. Working in that form is worth a file of its own because it removes the same three obligations from every step of every phase:

obligation	in the general form	here
the symbol under the head	tp (Sum.inl s) = Sum.inr a	f s, no equation
the frame condition	∀ p : WPoint A, p ≠ Sum.inl s → …	∀ r, r ≠ s → f' r = f r
the control points	a case of every proof	discharged once

DescriptiveComplexity.step_wideTape_right and its leftward twin are the step in that form, DescriptiveComplexity.reaches_scan_tape and DescriptiveComplexity.reaches_scanBack_tape are the scans, and DescriptiveComplexity.isInit_wideTape is the initial configuration of a program that has marked its register file (DescriptiveComplexity.Problems.Wide.Marks).

Note what is not here: Function.update. An address is a set, so equality of addresses is not decidable, and a program's tapes come from formulas anyway. A write is described by naming the new tape function and saying where it agrees with the old one, which is what hagree is in every statement below.

The tape of a program

def DescriptiveComplexity.wideTape {A : Type} (f : (A → Prop) → A) (b : A) : WPoint A → WPoint A

The tape a symbol assignment presents: the symbol of each address, and the blank on the control points, which are not cells and are never written.

Equations

• DescriptiveComplexity.wideTape f b (Sum.inl s) = Sum.inr (f s)
• DescriptiveComplexity.wideTape f b (Sum.inr val) = Sum.inr b

@[simp]

theorem DescriptiveComplexity.wideTape_addr {A : Type} (f : (A → Prop) → A) (b : A) (s : A → Prop) : wideTape f b (Sum.inl s) = Sum.inr (f s)

@[simp]

theorem DescriptiveComplexity.wideTape_ctrl {A : Type} (f : (A → Prop) → A) (b x : A) : wideTape f b (Sum.inr x) = Sum.inr b

theorem DescriptiveComplexity.wideTape_frame {A : Type} {f f' : (A → Prop) → A} {s : A → Prop} (hagree : ∀ (r : A → Prop), r ≠ s → f' r = f r) (b : A) (p : WPoint A) : p ≠ Sum.inl s → wideTape f' b p = wideTape f b p

The frame condition, in the program's form: two symbol assignments agreeing off one address present tapes agreeing off that cell. The control points are where the general statement needs a case and this one does not.

One step

theorem DescriptiveComplexity.step_wideTape_right {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {s t : A → Prop} (hi : WMIncr WMLe s t) {τ q q' b : A} {f f' : (A → Prop) → A} (htr : WMTr τ) (hsrc : WMSrc τ q) (hread : WMRead τ (f s)) (hdst : WMDst τ q') (hwrite : WMWrite τ (f' s)) (hright : WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ s → f' r = f r) : (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q', head := Sum.inl t, tape := wideTape f' b }

A right-moving step of a program. The head is on s, the transition τ applies to the state and to the symbol f s written there, and the new assignment f' differs from f at s only.

theorem DescriptiveComplexity.step_wideTape_left {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {s t : A → Prop} (hi : WMIncr WMLe t s) {τ q q' b : A} {f f' : (A → Prop) → A} (htr : WMTr τ) (hsrc : WMSrc τ q) (hread : WMRead τ (f s)) (hdst : WMDst τ q') (hwrite : WMWrite τ (f' s)) (hright : ¬WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ s → f' r = f r) : (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q', head := Sum.inl t, tape := wideTape f' b }

A left-moving step of a program, the head stepping down to the address whose increment it is on.

The scans

theorem DescriptiveComplexity.reachesIn_scan_tape {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {Stop : (A → Prop) → Prop} {s : A → Prop} (hex : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe s t) (hstep : ∀ (r : A → Prop), WMSetLe WMLe s r → (∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe r t) → ¬Stop r → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ WMRight τ) : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe s t ∧ (∀ (r : A → Prop), WMSetLe WMLe s r → WMSetLt WMLe r t → ¬Stop r) ∧ (wideData A).ReachesIn (wideRank t - wideRank s) { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl t, tape := wideTape f b }

A program scans right to the first cell that stops it. The scanning transition is asked for at the symbol the assignment gives, so no symbol is quantified: a caller supplies one transition per symbol it does not stop at.

theorem DescriptiveComplexity.reaches_scan_tape {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {Stop : (A → Prop) → Prop} {s : A → Prop} (hex : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe s t) (hstep : ∀ (r : A → Prop), WMSetLe WMLe s r → (∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe r t) → ¬Stop r → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ WMRight τ) : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe s t ∧ (∀ (r : A → Prop), WMSetLe WMLe s r → WMSetLt WMLe r t → ¬Stop r) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl t, tape := wideTape f b }

A program scans right to the first cell that stops it, the budget forgotten.

theorem DescriptiveComplexity.reachesIn_scanBack_tape {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {Stop : (A → Prop) → Prop} {s : A → Prop} (hex : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t s) (hstep : ∀ (r : A → Prop), WMSetLe WMLe r s → (∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t r) → ¬Stop r → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t s ∧ (∀ (r : A → Prop), WMSetLt WMLe t r → WMSetLe WMLe r s → ¬Stop r) ∧ (wideData A).ReachesIn (wideRank s - wideRank t) { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl t, tape := wideTape f b }

A program scans left to the first cell that stops it, the same reading downwards.

theorem DescriptiveComplexity.reaches_scanBack_tape {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {Stop : (A → Prop) → Prop} {s : A → Prop} (hex : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t s) (hstep : ∀ (r : A → Prop), WMSetLe WMLe r s → (∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t r) → ¬Stop r → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t s ∧ (∀ (r : A → Prop), WMSetLt WMLe t r → WMSetLe WMLe r s → ¬Stop r) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl t, tape := wideTape f b }

A program scans left to the first cell that stops it, the budget forgotten.

Writing a track across the tape

The phase a program spends laying something out: sweep up, writing one symbol per address as it goes. The tape it holds part-way through is written below the head and untouched at and above it, which is the address-scale twin of DescriptiveComplexity.Problems.Wide.Mirror's mirror during a register walk.

The new symbols are a parameter, so the same statement serves a deterministic layout phase – build the register file, plant a marker – and a guessing one: if the transition offered at each cell may write either of two symbols, the run below exists for every choice, and the choice is the certificate.

noncomputable def DescriptiveComplexity.midTape {A : Type} [FirstOrder.Language.wide.Structure A] {B : Type} (f₀ f₁ : (A → Prop) → B) (s : A → Prop) : (A → Prop) → B

A family in mid-installation: the new value at the addresses the head has passed, the old one where it stands and above. The value type is arbitrary – a sweep installs symbols this way, and a program installs whole backgrounds.

Equations

• DescriptiveComplexity.midTape f₀ f₁ s r = if DescriptiveComplexity.WMSetLt DescriptiveComplexity.WMLe r s then f₁ r else f₀ r

theorem DescriptiveComplexity.midTape_self {A : Type} [FirstOrder.Language.wide.Structure A] {B : Type} (f₀ f₁ : (A → Prop) → B) (s : A → Prop) : midTape f₀ f₁ s s = f₀ s

The cell the head stands on still holds its old symbol.

theorem DescriptiveComplexity.midTape_incr {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {B : Type} (h : IsLinOrd WMLe) (f₀ f₁ : (A → Prop) → B) {s t : A → Prop} (hi : WMIncr WMLe s t) : midTape f₀ f₁ t s = f₁ s

One increment later, the cell holds its new symbol.

theorem DescriptiveComplexity.midTape_agree {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {B : Type} (h : IsLinOrd WMLe) (f₀ f₁ : (A → Prop) → B) {s t : A → Prop} (hi : WMIncr WMLe s t) (r : A → Prop) : r ≠ s → midTape f₀ f₁ t r = midTape f₀ f₁ s r

A step of the sweep changes one cell: off the cell the head is on, the tape before and after the write agree.

theorem DescriptiveComplexity.reachesIn_of_wideWriteSt {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} {st f₀ f₁ : (A → Prop) → A} {s₀ s₁ : A → Prop} (hle : WMSetLe WMLe s₀ s₁) (hstep : ∀ (r r' : A → Prop), WMIncr WMLe r r' → WMSetLe WMLe s₀ r → WMSetLe WMLe r' s₁ → ∃ (τ : A), WMTr τ ∧ WMSrc τ (st r) ∧ WMRead τ (f₀ r) ∧ WMDst τ (st r') ∧ WMWrite τ (f₁ r) ∧ WMRight τ) : (wideData A).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (st s₀), head := Sum.inl s₀, tape := wideTape (midTape f₀ f₁ s₀) b } { state := Sum.inr (st s₁), head := Sum.inl s₁, tape := wideTape (midTape f₀ f₁ s₁) b }

A writing sweep carrying a state. At every cell of a stretch the machine writes the new symbol and moves right, and its state advances with the head: at the cell r it is st r, and the step to r's successor leaves it in that successor's state. It arrives at the top of the stretch with the tape rewritten below it and untouched above.

A state that varies is what lets a sweep write something different in every cell: a rule computes its symbol from what it reads and from the state, and the tape it reads is blank everywhere, so a phase laying down a pattern has to hold the pattern's index in the state. That is how a program builds its own register file – the state holds the element whose register the head is on, and the order successor moves it along.

theorem DescriptiveComplexity.reachesIn_of_wideWrite {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q b : A} {f₀ f₁ : (A → Prop) → A} {s₀ s₁ : A → Prop} (hle : WMSetLe WMLe s₀ s₁) (hstep : ∀ (r : A → Prop), WMSetLe WMLe s₀ r → WMSetLt WMLe r s₁ → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f₀ r) ∧ WMDst τ q ∧ WMWrite τ (f₁ r) ∧ WMRight τ) : (wideData A).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr q, head := Sum.inl s₀, tape := wideTape (midTape f₀ f₁ s₀) b } { state := Sum.inr q, head := Sum.inl s₁, tape := wideTape (midTape f₀ f₁ s₁) b }

A writing sweep. The previous statement in a fixed state.

The new assignment f₁ is universally quantified, so a guessing phase is this statement read at the guess: whatever the certificate, the run that writes it exists.

The two ends of a run

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

The initial configuration of a program: a start state, the head on the empty address, and the tape whose symbol at the cell of x is the name of x and whose symbol everywhere else is the blank.

theorem DescriptiveComplexity.acceptsSpace_of_wideTape {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMInp x (sym x)) {f : (A → Prop) → A} (hmark : ∀ (x : A), f (wmSeg x) = sym x) (hrest : ∀ (s : A → Prop), (∀ (x : A), s ≠ wmSeg x) → f s = b) {q₀ : A} (hq : WMStart q₀) {c : Config (WPoint A)} (hreach : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := wideTape f b } c) {qa : A} (hstate : c.state = Sum.inr qa) (hacc : WMAcc qa) : (wideData A).AcceptsSpace

A program accepts: it starts as DescriptiveComplexity.isInit_wideTape says, roams, and ends in an accepting state. This is the whole of DescriptiveComplexity.WideAcceptSpace for a program with a register file.

theorem DescriptiveComplexity.accepts_of_wideTape {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMInp x (sym x)) {f : (A → Prop) → A} (hmark : ∀ (x : A), f (wmSeg x) = sym x) (hrest : ∀ (s : A → Prop), (∀ (x : A), s ≠ wmSeg 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) : (wideData A).Accepts

A program on a clock accepts: the same run with its budget kept and compared once with the number of addresses.

theorem DescriptiveComplexity.accepts_of_wideTape_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), WMInp x (sym x)) {f : (A → Prop) → A} (hmark : ∀ (x : A), f (wmSeg x) = sym x) (hrest : ∀ (s : A → Prop), (∀ (x : A), s ≠ wmSeg 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) : (wideData A).Accepts

A program with a register file accepts on its clock, the budget compared against 2 ^ n.