P, FP, and PSPACE

This file defines P (polynomial time), FP (polynomial-time functions), and PSPACE (polynomial space) in terms of the base classes DTIME and DSPACE.

def Complexity.P : Set Language

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

Equations

• Complexity.P = ⋃ (k : ℕ), Complexity.DTIME fun (x : ℕ) => x ^ k

def Complexity.FP : Set (List Bool → List Bool)

FP is the class of functions computable by a deterministic TM in polynomial time.

Equations

• Complexity.FP = {f : List Bool → List Bool | ∃ (d : ℕ) (k : ℕ) (tm : Complexity.TM k) (T : ℕ → ℕ), tm.ComputesInTime f T ∧ Complexity.BigO T fun (x : ℕ) => x ^ d}

def Complexity.PSPACE : Set Language

PSPACE is the class of languages decidable by a deterministic TM using polynomial auxiliary space: PSPACE = ⋃_k DSPACE(n^k).

Equations

• Complexity.PSPACE = ⋃ (k : ℕ), Complexity.DSPACE fun (x : ℕ) => x ^ k