The machine of a quantified Boolean formula

The program half of QSAT ≤ᶠᵒ[≤] DTMAcceptSpace: the states, symbols and transitions of the machine built inside a QSAT instance, on the tape laid out in DescriptiveComplexity.Problems.Machine.QsatTape.

The program

Iterative evaluation of a quantified Boolean formula. The recursion stack is not a stack: each variable's own cell carries its current value b together with a bit f recording that both values have already been tried, which is all the standard algorithm needs.

  Desc      ⊢ → at each cell write (0,0), moving right → ⊣, then evaluate
  Eval f d c  sweep in direction d accumulating f := f ∨ QLit c x b;
              at the marker: ¬f → the matrix is false;
                             f and c has a successor → next clause, turn round;
                             f and c is the last → the matrix is true
  ToEnd b   walk right to ⊣, turn round, and return the value b
  Proc b    at the innermost unfinished variable x:
              the level is decided (∃ and b, or ∀ and ¬b, or f already set)
                                            → move left, keep returning b
              otherwise                     → write (1,1), move right, Desc
            at ⊢: b → accept; ¬b → no transition, the run dies

The machine is deterministic, which is the whole point: DTMAcceptSpace folds DescriptiveComplexity.TMData.Deterministic into its yes-instances, and a deterministic run is also what makes the converse half of correctness free (Relation.ReflTransGen.total_of_right_unique).

Malformed instances

DescriptiveComplexity.QsatHolds requires DescriptiveComplexity.QsatWf, so an instance whose prefix order is not a strict linear order on the marked variables must map to a machine that cannot accept. That is arranged by a guard on the accepting predicate (DescriptiveComplexity.QsatTM.QAcc) rather than by the tape order, which would not catch every violation.

Semantics first

As in DescriptiveComplexity.Problems.Machine.Hardness, everything here is a plain predicate on tagged tuples: the machine is assembled as a DescriptiveComplexity.TMData and reasoned about directly, and only later transcribed into defining formulas. A transition table type-checks whatever it says, so it has to be validated by proofs – which is what the second half of this file is.

The instance, read

def DescriptiveComplexity.QsatTM.QCl {A : Type} [FirstOrder.Language.qsat.Structure A] (c : A) : Prop

Being a clause of the matrix.

Equations

• DescriptiveComplexity.QsatTM.QCl c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsIsClause ![c]

def DescriptiveComplexity.QsatTM.QPosIn {A : Type} [FirstOrder.Language.qsat.Structure A] (c x : A) : Prop

The variable x occurs positively in the clause c.

Equations

• DescriptiveComplexity.QsatTM.QPosIn c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsPosIn ![c, x]

def DescriptiveComplexity.QsatTM.QNegIn {A : Type} [FirstOrder.Language.qsat.Structure A] (c x : A) : Prop

The variable x occurs negatively in the clause c.

Equations

• DescriptiveComplexity.QsatTM.QNegIn c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsNegIn ![c, x]

def DescriptiveComplexity.QsatTM.QLit {A : Type} [FirstOrder.Language.qsat.Structure A] (c x : A) (b : Bool) : Prop

The literal test: the cell of x, holding the truth value b, satisfies the clause c. This is the first-order test on the source structure that the evaluation sweep performs.

Equations

• DescriptiveComplexity.QsatTM.QLit c x b = (DescriptiveComplexity.QsatTM.QPosIn c x ∧ b = true ∨ DescriptiveComplexity.QsatTM.QNegIn c x ∧ b = false)

def DescriptiveComplexity.QsatTM.QMinCl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (c : A) : Prop

c is the lowest clause in the ambient order.

Equations

• DescriptiveComplexity.QsatTM.QMinCl c = (DescriptiveComplexity.QsatTM.QCl c ∧ ∀ (e : A), DescriptiveComplexity.QsatTM.QCl e → c ≤ e)

def DescriptiveComplexity.QsatTM.QMaxCl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (c : A) : Prop

c is the highest clause in the ambient order.

Equations

• DescriptiveComplexity.QsatTM.QMaxCl c = (DescriptiveComplexity.QsatTM.QCl c ∧ ∀ (e : A), DescriptiveComplexity.QsatTM.QCl e → e ≤ c)

def DescriptiveComplexity.QsatTM.QNextCl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (c c' : A) : Prop

c' is the clause immediately above c.

Equations

• DescriptiveComplexity.QsatTM.QNextCl c c' = (DescriptiveComplexity.QsatTM.QCl c ∧ DescriptiveComplexity.QsatTM.QCl c' ∧ c < c' ∧ ∀ (e : A), DescriptiveComplexity.QsatTM.QCl e → c < e → c' ≤ e)

def DescriptiveComplexity.QsatTM.QShort {A : Type} [FirstOrder.Language.qsat.Structure A] (v : Bool) (x : A) : Prop

The level is already decided: a returning value v settles the quantifier at x on its own – an existential level reached by a winning branch, a universal one by a losing branch.

Equations

• DescriptiveComplexity.QsatTM.QShort v x = (DescriptiveComplexity.IsQAll x ∧ v = false ∨ ¬DescriptiveComplexity.IsQAll x ∧ v = true)

The elements of the machine

