Bounded-error promise computation at a prescribed time

PromiseBPTIME enc T fixes a native fair-coin machine and an affine clock c₁ * T n + c₂ before the input. Every run halts within that clock, including off-promise runs. On yes-instances the output is [true] with probability at least 2/3, and on no-instances it is [false] with probability at least 2/3. No probability gap or answer is required outside the promise.

This is the library's time-indexed native-machine convention, extending BPTIME to partial promises: a decision problem is in PromiseBPTIME exactly when it is in BPTIME. It does not define the class through bounded-error total completions. A strict-majority completion belongs to PPTIME at the same caller-supplied clock, with ties rejecting; this is not a bounded-error completion in BPTIME.

The characterization by sample-and-verify and coin replay at the same clock, up to constant factors, is in CslibFrontier.Computability.Complexity.Classes.Promise.Time.Verifier.

Main definitions

• Turing.MultiTapePTM.SolvesPromiseWithBoundedErrorInTime: native clock and error contract.
• Cslib.Complexity.PromiseBPTIME: bounded-error promise computation in affine time.

Main results

• Turing.MultiTapePTM.solvesPromiseWithBoundedErrorInTime_ofSet_iff, ofSet_mem_PromiseBPTIME: on decision problems, the notions are Turing.MultiTapePTM.DecidesWithBoundedErrorInTime and BPTIME.
• PromiseBPTIME_mono: increasing the time bound preserves membership.
• mem_PromiseBPTIME_of_subset: shrinking either side of the promise preserves membership.
• promiseClass_BPTIME_subset_PromiseBPTIME: total bounded-error completions give witnesses.
• PromiseBPTIME_subset_promiseClass_PPTIME: a strict-majority completion at the same time scale.

def Turing.MultiTapePTM.SolvesPromiseWithBoundedErrorInTime {α : Type u_1} {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (enc : α ↪ List Bool) (Q : Cslib.Complexity.PromiseProblem α) (t : α → ℕ) : Prop

Every run halts by t; bounded error is required only on the two sides of the promise.

theorem Turing.MultiTapePTM.SolvesPromiseWithBoundedErrorInTime.mono {α : Type u_1} {k : ℕ} {State : Type} {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {Q : Cslib.Complexity.PromiseProblem α} {t t' : α → ℕ} (h : machine.SolvesPromiseWithBoundedErrorInTime enc Q t) (ht : ∀ (a : α), t a ≤ t' a) : machine.SolvesPromiseWithBoundedErrorInTime enc Q t'

A sufficiently long clock may be enlarged without changing the output law.

theorem Turing.MultiTapePTM.SolvesPromiseWithBoundedErrorInTime.of_subset {α : Type u_1} {k : ℕ} {State : Type} {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {Q Q' : Cslib.Complexity.PromiseProblem α} {t : α → ℕ} (h : machine.SolvesPromiseWithBoundedErrorInTime enc Q t) (hyes : Q'.yes ⊆ Q.yes) (hno : Q'.no ⊆ Q.no) : machine.SolvesPromiseWithBoundedErrorInTime enc Q' t

A machine solving a promise problem solves every promise problem with fewer yes-instances and fewer no-instances.

theorem Turing.MultiTapePTM.solvesPromiseWithBoundedErrorInTime_ofSet_iff {α : Type u_1} {k : ℕ} {State : Type} {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {t : α → ℕ} : machine.SolvesPromiseWithBoundedErrorInTime enc (Cslib.Complexity.PromiseProblem.ofSet A) t ↔ machine.DecidesWithBoundedErrorInTime enc A t

On a decision problem, solving with bounded error is deciding with bounded error.

def Cslib.Complexity.PromiseBPTIME {α : Type u_1} (enc : α ↪ List Bool) (T : ℕ → ℕ) : Set (PromiseProblem α)

Native bounded-error promise problems with fixed machine parameters and affine time T. All encoded inputs terminate, but the error conditions only constrain promised inputs.

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

Membership is monotone in the caller's time bound.

theorem Cslib.Complexity.mem_PromiseBPTIME_of_subset {α : Type u_1} {enc : α ↪ List Bool} {T : ℕ → ℕ} {Q Q' : PromiseProblem α} (hQ : Q ∈ PromiseBPTIME enc T) (hyes : Q'.yes ⊆ Q.yes) (hno : Q'.no ⊆ Q.no) : Q' ∈ PromiseBPTIME enc T

A promise problem with fewer yes-instances and fewer no-instances than one in PromiseBPTIME is in PromiseBPTIME.

@[simp]

theorem Cslib.Complexity.ofSet_mem_PromiseBPTIME {α : Type u_1} {enc : α ↪ List Bool} {T : ℕ → ℕ} {A : Set α} : PromiseProblem.ofSet A ∈ PromiseBPTIME enc T ↔ A ∈ BPTIME enc T

A decision problem, as a promise problem, is in PromiseBPTIME exactly when it is in BPTIME.

theorem Cslib.Complexity.promiseClass_BPTIME_subset_PromiseBPTIME {α : Type u_1} {enc : α ↪ List Bool} {T : ℕ → ℕ} : promiseClass (BPTIME enc T) ⊆ PromiseBPTIME enc T

A bounded-error total completion supplies a native bounded-error promise solver.

theorem Cslib.Complexity.PromiseBPTIME_subset_promiseClass_PPTIME {α : Type u_1} {enc : α ↪ List Bool} {T : ℕ → ℕ} : PromiseBPTIME enc T ⊆ promiseClass (PPTIME enc T)

Accepting by strict majority completes the promise in PPTIME without changing its clock. The completion may have an exact tie outside the promise; it need not belong to BPTIME.