Configurations of Multi-Tape Turing Machines

Configurations of a multi-tape Turing machine with a read-only input tape, k work tapes and one write-only output tape, together with what a single transition does to a configuration.

The configurations are used by both deterministic and nondeterministic multi-tape Turing machines and give instantaneous descriptions of their state. An Action describes how one configuration transitions to the next. It records which way the input head moves, what is written and where the work heads move, which symbol is emitted and which state follows. Action.apply carries out the action on a configuration.

Design

Configurations and actions are defined independently of a machine.

The output tape is part of the configuration, so the string emitted along a run can be read off the configuration the run ends in. An action can optionally output one symbol, which models the write-only output tape.

The input head can move freely on the input, but any move attempt beyond one cell outside the input results in no movement. Restricting the movement of the input head is not essential, but useful because it allows us to easily bound the number of possible configurations of a space-bounded machine. Most textbooks have this restriction.

This definition is adapted from the one in [Pap94a], chapter 2.3 including the sub-linear space modifications from chapter 2.5 with the following changes:

• We allow Turing machines to choose to not write on a tape. This is equivalent to writing the read symbol again but makes it easier to reason about the semantics.
• Our tapes are infinite in both directions instead of just to the right. This definition is equivalent (see [AB09], Claim 1.4). It saves us from having to add a "start marker" to the alphabet.
• We only have a single halting state. The different ways to halt (accepting, rejecting, etc) can be distinguished based on the output.
• The input-head restriction is enforced by Action.apply, rather than by restricting the transition relation. The two definitions are equivalent, but allowing all actions makes it easier to define a universal machine.

Important Declarations

• Cfg: the configuration: the internal state, the tape contents and head positions, and the output tape
• Action: what a machine does in one step
• Action.apply: the effect of one action on a configuration
• Cfg.Halted, Cfg.init: halting, and the configuration a machine starts in

References

• C. Papadimitriou, Computational Complexity
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

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

What a machine does in one step.

• inputTape : SignType

  The movement (attempt) of the input head.

• workTapes : Fin k → Option (Option Symbol) × SignType

  Actions on the work tapes: optionally a symbol to write and the head movement.

• output : Option Symbol

  An optional symbol to output.

• state : Option State

  The successor state or none to halt.

structure Turing.Cfg (k : ℕ) (Symbol : Type u_3) (State : Type u_4) (input : List Symbol) : Type (max u_3 u_4)

The configurations of a Turing machine is relative to the input of the machine and consist of:

• an Optional state (or none for the halting state),
• the position of the input head (shifted by one),
• the contents of the work tape,
• the positions of the work tape heads,
• the contents of the write-only output tape

• state : Option State

  the state of the TM (or none for the halting state)

• inputPos : Fin (input.length + 2)

  the position of the input head, shifted by one

• workTapes : Fin k → ℤ → Option Symbol

  the work tapes

• workTapePos : Fin k → ℤ

  the positions of the heads on the work tapes

• output : List Symbol

  the contents of the write-only output tape

theorem Turing.Cfg.ext {k : ℕ} {Symbol : Type u_3} {State : Type u_4} {input : List Symbol} {x y : Cfg k Symbol State input} (state : x.state = y.state) (inputPos : x.inputPos = y.inputPos) (workTapes : x.workTapes = y.workTapes) (workTapePos : x.workTapePos = y.workTapePos) (output : x.output = y.output) : x = y

theorem Turing.Cfg.ext_iff {k : ℕ} {Symbol : Type u_3} {State : Type u_4} {input : List Symbol} {x y : Cfg k Symbol State input} : x = y ↔ x.state = y.state ∧ x.inputPos = y.inputPos ∧ x.workTapes = y.workTapes ∧ x.workTapePos = y.workTapePos ∧ x.output = y.output

@[instance_reducible]

instance Turing.instInhabitedCfg {a✝ : ℕ} {a✝¹ : Type u_3} {a✝² : Type u_4} {a✝³ : List a✝¹} : Inhabited (Cfg a✝ a✝¹ a✝² a✝³)

theorem Turing.Cfg.ext_zero_tapes {Symbol : Type u_3} {State : Type u_4} {input : List Symbol} {cfg₁ cfg₂ : Cfg 0 Symbol State input} (state : cfg₁.state = cfg₂.state) (inputPos : cfg₁.inputPos = cfg₂.inputPos) (output : cfg₁.output = cfg₂.output) : cfg₁ = cfg₂

Two configurations with no work tapes are equal when their state, input head and output agree.

