Breadth-first search through the views of a nondeterministic machine

A nondeterministic machine accepts exactly when an accepting view (Turing.MultiTapeNTM.acceptingView: halted, with output [true]) is reachable from its initial view (Turing.MultiTapeNTM.accepts_iff_reflTransGen_viewStep). Breadth-first search through the views (Cslib.Reachability.search, along Turing.MultiTapeNTM.viewSucc) finds exactly the reachable views once it has run for as many rounds as there are (Turing.MultiTapeNTM.mem_search_iff). Under a logarithmic space bound there are polynomially many (Turing.MultiTapeNTM.length_le_of_nodup_reachable), so a polynomial number of rounds suffices, each round is polynomial-time in the views found so far, and these are polynomially many views of linear size. The search is therefore polynomial-time (Turing.MultiTapeNTM.exists_computableInPolyTime_search): reachability in the configuration graph, which has polynomially many vertices Sipser, Section 8.4. The search run until no new view appears, under any space bound, is Turing.MultiTapeNTM.reachableViews.

Main definitions

• Turing.MultiTapeNTM.viewSucc: the views a running view steps to.
• Turing.MultiTapeNTM.acceptingView: the test for a halted view with output [true].

Main results

• Turing.MultiTapeNTM.reflTransGen_viewSucc_iff: the successor lists give the reachable views.
• Turing.MultiTapeNTM.mem_search_iff: enough rounds find exactly the reachable views.
• Turing.MultiTapeNTM.computableInPolyTime_viewSucc, Turing.MultiTapeNTM.computableInPolyTime_acceptingView, Turing.MultiTapeNTM.computableInPolyTime_initView: the successors, the accepting test and the initial view in polynomial time.
• Turing.MultiTapeTM.ComputableInPolyTime.expand: a round in polynomial time.
• Turing.MultiTapeNTM.length_encList_search_le: under any space bound, the views found by any number of rounds are few and short.
• Turing.MultiTapeNTM.exists_computableInPolyTime_search: under a logarithmic space bound, enough rounds of breadth-first search find their views in polynomial time.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.4
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 4.1

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

The views a view steps to, other than itself: none for a halted view, and for a running view the summarized results of the actions its transition relation permits.

def Turing.MultiTapeNTM.acceptingView {k : ℕ} {State : Type} (finite : FiniteCfg k Bool State) : Bool

An accepting view: halted, with output [true].

theorem Turing.MultiTapeNTM.viewStep_of_mem_viewSucc {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {finite next : FiniteCfg k Bool State} (h : next ∈ ntm.viewSucc finite) : ntm.ViewStep finite next

A view steps to each of its successors.

theorem Turing.MultiTapeNTM.reflTransGen_viewSucc_iff {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {finite next : FiniteCfg k Bool State} : Relation.ReflTransGen (fun (a b : FiniteCfg k Bool State) => b ∈ ntm.viewSucc a) finite next ↔ Relation.ReflTransGen ntm.ViewStep finite next

The successor lists give the reachable views: a halted view steps only to itself, which adds nothing to reachability.

theorem Turing.MultiTapeNTM.mem_search_iff {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s rounds : ℕ} (hs : ntm.RunsInSpace input s) (hrounds : 2 ^ (2 * coreLengthBound k State input.length s + 1) ≤ rounds) {finite : FiniteCfg k Bool State} : finite ∈ Cslib.Reachability.search ntm.viewSucc rounds (ntm.initView input) ↔ Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite

Enough rounds find every reachable view: under a space bound s, breadth-first search for at least 2 ^ (2 * coreLengthBound k State n s + 1) rounds finds exactly the views reachable from the initial view.

Breadth-first search in polynomial time

theorem Turing.MultiTapeTM.ComputableInPolyTime.insertNew {α : Type} [DecidableEq α] {enc : α ↪ List Bool} : ComputableInPolyTime (fun (p : List α × α) => Cslib.Reachability.insertNew p.1 p.2) (encPair (encList enc) enc) (encList enc)

Appending an element unless it is already in the list is polynomial-time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.expand {α : Type} [DecidableEq α] {enc : α ↪ List Bool} {succ : α → List α} (hsucc : ComputableInPolyTime succ enc (encList enc)) : ComputableInPolyTime (Cslib.Reachability.expand succ) (encList enc) (encList enc)

A round of breadth-first search is polynomial-time when the successors are: the found elements and their successors are at most polynomially many and long.

theorem Turing.MultiTapeNTM.computableInPolyTime_viewSucc {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} : MultiTapeTM.ComputableInPolyTime ntm.viewSucc MultiTapeTM.encFiniteCfg (MultiTapeTM.encList MultiTapeTM.encFiniteCfg)

The successors of a view are polynomial-time.

theorem Turing.MultiTapeNTM.computableInPolyTime_acceptingView {k : ℕ} {State : Type} [Finite State] : MultiTapeTM.ComputableInPolyTime acceptingView MultiTapeTM.encFiniteCfg MultiTapeTM.encBool

The accepting test is polynomial-time.

theorem Turing.MultiTapeNTM.computableInPolyTime_initView {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {α : Type} (enc : α ↪ List Bool) : MultiTapeTM.ComputableInPolyTime (fun (a : α) => ntm.initView (enc a)) enc MultiTapeTM.encFiniteCfg

The initial view of an encoded instance is polynomial-time.

theorem Turing.MultiTapeNTM.length_encList_search_le {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s : ℕ} (hs : ntm.RunsInSpace input s) (rounds : ℕ) : ((MultiTapeTM.encList MultiTapeTM.encFiniteCfg) (Cslib.Reachability.search ntm.viewSucc rounds (ntm.initView input))).length ≤ 2 ^ (2 * coreLengthBound k State input.length s + 1) * (2 * viewLengthBound k State input.length s + 1)

Breadth-first search finds few short views: under a space bound s, any number of rounds of the search from the initial view finds at most 2 ^ (2 * coreLengthBound + 1) views, each encoded within 2 * viewLengthBound + 1 bits.

theorem Turing.MultiTapeNTM.exists_computableInPolyTime_search {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {α : Type} {enc : α ↪ List Bool} {c : ℕ} (hs : ∀ (a : α), ntm.RunsInSpace (enc a) (c * ((enc a).length.log2 + 1))) : ∃ (rounds : α → ℕ), (∀ (a : α), 2 ^ (2 * coreLengthBound k State (enc a).length (c * ((enc a).length.log2 + 1)) + 1) ≤ rounds a) ∧ MultiTapeTM.ComputableInPolyTime (fun (a : α) => Cslib.Reachability.search ntm.viewSucc (rounds a) (ntm.initView (enc a))) enc (MultiTapeTM.encList MultiTapeTM.encFiniteCfg)

Breadth-first search within logarithmic space is polynomial-time. If every computation prefix of ntm on every encoded instance enc a stays within space c * (Nat.log2 n + 1), then for some polynomial number of rounds, at least the bound of Turing.MultiTapeNTM.mem_search_iff, the list of views found by breadth-first search from the initial view is polynomial-time in the encoded instance.