Lax Lean Archive

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

The classes PSPACE and coPSPACE

Lax134656.ClassPSPACE · concepts/Lax134656/ClassPSPACE.lean · lax-134656

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

    PSPACE is the class of decision problems definable in second-order logic with a transitive closure, SO(TC), which captures polynomial space on ordered structures. Hardness is the cofinal hardness of the NP core, under relativized ordered first-order reductions, and coPSPACE is the class of problems whose complement is in PSPACE. PSPACE-completeness is membership together with PSPACE-hardness, under first-order reductions. No machine enters the definition.

    Concept map
    9 concepts; 15 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 Lax134656.SecondOrderTransitiveClosure
    5
    6/-!
    7---
    8title: The classes PSPACE and coPSPACE
    9type: definition
    10---
    11PSPACE is the class of decision problems definable in second-order logic
    12with a transitive closure, SO(TC), which captures polynomial space on
    13ordered structures. Hardness is the cofinal hardness of the NP core, under
    14relativized ordered first-order reductions, and coPSPACE is the class of
    15problems whose complement is in PSPACE. PSPACE-completeness is membership
    16together with PSPACE-hardness, under first-order reductions. No machine
    17enters the definition.
    18-/
    19
    20namespace Lax134656.ClassPSPACE
    21
    22open Lax904597.Problems Lax904597.Classes Lax485149.Complement
    23open Lax134656.SecondOrderTransitiveClosure
    24
    25/-- **PSPACE**: the class of the SO(TC) definable problems, with cofinal
    26hardness. -/
    27def PSPACE : ComplexityClass :=
    28 ComplexityClass.ofMem fun P => SOTCDefinable P
    29
    30/-- **coPSPACE**: the problems whose complement is in PSPACE. -/
    31def coPSPACE : ComplexityClass :=
    32 ComplexityClass.ofMem fun P => SOTCDefinable (DecisionProblem.compl P)
    33
    34end Lax134656.ClassPSPACE
    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…