Combining verifiers

The counting classes #P, PP, RP and BPP are all defined through polynomial-time functions V : α × List Bool → Bool that read an instance and a string of bits, and through the number Cslib.Complexity.acceptCount V a n of strings of length n that V accepts together with a. This file provides verifiers built from other verifiers, each with its polynomial-time rule (registered with fun_prop) and the number of strings it accepts.

• Cslib.Complexity.andVerifier k V₁ V₂ runs V₁ on the first k a bits and V₂ on the rest, and accepts when both accept. The number of strings it accepts is the product of the numbers that V₁ and V₂ accept (Cslib.Complexity.acceptCount_andVerifier). With V₂ accepting everything, it multiplies the count by a power of two.
• Cslib.Complexity.padVerifier k V runs V on the first k a bits and requires the rest to be false (Cslib.Complexity.allFalseVerifier), so it accepts as many strings of any length n ≥ k a as V accepts of length k a (Cslib.Complexity.acceptCount_padVerifier_of_le).
• Cslib.Complexity.orVerifier k V₁ V₂ accepts when either accepts; the rejected strings multiply (Cslib.Complexity.acceptCount_orVerifier).
• Cslib.Complexity.selectVerifier V₀ V₁ lets the first bit choose between V₀ and V₁ on the remaining bits; the counts add (Cslib.Complexity.acceptCount_selectVerifier).
• Cslib.Complexity.sumVerifier k₁ k₂ V₁ V₂ selects between V₁ and V₂ padded to a common length, so it adds counts taken at different lengths k₁ a and k₂ a (Cslib.Complexity.acceptCount_sumVerifier). This is how #P is closed under addition.

Running two verifiers on disjoint parts of the random string is the usual way to combine independent random choices Arora and Barak, Chapters 7 and 17.

Main definitions

• Cslib.Complexity.allFalseVerifier, Cslib.Complexity.andVerifier, Cslib.Complexity.padVerifier, Cslib.Complexity.orVerifier, Cslib.Complexity.selectVerifier, Cslib.Complexity.sumVerifier.

Main results

• Cslib.Complexity.acceptCount_andVerifier, Cslib.Complexity.acceptCount_padVerifier_of_le, Cslib.Complexity.acceptCount_orVerifier, Cslib.Complexity.acceptCount_selectVerifier, Cslib.Complexity.acceptCount_sumVerifier: counts of the combined verifiers.
• Cslib.Complexity.computableInPolyTime_andVerifier, Cslib.Complexity.computableInPolyTime_padVerifier, Cslib.Complexity.computableInPolyTime_orVerifier, Cslib.Complexity.computableInPolyTime_selectVerifier, Cslib.Complexity.computableInPolyTime_sumVerifier: the combined verifiers are polynomial-time.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

The string of falses

def Cslib.Complexity.allFalseVerifier {α : Type} (x : α × List Bool) : Bool

The verifier accepting, with every instance, exactly the strings of falses.

@[simp]

theorem Cslib.Complexity.acceptCount_allFalseVerifier {α : Type} (a : α) (n : ℕ) : acceptCount allFalseVerifier a n = 1

allFalseVerifier accepts one string of each length.

