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 [Pap94], 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
• Adapter, Follows: a machine follows another when it performs each of its transitions, reading and acting through an adapter
• Follows.step, Follows.runningStepHom, Follows.stepHom: a configuration map that agrees with the adapter maps steps to steps, so it is a homomorphism of step relations and maps run paths
• 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.

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

Equations

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

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

Equations

• ntm.runningStepRel input = {(c, c') : Turing.Cfg k Symbol State input × Turing.Cfg k Symbol State input | ¬c.Halted ∧ ntm.Step c c'}

@[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 (ntm.stepRel input)

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

Equations

• p.map f = RelSeries.map p f

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

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.

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.

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.

Following a machine

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

How a machine with k' work tapes and states State' performs the transitions of a machine with k work tapes and states State. A transition turns the symbols under the heads into an action, so the outer machine translates both ends: read computes the symbols the inner machine reads from those under the outer heads, and action turns the inner action into an outer one, which may also depend on the outer symbols.

• read : HeadSymbols k' Symbol → HeadSymbols k Symbol

  the symbols the inner machine reads

• action : HeadSymbols k' Symbol → Action k Symbol State → Action k' Symbol State'

  the outer action performing an inner action

def Turing.MultiTapeNTM.Adapter.mapState {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (φ : Option State → Option State') : Adapter k k Symbol State State'

The adapter that relabels the states through φ and reads and acts on the same tapes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Turing.MultiTapeNTM.Adapter.mapState_action_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (φ : Option State → Option State') (x✝ : HeadSymbols k Symbol) (a : Action k Symbol State) (a✝ : Fin k) : ((mapState φ).action x✝ a).workTapes a✝ = a.workTapes a✝

@[simp]

theorem Turing.MultiTapeNTM.Adapter.mapState_action_inputTape {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (φ : Option State → Option State') (x✝ : HeadSymbols k Symbol) (a : Action k Symbol State) : ((mapState φ).action x✝ a).inputTape = a.inputTape

@[simp]

theorem Turing.MultiTapeNTM.Adapter.mapState_read {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (φ : Option State → Option State') (a : HeadSymbols k Symbol) : (mapState φ).read a = id a

@[simp]

theorem Turing.MultiTapeNTM.Adapter.mapState_action_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (φ : Option State → Option State') (x✝ : HeadSymbols k Symbol) (a : Action k Symbol State) : ((mapState φ).action x✝ a).state = φ a.state

@[simp]

theorem Turing.MultiTapeNTM.Adapter.mapState_action_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (φ : Option State → Option State') (x✝ : HeadSymbols k Symbol) (a : Action k Symbol State) : ((mapState φ).action x✝ a).output = a.output

def Turing.MultiTapeNTM.Follows {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {k' : ℕ} {State' : Type u_3} (ntm' : MultiTapeNTM k' Symbol State') (ntm : MultiTapeNTM k Symbol State) (state : State → State') (adapter : Adapter k k' Symbol State State') : Prop

ntm' follows ntm through adapter, in state state q while ntm is in state q: whatever ntm may do in q on what adapter reads, ntm' may do the adapted action in state q.

Equations

• One or more equations did not get rendered due to their size.

theorem Turing.MultiTapeNTM.Follows.step {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'} {state : State → State'} {adapter : Adapter k k' Symbol State State'} (h : ntm'.Follows ntm state adapter) (f : Cfg k Symbol State input → Cfg k' Symbol State' input') {c c' : Cfg k Symbol State input} (hstep : ntm.Step c c') (hstate : Option.map state c.state = (f c).state) (hread : adapter.read (f c).headSymbols = c.headSymbols) (haction : ∀ (action : Action k Symbol State), action.apply c = c' → (adapter.action (f c).headSymbols action).apply (f c) = f c') : ntm'.Step (f c) (f c')

A follower mirrors a step. If ntm' follows ntm, and the map f relabels the state of c through state, reads through adapter what c reads, and carries the action of a step from c to its adaptation, then f maps the step to a step of ntm'.

def Turing.MultiTapeNTM.Follows.runningStepHom {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'} {state : State → State'} {adapter : Adapter k k' Symbol State State'} (h : ntm'.Follows ntm state adapter) (f : Cfg k Symbol State input → Cfg k' Symbol State' input') (hstate : ∀ (c : Cfg k Symbol State input) (q : State), c.state = some q → (f c).state = some (state q)) (hread : ∀ (c : Cfg k Symbol State input), adapter.read (f c).headSymbols = c.headSymbols) (haction : ∀ (c : Cfg k Symbol State input) (action : Action k Symbol State), (adapter.action (f c).headSymbols action).apply (f c) = f (action.apply c)) : (ntm.runningStepRel input).Hom (ntm'.stepRel input')

A follower mirrors the running steps. If ntm' follows ntm, and f sends a configuration in state q to one in state state q, from which adapter reads what the configuration reads and on which each adapted action acts as the action acts on the configuration, then f maps each running step of ntm to a step of ntm'.

Equations

• h.runningStepHom f hstate hread haction = { toFun := f, map_rel' := ⋯ }

def Turing.MultiTapeNTM.Follows.stepHom {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'} {state : State → State'} {adapter : Adapter k k' Symbol State State'} (h : ntm'.Follows ntm state adapter) (f : Cfg k Symbol State input → Cfg k' Symbol State' input') (hstate : ∀ (c : Cfg k Symbol State input), Option.map state c.state = (f c).state) (hread : ∀ (c : Cfg k Symbol State input), adapter.read (f c).headSymbols = c.headSymbols) (haction : ∀ (c : Cfg k Symbol State input) (action : Action k Symbol State), (adapter.action (f c).headSymbols action).apply (f c) = f (action.apply c)) : (ntm.stepRel input).Hom (ntm'.stepRel input')

A follower mirrors the steps. As runningStepHom, for an f that relabels every state through state, so that it also keeps halted configurations halted.

Equations

• h.stepHom f hstate hread haction = { toFun := f, map_rel' := ⋯ }

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.

Equations

• ntm.prependOutputHom pre = Turing.MultiTapeNTM.Follows.stepHom ⋯ (fun (x : Turing.Cfg k Symbol State input) => x.prependOutput pre) ⋯ ⋯ ⋯

@[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) (x✝ : Cfg k Symbol State input) : (ntm.prependOutputHom pre) x✝ = x✝.prependOutput pre