noncomputable def DescriptiveComplexity.QsatTM.qBot {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.QsatTM.qBot = ⋯.choose

theorem DescriptiveComplexity.QsatTM.qBot_le {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) : qBot ≤ a

theorem DescriptiveComplexity.QsatTM.isMinTup_qBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : IsMinTup fun (x : Fin 2) => qBot

noncomputable def DescriptiveComplexity.QsatTM.qCst {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : QTag) : QV A

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

Equations

• DescriptiveComplexity.QsatTM.qCst t = (t, fun (x : Fin 2) => DescriptiveComplexity.QsatTM.qBot)

noncomputable def DescriptiveComplexity.QsatTM.qOne {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : QTag) (a : A) : QV A

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

Equations

• DescriptiveComplexity.QsatTM.qOne t a = (t, ![a, DescriptiveComplexity.QsatTM.qBot])

Symbols

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.symStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : QV A

The left-marker symbol.

Equations

• DescriptiveComplexity.QsatTM.symStart = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.sStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.symEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : QV A

The right-marker symbol.

Equations

• DescriptiveComplexity.QsatTM.symEnd = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.sEnd

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.symV {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (b f : Bool) (x : A) : QV A

The symbol of the cell of x: value b, flag f.

Equations

• DescriptiveComplexity.QsatTM.symV b f x = DescriptiveComplexity.QsatTM.qOne (DescriptiveComplexity.QsatTM.QTag.sVal b f) x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.markerSym {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (d : Bool) : QV A

The marker a sweep in direction d ends at.

Equations

• DescriptiveComplexity.QsatTM.markerSym d = if d = true then DescriptiveComplexity.QsatTM.symEnd else DescriptiveComplexity.QsatTM.symStart

Positions

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : QV A

The left-marker cell.

Equations

• DescriptiveComplexity.QsatTM.posStart = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.pStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.posCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : QV A

The cell of the variable x.

Equations

• DescriptiveComplexity.QsatTM.posCell x = DescriptiveComplexity.QsatTM.qOne DescriptiveComplexity.QsatTM.QTag.pCell x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : QV A

The right-marker cell.

Equations

• DescriptiveComplexity.QsatTM.posEnd = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.pEnd

States

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stDesc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : QV A

Descending: initializing the cells to the right.

Equations

• DescriptiveComplexity.QsatTM.stDesc = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.qDesc

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stEval {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f d : Bool) (c : A) : QV A

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

Equations

• DescriptiveComplexity.QsatTM.stEval f d c = DescriptiveComplexity.QsatTM.qOne (DescriptiveComplexity.QsatTM.QTag.qEval f d) c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stToEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (b : Bool) : QV A

Carrying the value b to the right marker.

Equations

• DescriptiveComplexity.QsatTM.stToEnd b = DescriptiveComplexity.QsatTM.qCst (DescriptiveComplexity.QsatTM.QTag.qToEnd b)

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stProc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (b : Bool) : QV A

Returning the value b through the prefix.

Equations

• DescriptiveComplexity.QsatTM.stProc b = DescriptiveComplexity.QsatTM.qCst (DescriptiveComplexity.QsatTM.QTag.qProc b)

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stAcc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : QV A

The accepting state.

Equations

• DescriptiveComplexity.QsatTM.stAcc = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.qAcc

The transition table

def DescriptiveComplexity.QsatTM.IsMin1 {A : Type} [LinearOrder A] (p : QV A) : Prop

The second coordinate of a tuple is the least element: the padding of the tags that carry a single element.

Equations

• DescriptiveComplexity.QsatTM.IsMin1 p = ∀ (a : A), p.2 1 ≤ a

def DescriptiveComplexity.QsatTM.QTr {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (τ : QV A) : Prop

Which tagged tuples are transitions. The payload is pinned exactly as far as the transition needs it.

Equations

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

def DescriptiveComplexity.QsatTM.QSrc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ q : QV A) : Prop

The state a transition applies in.

Equations

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

def DescriptiveComplexity.QsatTM.QRead {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : QV A) : Prop

The symbol a transition reads.

Equations

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

def DescriptiveComplexity.QsatTM.QDst {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ q : QV A) : Prop

The state a transition moves to. The only place the instance is consulted is the evaluation sweep, where the new flag depends on DescriptiveComplexity.QsatTM.QLit.

Equations

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

def DescriptiveComplexity.QsatTM.QWrite {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : QV A) : Prop

The symbol a transition writes: the descent resets a cell, the switch sets the second value with the flag up, and everything else leaves the tape as it found it.

Equations

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

def DescriptiveComplexity.QsatTM.QRight {A : Type} (τ : QV A) : Prop

Which transitions move the head right: the descent and the carry always do, a sweep goes in its own direction, a turn reverses, and the return walks leftwards.

Equations

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

def DescriptiveComplexity.QsatTM.QAcc {A : Type} [FirstOrder.Language.qsat.Structure A] (q : QV A) : Prop

Accepting states, guarded by well-formedness of the instance: a malformed instance is a no-instance of QSAT, and its machine has no accepting state at all.

Equations

• DescriptiveComplexity.QsatTM.QAcc q = (DescriptiveComplexity.QsatWf A ∧ q.1 = DescriptiveComplexity.QsatTM.QTag.qAcc)

def DescriptiveComplexity.QsatTM.QStart {A : Type} [LinearOrder A] (q : QV A) : Prop

Start states: just DescriptiveComplexity.QsatTM.stDesc.

Equations

• DescriptiveComplexity.QsatTM.QStart q = (q.1 = DescriptiveComplexity.QsatTM.QTag.qDesc ∧ DescriptiveComplexity.IsMinTup q.2)

def DescriptiveComplexity.QsatTM.qsatMachine (A : Type) [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : TMData (QV A)

The machine of a quantified Boolean formula.

Equations

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

The table is a table

Before any run is considered: each transition has exactly one destination and symbol written, and the state together with the symbol read pins the transition. A mistake in the table shows up here first, which is why these come before the correctness proof.

theorem DescriptiveComplexity.QsatTM.qOne_eq_qOne_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : QTag} {a a' : A} : qOne t a = qOne t' a' ↔ t = t' ∧ a = a'

The tag of a transition, seen from the state and the symbol