theorem Cslib.Complexity.computableInPolyTime_allFalseVerifier {α : Type} {enc : α ↪ List Bool} : Turing.MultiTapeTM.ComputableInPolyTime allFalseVerifier (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

allFalseVerifier is polynomial-time.

Conjunction on disjoint parts of the string

def Cslib.Complexity.andVerifier {α : Type} (k : α → ℕ) (V₁ V₂ : α × List Bool → Bool) (x : α × List Bool) : Bool

Run V₁ on the first k a bits and V₂ on the remaining bits, and accept when both accept.

theorem Cslib.Complexity.acceptCount_andVerifier {α : Type} (k : α → ℕ) (V₁ V₂ : α × List Bool → Bool) (a : α) (n : ℕ) : acceptCount (andVerifier k V₁ V₂) a (k a + n) = acceptCount V₁ a (k a) * acceptCount V₂ a n

Independent runs multiply: on strings of length k a + n, andVerifier k V₁ V₂ accepts the product of the numbers of strings that V₁ and V₂ accept.

theorem Cslib.Complexity.acceptCount_andVerifier_true {α : Type} (k : α → ℕ) (V : α × List Bool → Bool) (a : α) (n : ℕ) : acceptCount (andVerifier k V fun (x : α × List Bool) => true) a (k a + n) = acceptCount V a (k a) * 2 ^ n

Ignoring the bits after the first k a multiplies the number of accepted strings by a power of two.

theorem Cslib.Complexity.computableInPolyTime_andVerifier {α : Type} {enc : α ↪ List Bool} {k : α → ℕ} {V₁ V₂ : α × List Bool → Bool} (hk : Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encUnary) (hV₁ : Turing.MultiTapeTM.ComputableInPolyTime V₁ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hV₂ : Turing.MultiTapeTM.ComputableInPolyTime V₂ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (andVerifier k V₁ V₂) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Independent conjunction of plain polynomial-time verifiers is polynomial-time.

Padding

def Cslib.Complexity.padVerifier {α : Type} (k : α → ℕ) (V : α × List Bool → Bool) : α × List Bool → Bool

Run V on the first k a bits and require the remaining bits to be false.

theorem Cslib.Complexity.acceptCount_padVerifier_of_le {α : Type} (k : α → ℕ) (V : α × List Bool → Bool) {a : α} {n : ℕ} (h : k a ≤ n) : acceptCount (padVerifier k V) a n = acceptCount V a (k a)

Padding: on strings of any length n ≥ k a, padVerifier k V accepts as many strings as V accepts of length k a.

theorem Cslib.Complexity.computableInPolyTime_padVerifier {α : Type} {enc : α ↪ List Bool} {k : α → ℕ} {V : α × List Bool → Bool} (hk : Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encUnary) (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (padVerifier k V) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Padding a plain polynomial-time verifier is polynomial-time.

Disjunction on disjoint parts of the string

def Cslib.Complexity.orVerifier {α : Type} (k : α → ℕ) (V₁ V₂ : α × List Bool → Bool) (x : α × List Bool) : Bool

Run V₁ on the first k a bits and V₂ on the remaining bits, and accept when either accepts.

theorem Cslib.Complexity.acceptCount_orVerifier {α : Type} (k : α → ℕ) (V₁ V₂ : α × List Bool → Bool) (a : α) (n : ℕ) : acceptCount (orVerifier k V₁ V₂) a (k a + n) + acceptCount (fun (x : α × List Bool) => !V₁ x) a (k a) * acceptCount (fun (x : α × List Bool) => !V₂ x) a n = 2 ^ (k a + n)

Independent rejections multiply: on strings of length k a + n, orVerifier k V₁ V₂ rejects the product of the numbers of strings that V₁ and V₂ reject.

theorem Cslib.Complexity.computableInPolyTime_orVerifier {α : Type} {enc : α ↪ List Bool} {k : α → ℕ} {V₁ V₂ : α × List Bool → Bool} (hk : Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encUnary) (hV₁ : Turing.MultiTapeTM.ComputableInPolyTime V₁ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hV₂ : Turing.MultiTapeTM.ComputableInPolyTime V₂ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (orVerifier k V₁ V₂) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Independent disjunction of plain polynomial-time verifiers is polynomial-time.

Choosing by the first bit

def Cslib.Complexity.selectVerifier {α : Type} (V₀ V₁ : α × List Bool → Bool) (x : α × List Bool) : Bool

Run V₀ on the remaining bits when the first bit is false, and V₁ when it is true.

theorem Cslib.Complexity.acceptCount_selectVerifier {α : Type} (V₀ V₁ : α × List Bool → Bool) (a : α) (n : ℕ) : acceptCount (selectVerifier V₀ V₁) a (n + 1) = acceptCount V₀ a n + acceptCount V₁ a n

Choices add: on strings of length n + 1, selectVerifier V₀ V₁ accepts the sum of the numbers of strings of length n that V₀ and V₁ accept.

theorem Cslib.Complexity.computableInPolyTime_selectVerifier {α : Type} {enc : α ↪ List Bool} {V₀ V₁ : α × List Bool → Bool} (hV₀ : Turing.MultiTapeTM.ComputableInPolyTime V₀ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hV₁ : Turing.MultiTapeTM.ComputableInPolyTime V₁ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (selectVerifier V₀ V₁) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Selection by the first bit preserves plain polynomial-time verification.

Sums of two counts

def Cslib.Complexity.sumVerifier {α : Type} (k₁ k₂ : α → ℕ) (V₁ V₂ : α × List Bool → Bool) : α × List Bool → Bool

Let the first bit choose between V₁ on k₁ a bits and V₂ on k₂ a bits, padding the chosen verifier's strings to k₁ a + k₂ a bits with falses.

theorem Cslib.Complexity.acceptCount_sumVerifier {α : Type} (k₁ k₂ : α → ℕ) (V₁ V₂ : α × List Bool → Bool) (a : α) : acceptCount (sumVerifier k₁ k₂ V₁ V₂) a (k₁ a + k₂ a + 1) = acceptCount V₁ a (k₁ a) + acceptCount V₂ a (k₂ a)

Counts add: on strings of length k₁ a + k₂ a + 1, sumVerifier k₁ k₂ V₁ V₂ accepts the sum of the numbers of strings that V₁ accepts of length k₁ a and V₂ of length k₂ a.

theorem Cslib.Complexity.computableInPolyTime_sumVerifier {α : Type} {enc : α ↪ List Bool} {k₁ k₂ : α → ℕ} {V₁ V₂ : α × List Bool → Bool} (hk₁ : Turing.MultiTapeTM.ComputableInPolyTime k₁ enc Turing.MultiTapeTM.encUnary) (hk₂ : Turing.MultiTapeTM.ComputableInPolyTime k₂ enc Turing.MultiTapeTM.encUnary) (hV₁ : Turing.MultiTapeTM.ComputableInPolyTime V₁ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hV₂ : Turing.MultiTapeTM.ComputableInPolyTime V₂ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (sumVerifier k₁ k₂ V₁ V₂) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The sum of two plain polynomial-time verifiers is polynomial-time.