The polynomial hierarchy

The levels Σₖ and Πₖ of the polynomial hierarchy are defined like NP (Cslib.Complexity.NP), through polynomial-time verifiers, now with k alternating quantifiers over certificates Arora and Barak, Definition 5.3, Wrathall: A ∈ SigmaP k enc when there are polynomials p₁, …, pₖ and a function V : α × List Bool → Bool, computable in polynomial time on inputs encPair enc encBits (a, w) = frame (enc a) ++ w, such that a ∈ A ↔ ∃ w₁, ∀ w₂, ∃ w₃, …, V (a, w₁ ++ w₂ ++ ⋯ ++ wₖ) = true, where wᵢ ranges over the strings of length pᵢ (enc a).length. PiP k enc is the same with a universal quantifier first, and PH enc is the union of the levels SigmaP k enc Stockmeyer.

Two choices make the inclusions between levels hold with the same verifier, and hence without any facts about polynomial time:

• The certificates are concatenated into one string, as in NP, so that SigmaP 1 enc = NP enc (SigmaP_one).
• Each block of certificates has its own length pᵢ, where Arora and Barak use one polynomial for all blocks. A block of length 0 is a vacuous quantifier, so adding one at either end of the quantifier prefix shows SigmaP k ∪ PiP k ⊆ SigmaP (k + 1) ∩ PiP (k + 1). The two definitions give the same classes, since padding every block to the largest length only needs a verifier that skips the padding.

The zero levels are P: a decider can ignore its certificate, and a verifier with no quantifiers can be run on the empty certificate. That Πₖ consists of the complements of the problems in Σₖ follows from quantifier duality (not_alternation) and closure of polynomial time under Boolean negation. These transformations use the polynomial-time machine calculus.

Main definitions

• Cslib.Complexity.Alternation: alternating quantifiers over binary strings of given lengths.
• Cslib.Complexity.IsAlternatingVerifier: the verifier condition.
• Cslib.Complexity.SigmaP, Cslib.Complexity.PiP, Cslib.Complexity.PH.

Main results

• Cslib.Complexity.not_alternation: the duality of alternating quantifiers.
• Cslib.Complexity.SigmaP_zero, Cslib.Complexity.PiP_zero: Σ₀ = Π₀ = P.
• Cslib.Complexity.PiP_eq_preimage_compl_SigmaP: Πₖ = coΣₖ.
• Cslib.Complexity.SigmaP_one: Σ₁ = NP; Cslib.Complexity.PiP_one_eq_coNP: Π₁ = coNP.
• Cslib.Complexity.SigmaP_subset_SigmaP_succ, Cslib.Complexity.SigmaP_subset_PiP_succ, Cslib.Complexity.PiP_subset_SigmaP_succ, Cslib.Complexity.PiP_subset_PiP_succ: the inclusions between consecutive levels.
• Cslib.Complexity.PH_eq_iUnion_PiP: PH = ⋃ Πₖ.
• Cslib.Complexity.P_subset_PH, Cslib.Complexity.NP_subset_PH, Cslib.Complexity.coNP_subset_PH.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• L. Stockmeyer, The polynomial-time hierarchy
• C. Wrathall, Complete sets and the polynomial-time hierarchy

Alternating quantifiers

def Cslib.Complexity.Alternation : Bool → List ℕ → (List Bool → Prop) → Prop

Alternating quantifiers over binary strings: Alternation q [n₁, …, nₖ] P says Q₁ w₁, Q₂ w₂, …, Qₖ wₖ, P (w₁ ++ w₂ ++ ⋯ ++ wₖ), where wᵢ ranges over the strings of length nᵢ and the quantifiers Qᵢ alternate, starting with ∃ if q is true and with ∀ if q is false.

@[simp]

theorem Cslib.Complexity.alternation_nil {q : Bool} {P : List Bool → Prop} : Alternation q [] P ↔ P []

theorem Cslib.Complexity.alternation_true_cons {n : ℕ} {ns : List ℕ} {P : List Bool → Prop} : Alternation true (n :: ns) P ↔ ∃ (w : List Bool), w.length = n ∧ Alternation false ns fun (v : List Bool) => P (w ++ v)

theorem Cslib.Complexity.alternation_false_cons {n : ℕ} {ns : List ℕ} {P : List Bool → Prop} : Alternation false (n :: ns) P ↔ ∀ (w : List Bool), w.length = n → Alternation true ns fun (v : List Bool) => P (w ++ v)

theorem Cslib.Complexity.Alternation.mono {q : Bool} {ns : List ℕ} {P Q : List Bool → Prop} (h : ∀ (w : List Bool), P w → Q w) : Alternation q ns P → Alternation q ns Q

theorem Cslib.Complexity.alternation_congr {q : Bool} {ns : List ℕ} {P Q : List Bool → Prop} (h : ∀ (w : List Bool), P w ↔ Q w) : Alternation q ns P ↔ Alternation q ns Q

theorem Cslib.Complexity.not_alternation {q : Bool} {ns : List ℕ} {P : List Bool → Prop} : ¬Alternation q ns P ↔ Alternation (!q) ns fun (w : List Bool) => ¬P w

