Lax Lean Archive

The classes NL and coNL

Lax485149.ClassNL · concepts/Lax485149/ClassNL.lean · lax-485149

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

    NL is the class of decision problems definable in the Krom fragment of existential second-order logic, which captures nondeterministic logarithmic space on ordered structures by a theorem of Grädel. Hardness is the cofinal hardness of the NP core: a problem is NL-hard when every problem it reduces to, by a relativized ordered first-order reduction, is reduced to by every problem of NL. coNL is the class of problems whose complement is in NL. NL-completeness is membership together with NL-hardness. No machine enters the definition.

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

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Classes
    3import Lax485149.Complement
    4import Lax485149.KromFragment
    5
    6/-!
    7---
    8title: The classes NL and coNL
    9type: definition
    10---
    11NL is the class of decision problems definable in the Krom fragment of
    12existential second-order logic, which captures nondeterministic logarithmic
    13space on ordered structures by a theorem of Grädel. Hardness is the cofinal
    14hardness of the NP core: a problem is NL-hard when every problem it reduces
    15to, by a relativized ordered first-order reduction, is reduced to by every
    16problem of NL. coNL is the class of problems whose complement is in NL.
    17NL-completeness is membership together with NL-hardness. No machine enters
    18the definition.
    19-/
    20
    21namespace Lax485149.ClassNL
    22
    23open Lax904597.Problems Lax904597.Classes Lax485149.Complement Lax485149.KromFragment
    24
    25/-- **NL**: the class of the SO-Krom definable problems, with cofinal
    26hardness. -/
    27def NL : ComplexityClass :=
    28 ComplexityClass.ofMem fun P => SigmaSOKromDefinable P
    29
    30/-- **coNL**: the problems whose complement is in NL. -/
    31def coNL : ComplexityClass :=
    32 ComplexityClass.ofMem fun P => SigmaSOKromDefinable (DecisionProblem.compl P)
    33
    34end Lax485149.ClassNL
    35
    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…