The reduction to TQBF in polynomial time

A formula is encoded by the list of its tokens in prefix order (Cslib.Complexity.encQBF), so a formula is computed in polynomial time as soon as its tokens are (Cslib.Complexity.TQBF.computableTidilyInPolyTime_of_tokens). The connectives of Cslib.Logic.PL.QBF and the derived connectives of the midpoint formulas (blocks of quantifiers, conjunctions of lists, implication, equivalence, literals, formulas in conjunctive normal form) get composition rules for fun_prop, with their tokens written out explicitly (Cslib.Logic.PL.QBF.tokens_exs, Cslib.Logic.PL.QBF.tokens_conj, …).

The variables of the blocks are numbered by 2 * Nat.pair (3 * i + kind) j for a level i and an index j below the width w, so they are computed in unary, where their size is polynomial in w, and converted to binary. The midpoint formula of level d is computed from its tokens (Cslib.Complexity.TQBF.tokens_midpoint): the levels from d down to 1, each with O(w) tokens, then the formula of level 0. So Savitch's formula is polynomial-time in the width and depth in unary, the two words, and the formula of level 0 (Cslib.Complexity.TQBF.computableTidilyInPolyTime_savitchFormula).

The formula of level 0 numbers the variables of a Cook–Levin tableau by odd numbers (Cslib.Complexity.TQBF.computableTidilyInPolyTime_tabVar), and is polynomial-time in the tableau. Composed with the polynomial-time width and codes of the views (Turing.MultiTapeNTM.computableTidilyInPolyTime_codeWidth) and the polynomial-time Cook–Levin tableau (Cslib.Complexity.CookLevin.computableTidilyInPolyTime_tableau), the reduction Cslib.Complexity.TQBF.reduce is polynomial-time, for every machine standing for the test of one step or none and every polynomial time bound (Cslib.Complexity.TQBF.computableTidilyInPolyTime_reduce). That test is itself polynomial-time (Cslib.Complexity.TQBF.computableTidilyInPolyTime_edgeTest), which provides the machine.

Main results

• Cslib.Complexity.TQBF.computableTidilyInPolyTime_of_tokens: formulas from their tokens.
• Cslib.Complexity.TQBF.computableTidilyInPolyTime_savitchFormula: Savitch's formula is polynomial-time.
• Cslib.Complexity.TQBF.computableTidilyInPolyTime_baseFormula: a tableau as the formula of level 0 is polynomial-time.
• Cslib.Complexity.TQBF.computableTidilyInPolyTime_edgeTest: the test of one step or none is polynomial-time.
• Cslib.Complexity.TQBF.computableTidilyInPolyTime_reduce: the reduction is polynomial-time.

References

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

Formulas from their tokens

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_tokens : Turing.MultiTapeTM.ComputableTidilyInPolyTime Logic.PL.QBF.tokens encQBF (Turing.MultiTapeTM.encList encToken)

The tokens of an encoded formula, the identity on encoded values.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_of_tokens {γ : Type} {encIn : γ ↪ List Bool} {f : γ → Logic.PL.QBF ℕ} {l : γ → List (Logic.PL.QBF.Kind × ℕ)} (hl : Turing.MultiTapeTM.ComputableTidilyInPolyTime l encIn (Turing.MultiTapeTM.encList encToken)) (h : ∀ (x : γ), (f x).tokens = l x) : Turing.MultiTapeTM.ComputableTidilyInPolyTime f encIn encQBF

A formula is polynomial-time when its tokens are.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_var {γ : Type} {encIn : γ ↪ List Bool} {v : γ → ℕ} (hv : Turing.MultiTapeTM.ComputableTidilyInPolyTime v encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => Logic.PL.QBF.var (v x)) encIn encQBF

A variable, from its number in binary.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_not {γ : Type} {encIn : γ ↪ List Bool} {φ : γ → Logic.PL.QBF ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ encIn encQBF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => (φ x).not) encIn encQBF

Negation.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_and {γ : Type} {encIn : γ ↪ List Bool} {φ ψ : γ → Logic.PL.QBF ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ encIn encQBF) (hψ : Turing.MultiTapeTM.ComputableTidilyInPolyTime ψ encIn encQBF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => (φ x).and (ψ x)) encIn encQBF

