Savitch's decider for space-bounded nondeterministic machines

A nondeterministic machine with finitely many states, all of whose computation paths on an input of length n visit at most c * (n + 1) ^ d work cells, is decided by the deterministic Turing.MultiTapeNTM.savitchDecide: Savitch's midpoint recursion with an explicit stack (Cslib.Reachability.savitch) on the codes of the finite views of the machine, asking whether the accepting code is reachable from the code of the initial view.

Every view reachable from the initial view has an encoding of length at most Turing.MultiTapeNTM.viewLengthBound, linear in n and the space bound, whatever the length of the path reaching it (Turing.MultiTapeNTM.length_encFiniteCfg_le), so the codes have a width W polynomial in n. Acceptance is reachability of the accepting code along the edges between codes of 2 * W + 2 bits (Turing.MultiTapeNTM.accepts_iff_reflTransGen_codeStep). There are 2 ^ (2 * W + 2) such words, so it is reachability within as many steps, which the recursion decides at depth 2 * W + 2. The edge test, the codes and the width are polynomial-time, so the decider runs in space polynomial in n, charging the stack of frames, the counters and the edge test (Cslib.Reachability.exists_polyBounded_space_savitch); its time is exponential.

The decider retains the whole input, so this is the polynomial-space consequence of Savitch's theorem. The quadratic bound NSPACE(s) ⊆ DSPACE(s ^ 2), including sublinear s, is Turing.MultiTapeNTM.exists_decidableInTimeAndSpace_sq, which never copies the input.

Main definitions

• Turing.MultiTapeNTM.codeWidth: the width of the codes of the views.
• Turing.MultiTapeNTM.viewCodeWidth: the bit-length 2 * codeWidth + 2 of the codes of the views.
• Turing.MultiTapeNTM.savitchDecide: the deterministic decider of acceptance.

Main results

• Turing.MultiTapeNTM.savitchDecide_eq_true_iff: the decider decides acceptance.
• Turing.MultiTapeNTM.computableInPolyTime_codeWidth: the width of the codes is polynomial-time.
• Turing.MultiTapeNTM.computableInPolyTime_viewCodeWidth: the bit-length of the codes of the views is polynomial-time.
• Turing.MultiTapeNTM.exists_polyBounded_space_savitchDecide: it runs in polynomial space.

References

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

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

The width of the codes of the views on input, under the space bound c * (input.length + 1) ^ d: the length of the encoding of the initial view plus the bound Turing.MultiTapeNTM.viewLengthBound on the encodings of all reachable views.

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

The bit-length 2 * ntm.codeWidth c d input + 2 of the codes (Turing.MultiTapeNTM.viewCode and Turing.MultiTapeNTM.acceptCode) of the views on input, under the space bound c * (input.length + 1) ^ d.

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

Savitch's decider: whether the accepting code is reachable from the code of the initial view, by Savitch's midpoint recursion on words of ntm.viewCodeWidth c d input bits at depth ntm.viewCodeWidth c d input.

theorem Turing.MultiTapeNTM.savitchDecide_eq_true_iff {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {c d s : ℕ} {input : List Bool} (hs : ntm.RunsInSpace input s) (hsc : s ≤ c * (input.length + 1) ^ d) : ntm.savitchDecide c d input = true ↔ ntm.Accepts input

Savitch's decider decides acceptance of a machine whose computation paths on input visit at most c * (input.length + 1) ^ d work cells.

theorem Turing.MultiTapeNTM.computableInPolyTime_codeWidth {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {α : Type} {enc : α ↪ List Bool} (c d : ℕ) : MultiTapeTM.ComputableInPolyTime (fun (a : α) => ntm.codeWidth c d (enc a)) enc MultiTapeTM.encUnary

The width of the codes is polynomial-time, in unary.

theorem Turing.MultiTapeNTM.computableInPolyTime_viewCodeWidth {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} (c d : ℕ) : MultiTapeTM.ComputableInPolyTime (ntm.viewCodeWidth c d) MultiTapeTM.encBits MultiTapeTM.encUnary

The bit-length of the codes of the views is polynomial-time, in unary.

theorem Turing.MultiTapeNTM.exists_polyBounded_space_savitchDecide {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) {α : Type} (enc : α ↪ List Bool) (c d : ℕ) : ∃ (t : α → ℕ) (s : α → ℕ), MultiTapeTM.PolyBounded (fun (a : α) => (enc a).length) s ∧ MultiTapeTM.ComputableInTimeAndSpace (fun (a : α) => ntm.savitchDecide c d (enc a)) enc MultiTapeTM.encBool t s

Savitch's decider runs in polynomial space: within some time and within space polynomially bounded in the length of the encoded instance.