Documentation

CslibFrontier.Computability.Complexity.Classes.Hierarchy.Time

The time hierarchy theorem #

The deterministic time class Cslib.Complexity.DTIME enc t of CslibFrontier.Computability.Complexity.Classes.Time consists of the problems that some machine with a binary alphabet and finitely many states decides within time c₁ * t n + c₂, for constants c₁ and c₂, on instances whose encoding under enc has length n. A bound t is time-constructible (Cslib.Complexity.TimeConstructible) when such a machine computes t n in binary from any word of length n within time O(t n); so are 2 ^ n and (n + 1) ^ k for k ≥ 2. These definitions and their generic API are in CslibFrontier.Computability.Complexity.Classes.Constructible.

The time hierarchy theorem #

The clocked diagonal Cslib.Complexity.clockedDiagonal J of CslibFrontier.Computability.Complexity.Classes.Hierarchy runs the machine described at the start of its input x on x for J x.length steps with the universal function, and negates the verdict; the diagonal function Cslib.Complexity.diagonal has the clock 2 ^ n. Cslib.Complexity.timeDiagonal J applies it only when the framed description is short, 2 ^ |unframe x| ≤ |x| (Cslib.Complexity.Diagonal.shortDesc, in CslibFrontier.Computability.Complexity.Classes.Hierarchy.ShortDesc), and answers false otherwise. Decoding a description of L bits takes time polynomial in L, of a degree fixed by the decoder, hence O(2 ^ L), which is O(n) on short descriptions; padded descriptions are short.

The resource estimate used here bounds J simulated steps by O(B ^ 5 * J ^ 3), where B bounds the encoded description, input and clock length. This weakens the sharper O((B + 1) ^ 4 * J ^ 2) bound (Turing.MultiTapeTM.Universal.universal_bounds_le), so the problem decided by timeDiagonal J is in DTIME ((n + 1) ^ 5 * (J n + 1) ^ 3) for a time-constructible clock J (Cslib.Complexity.setOf_timeDiagonal_mem_DTIME). It is not in DTIME f when every c * f n + c is eventually below J n, by the diagonal argument (Cslib.Complexity.setOf_timeDiagonal_notMem_DTIME). In fact each constant need only be beaten at arbitrarily large lengths (Cslib.Complexity.setOf_timeDiagonal_notMem_DTIME_of_frequently_le); this also yields noninclusion when the bounds are incomparable at other lengths. Hence DTIME f ⊂ DTIME g Arora and Barak, Theorem 3.1, Sipser, Theorem 9.10:

The polynomial gap is the overhead of the polynomial-certificate universal interpreter, which is polynomial in the description and in the clock. Hierarchy.TimePolylog uses the O(t log t) universal simulation instead and narrows the gap to a polylogarithmic factor: g need only eventually exceed n + (log (n + 1) + 1) ^ k * (J n + 1) * (log (J n + 1) + 1) for an absolute constant k, or (f n + 1) * (log (f n + 1) + 1) ^ k for a time-constructible f. The textbook gap f n * log (f n) = o(g n) needs the diagonal to clock the universal machine's own steps and is not claimed. Hierarchy.LogClock reduces the clock inflation to f n * (Nat.size (f n) + 1). Hierarchy.Polynomial uses native padding to prove strictness between every pair of distinct positive integer polynomial degrees, despite this interpreter overhead.

Main definitions #

Main results #

References #

The clocked diagonal #

source
def Cslib.Complexity.timeDiagonal (J : ℕ → ℕ) (x : List Bool) :
Bool

The clocked diagonal on short descriptions. The clocked diagonal Cslib.Complexity.clockedDiagonal J when the description framed at the start of x is short (Cslib.Complexity.Diagonal.shortDesc), and false otherwise.

