Constructible resource bounds

A time- or space-constructible bound is computed in binary from a word of length n by one finite-state binary-alphabet machine, within O(t n) time or O(s n) work space respectively. The input tape is read-only and the output tape write-only. Neither definition imposes a lower bound on the resource function; hierarchy theorems state the lower bounds they need separately.

The shared length and arithmetic routines give concrete constructible bounds, without importing any hierarchy theorem. The length of a word in binary, computed in linear time (Turing.MultiTapeTM.ComputableInO.lengthNat), and the bounds on binary digits (Turing.MultiTapeTM.exists_pow_length_encNat_le) are in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible; unary word length is supplied by the quantitative API (Turing.MultiTapeTM.ComputableInO.lengthUnary).

Main definitions

• Cslib.Complexity.TimeConstructible: time-constructible bounds.
• Cslib.Complexity.SpaceConstructible: space-constructible bounds.

Main results

• Cslib.Complexity.TimeConstructible.spaceConstructible: time constructibility implies space constructibility.
• Cslib.Complexity.timeConstructible_const, Cslib.Complexity.timeConstructible_id, Cslib.Complexity.timeConstructible_succ, Cslib.Complexity.timeConstructible_two_pow, Cslib.Complexity.timeConstructible_two_pow_two_pow, Cslib.Complexity.timeConstructible_succ_pow, Cslib.Complexity.TimeConstructible.succ, Cslib.Complexity.TimeConstructible.succ_mul: time-constructible bounds.
• Cslib.Complexity.spaceConstructible_const, Cslib.Complexity.spaceConstructible_id, Cslib.Complexity.spaceConstructible_succ, Cslib.Complexity.spaceConstructible_succ_pow, Cslib.Complexity.spaceConstructible_two_pow, Cslib.Complexity.spaceConstructible_two_pow_two_pow: space-constructible bounds.

References

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

def Cslib.Complexity.TimeConstructible (t : ℕ → ℕ) : Prop

A bound t is time-constructible when some machine with a binary alphabet and finitely many states computes t n in binary from any word of length n within time O(t n). Arora and Barak also ask for n ≤ t n Arora and Barak, Section 1.3; this definition omits that condition, and the results that need it, such as Cslib.Complexity.DTIME_ssubset_DTIME, assume it separately.

theorem Cslib.Complexity.TimeConstructible.computableInO {t : ℕ → ℕ} (ht : TimeConstructible t) : Turing.MultiTapeTM.ComputableInO (fun (x : List Bool) => t x.length) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat (fun (x : List Bool) => t x.length) fun (x : List Bool) => t x.length

A time-constructible bound is computed within time and space O(t n).

theorem Cslib.Complexity.TimeConstructible.of_computableInO {t : ℕ → ℕ} {T S : List Bool → ℕ} {s : ℕ → ℕ} (c : ℕ) (h : Turing.MultiTapeTM.ComputableInO (fun (x : List Bool) => t x.length) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat T S) (hT : ∀ (x : List Bool), T x ≤ c * t x.length + c) (hS : ∀ (x : List Bool), S x ≤ s x.length) : TimeConstructible t

A computation of t n in binary within time O(t n) makes t time-constructible.

theorem Cslib.Complexity.TimeConstructible.succ {t : ℕ → ℕ} (ht : TimeConstructible t) : TimeConstructible fun (n : ℕ) => t n + 1

Adding one to a time-constructible bound preserves time constructibility.

theorem Cslib.Complexity.timeConstructible_const (c : ℕ) : TimeConstructible fun (x : ℕ) => c

Constant bounds are time-constructible.

theorem Cslib.Complexity.timeConstructible_id : TimeConstructible fun (n : ℕ) => n

n is time-constructible: count the length of the word in binary, in linear time.

theorem Cslib.Complexity.timeConstructible_succ : TimeConstructible fun (n : ℕ) => n + 1

n + 1 is time-constructible.

theorem Cslib.Complexity.timeConstructible_two_pow : TimeConstructible fun (x : ℕ) => 2 ^ x

2 ^ n is time-constructible: its binary digits are n zeros followed by a one.

theorem Cslib.Complexity.timeConstructible_two_pow_two_pow : TimeConstructible fun (n : ℕ) => 2 ^ 2 ^ n

