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.

Design

Nothing here mentions a machine. A step is described in two parts: an Action, recording which way the input head moves, what is written and where the work heads move, which symbol is emitted and which state follows; and Action.apply, which carries it out on a configuration.

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.

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

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✝³)

Equations

• Turing.instInhabitedCfg = { default := Turing.instInhabitedCfg.default }

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.

Equations

• Turing.moveInputPos pos m = if h : (↑↑pos + ↑m).toNat < n + 2 then ⟨(↑↑pos + ↑m).toNat, h⟩ else ⟨n + 1, ⋯⟩

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

Equations

• cfg.inputSymbol = if h₁ : cfg.inputPos = 0 then none else if h₂ : ↑cfg.inputPos = input.length + 1 then none else some input[↑cfg.inputPos - 1]

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.

Equations

• cfg.workTapeSymbols i = cfg.workTapes i (cfg.workTapePos 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.

Equations

• cfg.Halted = (cfg.state = none)

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

The same configuration with a different output tape.

Equations

• c.withOutput out = { state := c.state, inputPos := c.inputPos, workTapes := c.workTapes, workTapePos := c.workTapePos, output := out }

@[simp]

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

@[simp]

theorem Turing.Cfg.withOutput_inputPos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (out : List Symbol) : (c.withOutput out).inputPos = c.inputPos

@[simp]

theorem Turing.Cfg.withOutput_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (out : List Symbol) : (c.withOutput out).state = c.state

@[simp]

theorem Turing.Cfg.withOutput_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (out : List Symbol) : (c.withOutput out).output = out

@[simp]

theorem Turing.Cfg.withOutput_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (out : List Symbol) (a✝ : Fin k) (a✝¹ : ℤ) : (c.withOutput out).workTapes a✝ a✝¹ = c.workTapes a✝ 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.

Equations

• cfg.withState q = { state := q, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos, output := cfg.output }

@[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_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_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✝¹

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

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.

Equations

• Turing.Cfg.mapState φ c = { state := φ c.state, inputPos := c.inputPos, workTapes := c.workTapes, workTapePos := c.workTapePos, output := c.output }

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

@[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_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✝¹

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.

Equations

• Turing.Cfg.init q₀ input = { state := some q₀, inputPos := 1, workTapes := fun (x : Fin k) (x_1 : ℤ) => none, workTapePos := fun (x : Fin k) => 0, output := [] }

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.

Equations

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

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