Codes of views without the input

A view of a nondeterministic machine (Turing.FiniteCfg, as in Turing.MultiTapeNTM.accepts_iff_reflTransGen_viewStep) stores its input, so its encoding is at least as long as the input. All the views reachable on one input share that input, and the rest of a view is short under a small space bound: Turing.MultiTapeNTM.coreCode encodes the input head position in binary, the control, the work tapes relative to their heads and the output summary. It identifies views with the same input (Turing.MultiTapeNTM.coreCode_injective), and on views reachable within space s on an input of length n it has length O(log n + s) (Turing.MultiTapeNTM.length_coreCode_le). So at most 2 ^ O(log n + s) distinct views are reachable (Turing.MultiTapeNTM.length_le_of_nodup_reachable), polynomially many in n under a logarithmic space bound Sipser, Section 8.4.

Main definitions

• Turing.MultiTapeNTM.coreCode: the code of a view without its input.
• Turing.MultiTapeNTM.coreLengthBound: the bound on the codes of reachable views.

Main results

• Turing.MultiTapeNTM.spaceUsed_workTapes_le: reachable views store few cells per work tape.
• Turing.MultiTapeNTM.coreCode_injective: the code identifies views with the same input.
• Turing.MultiTapeNTM.length_coreCode_le: reachable views have short codes.
• Turing.MultiTapeNTM.length_le_of_nodup_reachable: few distinct views are reachable.

References

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

theorem Turing.MultiTapeNTM.spaceUsed_workTapes_le {k : ℕ} {State : Type} {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s : ℕ} (hs : ntm.RunsInSpace input s) {finite : FiniteCfg k Bool State} (h : Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite) (tape : Fin k) : (finite.workTapes tape).spaceUsed ≤ 4 * s + 1

Reachable views store few cells per work tape: under a space bound s, every work tape of a view reachable from the initial view is stored in at most 4 * s + 1 cells.

noncomputable def Turing.MultiTapeNTM.encCore {k : ℕ} {State : Type} [Finite State] : ℕ × Option State × (Fin k → Cslib.Turing.BiTape Bool) × List Bool ↪ List Bool

The encoding of a view without its input: the input head position in binary, the control, the work tapes and the output.

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

The code of a view without its input: its input head position in binary, its control, its work tapes relative to their heads and its output.

theorem Turing.MultiTapeNTM.coreCode_injective {k : ℕ} {State : Type} [Finite State] {finite finite' : FiniteCfg k Bool State} (hinput : finite.input = finite'.input) (h : coreCode finite = coreCode finite') : finite = finite'

The code identifies views with the same input.

noncomputable def Turing.MultiTapeNTM.coreLengthBound (k : ℕ) (State : Type) (n s : ℕ) : ℕ

The bound on the codes of the views reachable within space s on inputs of length n: logarithmic in n and linear in s, with a constant depending only on k and State.

theorem Turing.MultiTapeNTM.length_coreCode_le {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s : ℕ} (hs : ntm.RunsInSpace input s) {finite : FiniteCfg k Bool State} (h : Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite) : (coreCode finite).length ≤ coreLengthBound k State input.length s

Reachable views have short codes: under a space bound s, the code of every view reachable from the initial view has length at most coreLengthBound k State n s.

theorem Turing.MultiTapeNTM.length_le_of_nodup_reachable {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {s : ℕ} (hs : ntm.RunsInSpace input s) {views : List (FiniteCfg k Bool State)} (hnodup : views.Nodup) (hreach : ∀ finite ∈ views, Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite) : views.length ≤ 2 ^ (2 * coreLengthBound k State input.length s + 1)

Few distinct views are reachable: under a space bound s, a list of distinct views reachable from the initial view has at most 2 ^ (2 * coreLengthBound k State n s + 1) entries, since padding their codes to one length identifies no two of them.