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.

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}
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
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)
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
Sources
  • W. J. Savitch, "Relationships between nondeterministic and deterministic tape complexities", Journal of Computer and System Sciences 4 (1970), 177-192.
Uses 3
4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.