The tape of the QBF machine

The layout half of QSAT ≤ᶠᵒ[≤] DTMAcceptSpace: which tagged tuples are positions, in what order they sit, and what the tape holds to begin with. The program that runs on this tape – states, symbols, transitions – is separate.

The layout

One cell per quantified variable, bracketed by two markers:

  ⊢   v₁ v₂ … vₙ   ⊣

There are no filler cells: DescriptiveComplexity.TMData.AcceptsSpace has no step bound, so unlike the tape of DescriptiveComplexity.Problems.Machine.Tape this one needs to supply space only, and the space it must supply is one bit of value and one bit of “both values already tried” per variable – the stack of the recursive evaluation of a quantified Boolean formula, held in the variables' own cells.

The order is the quantifier prefix

The head walks the variables in the order the quantifiers bind them, so the tape order cannot be the ambient one. DescriptiveComplexity.QsatTM.PLe puts the quantified variables first, in prefix order, and everything else after them in the ambient order; it is a linear order on the universe exactly when the instance is well formed (DescriptiveComplexity.QsatWf), and DescriptiveComplexity.QsatTM.QLe is the lexicographic order built from it – tag index first, then the two coordinates.

Malformed instances are not handled by the order: they are handled by a guard on the accepting predicate, in the program file. QsatWf is first-order, and DescriptiveComplexity.QsatHolds requires it, so an instance violating it must map to a machine that cannot accept – which a guard achieves and a broken order would not (an instance whose prefix order relates a non-variable still has a linear PLe).

The tags

inductive DescriptiveComplexity.QsatTM.QTag : Type

The tags of the QBF machine. Positions come first, so that the tape order is the order of their indices; symbols, states and transitions follow.

• pStart : QTag

  The left marker cell.

• pCell : QTag

  The cell of a quantified variable.

• pEnd : QTag

  The right marker cell.

• sStart : QTag

  The left-marker symbol ⊢.

• sEnd : QTag

  The right-marker symbol ⊣.

• sBlank : QTag

  The blank symbol.

• sVal (b f : Bool) : QTag

  The symbol of a variable's cell: value b, and f recording that both values have already been tried.

• qDesc : QTag

  Descending into the subtree: initialise the cells to the right.

• qEval (f d : Bool) : QTag

  Evaluating the matrix: the clause is carried by the state, f is the accumulated flag and d the sweep direction (true = rightwards).

• qToEnd (b : Bool) : QTag

  Carrying the value b back to the right marker.

• qProc (b : Bool) : QTag

  Returning the value b through the quantifier prefix.

• qAcc : QTag

  The accepting state, a sink.

• tDescStart : QTag

  Descend: step over the left marker.

• tDescCell (b f : Bool) : QTag

  Descend: initialise a variable's cell, reading (b, f).

• tDescEndTrue : QTag

  Descend over, and the matrix has no clause: it is true.

• tDescEndEval : QTag

  Descend over: start evaluating the lowest clause.

• tEval (b f fl d : Bool) : QTag

  Evaluate: read (b, f) at a cell, with flag fl, sweeping in direction d.

• tTurnNext (d : Bool) : QTag

  Evaluate: the clause is satisfied and another one follows.

• tTurnLast (d : Bool) : QTag

  Evaluate: the clause is satisfied and it was the last one.

• tTurnFalse (d : Bool) : QTag

  Evaluate: the clause is not satisfied, so the matrix is false.

• tToEndCell (v b f : Bool) : QTag

  Carry: step over a variable's cell, reading (b, f).

• tToEndStart (v : Bool) : QTag

  Carry: step over the left marker.

• tToEndTurn (v : Bool) : QTag

  Carry: the right marker is reached, turn round and return.

• tProcSkip (v b f : Bool) : QTag

  Return: this level is decided, pass the value on.

• tProcSwitch (v b f : Bool) : QTag

  Return: this level must try its second value.

• tProcAcc : QTag

  Return: the prefix is exhausted and the value is true.

def DescriptiveComplexity.QsatTM.instDecidableEqQTag.decEq (x✝ x✝¹ : QTag) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.QsatTM.instDecidableEqQTag : DecidableEq QTag

Equations

• DescriptiveComplexity.QsatTM.instDecidableEqQTag = DescriptiveComplexity.QsatTM.instDecidableEqQTag.decEq

@[instance_reducible]

instance DescriptiveComplexity.QsatTM.instFintypeQTag : Fintype QTag

Equations

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

instance DescriptiveComplexity.QsatTM.instNonemptyQTag : Nonempty QTag

def DescriptiveComplexity.QsatTM.qTagIdx : QTag → ℕ

