The time hierarchy with a polylogarithmic gap

With the universal machine running a fixed machine for t steps within time O(t log t) (Turing.MultiTapeTM.Universal.computableInO_universal_nlogn), the clocked diagonal on short descriptions Cslib.Complexity.timeDiagonal J of Hierarchy.Time is computable within time and space O(n + (log (n + 1) + 1) ^ k * (J n + 1) * (log (J n + 1) + 1)) on inputs of length n, for a time-constructible clock J and an absolute constant k (Cslib.Complexity.exists_computableInO_timeDiagonal_polylog). On a short description, of L ≤ log n bits, the decoded description has encoded length polynomial in L, so the overhead of the universal machine, polynomial in that length, is polylogarithmic in n; the symbols are bits. Shortness and the final test are decided in linear time.

The diagonal argument of Hierarchy.Time then gives DTIME f ⊂ DTIME g Arora and Barak, Theorem 3.1, Sipser, Theorem 9.10:

• when a time-constructible clock J eventually exceeds every c * f n + c and n + (log (n + 1) + 1) ^ k * (J n + 1) * (log (J n + 1) + 1) ≤ g n eventually (Cslib.Complexity.exists_DTIME_ssubset_DTIME_of_clock_polylog), or when the clock beats each c * f n + c only at arbitrarily large lengths and f ≤ g eventually (Cslib.Complexity.exists_DTIME_ssubset_DTIME_of_frequently_clock_polylog);
• when f is time-constructible, n ≤ f n and (f n + 1) * (log (f n + 1) + 1) ^ k ≤ g n eventually (Cslib.Complexity.exists_DTIME_ssubset_DTIME_polylog), with the clock f n * (Nat.size (f n) + 1) of Hierarchy.LogClock.

Each statement asserts an absolute exponent k, chosen before the bounds. The bounds are monotone in k, so one exponent serves any finitely many of them. The gap is a polylogarithmic factor, weaker than the textbook f n * log (f n) = o(g n), which needs the diagonal to count the steps of the universal machine itself rather than those of the simulated machine. Here the exponent k comes from the polynomial overhead of the universal machine in the description and from the degree of the description decoder; for time-constructible f it also absorbs the logarithmic inflation of the clock f n * (Nat.size (f n) + 1) and the J log J term.

Main results

• Cslib.Complexity.exists_computableInO_timeDiagonal_polylog: the clocked diagonal within time O(n + polylog(n) * J log J).
• Cslib.Complexity.exists_setOf_timeDiagonal_mem_DTIME_polylog: its problem is in the corresponding class.
• Cslib.Complexity.exists_DTIME_not_subset_DTIME_of_clock_polylog, Cslib.Complexity.exists_DTIME_ssubset_DTIME_of_frequently_clock_polylog, Cslib.Complexity.exists_DTIME_ssubset_DTIME_of_clock_polylog: the time hierarchy for a clock.
• Cslib.Complexity.exists_DTIME_ssubset_DTIME_polylog: the time hierarchy for a time-constructible bound, with gap f * polylog f.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• M. Sipser, Introduction to the Theory of Computation

theorem Cslib.Complexity.exists_computableInO_timeDiagonal_polylog : ∃ (k : ℕ), ∀ {J : ℕ → ℕ}, TimeConstructible J → Turing.MultiTapeTM.ComputableInO (timeDiagonal J) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool (fun (x : List Bool) => x.length + (Nat.log 2 (x.length + 1) + 1) ^ k * ((J x.length + 1) * (Nat.log 2 (J x.length + 1) + 1))) fun (x : List Bool) => x.length + (Nat.log 2 (x.length + 1) + 1) ^ k * ((J x.length + 1) * (Nat.log 2 (J x.length + 1) + 1))

The clocked diagonal in time O(n + polylog(n) · J log J). There is an absolute constant k such that, for every time-constructible clock J, the clocked diagonal on short descriptions is computable within time and space O(n + (log (n + 1) + 1) ^ k * (J n + 1) * (log (J n + 1) + 1)) on inputs of length n. It charges the shortness test, decoding, the symbols, the clock, the O(t log t) universal run and the test.

