Reading a block's assignment off an arbitrary run

The direction a universal round needs. DescriptiveComplexity.AltQbf.steps_sweep exhibits the run of a sweep against a given assignment; a universal player must be answered for every play of its block, so the converse is needed: whatever the machine does during sweep i, it is the intended run of some assignment of block i.

The invariant is DescriptiveComplexity.AltQbf.InSweepR: at every moment of the rightward pass the tape is tapeAfter (Function.update νs i ν') (i+1) for the ν' the sweep has written so far, which is supported strictly below the head. Cells at or above the head are therefore untouched – ν' is false there, and DescriptiveComplexity.AltQbf.valAfter_update_succ collapses the disjunction back to the old value – so one statement covers the whole pass rather than needing a separate “below the head” clause.

The only two transitions that can fire at a cell are tGKeep, which changes nothing, and tGSet, which adds the cell's variable to ν'. That the machine has no other choice is DescriptiveComplexity.AltQbf.altTr_unique.

Comparing tapes

The invariant of a rightward pass

def DescriptiveComplexity.AltQbf.InSweepR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (i : Fin k) (νs : Fin k → A → Prop) (c : Config (AltV k A)) : Prop

What is true at every moment of the rightward pass of sweep i. The witness ν' is what the sweep has written so far: a set of variables block i marks, all of them strictly below the head. The head itself lies between the first cell and the right marker, which is what says that the machine still has a move: above the right marker the tape is blank, and no transition reads a blank.

Equations

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

What the tape says about the head

Writing one cell

One step of the pass

def DescriptiveComplexity.AltQbf.InSweepL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (i : Fin k) (νs : Fin k → A → Prop) (c : Config (AltV k A)) : Prop

What is true at every moment of the leftward pass: the sweep is over, the tape holds what it wrote, and the head is on its way back down from the last cell.

Equations

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

theorem DescriptiveComplexity.AltQbf.inSweepR_step {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {i : Fin k} {νs : Fin k → A → Prop} {c c' : Config (AltV k A)} (hinv : InSweepR i νs c) (hstep : (altMachine k A cnf).Step c c') : InSweepR i νs c' ∧ bitRank tagTupleLe AltPosn c.head < bitRank tagTupleLe AltPosn c'.head ∨ InSweepL i νs c'

One step of the rightward pass, whatever the machine chooses. Only three transitions can fire once the pass has left the left marker: the turn at the right one changes nothing, tGKeep leaves the cell alone, and tGSet adds its variable to what the block has assigned. The head moves up until the turn, which is what makes the pass terminate.

Where a sweep hands over

def DescriptiveComplexity.AltQbf.AfterSweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (i : Fin k) (ρ : Fin k → A → Prop) (c : Config (AltV k A)) : Prop

What the machine has reached once the sweep of index i is over: the head is back at the first cell and the tape holds what the block wrote. The state is the entry of the next sweep, or – after the last one – the entry of the check phase, or acceptance outright, an instance with no clause at all being satisfied by a conjunctive matrix.

Equations

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

theorem DescriptiveComplexity.AltQbf.inSweepL_step {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {i : Fin k} {νs : Fin k → A → Prop} {c c' : Config (AltV k A)} (hinv : InSweepL i νs c) (hstep : (altMachine k A cnf).Step c c') : InSweepL i νs c' ∧ bitRank tagTupleLe AltPosn c'.head < bitRank tagTupleLe AltPosn c.head ∨ ∃ (ν' : A → Prop), (∀ (x : A), ν' x → QbfBlk i x) ∧ AfterSweep cnf i (Function.update νs i ν') c'

One step of the leftward pass, whatever the machine chooses. Only four transitions can fire from a leftward sweeping state, and none of them writes: tGBack walks the cells back, and the three that fire at the left marker hand the tape over – to the next sweep, to the check phase, or to acceptance.