Instances For
    source
    theorem Cslib.Complexity.computableInO_timeDiagonal {J : ℕ → ℕ} (hJ : TimeConstructible J) :
    Turing.MultiTapeTM.ComputableInO (timeDiagonal J) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool (fun (x : List Bool) => (x.length + 1) ^ 5 * (J x.length + 1) ^ 3) fun (x : List Bool) => (x.length + 1) ^ 5 * (J x.length + 1) ^ 3

    The clocked diagonal is computable within the time of the universal machine: within time and space O((n + 1) ^ 5 * (J n + 1) ^ 3) on inputs of length n, for a time-constructible clock J, charging the shortness test, decoding, the symbols, the clock, the universal run and the test.

    source
    theorem Cslib.Complexity.setOf_timeDiagonal_notMem_DTIME_of_frequently_le {f J : ℕ → ℕ} (hJ : ∀ (c : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ J n) :
    {x : List Bool | timeDiagonal J x = true} ∉ DTIME Turing.MultiTapeTM.encBits f

    Diagonalization at arbitrarily large favorable lengths. The clock need only dominate each linear bound infinitely often. A description can be padded to every sufficiently large length, so the diagonal argument does not require eventual domination or monotonicity.

    source
    theorem Cslib.Complexity.setOf_timeDiagonal_notMem_DTIME {f J : ℕ → ℕ} (hJ : ∀ (c : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ J n) :
    {x : List Bool | timeDiagonal J x = true} ∉ DTIME Turing.MultiTapeTM.encBits f

    The diagonal argument for time. Eventual domination of every linear time bound is a sufficient special case of diagonalization at arbitrarily large favorable lengths.

    source
    theorem Cslib.Complexity.setOf_timeDiagonal_mem_DTIME {J : ℕ → ℕ} (hJ : TimeConstructible J) :
    {x : List Bool | timeDiagonal J x = true} ∈ DTIME Turing.MultiTapeTM.encBits fun (n : ℕ) => (n + 1) ^ 5 * (J n + 1) ^ 3

    The problem of the clocked diagonal is decidable within time O((n + 1) ^ 5 * (J n + 1) ^ 3).

    The time hierarchy theorem #

    source
    theorem Cslib.Complexity.DTIME_not_subset_DTIME_of_clock {f g J : ℕ → ℕ} (hJ : TimeConstructible J) (hfJ : ∀ (c : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ J n) (hg : ∀ᶠ (n : ℕ) in Filter.atTop, (n + 1) ^ 5 * (J n + 1) ^ 3 ≤ g n) :
    ¬DTIME Turing.MultiTapeTM.encBits g ⊆ DTIME Turing.MultiTapeTM.encBits f

    Time-class noninclusion from a clock. Infinitely many favorable lengths for each constant suffice to separate the upper class from DTIME f. Unlike strict inclusion, this statement needs no comparison between f and g at the other lengths.

    source
    theorem Cslib.Complexity.DTIME_ssubset_DTIME_of_frequently_clock {f g J : ℕ → ℕ} (hJ : TimeConstructible J) (hfJ : ∀ (c : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ J n) (hfg : ∀ᶠ (n : ℕ) in Filter.atTop, f n ≤ g n) (hg : ∀ᶠ (n : ℕ) in Filter.atTop, (n + 1) ^ 5 * (J n + 1) ^ 3 ≤ g n) :
    DTIME Turing.MultiTapeTM.encBits f ⊂ DTIME Turing.MultiTapeTM.encBits g

    A hierarchy for irregular bounds. The clock must dominate the lower bound only infinitely often for each constant. Eventual f ≤ g supplies the inclusion separately.

    source
    theorem Cslib.Complexity.DTIME_ssubset_DTIME_of_clock {f g J : ℕ → ℕ} (hJ : TimeConstructible J) (hfJ : ∀ (c : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ J n) (hg : ∀ᶠ (n : ℕ) in Filter.atTop, (n + 1) ^ 5 * (J n + 1) ^ 3 ≤ g n) :
    DTIME Turing.MultiTapeTM.encBits f ⊂ DTIME Turing.MultiTapeTM.encBits g

    The time hierarchy theorem, for a clock. If a time-constructible clock J eventually exceeds every c * f n + c, then DTIME f is strictly contained in every DTIME g with (n + 1) ^ 5 * (J n + 1) ^ 3 ≤ g n eventually Arora and Barak, Theorem 3.1.

    source
    theorem Cslib.Complexity.DTIME_ssubset_DTIME {f g : ℕ → ℕ} (hf : TimeConstructible f) (hn : ∀ (n : ℕ), n ≤ f n) (hg : ∀ᶠ (n : ℕ) in Filter.atTop, (n + 1) ^ 8 * (f n + 1) ^ 3 ≤ g n) :
    DTIME Turing.MultiTapeTM.encBits f ⊂ DTIME Turing.MultiTapeTM.encBits g

    The time hierarchy theorem. If f is time-constructible and n ≤ f n, then DTIME f is strictly contained in every DTIME g with (n + 1) ^ 8 * (f n + 1) ^ 3 ≤ g n eventually Arora and Barak, Theorem 3.1, Sipser, Theorem 9.10. The gap is the polynomial overhead of the polynomial-certificate universal interpreter; Cslib.Complexity.exists_DTIME_ssubset_DTIME_polylog narrows it to a polylogarithmic factor.