The tape of a machine playing a second-order game

The layout half of SO-GAME ≤ʳᶠᵒ[≤] ATMAcceptSpace: which tagged tuples the emitted machine calls positions, in what order they sit, and what a tape is.

The layout

  ⊢₀ ⊢₁ | region 0: one cell per atom | region 1: one cell per atom | ⊣

A cell is (region, relation variable i, ā) with ā a tuple of arity i elements of the instance, so the cells of one region are exactly the atoms of a block assignment and a region is a point of the second-order game – n^a bits, one tape's worth, which is the whole reason APSPACE = EXPTIME. The two regions hold the current position and the candidate; their roles swap at each move of the game, so nothing is ever copied.

The two left sentinels are there because DescriptiveComplexity.TMData.Step has no stay-put option: every step moves the head, so the phases that do not touch the tape have to bounce it somewhere harmless, and they bounce between these two. Two of them exist whatever |A| is, because a sentinel tag pins every coordinate to the minimum and so carries exactly one position. The right sentinel does the same service for a step that runs off the last cell.

A cell holds its own address

The symbol in the cell of the atom i ā of region r is not a bit but DescriptiveComplexity.valPt b r i ā: the bit together with the address of the cell. That is the one decision of the layout that is repaid several times over, and it is available only because a tape here is a function A → A into the emitted universe, so a symbol may carry a tuple.

The machine never has to know where its head is.

Without it, every walk would have to carry the head's address in its state and preserve the invariant the tracked address is the head's position – the single most expensive invariant of a tape-walking reduction. With it:

• a seek to the cell of a computed atom walks right and stops when the symbol it reads carries the target address, which is a first-order condition on the transition's own tuple;
• a sweep writing a guessed assignment into region r needs no phase per region: the transitions that guess are the ones whose read symbol has region r, and those that copy back are the ones whose read symbol has region !r, so the machine's own alphabet decides which fires;
• the sentinels carry DescriptiveComplexity.markPt, a symbol of their own, so a walk knows it has reached an end by reading it, and the initial tape is first-order definable and total – which is what DescriptiveComplexity.TMData.WellFormed demands of the input.

The order

A tag's DescriptiveComplexity.TapeTag.fam is what the order is designed around – the five position families above, then the symbols, with the control above all of them – and inside a family any fixed order will do, so the linear order on tags is (fam, an arbitrary tie-break) read lexicographically (DescriptiveComplexity.machTagOrder). No hand-built numbering of the constructors is needed, and none of the control's tags has to be numbered at all. On tuples the order is then DescriptiveComplexity.tagTupleLe, the tag first and the coordinates lexicographically, which DescriptiveComplexity.OrderedComposition already supplies and already proves linear.

The domain

The reduction is relativized, so a tag may pin the coordinates it does not use: DescriptiveComplexity.machDom says every coordinate from a tag's own arity on is a minimum (DescriptiveComplexity.Canon). That is what makes the cells of variable i correspond to the atoms of i one for one, rather than n^{dim - arity i} times over.

The tags of the tape

inductive DescriptiveComplexity.TapeTag (B : SOBlock) : Type

The tags of the tape: two left sentinels, one family of cells per region and relation variable, a right sentinel, the symbols carrying a bit and the address of their cell, and the sentinels' own symbol.

• left {B : SOBlock} (b : Bool) : TapeTag B

  A left sentinel; left false is the lowest position of all.

• cell {B : SOBlock} (r : Bool) (i : B.ι) : TapeTag B

  The cells of region r holding the relation variable i.

• right {B : SOBlock} : TapeTag B

  The right sentinel, the highest position.

• val {B : SOBlock} (b r : Bool) (i : B.ι) : TapeTag B

  The symbol of a cell: the bit b, and the address of the cell itself.

• mark {B : SOBlock} (b : Bool) : TapeTag B

  The symbol on the sentinels: mark false on the left pair, mark true on the right one, so that a walk can tell which end it has reached.