theorem Cslib.Complexity.exists_setOf_timeDiagonal_mem_DTIME_polylog : ∃ (k : ℕ), ∀ {J : ℕ → ℕ}, TimeConstructible J → {x : List Bool | timeDiagonal J x = true} ∈ DTIME Turing.MultiTapeTM.encBits fun (n : ℕ) => n + (Nat.log 2 (n + 1) + 1) ^ k * ((J n + 1) * (Nat.log 2 (J n + 1) + 1))

The problem of the clocked diagonal is decidable within time O(n + (log (n + 1) + 1) ^ k * (J n + 1) * (log (J n + 1) + 1)), for an absolute constant k.

The time hierarchy theorem

theorem Cslib.Complexity.exists_DTIME_not_subset_DTIME_of_clock_polylog : ∃ (k : ℕ), ∀ {f g J : ℕ → ℕ}, TimeConstructible J → (∀ (c : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ J n) → (∀ᶠ (n : ℕ) in Filter.atTop, n + (Nat.log 2 (n + 1) + 1) ^ k * ((J n + 1) * (Nat.log 2 (J n + 1) + 1)) ≤ g n) → ¬DTIME Turing.MultiTapeTM.encBits g ⊆ DTIME Turing.MultiTapeTM.encBits f

Time-class noninclusion from a clock, with a polylogarithmic gap. Infinitely many favorable lengths for each constant suffice to separate the upper class from DTIME f.

theorem Cslib.Complexity.exists_DTIME_ssubset_DTIME_of_frequently_clock_polylog : ∃ (k : ℕ), ∀ {f g J : ℕ → ℕ}, TimeConstructible J → (∀ (c : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ J n) → (∀ᶠ (n : ℕ) in Filter.atTop, f n ≤ g n) → (∀ᶠ (n : ℕ) in Filter.atTop, n + (Nat.log 2 (n + 1) + 1) ^ k * ((J n + 1) * (Nat.log 2 (J n + 1) + 1)) ≤ g n) → DTIME Turing.MultiTapeTM.encBits f ⊂ DTIME Turing.MultiTapeTM.encBits g

A hierarchy for irregular bounds, with a polylogarithmic gap. The clock must dominate the lower bound only infinitely often for each constant; eventual f ≤ g supplies the inclusion.

theorem Cslib.Complexity.exists_DTIME_ssubset_DTIME_of_clock_polylog : ∃ (k : ℕ), ∀ {f g J : ℕ → ℕ}, TimeConstructible J → (∀ (c : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ J n) → (∀ᶠ (n : ℕ) in Filter.atTop, n + (Nat.log 2 (n + 1) + 1) ^ k * ((J n + 1) * (Nat.log 2 (J n + 1) + 1)) ≤ g n) → DTIME Turing.MultiTapeTM.encBits f ⊂ DTIME Turing.MultiTapeTM.encBits g

The time hierarchy theorem for a clock, with a polylogarithmic gap. There is an absolute constant k such that, 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 + (log (n + 1) + 1) ^ k * (J n + 1) * (log (J n + 1) + 1) ≤ g n eventually Arora and Barak, Theorem 3.1.

theorem Cslib.Complexity.exists_DTIME_ssubset_DTIME_polylog : ∃ (k : ℕ), ∀ {f g : ℕ → ℕ}, TimeConstructible f → (∀ (n : ℕ), n ≤ f n) → (∀ᶠ (n : ℕ) in Filter.atTop, (f n + 1) * (Nat.log 2 (f n + 1) + 1) ^ k ≤ g n) → DTIME Turing.MultiTapeTM.encBits f ⊂ DTIME Turing.MultiTapeTM.encBits g

The time hierarchy theorem, with a polylogarithmic gap. There is an absolute constant k such that, if f is time-constructible and n ≤ f n, then DTIME f is strictly contained in every DTIME g with (f n + 1) * (log (f n + 1) + 1) ^ k ≤ g n eventually Arora and Barak, Theorem 3.1, Sipser, Theorem 9.10. The gap is a polylogarithmic factor, not the textbook f n * log (f n) = o(g n).