Closedness of a quantified Boolean formula in polynomial time

The free variables of a formula are computed by one scan of its tokens from right to left, with a stack holding the free variables of the subformulas read so far (Cslib.Logic.PL.QBF.freeVarStep): a variable pushes itself, a constant pushes nothing, a binary connective joins the two lists on top of the stack, and a quantifier removes its variable from the list on top. On the tokens of a formula the scan ends with the list of its free variables (Cslib.Logic.PL.QBF.foldl_freeVarStep_tokens), so a formula is closed exactly when that list is empty (Cslib.Logic.PL.QBF.isClosed_tokens), and closedness is decided in polynomial time (Cslib.Complexity.TQBF.computableInPolyTime_decide_closed).

Main definitions

• Cslib.Logic.PL.QBF.freeVarList: the free variables of a formula, with multiplicity.
• Cslib.Logic.PL.QBF.freeVarStep, Cslib.Logic.PL.QBF.isClosed: the scan of the tokens.

Main results

• Cslib.Logic.PL.QBF.mem_freeVarList: the list has the free variables as elements.
• Cslib.Logic.PL.QBF.isClosed_tokens: the scan decides closedness.
• Cslib.Complexity.TQBF.computableInPolyTime_decide_closed: in polynomial time.

Free variables by a scan of the tokens

def Cslib.Logic.PL.QBF.freeVarList : QBF ℕ → List ℕ

The free variables of a formula, with multiplicity.

theorem Cslib.Logic.PL.QBF.mem_freeVarList {φ : QBF ℕ} {x : ℕ} : x ∈ φ.freeVarList ↔ x ∈ φ.freeVars

The elements of freeVarList φ are the free variables of φ.

theorem Cslib.Logic.PL.QBF.closed_iff_freeVarList_eq_nil {φ : QBF ℕ} : φ.Closed ↔ φ.freeVarList = []

A formula is closed exactly when its list of free variables is empty.

def Cslib.Logic.PL.QBF.freeVarStepAt : Kind → ℕ → List (List ℕ) → List (List ℕ)

One step of the scan of the tokens from right to left, for a token of kind k and variable v, on the stack of the lists of free variables of the subformulas read so far.

def Cslib.Logic.PL.QBF.freeVarStep (stack : List (List ℕ)) (t : Kind × ℕ) : List (List ℕ)

One step of the scan of the tokens from right to left.

theorem Cslib.Logic.PL.QBF.foldl_freeVarStep_tokens (φ : QBF ℕ) (stack : List (List ℕ)) : List.foldl freeVarStep stack φ.tokens.reverse = φ.freeVarList :: stack

The scan of the tokens of a formula pushes the list of its free variables.

def Cslib.Logic.PL.QBF.isClosed (tokens : List (Kind × ℕ)) : Bool

Whether the scan of a list of tokens finds no free variable.

theorem Cslib.Logic.PL.QBF.isClosed_tokens (φ : QBF ℕ) : isClosed φ.tokens = decide φ.Closed

The scan decides closedness.

theorem Cslib.Complexity.TQBF.computableInPolyTime_decide_closed : Turing.MultiTapeTM.ComputableInPolyTime (fun (φ : Logic.PL.QBF ℕ) => decide φ.Closed) encQBF Turing.MultiTapeTM.encBool

Closedness is decided in polynomial time.