Lax434930.SpaceBounds
Deterministic and nondeterministic space bounds
concepts/Lax434930/SpaceBounds.lean · lax-434930
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
For a function , the classes DSPACE and NSPACE below use the exact bound 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 respects the bound. DSPACE additionally requires deterministic transitions. Constant factors are quantified explicitly when the classical space classes are defined. We use as a positive logarithmic bound, so empty inputs are included without a special case.
Lean source view on GitHub
| 1 | import Lax434930.SpaceMachines |
| 2 | import Mathlib.Data.Nat.Log |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Deterministic and nondeterministic space bounds |
| 7 | type: definition |
| 8 | --- |
| 9 | For a function , the classes DSPACE and NSPACE |
| 10 | below use the exact bound on the number of work cells visited. |
| 11 | There is one machine for all inputs, it halts on every branch, and every |
| 12 | reachable configuration on an input of length respects the bound. |
| 13 | DSPACE additionally requires deterministic transitions. Constant factors |
| 14 | are quantified explicitly when the classical space classes are defined. |
| 15 | We use as a positive logarithmic bound, so |
| 16 | empty inputs are included without a special case. |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax434930.SpaceBounds |
| 20 | |
| 21 | open PolynomialTime SpaceMachines |
| 22 | |
| 23 | /-- Deterministic deciders using at most `s n` work cells on inputs of length `n`. -/ |
| 24 | def 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. -/ |
| 29 | def 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. -/ |
| 33 | def logSpace (n : ℕ) : ℕ := Nat.log 2 (n + 2) |
| 34 | |
| 35 | end 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