The machine of a quantified Boolean formula

The program half of QBF k ≤ᶠᵒ[≤] ATMAccept k: the states, symbols and transitions of the alternating machine M_φ built inside an ordered QBF instance, on the tape laid out in DescriptiveComplexity.Problems.Machine.AltTape.

The program

  sweep i:  ⊢ →  at each cell (x, b): if block i marks x and b is false,
                 write true or leave it – the round's choice        → ⊣
            ⊣ ←  back over the cells, unchanged                     → ⊢
            at ⊢: hand over to sweep i + 1, or start the check
  check c:  sweep over the cells accumulating
              flag := flag ∨ (the literal of c at this cell is `good`)
            at the far marker: settle the clause, or die
  accept:   the check has settled every clause

Three things differ from the SAT machine of DescriptiveComplexity.Problems.Machine.Hardness.

The guess is spread over k sweeps, and it accumulates. A cell holds one truth value, initially false, and sweep i may turn it to true when block i marks the variable – never back. After the k sweeps the cell holds DescriptiveComplexity.qbfVal, which is a disjunction over the blocks marking the variable. So there are two transitions available at a cell block i marks and holds false, and one everywhere else: the choice a round makes is exactly its block's truth assignment.

Only the guess is nondeterministic, as in the SAT machine – which is what makes the check work at either polarity: a universal block whose configuration has a single available move is an existential one.

The check serves both matrix shapes. For a conjunctive matrix the flag records that some literal of the clause is satisfied, and a clause is settled when the flag is set; for a disjunctive one it records that some literal is violated, and a term is settled – by accepting – when the flag is clear. The two are the same clause with the truth value flipped (DescriptiveComplexity.xorB), which is why one table serves both.

Semantics first

Everything here is a plain predicate on tagged tuples: the machine is assembled as a DescriptiveComplexity.ATMData and reasoned about directly. Only once its correctness is proved does the first-order transcription happen.

The instance, read

def DescriptiveComplexity.AltQbf.QbfCl (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] (c : A) : Prop

Being a clause – a term, for a disjunctive matrix – of the instance.

Equations

• DescriptiveComplexity.AltQbf.QbfCl k c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qbfIsClause ![c]

def DescriptiveComplexity.AltQbf.QbfPos (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] (c x : A) : Prop

The variable x occurs positively in the clause c.

Equations

• DescriptiveComplexity.AltQbf.QbfPos k c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qbfPosIn ![c, x]

def DescriptiveComplexity.AltQbf.QbfNeg (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] (c x : A) : Prop

The variable x occurs negatively in the clause c.

Equations

• DescriptiveComplexity.AltQbf.QbfNeg k c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qbfNegIn ![c, x]