def DescriptiveComplexity.TapeTag.equivSum {B : SOBlock} : TapeTag B ≃ Bool ⊕ Bool × B.ι ⊕ Unit ⊕ Bool × Bool × B.ι ⊕ Bool

The tape tags as a sum, for the Finite instance.

Equations

• One or more equations did not get rendered due to their size.

instance DescriptiveComplexity.TapeTag.instFinite {B : SOBlock} : Finite (TapeTag B)

instance DescriptiveComplexity.TapeTag.instNonempty {B : SOBlock} : Nonempty (TapeTag B)

def DescriptiveComplexity.TapeTag.fam {B : SOBlock} : TapeTag B → ℕ

The family of a tag, which is what the order of the tape is designed around: the sentinels, then the cells of region 0, then those of region 1, then the right sentinel, then the symbols.

Equations

• (DescriptiveComplexity.TapeTag.left false).fam = 0
• (DescriptiveComplexity.TapeTag.left true).fam = 1
• (DescriptiveComplexity.TapeTag.cell false i).fam = 2
• (DescriptiveComplexity.TapeTag.cell true i).fam = 3
• DescriptiveComplexity.TapeTag.right.fam = 4
• (DescriptiveComplexity.TapeTag.val b r i).fam = 5
• (DescriptiveComplexity.TapeTag.mark b).fam = 6

def DescriptiveComplexity.TapeTag.arity {B : SOBlock} : TapeTag B → ℕ

The number of coordinates a tag uses: an address for a cell and for the symbol of a cell, none for a sentinel or the mark.

Equations

• (DescriptiveComplexity.TapeTag.cell r i).arity = B.arity i
• (DescriptiveComplexity.TapeTag.val b r i).arity = B.arity i
• x✝.arity = 0

def DescriptiveComplexity.TapeTag.IsPos {B : SOBlock} : TapeTag B → Prop

Being a position: the sentinels and the cells, not the symbols.

Equations

• (DescriptiveComplexity.TapeTag.val b r i).IsPos = False
• (DescriptiveComplexity.TapeTag.mark b).IsPos = False
• x✝.IsPos = True

theorem DescriptiveComplexity.TapeTag.fam_le_four {B : SOBlock} {t : TapeTag B} (h : t.IsPos) : t.fam ≤ 4

theorem DescriptiveComplexity.TapeTag.eq_left_false_of_fam_zero {B : SOBlock} {t : TapeTag B} (h : t.fam = 0) : t = left false

theorem DescriptiveComplexity.TapeTag.eq_left_true_of_fam_one {B : SOBlock} {t : TapeTag B} (h : t.fam = 1) : t = left true

theorem DescriptiveComplexity.TapeTag.eq_right_of_fam_four {B : SOBlock} {t : TapeTag B} (h : t.fam = 4) : t = right

The tags of the machine, and their order

@[reducible, inline]

abbrev DescriptiveComplexity.MachTag (B : SOBlock) (C : Type) : Type

The tags of the machine: the tape's, and the control's. The control is a parameter, so this file fixes the tape without committing to the phases.

Equations

• DescriptiveComplexity.MachTag B C = (DescriptiveComplexity.TapeTag B ⊕ C)

def DescriptiveComplexity.MachTag.fam {B : SOBlock} {C : Type} : MachTag B C → ℕ

The family of a machine tag: the control sits above the whole tape.

Equations

• DescriptiveComplexity.MachTag.fam = Sum.elim DescriptiveComplexity.TapeTag.fam fun (x : C) => 7

def DescriptiveComplexity.MachTag.IsPos {B : SOBlock} {C : Type} : MachTag B C → Prop

Being a position: only the tape's positions are.

Equations

• DescriptiveComplexity.MachTag.IsPos = Sum.elim DescriptiveComplexity.TapeTag.IsPos fun (x : C) => False

def DescriptiveComplexity.MachTag.arity {B : SOBlock} {C : Type} (carity : C → ℕ) : MachTag B C → ℕ

The number of coordinates a tag uses, the control's arities being given.

Equations

