Views and their codes in polynomial time

The step relation of the views of a machine with finitely many states (Turing.MultiTapeNTM.ViewStep) is decided by Turing.MultiTapeNTM.viewStepB: a halted view steps only to itself, and a running view to the summarized result of one of the finitely many actions its transition relation permits for its control and read symbols. The test is polynomial-time in the encoded pair of views: it branches on the finite key of the first view, and each branch compares the second view with the results of a fixed finite list of fixed actions.

For Savitch's theorem the views are written as words of one width: the code of a view is a zero tag followed by its encoding padded by Cslib.BitString.padWord, and the accepting code is the word of all ones. The edge test Turing.MultiTapeNTM.codeEdge decodes both words by Turing.MultiTapeTM.decodeFiniteCfg and links the code of a view to the code of each view it steps to, and the code of a halted view with output [true] to every word with tag one. Malformed words with tag zero decode to some view, which is harmless: every word with tag zero reachable from the code of the initial view decodes to a view reachable from the initial view. Acceptance is then reachability of the accepting code (Turing.MultiTapeNTM.accepts_iff_reflTransGen_codeStep), and the edge test, the initial code and the accepting code are polynomial-time.

Main definitions

• Turing.MultiTapeNTM.viewStepB: the Boolean step test of views.
• Turing.MultiTapeNTM.viewCode, Turing.MultiTapeNTM.acceptCode: codes of views and the accepting code.
• Turing.MultiTapeNTM.codeEdge, Turing.MultiTapeNTM.CodeStep: the edges between codes.

Main results

• Turing.MultiTapeNTM.viewStepB_iff: the test decides Turing.MultiTapeNTM.ViewStep.
• Turing.MultiTapeNTM.computableInPolyTime_viewStepB: the test is polynomial-time.
• Turing.MultiTapeNTM.computableInPolyTime_decodeView: reading the view of a computed code is polynomial-time.
• Turing.MultiTapeNTM.accepts_iff_reflTransGen_codeStep: acceptance is reachability of the accepting code.
• Turing.MultiTapeNTM.computableInPolyTime_codeEdge, Turing.MultiTapeNTM.computableInPolyTime_viewCode_initView, Turing.MultiTapeNTM.computableInPolyTime_acceptCode: the edge test, the initial code and the accepting code are polynomial-time.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.5

theorem Turing.MultiTapeTM.ComputableInPolyTime.outputClass : ComputableInPolyTime MultiTapeNTM.outputClass encBits encBits

