Integer weights for adaptive Boolean computations

A finite computation chooses a Boolean answer at each step. The two answer weights sum to a common denominator D, but may depend on the complete current state. Thus later answer weights may depend on earlier answers. Products of these weights give unnormalized transcript weights.

This finite weighted-tree calculation is used in approximate oracle simulation [Fen03]. It makes no computability or machine-resource assumption.

Main definitions

• AdaptiveWeights.branchWeight: the weight of one answer, p s for true and D - p s for false.
• AdaptiveWeights.pathWeight: the product of weights along an explicit answer list.
• AdaptiveWeights.acceptWeight: the total weight of accepting answer sequences.

Main results

• AdaptiveWeights.pathWeight_eq_prod: express a transcript weight as a product over prefixes.
• AdaptiveWeights.acceptWeight_eq_sum: express the accepting weight as a finite Boolean sum.
• AdaptiveWeights.acceptWeight_bounds: accepting weight lies between zero and D ^ n.
• AdaptiveWeights.acceptWeight_error: per-step wrong-answer bounds give an adaptive error bound.
• AdaptiveWeights.sum_error: amplified error remains small after summing a Boolean batch.

References

• S. Fenner, PP-Lowness and a Simple Definition of AWPP

def Cslib.Probability.AdaptiveWeights.branchWeight {σ : Type u_1} (D : ℤ) (p : σ → ℤ) (s : σ) (b : Bool) : ℤ

Branch weights with a common total D; the true-answer numerator may depend on the state.

def Cslib.Probability.AdaptiveWeights.pathWeight {σ : Type u_1} (D : ℤ) (p : σ → ℤ) (step : σ → Bool → σ) : σ → List Bool → ℤ

The product of branch weights along a transcript. The transition may depend on each answer.

theorem Cslib.Probability.AdaptiveWeights.pathWeight_eq_prod {σ : Type u_1} (D : ℤ) (p : σ → ℤ) (step : σ → Bool → σ) (s : σ) (bs : List Bool) : pathWeight D p step s bs = ∏ i ∈ Finset.range bs.length, branchWeight D p (List.foldl step s (List.take i bs)) (bs.getD i false)

A product over the successive replay prefixes, suitable for uniform counting products.

def Cslib.Probability.AdaptiveWeights.acceptWeight {σ : Type u_1} (D : ℤ) (p : σ → ℤ) (step : σ → Bool → σ) (accept : σ → Bool) : ℕ → σ → ℤ

Total accepting weight after a fixed number of adaptive steps.

theorem Cslib.Probability.AdaptiveWeights.acceptWeight_eq_sum {σ : Type u_1} (D : ℤ) (p : σ → ℤ) (step : σ → Bool → σ) (accept : σ → Bool) (n : ℕ) (s : σ) : acceptWeight D p step accept n s = ∑ w : Fin n → Bool, pathWeight D p step s (List.ofFn w) * if accept (List.foldl step s (List.ofFn w)) = true then 1 else 0

The recursive weighted computation sums precisely the accepting transcript weights.

theorem Cslib.Probability.AdaptiveWeights.acceptWeight_bounds {σ : Type u_1} {D : ℤ} {p : σ → ℤ} (step : σ → Bool → σ) (accept : σ → Bool) (hp : ∀ (s : σ), 0 ≤ p s ∧ p s ≤ D) (n : ℕ) (s : σ) : 0 ≤ acceptWeight D p step accept n s ∧ acceptWeight D p step accept n s ≤ D ^ n

Nonnegative branch weights give an accepting weight between zero and the total mass.

theorem Cslib.Probability.AdaptiveWeights.acceptWeight_error {σ : Type u_1} {D M : ℤ} {p : σ → ℤ} (step : σ → Bool → σ) (accept answer : σ → Bool) (hD : 0 ≤ D) (hM : 0 ≤ M) (hp : ∀ (s : σ), 0 ≤ p s ∧ p s ≤ D) (herr : ∀ (s : σ), (M * branchWeight D p s !answer s) ≤ D) (n : ℕ) (s : σ) : M * |acceptWeight D p step accept n s - D ^ n * if accept ((fun (s : σ) => step s (answer s))^[n] s) = true then 1 else 0| ≤ ↑n * D ^ n

If every step gives weight at most D / M to the wrong answer, the total acceptance weight differs from the ideal deterministic answer by at most n / M of the total mass. Answers and future weights may depend on the state, so the estimate includes adaptive computations.

theorem Cslib.Probability.AdaptiveWeights.sum_error {m n : ℕ} {E : ℤ} (hE : 0 ≤ E) (f : (Fin m → Bool) → ℤ) (ideal : (Fin m → Bool) → Bool) (herr : ∀ (w : Fin m → Bool), 2 ^ (m + n + 4) * |f w - E * if ideal w = true then 1 else 0| ≤ ↑n * E) : 16 * |∑ w : Fin m → Bool, f w - E * ∑ w : Fin m → Bool, if ideal w = true then 1 else 0| ≤ E

Summing over m witness bits preserves a one-sixteenth total error when each of n steps has error at most 2 ^ -(m + n + 4). All quantities are unnormalized integers.