• DescriptiveComplexity.MachTag.arity carity = Sum.elim DescriptiveComplexity.TapeTag.arity carity

@[simp]

theorem DescriptiveComplexity.MachTag.fam_inl {B : SOBlock} {C : Type} (t : TapeTag B) : fam (Sum.inl t) = t.fam

@[simp]

theorem DescriptiveComplexity.MachTag.isPos_inl {B : SOBlock} {C : Type} (t : TapeTag B) : IsPos (Sum.inl t) = t.IsPos

@[simp]

theorem DescriptiveComplexity.MachTag.isPos_inr {B : SOBlock} {C : Type} (c : C) : IsPos (Sum.inr c) = False

@[simp]

theorem DescriptiveComplexity.MachTag.arity_inl {B : SOBlock} {C : Type} (carity : C → ℕ) (t : TapeTag B) : arity carity (Sum.inl t) = t.arity

theorem DescriptiveComplexity.MachTag.exists_tapeTag_of_isPos {B : SOBlock} {C : Type} {t : MachTag B C} (h : t.IsPos) : ∃ (s : TapeTag B), t = Sum.inl s ∧ s.IsPos

A position's tag is a tape tag.

noncomputable def DescriptiveComplexity.finiteIdx (T : Type) [Finite T] (t : T) : ℕ

An arbitrary injection of a finite type into ℕ, used only to break ties inside a family of tags.

Equations

• DescriptiveComplexity.finiteIdx T t = ↑((Fintype.equivFin T) t)

theorem DescriptiveComplexity.finiteIdx_injective (T : Type) [Finite T] : Function.Injective (finiteIdx T)

noncomputable def DescriptiveComplexity.machKey {B : SOBlock} {C : Type} [Finite C] (t : MachTag B C) : Lex (ℕ × ℕ)

The sort key of a machine tag: its family, then an arbitrary tie-break, read lexicographically. Only the family is designed.

Equations

• DescriptiveComplexity.machKey t = toLex (t.fam, DescriptiveComplexity.finiteIdx (DescriptiveComplexity.MachTag B C) t)

theorem DescriptiveComplexity.machKey_injective {B : SOBlock} {C : Type} [Finite C] : Function.Injective machKey

@[instance_reducible]

noncomputable def DescriptiveComplexity.machTagOrder {B : SOBlock} {C : Type} [Finite C] : LinearOrder (MachTag B C)

The order on the machine's tags: by family, then arbitrarily.

Equations

• DescriptiveComplexity.machTagOrder = LinearOrder.lift' DescriptiveComplexity.machKey ⋯

theorem DescriptiveComplexity.machTag_fam_le_of_le {B : SOBlock} {C : Type} [Finite C] {t t' : MachTag B C} (h : t ≤ t') : t.fam ≤ t'.fam

A lower tag is in a family at most as high.

theorem DescriptiveComplexity.machTag_lt_of_fam_lt {B : SOBlock} {C : Type} [Finite C] {t t' : MachTag B C} (h : t.fam < t'.fam) : t < t'

A tag of a lower family is lower.

The points of the emitted universe

@[reducible, inline]

abbrev DescriptiveComplexity.Pt (B : SOBlock) (C : Type) (dim : ℕ) (A : Type) : Type

A tagged tuple of the emitted universe, before the domain is imposed.

Equations

• DescriptiveComplexity.Pt B C dim A = (DescriptiveComplexity.MachTag B C × (Fin dim → A))

def DescriptiveComplexity.machDom {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} [LinearOrder A] (carity : C → ℕ) (p : Pt B C dim A) : Prop

The domain of the reduction: every coordinate a tag does not use is a minimum, so that a cell of the relation variable i corresponds to exactly one atom of i.

Equations

• DescriptiveComplexity.machDom carity p = DescriptiveComplexity.Canon (DescriptiveComplexity.MachTag.arity carity p.1) p.2

def DescriptiveComplexity.machPosn {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (p : Pt B C dim A) : Prop

Being a position of the tape.

Equations

• DescriptiveComplexity.machPosn p = p.1.IsPos

def DescriptiveComplexity.cellPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) : Pt B C dim A

