Parallel complexity class NC
TheoremNC^1 is contained in L#●ready to prove
MetaMathlibExt.Complexity.KeyTheorems.NC1SubsetL.nc1_subset_logspace
Every decision problem in \(\mathsf{NC}^1\) belongs to the class \(\mathsf{L}\) of decision problems decidable in deterministic logarithmic space.
public theorem_wanted nc1_subset_logspace :
NCK 1 ⊆ LogSpacedef NCK (k : ℕ) : DecisionComplexityClass :=
{L | ∃ c, ∃ p : Polynomial ℕ, ∃ C : (n : ℕ) → List (ACGate n),
UniformCircuitFamily C ∧
∀ n, WellFormedCircuit (C n) ∧ IsModFree (C n) ∧ IsFanInLeTwo (C n) ∧
(C n).length ≤ p.eval n ∧
circuitDepth (C n) ≤ c * (Nat.log 2 (n + 1) + 1) ^ k ∧
∀ x : List Bool, x.length = n →
(L x = true ↔
(circuitEval (C n) (fun i => x.getD (i : ℕ) false)).getLast? = some true)}CSLibExt/Computability/Complexity/Classes.lean:712
def LogSpace : DecisionComplexityClass :=
{L | ∃ c, langOf L ∈
Cslib.Turing.MultiTapeTM.DSPACE (fun n => c * Nat.log 2 (n + 1) + c)}CSLibExt/Computability/Complexity/Classes.lean:133
Sources
Sources
- S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 6.22 (NC¹ ⊆ L); M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Theorem 9.21 (NC¹ ⊆ L).
Uses 4
Statement usesDeterministic logarithmic space · The class NC^k · Complexity classes · Decision problems
TheoremNC is contained in P#●ready to prove
MetaMathlibExt.Complexity.KeyTheorems.NCSubsetP.nc_subset_p
Every decision problem in \(\mathsf{NC}\) belongs to \(\mathsf{P}\).
public theorem_wanted nc_subset_p :
NC ⊆ Pdef NC : DecisionComplexityClass := ⋃ k, NCK kCSLibExt/Computability/Complexity/Classes.lean:726
def P : DecisionComplexityClass :=
{ L | IsPolyTime L }MathlibExt/Computability/Complexity.lean:194
Sources
Sources
- S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 6.22 (NC ⊆ P); M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Theorem 9.21.
Uses 4
Statement usesThe class NC · Complexity classes · Decision problems · The complexity class P
2 ready to prove
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.