2 ^ (2 ^ n) is time-constructible: count 2 ^ n in unary and then write 2 ^ (2 ^ n) in binary as 2 ^ n zeros followed by a one.

theorem Cslib.Complexity.TimeConstructible.succ_mul_of_computableInO {f : ℕ → ℕ} {T : List Bool → ℕ} {S : ℕ → ℕ} (c : ℕ) (hf : Turing.MultiTapeTM.ComputableInO (fun (x : List Bool) => f x.length) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat T fun (x : List Bool) => S x.length) (hT : ∀ (x : List Bool), T x ≤ c * ((x.length + 1) * f x.length) + c) (hn : ∀ (n : ℕ), n ≤ f n) : TimeConstructible fun (n : ℕ) => (n + 1) * f n

If f n is computed in binary from words of length n within time O((n + 1) * f n) and n ≤ f n, then (n + 1) * f n is time-constructible: writing the length of the word in binary takes linear time, and the product time polylogarithmic in the factors.

theorem Cslib.Complexity.TimeConstructible.succ_mul {f : ℕ → ℕ} (hf : TimeConstructible f) (hn : ∀ (n : ℕ), n ≤ f n) : TimeConstructible fun (n : ℕ) => (n + 1) * f n

If f is time-constructible and n ≤ f n, then so is (n + 1) * f n.

theorem Cslib.Complexity.timeConstructible_succ_pow (k : ℕ) : TimeConstructible fun (n : ℕ) => (n + 1) ^ k

(n + 1) ^ k is time-constructible.

theorem Cslib.Complexity.timeConstructible_succ_sq : TimeConstructible fun (n : ℕ) => (n + 1) ^ 2

(n + 1) ^ 2 is time-constructible.

Space-constructible bounds

def Cslib.Complexity.SpaceConstructible (s : ℕ → ℕ) : Prop

A bound s is space-constructible when some machine with a binary alphabet and finitely many states computes s n in binary from any word of length n within space O(s n), halting Sipser, Definition 9.1. Unlike Sipser, Definition 9.1, s n ≥ log n is not required here; the space hierarchy theorem asks for ⌊log₂ n⌋ ≤ s n separately.

theorem Cslib.Complexity.SpaceConstructible.computableInO {s : ℕ → ℕ} (hs : SpaceConstructible s) : ∃ (T : List Bool → ℕ), Turing.MultiTapeTM.ComputableInO (fun (x : List Bool) => s x.length) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat T fun (x : List Bool) => s x.length

A space-constructible bound is computed within space O(s n), within some time.

theorem Cslib.Complexity.TimeConstructible.spaceConstructible {t : ℕ → ℕ} (ht : TimeConstructible t) : SpaceConstructible t

A time-constructible bound is space-constructible, since space is at most time.

theorem Cslib.Complexity.SpaceConstructible.of_computableInO {s : ℕ → ℕ} {T S : List Bool → ℕ} (c : ℕ) (h : Turing.MultiTapeTM.ComputableInO (fun (x : List Bool) => s x.length) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat T S) (hS : ∀ (x : List Bool), S x ≤ c * s x.length + c) : SpaceConstructible s

A computation of s n in binary within space O(s n) makes s space-constructible: it halts within a time bound of n, its number of configurations.

theorem Cslib.Complexity.spaceConstructible_id : SpaceConstructible fun (n : ℕ) => n

n is space-constructible: count the length of the word in binary.

theorem Cslib.Complexity.spaceConstructible_succ : SpaceConstructible fun (n : ℕ) => n + 1

n + 1 is space-constructible.

theorem Cslib.Complexity.spaceConstructible_const (c : ℕ) : SpaceConstructible fun (x : ℕ) => c

Constant bounds are space-constructible, in zero space.

theorem Cslib.Complexity.spaceConstructible_succ_pow (k : ℕ) : SpaceConstructible fun (n : ℕ) => (n + 1) ^ k

(n + 1) ^ k is space-constructible.

theorem Cslib.Complexity.spaceConstructible_two_pow : SpaceConstructible fun (x : ℕ) => 2 ^ x

2 ^ n is space-constructible.

theorem Cslib.Complexity.spaceConstructible_two_pow_two_pow : SpaceConstructible fun (n : ℕ) => 2 ^ 2 ^ n

2 ^ (2 ^ n) is space-constructible.