Complexity classes
Definitions of time and space complexity on machine models (P, NP, PSPACE, EXP, L, NL, the polynomial hierarchy, FPT and W[1]), polynomial-time encodings and reductions, simulation overheads, Blum measures, and inclusions and collapses among deterministic and nondeterministic classes (Savitch, Immerman–Szelepcsényi, Karp–Lipton, Ladner, Mahaney). Randomized, counting, circuit and quantum classes have their own fields.
- Blum complexity measures
- Polynomially bounded functions
- Quadratic overhead of single-tape simulation
- The classes P, NP and coNP
- Mahaney's theorem
- Polynomial time in a cost-annotated programming model
- Polynomial time on single-tape machines
- Time and space classes on multi-tape machines
- Time and space complexity classes
- Containments between time and space classes
- Parameterized complexity
- Polynomial hierarchy
- Time- and resource-bounded runs of abstract machines
TheoremImmerman-Szelepcsenyi theorem: NL = coNL#●ready to prove
The complexity class NL is closed under complementation: a decision problem \(L\) belongs to NL if and only if its complement, the decision problem that is true exactly on the bitstrings where \(L\) is false, belongs to NL.
public theorem_wanted immerman_szelepcsenyi :
NL = {L : MetaMathlibExt.ComplexityTheory.DecisionProblem | Lᶜ ∈ NL}
def NL : DecisionComplexityClass :=
{L | ∃ c, langOf L ∈ NSPACE (fun n => c * Nat.log 2 (n + 1) + c)}
CSLibExt/Computability/Complexity/Classes.lean:184
abbrev DecisionProblem := List Bool → Bool
MathlibExt/Computability/Complexity.lean:170
Sources
- N. Immerman, "Nondeterministic space is closed under complementation", SIAM Journal on Computing 17 (1988), 935-938; R. Szelepcsenyi, "The method of forced enumeration for nondeterministic automata", Acta Informatica 26 (1988), 279-284.
Uses 3
TheoremKarp-Lipton theorem: NP in P/poly collapses PH#●ready to prove
If every decision problem in NP belongs to P/poly (polynomial time with polynomial advice), then the polynomial hierarchy PH equals its second level \(\Sigma_2^p\).
public theorem_wanted karp_lipton :
MetaMathlibExt.ComplexityTheory.NP ⊆ PPoly → PH = SigmaK 2
def NP : DecisionComplexityClass :=
{ L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
IsPolyTime R ∧
∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }
MathlibExt/Computability/Complexity.lean:200
def PPoly : DecisionComplexityClass :=
{L | ∃ p : Polynomial ℕ, ∃ advice : ℕ → List Bool,
(∀ n, (advice n).length ≤ p.eval n) ∧
∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
∀ x, L x ↔ R (x, advice x.length) = true}
CSLibExt/Computability/Complexity/Classes.lean:222
def PH : DecisionComplexityClass := ⋃ k, SigmaK k
CSLibExt/Computability/Complexity/Classes.lean:323
def SigmaK (k : ℕ) : DecisionComplexityClass :=
{L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List (List Bool) → Bool, IsPolyTime R ∧
∀ x, L x ↔ AltQuant (fun n => p.eval n) k true R x}
CSLibExt/Computability/Complexity/Classes.lean:313
Sources
- R. M. Karp and R. J. Lipton, "Some connections between nonuniform and uniform complexity classes", Proceedings of the Twelfth Annual ACM Symposium on Theory of Computing (STOC 1980), 302-309.
Uses 6
TheoremLadner's theorem: NP-intermediate languages exist#●ready to prove
If P \(\ne\) NP, then there is a decision problem \(L\) in NP that is not in P and to which not every decision problem in NP reduces by a polynomial-time many-one reduction; that is, \(L\) is in NP but is neither in P nor NP-complete.
public theorem_wanted ladner :
MetaMathlibExt.ComplexityTheory.P ≠ MetaMathlibExt.ComplexityTheory.NP →
∃ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
L ∈ MetaMathlibExt.ComplexityTheory.NP ∧ L ∉ MetaMathlibExt.ComplexityTheory.P ∧
¬ (∀ L' : MetaMathlibExt.ComplexityTheory.DecisionProblem,
L' ∈ MetaMathlibExt.ComplexityTheory.NP →
Cslib.CookLevin.PolyManyOneRed L' L)
def P : DecisionComplexityClass :=
{ L | IsPolyTime L }
MathlibExt/Computability/Complexity.lean:194
def NP : DecisionComplexityClass :=
{ L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
IsPolyTime R ∧
∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }
MathlibExt/Computability/Complexity.lean:200
abbrev DecisionProblem := List Bool → Bool
MathlibExt/Computability/Complexity.lean:170
def PolyManyOneRed (L₁ L₂ : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
∃ reduce : List Bool → List Bool,
MetaMathlibExt.ComplexityTheory.IsPolyTime reduce ∧ ∀ x, L₁ x = L₂ (reduce x)
CSLibExt/Computability/CookLevin.lean:396
Sources
- R. E. Ladner, "On the structure of polynomial time reducibility", Journal of the ACM 22 (1975), 155-171.
Uses 5
TheoremSavitch's theorem: NPSPACE = PSPACE#●ready to prove
The complexity class NPSPACE of decision problems decided in polynomial space by nondeterministic multi-tape Turing machines equals the class PSPACE of decision problems decided in polynomial space by deterministic multi-tape Turing machines.
public theorem_wanted savitch :
NPSPACE = PSPACE
def NPSPACE : DecisionComplexityClass :=
{L | ∃ d, langOf L ∈ NSPACE (fun n => n ^ d)}
CSLibExt/Computability/Complexity/Classes.lean:188
def PSPACE : DecisionComplexityClass :=
{L | langOf L ∈ Cslib.Turing.MultiTapeTM.Classes.PSPACE}
CSLibExt/Computability/Complexity/Classes.lean:117
Sources
- W. J. Savitch, "Relationships between nondeterministic and deterministic tape complexities", Journal of Computer and System Sciences 4 (1970), 177-192.
Uses 3
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.