feat(MultiTapeTM): Prove time upper-bounds for space-bounded classes - #767
feat(MultiTapeTM): Prove time upper-bounds for space-bounded classes#767crei wants to merge 2 commits into
Conversation
Proves bounds on the number of configurations reachable in bounded space and proves complexity-class inclusions from that: DSPACE(s) \subseteq DTIME(n * 2^(O(s))
| subst h_zero | ||
| simp | ||
|
|
||
| /-- The number of cells touched by a single work tape grows by at most one each step. -/ |
There was a problem hiding this comment.
These were moved to TapeLemmas.lean
| obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h | ||
| rw [Nat.add_comm, tm.configs_add, tm.iter_step_eq_of_halt hm] | ||
|
|
||
| /-- If a deterministic machine revisits a non-halting configuration, it never halts: revisiting a |
There was a problem hiding this comment.
This sounds like super generic result which should be part of LTS or even "iterated functions" in general. @fmontesi do we have this already somewhere?
|
|
||
| open Classes | ||
|
|
||
| /-- `2 ^ log₂ n ≤ n + 1` for all `n`, including `n = 0` (where both sides are `1`). -/ |
There was a problem hiding this comment.
Everything below here should just follow "directly" from the generic result above. I think we need more reusable results / tactics about growth functions in general. Also see my comment in #468
| definition similar to this one ([AroraBarak09], [Sipser2013]). The fuzzy definition is justified by | ||
| the space and time compression / speedup theorems (which are not proven here) and allow for | ||
| easier proofs and simpler theorem statements. Once we have better machinery, we can prove the | ||
| compression / speedup theorems and potentially move to exact bounds. |
There was a problem hiding this comment.
I prefer the fuzzy definitions as they are more likely to be TM-definition independent.
| /-- The complexity class of languages decidable in time linear in `t` by a deterministic multi-tape | ||
| Turing machine, disregarding the space requirement. -/ | ||
| def DTIME (t : ℕ → ℕ) := | ||
| {L : Language Symbol | ∃ c₁ c₂ : ℕ, ∃ s, DecidableInTimeAndSpace L (c₁ * t · + c₂) s} |
There was a problem hiding this comment.
It would be nice if these definitions used big-O notation instead. I understand you're adding the additive constant here, but is that really necessary or standard?
|
I'd like to see this split up, I think it would be easier to review and easier to come to agreement on it. Left a few comments on bits which are salient for me for now. |
|
I split some of the content into a separate PR and I'm changing this one back into draft. |
2 participants
Proves
DSPACE s ⊆ ⋃ c, DTIME (fun n => n * 2 ^ (c * s n)). From this, the inclusionsL ⊆ PandPSPACE ⊆ EXPare proven.This PR also defines several complexity classes based on the multi-tape Turing machine model.
The key lemma to get to the theorem is a bound of the number of reachable configurations in bounded space. The configurations are split into the actual "storage" part (state, work tape positions, work tape contents) and the input head position. This is not required to prove the result but it will help proving
DSPACE log log n = DSPACE 1in a subsequent PR.NB: AI was used to generate this content, but it was heavily edited and checked.