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

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.

The scans

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.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.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.