Lax Lean Archive

The complexity classes coNL and coNP

Lax434930.ComplementClasses · concepts/Lax434930/ComplementClasses.lean · lax-434930

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    For a class C\mathcal C of binary languages, coC\mathrm{co}\mathcal C consists of languages whose complements belong to C\mathcal C. Complements are taken among all finite binary strings. In particular, A∈coNLA\in\mathrm{coNL} means A‾∈NL\overline A\in\mathrm{NL}, and A∈coNPA\in\mathrm{coNP} means A‾∈NP\overline A\in\mathrm{NP}. This operation complements each language; it does not take the set-theoretic complement of the class of languages.

    Concept map
    7 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax434930.NondeterministicLogarithmicSpace
    2import Lax434930.NondeterministicPolynomialTime
    3
    4/-!
    5---
    6title: The complexity classes coNL and coNP
    7type: definition
    8---
    9For a class C\mathcal C of binary languages, coC\mathrm{co}\mathcal C
    10consists of languages whose complements belong to C\mathcal C.
    11Complements are taken among all finite binary strings. In particular,
    12A∈coNLA\in\mathrm{coNL} means A‾∈NL\overline A\in\mathrm{NL}, and
    13A∈coNPA\in\mathrm{coNP} means A‾∈NP\overline A\in\mathrm{NP}.
    14This operation complements each language; it does not take the set-theoretic
    15complement of the class of languages.
    16-/
    17
    18namespace Lax434930.ComplementClasses
    19
    20open PolynomialTime NondeterministicLogarithmicSpace NondeterministicPolynomialTime
    21
    22/-- The class of languages whose complements belong to the given class. -/
    23def co (C : Set Language) : Set Language := {A | Aᶜ ∈ C}
    24
    25/-- Complements of languages in NL. -/
    26def coNL : Set Language := co NL
    27
    28/-- Complements of languages in NP. -/
    29def coNP : Set Language := co NP
    30
    31end Lax434930.ComplementClasses
    32
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…