Simultaneous time-space complexity classes

This file defines the simultaneous time-space class DTISP(T, S) and SC (Steve's Class).

The key distinction from intersecting separate time and space classes is that DTISP requires a single machine satisfying both bounds simultaneously.

def Complexity.DTISP (T S : ℕ → ℕ) : Set Language

DTISP(T, S) is the class of languages decidable by a single deterministic TM running in time O(T(n)) and space O(S(n)) simultaneously (AB Definition 4.11). Space includes work tapes, excess read-only input-head travel, and two-way output-head travel beyond the free verdict cell.

Equations

• Complexity.DTISP T S = {L : Complexity.Language | ∃ (k : ℕ) (tm : Complexity.TM k) (t : ℕ → ℕ) (s : ℕ → ℕ), tm.DecidesInTimeSpace L t s ∧ Complexity.BigO t T ∧ Complexity.BigO s S}

def Complexity.SC : Set Language

SC (Steve's Class, named after Stephen Cook) is the class of languages decidable in polynomial time and polylogarithmic space simultaneously: SC = ⋃_{k,j} DTISP(n^k, (log n)^j).

Equations

• Complexity.SC = ⋃ (k : ℕ), ⋃ (j : ℕ), Complexity.DTISP (fun (x : ℕ) => x ^ k) fun (n : ℕ) => Nat.log 2 n ^ j