The complexity class EXPTIME

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

definition

Loading review…

Sign in with ORCID

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 binary language belongs to EXPTIME\mathrm{EXPTIME} if a deterministic Turing machine decides membership within 2p(n)2^{p(n)} transitions on every input of length nn, for some polynomial p∈N[X]p\in\mathbb{N}[X]. The machine is the finite elementary single-tape machine defined here: input bits are distinct from blank, input appears in its original order, and each transition performs one move or one write. A terminal state's Boolean label gives the answer. The polynomial in the exponent may have any fixed degree; this is the usual EXPTIME, also called EXP.

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

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Lax434930.PolynomialTime
    2import Lax434930.MachineModels
    3
    4/-!
    5---
    6title: The complexity class EXPTIME
    7type: definition
    8---
    9A binary language belongs to EXPTIME\mathrm{EXPTIME} if a deterministic Turing
    10machine decides membership within 2p(n)2^{p(n)} transitions on every input
    11of length nn, for some polynomial p∈N[X]p\in\mathbb{N}[X].
    12The machine is the finite elementary single-tape machine defined here:
    13input bits are distinct from blank, input appears in its original order,
    14and each transition performs one move or one write. A terminal state's
    15Boolean label gives the answer. The polynomial in the exponent may have
    16any fixed degree; this is the usual EXPTIME, also called EXP.
    17-/
    18
    19namespace Lax434930.ExponentialTime
    20
    21open PolynomialTime Lax434930.MachineModels Turing
    22
    23/-- Deterministic time bounded by two to a polynomial in the input length. -/
    24def EXPTIME : Set Language :=
    25 {A | ∃ (M : SingleTape) (p : Polynomial ℕ), ∀ w : Word,
    26 ∃ c : TM0.Cfg M.Γ M.Q,
    27 Nonempty (StateTransition.EvalsToInTime (TM0.step M.transition)
    28 (TM0.init (w.map M.input)) (some c) (2 ^ p.eval w.length)) ∧
    29 TM0.step M.transition c = none ∧ (M.accept c.q = true ↔ w ∈ A)}
    30
    31end Lax434930.ExponentialTime
    32

    Discussion

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

    Loading discussion…