The point of the cell of region r holding the atom i ā.

Equations

• DescriptiveComplexity.cellPt a₀ r i ā = (Sum.inl (DescriptiveComplexity.TapeTag.cell r i), DescriptiveComplexity.pad a₀ ā)

def DescriptiveComplexity.valPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (b r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) : Pt B C dim A

The symbol of that cell: the bit b, together with the address of the cell it sits in.

Equations

• DescriptiveComplexity.valPt a₀ b r i ā = (Sum.inl (DescriptiveComplexity.TapeTag.val b r i), DescriptiveComplexity.pad a₀ ā)

def DescriptiveComplexity.leftPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (b : Bool) : Pt B C dim A

One of the two left sentinels.

Equations

• DescriptiveComplexity.leftPt a₀ b = (Sum.inl (DescriptiveComplexity.TapeTag.left b), fun (x : Fin dim) => a₀)

def DescriptiveComplexity.rightPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) : Pt B C dim A

The right sentinel.

Equations

• DescriptiveComplexity.rightPt a₀ = (Sum.inl DescriptiveComplexity.TapeTag.right, fun (x : Fin dim) => a₀)

def DescriptiveComplexity.markPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (b : Bool) : Pt B C dim A

The symbol on the sentinels: markPt a₀ false on the left pair, markPt a₀ true on the right one. The blank is markPt a₀ false.

Equations

• DescriptiveComplexity.markPt a₀ b = (Sum.inl (DescriptiveComplexity.TapeTag.mark b), fun (x : Fin dim) => a₀)

theorem DescriptiveComplexity.machPosn_cellPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) : machPosn (cellPt a₀ r i ā)

theorem DescriptiveComplexity.machPosn_leftPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (b : Bool) : machPosn (leftPt a₀ b)

theorem DescriptiveComplexity.machPosn_rightPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) : machPosn (rightPt a₀)

theorem DescriptiveComplexity.leftPt_ne_rightPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (b : Bool) : leftPt a₀ b ≠ rightPt a₀

The two ends of the tape are different points.

theorem DescriptiveComplexity.leftPt_ne_cellPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (b r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) : leftPt a₀ b ≠ cellPt a₀ r i ā

A sentinel is not a cell, so a walk reading a mark is not reading an atom.

theorem DescriptiveComplexity.rightPt_ne_cellPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) : rightPt a₀ ≠ cellPt a₀ r i ā

theorem DescriptiveComplexity.valPt_inj_bit {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) {b b' r : Bool} {i : B.ι} {ā : Fin (B.arity i) → A} (h : valPt a₀ b r i ā = valPt a₀ b' r i ā) : b = b'

A symbol determines its bit, at a fixed cell.

theorem DescriptiveComplexity.markPt_ne_markPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) {b b' : Bool} (h : b ≠ b') : markPt a₀ b ≠ markPt a₀ b'

The two marks are different symbols, which is how a walk tells the ends of the tape apart.

