Documentation

CslibFrontier.Computability.Complexity.Classes.Time

Time classes #

The three parametric time classes, each relative to an encoding enc : α ↪ List Bool of instances, with a bound t : ℕ → ℕ of the length n of the encoded instance, up to constants c₁ * t n + c₂:

The unbounded-error class Cslib.Complexity.PPTIME enc t, decided by strict majority by the same fair-coin machines, is in CslibFrontier.Computability.Complexity.Classes.PP.Time.

Each polynomial class of the library is the union of the corresponding classes of time O(n ^ k), as in the textbook Arora and Barak, Definition 1.13, Theorem 2.6, Definition 7.2: P (Cslib.Complexity.mem_P_iff_exists_mem_DTIME), NP (Cslib.Complexity.mem_NP_iff_exists_mem_NTIME, through the machine characterisation Cslib.Complexity.mem_NP_iff_decidableInPolyTime) and BPP (Cslib.Complexity.mem_BPP_iff_exists_mem_BPTIME). For BPP, defined by polynomial-time verifiers reading random strings, this is the characterisation by probabilistic machines: a verifier is run on sampled coins by a fair-coin machine compiled with a halting polynomial clock (Cslib.Probability.IsPPTOn.exists_halting_machine), and a fair-coin machine halting within T steps is a verifier replaying T coins (Turing.MultiTapePTM.computableInPolyTime_decide_runClosedCoins).

Timed reductions #

A problem B decidable within time O(t' m) on instances of length m pulls back along a function g computable within time O(T a) to a problem decidable within time O(T a + t' |encB (g a)|) (Cslib.Complexity.preimage_mem_DTIME): compute g a, then decide whether it is in B. A decider of B within time O(t' m) gives a plain ComputableInO certificate within time and space O(t' m) (Cslib.Complexity.computableInO_indicator_of_mem_DTIME), in which computations compose.

Main definitions #

Main results #

References #

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

