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.

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

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

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)

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 ⋯

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

The ends of the tape

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.

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

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)