Exponential time complexity classes

This file defines EXP and NEXP, the exponential-time analogues of P and NP respectively.

def Complexity.EXP : Set Language

EXP is the class of languages decidable by a deterministic TM in exponential time: EXP = ⋃_k DTIME(2^(n^k)).

Equations

• Complexity.EXP = ⋃ (k : ℕ), Complexity.DTIME fun (n : ℕ) => 2 ^ n ^ k

def Complexity.NEXP : Set Language

NEXP is the class of languages decidable by a nondeterministic TM in exponential time: NEXP = ⋃_k NTIME(2^(n^k)).

Equations

• Complexity.NEXP = ⋃ (k : ℕ), Complexity.NTIME fun (n : ℕ) => 2 ^ n ^ k