machine decides A with bounded error 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 the run outputs [true] if a ∈ A, and [false] otherwise, with probability at least 2 / 3.

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

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

    Deterministic time #

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

    The problems decidable 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 machine with a binary alphabet and finitely many states, with any space bound Arora and Barak, Definition 1.12.

    Instances For
      source
      theorem Cslib.Complexity.DTIME_mono_of_le_mul_add {α : Type u_1} {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} {C : ℕ} (h : ∀ (n : ℕ), t₁ n ≤ C * t₂ n + C) :
      DTIME enc t₁ ⊆ DTIME enc t₂

      DTIME absorbs constant factors: a bound t₁ n ≤ C * t₂ n + C puts DTIME enc t₁ inside DTIME enc t₂.

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

      DTIME is monotone in the time bound.

      source
      theorem Cslib.Complexity.DTIME_mono_of_eventually_le {α : Type u_1} {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} (h : ∀ᶠ (n : ℕ) in Filter.atTop, t₁ n ≤ t₂ n) :
      DTIME enc t₁ ⊆ DTIME enc t₂

      DTIME only depends on the time bound eventually: the finitely many other values are absorbed by the additive constant.

      source
      theorem Cslib.Complexity.setOf_mem_DTIME_of_computableInO {α : Type u_1} {enc : α ↪ List Bool} {f : α → Bool} {T S : α → ℕ} {t : ℕ → ℕ} (h : Turing.MultiTapeTM.ComputableInO f enc Turing.MultiTapeTM.encBool T S) (hT : ∀ (a : α), T a ≤ t (enc a).length) :
      {a : α | f a = true} ∈ DTIME enc t

      A Boolean function, computable within a time bound of the length of the encoded instance, decides a problem within that time.

      source
      theorem Cslib.Complexity.computableInO_indicator_of_mem_DTIME {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} (h : A ∈ DTIME enc t) :
      Turing.MultiTapeTM.ComputableInO (Turing.MultiTapeTM.indicator A) enc Turing.MultiTapeTM.encBool (fun (a : α) => t (enc a).length) fun (a : α) => t (enc a).length

      A problem in DTIME enc t is decided by a machine computing its indicator within time and space O(t n), on instances whose encoding has length n.

      source
      theorem Cslib.Complexity.preimage_mem_DTIME {α β : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {B : Set β} {t' t : ℕ → ℕ} {g : α → β} {T S : α → ℕ} {C : ℕ} (hB : B ∈ DTIME encB t') (hg : Turing.MultiTapeTM.ComputableInO g enc encB T S) (ht : ∀ (a : α), T a + t' (encB (g a)).length ≤ C * t (enc a).length + C) :
      g ⁻¹' B ∈ DTIME enc t

      DTIME under timed reductions. If B is decidable within time O(t' m) on instances whose encoding has length m, and g is computable within time O(T a), then g ⁻¹' B is decidable within time O(t n) on instances whose encoding has length n, as soon as T a + t' |encB (g a)| is within O(t |enc a|): compute g a, then decide whether it is in B.

      Nondeterministic time #

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

      The problems decidable 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 nondeterministic machine with a binary alphabet and finitely many states: every computation path of that many steps has halted, and a ∈ A exactly when some computation path halts with output [true] Arora and Barak, Definition 2.5.

      Instances For
        source
        theorem Cslib.Complexity.NTIME_mono_of_le_mul_add {α : Type u_1} {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} {C : ℕ} (h : ∀ (n : ℕ), t₁ n ≤ C * t₂ n + C) :
        NTIME enc t₁ ⊆ NTIME enc t₂

        NTIME absorbs constant factors: a bound t₁ n ≤ C * t₂ n + C puts NTIME enc t₁ inside NTIME enc t₂.

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

        NTIME is monotone in the time bound.

        source
        theorem Cslib.Complexity.NTIME_mono_of_eventually_le {α : Type u_1} {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} (h : ∀ᶠ (n : ℕ) in Filter.atTop, t₁ n ≤ t₂ n) :
        NTIME enc t₁ ⊆ NTIME enc t₂

        NTIME only depends on the time bound eventually.

        source
        theorem Cslib.Complexity.DTIME_subset_NTIME {α : Type u_1} {enc : α ↪ List Bool} {t : ℕ → ℕ} :
        DTIME enc t ⊆ NTIME enc t

        A deterministic machine is a nondeterministic machine, with one computation path, which accepts exactly when the deterministic machine halts with output [true].

        Bounded-error probabilistic time #

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

        The problems decidable with bounded error 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 outputs the right answer with probability at least 2 / 3 Arora and Barak, Definition 7.2.

        Instances For
          source
          theorem Cslib.Complexity.BPTIME_mono_of_le_mul_add {α : Type u_1} {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} {C : ℕ} (h : ∀ (n : ℕ), t₁ n ≤ C * t₂ n + C) :
          BPTIME enc t₁ ⊆ BPTIME enc t₂

          BPTIME absorbs constant factors: a bound t₁ n ≤ C * t₂ n + C puts BPTIME enc t₁ inside BPTIME enc t₂.

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

          BPTIME is monotone in the time bound.

          source
          theorem Cslib.Complexity.BPTIME_mono_of_eventually_le {α : Type u_1} {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} (h : ∀ᶠ (n : ℕ) in Filter.atTop, t₁ n ≤ t₂ n) :
          BPTIME enc t₁ ⊆ BPTIME enc t₂

          BPTIME only depends on the time bound eventually.

          The polynomial classes #

          source
          theorem Cslib.Complexity.mem_P_iff_exists_mem_DTIME {α : Type u_2} {enc : α ↪ List Bool} {A : Set α} :
          A ∈ P enc ↔ ∃ (k : ℕ), A ∈ DTIME enc fun (x : ℕ) => x ^ k

          P is the union of the classes DTIME (n ^ k), the definition of P in the classes proposed upstream Arora and Barak, Definition 1.13.

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

          NP is the union of the classes NTIME (n ^ k), through the characterisation of NP by nondeterministic machines Arora and Barak, Theorem 2.6.

          Bounded-error polynomial time #

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

          BPP is the union of the classes BPTIME (n ^ k) Arora and Barak, Definition 7.2, Section 7.1: 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.