theorem DescriptiveComplexity.valPt_ne_markPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) {b r : Bool} {i : B.ι} {ā : Fin (B.arity i) → A} {b' : Bool} : valPt a₀ b r i ā ≠ markPt a₀ b'

A cell's symbol is not a mark.

theorem DescriptiveComplexity.valPt_inj_tag {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) {b b₂ r r₂ : Bool} {i i₂ : B.ι} {ā : Fin (B.arity i) → A} {ā₂ : Fin (B.arity i₂) → A} (h : valPt a₀ b r i ā = valPt a₀ b₂ r₂ i₂ ā₂) : b = b₂ ∧ r = r₂ ∧ i = i₂

A symbol determines its bit, its region and its relation variable.

theorem DescriptiveComplexity.valPt_eq_of_valPt_eq {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) (b₃ : Bool) {b b₂ r r₂ : Bool} {i i₂ : B.ι} {ā : Fin (B.arity i) → A} {ā₂ : Fin (B.arity i₂) → A} (h : valPt a₀ b r i ā = valPt a₀ b₂ r₂ i₂ ā₂) : valPt a₀ b₃ r i ā = valPt a₀ b₃ r₂ i₂ ā₂

Two symbols that are the same point sit in the same cell, so a walk may write back to it with a different bit.

theorem DescriptiveComplexity.args_eq_of_valPt_eq {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) {b b₂ r r₂ : Bool} {i : B.ι} {ā ā₂ : Fin (B.arity i) → A} (h : valPt a₀ b r i ā = valPt a₀ b₂ r₂ i ā₂) : ā = ā₂

A symbol determines its address, at a fixed relation variable.

theorem DescriptiveComplexity.cellPt_eq_of_valPt_eq {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) {b b₂ r r₂ : Bool} {i i₂ : B.ι} {ā : Fin (B.arity i) → A} {ā₂ : Fin (B.arity i₂) → A} (h : valPt a₀ b r i ā = valPt a₀ b₂ r₂ i₂ ā₂) : cellPt a₀ r i ā = cellPt a₀ r₂ i₂ ā₂

The cell a symbol sits in, from the symbol read at it.

theorem DescriptiveComplexity.machDom_cellPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} [LinearOrder A] (a₀ : A) {carity : C → ℕ} (h₀ : IsBot a₀) (r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) : machDom carity (cellPt a₀ r i ā)

A cell is in the domain.

The ends of the tape

