Verifier characterization of PromiseBPTIME within explicit time

Promise problems Goldreich in Cslib.Complexity.PromiseBPTIME enc t are characterized by deterministic verifiers reading random strings, keeping the time bound up to constant factors:

• Sample and verify (Cslib.Complexity.mem_PromiseBPTIME_of_verifier). If a verifier V is computable within time T (a, w) on encoded pairs, the length ℓ a of the random string is computable in unary within Tℓ a, and (enc a).length + Tℓ a + T (a, w) is within O(t (enc a).length), then a promise problem is in PromiseBPTIME enc t when at least two thirds of the strings of length ℓ a are accepted on its yes-instances and rejected on its no-instances. The machine is Cslib.Complexity.exists_machine_sampleVerify.
• Coin replay (Cslib.Complexity.exists_verifier_of_mem_PromiseBPTIME). A promise problem in PromiseBPTIME enc t has a verifier computable in linear time on encoded pairs: replay the coins on the machine and test whether the output is [true]. Every random-string length of at least c * t (enc a).length + c works, since a halted run ignores further coins.

The polynomial characterization of PromiseBPP (Cslib.Complexity.mem_PromiseBPP_iff_exists_isPPTOn) loses the polynomial degree; these explicit-time forms are what a time hierarchy for promise problems needs. Such a hierarchy is known without advice, by delayed diagonalization He, while the hierarchy for BPTIME itself is open.

Main results

• Cslib.Complexity.mem_PromiseBPTIME_of_verifier: sample and verify within explicit time.
• Cslib.Complexity.exists_verifier_of_mem_PromiseBPTIME: a linear-time coin-replay verifier.

References

• O. Goldreich, On promise problems: a survey
• S. He, A note on a hierarchy theorem for promise-BPTIME

theorem Cslib.Complexity.mem_PromiseBPTIME_of_verifier {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} {V : α × List Bool → Bool} {ℓ : α → ℕ} {t : ℕ → ℕ} {Tℓ Sℓ : α → ℕ} {T S : α × List Bool → ℕ} {C : ℕ} (hℓ : Turing.MultiTapeTM.ComputableInO ℓ enc Turing.MultiTapeTM.encUnary Tℓ Sℓ) (hV : Turing.MultiTapeTM.ComputableInO V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool T S) (ht : ∀ (a : α) (w : List Bool), w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C) (hyes : ∀ a ∈ Q.yes, 2 * 2 ^ ℓ a ≤ 3 * acceptCount V a (ℓ a)) (hno : ∀ a ∈ Q.no, 2 * 2 ^ ℓ a ≤ 3 * acceptCount (fun (p : α × List Bool) => !V p) a (ℓ a)) : Q ∈ PromiseBPTIME enc t

Sample and verify, within explicit time. If a verifier V is computable within time T (a, w) on encoded pairs, and the length ℓ a of the random string is computable in unary within time Tℓ a, with (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C for every string w of length ℓ a, then a promise problem is in PromiseBPTIME enc t when V accepts at least two thirds of the strings of length ℓ a together with each yes-instance a, and rejects at least two thirds of them together with each no-instance.

theorem Cslib.Complexity.exists_verifier_of_mem_PromiseBPTIME {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} {t : ℕ → ℕ} (hQ : Q ∈ PromiseBPTIME enc t) : ∃ (V : α × List Bool → Bool) (c : ℕ), (Turing.MultiTapeTM.ComputableInO V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool (fun (p : α × List Bool) => ((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) p).length) fun (p : α × List Bool) => ((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) p).length) ∧ ∀ (a : α) (L : ℕ), c * t (enc a).length + c ≤ L → (a ∈ Q.yes → 2 * 2 ^ L ≤ 3 * acceptCount V a L) ∧ (a ∈ Q.no → 2 * 2 ^ L ≤ 3 * acceptCount (fun (p : α × List Bool) => !V p) a L)

A linear-time verifier for promise-problem probabilistic time. A promise problem in PromiseBPTIME enc t has a verifier computable in linear time on encoded pairs. For a constant c, every random-string length L ≥ c * t (enc a).length + c works: the verifier accepts at least two thirds of the strings of length L together with each yes-instance, and rejects at least two thirds of them together with each no-instance. The verifier replays the coins on the machine and tests whether the output is [true].