Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The classes PTIME and coPTIME

Lax535992.ClassPTIME · concepts/Lax535992/ClassPTIME.lean · lax-535992

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

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

    Concept map
    9 concepts; 16 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 Lax535992.HornFragment
    5
    6/-!
    7---
    8title: The classes PTIME and coPTIME
    9type: definition
    10---
    11PTIME is the class of decision problems definable in the Horn fragment of
    12existential second-order logic, which captures polynomial time on ordered
    13structures by a theorem of Grädel. Hardness is the cofinal hardness of the
    14NP core: a problem is PTIME-hard when every problem it reduces to, by a
    15relativized ordered first-order reduction, is reduced to by every problem of
    16PTIME. coPTIME is the class of problems whose complement is in PTIME.
    17PTIME-completeness is membership together with PTIME-hardness, under
    18first-order reductions. No machine enters the definition.
    19-/
    20
    21namespace Lax535992.ClassPTIME
    22
    23open Lax904597.Problems Lax904597.Classes Lax485149.Complement Lax535992.HornFragment
    24
    25/-- **PTIME**: the class of the SO-Horn definable problems, with cofinal
    26hardness. -/
    27def PTIME : ComplexityClass :=
    28 ComplexityClass.ofMem fun P => SigmaSOHornDefinable P
    29
    30/-- **coPTIME**: the problems whose complement is in PTIME. -/
    31def coPTIME : ComplexityClass :=
    32 ComplexityClass.ofMem fun P => SigmaSOHornDefinable (DecisionProblem.compl P)
    33
    34end Lax535992.ClassPTIME
    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…