The index of a tag: the tape order on the position tags, and an arbitrary injective numbering of the rest.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.pStart = 0
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.pCell = 1
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.pEnd = 2
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.sStart = 3
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.sEnd = 4
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.sBlank = 5
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.sVal a a_1) = (6 + if a = true then 1 else 0) + if a_1 = true then 2 else 0
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.qDesc = 10
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.qEval a a_1) = (11 + if a = true then 1 else 0) + if a_1 = true then 2 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.qToEnd a) = 15 + if a = true then 1 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.qProc a) = 17 + if a = true then 1 else 0
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.qAcc = 19
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.tDescStart = 20
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tDescCell a a_1) = (21 + if a = true then 1 else 0) + if a_1 = true then 2 else 0
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.tDescEndTrue = 25
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.tDescEndEval = 26
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tTurnNext a) = 43 + if a = true then 1 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tTurnLast a) = 45 + if a = true then 1 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tTurnFalse a) = 47 + if a = true then 1 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tToEndCell a a_1 a_2) = ((49 + if a = true then 1 else 0) + if a_1 = true then 2 else 0) + if a_2 = true then 4 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tToEndStart a) = 57 + if a = true then 1 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tToEndTurn a) = 59 + if a = true then 1 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tProcSkip a a_1 a_2) = ((61 + if a = true then 1 else 0) + if a_1 = true then 2 else 0) + if a_2 = true then 4 else 0
• DescriptiveComplexity.QsatTM.qTagIdx (DescriptiveComplexity.QsatTM.QTag.tProcSwitch a a_1 a_2) = ((69 + if a = true then 1 else 0) + if a_1 = true then 2 else 0) + if a_2 = true then 4 else 0
• DescriptiveComplexity.QsatTM.qTagIdx DescriptiveComplexity.QsatTM.QTag.tProcAcc = 77

theorem DescriptiveComplexity.QsatTM.qTagIdx_injective : Function.Injective qTagIdx

The prefix order, as an order on the universe

The quantified variables come first, in the order the prefix binds them; every other element comes after, in the ambient order.

def DescriptiveComplexity.QsatTM.PLe {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (x y : A) : Prop

The tape order on elements: quantified variables first in prefix order, the rest afterwards in the ambient order.

Equations

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

theorem DescriptiveComplexity.QsatTM.isLinOrd_pLe (A : Type) [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (hwf : QsatWf A) : IsLinOrd PLe

The tape order is a linear order on a well-formed instance.

The order on the universe

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.QV (A : Type) : Type

The universe of the QBF machine: tagged pairs.

Equations

• DescriptiveComplexity.QsatTM.QV A = (DescriptiveComplexity.QsatTM.QTag × (Fin 2 → A))

def DescriptiveComplexity.QsatTM.QTupLe {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (u v : Fin 2 → A) : Prop

The tape order on tuples: lexicographic in DescriptiveComplexity.QsatTM.PLe.

Equations

• DescriptiveComplexity.QsatTM.QTupLe u v = (DescriptiveComplexity.QsatTM.PLe (u 0) (v 0) ∧ u 0 ≠ v 0 ∨ u 0 = v 0 ∧ DescriptiveComplexity.QsatTM.PLe (u 1) (v 1))

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

The tape order: tag index first, then the tuple lexicographically.

Equations

• DescriptiveComplexity.QsatTM.QLe p q = (DescriptiveComplexity.QsatTM.qTagIdx p.1 < DescriptiveComplexity.QsatTM.qTagIdx q.1 ∨ p.1 = q.1 ∧ DescriptiveComplexity.QsatTM.QTupLe p.2 q.2)

theorem DescriptiveComplexity.QsatTM.isLinOrd_qLe (A : Type) [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (hwf : QsatWf A) : IsLinOrd QLe

The tape order is linear on a well-formed instance.

Positions, blank and the initial tape

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

The tagged tuples that are positions: the two markers, pinned to the tuple of ambient minima, and one cell per quantified variable.

Equations

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

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

The blank symbol, pinned to the tuple of ambient minima. It is never read: every cell of the initial tape carries a symbol.

Equations

• DescriptiveComplexity.QsatTM.QBlank p = (p.1 = DescriptiveComplexity.QsatTM.QTag.sBlank ∧ DescriptiveComplexity.IsMinTup p.2)

theorem DescriptiveComplexity.QsatTM.exists_qBlank {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : ∃ (p : QV A), QBlank p

theorem DescriptiveComplexity.QsatTM.qBlank_unique {A : Type} [LinearOrder A] {p q : QV A} (hp : QBlank p) (hq : QBlank q) : p = q

theorem DescriptiveComplexity.QsatTM.exists_qPosn {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ∃ (p : QV A), QPosn p

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

The initial tape: the markers hold their own symbols, and a variable's cell holds the value false with the flag down.

Equations

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

theorem DescriptiveComplexity.QsatTM.qInp_functional {A : Type} [LinearOrder A] {p a b : QV A} (ha : QInp p a) (hb : QInp p b) : a = b

The initial tape is functional: a cell holds at most one symbol.