theorem DescriptiveComplexity.eq_const_of_dom {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {carity : C → ℕ} {p : Pt B C dim A} (hp : machDom carity p) (harity : MachTag.arity carity p.1 = 0) : p.2 = fun (x : Fin dim) => a₀

A point of the domain whose tag uses no coordinate is the constant tuple: the sentinels and the mark carry exactly one point each.

theorem DescriptiveComplexity.minPos_leftPt {B : SOBlock} {C : Type} [Finite C] {dim : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {carity : C → ℕ} : MinPos tagTupleLe (fun (p : MachTag B C × (Fin dim → A)) => machPosn p ∧ machDom carity p) (leftPt a₀ false)

The lowest position is the first left sentinel.

theorem DescriptiveComplexity.eq_leftPt_of_le {B : SOBlock} {C : Type} [Finite C] {dim : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {carity : C → ℕ} {q : Pt B C dim A} (hq : machPosn q ∧ machDom carity q) (hle : tagTupleLe q (leftPt a₀ true)) : q = leftPt a₀ false ∨ q = leftPt a₀ true

Only the two sentinels sit at or below the second one.

theorem DescriptiveComplexity.leftPt_le_leftPt_true {B : SOBlock} {C : Type} [Finite C] {dim : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (b : Bool) : tagTupleLe (leftPt a₀ b) (leftPt a₀ true)

Both sentinels sit at or below the second one.

theorem DescriptiveComplexity.succPos_leftPt {B : SOBlock} {C : Type} [Finite C] {dim : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {carity : C → ℕ} : SuccPos tagTupleLe (fun (p : MachTag B C × (Fin dim → A)) => machPosn p ∧ machDom carity p) (leftPt a₀ false) (leftPt a₀ true)

The two left sentinels are adjacent. This is the one order fact about the layout the development needs: a rewind hands over on reading the left mark and moves left in the same step, so it has to land on the lowest position, and it does exactly because nothing sits between the two sentinels.

theorem DescriptiveComplexity.succPos_ne_leftPt {B : SOBlock} {C : Type} [Finite C] {dim : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {carity : C → ℕ} {p q : Pt B C dim A} (hfam : 1 < q.1.fam) (hs : SuccPos tagTupleLe (fun (x : MachTag B C × (Fin dim → A)) => machPosn x ∧ machDom carity x) p q) : p ≠ leftPt a₀ false

Nothing above the second sentinel sits next to the first: the second one is between them. So a leftward walk leaving a cell – or the right sentinel – does not land on the lowest position, which is what tells a rewind that it still has the left mark to read.

theorem DescriptiveComplexity.one_lt_fam_cellPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} {a₀ : A} (r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) : 1 < (cellPt a₀ r i ā).1.fam

A cell sits above the second sentinel.

theorem DescriptiveComplexity.one_lt_fam_rightPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} {a₀ : A} : 1 < (rightPt a₀).1.fam

So does the right sentinel.

theorem DescriptiveComplexity.posn_cases_tape {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {carity : C → ℕ} (hdim : blockArityBound B ≤ dim) {p : Pt B C dim A} (hp : machPosn p) (hd : machDom carity p) : (∃ (b : Bool), p = leftPt a₀ b) ∨ (∃ (r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A), p = cellPt a₀ r i ā) ∨ p = rightPt a₀

What a position is: a left sentinel, a cell, or the right sentinel – which is where every walk's step analysis begins, the symbol under the head following from the case.

theorem DescriptiveComplexity.maxPos_rightPt {B : SOBlock} {C : Type} [Finite C] {dim : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {carity : C → ℕ} : MaxPos tagTupleLe (fun (p : MachTag B C × (Fin dim → A)) => machPosn p ∧ machDom carity p) (rightPt a₀)

The highest position is the right sentinel.

A tape is a pair of assignments

def DescriptiveComplexity.assignOfTape {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (tape : Pt B C dim A → Pt B C dim A) (r : Bool) : B.Assignment A

The assignment a tape holds in region r: the atom i ā belongs to it exactly when the cell of that atom carries the bit true.

Equations

• DescriptiveComplexity.assignOfTape a₀ tape r i ā = (tape (DescriptiveComplexity.cellPt a₀ r i ā) = DescriptiveComplexity.valPt a₀ true r i ā)

noncomputable def DescriptiveComplexity.tapeOfAssign {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) (ρ σ : B.Assignment A) : Pt B C dim A → Pt B C dim A

The tape holding two assignments: the first in region 0, the second in region 1, each cell carrying its own address, the mark everywhere else.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.tapeOfAssign_cellPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) (ρ σ : B.Assignment A) (r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) : tapeOfAssign a₀ hdim ρ σ (cellPt a₀ r i ā) = valPt a₀ (decide ((bif r then σ else ρ) i ā)) r i ā

The symbol a cell carries is the cell's own address, tagged with the bit the assignment gives its atom. This is what lets a walk recognize where it is from what it reads.

theorem DescriptiveComplexity.tapeOfAssign_leftPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) (ρ σ : B.Assignment A) (b : Bool) : tapeOfAssign a₀ hdim ρ σ (leftPt a₀ b) = markPt a₀ false

The left sentinels carry the left mark.

theorem DescriptiveComplexity.tapeOfAssign_rightPt {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) (ρ σ : B.Assignment A) : tapeOfAssign a₀ hdim ρ σ (rightPt a₀) = markPt a₀ true

The right sentinel carries the right mark, which is what tells a rightward walk that it is over.

theorem DescriptiveComplexity.assignOfTape_tapeOfAssign {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) (ρ σ : B.Assignment A) (r : Bool) : assignOfTape a₀ (tapeOfAssign a₀ hdim ρ σ) r = bif r then σ else ρ

The tape of two assignments holds them back.

One cell of an assignment, rewritten

noncomputable def DescriptiveComplexity.updAssign {B : SOBlock} {A : Type} (α : B.Assignment A) (i : B.ι) (ā : Fin (B.arity i) → A) (b : Bool) : B.Assignment A

An assignment with one atom's value changed: what one step of a sweep does to the region it is writing. Named rather than written inline, because DescriptiveComplexity.SOBlock.Assignment is a non-reducible def.

Equations

• DescriptiveComplexity.updAssign α i ā b i' ā' = if ⟨i', ā'⟩ = ⟨i, ā⟩ then b = true else α i' ā'

theorem DescriptiveComplexity.updAssign_self {B : SOBlock} {A : Type} (α : B.Assignment A) (i : B.ι) (ā : Fin (B.arity i) → A) (b : Bool) : updAssign α i ā b i ā = (b = true)

theorem DescriptiveComplexity.updAssign_of_ne {B : SOBlock} {A : Type} (α : B.Assignment A) (i : B.ι) (ā : Fin (B.arity i) → A) (b : Bool) {i' : B.ι} {ā' : Fin (B.arity i') → A} (h : ⟨i', ā'⟩ ≠ ⟨i, ā⟩) : updAssign α i ā b i' ā' = α i' ā'

theorem DescriptiveComplexity.exists_tapeOfAssign_upd {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) [LinearOrder A] {carity : C → ℕ} (h₀ : IsBot a₀) (hdim : blockArityBound B ≤ dim) (ρ' σ' : B.Assignment A) (tgt : Bool) (i : B.ι) (ā : Fin (B.arity i) → A) (b' : Bool) : ∃ (ρ'' : B.Assignment A) (σ'' : B.Assignment A), (∀ (rr : Bool), rr ≠ tgt → (bif rr then σ'' else ρ'') = bif rr then σ' else ρ') ∧ (∀ (q : Pt B C dim A), machPosn q → machDom carity q → q ≠ cellPt a₀ tgt i ā → tapeOfAssign a₀ hdim ρ'' σ'' q = tapeOfAssign a₀ hdim ρ' σ' q) ∧ tapeOfAssign a₀ hdim ρ'' σ'' (cellPt a₀ tgt i ā) = valPt a₀ b' tgt i ā

A sweep step rewrites one cell, and the tape is again a pair of assignments – a pair agreeing with the old one outside the region being written. This is the whole content of the sweep's invariant: what it has done so far is some assignment of that region.

A tape is only ever read at a position

theorem DescriptiveComplexity.assignOfTape_congr {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} [LinearOrder A] (a₀ : A) {carity : C → ℕ} (h₀ : IsBot a₀) {t u : Pt B C dim A → Pt B C dim A} (h : ∀ (p : Pt B C dim A), machPosn p → machDom carity p → t p = u p) (r : Bool) : assignOfTape a₀ t r = assignOfTape a₀ u r

Two tapes that agree at the positions hold the same assignments. A machine reads its tape only under its head, and its head is always a position, so this is the only sense in which a walk has to control the tape – the non-canonical tagged tuples, which are not positions, keep whatever they started with and are never read.

The initial tape

def DescriptiveComplexity.emptyAssign (B : SOBlock) (A : Type) : B.Assignment A

The empty assignment. Named rather than written as a lambda, because DescriptiveComplexity.SOBlock.Assignment is a non-reducible def and a lambda literal in that position is ill-typed at implicit transparency, which makes rw fail.

Equations

• DescriptiveComplexity.emptyAssign B A x✝¹ x✝ = False

noncomputable def DescriptiveComplexity.gameInitTape {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) : Pt B C dim A → Pt B C dim A

The initial tape: both regions empty, the sentinels marked.

Equations

• DescriptiveComplexity.gameInitTape a₀ hdim = DescriptiveComplexity.tapeOfAssign a₀ hdim (DescriptiveComplexity.emptyAssign B A) (DescriptiveComplexity.emptyAssign B A)

def DescriptiveComplexity.machInp {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} (a₀ : A) (hdim : blockArityBound B ≤ dim) (p x : Pt B C dim A) : Prop

The input of the machine: which symbol each position starts with. It is total on the positions – every cell starts empty rather than blank – which is what makes it functional, as DescriptiveComplexity.TMData.WellFormed demands, and what pins the initial configuration.

Equations

• DescriptiveComplexity.machInp a₀ hdim p x = (DescriptiveComplexity.machPosn p ∧ x = DescriptiveComplexity.gameInitTape a₀ hdim p)

theorem DescriptiveComplexity.machInp_functional {B : SOBlock} {C : Type} {dim : ℕ} {A : Type} {a₀ : A} {hdim : blockArityBound B ≤ dim} {p x y : Pt B C dim A} (hx : machInp a₀ hdim p x) (hy : machInp a₀ hdim p y) : x = y

The input is functional.