Nondeterministic Multi-Tape Turing Machines

Defines nondeterministic Turing machines with a read-only input tape, k work tapes and one write-only output tape, their computation paths, and time bounds.

Design

The design choices for configurations and actions are documented in Cslib.Computability.Machines.Turing.MultiTape.Configuration.

Following [Pap94a], chapter 2.7, a nondeterministic machine is a Turing machine whose transition function is replaced by a transition relation: Tr q input work action holds when Tr relates the state q and the read symbols input and work to action.

A halted configuration steps to itself, so once a machine has halted it has a run of every length. A time bound is therefore an upper bound, with no separate account of the step at which it halted.

The transition relation may be empty at a running configuration. Such a configuration has no successor configuration and is called stuck.

Time bounds apply to every computation path, regardless of its outcome. RunsInTime input t requires every path of at least t steps to end in a halted configuration.

Important Declarations

• MultiTapeNTM: the machine, an initial state and a transition relation
• Step: the one-step relation on configurations
• RunPath: finite relation series of steps
• ComputationPath: a run path starting at the initial configuration
• RunsInTime: every computation path of at least the given length ends in a halted configuration

References

• C. Papadimitriou, Computational Complexity
• M. Sipser, Introduction to the Theory of Computation

theorem RelSeries.exists_of_mem_map {α : Type u_1} {β : Type u_2} {r : SetRel α α} {s : SetRel β β} {p : RelSeries r} {f : r.Hom s} {b : β} (hb : b ∈ p.map f) : ∃ a ∈ p, f a = b

A member of a mapped series is the image of a member.

theorem RelSeries.mem_or_mem_of_mem_smash {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} {h : p.last = q.head} {a : α} (ha : a ∈ p.smash q h) : a ∈ p ∨ a ∈ q

A member of two joined series lies on one of them.

structure Turing.MultiTapeNTM (k : ℕ) (Symbol : Type u_3) (State : Type u_4) : Type (max u_3 u_4)

A nondeterministic multi-tape Turing machine with k work tapes over the alphabet of Option Symbol (where none is the blank symbol). Neither Symbol nor State is required to be finite.

• q₀ : State

  initial state

• Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) (action : Action k Symbol State) : Prop

  transition relation: which combinations of state, current input symbol, tuple of work head symbols and resulting actions are valid transitions

def Turing.MultiTapeNTM.Step {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (ntm : MultiTapeNTM k Symbol State) (c₁ c₂ : Cfg k Symbol State input) : Prop

The one-step relation on configurations. A halted configuration steps only to itself. A running configuration steps by applying any action related to its state and read symbols by Tr.

theorem Turing.MultiTapeNTM.step_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {c c' : Cfg k Symbol State input} (h : c.Halted) : ntm.Step c c' ↔ c' = c

A halted configuration steps only to itself.

def Turing.MultiTapeNTM.initCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : Cfg k Symbol State input

The initial configuration corresponding to an input string.

@[reducible, inline]

abbrev Turing.MultiTapeNTM.stepRel {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : SetRel (Cfg k Symbol State input) (Cfg k Symbol State input)

The one-step relation on configurations for input, as a set of pairs.

@[reducible, inline]

abbrev Turing.MultiTapeNTM.runningStepRel {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : SetRel (Cfg k Symbol State input) (Cfg k Symbol State input)

The steps of ntm from running configurations: the steps within a run until it halts.

@[reducible, inline]

abbrev Turing.MultiTapeNTM.RunPath {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : Type (max u_1 u_2)

A nonempty list of configurations joined by steps of ntm.

@[reducible, inline]

abbrev Turing.MultiTapeNTM.RunPath.map {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {ntm' : MultiTapeNTM k' Symbol State'} (p : ntm.RunPath input) (f : (ntm.stepRel input).Hom (ntm'.stepRel input')) : ntm'.RunPath input'

A run path mapped along a step-preserving map of configurations: RelSeries.map, typed as a run path of the target machine.

theorem Turing.MultiTapeNTM.RunPath.length_output_mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) : Monotone fun (i : Fin (p.length + 1)) => (p.toFun i).output.length

The output only grows along a run path.

theorem Turing.MultiTapeNTM.RunPath.last_eq_of_head_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (h : (RelSeries.head p).Halted) : RelSeries.last p = RelSeries.head p

Once a run path is halted, its configuration stays unchanged.

theorem Turing.MultiTapeNTM.RunPath.last_eq_of_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (i : Fin (p.length + 1)) (h : (p.toFun i).Halted) : RelSeries.last p = p.toFun i

The last configuration equals any earlier halted configuration.

def Turing.MultiTapeNTM.RunPath.time {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) : ℕ

The number of steps taken by a run path.

theorem Turing.MultiTapeNTM.RunPath.exists_running {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (h : (RelSeries.last p).Halted) : ∃ (q : RelSeries (ntm.runningStepRel input)), q.head = RelSeries.head p ∧ q.last = RelSeries.last p ∧ q.length ≤ p.length ∧ ∀ c ∈ q, c ∈ p

A path that ends halted runs from its head to its last configuration in running steps, up to its first halted configuration.

def Turing.MultiTapeNTM.prependOutputHom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (ntm : MultiTapeNTM k Symbol State) (pre : List Symbol) : (ntm.stepRel input).Hom (ntm.stepRel input)

A machine never reads its output tape, so prepending a word to the output preserves steps.

@[simp]

theorem Turing.MultiTapeNTM.prependOutputHom_apply {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (ntm : MultiTapeNTM k Symbol State) (pre : List Symbol) (c : Cfg k Symbol State input) : (ntm.prependOutputHom pre) c = c.prependOutput pre

structure Turing.MultiTapeNTM.ComputationPath {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) extends RelSeries (ntm.stepRel input) : Type (max u_1 u_2)

A run path starting at the initial configuration for input.

• length : ℕ
• toFun : Fin (self.length + 1) → Turing.Cfg k Symbol State input
• step (i : Fin self.length) : (self.toFun i.castSucc, self.toFun i.succ) ∈ ntm.stepRel input
• head_eq : self.head = ntm.initCfg input

  the path starts at the initial configuration

def Turing.MultiTapeNTM.ComputationPath.time {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.ComputationPath input) : ℕ

The number of steps taken by a computation path.

def Turing.MultiTapeNTM.RunsInTime {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) (t : ℕ) : Prop

Every computation path on input of at least t steps ends in a halted configuration. A path ending in a stuck configuration must have fewer than t steps.

theorem Turing.MultiTapeNTM.RunsInTime.mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} {t t' : ℕ} (h : ntm.RunsInTime input t) (ht : t ≤ t') : ntm.RunsInTime input t'

A time bound can be increased.