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
• tapeOfList, wordsCfg: tapes and configurations holding given words

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 of a machine without work tapes are equal if their states, input head positions and outputs are equal.

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.

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]

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

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. This is the shape of embedding used to place a sub-machine's configurations into a larger machine built from it.

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

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.tapeOfList {Symbol : Type u_2} (xs : List Symbol) : ℤ → Option Symbol

A tape containing exactly the symbols of xs at positions 0, ..., xs.length - 1.

Equations

• Turing.tapeOfList xs (Int.ofNat n) = xs[n]?
• Turing.tapeOfList xs (Int.negSucc a) = none

@[simp]

theorem Turing.tapeOfList_ofNat {Symbol : Type u_2} (xs : List Symbol) (n : ℕ) : tapeOfList xs ↑n = xs[n]?

@[simp]

theorem Turing.tapeOfList_negSucc {Symbol : Type u_2} (xs : List Symbol) (n : ℕ) : tapeOfList xs (Int.negSucc n) = none

theorem Turing.tapeOfList_append_single {Symbol : Type u_2} (xs : List Symbol) (x : Symbol) : tapeOfList (xs ++ [x]) = Function.update (tapeOfList xs) (↑xs.length) (some x)

Appending one symbol writes precisely the cell after the existing word.

@[simp]

theorem Turing.tapeOfList_nil {Symbol : Type u_2} : tapeOfList [] = fun (x : ℤ) => none

The blank tape holds the empty word.

theorem Turing.tapeOfList_zero {Symbol : Type u_2} (xs : List Symbol) : tapeOfList xs 0 = xs.head?

The cell at position 0 holds the first symbol of the word.

def Turing.wordsCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : Cfg k Symbol State input

The configuration whose work tape i holds exactly the word ws i with its head at the start, whose input head is at the start of the input, in state q with output out.

Equations

• Turing.wordsCfg input q ws out = { state := q, inputPos := 1, workTapes := fun (i : Fin k) => Turing.tapeOfList (ws i), workTapePos := fun (x : Fin k) => 0, output := out }

@[simp]

theorem Turing.wordsCfg_inputPos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).inputPos = 1

@[simp]

theorem Turing.wordsCfg_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).output = out

@[simp]

theorem Turing.wordsCfg_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).state = q

@[simp]

theorem Turing.wordsCfg_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (i : Fin k) (a✝ : ℤ) : (wordsCfg input q ws out).workTapes i a✝ = tapeOfList (ws i) a✝

@[simp]

theorem Turing.wordsCfg_workTapePos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (x✝ : Fin k) : (wordsCfg input q ws out).workTapePos x✝ = 0

@[simp]

theorem Turing.mapState_wordsCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (φ : Option State → Option State') (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : Cfg.mapState φ (wordsCfg input q ws out) = wordsCfg input (φ q) ws out

Remapping the state of a wordsCfg remaps its state and leaves the words alone.

theorem Turing.Cfg.init_eq_wordsCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (input : List Symbol) : init q₀ input = wordsCfg input (some q₀) (fun (x : Fin k) => []) []

The initial configuration is the word configuration with blank tapes and no 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.

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.