def DescriptiveComplexity.AltQbf.QbfBlk {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (i : Fin k) (x : A) : Prop

The variable x carries the mark of block i.

Equations

• DescriptiveComplexity.AltQbf.QbfBlk i x = FirstOrder.Language.Structure.RelMap (FirstOrder.Language.qbfBlock i) ![x]

def DescriptiveComplexity.AltQbf.QbfBlkAt {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (i : Fin (k + 1)) (x : A) : Prop

The variable x carries the mark of the block of index i, where i is allowed to be the sentinel k: at the sentinel, no mark.

Equations

• DescriptiveComplexity.AltQbf.QbfBlkAt i x = ∃ (j : Fin k), ↑j = ↑i ∧ DescriptiveComplexity.AltQbf.QbfBlk j x

def DescriptiveComplexity.AltQbf.QbfLit (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] (c x : A) (v : Bool) : Prop

The literal test: the cell x, holding the truth value v, satisfies the clause c. This is the first-order test on the source structure that the transition relation performs.

Equations

• DescriptiveComplexity.AltQbf.QbfLit k c x v = (DescriptiveComplexity.AltQbf.QbfPos k c x ∧ v = true ∨ DescriptiveComplexity.AltQbf.QbfNeg k c x ∧ v = false)

def DescriptiveComplexity.AltQbf.xorB (cnf v : Bool) : Bool

The truth value the check phase tests: the value itself for a conjunctive matrix, its negation for a disjunctive one, so that the flag records a satisfied literal in the first case and a violated one in the second.

Equations

• DescriptiveComplexity.AltQbf.xorB cnf v = if cnf = true then v else !v

def DescriptiveComplexity.AltQbf.QbfMinCl (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (c : A) : Prop

c is the lowest clause.

Equations

• DescriptiveComplexity.AltQbf.QbfMinCl k c = (DescriptiveComplexity.AltQbf.QbfCl k c ∧ ∀ (e : A), DescriptiveComplexity.AltQbf.QbfCl k e → c ≤ e)

def DescriptiveComplexity.AltQbf.QbfMaxCl (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (c : A) : Prop

c is the highest clause.

Equations

• DescriptiveComplexity.AltQbf.QbfMaxCl k c = (DescriptiveComplexity.AltQbf.QbfCl k c ∧ ∀ (e : A), DescriptiveComplexity.AltQbf.QbfCl k e → e ≤ c)

def DescriptiveComplexity.AltQbf.QbfNextCl (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (c c' : A) : Prop

c' is the clause immediately above c.

Equations

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

The elements of the machine

noncomputable def DescriptiveComplexity.AltQbf.qbotA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : A

The least element of the instance, to which every constant of the machine is pinned.

Equations

• DescriptiveComplexity.AltQbf.qbotA = ⋯.choose

theorem DescriptiveComplexity.AltQbf.qbotA_le {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) : qbotA ≤ a

theorem DescriptiveComplexity.AltQbf.isMinTup2_qbot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : IsMinTup2 fun (x : Fin 2) => qbotA

@[reducible, inline]

abbrev DescriptiveComplexity.AltQbf.AltV (k : ℕ) (A : Type) : Type

The universe of the machine: tagged pairs.

Equations

• DescriptiveComplexity.AltQbf.AltV k A = (DescriptiveComplexity.AltQbf.AltTag k × (Fin 2 → A))

noncomputable def DescriptiveComplexity.AltQbf.acstI {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : AltBase) (i : Fin (k + 1)) : AltV k A

A constant of the machine at the sweep index i.

Equations

• DescriptiveComplexity.AltQbf.acstI t i = ((t, i), fun (x : Fin 2) => DescriptiveComplexity.AltQbf.qbotA)

noncomputable def DescriptiveComplexity.AltQbf.aoneI {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : AltBase) (i : Fin (k + 1)) (a : A) : AltV k A

A tag carrying one element at the sweep index i.

Equations

• DescriptiveComplexity.AltQbf.aoneI t i a = ((t, i), ![a, DescriptiveComplexity.AltQbf.qbotA])

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.acst {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : AltBase) : AltV k A

A constant of the machine: a tag on the pair of least elements.

Equations

• DescriptiveComplexity.AltQbf.acst t = DescriptiveComplexity.AltQbf.acstI t 0

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.aone {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : AltBase) (a : A) : AltV k A

A tag carrying one element, pinned in the second coordinate.

Equations

• DescriptiveComplexity.AltQbf.aone t a = DescriptiveComplexity.AltQbf.aoneI t 0 a

Symbols

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.symStart {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : AltV k A

The left-marker symbol.

Equations

• DescriptiveComplexity.AltQbf.symStart = DescriptiveComplexity.AltQbf.acst DescriptiveComplexity.AltQbf.AltBase.sStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.symEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : AltV k A

The right-marker symbol.

Equations

• DescriptiveComplexity.AltQbf.symEnd = DescriptiveComplexity.AltQbf.acst DescriptiveComplexity.AltQbf.AltBase.sEnd

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.symBlank {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : AltV k A

The blank symbol.

Equations

• DescriptiveComplexity.AltQbf.symBlank = DescriptiveComplexity.AltQbf.acst DescriptiveComplexity.AltQbf.AltBase.sBlank

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.symV {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (v : Bool) (x : A) : AltV k A

The symbol of the cell of x, holding the truth value v.

Equations

• DescriptiveComplexity.AltQbf.symV v x = DescriptiveComplexity.AltQbf.aone (DescriptiveComplexity.AltQbf.AltBase.sVal v) x

Positions

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.posStart {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : AltV k A

The left-marker cell.

Equations

• DescriptiveComplexity.AltQbf.posStart = DescriptiveComplexity.AltQbf.acst DescriptiveComplexity.AltQbf.AltBase.pStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.posCell {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : AltV k A

The cell of the element x.

Equations

• DescriptiveComplexity.AltQbf.posCell x = DescriptiveComplexity.AltQbf.aone DescriptiveComplexity.AltQbf.AltBase.pCell x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : AltV k A

The right-marker cell.

Equations

• DescriptiveComplexity.AltQbf.posEnd = DescriptiveComplexity.AltQbf.acst DescriptiveComplexity.AltQbf.AltBase.pEnd

States

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.stG {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (i : Fin (k + 1)) (d : Bool) : AltV k A

Sweeping in direction d during the sweep of index i. The index runs over Fin (k + 1), but only the values below k are ever reached.

Equations

• DescriptiveComplexity.AltQbf.stG i d = DescriptiveComplexity.AltQbf.acstI (DescriptiveComplexity.AltQbf.AltBase.qG d) i

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.stChk {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f d : Bool) (c : A) : AltV k A

Checking the clause c, flag f, sweeping in direction d.

Equations

• DescriptiveComplexity.AltQbf.stChk f d c = DescriptiveComplexity.AltQbf.aone (DescriptiveComplexity.AltQbf.AltBase.qChk f d) c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.AltQbf.stAcc {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : AltV k A

The accepting state.

Equations

• DescriptiveComplexity.AltQbf.stAcc = DescriptiveComplexity.AltQbf.acst DescriptiveComplexity.AltQbf.AltBase.qAcc

The transition table

def DescriptiveComplexity.AltQbf.AltTr {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (τ : AltV k A) : Prop

Which tagged tuples are transitions. The payload is pinned exactly as far as the transition needs it, the sweep index is required to be a real sweep, and the clause coordinates are required to be clauses, so that no junk element is ever a transition.

Equations

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

def DescriptiveComplexity.AltQbf.AltSrc {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (τ q : AltV k A) : Prop

The state a transition applies in. The accepting turn fires at the flag cnf: set, for a conjunctive matrix, where it means the clause is satisfied; clear, for a disjunctive one, where it means no literal of the term is violated.

Equations

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

def DescriptiveComplexity.AltQbf.AltRead {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : AltV k A) : Prop

The symbol a transition reads.

Equations

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

def DescriptiveComplexity.AltQbf.AltDst {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (τ q : AltV k A) : Prop

The state a transition moves to. The only place the instance is consulted is the check clause, where the new flag depends on DescriptiveComplexity.QbfLit.

Equations

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

def DescriptiveComplexity.AltQbf.AltWrite {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : AltV k A) : Prop

The symbol a transition writes: only a guessing sweep ever changes the tape, and only from false to true.

Equations

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

def DescriptiveComplexity.AltQbf.AltRight {k : ℕ} {A : Type} (τ : AltV k A) : Prop

Which transitions move the head right: a sweep goes in its own direction, and every transition that fires at a marker moves away from it.

Equations

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

def DescriptiveComplexity.AltQbf.AltAccSt {k : ℕ} {A : Type} (q : AltV k A) : Prop

Accepting states: just DescriptiveComplexity.stAcc.

Equations

• DescriptiveComplexity.AltQbf.AltAccSt q = (q.1.1 = DescriptiveComplexity.AltQbf.AltBase.qAcc)

def DescriptiveComplexity.AltQbf.AltStartSt {k : ℕ} {A : Type} [LinearOrder A] (q : AltV k A) : Prop

Start states: the rightward sweep of index 0.

Equations

• DescriptiveComplexity.AltQbf.AltStartSt q = (q.1 = (DescriptiveComplexity.AltQbf.AltBase.qG true, 0) ∧ DescriptiveComplexity.AltQbf.IsMinTup2 q.2)

def DescriptiveComplexity.AltQbf.altBlockOf {k : ℕ} {A : Type} (q : AltV k A) : ℕ

The quantifier block an element belongs to: its sweep index for a sweeping state, the last block for the check and the accepting state, and block 0 for everything else – DescriptiveComplexity.ATMData.BlocksWellFormed asks every element for a block, junk included.

Equations

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

def DescriptiveComplexity.AltQbf.AltBlkOf {k : ℕ} {A : Type} (j : ℕ) (q : AltV k A) : Prop

The block marks of the machine.

Equations

• DescriptiveComplexity.AltQbf.AltBlkOf j q = (j = DescriptiveComplexity.AltQbf.altBlockOf q)

def DescriptiveComplexity.AltQbf.altMachine (k : ℕ) (A : Type) [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) : ATMData (AltV k A)

The alternating machine of a quantified Boolean formula.

Equations

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

The instance obligations

Everything DescriptiveComplexity.TMData.WellFormed and DescriptiveComplexity.ATMData.BlocksWellFormed ask, discharged before any run is considered.

theorem DescriptiveComplexity.AltQbf.altMachine_wellFormed {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) : (altMachine k A cnf).WellFormed

theorem DescriptiveComplexity.AltQbf.altBlockOf_lt {k : ℕ} {A : Type} (hk : 0 < k) (q : AltV k A) : altBlockOf q < k

theorem DescriptiveComplexity.AltQbf.altBlockOf_stG {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {i : Fin (k + 1)} (hi : ↑i < k) (d : Bool) : altBlockOf (stG i d) = ↑i

A sweeping state's block is its sweep index.

theorem DescriptiveComplexity.AltQbf.altBlockOf_stChk {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f d : Bool) (c : A) : altBlockOf (stChk f d c) = k - 1

theorem DescriptiveComplexity.AltQbf.altBlockOf_stAcc {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : altBlockOf stAcc = k - 1

theorem DescriptiveComplexity.AltQbf.altMachine_blocksWellFormed {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (hk : 0 < k) : (altMachine k A cnf).BlocksWellFormed k

The block structure is well formed: every element has exactly one block, a transition stays in its block or moves to the next one, and a start state is in block 0.