Simulating multi-tape machines on numbers

The universal machine simulates a multi-tape Turing machine over the states and symbols ℕ from a description (Turing.MultiTapeTM.Universal.Desc): the number of work tapes, the initial state and a transition table. A transition maps a key (Turing.MultiTapeTM.Universal.Key) — the state and the symbols under the heads, as the arguments of Turing.MultiTapeTM.tr — to an action (Turing.MultiTapeTM.Universal.Act), which mirrors Turing.Action with the work tapes in a list. A missing transition halts the machine.

The configurations (Turing.MultiTapeTM.Universal.SCfg) mirror Turing.Cfg without the output: a step returns the symbol it emits, if any, and it is up to the caller to collect, use or discard it. A work tape (Turing.MultiTapeTM.Universal.Tape) is a zipper: the position of its head, the cells left of the head, nearest first, and the cells from the head on. It holds no more cells than the head has visited, so a configuration takes space linear in the space of the simulated machine. The input head is a number, encoded in binary by the universal machine.

Main definitions

• Turing.MultiTapeTM.Universal.Desc: descriptions of machines.
• Turing.MultiTapeTM.Universal.SCfg: configurations of the simulation.
• Turing.MultiTapeTM.Universal.step: one step of the simulation, and the symbol it emits.
• Turing.MultiTapeTM.Universal.simulate: the output after a number of steps, and whether the machine has halted.

structure Turing.MultiTapeTM.Universal.Key : Type

The key of a transition: the state and the symbols under the input head and the work-tape heads.

• state : ℕ

  The state.

• input : Option ℕ

  The symbol under the input head.

• work : List (Option ℕ)

  The symbols under the work-tape heads.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instDecidableEqKey : DecidableEq Key

def Turing.MultiTapeTM.Universal.instDecidableEqKey.decEq (x✝ x✝¹ : Key) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instInhabitedKey : Inhabited Key

structure Turing.MultiTapeTM.Universal.Act : Type

An action, as Turing.Action with the work tapes in a list.

• inputTape : SignType

  The move of the input head.

• workTapes : List (Option (Option ℕ) × SignType)

  What to write on each work tape, if anything, and how to move its head.

• output : Option ℕ

  The symbol to emit, if any.

• state : Option ℕ

  The next state, or none to halt.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instInhabitedAct : Inhabited Act

structure Turing.MultiTapeTM.Universal.Desc : Type

A description of a machine: the number of work tapes, the initial state and the transitions.

• tapes : ℕ

  The number of work tapes.

• q₀ : ℕ

  The initial state.

• table : List (Key × Act)

  The transitions.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instInhabitedDesc : Inhabited Desc

structure Turing.MultiTapeTM.Universal.Tape : Type

A simulated work tape, as a zipper.

• head : ℤ

  The position of the head.

• left : List (Option ℕ)

  The cells left of the head, nearest first.

• right : List (Option ℕ)

  The cells from the head on.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instInhabitedTape : Inhabited Tape

structure Turing.MultiTapeTM.Universal.SCfg : Type

A configuration of the simulation, as Turing.Cfg with the work tapes in a list and without the output.

• state : Option ℕ

  The state, or none once halted.

• inputPos : ℕ

  The position of the input head.

• workTapes : List Tape

  The work tapes.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instInhabitedSCfg : Inhabited SCfg

def Turing.MultiTapeTM.Universal.Tape.read (t : Tape) : Option ℕ

The symbol under the head.

def Turing.MultiTapeTM.Universal.Tape.write (t : Tape) (o : Option ℕ) : Tape

Writes o under the head.

def Turing.MultiTapeTM.Universal.Tape.move (t : Tape) : SignType → Tape

Moves the head by m.

def Turing.MultiTapeTM.Universal.Tape.apply (t : Tape) (a : Option (Option ℕ) × SignType) : Tape

Applies the action on a work tape: write, then move.

def Turing.MultiTapeTM.Universal.inputSymbol (x : List ℕ) (p : ℕ) : Option ℕ

The symbol at position p of the input x, with blanks at position 0 and after the input.

def Turing.MultiTapeTM.Universal.moveInput (p : ℕ) (a : Option ℕ) : SignType → ℕ

Moves the input head at position p, reading a, by m: right moves stop at the blank after the input, which is the only blank right of position 0.

theorem Turing.MultiTapeTM.Universal.isSome_inputSymbol (x : List ℕ) (p : ℕ) : (inputSymbol x p).isSome = true ↔ 0 < p ∧ p ≤ x.length

theorem Turing.MultiTapeTM.Universal.moveInput_le {x : List ℕ} {p : ℕ} (h : p ≤ x.length + 1) (m : SignType) : moveInput p (inputSymbol x p) m ≤ x.length + 1

def Turing.MultiTapeTM.Universal.applyTapes : List Tape → List (Option (Option ℕ) × SignType) → List Tape

Applies the actions to the work tapes, in order; a tape without an action is unchanged.

def Turing.MultiTapeTM.Universal.Act.apply (a : Act) (x : List ℕ) (c : SCfg) : SCfg

The effect of an action on a configuration on the input x, as Turing.Action.apply, without the output.

def Turing.MultiTapeTM.Universal.SCfg.key (c : SCfg) (x : List ℕ) (q : ℕ) : Key

The key of the transition to take in c, on the input x, in the state q.

def Turing.MultiTapeTM.Universal.stepWith (d : Desc) (c : SCfg) (a : Option ℕ) : SCfg × Option ℕ

One step of the machine described by d with the input head reading a, and the symbol it emits: the step without the input.

def Turing.MultiTapeTM.Universal.step (d : Desc) (x : List ℕ) (c : SCfg) : SCfg × Option ℕ

One step of the machine described by d on the input x, and the symbol it emits.

theorem Turing.MultiTapeTM.Universal.step_eq_stepWith (d : Desc) (x : List ℕ) (c : SCfg) : step d x c = stepWith d c (inputSymbol x c.inputPos)

A step reads the input only at the input head.

def Turing.MultiTapeTM.Universal.init (d : Desc) : SCfg

The initial configuration: the initial state, the input head on the first symbol and blank work tapes.

def Turing.MultiTapeTM.Universal.stepOut (d : Desc) (x : List ℕ) (c : SCfg × List ℕ) : SCfg × List ℕ

A step that collects the emitted symbol.

def Turing.MultiTapeTM.Universal.simulate (d : Desc) (x : List ℕ) (t : ℕ) : List ℕ × Bool

The output of the machine described by d on the input x after t steps, and whether it has halted by then.