Truncated breadth-first search through the views

Breadth-first search through the views of a nondeterministic machine (Cslib.Reachability.search, along Turing.MultiTapeNTM.viewSucc) finds every reachable view once it has run for as many rounds as there are reachable views (Turing.MultiTapeNTM.mem_search_iff). Under a space bound s there are at most 2 ^ (2 * coreLengthBound k State n s + 1) of them. For a polynomial s that is exponential, and a polynomial-time analysis must then be relative to the number of rounds. The truncated search Turing.MultiTapeNTM.boundedSearch keeps at most cap views after each round, so its lists have at most cap + 1 views of size polynomial in the instance and the space bound (Turing.MultiTapeNTM.length_boundedSearch_le). With the cap and the number of rounds given in unary, it is polynomial-time (Turing.MultiTapeNTM.computableInPolyTime_boundedSearch). Truncation never discards a view once cap bounds the number of reachable views (Turing.MultiTapeNTM.boundedSearch_eq_search), so it then finds exactly the reachable views (Turing.MultiTapeNTM.mem_boundedSearch_iff). This is the configuration-graph construction of Sipser, Section 8.4, with the graph size passed as a unary parameter.

Main definitions

• Turing.MultiTapeNTM.boundedSearch: breadth-first search through the views, truncated to a cap.

Main results

• Turing.MultiTapeNTM.length_boundedSearch_le: the truncated search keeps at most cap + 1 views.
• Turing.MultiTapeNTM.reflTransGen_of_mem_boundedSearch: it finds only reachable views.
• Turing.MultiTapeNTM.boundedSearch_eq_search, Turing.MultiTapeNTM.mem_boundedSearch_iff: once the cap bounds the number of reachable views, truncation changes nothing and enough rounds find exactly the reachable views.
• Turing.MultiTapeNTM.computableInPolyTime_boundedSearch: under a polynomial space bound, the truncated search is polynomial-time in the instance and the unary cap.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.4

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

Breadth-first search through the views for rounds rounds, keeping at most cap views after each round. Truncation changes nothing once cap bounds the number of reachable views, and keeps the search polynomial in cap otherwise.

theorem Turing.MultiTapeNTM.length_boundedSearch_le {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} (input : List Bool) (cap rounds : ℕ) : (ntm.boundedSearch input cap rounds).length ≤ cap + 1

The truncated search keeps at most cap + 1 views.

theorem Turing.MultiTapeNTM.reflTransGen_of_mem_boundedSearch {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {cap rounds : ℕ} {finite : FiniteCfg k Bool State} (h : finite ∈ ntm.boundedSearch input cap rounds) : Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite

The truncated search finds only reachable views.

theorem Turing.MultiTapeNTM.boundedSearch_eq_search {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s cap : ℕ} (hs : ntm.RunsInSpace input s) (hcap : 2 ^ (2 * coreLengthBound k State input.length s + 1) ≤ cap) (rounds : ℕ) : ntm.boundedSearch input cap rounds = Cslib.Reachability.search ntm.viewSucc rounds (ntm.initView input)

Truncation changes nothing once cap bounds the number of reachable views: under a space bound s, 2 ^ (2 * coreLengthBound k State n s + 1) of them.

theorem Turing.MultiTapeNTM.mem_boundedSearch_iff {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s N : ℕ} (hs : ntm.RunsInSpace input s) (hN : 2 ^ (2 * coreLengthBound k State input.length s + 1) ≤ N) {finite : FiniteCfg k Bool State} : finite ∈ ntm.boundedSearch input N N ↔ Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite

The truncated search finds the reachable views once N, as both the cap and the number of rounds, bounds their number.

theorem Turing.MultiTapeNTM.computableInPolyTime_boundedSearch {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {α : Type} {enc : α ↪ List Bool} {s : α → ℕ} (hs : ∀ (a : α), ntm.RunsInSpace (enc a) (s a)) (hpoly : MultiTapeTM.PolyBounded (fun (a : α) => (enc a).length) s) : MultiTapeTM.ComputableInPolyTime (fun (x : α × ℕ) => ntm.boundedSearch (enc x.1) x.2 x.2) (MultiTapeTM.encPair enc MultiTapeTM.encUnary) (MultiTapeTM.encList MultiTapeTM.encFiniteCfg)

The truncated search is polynomial-time in the instance and the unary number N, used as both the cap and the number of rounds, when the space bound is polynomial in the instance: each list holds at most N + 1 views of size polynomial in the instance.