Conjunction.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_or {γ : Type} {encIn : γ ↪ List Bool} {φ ψ : γ → Logic.PL.QBF ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ encIn encQBF) (hψ : Turing.MultiTapeTM.ComputableTidilyInPolyTime ψ encIn encQBF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => (φ x).or (ψ x)) encIn encQBF

Disjunction.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_exs {γ : Type} {encIn : γ ↪ List Bool} {vs : γ → List ℕ} {φ : γ → Logic.PL.QBF ℕ} (hvs : Turing.MultiTapeTM.ComputableTidilyInPolyTime vs encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ encIn encQBF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => Logic.PL.QBF.exs (vs x) (φ x)) encIn encQBF

A block of existential quantifiers, over a list of variables in binary.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_alls {γ : Type} {encIn : γ ↪ List Bool} {vs : γ → List ℕ} {φ : γ → Logic.PL.QBF ℕ} (hvs : Turing.MultiTapeTM.ComputableTidilyInPolyTime vs encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ encIn encQBF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => Logic.PL.QBF.alls (vs x) (φ x)) encIn encQBF

A block of universal quantifiers, over a list of variables in binary.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_conj {γ : Type} {encIn : γ ↪ List Bool} {l : γ → List (Logic.PL.QBF ℕ)} (hl : Turing.MultiTapeTM.ComputableTidilyInPolyTime l encIn (Turing.MultiTapeTM.encList encQBF)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => Logic.PL.QBF.conj (l x)) encIn encQBF

The conjunction of a list of formulas.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_imp {γ : Type} {encIn : γ ↪ List Bool} {φ ψ : γ → Logic.PL.QBF ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ encIn encQBF) (hψ : Turing.MultiTapeTM.ComputableTidilyInPolyTime ψ encIn encQBF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => (φ x).imp (ψ x)) encIn encQBF

Implication.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_iff {γ : Type} {encIn : γ ↪ List Bool} {φ ψ : γ → Logic.PL.QBF ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ encIn encQBF) (hψ : Turing.MultiTapeTM.ComputableTidilyInPolyTime ψ encIn encQBF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => (φ x).iff (ψ x)) encIn encQBF

Equivalence.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_lit {γ : Type} {encIn : γ ↪ List Bool} {v : γ → ℕ} {b : γ → Bool} (hv : Turing.MultiTapeTM.ComputableTidilyInPolyTime v encIn Turing.MultiTapeTM.encNat) (hb : Turing.MultiTapeTM.ComputableTidilyInPolyTime b encIn Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => Logic.PL.QBF.lit (v x) (b x)) encIn encQBF

A literal, from its variable in binary and its sign.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_ofCNF {γ : Type} {encIn : γ ↪ List Bool} {φ : γ → Logic.PL.CNF ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)))) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => Logic.PL.QBF.ofCNF (φ x)) encIn encQBF

A formula in conjunctive normal form, from its clauses in the encoding of Cslib.Complexity.encCNF.

The midpoint formulas

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_blockVar {γ : Type} {encIn : γ ↪ List Bool} {kind i j : γ → ℕ} (hkind : Turing.MultiTapeTM.ComputableTidilyInPolyTime kind encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableTidilyInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => blockVar (kind x) (i x) (j x)) encIn Turing.MultiTapeTM.encNat

