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_computableInPolyTime_pad): the padding is written and Ψ run in time 2 ^ O(|y|) (Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_pad).

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.DTIME_two_pow_subset_EXP, Cslib.Complexity.NTIME_two_pow_subset_NEXP: time 2 ^ h n for a polynomially bounded h is exponential time.
• Cslib.Complexity.P_ssubset_EXP: polynomial time is strictly within exponential time.
• Cslib.Complexity.compl_mem_E, Cslib.Complexity.compl_mem_EXP: closure under complement.
• Cslib.Complexity.setOf_mem_E_of_computableInPolyTime_pad: polynomial time on inputs padded to length 2 ^ n gives E.
• Cslib.Complexity.PolyTimeReducible.mem_EXP: EXP is closed under polynomial-time many-one reductions.

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.DTIME_two_pow_subset_EXP {α : Type u_1} {enc : α ↪ List Bool} {h : ℕ → ℕ} (hh : PolynomiallyBounded h) : (DTIME enc fun (n : ℕ) => 2 ^ h n) ⊆ EXP enc

Deterministic time 2 ^ h n, for a polynomially bounded exponent h, is within exponential time.

theorem Cslib.Complexity.NTIME_two_pow_subset_NEXP {α : Type u_1} {enc : α ↪ List Bool} {h : ℕ → ℕ} (hh : PolynomiallyBounded h) : (NTIME enc fun (n : ℕ) => 2 ^ h n) ⊆ NEXP enc

Nondeterministic time 2 ^ h n, for a polynomially bounded exponent h, is within nondeterministic exponential time.

theorem Cslib.Complexity.compl_mem_E {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : A ∈ E enc) : Aᶜ ∈ E enc

E is closed under complement (Cslib.Complexity.compl_mem_DTIME).

theorem Cslib.Complexity.compl_mem_EXP {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : A ∈ EXP enc) : Aᶜ ∈ EXP enc

EXP is closed under complement (Cslib.Complexity.compl_mem_DTIME).

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_computableInPolyTime_pad {Ψ : List Bool × ℕ → Bool} (hΨ : Turing.MultiTapeTM.ComputableInPolyTime Ψ (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: writing the padding 2 ^ |y| and running Ψ takes time C 2 ^ (D |y|) (|y| + 1) ^ D (Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_pad), which is 2 ^ O(|y|).

theorem Cslib.Complexity.PolyTimeReducible.mem_EXP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hAB : PolyTimeReducible encA encB A B) (hB : B ∈ EXP encB) : A ∈ EXP encA

EXP is closed under polynomial-time many-one reductions.