def Turing.moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : Fin (n + 2)

Attempt to move the input tape head. The machine can only read one empty cell outside of the input, any attempted movement beyond that results in no movement.

The addition is performed in ℤ before clamping. Performing it in Fin (n + 2) would wrap an outward boundary move to the opposite end of the input.

@[simp]

theorem Turing.moveInputPos_zero {n : ℕ} (pos : Fin (n + 2)) : moveInputPos pos 0 = pos

@[simp]

theorem Turing.moveInputPos_leftBoundary {n : ℕ} : moveInputPos 0 (-1) = 0

@[simp]

theorem Turing.moveInputPos_rightBoundary {n : ℕ} : moveInputPos ⟨n + 1, ⋯⟩ 1 = ⟨n + 1, ⋯⟩

theorem Turing.moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) : moveInputPos p SignType.neg = ⟨↑p - 1, ⋯⟩

A left move away from the left input boundary decrements the native input position.

theorem Turing.moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : ↑p ≠ n + 1) : moveInputPos p SignType.pos = ⟨↑p + 1, ⋯⟩

A right move away from the right input boundary increments the native input position.

theorem Turing.val_moveInputPos_eq {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : ↑↑(moveInputPos pos m) = min (↑n + 1) (max 0 (↑↑pos + ↑m))

The value of the input head after a move, as a clamped integer. omega-friendly.

theorem Turing.val_moveInputPos_le {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : ↑(moveInputPos pos m) ≤ ↑pos + 1

The input head moves by at most one position.

def Turing.Cfg.inputSymbol {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) : Option Symbol

The symbol currently under the input tape head.

theorem Turing.inputSymbol_eq_none_of_boundary {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {cfg : Cfg k Symbol State input} (h : ↑cfg.inputPos = 0 ∨ ↑cfg.inputPos = input.length + 1) : cfg.inputSymbol = none

At either boundary of the input, the head reads a blank.

@[simp]

theorem Turing.inputSymbolInner {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {cfg : Cfg k Symbol State input} (p : ℕ) (h₁ : ↑cfg.inputPos = 1 + p) (h₂ : p < input.length) : cfg.inputSymbol = some input[p]

def Turing.Cfg.workTapeSymbols {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol

The symbol read by work tape i.

@[reducible, inline]

abbrev Turing.Cfg.Halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) : Prop

A configuration is halted when it has no state to continue from.

def Turing.Cfg.prependOutput {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (pre : List Symbol) : Cfg k Symbol State input

The same configuration with a word prepended to the output tape. A machine never reads its output, so prepending to it preserves steps: cf. Turing.MultiTapeNTM.prependOutputHom.

@[simp]

theorem Turing.Cfg.prependOutput_inputPos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (pre : List Symbol) : (c.prependOutput pre).inputPos = c.inputPos

@[simp]

theorem Turing.Cfg.prependOutput_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (pre : List Symbol) : (c.prependOutput pre).state = c.state

@[simp]

theorem Turing.Cfg.prependOutput_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (pre : List Symbol) (a✝ : Fin k) (a✝¹ : ℤ) : (c.prependOutput pre).workTapes a✝ a✝¹ = c.workTapes a✝ a✝¹

@[simp]

theorem Turing.Cfg.prependOutput_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (pre : List Symbol) : (c.prependOutput pre).output = pre ++ c.output

@[simp]

theorem Turing.Cfg.prependOutput_workTapePos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (pre : List Symbol) (a✝ : Fin k) : (c.prependOutput pre).workTapePos a✝ = c.workTapePos a✝

def Turing.Cfg.withState {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) {State' : Type u_3} (q : Option State') : Cfg k Symbol State' input

The same configuration in a different control state, possibly of a different state type.

@[simp]

theorem Turing.Cfg.withState_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) {State' : Type u_3} (q : Option State') : (cfg.withState q).output = cfg.output

@[simp]

theorem Turing.Cfg.withState_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) {State' : Type u_3} (q : Option State') : (cfg.withState q).state = q

@[simp]

theorem Turing.Cfg.withState_workTapePos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) {State' : Type u_3} (q : Option State') (a✝ : Fin k) : (cfg.withState q).workTapePos a✝ = cfg.workTapePos a✝

@[simp]

theorem Turing.Cfg.withState_inputPos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) {State' : Type u_3} (q : Option State') : (cfg.withState q).inputPos = cfg.inputPos

@[simp]

theorem Turing.Cfg.withState_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) {State' : Type u_3} (q : Option State') (a✝ : Fin k) (a✝¹ : ℤ) : (cfg.withState q).workTapes a✝ a✝¹ = cfg.workTapes a✝ a✝¹

