The simulation is correct

A configuration of the simulation, together with the output so far, is a configuration of a machine over ℕ (Turing.MultiTapeTM.Universal.SCfg.toCfg), the zippers holding the symbols of the work tapes. If the description holds the transition of the machine for the current key, a step of the simulation is a step of the machine, and emits the same symbol (Turing.MultiTapeTM.Universal.toCfg_step).

A machine with finitely many states and symbols, renamed into ℕ by Turing.MultiTapeTM.map, has a description listing its transitions (Turing.MultiTapeTM.Universal.desc). Since runs commute with renaming, simulating the description yields the renamed output of the machine.

Main definitions

• Turing.MultiTapeTM.Universal.desc: the description of a machine.

Main results

• Turing.MultiTapeTM.Universal.simulate_desc: the simulation agrees with the machine.

def Turing.MultiTapeTM.Universal.key {k : ℕ} (q : ℕ) (inp : Option ℕ) (work : Fin k → Option ℕ) : Key

The key of the arguments of a transition.

def Turing.MultiTapeTM.Universal.Act.ofAction {k : ℕ} (a : Action k ℕ ℕ) : Act

An action, with the work tapes in a list.

def Turing.MultiTapeTM.Universal.Desc.Holds {k : ℕ} (d : Desc) (tm : MultiTapeTM k ℕ ℕ) (q : ℕ) (inp : Option ℕ) (work : Fin k → Option ℕ) : Prop

The description d holds the transition of tm for the key (q, inp, work).

Configurations of the simulation as configurations

def Turing.MultiTapeTM.Universal.Tape.cellAt (t : Tape) (z : ℤ) : Option ℕ

The symbol at position z.

theorem Turing.MultiTapeTM.Universal.Tape.read_eq (t : Tape) : t.read = t.cellAt t.head

The symbol under the head is the cell at the head position.

theorem Turing.MultiTapeTM.Universal.Tape.head_move (t : Tape) (m : SignType) : (t.move m).head = t.head + ↑m

Moving a tape moves its head by the direction.

def Turing.MultiTapeTM.Universal.Tape.blank : Tape

The empty work tape, for missing work tapes.

def Turing.MultiTapeTM.Universal.SCfg.toCfg (k : ℕ) (x : List ℕ) (s : SCfg) (out : List ℕ) : Cfg k ℕ ℕ x

The configuration of a machine with k work tapes on the input x that s represents, with the output out: the work tapes hold the symbols of the zippers. Missing work tapes are blank and an input head beyond the input is clamped; on well-shaped configurations neither happens.

structure Turing.MultiTapeTM.Universal.SCfg.WellShaped (k : ℕ) (x : List ℕ) (s : SCfg) : Prop

s has k work tapes and its input head on the input x or its boundaries.

• length_workTapes : s.workTapes.length = k
• inputPos_le : s.inputPos ≤ x.length + 1

theorem Turing.MultiTapeTM.Universal.key_toCfg {k : ℕ} {x : List ℕ} {s : SCfg} (hs : SCfg.WellShaped k x s) (out : List ℕ) (q : ℕ) : s.key x q = key q (SCfg.toCfg k x s out).inputSymbol (SCfg.toCfg k x s out).workTapeSymbols

The key of a well-shaped configuration of the simulation is the key of the configuration it represents.

theorem Turing.MultiTapeTM.Universal.toCfg_step {k : ℕ} {x : List ℕ} {tm : MultiTapeTM k ℕ ℕ} {d : Desc} {s : SCfg} {out : List ℕ} (hs : SCfg.WellShaped k x s) (hd : ∀ (q : ℕ), (SCfg.toCfg k x s out).state = some q → d.Holds tm q (SCfg.toCfg k x s out).inputSymbol (SCfg.toCfg k x s out).workTapeSymbols) : SCfg.toCfg k x (step d x s).1 (out ++ (step d x s).2.toList) = MultiTapeTM.step (SCfg.toCfg k x s out) ∧ SCfg.WellShaped k x (step d x s).1

A step of the simulation is a step of the machine, emitting the same symbol, if the description holds the transition for the current key.

theorem Turing.MultiTapeTM.Universal.toCfg_apply {k : ℕ} {x : List ℕ} {s : SCfg} {q : ℕ} (hs : SCfg.WellShaped k x s) (hq : s.state = some q) (out : List ℕ) (a : Action k ℕ ℕ) : SCfg.toCfg k x ((Act.ofAction a).apply x s) (out ++ a.output.toList) = a.apply (SCfg.toCfg k x s out) ∧ SCfg.WellShaped k x ((Act.ofAction a).apply x s)

An action applied to a running configuration of the simulation is the action applied to the configuration it represents, and the symbol it emits is appended to the output.

theorem Turing.MultiTapeTM.Universal.toCfg_init {k : ℕ} {x : List ℕ} {d : Desc} (hk : d.tapes = k) : SCfg.toCfg k x (init d) [] = Cfg.init d.q₀ x ∧ SCfg.WellShaped k x (init d)

The initial configuration of the simulation is the initial configuration.

Descriptions of machines

noncomputable def Turing.MultiTapeTM.Universal.desc {k : ℕ} {Symbol State : Type} [Fintype State] [Fintype Symbol] (eS : State ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol State) : Desc

The description of a machine with finitely many states and symbols, renamed into ℕ by eS and eY: a transition for every state and every choice of read symbols.

theorem Turing.MultiTapeTM.Universal.key_injective {k : ℕ} {Symbol State : Type} (eS : State ↪ ℕ) (eY : Symbol ↪ ℕ) : Function.Injective fun (e : State × Option Symbol × (Fin k → Option Symbol)) => key (eS e.1) (Option.map (⇑eY) e.2.1) (Option.map ⇑eY ∘ e.2.2)

Renamed keys determine the state and the read symbols.

theorem Turing.MultiTapeTM.Universal.toCfg_iterate {k : ℕ} {Symbol State : Type} [Fintype State] [Fintype Symbol] (eS : State ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol State) (x : List Symbol) (t : ℕ) : Cfg.map eS eY (runFrom (tm.initCfg x) t) = SCfg.toCfg k (List.map (⇑eY) x) ((stepOut (desc eS eY tm) (List.map (⇑eY) x))^[t] (init (desc eS eY tm), [])).1 ((stepOut (desc eS eY tm) (List.map (⇑eY) x))^[t] (init (desc eS eY tm), [])).2 ∧ SCfg.WellShaped k (List.map (⇑eY) x) ((stepOut (desc eS eY tm) (List.map (⇑eY) x))^[t] (init (desc eS eY tm), [])).1

The run of the simulation of the description of tm, read as configurations, is the renamed run of tm.

theorem Turing.MultiTapeTM.Universal.simulate_desc {k : ℕ} {Symbol State : Type} [Fintype State] [Fintype Symbol] (eS : State ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol State) (x : List Symbol) (t : ℕ) : simulate (desc eS eY tm) (List.map (⇑eY) x) t = (List.map (⇑eY) (runFrom (tm.initCfg x) t).output, (runFrom (tm.initCfg x) t).state.isNone)

The simulation is correct: simulating the description of tm on the renamed input for t steps yields the renamed output of tm after t steps, and whether tm has halted.