The reachable views within exponential time

Breadth-first search through the views of a nondeterministic machine, run until a round finds no new view (Cslib.Reachability.closingRound), lists exactly the views reachable from the initial view (Turing.MultiTapeNTM.mem_reachableViews_iff). Under a space bound s there are at most 2 ^ O(log₂ n + s) of them, each of length O(n + s), so the search finishes within 2 ^ O(log₂ n + s) rounds of polynomial cost in the views found. Any polynomial-time function of the list of views is therefore computable within time and space 2 ^ O(log₂ n + s) (Turing.MultiTapeNTM.exists_computableInTimeAndSpace_reachableViews).

The space bound need not be computable. The search stops by itself when the views are closed under successors, so no bound on the number of rounds is computed in advance, and the space bound enters only the analysis. This is the configuration-graph search behind NSPACE(s) ⊆ DTIME(2 ^ O(s)) and, with the marking of Turing.MultiTapeATM.markAccepts, behind ASPACE(s) ⊆ DTIME(2 ^ O(s)) Sipser, Sections 8.4 and 10.3 Chandra, Kozen and Stockmeyer, Section 3.

Main definitions

• Turing.MultiTapeNTM.reachableViews: breadth-first search through the views until closed.

Main results

• Turing.MultiTapeNTM.mem_reachableViews_iff: under a space bound, the listed views are exactly the reachable ones.
• Turing.MultiTapeNTM.head?_reachableViews: the initial view comes first.
• Turing.MultiTapeNTM.exists_computableInTimeAndSpace_reachableViews: a polynomial-time function of the reachable views is computable within time and space 2 ^ O(log₂ n + s).

References

• M. Sipser, Introduction to the Theory of Computation, Sections 8.4 and 10.3
• A. K. Chandra, D. C. Kozen, L. J. Stockmeyer, Alternation, Section 3

noncomputable def Turing.MultiTapeNTM.reachableViews {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) : List (FiniteCfg k Bool State)

The reachable views: breadth-first search through the views from the initial view on input, until a round finds no new view.

theorem Turing.MultiTapeNTM.mem_reachableViews_iff {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s : ℕ} (hs : ntm.RunsInSpace input s) {finite : FiniteCfg k Bool State} : finite ∈ ntm.reachableViews input ↔ Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite

The reachable views are found: under a space bound, the views listed by breadth-first search until closed are exactly those reachable from the initial view.

theorem Turing.MultiTapeNTM.head?_reachableViews {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} (input : List Bool) : (ntm.reachableViews input).head? = some (ntm.initView input)

The initial view comes first among the reachable views.

Exponential time

theorem Turing.MultiTapeNTM.exists_computableInTimeAndSpace_reachableViews {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {α γ : Type} {enc : α ↪ List Bool} {encOut : γ ↪ List Bool} {s : α → ℕ} (hs : ∀ (a : α), ntm.RunsInSpace (enc a) (s a)) {g : List (FiniteCfg k Bool State) → γ} (hg : MultiTapeTM.ComputableInPolyTime g (MultiTapeTM.encList MultiTapeTM.encFiniteCfg) encOut) : ∃ (c : ℕ), MultiTapeTM.ComputableInTimeAndSpace (fun (a : α) => g (ntm.reachableViews (enc a))) enc encOut (fun (a : α) => 2 ^ (c * ((enc a).length.log2 + s a + 1))) fun (a : α) => 2 ^ (c * ((enc a).length.log2 + s a + 1))

A polynomial-time function of the reachable views is computable within exponential time: if every computation prefix of ntm on every encoded instance stays within space s a, then for every polynomial-time g, the value of g on the reachable views is computable within time and space 2 ^ (c * (log₂ n + s a + 1)). The space bound need not be computable.