Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax434930.SpaceBounds

Deterministic and nondeterministic space bounds

concepts/Lax434930/SpaceBounds.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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    For a function s:NNs:\mathbb{N}\to\mathbb{N}, the classes DSPACE and NSPACE below use the exact bound s(n)s(n) on the number of work cells visited. There is one machine for all inputs, it halts on every branch, and every reachable configuration on an input of length nn respects the bound. DSPACE additionally requires deterministic transitions. Constant factors are quantified explicitly when the classical space classes are defined. We use log2(n+2)\lfloor\log_2(n+2)\rfloor as a positive logarithmic bound, so empty inputs are included without a special case.

    Lean source view on GitHub

    1import Lax434930.SpaceMachines
    2import Mathlib.Data.Nat.Log
    3
    4/-!
    5---
    6title: Deterministic and nondeterministic space bounds
    7type: definition
    8---
    9For a function s:NNs:\mathbb{N}\to\mathbb{N}, the classes DSPACE and NSPACE
    10below use the exact bound s(n)s(n) on the number of work cells visited.
    11There is one machine for all inputs, it halts on every branch, and every
    12reachable configuration on an input of length nn respects the bound.
    13DSPACE additionally requires deterministic transitions. Constant factors
    14are quantified explicitly when the classical space classes are defined.
    15We use log2(n+2)\lfloor\log_2(n+2)\rfloor as a positive logarithmic bound, so
    16empty inputs are included without a special case.
    17-/
    18
    19namespace Lax434930.SpaceBounds
    20
    21open PolynomialTime SpaceMachines
    22
    23/-- Deterministic deciders using at most `s n` work cells on inputs of length `n`. -/
    24def DSPACE (s : ℕ → ℕ) : Set Language :=
    25 {A | ∃ M : Machine, M.Deterministic ∧ M.Decides A ∧
    26 ∀ w : Word, M.UsesSpace w (s w.length)}
    27
    28/-- Nondeterministic deciders using at most `s n` work cells on every branch. -/
    29def NSPACE (s : ℕ → ℕ) : Set Language :=
    30 {A | ∃ M : Machine, M.Decides A ∧ ∀ w : Word, M.UsesSpace w (s w.length)}
    31
    32/-- An integer logarithm that is positive even at input length zero. -/
    33def logSpace (n : ℕ) : ℕ := Nat.log 2 (n + 2)
    34
    35end Lax434930.SpaceBounds
    36

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…