The sweep, read back

DescriptiveComplexity.sweep_run says what a sweep may do; the game needs the converse as well, because the universal player's move is a sweep and DescriptiveComplexity.ATMData.AltWin.all quantifies over every step. So a sweep has to be read back the way DescriptiveComplexity.ctrlCfg_cases reads back a control step.

The invariant

DescriptiveComplexity.SweptCfg is the tape is tapeOfAssign ρ' σ' for some pair agreeing with the original outside the swept region. That is exactly what a half-finished sweep has: the cells it has passed hold the new assignment, those ahead the old one, and a mixture of the two is again an assignment – so no notion of “how far it has got” is needed, and the order on cells is never consulted.

The step that rewrites one cell is DescriptiveComplexity.exists_tapeOfAssign_upd, and the whole content of DescriptiveComplexity.sweepCfg_cases is that every step either keeps the family and moves the head on, or is the handover to the rewind at the right sentinel.

What the game gets

• DescriptiveComplexity.altWin_sweep_ex – the existential player sweeps a chosen assignment in and the play continues at the rewind's target;
• DescriptiveComplexity.altWin_sweep_all – the universal player's sweep, where every assignment of the region has to be answered. It is the one place a walk is run backwards, through DescriptiveComplexity.altWin_of_walk.

A configuration of a sweep

def DescriptiveComplexity.SweptCfg {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] (a₀ : A) (hdim : blockArityBound B ≤ gameDim B V) (vars : GameQuestion → ℕ) (ρ σ : B.Assignment A) (tgt : Bool) (p : MachPh V M) (c : Config (GamePt B V M A)) : Prop

A tape a sweep may have produced: the machine is in the given phase at the constant valuation, its head is a position, and the tape holds a pair of assignments agreeing with the original outside the region being written.

Equations

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

theorem DescriptiveComplexity.sweepCfg_cases {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ρ σ : B.Assignment A} {r tgt : Bool} {cont : SweepCont} {par : Bool} (h₀ : IsBot a₀) {c c' : Config (GamePt B V M A)} (h : SweptCfg a₀ hdim vars ρ σ tgt (MachPh.sweepPh r tgt cont par) c) (hstep : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c c') : SweptCfg a₀ hdim vars ρ σ tgt (MachPh.sweepPh r tgt cont par) c' ∧ SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head c'.head ∨ SweptCfg a₀ hdim vars ρ σ tgt (MachPh.rewindPh r tgt cont false) c' ∧ c'.head ≠ rightPt a₀ ∧ c'.head ≠ leftPt a₀ false

Every step of a sweep either carries it on or hands over to its rewind. The three rule families are told apart by the symbol read – the left mark, a cell's symbol, the right mark – so the head's position decides which fires, and the family is closed because rewriting one cell of the swept region gives another assignment of it.

The rewind that follows a sweep

theorem DescriptiveComplexity.altWin_rewind {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] [Finite A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {r tgt : Bool} {cont : SweepCont} (h₀ : IsBot a₀) {ρ' σ' : B.Assignment A} {d : Config (GamePt B V M A)} (hstate : d.state = phasePt (MachPh.rewindPh r tgt cont false) fun (x : Fin (gameDim B V)) => a₀) (hpos : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn d.head) (hne : d.head ≠ rightPt a₀) (hlow : d.head ≠ leftPt a₀ false) (htape : ∀ (q : GamePt B V M A), machPosn q → machDom (ctrlArity vars) q → d.tape q = tapeOfAssign a₀ hdim ρ' σ' q) (hcont : ∀ (c' : Config (GamePt B V M A)), CtrlCfg a₀ hdim vars ρ' σ' (MachPh.rewindPh r tgt cont false).rewindTarget (fun (x : Fin (gameDim B V)) => a₀) c' → (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c') : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true d

A rewind wins if its continuation does. It changes nothing and its phase is existential, so the whole walk back is one guarded chain.

The two sweeps

theorem DescriptiveComplexity.altWin_sweep_ex {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] [Finite A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ρ σ : B.Assignment A} {r tgt : Bool} {cont : SweepCont} {par : Bool} (h₀ : IsBot a₀) {ρ' σ' : B.Assignment A} (hkeep : ∀ (rr : Bool), rr ≠ tgt → (bif rr then σ' else ρ') = bif rr then σ else ρ) (hnu : MachPh.IsUniv pol (MachPh.sweepPh r tgt cont par) = false) {c : Config (GamePt B V M A)} (hstate : c.state = phasePt (MachPh.sweepPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) {bhd : Bool} (hhead : c.head = leftPt a₀ bhd) (htape : ∀ (q : GamePt B V M A), machPosn q → machDom (ctrlArity vars) q → c.tape q = tapeOfAssign a₀ hdim ρ σ q) (hcont : ∀ (c' : Config (GamePt B V M A)), CtrlCfg a₀ hdim vars ρ' σ' (MachPh.rewindPh r tgt cont false).rewindTarget (fun (x : Fin (gameDim B V)) => a₀) c' → (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c') : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c

An existential sweep writes the assignment its owner chooses, and the play continues at the rewind's target.

theorem DescriptiveComplexity.altWin_sweep_all {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] [Finite A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ρ σ : B.Assignment A} {r tgt : Bool} {cont : SweepCont} {par : Bool} (h₀ : IsBot a₀) (hu : MachPh.IsUniv pol (MachPh.sweepPh r tgt cont par) = true) {c : Config (GamePt B V M A)} (hc : SweptCfg a₀ hdim vars ρ σ tgt (MachPh.sweepPh r tgt cont par) c) (hcont : ∀ (ρ' σ' : B.Assignment A), (∀ (rr : Bool), rr ≠ tgt → (bif rr then σ' else ρ') = bif rr then σ else ρ) → ∀ (c' : Config (GamePt B V M A)), CtrlCfg a₀ hdim vars ρ' σ' (MachPh.rewindPh r tgt cont false).rewindTarget (fun (x : Fin (gameDim B V)) => a₀) c' → (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c') : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c

A universal sweep is answered for every assignment of its region. This is the one place the simulation runs a walk backwards: AltWin.all quantifies over every step, so the sweep cannot be summarized by its run.