Evaluating quantified Boolean formulas with an explicit stack

A formula is evaluated by reading its tokens in prefix order (Cslib.Logic.PL.QBF.tokens) with an explicit stack of frames. A frame records an operator whose operands are being evaluated: its token, the value of its first operand once it has returned, and the tokens following the operator. One total step function (Cslib.Complexity.TQBF.step) either reads a token or returns a value:

• a variable, top or bot is a value: a variable takes the value given by the innermost quantifier frame over it, and clears the flag ok when there is none;
• an operator pushes a frame, and the tokens of its first operand follow it;
• a value returned into a negation is negated; a value returned into the first operand of a conjunction or disjunction is recorded, and the tokens of the second operand follow it;
• a value returned into the first pass of a quantifier over v, which ran with v false, is recorded, and the reading rewinds to the body of the quantifier for a second pass with v true;
• a value returned into the second operand or pass is combined with the first, and the frame is popped; an empty stack holding a value is a fixed point.

So the stack is the call stack of the recursive evaluation, and the environment of the recursion is read off the quantifier frames (Cslib.Complexity.TQBF.assignment): during its first pass a quantifier over v sets v to false, during its second pass to true. Every token of the formula is read at least once, so the flag records whether every variable occurrence is bound.

A call on a formula φ returns to the same stack, with the value of φ under the assignment of the stack and the flag updated by the closedness of φ relative to the stack, within Cslib.Complexity.TQBF.callSteps φ < 4 ^ φ.tokens.length steps (Cslib.Complexity.TQBF.exists_iterate_step_call). The evaluator (Cslib.Complexity.TQBF.evaluate) runs the machine from the empty stack for 2 ^ (encQBF φ).length steps and decides TQBF (Cslib.Complexity.TQBF.evaluate_eq_true_iff).

Along every run, the input is a suffix of the tokens of the formula, every frame stores a token of the formula and a suffix of its tokens, and the suffixes stored in the stack are strictly nested, so the stack is no deeper than the number of tokens (Cslib.Complexity.TQBF.Good, Cslib.Complexity.TQBF.good_iterate_step). The time and space of the evaluator on multi-tape machines are in Cslib.Computability.Complexity.Classes.Space.TQBF.Membership.

Main definitions

• Cslib.Complexity.TQBF.Frame, Cslib.Complexity.TQBF.State, Cslib.Complexity.TQBF.step: the stack machine.
• Cslib.Complexity.TQBF.assignment, Cslib.Complexity.TQBF.closedIn: the assignment of a stack, and closedness relative to a stack.
• Cslib.Complexity.TQBF.callSteps: the number of steps of a call.
• Cslib.Complexity.TQBF.evaluate: the evaluator.
• Cslib.Complexity.TQBF.Good: the invariant of the runs.

Main results

• Cslib.Complexity.TQBF.exists_iterate_step_call: every call returns its value.
• Cslib.Complexity.TQBF.evaluate_eq, Cslib.Complexity.TQBF.evaluate_eq_true_iff: the evaluator decides TQBF.
• Cslib.Complexity.TQBF.good_iterate_step, Cslib.Complexity.TQBF.Good.length_stack_le: the states of a run are small.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.9
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Theorem 4.13

The stack machine

structure Cslib.Complexity.TQBF.Frame : Type

A frame of the stack: an operator token whose operands are being evaluated, the value of its first operand (for a quantifier, of its first pass) once it has returned, and the tokens following the operator; for a quantifier, these are its body followed by the rest of the input, to which the second pass rewinds.

• token : Logic.PL.QBF.Kind × ℕ

  The operator.

• first : Option Bool

  The value of the first operand or pass, once it has returned.

• rest : List (Logic.PL.QBF.Kind × ℕ)

  The tokens following the operator.

@[instance_reducible]

instance Cslib.Complexity.TQBF.instInhabitedFrame : Inhabited Frame

structure Cslib.Complexity.TQBF.State : Type

The state of the machine.

• input : List (Logic.PL.QBF.Kind × ℕ)

  The tokens still to be read.

• stack : List Frame

  The frames of the operators in progress, the innermost first.

• value : Option Bool

  The value being returned, or none when the next token is to be read.

• ok : Bool

  Whether every variable read so far was bound by a quantifier frame.

@[instance_reducible]

instance Cslib.Complexity.TQBF.instInhabitedState : Inhabited State

def Cslib.Complexity.TQBF.Frame.binds (v : ℕ) (f : Frame) : Bool

Whether a frame is a quantifier over v.

def Cslib.Complexity.TQBF.lookup (stack : List Frame) (v : ℕ) : Option Bool

