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 [Papadimitriou94], 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][Papadimitriou94]
• [M. Sipser, Introduction to the Theory of Computation][Sipser2013]

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.

Equations

• ntm.Step c₁ c₂ = match c₁.state with | none => c₂ = c₁ | some q => ∃ (action : Turing.Action k Symbol State), ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols action ∧ c₂ = action.apply c₁

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.

Equations

• ntm.initCfg input = Turing.Cfg.init ntm.q₀ input

@[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.

Equations

• ntm.RunPath input = RelSeries {(c, c') : Turing.Cfg k Symbol State input × Turing.Cfg k Symbol State input | ntm.Step c c'}

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.

Equations

• p.time = p.length

structure Turing.MultiTapeNTM.ComputationPath {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) extends RelSeries {(c, c') : Turing.Cfg k Symbol State input × Turing.Cfg k Symbol State input | ntm.Step c c'} : 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) ∈ {(c, c') : Turing.Cfg k Symbol State input × Turing.Cfg k Symbol State input | ntm.Step c c'}
• 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.

Equations

• p.time = Turing.MultiTapeNTM.RunPath.time p.toRunPath

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.

Equations

• ntm.RunsInTime input t = ∀ (p : ntm.ComputationPath input), t ≤ p.time → p.last.Halted

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.