Finite views of space-bounded nondeterministic machines

A nondeterministic machine whose computation paths visit at most s work-tape cells reaches only configurations of bounded size, however long it runs. This file gives these configurations a finite description that preserves acceptance.

Along a run path from blank tapes with every head at 0, the heads move by at most one cell per step and only visited cells are written, so every head position and every non-blank cell lies within the space used by its tape (Turing.MultiTapeNTM.RunPath.natAbs_lt_spaceUsedByTape).

A configuration is viewed as finite data (Turing.FiniteCfg), with every work tape stored relative to its head and the append-only output summarized by Turing.MultiTapeNTM.outputClass: empty, exactly [true], or [false] for every other word. The summary is a congruence for appending, so the views step exactly as the machine does (Turing.MultiTapeNTM.ViewStep); a halted view steps only to itself. A computation path accepts exactly when a halted view with output [true] is reachable from the initial view (Turing.MultiTapeNTM.accepts_iff_reflTransGen_viewStep). Under a space bound every reachable view has a bounded encoding (Turing.MultiTapeNTM.length_encFiniteCfg_le), whatever the length of the path reaching it.

Main definitions

• Turing.MultiTapeNTM.outputClass: the summary of an output word.
• Turing.MultiTapeNTM.ViewStep: the steps of the views of a machine.

Main results

• Turing.MultiTapeNTM.RunPath.natAbs_lt_spaceUsedByTape: heads and non-blank cells lie within the space used.
• Turing.MultiTapeNTM.accepts_iff_reflTransGen_viewStep: acceptance is reachability of views.
• Turing.MultiTapeNTM.length_encFiniteCfg_le: reachable views are small under a space bound.

References

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

