The run of the QBF machine

What the machine computes. This file opens with the dictionary between a tape and a valuation, since that is what the evaluation sweep and the game semantics have to be compared through.

A tape of the machine is laid out (DescriptiveComplexity.QsatTM.TapeOk) when every quantified variable's cell holds one of the four sVal symbols – which the initial tape does and every transition preserves. Such a tape is a valuation (DescriptiveComplexity.QsatTM.TapeTrue: the variable is true when its cell holds the value true), and under that dictionary the first-order literal test the transition table performs (DescriptiveComplexity.QsatTM.QLit) is the literal of DescriptiveComplexity.QsatMatrix. DescriptiveComplexity.QsatTM.qsatMatrix_iff is the resulting reading of the matrix: it holds exactly when every clause has a variable whose cell satisfies it, which is what one full sweep of the Eval phase decides.

A tape is a valuation

def DescriptiveComplexity.QsatTM.TapeOk {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) : Prop

A tape is laid out when every quantified variable's cell holds a value and a flag. The initial tape is, and every transition preserves it.

Equations

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

def DescriptiveComplexity.QsatTM.TapeTrue {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (x : A) : Prop

The valuation a tape encodes: the variable x is true when its cell holds the value true.

Equations

• DescriptiveComplexity.QsatTM.TapeTrue σ x = ∃ (f : Bool), σ (DescriptiveComplexity.QsatTM.posCell x) = DescriptiveComplexity.QsatTM.symV true f x

The matrix, read off the tape

theorem DescriptiveComplexity.QsatTM.qsatMatrix_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hok : TapeOk σ) : QsatMatrix (TapeTrue σ) ↔ ∀ (c : A), QCl c → ∃ (x : A) (b : Bool) (f : Bool), IsQVar x ∧ σ (posCell x) = symV b f x ∧ QLit c x b

The matrix holds of a laid-out tape exactly when every clause has a cell satisfying it. The right-hand side is what one full sweep of the evaluation phase decides, clause by clause; the left-hand side is what the game asks at a leaf.

Writing a cell

Every transition that changes the tape changes one cell of one variable, so the run only ever needs this one update. The step lemmas of DescriptiveComplexity.Problems.Machine.QsatStep take the next tape as an arbitrary σ' pinned at the head; DescriptiveComplexity.QsatTM.setCell is the σ' the run will always pass them.

noncomputable def DescriptiveComplexity.QsatTM.setCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (x : A) (b f : Bool) : QV A → QV A

The tape σ with the cell of x set to the value b and the flag f.

Equations

• DescriptiveComplexity.QsatTM.setCell σ x b f r = if r = DescriptiveComplexity.QsatTM.posCell x then DescriptiveComplexity.QsatTM.symV b f x else σ r

@[simp]

theorem DescriptiveComplexity.QsatTM.setCell_self {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (x : A) (b f : Bool) : setCell σ x b f (posCell x) = symV b f x

theorem DescriptiveComplexity.QsatTM.setCell_ne {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {x : A} {b f : Bool} {r : QV A} (h : r ≠ posCell x) : setCell σ x b f r = σ r

@[simp]

theorem DescriptiveComplexity.QsatTM.tapeTrue_setCell_self {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {x : A} {b f : Bool} : TapeTrue (setCell σ x b f) x ↔ b = true

Writing a cell sets that variable's value.

The descent

The machine's first act, and the act it repeats every time a level switches to its second value: sweep rightwards to the right marker, resetting every variable's cell on the way. The sweep is the segment primitive of DescriptiveComplexity.Problems.Machine.Program, whose configuration family is p ↦ ⟨stDesc, p, resetSeg σ p₀ p⟩ – the tape with every variable cell of the half-open segment [p₀, p) reset.

The evaluation sweep

One pass over the tape for one clause. The state carries the flag, and the flag at a position is exactly “some variable's cell already swept satisfies the clause”; the pass therefore ends at the far marker with the flag set iff the clause holds of the tape.

The clause loop

One pass per clause, alternating direction, until a clause fails or the last one succeeds. The recursion is on the clause in the ambient order, which is well founded because the instance is finite.

theorem DescriptiveComplexity.QsatTM.marker_tape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hS : σ posStart = symStart) (hE : σ posEnd = symEnd) (d : Bool) : σ (markerPos d) = markerSym d

Carrying the verdict back

The position of the game, read off the tape

The dictionary for the prefix, as DescriptiveComplexity.QsatTM.TapeTrue was the dictionary for the valuation: the head sitting at p means the game has already quantified exactly the variables whose cells lie strictly below p.

The two ways a level is decided

The Proc phase reads a returned value and either settles the level or tries its second value. These are the two game-theoretic facts behind that, and they are about DescriptiveComplexity.QsatWins alone – no machine.

The game induction

The last step, and the one the whole file was preparing: the machine's descent and return compute the value of the game position its head sits at.

Two nested recursions. The outer one is on the variables still to be quantified at p; the inner one walks the Proc phase leftwards from the innermost variable back to p. The inner walk calls the outer one exactly once, at a switch, and on strictly fewer variables – which is what makes the pair well founded.

The tape after a descent

The tape the machine starts on

The machine decides QSAT

theorem DescriptiveComplexity.QsatTM.qsatMachine_correct {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (qsatMachine A).WellFormed ∧ (qsatMachine A).Deterministic ∧ (qsatMachine A).AcceptsSpace ↔ QsatHolds A

The machine of a QSAT instance decides it. A malformed instance has no accepting state, so it is a no-instance on both sides.