Base time complexity classes

This file defines the parametric time complexity classes DTIME(T) and NTIME(T), the building blocks from which polynomial, exponential, and randomized time classes are derived.

Both use =O (Mathlib's IsBigO lifted to ℕ → ℕ) to express asymptotic bounds.

def Complexity.DTIME (T : ℕ → ℕ) : Set Language

DTIME(T) is the class of languages decidable by a deterministic TM in time O(T(n)) (AB Definition 1.6). The machine may have any number of work tapes.

Equations

• Complexity.DTIME T = {L : Complexity.Language | ∃ (k : ℕ) (tm : Complexity.TM k) (f : ℕ → ℕ), tm.DecidesInTime L f ∧ Complexity.BigO f T}

def Complexity.NTIME (T : ℕ → ℕ) : Set Language

NTIME(T) is the class of languages decidable by a nondeterministic TM in time O(T(n)) (AB Definition 2.1). The machine may have any number of work tapes.

Equations

• Complexity.NTIME T = {L : Complexity.Language | ∃ (k : ℕ) (tm : Complexity.NTM k) (f : ℕ → ℕ), tm.DecidesInTime L f ∧ Complexity.BigO f T}

def Complexity.complClass (C : Set Language) : Set Language

Complement class constructor: complClass C = {L | Lᶜ ∈ C}. Used to uniformly define coNP, coRP, coNL, etc.

Equations

• Complexity.complClass C = {L : Complexity.Language | Lᶜ ∈ C}

@[simp]

theorem Complexity.mem_complClass {L : Language} {C : Set Language} : L ∈ complClass C ↔ Lᶜ ∈ C

Membership in complClass C is exactly membership of the complement in C.

theorem Complexity.complClass_complClass (C : Set Language) : complClass (complClass C) = C

The complement class is involutive: complClass (complClass C) = C.