Documentation

DescriptiveComplexity.Problems.Machine.AltTape

The tape of the alternating QBF machine #

The layout half of QBF k ≤ᶠᵒ[≤] ATMAccept k: which tagged tuples are positions, in what order they sit, and why there are enough of them. It is the tape of DescriptiveComplexity.Problems.Machine.Tape with the guessing phase split into k sweeps.

The layout #

  ⊢   x₁ x₂ … xₙ   ⊣   fillers…

one cell per element, bracketed by two markers, then filler cells that exist only to supply time – exactly as for the SAT machine. What changes is the symbol in a cell and the number of tags.

A cell holds a truth value, not an “unassigned” mark. The value of a variable under a tuple of block assignments is DescriptiveComplexity.qbfVal, which is a disjunction: x is true when some block marking it assigns it true. A variable may carry several block marks, or none. So the cell of x starts at false and sweep i may turn it to true; after all k sweeps it holds the disjunction, and a variable no block marks stays false – which is what qbfVal says about it. Monotone accumulation is what makes one bit per cell enough.

The tags, and why the order is by key #

The SAT machine numbers its tags by hand. Here the families are indexed by k, so the numbering is a pair – a family index and an offset inside the family – ordered lexicographically (DescriptiveComplexity.altTagKey). The position families come first, so the order of the positions is undisturbed by the program's tags, exactly as DescriptiveComplexity.satTagIdx arranges.

The Fin (k + 1) every tag carries is the price of one sweep per block, and the alternative is worth recording because it looks cheaper and is not: a single sweep, with the cells ordered by (block of the variable, variable), so that the state's block is read off the variable under the head. It removes the Fin (k + 1) from the tags and puts a bespoke linear order on the interpreted universe in its place – DescriptiveComplexity.isLinOrd_altTagTupleLe no longer applies – and DescriptiveComplexity.QBF promises nothing about its marks, so the sort key must still invent a k-th class for the unmarked variables. Not taken.

The budget #

Each of the k sweeps goes right and comes back, so 2k(n + 2) steps, and the check costs (m + 1)(n + 2) for m ≤ n clauses: at most (2k + n + 1)(n + 2). The 8(k + 1) filler tags at dimension two supply 8(k + 1)n² positions on their own, and DescriptiveComplexity.alt_budget says that is always more – the filler is over-provisioned rather than the bound tightened, as in DescriptiveComplexity.sat_budget.

The tags of the positions #

inductive DescriptiveComplexity.AltQbf.AltBase :

The base tags of the alternating QBF machine: everything but the sweep index, which a tag carries alongside. Keeping this type independent of k is what makes its numbering – and hence the tape order – a decide.

pStart : AltBase
The left marker cell.
pCell : AltBase
The cell of an element: one per element of the instance.
pEnd : AltBase
The right marker cell.
pFill (i : Fin 8) : AltBase
Filler cells, eight base tags' worth, each with k + 1 sweep indices.
sStart : AltBase
The left-marker symbol ⊢.
sEnd : AltBase
The right-marker symbol ⊣.
sBlank : AltBase
The blank symbol.
sVal (b : Bool) : AltBase
The symbol (x, b): the cell of x, currently holding the truth value b.
qG (d : Bool) : AltBase
A guessing sweep, sweeping in direction d (true = rightwards); which sweep is the tag's index.
qChk (f d : Bool) : AltBase
Checking a clause with the accumulated flag f, sweeping in direction d.
qAcc : AltBase
The accepting state.
tGStart : AltBase
A sweep: step over the left marker, rightwards.
tGKeep (b : Bool) : AltBase
A sweep, rightwards: leave a cell holding b alone.
tGSet : AltBase
A sweep, rightwards: turn a cell of a variable this block marks from false to true.
tGTurn : AltBase
A sweep: turn round at the right marker.
tGBack (b : Bool) : AltBase
A sweep, leftwards: step back over a cell holding b.
tGNext : AltBase
A sweep: at the left marker, hand over to the next sweep.
tGEndAcc : AltBase
The last sweep is over and there is no clause: accept.
tGEndChk : AltBase
The last sweep is over: start checking the lowest clause.
tChk (b f d : Bool) : AltBase
Check phase: read (x, b) with flag f, sweeping in direction d.
tTurnNext (d : Bool) : AltBase
Check phase: the clause is settled and another one follows.
tTurnAcc (d : Bool) : AltBase
Check phase: the clause is settled and it was the last one.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.AltQbf.instDecidableEqAltBase :

DecidableEq AltBase

Equations

DescriptiveComplexity.AltQbf.instDecidableEqAltBase = DescriptiveComplexity.AltQbf.instDecidableEqAltBase.decEq

Dependency graph

def DescriptiveComplexity.AltQbf.instDecidableEqAltBase.decEq (x✝ x✝¹ : AltBase) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.AltQbf.instFintypeAltBase :

Fintype AltBase

Equations

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

Dependency graph

instance DescriptiveComplexity.AltQbf.instNonemptyAltBase :

Nonempty AltBase

Dependency graph

def DescriptiveComplexity.AltQbf.altBaseIdx :

AltBase → ℕ

The position of a base tag in the tape order.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.altBaseIdx_injective :

Function.Injective altBaseIdx

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.AltQbf.AltTag (k : ℕ) :