Quantifier duality. Negating alternating quantifiers swaps every quantifier and negates the predicate.

theorem Cslib.Complexity.alternation_append_zero {q : Bool} {ns : List ℕ} {P : List Bool → Prop} : Alternation q (ns ++ [0]) P ↔ Alternation q ns P

A quantifier over strings of length 0 at the end of the prefix is vacuous.

theorem Cslib.Complexity.alternation_zero_cons {q : Bool} {ns : List ℕ} {P : List Bool → Prop} : Alternation q (0 :: ns) P ↔ Alternation (!q) ns P

A quantifier over strings of length 0 at the start of the prefix is vacuous.

theorem Cslib.Complexity.alternation_singleton_true {n : ℕ} {P : List Bool → Prop} : Alternation true [n] P ↔ ∃ (w : List Bool), w.length = n ∧ P w

Alternating verifiers

def Cslib.Complexity.IsAlternatingVerifier {α : Type} (enc : α ↪ List Bool) (q : Bool) (ps : List (Polynomial ℕ)) (V : α × List Bool → Bool) (A : Set α) : Prop

V verifies A through alternating quantifiers over certificates whose lengths are the polynomials ps, evaluated at the length of the encoded instance, starting with ∃ if q is true and with ∀ if q is false: a ∈ A iff Q₁ w₁, Q₂ w₂, …, V (a, w₁ ++ w₂ ++ ⋯).

theorem Cslib.Complexity.IsAlternatingVerifier.compl {α : Type} {enc : α ↪ List Bool} {q : Bool} {ps : List (Polynomial ℕ)} {V : α × List Bool → Bool} {A : Set α} (h : IsAlternatingVerifier enc q ps V A) : IsAlternatingVerifier enc (!q) ps (fun (x : α × List Bool) => !V x) Aᶜ

Negating the verifier verifies the complement with every quantifier swapped.

theorem Cslib.Complexity.IsAlternatingVerifier.append_zero {α : Type} {enc : α ↪ List Bool} {q : Bool} {ps : List (Polynomial ℕ)} {V : α × List Bool → Bool} {A : Set α} (h : IsAlternatingVerifier enc q ps V A) : IsAlternatingVerifier enc q (ps ++ [0]) V A

A block of certificates of length 0 can be added at the end.

theorem Cslib.Complexity.IsAlternatingVerifier.zero_cons {α : Type} {enc : α ↪ List Bool} {q : Bool} {ps : List (Polynomial ℕ)} {V : α × List Bool → Bool} {A : Set α} (h : IsAlternatingVerifier enc q ps V A) : IsAlternatingVerifier enc (!q) (0 :: ps) V A

A block of certificates of length 0 can be added at the start, as a quantifier of the other kind.