The output summary is polynomial-time on raw words.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_summarizeOutput {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime FiniteCfg.summarizeOutput encFiniteCfg encFiniteCfg

Summarizing the output of a configuration is polynomial-time.

noncomputable def Turing.MultiTapeNTM.viewStepB {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (views : FiniteCfg k Bool State × FiniteCfg k Bool State) : Bool

The step test of views.

theorem Turing.MultiTapeNTM.viewStepB_iff {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) {finite next : FiniteCfg k Bool State} : ntm.viewStepB (finite, next) = true ↔ ntm.ViewStep finite next

The test decides the steps of views.

theorem Turing.MultiTapeNTM.computableInPolyTime_viewStepB {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) : MultiTapeTM.ComputableInPolyTime ntm.viewStepB (MultiTapeTM.encPair MultiTapeTM.encFiniteCfg MultiTapeTM.encFiniteCfg) MultiTapeTM.encBool

The step test is polynomial-time in the encoded pair of views.

Codes of views

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

The code of a view for encodings of length at most width: a zero tag, then its encoding padded to 2 * width + 1 bits (Cslib.BitString.padWord).

def Turing.MultiTapeNTM.acceptCode (width : ℕ) : List Bool

The accepting code for width width: all ones. Its tag is one, so it is no view's code.

noncomputable def Turing.MultiTapeNTM.decodeView {k : ℕ} {State : Type} [Finite State] : List Bool → Option (FiniteCfg k Bool State)

Read the view of a code with a zero tag: decode its first frame by Turing.MultiTapeTM.decodeFiniteCfg.

noncomputable def Turing.MultiTapeNTM.codeEdge {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (code next : List Bool) : Bool

The edge test of codes. A code of a view finite has an edge to every code with tag one if finite has halted with output [true], and to the code of every view finite steps to.

def Turing.MultiTapeNTM.CodeStep {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (width : ℕ) (code next : List Bool) : Prop

The edges between codes of 2 * width + 2 bits.

theorem Turing.MultiTapeNTM.decodeView_viewCode {k : ℕ} {State : Type} [Finite State] (width : ℕ) (finite : FiniteCfg k Bool State) : decodeView (viewCode width finite) = some finite

The code of a view decodes to the view.

theorem Turing.MultiTapeNTM.length_viewCode {k : ℕ} {State : Type} [Finite State] {width : ℕ} {finite : FiniteCfg k Bool State} (h : (MultiTapeTM.encFiniteCfg finite).length ≤ width) : (viewCode width finite).length = 2 * width + 2

The code of a view with an encoding of length at most width has 2 * width + 2 bits.

theorem Turing.MultiTapeNTM.codeEdge_viewCode {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {width : ℕ} {finite next : FiniteCfg k Bool State} : ntm.codeEdge (viewCode width finite) (viewCode width next) = true ↔ ntm.ViewStep finite next

Between codes of views, the edges are the steps of the views.

theorem Turing.MultiTapeNTM.codeEdge_acceptCode {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {width : ℕ} {finite : FiniteCfg k Bool State} : ntm.codeEdge (viewCode width finite) (acceptCode width) = true ↔ finite.state = none ∧ finite.output = [true]

The code of a view has an edge to the accepting code exactly when the view has halted with output [true].

theorem Turing.MultiTapeNTM.accepts_iff_reflTransGen_codeStep {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {width : ℕ} (hwidth : ∀ (finite : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite → (MultiTapeTM.encFiniteCfg finite).length ≤ width) : ntm.Accepts input ↔ Relation.ReflTransGen (ntm.CodeStep width) (viewCode width (ntm.initView input)) (acceptCode width)

Acceptance is reachability of the accepting code, along the edges between codes of a width at least the length of the encoding of every reachable view.

The edge test in polynomial time

theorem Turing.MultiTapeNTM.decodeView_eq {k : ℕ} {State : Type} [Finite State] (code : List Bool) : decodeView code = if code.headD true = true then none else some (MultiTapeTM.decodeFiniteCfg (MultiTapeTM.unframe code.tail))

Reading the view of a code, by cases on its tag.

theorem Turing.MultiTapeNTM.computableInPolyTime_decodeView {k : ℕ} {State : Type} [Finite State] {α : Type} {encA : α ↪ List Bool} {code : α → List Bool} (hcode : MultiTapeTM.ComputableInPolyTime code encA MultiTapeTM.encBits) : MultiTapeTM.ComputableInPolyTime (fun (a : α) => decodeView (code a)) encA (MultiTapeTM.encOption MultiTapeTM.encFiniteCfg)

Reading the view of a computed code is polynomial-time.

theorem Turing.MultiTapeNTM.computableInPolyTime_codeEdge {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {α : Type} {encA : α ↪ List Bool} {code next : α → List Bool} (hcode : MultiTapeTM.ComputableInPolyTime code encA MultiTapeTM.encBits) (hnext : MultiTapeTM.ComputableInPolyTime next encA MultiTapeTM.encBits) : MultiTapeTM.ComputableInPolyTime (fun (a : α) => ntm.codeEdge (code a) (next a)) encA MultiTapeTM.encBool

The edge test of codes is polynomial-time.

theorem Turing.MultiTapeNTM.computableInPolyTime_viewCode_initView {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {α : Type} {encA : α ↪ List Bool} {width : α → ℕ} {word : α → List Bool} (hwidth : MultiTapeTM.ComputableInPolyTime width encA MultiTapeTM.encUnary) (hword : MultiTapeTM.ComputableInPolyTime word encA MultiTapeTM.encBits) : MultiTapeTM.ComputableInPolyTime (fun (a : α) => viewCode (width a) (ntm.initView (word a))) encA MultiTapeTM.encBits

The code of the initial view of a computed input is polynomial-time, for a polynomial-time width.

theorem Turing.MultiTapeNTM.computableInPolyTime_acceptCode {α : Type} {encA : α ↪ List Bool} {width : α → ℕ} (hwidth : MultiTapeTM.ComputableInPolyTime width encA MultiTapeTM.encUnary) : MultiTapeTM.ComputableInPolyTime (fun (a : α) => acceptCode (width a)) encA MultiTapeTM.encBits

The accepting code of a polynomial-time width is polynomial-time.