NP, coNP, and NPSPACE

This file defines NP (nondeterministic polynomial time), coNP, and NPSPACE (nondeterministic polynomial space) in terms of the base classes NTIME and NSPACE.

def Complexity.NP : Set Language

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

Equations

• Complexity.NP = ⋃ (k : ℕ), Complexity.NTIME fun (x : ℕ) => x ^ k

def Complexity.coNP : Set Language

coNP is the class of languages whose complements are in NP.

Equations

• Complexity.coNP = Complexity.complClass Complexity.NP

def Complexity.NPSPACE : Set Language

NPSPACE is the class of languages decidable by a nondeterministic TM using polynomial auxiliary space: NPSPACE = ⋃_k NSPACE(n^k).

Equations

• Complexity.NPSPACE = ⋃ (k : ℕ), Complexity.NSPACE fun (x : ℕ) => x ^ k