Hierarchy theorems and proof barriers
Time and space hierarchy theorems and diagonalization against time-bounded machines, separations such as P ≠ EXP, and barriers to separating classes: relativization (Baker–Gill–Solovay, oracle separations), natural proofs and algebrization.
- Algebrization barrier
- Natural proofs barrier
- Relativization and oracle separations
- Space hierarchy theorem
- Time hierarchy theorem
TheoremNondeterministic time hierarchy#●ready to prove
MetaMathlibExt.Complexity.KeyTheorems.NondetTimeHierarchy.nondet_time_hierarchy
Source: S. A. Cook, "A hierarchy for nondeterministic time complexity", Journal of Computer and System Sciences 7 (1973), 343-353; S. Zak, "A Turing machine time hierarchy", Theoretical Computer Science 26 (1983), 327-333.
public theorem_wanted nondet_time_hierarchy :
∃ L : Set (List Bool), L ∈ NTIME (fun n => n ^ 2) ∧ L ∉ NTIME (fun n => n)def NTIME (t : ℕ → ℕ) : Set (Set (List Bool)) :=
{L | ∃ c₁ c₂, ∃ k, ∃ (State : Type) (_ : Finite State),
∃ ntm : Turing.MultiTapeNTM k Bool State,
NTMDecidesInTime ntm (fun n => c₁ * t n + c₂) L}CSLibExt/Computability/Complexity/Classes.lean:172
Uses 1
Statement usesNondeterministic time classes
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.