The value of v given by the innermost quantifier frame over v: false during its first pass, true during its second; none when no frame quantifies over v.

def Cslib.Complexity.TQBF.assignment (stack : List Frame) (v : ℕ) : Bool

The assignment of a stack, false on the variables it does not bind.

def Cslib.Complexity.TQBF.step (s : State) : State

One step of the evaluator. See the module docstring for the cases.

def Cslib.Complexity.TQBF.closedIn (stack : List Frame) (φ : Logic.PL.QBF ℕ) : Bool

Whether every free variable of φ is bound by a quantifier frame of the stack.

def Cslib.Complexity.TQBF.callSteps : Logic.PL.QBF ℕ → ℕ

The number of steps of a call on a formula: one step to read each token, and one step to return into each operator for each of its operands or passes.

The assignment of a stack

theorem Cslib.Complexity.TQBF.closedIn_not (stack : List Frame) (φ : Logic.PL.QBF ℕ) : closedIn stack φ.not = closedIn stack φ

Closedness of a negation.

Every call returns its value

theorem Cslib.Complexity.TQBF.exists_iterate_step_call (φ : Logic.PL.QBF ℕ) (input : List (Logic.PL.QBF.Kind × ℕ)) (stack : List Frame) (ok : Bool) : ∃ T ≤ callSteps φ, step^[T] { input := φ.tokens ++ input, stack := stack, value := none, ok := ok } = { input := input, stack := stack, value := some (Logic.PL.QBF.eval (assignment stack) φ), ok := ok && closedIn stack φ }

Every call returns its value. From the tokens of φ followed by input, the machine returns to the same stack, having read the tokens of φ, the value of φ under the assignment of the stack, and the flag updated by the closedness of φ relative to the stack, within callSteps φ steps.

theorem Cslib.Complexity.TQBF.callSteps_le (φ : Logic.PL.QBF ℕ) : callSteps φ ≤ 2 ^ (encQBF φ).length

The evaluator runs the machine long enough: 2 ^ (encQBF φ).length steps.

The evaluator

def Cslib.Complexity.TQBF.init (φ : Logic.PL.QBF ℕ) : State

The initial state on a formula: its tokens, the empty stack, nothing to return, no unbound variable met.

def Cslib.Complexity.TQBF.State.answer (s : State) : Bool

The answer held by a state: whether no unbound variable was met and the value returned is true.

def Cslib.Complexity.TQBF.evaluate (φ : Logic.PL.QBF ℕ) : Bool

The evaluator: run the machine from the initial state for 2 ^ (encQBF φ).length steps and read the answer.

theorem Cslib.Complexity.TQBF.evaluate_eq (φ : Logic.PL.QBF ℕ) : evaluate φ = (decide φ.Closed && Logic.PL.QBF.eval (fun (x : ℕ) => false) φ)

The evaluator computes closedness and the value.

theorem Cslib.Complexity.TQBF.evaluate_eq_true_iff {φ : Logic.PL.QBF ℕ} : evaluate φ = true ↔ φ ∈ TQBF

The evaluator decides TQBF.

The states of a run

def Cslib.Complexity.TQBF.Nested (n : ℕ) : ℕ → List Frame → Prop

The suffixes stored in a stack are strictly nested above a bound: the input, of length at most r, is no longer than the suffix of the top frame, which is shorter than the suffix of the frame below, and so on, and the suffix of the bottom frame is shorter than n.

theorem Cslib.Complexity.TQBF.Nested.mono {n r r' : ℕ} {stack : List Frame} : Nested n r stack → r' ≤ r → Nested n r' stack

Nesting is preserved by a shorter input.

structure Cslib.Complexity.TQBF.Good (φ : Logic.PL.QBF ℕ) (s : State) : Prop

The invariant of the runs on the formula φ: the input is a suffix of the tokens of φ, each frame stores a token of φ followed by a suffix of the tokens of φ, and the stored suffixes are nested.

• input : s.input <:+ φ.tokens

  The input is a suffix of the tokens.

• frames (f : Frame) : f ∈ s.stack → f.token :: f.rest <:+ φ.tokens

  Each frame stores a suffix of the tokens.

• nested : Nested φ.tokens.length s.input.length s.stack

  The stored suffixes are nested.

theorem Cslib.Complexity.TQBF.good_iterate_step (φ : Logic.PL.QBF ℕ) (n : ℕ) : Good φ (step^[n] (init φ))

Every state of a run satisfies the invariant.

theorem Cslib.Complexity.TQBF.Good.length_stack_le {φ : Logic.PL.QBF ℕ} {s : State} (h : Good φ s) : s.stack.length ≤ φ.tokens.length

A state satisfying the invariant has at most as many frames as the formula has tokens.