Lax Lean Archive

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

The exponential classes

Lax480241.ExponentialClasses · concepts/Lax480241/ExponentialClasses.lean · lax-480241

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

    A problem PP is definable in a class CC one exponential up when an exponential expansion XX and a problem QQ of CC over its vocabulary are such that P(A)P(A) holds exactly when Q(X(A))Q(X(A)) does, for every nonempty finite structure AA and every linear order on it; these problems form the class Cexp⁡C^{\exp}, with cofinal hardness. EXPTIME and EXPSPACE are the classes of the problems definable in SO(≤, LFP) and in SO(≤, PFP), NEXPTIME is NPexp⁡^{\exp}, and coEXPTIME and coEXPSPACE are the classes of the complements of their problems.

    Concept map
    15 concepts; 6 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.Problems
    4import Lax485149.Complement
    5import Lax480241.Expansions
    6import Lax480241.SecondOrderFixedPoints
    7
    8/-!
    9---
    10title: The exponential classes
    11type: definition
    12---
    13A problem PP is definable in a class CC one exponential up when an
    14exponential expansion XX and a problem QQ of CC over its vocabulary are
    15such that P(A)P(A) holds exactly when Q(X(A))Q(X(A)) does, for every nonempty
    16finite structure AA and every linear order on it; these problems form the
    17class Cexp⁡C^{\exp}, with cofinal hardness. EXPTIME and EXPSPACE are the
    18classes of the problems definable in SO(≤, LFP) and in SO(≤, PFP), NEXPTIME
    19is NPexp⁡^{\exp}, and coEXPTIME and coEXPSPACE are the classes of the
    20complements of their problems.
    21-/
    22
    23namespace Lax480241.ExponentialClasses
    24
    25open FirstOrder FirstOrder.Language
    26open Lax904597.Problems Lax904597.Classes Lax485149.Complement
    27open Lax480241.Expansions Lax480241.SecondOrderFixedPoints
    28
    29/-- **Definability one exponential up**: some expansion turns the problem into a
    30problem of the class. -/
    31def ExpDefinable (C : ComplexityClass) {L : Language.{0, 0}} [L.IsRelational]
    32 (P : DecisionProblem L) : Prop :=
    33 ∃ (X : ExpExpansion L) (Q : DecisionProblem X.E), C.Mem Q ∧
    34 ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A], P A ↔ Q (X.Map A)
    35
    36/-- **The exponential of a class**: the problems definable in it one exponential
    37up, with cofinal hardness. -/
    38def expClass (C : ComplexityClass) : ComplexityClass :=
    39 ComplexityClass.ofMem fun P => ExpDefinable C P
    40
    41/-- **EXPTIME**: the problems definable in SO(≤, LFP). -/
    42def EXPTIME : ComplexityClass :=
    43 ComplexityClass.ofMem fun P => SOLFPDefinable P
    44
    45/-- **EXPSPACE**: the problems definable in SO(≤, PFP). -/
    46def EXPSPACE : ComplexityClass :=
    47 ComplexityClass.ofMem fun P => SOPFPDefinable P
    48
    49/-- **NEXPTIME**: NP read one exponential up. -/
    50def NEXPTIME : ComplexityClass :=
    51 expClass NP
    52
    53/-- **coEXPTIME**: the complements of the problems of EXPTIME. -/
    54def coEXPTIME : ComplexityClass :=
    55 ComplexityClass.ofMem fun P => EXPTIME.Mem (DecisionProblem.compl P)
    56
    57/-- **coEXPSPACE**: the complements of the problems of EXPSPACE. -/
    58def coEXPSPACE : ComplexityClass :=
    59 ComplexityClass.ofMem fun P => EXPSPACE.Mem (DecisionProblem.compl P)
    60
    61end Lax480241.ExponentialClasses
    62
    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…