The rounds, one block at a time

The induction that turns the machine into the quantifier prefix. Round m starts at DescriptiveComplexity.AltQbf.AtRound: the head at the first cell, the tape holding what the blocks below m have written, and the state the entry of sweep m – or, when every block has played, the entry of the check phase.

Each round is answered by whichever player owns its block, and the four corners were built in AltGuess: an existential round picks an assignment (altAcc_passes_up) and any accepting run of it hands one over (exit_of_altAcc); a universal round survives all of them (altAcc_of_inSweepR) and is followed along the run of any given one (altAcc_passes_down). The base case is the check phase, decided both ways in AltVerdict.

The read-off returns some assignment, not a chosen one, which is what an existential round wants and a universal one does not. So a universal round does not follow the read-off at all: it names the configuration it wants to hand over (DescriptiveComplexity.AltQbf.exists_atRound) and appeals to the fact that every successor of a universal configuration accepts.

Where the machine stands between rounds

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

The entry of round m: the head at the first cell, the tape holding what the blocks below m wrote, and the state the entry of sweep m – or, once every block has played, the entry of the check phase, or acceptance outright when there is nothing to check.

Equations

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

theorem DescriptiveComplexity.AltQbf.exists_atRound {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {m : ℕ} (hm : m ≤ k) (νs : Fin k → A → Prop) (hover : m = k → CanHandOver k A cnf) : ∃ (c : Config (AltV k A)), AtRound cnf m νs c

The entry of a round exists. Before the last block has played it is the entry of the next sweep; after it, the check phase starts at the lowest clause, or the machine accepts outright when there is nothing to check.

The budget

A round costs a sweep, and a universal round costs a walk up and back down the tape once for each of the two passes, whatever the play.

noncomputable def DescriptiveComplexity.AltQbf.roundStep (k : ℕ) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : ℕ

What one round costs: exactly the sweep it plays, whichever player owns it.

Equations

• DescriptiveComplexity.AltQbf.roundStep k A = DescriptiveComplexity.AltQbf.sweepLen k A

noncomputable def DescriptiveComplexity.AltQbf.roundBound (k : ℕ) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : ℕ → ℕ

What the last r rounds cost, the check phase included.

Equations

• DescriptiveComplexity.AltQbf.roundBound k A 0 = DescriptiveComplexity.AltQbf.chkLen k A
• DescriptiveComplexity.AltQbf.roundBound k A r.succ = DescriptiveComplexity.AltQbf.roundBound k A r + DescriptiveComplexity.AltQbf.roundStep k A

The induction over rounds

The whole run

The first sweep starts at the left marker rather than at the first cell, so the run has one step to take before round 0 begins. It is a forced step – the machine reads ⊢, which is not a guess – so it costs one unit of budget and nothing else.

The tape is long enough

The k rounds cost one sweep each and the check one sweep per clause, which is what DescriptiveComplexity.AltQbf.alt_budget was proved for: the filler positions alone outnumber them.

theorem DescriptiveComplexity.AltQbf.roundBound_eq {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (r : ℕ) : roundBound k A r = chkLen k A + r * sweepLen k A

theorem DescriptiveComplexity.AltQbf.altAccepts_iff_qbf {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} (hk : 0 < k) : (altMachine k A cnf).AltAccepts start ↔ altQuant A k (QbfMatrix cnf) start

The machine of a quantified Boolean formula accepts exactly when the formula is true. The semantic half of QBF k ≤ᶠᵒ[≤] ATMAccept k: what is left is to write the machine down in first-order logic.