Exponential time

Cslib.Complexity.EXP enc is the union of the deterministic time classes Cslib.Complexity.DTIME enc (2 ^ n ^ k) over k, and Cslib.Complexity.E enc the union of the classes DTIME enc (2 ^ (k * n)), as in the classes proposed upstream in cslib pull request #767. Their nondeterministic counterparts Cslib.Complexity.NEXP enc and Cslib.Complexity.NE enc are the unions of the classes Cslib.Complexity.NTIME enc (2 ^ n ^ k) and NTIME enc (2 ^ (k * n)) Arora and Barak, Sections 2.1 and 2.6.

P is the union of the classes DTIME (n ^ k) (Cslib.Complexity.mem_P_iff_exists_mem_DTIME) and NP that of the classes NTIME (n ^ k) (Cslib.Complexity.mem_NP_iff_exists_mem_NTIME), so P ⊆ E ⊆ EXP, NP ⊆ NE ⊆ NEXP, and each deterministic class is within its nondeterministic counterpart (Cslib.Complexity.DTIME_subset_NTIME).

The inclusion P ⊆ EXP is strict for problems on bit words (Cslib.Complexity.P_ssubset_EXP): the diagonal problem of Cslib.Complexity.diagonal is decided within time O(2 ^ (4 * n)), which is within 2 ^ n ^ 2 from n = 4 on, and is not in P by the diagonal argument of the time hierarchy theorem Arora and Barak, Theorem 3.1, Sipser, Theorem 9.10.

Polynomial-time computation on a bit word y paired with unary padding 2 ^ |y| gives a problem in E (Cslib.Complexity.setOf_mem_E_of_computableTidilyInPolyTime_pad), by writing the padding in exponential time and applying the timed-reduction API.

Main definitions

• Cslib.Complexity.E, Cslib.Complexity.EXP: deterministic exponential time.
• Cslib.Complexity.NE, Cslib.Complexity.NEXP: nondeterministic exponential time.

Main results

• Cslib.Complexity.P_subset_E, Cslib.Complexity.E_subset_EXP, Cslib.Complexity.P_subset_EXP: polynomial time is within exponential time.
• Cslib.Complexity.NP_subset_NE, Cslib.Complexity.NE_subset_NEXP, Cslib.Complexity.NP_subset_NEXP: the same for nondeterministic time.
• Cslib.Complexity.E_subset_NE, Cslib.Complexity.EXP_subset_NEXP: determinism is a special case.
• Cslib.Complexity.P_ssubset_EXP: polynomial time is strictly within exponential time.
• Cslib.Complexity.setOf_mem_E_of_computableTidilyInPolyTime_pad: polynomial time on inputs padded to length 2 ^ n gives E.

References

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

def Cslib.Complexity.EXP {α : Type u_1} (enc : α ↪ List Bool) : Set (Set α)

The problems decidable within time O(2 ^ n ^ k) for some k, on instances whose encoding under enc has length n Arora and Barak, Section 2.6.

theorem Cslib.Complexity.mem_EXP_iff {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : A ∈ EXP enc ↔ ∃ (k : ℕ), A ∈ DTIME enc fun (n : ℕ) => 2 ^ n ^ k

def Cslib.Complexity.E {α : Type u_1} (enc : α ↪ List Bool) : Set (Set α)

The problems decidable within time O(2 ^ (k * n)) for some k, on instances whose encoding under enc has length n.

theorem Cslib.Complexity.mem_E_iff {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : A ∈ E enc ↔ ∃ (k : ℕ), A ∈ DTIME enc fun (n : ℕ) => 2 ^ (k * n)

def Cslib.Complexity.NEXP {α : Type u_1} (enc : α ↪ List Bool) : Set (Set α)

The problems decidable by a nondeterministic machine within time O(2 ^ n ^ k) for some k, on instances whose encoding under enc has length n Arora and Barak, Section 2.6.

theorem Cslib.Complexity.mem_NEXP_iff {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : A ∈ NEXP enc ↔ ∃ (k : ℕ), A ∈ NTIME enc fun (n : ℕ) => 2 ^ n ^ k

def Cslib.Complexity.NE {α : Type u_1} (enc : α ↪ List Bool) : Set (Set α)

The problems decidable by a nondeterministic machine within time O(2 ^ (k * n)) for some k, on instances whose encoding under enc has length n.

theorem Cslib.Complexity.mem_NE_iff {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : A ∈ NE enc ↔ ∃ (k : ℕ), A ∈ NTIME enc fun (n : ℕ) => 2 ^ (k * n)

theorem Cslib.Complexity.P_subset_E {α : Type u_1} {enc : α ↪ List Bool} : P enc ⊆ E enc

Polynomial time is within linear exponential time.

theorem Cslib.Complexity.E_subset_EXP {α : Type u_1} {enc : α ↪ List Bool} : E enc ⊆ EXP enc

Linear exponential time is within exponential time.

theorem Cslib.Complexity.NP_subset_NE {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ NE enc

Nondeterministic polynomial time is within nondeterministic linear exponential time.

theorem Cslib.Complexity.NE_subset_NEXP {α : Type u_1} {enc : α ↪ List Bool} : NE enc ⊆ NEXP enc

Nondeterministic linear exponential time is within nondeterministic exponential time.

theorem Cslib.Complexity.NP_subset_NEXP {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ NEXP enc

Nondeterministic polynomial time is within nondeterministic exponential time.

theorem Cslib.Complexity.E_subset_NE {α : Type u_1} {enc : α ↪ List Bool} : E enc ⊆ NE enc

Linear exponential time is within nondeterministic linear exponential time.

theorem Cslib.Complexity.EXP_subset_NEXP {α : Type u_1} {enc : α ↪ List Bool} : EXP enc ⊆ NEXP enc

Exponential time is within nondeterministic exponential time.

theorem Cslib.Complexity.P_subset_EXP {α : Type u_1} {enc : α ↪ List Bool} : P enc ⊆ EXP enc

Polynomial time is within exponential time.

theorem Cslib.Complexity.setOf_diagonal_mem_EXP : {x : List Bool | diagonal x = true} ∈ EXP Turing.MultiTapeTM.encBits

The diagonal problem is in exponential time.

theorem Cslib.Complexity.P_ssubset_EXP : P Turing.MultiTapeTM.encBits ⊂ EXP Turing.MultiTapeTM.encBits

Polynomial time is strictly within exponential time, for problems on bit words: the diagonal problem is in EXP and not in P Arora and Barak, Theorem 3.1.

Exponential padding

theorem Cslib.Complexity.setOf_mem_E_of_computableTidilyInPolyTime_pad {Ψ : List Bool × ℕ → Bool} (hΨ : Turing.MultiTapeTM.ComputableTidilyInPolyTime Ψ (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) : {y : List Bool | Ψ (y, 2 ^ y.length) = true} ∈ E Turing.MultiTapeTM.encBits

Padding to exponential length. If Ψ is polynomial-time on pairs of a bit word and a unary number, then the words y with Ψ (y, 2 ^ |y|) form a problem in E: the padding y ↦ (y, 2 ^ |y|) is written within time O(4 ^ |y|), and the problem decided by Ψ is in DTIME (n ↦ c (n + 1) ^ d) (preimage_mem_DTIME).