One step of the QBF machine

The transition table of DescriptiveComplexity.Problems.Machine.QsatProgram says which tuples are transitions; this file says what they do. There is one lemma per line of the program, each of the shape

in this state, at this cell, reading this symbol, the machine steps to that state, that cell, and that tape

with the movement supplied as a DescriptiveComplexity.SuccPos hypothesis, so that the boundary cases – the outermost variable, the innermost one, the degenerate instance with no variable at all – are handled by passing a different lemma of DescriptiveComplexity.Problems.Machine.QsatGeom rather than by duplicating each line of the program.

The tape after a step is never built here either: it is an arbitrary σ' required to hold the written symbol at the head and to agree with σ everywhere else, which is exactly what DescriptiveComplexity.TMData.Step asks and what the run induction will supply.

@[reducible, inline]

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

The marker a sweep in direction d ends at, as a position.

Equations

• DescriptiveComplexity.QsatTM.markerPos d = if d = true then DescriptiveComplexity.QsatTM.posEnd else DescriptiveComplexity.QsatTM.posStart

Descending

Evaluating the matrix

Carrying the value to the right marker

Returning through the prefix

The initial configuration

Where the machine starts: descending, at the left marker, on the tape the instance prescribes. Every cell of the tape carries a symbol – the markers their own, a variable's cell the value false with the flag down – so the blank is never read, and it is only there because DescriptiveComplexity.TMData.InitTape needs a default for the tuples that are not cells at all.

noncomputable def DescriptiveComplexity.QsatTM.initTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (p : QV A) : QV A

The tape the machine starts on. It depends on the tag and on the first coordinate alone, which is what makes it agree with DescriptiveComplexity.QsatTM.QInp at every tuple, junk included.

Equations

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

@[simp]

theorem DescriptiveComplexity.QsatTM.initTape_posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : initTape posStart = symStart

The starting tape, read at the left marker.

@[simp]

theorem DescriptiveComplexity.QsatTM.initTape_posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : initTape posEnd = symEnd

The starting tape, read at the right marker.

@[simp]

theorem DescriptiveComplexity.QsatTM.initTape_posCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : initTape (posCell x) = symV false false x

The starting tape, read at a variable's cell.

Where the machine stops

The two dead ends, both of them facts about the table alone: nothing follows an accepting configuration, and nothing follows a false returned past the outermost quantifier. They are exactly the side conditions of DescriptiveComplexity.TMData.not_acceptsSpace_of_reaches_dead, which is what turns one exhibited run into non-acceptance for a no-instance.