The tags of the tape: a base tag together with a sweep index. The index is the sweep a guessing state or transition belongs to, and the second coordinate of a filler cell; everywhere else it is pinned to 0 by DescriptiveComplexity.AltPosn and the machine's own definitions.

Equations

DescriptiveComplexity.AltQbf.AltTag k = (DescriptiveComplexity.AltQbf.AltBase × Fin (k + 1))

Instances For

Dependency graph

def DescriptiveComplexity.AltQbf.altTagKey {k : ℕ} (t : AltTag k) :

Lex (ℕ × ℕ)

The sort key of a tag: the base tag, then the sweep index.

Equations

DescriptiveComplexity.AltQbf.altTagKey t = toLex (DescriptiveComplexity.AltQbf.altBaseIdx t.1, ↑t.2)

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.altTagKey_injective {k : ℕ} :

Function.Injective altTagKey

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.AltQbf.instLinearOrderAltTag (k : ℕ) :

LinearOrder (AltTag k)

The tape order on tags: the base tag first, then the sweep index. The position families come first, so the program's tags never disturb the order of the positions.

Equations

DescriptiveComplexity.AltQbf.instLinearOrderAltTag k = LinearOrder.lift' DescriptiveComplexity.AltQbf.altTagKey ⋯

Dependency graph

The intended positions #

def DescriptiveComplexity.AltQbf.AltPosn {k : ℕ} {A : Type} [LinearOrder A] (p : AltTag k × (Fin 2 → A)) :

The tagged tuples that are positions: the two markers are the single tuple of minima, an element's cell is that element in the first coordinate, and the fillers are unrestricted.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.AltQbf.IsMinTup2 {A : Type} [LinearOrder A] (w : Fin 2 → A) :

The tuple of minima: the coordinates a marker or a constant symbol is pinned to, so that exactly one tuple carries such a tag.

Equations

DescriptiveComplexity.AltQbf.IsMinTup2 w = ((∀ (a : A), w 0 ≤ a) ∧ ∀ (a : A), w 1 ≤ a)

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.isMinTup2_unique {A : Type} [LinearOrder A] {w w' : Fin 2 → A} (h : IsMinTup2 w) (h' : IsMinTup2 w') :

w = w'

Dependency graph

theorem DescriptiveComplexity.AltQbf.exists_isMinTup2 {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

∃ (w : Fin 2 → A), IsMinTup2 w

Dependency graph

def DescriptiveComplexity.AltQbf.AltBlank {k : ℕ} {A : Type} [LinearOrder A] (p : AltTag k × (Fin 2 → A)) :

The blank symbol: one element, pinned to the tuple of minima.

Equations

DescriptiveComplexity.AltQbf.AltBlank p = (p.1 = (DescriptiveComplexity.AltQbf.AltBase.sBlank , 0) ∧ DescriptiveComplexity.AltQbf.IsMinTup2 p.2)

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.exists_altBlank {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

∃ (p : AltTag k × (Fin 2 → A)), AltBlank p

Dependency graph

theorem DescriptiveComplexity.AltQbf.altBlank_unique {k : ℕ} {A : Type} [LinearOrder A] {p q : AltTag k × (Fin 2 → A)} (hp : AltBlank p) (hq : AltBlank q) :

p = q

Dependency graph

def DescriptiveComplexity.AltQbf.AltInp {k : ℕ} {A : Type} [LinearOrder A] (p a : AltTag k × (Fin 2 → A)) :

The initial tape: the markers hold their own symbols and the cell of an element holds that element with the truth value false – no block has assigned anything yet. The fillers hold the blank.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.altInp_functional {k : ℕ} {A : Type} [LinearOrder A] {p a b : AltTag k × (Fin 2 → A)} (ha : AltInp p a) (hb : AltInp p b) :

a = b

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

Dependency graph

theorem DescriptiveComplexity.AltQbf.exists_altPosn {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

∃ (p : AltTag k × (Fin 2 → A)), AltPosn p

There is a position: the start marker.

Dependency graph

theorem DescriptiveComplexity.AltQbf.isLinOrd_altTagTupleLe {k : ℕ} {A : Type} [LinearOrder A] :

IsLinOrd tagTupleLe

The interpreted order is linear, from DescriptiveComplexity.tagTupleOrder.

Dependency graph

The budget #

theorem DescriptiveComplexity.AltQbf.alt_budget {k n m : ℕ} (hn : 1 ≤ n) (hm : m ≤ n) :

(2 * k + m + 1) * (n + 2) < 8 * (k + 1) * n * n

The filler cells alone are enough. The k sweeps cost 2k(n + 2) steps, the check (m + 1)(n + 2) for m ≤ n clauses, and the 8(k + 1) filler tags contribute 8(k + 1)n² positions by themselves.

The inequality is strict, as DescriptiveComplexity.TMData.Accepts requires.

Dependency graph

theorem DescriptiveComplexity.AltQbf.alt_card_le_card_posn (k : ℕ) (A : Type) [LinearOrder A] [Finite A] :

8 * (k + 1) * Nat.card A * Nat.card A ≤ Nat.card { p : AltTag k × (Fin 2 → A) // AltPosn p }

The tape really has that many positions: the filler tuples alone inject into the positions.

Dependency graph