Unbounded-error probabilistic time

Cslib.Complexity.PPTIME enc t consists of the problems decided by strict majority within time O(t n), that is c₁ * t n + c₂ for constants c₁ and c₂, by a fair-coin machine with a binary alphabet and finitely many states (Turing.MultiTapePTM.DecidesByMajorityInTime): every run on that many coins has halted, and a ∈ A exactly when the run outputs [true] with probability more than 1 / 2. It is the unbounded-error counterpart of Cslib.Complexity.BPTIME, with the same machines and clocks.

Convention. Unbounded-error probabilistic computation goes back to Gill [Gil77]. The timed predicate here is this library's convention, not a transcription of a source definition: acceptance is strict and ties reject. A nonmember may output [true] with probability exactly 1 / 2, and its other outputs are unconstrained, so it need not output [false] with probability more than 1 / 2. This is the threshold of the library's verifier-based PP (Cslib.Complexity.DecidesByMajority), and the two agree at polynomial time (Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME). That equivalence is a union over all polynomial clocks; for a fixed time bound, no comparison with conventions that require a strict majority of [false] on nonmembers is proved here.

A fair-coin machine draws one coin per live step, so its acceptance probability within the clock t is the number of accepting coin strings of length t divided by 2 ^ t. Deciding by majority is therefore the comparison 2 ^ t < 2 * count of that count, an Cslib.Complexity.acceptCount of the coin replay Turing.MultiTapePTM.runClosedCoins (Turing.MultiTapePTM.decidesByMajorityInTime_iff).

PP (Cslib.Complexity.PP) is defined through polynomial-time verifiers reading random strings. It is the union of the classes PPTIME (n ^ k) (Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME), by the argument for BPP and BPTIME (Cslib.Complexity.mem_BPP_iff_exists_mem_BPTIME): a verifier run on sampled coins is a fair-coin machine with a halting polynomial clock, and a fair-coin machine halting within T steps is a verifier replaying T coins. A bounded-error decider decides by majority (Cslib.Complexity.BPTIME_subset_PPTIME).

Main definitions

• Turing.MultiTapePTM.DecidesByMajorityInTime: strict majority within a clock.
• Cslib.Complexity.PPTIME: unbounded-error probabilistic time.

Main results

• Turing.MultiTapePTM.decidesByMajorityInTime_iff: the majority condition as a count of accepting coin strings.
• Cslib.Complexity.PPTIME_mono: PPTIME is monotone in the time bound.
• Cslib.Complexity.BPTIME_subset_PPTIME: bounded error is a strict majority.
• Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME: PP is the union of the classes PPTIME (n ^ k).

References

• J. Gill, Computational complexity of probabilistic Turing machines
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Turing.MultiTapePTM.DecidesByMajorityInTime {k : ℕ} {State : Type} {α : Type u_1} (machine : MultiTapePTM k Bool State) (enc : α ↪ List Bool) (A : Set α) (t : α → ℕ) : Prop

machine decides A by strict majority within t, relative to the encoding enc: on every encoded instance enc a, every run of t a steps with fair coins has halted, and a ∈ A exactly when the run outputs [true] with probability more than 1 / 2. Ties reject, and outputs other than [true] are unconstrained; this is the library's convention, described in the module docstring.

theorem Turing.MultiTapePTM.DecidesByMajorityInTime.mono {k : ℕ} {State : Type} {α : Type u_1} {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {t t' : α → ℕ} (h : machine.DecidesByMajorityInTime enc A t) (ht : ∀ (a : α), t a ≤ t' a) : machine.DecidesByMajorityInTime enc A t'

Time bounds can be increased: a halted run ignores further coins.

theorem Turing.MultiTapePTM.decidesByMajorityInTime_iff {k : ℕ} {State : Type} {α : Type u_1} {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {t : α → ℕ} : machine.DecidesByMajorityInTime enc A t ↔ ∀ (a : α), (∀ final ∈ (machine.runClosedConfigFrom (t a) (MultiTapeMachine.initialConfig machine (enc a))).eval.support, final.tapes.state = none) ∧ (a ∈ A ↔ 2 ^ t a < 2 * Cslib.Complexity.acceptCount (fun (x : List Bool × List Bool) => decide (machine.runClosedCoins x.2 x.1 = [true])) (enc a) (t a))

Deciding by majority is a count comparison. A fair-coin machine decides A by strict majority within t exactly when, on every instance, every run has halted by the clock and a ∈ A exactly when more than half of the coin strings of length t a make the coin replay Turing.MultiTapePTM.runClosedCoins output [true].

def Cslib.Complexity.PPTIME {α : Type u_1} (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α)

The problems decidable by strict majority within time O(t n), that is c₁ * t n + c₂ for constants c₁ and c₂, on instances whose encoding under enc has length n, by a fair-coin machine with a binary alphabet and finitely many states: every run of that many steps has halted, and a ∈ A exactly when the run outputs [true] with probability more than 1 / 2. Ties reject (Turing.MultiTapePTM.DecidesByMajorityInTime).

theorem Cslib.Complexity.PPTIME_mono {α : Type u_1} {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} (h : ∀ (n : ℕ), t₁ n ≤ t₂ n) : PPTIME enc t₁ ⊆ PPTIME enc t₂

PPTIME is monotone in the time bound.

theorem Cslib.Complexity.BPTIME_subset_PPTIME {α : Type u_1} {enc : α ↪ List Bool} {t : ℕ → ℕ} : BPTIME enc t ⊆ PPTIME enc t

Bounded error is a strict majority: a machine outputting the right answer with probability at least 2 / 3 outputs [true] with probability at least 2 / 3 on members, and at most 1 / 3 on the others.

theorem Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ PP enc ↔ ∃ (k : ℕ), A ∈ PPTIME enc fun (x : ℕ) => x ^ k

PP is the union of the classes PPTIME (n ^ k): a polynomial-time verifier run on uniformly sampled random strings is a fair-coin machine halting within a polynomial clock, and a fair-coin machine halting within the clock T is a verifier replaying random strings of length T.