Time-constructible functions

A function T : ℕ → ℕ is time-constructible if T(n) ≥ n and the mapping x ↦ T(|x|) can be computed by a deterministic TM in O(T(n)) time (AB Definition 1.12). The output is the binary encoding of T(|x|) via Nat.bits (LSB-first).

Time-constructibility is the standard assumption on time bounds used in the time hierarchy theorem and other separation results. Most "natural" time bounds (polynomials with T(n) ≥ n, exponentials, n log n, etc.) are time-constructible.

Main definitions

• TimeConstructible — a function T : ℕ → ℕ is time-constructible

Main results

• TimeConstructible.le_apply — T(n) ≥ n
• TimeConstructible.pos — T(n) > 0 when n > 0
• TimeConstructible.computable — extract the witnessing TM and time bound

def Complexity.TimeConstructible (T : ℕ → ℕ) : Prop

A function T : ℕ → ℕ is time-constructible (AB Definition 1.12) if T(n) ≥ n for all n, and the mapping x ↦ T(|x|) (encoded in binary via Nat.bits) can be computed by a deterministic TM in O(T(n)) time.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TimeConstructible.le_apply {T : ℕ → ℕ} (hT : TimeConstructible T) (n : ℕ) : n ≤ T n

A time-constructible function satisfies n ≤ T(n).

theorem Complexity.TimeConstructible.pos {T : ℕ → ℕ} (hT : TimeConstructible T) {n : ℕ} (hn : 0 < n) : 0 < T n

A time-constructible function is positive on positive inputs.

theorem Complexity.TimeConstructible.computable {T : ℕ → ℕ} (hT : TimeConstructible T) : ∃ (k : ℕ) (tm : TM k) (f : ℕ → ℕ), tm.ComputesInTime (fun (x : List Bool) => (T x.length).bits) f ∧ BigO f T

A time-constructible function is computable in O(T) time.