theorem Cslib.Complexity.isAlternatingVerifier_true_singleton {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {A : Set α} {p : Polynomial ℕ} : IsAlternatingVerifier enc true [p] V A ↔ IsVerifier enc p V A

With one existential block, an alternating verifier is a verifier in the sense of NP.

The levels of the hierarchy

def Cslib.Complexity.SigmaP {α : Type} (k : ℕ) (enc : α ↪ List Bool) : Set (Set α)

The level Σₖ of the polynomial hierarchy, with respect to the encoding enc of instances: the problems verified in polynomial time through k alternating blocks of polynomially long certificates, the first existential Arora and Barak, Definition 5.3, Wrathall.

def Cslib.Complexity.PiP {α : Type} (k : ℕ) (enc : α ↪ List Bool) : Set (Set α)

The level Πₖ of the polynomial hierarchy, with respect to the encoding enc of instances: the problems verified in polynomial time through k alternating blocks of polynomially long certificates, the first universal Arora and Barak, Definition 5.3, Wrathall.

def Cslib.Complexity.PH {α : Type} (enc : α ↪ List Bool) : Set (Set α)

The polynomial hierarchy: the union of the levels Σₖ Stockmeyer, Arora and Barak, Definition 5.3.

theorem Cslib.Complexity.mem_SigmaP {α : Type} {enc : α ↪ List Bool} {A : Set α} {k : ℕ} : A ∈ SigmaP k enc ↔ ∃ (ps : List (Polynomial ℕ)) (V : α × List Bool → Bool), ps.length = k ∧ Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ IsAlternatingVerifier enc true ps V A

theorem Cslib.Complexity.mem_PiP {α : Type} {enc : α ↪ List Bool} {A : Set α} {k : ℕ} : A ∈ PiP k enc ↔ ∃ (ps : List (Polynomial ℕ)) (V : α × List Bool → Bool), ps.length = k ∧ Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ IsAlternatingVerifier enc false ps V A

theorem Cslib.Complexity.mem_PH {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ PH enc ↔ ∃ (k : ℕ), A ∈ SigmaP k enc

A problem is in the polynomial hierarchy exactly when it is in some level Σₖ.

The first levels

theorem Cslib.Complexity.SigmaP_zero_eq_PiP_zero {α : Type} {enc : α ↪ List Bool} : SigmaP 0 enc = PiP 0 enc

Without quantifiers, it does not matter which quantifier would have come first.

theorem Cslib.Complexity.SigmaP_one {α : Type} {enc : α ↪ List Bool} : SigmaP 1 enc = NP enc

Σ₁ = NP.

theorem Cslib.Complexity.P_subset_SigmaP_zero {α : Type} {enc : α ↪ List Bool} : P enc ⊆ SigmaP 0 enc

P ⊆ Σ₀: a decider can ignore its certificate.

theorem Cslib.Complexity.SigmaP_zero_subset_P {α : Type} {enc : α ↪ List Bool} : SigmaP 0 enc ⊆ P enc

Σ₀ ⊆ P: run a verifier with no quantifiers on the empty certificate.

theorem Cslib.Complexity.SigmaP_zero {α : Type} {enc : α ↪ List Bool} : SigmaP 0 enc = P enc

Σ₀ = P.

theorem Cslib.Complexity.PiP_zero {α : Type} {enc : α ↪ List Bool} : PiP 0 enc = P enc

Π₀ = P.

Inclusions between levels

theorem Cslib.Complexity.SigmaP_subset_SigmaP_succ {α : Type} {enc : α ↪ List Bool} (k : ℕ) : SigmaP k enc ⊆ SigmaP (k + 1) enc

Σₖ ⊆ Σₖ₊₁: a block of certificates of length 0 is added at the end.

theorem Cslib.Complexity.PiP_subset_PiP_succ {α : Type} {enc : α ↪ List Bool} (k : ℕ) : PiP k enc ⊆ PiP (k + 1) enc

Πₖ ⊆ Πₖ₊₁: a block of certificates of length 0 is added at the end.

theorem Cslib.Complexity.SigmaP_subset_PiP_succ {α : Type} {enc : α ↪ List Bool} (k : ℕ) : SigmaP k enc ⊆ PiP (k + 1) enc

Σₖ ⊆ Πₖ₊₁: a universal block of certificates of length 0 is added at the start.

theorem Cslib.Complexity.PiP_subset_SigmaP_succ {α : Type} {enc : α ↪ List Bool} (k : ℕ) : PiP k enc ⊆ SigmaP (k + 1) enc

Πₖ ⊆ Σₖ₊₁: an existential block of certificates of length 0 is added at the start.

theorem Cslib.Complexity.SigmaP_mono {α : Type} {enc : α ↪ List Bool} : Monotone fun (k : ℕ) => SigmaP k enc

theorem Cslib.Complexity.PiP_mono {α : Type} {enc : α ↪ List Bool} : Monotone fun (k : ℕ) => PiP k enc

theorem Cslib.Complexity.SigmaP_subset_PH {α : Type} {enc : α ↪ List Bool} (k : ℕ) : SigmaP k enc ⊆ PH enc

theorem Cslib.Complexity.PiP_subset_PH {α : Type} {enc : α ↪ List Bool} (k : ℕ) : PiP k enc ⊆ PH enc

theorem Cslib.Complexity.PH_eq_iUnion_PiP {α : Type} {enc : α ↪ List Bool} : PH enc = ⋃ (k : ℕ), PiP k enc

The polynomial hierarchy is also the union of the levels Πₖ.

theorem Cslib.Complexity.NP_subset_PH {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ PH enc

NP ⊆ PH, since NP = Σ₁.

theorem Cslib.Complexity.P_subset_PH {α : Type} {enc : α ↪ List Bool} : P enc ⊆ PH enc

P ⊆ PH, since P ⊆ Σ₀.

Quantifier duality

theorem Cslib.Complexity.compl_mem_PiP_of_mem_SigmaP {α : Type} {enc : α ↪ List Bool} {A : Set α} {k : ℕ} (hA : A ∈ SigmaP k enc) : Aᶜ ∈ PiP k enc

theorem Cslib.Complexity.compl_mem_SigmaP_of_mem_PiP {α : Type} {enc : α ↪ List Bool} {A : Set α} {k : ℕ} (hA : A ∈ PiP k enc) : Aᶜ ∈ SigmaP k enc

theorem Cslib.Complexity.PiP_eq_preimage_compl_SigmaP {α : Type} {enc : α ↪ List Bool} {k : ℕ} : PiP k enc = compl ⁻¹' SigmaP k enc

Πₖ = coΣₖ.

theorem Cslib.Complexity.SigmaP_eq_preimage_compl_PiP {α : Type} {enc : α ↪ List Bool} {k : ℕ} : SigmaP k enc = compl ⁻¹' PiP k enc

Σₖ = coΠₖ.

theorem Cslib.Complexity.PiP_one_eq_coNP {α : Type} {enc : α ↪ List Bool} : PiP 1 enc = coNP enc

Π₁ = coNP.

theorem Cslib.Complexity.coNP_subset_PH {α : Type} {enc : α ↪ List Bool} : coNP enc ⊆ PH enc

coNP ⊆ PH, since coNP = Π₁.