theorem Turing.MultiTapeNTM.RunPath.mem_visitedByTapeHead_iff {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {p : ntm.RunPath input} {i : Fin k} {z : ℤ} : z ∈ p.visitedByTapeHead i ↔ ∃ c ∈ p, c.workTapePos i = z

A position is visited exactly when a configuration of the path has the head there.

theorem Turing.MultiTapeNTM.RunPath.visitedByTapeHead_snoc {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (c : Cfg k Symbol State input) (h : (RelSeries.last p, c) ∈ ntm.stepRel input) (i : Fin k) : visitedByTapeHead (RelSeries.snoc p c h) i = insert (c.workTapePos i) (p.visitedByTapeHead i)

The positions visited by a head after one more step.

theorem Turing.MultiTapeNTM.RunPath.visitedByTapeHead_singleton {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (c : Cfg k Symbol State input) (i : Fin k) : visitedByTapeHead (RelSeries.singleton (ntm.stepRel input) c) i = {c.workTapePos i}

A single configuration visits its head position only.

structure Turing.MultiTapeNTM.RunPath.VisitedInterval {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (i : Fin k) : Prop

The invariant of a run path from blank tapes with the heads at 0: the visited positions form an interval around 0 containing every non-blank cell.

• zero_mem : 0 ∈ p.visitedByTapeHead i

  The starting position is visited.

• convex (a : ℤ) : a ∈ p.visitedByTapeHead i → ∀ b ∈ p.visitedByTapeHead i, ∀ (z : ℤ), a ≤ z → z ≤ b → z ∈ p.visitedByTapeHead i

  The visited positions form an interval.

• written (z : ℤ) : (RelSeries.last p).workTapes i z ≠ none → z ∈ p.visitedByTapeHead i

  Every non-blank cell of the last configuration has been visited.

theorem Turing.MultiTapeNTM.RunPath.visitedInterval {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (hblank : ∀ (i : Fin k) (z : ℤ), (RelSeries.head p).workTapes i z = none) (hpos : ∀ (i : Fin k), (RelSeries.head p).workTapePos i = 0) (i : Fin k) : p.VisitedInterval i

The invariant holds along every run path from blank tapes with the heads at 0.

theorem Turing.MultiTapeNTM.RunPath.VisitedInterval.natAbs_lt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {p : ntm.RunPath input} {i : Fin k} (h : p.VisitedInterval i) {z : ℤ} (hz : z ∈ p.visitedByTapeHead i) : z.natAbs < p.spaceUsedByTape i

Positions of an interval around 0 are smaller than its size.

theorem Turing.MultiTapeNTM.RunPath.natAbs_lt_spaceUsedByTape {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (hblank : ∀ (i : Fin k) (z : ℤ), (RelSeries.head p).workTapes i z = none) (hpos : ∀ (i : Fin k), (RelSeries.head p).workTapePos i = 0) (i : Fin k) : ((RelSeries.last p).workTapePos i).natAbs < p.spaceUsedByTape i ∧ ∀ (z : ℤ), (RelSeries.last p).workTapes i z ≠ none → z.natAbs < p.spaceUsedByTape i

Heads and written cells lie within the space used. On a run path from blank tapes with the heads at 0, the last head position and every non-blank cell of a tape are smaller in absolute value than the number of cells the tape's head has visited.

The size of tapes with bounded contents

theorem Cslib.Turing.StackTape.length_le_of_read_eq_none {Symbol : Type u_1} (tape : StackTape Symbol) {m : ℕ} (h : ∀ (j : ℕ), m ≤ j → tape.read j = none) : tape.length ≤ m

A stack that reads blank from position m on stores at most m cells, since its last stored cell is not blank.

theorem Cslib.Turing.BiTape.spaceUsed_le_of_read_eq_none {Symbol : Type u_1} (tape : BiTape Symbol) {m : ℕ} (hleft : ∀ (j : ℕ), m ≤ j → tape.read (Int.negSucc j) = none) (hright : ∀ (j : ℕ), m ≤ j → tape.read (↑j + 1) = none) : tape.spaceUsed ≤ 2 * m + 1

A tape whose cells are blank from displacement m on, on both sides, uses at most 2 * m + 1 cells.

Views

def Turing.MultiTapeNTM.outputClass (word : List Bool) : List Bool

The summary of an output word for acceptance: empty, exactly [true], or [false] for every other word.

@[simp]

theorem Turing.MultiTapeNTM.outputClass_nil : outputClass [] = []

The empty word is its own summary.

theorem Turing.MultiTapeNTM.outputClass_eq_true_iff {word : List Bool} : outputClass word = [true] ↔ word = [true]

The summary is [true] exactly for the word [true].

theorem Turing.MultiTapeNTM.outputClass_of_two_le {word : List Bool} (h : 2 ≤ word.length) : outputClass word = [false]

Words of at least two symbols are summarized as [false].

theorem Turing.MultiTapeNTM.length_outputClass_cons (a : Bool) (word : List Bool) : (outputClass (a :: word)).length = 1

Nonempty words have a summary of one symbol.

theorem Turing.MultiTapeNTM.outputClass_append (word : List Bool) (symbol : Option Bool) : outputClass (outputClass word ++ symbol.toList) = outputClass (word ++ symbol.toList)

The summary is a congruence for appending a symbol.

theorem Turing.MultiTapeNTM.length_outputClass_le (word : List Bool) : (outputClass word).length ≤ 1

The summary has at most one symbol.

def Turing.FiniteCfg.summarizeOutput {k : ℕ} {State : Type u_1} (finite : FiniteCfg k Bool State) : FiniteCfg k Bool State

The finite configuration with its output replaced by the summary.

def Turing.MultiTapeNTM.ViewStep {k : ℕ} {State : Type u_1} (ntm : MultiTapeNTM k Bool State) (finite next : FiniteCfg k Bool State) : Prop

The steps of the views. A running view takes the summarized result of a permitted action; a halted view steps only to itself.

def Turing.MultiTapeNTM.initView {k : ℕ} {State : Type u_1} (ntm : MultiTapeNTM k Bool State) (input : List Bool) : FiniteCfg k Bool State

The initial view on an input.

structure Turing.MultiTapeNTM.ViewRep {k : ℕ} {State : Type u_1} {input : List Bool} (finite : FiniteCfg k Bool State) (cfg : Cfg k Bool State input) : Prop

A view represents a native configuration on input: the same input, control and input head, work tapes centered at the native heads, and the summary of the native output. With the native output in place of the summary, it is Turing.FiniteCfg.Represents (ViewRep.represents).

• input : finite.input = input

  The inputs agree.

• state : finite.state = cfg.state

  The controls agree.

• inputPos : ↑finite.inputPos = ↑cfg.inputPos

  The input heads agree.

• workTapes (tape : Fin k) : (finite.workTapes tape).Represents (cfg.workTapes tape) (cfg.workTapePos tape)

  Each work tape represents the native tape at its native head.

• output : finite.output = outputClass cfg.output

  The output is the summary of the native output.

theorem Turing.MultiTapeNTM.viewRep_init {k : ℕ} {State : Type u_1} {ntm : MultiTapeNTM k Bool State} (input : List Bool) : ViewRep (ntm.initView input) (ntm.initCfg input)

The initial view represents the initial configuration.

theorem Turing.MultiTapeNTM.ViewRep.represents {k : ℕ} {State : Type u_1} {finite : FiniteCfg k Bool State} {cfg : Cfg k Bool State finite.input} (h : ViewRep finite cfg) : { input := finite.input, state := finite.state, inputPos := finite.inputPos, workTapes := finite.workTapes, output := cfg.output }.Represents cfg

With the native output in place of the summary, a view on the native input is a Turing.FiniteCfg.Represents of the native configuration.

theorem Turing.MultiTapeNTM.ViewRep.symbols {k : ℕ} {State : Type u_1} {input : List Bool} {finite : FiniteCfg k Bool State} {cfg : Cfg k Bool State input} (h : ViewRep finite cfg) : finite.inputSymbol = cfg.inputSymbol ∧ finite.workTapeSymbols = cfg.workTapeSymbols

Represented configurations read the same symbols.

theorem Turing.MultiTapeNTM.ViewRep.step {k : ℕ} {State : Type u_1} {input : List Bool} {finite : FiniteCfg k Bool State} {cfg : Cfg k Bool State input} (h : ViewRep finite cfg) (action : Action k Bool State) : ViewRep (finite.step action).summarizeOutput (action.apply cfg)

Views step with the machine. The same action preserves the representation.

theorem Turing.MultiTapeNTM.exists_viewStep_of_runPath {k : ℕ} {State : Type u_1} {ntm : MultiTapeNTM k Bool State} {input : List Bool} (p : ntm.RunPath input) (hp : RelSeries.head p = ntm.initCfg input) : ∃ (finite : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite ∧ ViewRep finite (RelSeries.last p)

Every computation path has a reachable view.

theorem Turing.MultiTapeNTM.exists_computationPath_of_viewStep {k : ℕ} {State : Type u_1} {ntm : MultiTapeNTM k Bool State} {input : List Bool} {finite : FiniteCfg k Bool State} (h : Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite) : ∃ (p : ntm.ComputationPath input), ViewRep finite p.last

Every reachable view is the view of a computation path.

theorem Turing.MultiTapeNTM.accepts_iff_reflTransGen_viewStep {k : ℕ} {State : Type u_1} {ntm : MultiTapeNTM k Bool State} {input : List Bool} : ntm.Accepts input ↔ ∃ (finite : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite ∧ finite.state = none ∧ finite.output = [true]

Acceptance is reachability of views. A machine accepts exactly when a halted view with output [true] is reachable from the initial view.

The size of reachable views

theorem Cslib.Turing.BiTape.Represents.spaceUsed_le {tape : BiTape Bool} {contents : ℤ → Option Bool} {head : ℤ} (h : tape.Represents contents head) {s : ℕ} (hhead : head.natAbs < s) (hcells : ∀ (z : ℤ), contents z ≠ none → z.natAbs < s) : tape.spaceUsed ≤ 4 * s + 1

A tape representing contents whose head and non-blank cells lie within distance s of 0 is stored in at most 4 * s + 1 cells relative to its head.

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

The bound of Turing.MultiTapeNTM.length_encFiniteCfg_le on the encodings of the reachable views of a machine with k work tapes and controls State, on inputs of length n under the space bound s: linear in n and s, with a constant depending only on k and State.

theorem Turing.MultiTapeNTM.viewLengthBound_mono (k : ℕ) (State : Type u_1) (n : ℕ) {s s' : ℕ} (h : s ≤ s') : viewLengthBound k State n s ≤ viewLengthBound k State n s'

The bound grows with the space bound.

theorem Turing.MultiTapeNTM.length_encFiniteCfg_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) : (MultiTapeTM.encFiniteCfg finite).length ≤ viewLengthBound k State input.length s

Reachable views are small. Under a space bound s, every view reachable from the initial view has an encoding of length at most Turing.MultiTapeNTM.viewLengthBound, linear in the input and in s, whatever the length of the path reaching it.