Documentation

Complexity.Computability.Complexity.Classes.RepeatedTrials

Deterministic computations on repeated random-tape blocks #

Split a supplied bit list into fixed-width rows and collect one Boolean vote per row. Callers can compute the dimensions from the encoded instance length. Missing bits read as false; extra bits are ignored, and zero-width rows are retained. No probability distribution or complexity-class error condition is imposed here.

repeatAny and repeatMajority aggregate the same votes. Their error bounds belong to the class-specific amplification modules. Complexity.Computability.Probabilistic.Repeat provides the separate probabilistic-program interface for independently sampled runs.

Main definitions #

Main results #

References #

Extracted from the deterministic repetition implementations in BPP.Amplification and RP by Samuel Schlesinger. For their use in error reduction, see S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 7.

source
def Cslib.Complexity.repeatVotes {α : Type} (trials width : ℕ) (V : α × List Bool → Bool) (input : α × List Bool) :
List Bool

Collect votes on fixed-width rows of a supplied random tape, padding missing bits with false and ignoring bits beyond the prescribed rows. Zero-width rows still contribute votes.

Instances For
    source
    @[simp]
    theorem Cslib.Complexity.length_repeatVotes {α : Type} (trials width : ℕ) (V : α × List Bool → Bool) (input : α × List Bool) :
    (repeatVotes trials width V input).length = trials

    Repetition produces one vote for each prescribed trial, even on a short tape.

    source
    theorem Cslib.Complexity.repeatVotes_ofFn {α : Type} {trials width : ℕ} {V : α × List Bool → Bool} (a : α) (x : BitString (trials * width)) :
    repeatVotes trials width V (a, List.ofFn x) = List.ofFn fun (i : Fin trials) => V (a, List.ofFn (BitString.block x i))

    On a full tape, votes are evaluations on its finite blocks, in order.

    source
    theorem Cslib.Complexity.computableInPolyTime_repeatVotes {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {trials width : α × List Bool → ℕ} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (htrials : Turing.MultiTapeTM.ComputableInPolyTime trials (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) (hwidth : Turing.MultiTapeTM.ComputableInPolyTime width (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (input : α × List Bool) => repeatVotes (trials input) (width input) V input) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

    Producing votes takes polynomial time when the verifier and the unary dimensions do. The dimensions may depend on the complete input, and output uses the raw bit-list encoding.

    source
    def Cslib.Complexity.repeatMajority {α : Type} (enc : α ↪ List Bool) (r p : Polynomial ℕ) (V : α × List Bool → Bool) (x : α × List Bool) :
    Bool

    The strict majority of 2 r(n) runs of V, where n is the length of the encoded instance: the random string is cut into 2 r(n) rows of p(n) bits (Cslib.BitString.listRows), V runs on each row, and the answer is true when more than r(n) runs accept. Bits missing from a short random string read as false.

    Instances For
      source
      theorem Cslib.Complexity.computableInPolyTime_repeatMajority {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (r p : Polynomial ℕ) :
      Turing.MultiTapeTM.ComputableInPolyTime (repeatMajority enc r p V) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

      Majority votes of a polynomial-time decider take polynomial time.

      source
      theorem Cslib.Complexity.repeatMajority_ofFn {α : Type} {enc : α ↪ List Bool} {r p : Polynomial ℕ} {V : α × List Bool → Bool} (a : α) (x : BitString (2 * Polynomial.eval (enc a).length r * Polynomial.eval (enc a).length p)) :
      repeatMajority enc r p V (a, List.ofFn x) = decide (Polynomial.eval (enc a).length r < {i : Fin (2 * Polynomial.eval (enc a).length r) | V (a, List.ofFn (BitString.block x i)) = true}.card)

      On a random string of 2 r(n) rows of p(n) bits, the majority vote compares the number of accepting rows with r(n).

      source
      def Cslib.Complexity.repeatAny {α : Type} (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) (x : α × List Bool) :
      Bool

      The disjunction of q(n) runs of V, where n is the length of the encoded instance: the random string is cut into q(n) rows of p(n) bits (Cslib.BitString.listRows), V runs on each row, and the answer is true when some run accepts. Bits missing from a short random string read as false.

      Instances For
        source
        theorem Cslib.Complexity.computableInPolyTime_repeatAny {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (q p : Polynomial ℕ) :
        Turing.MultiTapeTM.ComputableInPolyTime (repeatAny enc q p V) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

        Repeating a polynomial-time decider takes polynomial time.

        source
        theorem Cslib.Complexity.repeatAny_ofFn_eq_true_iff {α : Type} {enc : α ↪ List Bool} {q p : Polynomial ℕ} {V : α × List Bool → Bool} (a : α) (x : BitString (Polynomial.eval (enc a).length q * Polynomial.eval (enc a).length p)) :
        repeatAny enc q p V (a, List.ofFn x) = true ↔ ∃ (i : Fin (Polynomial.eval (enc a).length q)), V (a, List.ofFn (BitString.block x i)) = true

        On a random string of q(n) rows of p(n) bits, the repetition accepts when some row is accepted.