A block variable, from its kind, level and index in unary, in binary.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_blockVars {γ : Type} {encIn : γ ↪ List Bool} {w kind i : γ → ℕ} (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) (hkind : Turing.MultiTapeTM.ComputableTidilyInPolyTime kind encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => blockVars (w x) (kind x) (i x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

The variables of a block, from the width, kind and level in unary.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_eqBlock {γ : Type} {encIn : γ ↪ List Bool} {w k i k' i' : γ → ℕ} (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableTidilyInPolyTime k encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hk' : Turing.MultiTapeTM.ComputableTidilyInPolyTime k' encIn Turing.MultiTapeTM.encUnary) (hi' : Turing.MultiTapeTM.ComputableTidilyInPolyTime i' encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => eqBlock (w x) (k x) (i x) (k' x) (i' x)) encIn encQBF

The equality of two blocks.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_isBlock {γ : Type} {encIn : γ ↪ List Bool} {w k i : γ → ℕ} {u : γ → List Bool} (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableTidilyInPolyTime k encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hu : Turing.MultiTapeTM.ComputableTidilyInPolyTime u encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => isBlock (w x) (k x) (i x) (u x)) encIn encQBF

A block holding a word.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_halves {γ : Type} {encIn : γ ↪ List Bool} {w i : γ → ℕ} (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => halves (w x) (i x)) encIn encQBF

The hypothesis of a level.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_levelTokens {γ : Type} {encIn : γ ↪ List Bool} {w i : γ → ℕ} (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => levelTokens (w x) (i x)) encIn (Turing.MultiTapeTM.encList encToken)

The tokens a level adds to the midpoint formula.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_midpoint {γ : Type} {encIn : γ ↪ List Bool} {w d : γ → ℕ} {base : γ → Logic.PL.QBF ℕ} (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) (hbase : Turing.MultiTapeTM.ComputableTidilyInPolyTime base encIn encQBF) (hd : Turing.MultiTapeTM.ComputableTidilyInPolyTime d encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => midpoint (w x) (base x) (d x)) encIn encQBF

The midpoint formula of level d, from the width and level in unary and the formula of level 0.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_savitchFormula {γ : Type} {encIn : γ ↪ List Bool} {w d : γ → ℕ} {base : γ → Logic.PL.QBF ℕ} {u v : γ → List Bool} (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) (hd : Turing.MultiTapeTM.ComputableTidilyInPolyTime d encIn Turing.MultiTapeTM.encUnary) (hbase : Turing.MultiTapeTM.ComputableTidilyInPolyTime base encIn encQBF) (hu : Turing.MultiTapeTM.ComputableTidilyInPolyTime u encIn Turing.MultiTapeTM.encBits) (hv : Turing.MultiTapeTM.ComputableTidilyInPolyTime v encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => savitchFormula (w x) (d x) (base x) (u x) (v x)) encIn encQBF

Savitch's formula is polynomial-time in the width and depth in unary, the formula of level 0, and the two words.

The formula of level 0

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_tabVar {k : ℕ} {State : Type} [Fintype State] : Turing.MultiTapeTM.ComputableTidilyInPolyTime tabVar CookLevin.encVar Turing.MultiTapeTM.encNat

The numbering of the tableau variables by odd numbers, in binary.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_certVar {γ : Type} {encIn : γ ↪ List Bool} {w j : γ → ℕ} (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableTidilyInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => certVar (w x) (j x)) encIn Turing.MultiTapeTM.encNat

The block variable holding a certificate bit, from the width and the index in unary.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_baseFormula {γ : Type} {encIn : γ ↪ List Bool} {k : ℕ} {State : Type} [Fintype State] {tab : γ → Logic.PL.CNF (CookLevin.Var k State)} {w : γ → ℕ} (htab : Turing.MultiTapeTM.ComputableTidilyInPolyTime tab encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair CookLevin.encVar Turing.MultiTapeTM.encBool)))) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => baseFormula (tab x) (w x)) encIn encQBF

A tableau as the formula of level 0 is polynomial-time in the tableau and the width in unary.

The reduction

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_width {α : Type} {enc : α ↪ List Bool} {k : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} {c d : ℕ} : Turing.MultiTapeTM.ComputableTidilyInPolyTime (width enc ntm c d) enc Turing.MultiTapeTM.encUnary

The width of the words of the reduction, in unary.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_edgeTest {α : Type} {enc : α ↪ List Bool} {k : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} {c d : ℕ} : Turing.MultiTapeTM.ComputableTidilyInPolyTime (edgeTest enc ntm c d) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The test of one step or none between codes is polynomial-time, on the instance and the concatenation of the two codes.

theorem Cslib.Complexity.TQBF.computableTidilyInPolyTime_reduce {α : Type} {enc : α ↪ List Bool} {k : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} {c d kV : ℕ} {StateV : Type} [Fintype StateV] [DecidableEq StateV] (tmV : Turing.MultiTapeTM kV Bool StateV) (cV dV : ℕ) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (reduce enc ntm c d tmV cV dV) enc encQBF

The reduction to TQBF is polynomial-time, for every machine tmV standing for the test of one step or none and every time bound cV * (n + 1) ^ dV allowed to it.