def Turing.Cfg.forgetState {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) : Cfg k Symbol Unit input

Forget the control state of a configuration, keeping the input head, the work tapes, the work-tape heads and the output. A property of this part of a configuration makes sense for every machine, whatever its state type.

@[simp]

theorem Turing.Cfg.forgetState_workTapePos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) (a✝ : Fin k) : cfg.forgetState.workTapePos a✝ = cfg.workTapePos a✝

@[simp]

theorem Turing.Cfg.forgetState_inputPos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) : cfg.forgetState.inputPos = cfg.inputPos

@[simp]

theorem Turing.Cfg.forgetState_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) (a✝ : Fin k) (a✝¹ : ℤ) : cfg.forgetState.workTapes a✝ a✝¹ = cfg.workTapes a✝ a✝¹

@[simp]

theorem Turing.Cfg.forgetState_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) : cfg.forgetState.output = cfg.output

@[simp]

theorem Turing.Cfg.forgetState_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) : cfg.forgetState.state = some ()

def Turing.Cfg.mapState {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {State' : Type u_3} (φ : Option State → Option State') (c : Cfg k Symbol State input) : Cfg k Symbol State' input

Remap the (optional) state of a configuration through φ, leaving the input head, the work tapes, the work-tape heads and the output alone. Control-flow combinators such as seq embed a sub-machine's configurations into the combined machine by exactly such a state remap.

@[simp]

theorem Turing.Cfg.mapState_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {State' : Type u_3} (φ : Option State → Option State') (c : Cfg k Symbol State input) (a✝ : Fin k) (a✝¹ : ℤ) : (mapState φ c).workTapes a✝ a✝¹ = c.workTapes a✝ a✝¹

@[simp]

theorem Turing.Cfg.mapState_workTapePos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {State' : Type u_3} (φ : Option State → Option State') (c : Cfg k Symbol State input) (a✝ : Fin k) : (mapState φ c).workTapePos a✝ = c.workTapePos a✝

@[simp]

theorem Turing.Cfg.mapState_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {State' : Type u_3} (φ : Option State → Option State') (c : Cfg k Symbol State input) : (mapState φ c).state = φ c.state

@[simp]

theorem Turing.Cfg.mapState_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {State' : Type u_3} (φ : Option State → Option State') (c : Cfg k Symbol State input) : (mapState φ c).output = c.output

@[simp]

theorem Turing.Cfg.mapState_inputPos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {State' : Type u_3} (φ : Option State → Option State') (c : Cfg k Symbol State input) : (mapState φ c).inputPos = c.inputPos

def Turing.Cfg.init {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (input : List Symbol) : Cfg k Symbol State input

The initial configuration for a starting state and an input string.

def Turing.Action.apply {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (action : Action k Symbol State) (cfg : Cfg k Symbol State input) : Cfg k Symbol State input

The effect of an action on a configuration: move the input head, write and move on the work tapes, append the emitted symbol to the output tape, and go to the successor state. This is the part of a step that does not depend on how the action was chosen.

@[simp]

theorem Turing.Action.apply_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (action : Action k Symbol State) (cfg : Cfg k Symbol State input) : (action.apply cfg).output = cfg.output ++ action.output.toList

@[simp]

theorem Turing.Action.apply_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (action : Action k Symbol State) (cfg : Cfg k Symbol State input) : (action.apply cfg).workTapes = fun (i : Fin k) => match (motive := Option (Option Symbol) → ℤ → Option Symbol) (action.workTapes i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s

@[simp]

theorem Turing.Action.apply_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (action : Action k Symbol State) (cfg : Cfg k Symbol State input) : (action.apply cfg).state = action.state

@[simp]

theorem Turing.Action.apply_inputPos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (action : Action k Symbol State) (cfg : Cfg k Symbol State input) : (action.apply cfg).inputPos = moveInputPos cfg.inputPos action.inputTape

@[simp]

theorem Turing.Action.apply_workTapePos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (action : Action k Symbol State) (cfg : Cfg k Symbol State input) : (action.apply cfg).workTapePos = fun (i : Fin k) => cfg.workTapePos i + ↑(action.workTapes i).2

theorem Turing.workTapePos_apply_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (action : Action k Symbol State) (cfg : Cfg k Symbol State input) (i : Fin k) : |(action.apply cfg).workTapePos i - cfg.workTapePos i| ≤ 1

A work tape head moves by at most one cell when an action is applied.