The universal machine, reading its input in place

The universal function (Turing.MultiTapeTM.Universal.universal) is computed by a multi-pass fold over its input, one pass per step of the simulation. The state of the fold holds the description, the configuration and the number of steps left, but never the input x of the simulated machine: a pass reads the symbol under the simulated input head by counting down the symbols of x on the input tape. A finite-state translator (Turing.MultiTapeTM.Universal.inTr) turns the encoded input into events, one per unary digit and one per end of a symbol of x, so that the fold is a plain function on events.

Main definitions

• Turing.MultiTapeTM.Universal.inTr: the events of the encoded input.
• Turing.MultiTapeTM.Universal.scan: the countdown to the symbol under the input head.
• Turing.MultiTapeTM.Universal.stateSpace: a bound on the states of the fold.

Main results

• Turing.MultiTapeTM.Universal.events_eIn: the events of the encoded input.
• Turing.MultiTapeTM.Universal.inputSymbol_scan: the countdown finds the symbol under the input head.
• Turing.MultiTapeTM.Universal.computableTidilyInTimeAndSpace_universal_inPlace: the universal function is tidily computable in space linear in stateSpace.
• Turing.MultiTapeTM.Universal.stateSpace_desc: on descriptions of machines, stateSpace is linear in the description times the space of the machine, plus logarithms of the length of the input and of the number of steps, plus the largest symbol of the input.

def Turing.MultiTapeTM.doubled (w : List Bool) : List Bool

The bits of w, each after a marker true: frame w is doubled w followed by false.

@[simp]

theorem Turing.MultiTapeTM.doubled_nil : doubled [] = []

@[simp]

theorem Turing.MultiTapeTM.doubled_cons (b : Bool) (w : List Bool) : doubled (b :: w) = true :: b :: doubled w

@[simp]

theorem Turing.MultiTapeTM.doubled_append (u v : List Bool) : doubled (u ++ v) = doubled u ++ doubled v

theorem Turing.MultiTapeTM.frame_eq_doubled (w : List Bool) : frame w = doubled w ++ [false]

theorem Turing.MultiTapeTM.ComputableTidilyInO.of_transducer {Q : Type} [Finite Q] (τ : Transducer Bool Q) {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (hf : ∀ (a : α), encOut (f a) = τ.run τ.q₀ (encIn a)) : ComputableTidilyInO f encIn encOut (fun (a : α) => (encIn a).length) fun (a : α) => (encOut (f a)).length

A function computed by a transducer is computed in the space of its output.

The events of the input

inductive Turing.MultiTapeTM.Universal.InState : Type

The states of the translator: in the framed description, at a marker or a bit; in the framed input x, at a marker or a bit of the outer frame, before an inner marker or digit; after the input, in the number of steps.

• descMarker : InState
• descBit : InState
• marker : InState
• bit : InState
• digitMarker : InState
• digit : InState
• steps : InState

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instDecidableEqInState : DecidableEq InState

instance Turing.MultiTapeTM.Universal.instFiniteInState : Finite InState

def Turing.MultiTapeTM.Universal.inTr : Translator InState Bool

The translator of the encoded input into events: true for each unary digit of a symbol of x and false at the end of each symbol.

def Turing.MultiTapeTM.Universal.tok (n : ℕ) : List Bool

The events of a symbol: its unary digits, then the end.

theorem Turing.MultiTapeTM.Universal.inTr_run_frame (w v : List Bool) : inTr.run InState.descMarker (frame w ++ v) = inTr.run InState.marker v

The translator skips a framed word at the start of the input.

theorem Turing.MultiTapeTM.Universal.inTr_run_steps (v : List Bool) : inTr.run InState.steps v = (InState.steps, [])

After the framed list of symbols, the translator emits nothing.

theorem Turing.MultiTapeTM.Universal.inTr_run_symbol (n : ℕ) (v : List Bool) : inTr.run InState.marker (doubled (frame (List.replicate n true)) ++ v) = ((inTr.run InState.marker v).1, tok n ++ (inTr.run InState.marker v).2)

The translator turns a symbol of the framed list into its events.

theorem Turing.MultiTapeTM.Universal.inTr_events_frame (w : List Bool) (x : List ℕ) (v : List Bool) : inTr.events (frame w ++ (frame ((encList encUnary) x) ++ v)) = (List.map tok x).flatten

The events of an input made of a framed word, a framed list of symbols x and anything else are the events of the symbols of x.

theorem Turing.MultiTapeTM.Universal.events_eIn (d : Desc) (x : List ℕ) (t : ℕ) : inTr.events (eIn (d, x, t)) = (List.map tok x).flatten

The events of the encoded input are the events of the symbols of x.

The countdown

def Turing.MultiTapeTM.Universal.scan (p : ℕ × ℕ) (b : Bool) : ℕ × ℕ

A round of the countdown: a digit counts towards the symbol read while the countdown is at 1, and the end of a symbol counts down.

theorem Turing.MultiTapeTM.Universal.foldl_scan_replicate (k cur j : ℕ) : List.foldl scan (k, cur) (List.replicate j true) = (k, if k = 1 then cur + j else cur)

Along unary digits, the countdown stays and the symbol read grows while it is at 1.

theorem Turing.MultiTapeTM.Universal.scan_tok (k cur n : ℕ) : List.foldl scan (k, cur) (tok n) = (k - 1, if k = 1 then cur + n else cur)

theorem Turing.MultiTapeTM.Universal.scan_zero (l : List Bool) (cur : ℕ) : List.foldl scan (0, cur) l = (0, cur)

A finished countdown stays finished.

theorem Turing.MultiTapeTM.Universal.inputSymbol_scan (x : List ℕ) (p : ℕ) : inputSymbol x p = if p = 0 ∨ (List.foldl scan (p, 0) (List.map tok x).flatten).1 ≠ 0 then none else some (List.foldl scan (p, 0) (List.map tok x).flatten).2

The countdown finds the symbol under the input head.

The fold

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.St : Type

The state of the fold: the description and the configuration, then the number of steps left, the countdown and the symbol read so far.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eSt : St ↪ List Bool

The encoding of states of the fold, with the number of steps left and the countdown in binary.

def Turing.MultiTapeTM.Universal.foldInit (i : Desc × List ℕ × ℕ) : St

The initial state: the initial configuration, all steps left, and the countdown at the input head.

def Turing.MultiTapeTM.Universal.foldNext (p : St × Bool) : St

A round: one event of the countdown.

def Turing.MultiTapeTM.Universal.symAt (s : St) : Option ℕ

The symbol under the input head, at the end of a pass.

def Turing.MultiTapeTM.Universal.stepAt (s : St) : SCfg × Option ℕ

The step at the end of a pass, if any steps are left, and the symbol it emits.

def Turing.MultiTapeTM.Universal.foldEnd (s : St) : St

The end of a pass: the step, and the countdown reset to the new input head.

def Turing.MultiTapeTM.Universal.foldEmit (s : St) : List Bool

The emitted symbol, as its part of the encoded output.

def Turing.MultiTapeTM.Universal.foldCont (s : St) : Bool

Whether another pass follows.

def Turing.MultiTapeTM.Universal.foldFinish (s : St) : Bool

Whether the simulated machine has halted.

def Turing.MultiTapeTM.Universal.eHalted : Bool ↪ List Bool

The end of the encoded output: the end of the frame of the output, then whether the machine has halted.

def Turing.MultiTapeTM.Universal.events (x : List ℕ) : List Bool

The events of the input x.

theorem Turing.MultiTapeTM.Universal.stepAt_scan (d : Desc) (x : List ℕ) (c : SCfg) (r : ℕ) : stepAt ((d, c), r, List.foldl scan (c.inputPos, 0) (events x)) = if r = 0 then (c, none) else step d x c

The end of pass i, after the countdown over the input.

theorem Turing.MultiTapeTM.Universal.passState_fold (d : Desc) (x : List ℕ) (t i : ℕ) : passState (foldInit (d, x, t)) foldNext foldEnd (events x) i = ((d, run d x (min i t)), t - i, (run d x (min i t)).inputPos, 0)

The passes follow the steps of the simulation, as long as steps are left.

theorem Turing.MultiTapeTM.Universal.simulate_eq (d : Desc) (x : List ℕ) (t : ℕ) : simulate d x t = ((List.map (fun (i : ℕ) => (step d x (run d x i)).2.toList) (List.range t)).flatten, (run d x t).state.isNone)

theorem Turing.MultiTapeTM.Universal.eOut_universal (d : Desc) (x : List ℕ) (t : ℕ) : eOut (universal (d, x, t)) = (List.map (fun (i : ℕ) => encBits (foldEmit (streamState (passState (foldInit (d, x, t)) foldNext foldEnd (events x) i) foldNext (events x) (events x).length))) (List.range (t - 1 + 1))).flatten ++ eHalted (foldFinish (passState (foldInit (d, x, t)) foldNext foldEnd (events x) (t - 1 + 1)))

The encoded output: the symbols emitted by the passes, then whether the machine has halted.

The parts of the fold, within bounds in the length of the state

theorem Turing.MultiTapeTM.Universal.foldNext_inO : ComputableTidilyInO foldNext (encPair eSt encBool) eSt (fun (p : St × Bool) => (((encPair eSt encBool) p).length + 1) ^ 2) fun (p : St × Bool) => ((encPair eSt encBool) p).length + 1

A round of the countdown.

theorem Turing.MultiTapeTM.Universal.stepAt_inO : ComputableTidilyInO stepAt eSt (encPair eCfg eSym) (fun (s : St) => ((eSt s).length + 1) ^ 3) fun (s : St) => (eSt s).length + 1

The step at the end of a pass.

theorem Turing.MultiTapeTM.Universal.foldEnd_inO : ComputableTidilyInO foldEnd eSt eSt (fun (s : St) => ((eSt s).length + 1) ^ 3) fun (s : St) => (eSt s).length + 1

The end of a pass.

theorem Turing.MultiTapeTM.Universal.foldEmit_inO : ComputableTidilyInO foldEmit eSt encBits (fun (s : St) => ((eSt s).length + 1) ^ 3) fun (s : St) => (eSt s).length + 1

What a pass emits.

theorem Turing.MultiTapeTM.Universal.foldCont_inO : ComputableTidilyInO foldCont eSt encBool (fun (s : St) => ((eSt s).length + 1) ^ 3) fun (s : St) => (eSt s).length + 1

Whether another pass follows.

theorem Turing.MultiTapeTM.Universal.foldFinish_inO : ComputableTidilyInO foldFinish eSt eHalted (fun (s : St) => ((eSt s).length + 1) ^ 3) fun (s : St) => (eSt s).length + 1

Whether the simulated machine has halted.

The initial state, without the input

inductive Turing.MultiTapeTM.Universal.ExState : Type

The states of the extracting transducer: in the framed description, at a marker or a bit; in the framed input, at a marker or a bit; in the number of steps.

• descMarker : ExState
• descBit : ExState
• marker : ExState
• bit : ExState
• steps : ExState

instance Turing.MultiTapeTM.Universal.instFiniteExState : Finite ExState

def Turing.MultiTapeTM.Universal.extractT : Transducer Bool ExState

Copies the framed description, drops the framed input and copies the rest, the number of steps (Turing.MultiTapeTM.Universal.extractT_run_frame).

theorem Turing.MultiTapeTM.Universal.extractT_run_frame (w u v : List Bool) : extractT.run extractT.q₀ (frame w ++ (frame u ++ v)) = frame w ++ v

The extracting transducer copies a framed word and drops the framed word after it.

theorem Turing.MultiTapeTM.Universal.foldInit_inO : ComputableTidilyInO foldInit eIn eSt (fun (i : Desc × List ℕ × ℕ) => (eIn i).length + (((encPair eDesc encNat) (i.1, i.2.2)).length + 1) ^ 2) fun (i : Desc × List ℕ × ℕ) => ((encPair eDesc encNat) (i.1, i.2.2)).length + 1

The initial state, in the space of the description and the number of steps.

The size of the state

theorem Turing.MultiTapeTM.Universal.scan_take_tok (n k cur j : ℕ) : (List.foldl scan (k, cur) (List.take j (tok n))).1 ≤ k ∧ (List.foldl scan (k, cur) (List.take j (tok n))).2 ≤ cur + n ∧ ((List.foldl scan (k, cur) (List.take j (tok n))).2 = cur ∨ k = 1)

Along the events of a symbol, the countdown does not go up and the symbol read grows by at most the symbol.

theorem Turing.MultiTapeTM.Universal.scan_take (x : List ℕ) (k cur j : ℕ) : (List.foldl scan (k, cur) (List.take j (events x))).1 ≤ k ∧ (List.foldl scan (k, cur) (List.take j (events x))).2 ≤ cur + List.foldr max 0 x

Along the events of the input, the countdown does not go up and the symbol read stays within the largest symbol.

theorem Turing.MultiTapeTM.Universal.simSpace_mono (d : Desc) (x : List ℕ) {j j' : ℕ} (h : j ≤ j') : simSpace d x j ≤ simSpace d x j'

def Turing.MultiTapeTM.Universal.cfgSpace (d : Desc) (x : List ℕ) (t : ℕ) : ℕ

A bound on the configurations of the simulation within t steps, from Turing.MultiTapeTM.Universal.length_eCfg_le_space.

def Turing.MultiTapeTM.Universal.stateSpace (d : Desc) (x : List ℕ) (t : ℕ) : ℕ

A bound on the states of the fold: the description, a configuration, the number of steps and the position of the input head in binary, and the largest symbol of the input.

theorem Turing.MultiTapeTM.Universal.length_eSt_le (d : Desc) (x : List ℕ) (t i j : ℕ) : (eSt (streamState (passState (foldInit (d, x, t)) foldNext foldEnd (events x) i) foldNext (events x) j)).length ≤ stateSpace d x t

The size of the states of the fold.

The universal machine

theorem Turing.MultiTapeTM.Universal.final_time (c N t L P E : ℕ) (hP : P ≤ L) (hE : E ≤ L) : c * (N + (P + 1) ^ 2 + (E + 1) ^ 3 + (t - 1 + 1) * (N + (N + 1) * (9 * (L + 1) ^ 3 + L + 1))) ≤ 20 * c * ((t + 1) * (N + 1) ^ 2 * (L + 1) ^ 3)

The time of the universal machine, simplified.

theorem Turing.MultiTapeTM.Universal.computableTidilyInTimeAndSpace_universal_inPlace : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace universal eIn eOut (fun (i : Desc × List ℕ × ℕ) => c * ((i.2.2 + 1) * ((eIn i).length + 1) ^ 2 * (stateSpace i.1 i.2.1 i.2.2 + 1) ^ 3)) fun (i : Desc × List ℕ × ℕ) => c * (stateSpace i.1 i.2.1 i.2.2 + 1)

The universal machine, reading its input in place. The universal function is tidily computable in space linear in a bound on the states of the simulation (stateSpace): the description, a configuration, the number of steps and the position of the input head in binary, and the largest symbol of the input. It never copies the input. Each step reads the whole input.

theorem Turing.MultiTapeTM.Universal.stateSpace_le (d : Desc) (x : List ℕ) (t : ℕ) : stateSpace d x t ≤ 60 * (descLen d + 1) * (simSpace d x t + 1) + 6 * (encNat (x.length + 1)).length + 2 * (encNat t).length + List.foldr max 0 x

The bound on the states, in the description, the cells visited by the simulation, the lengths of the input and the number of steps in binary, and the largest symbol of the input.

theorem Turing.MultiTapeTM.Universal.stateSpace_desc {k : ℕ} {Symbol S : Type} [Fintype S] [Fintype Symbol] (eS : S ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol S) (x : List Symbol) (t : ℕ) : stateSpace (desc eS eY tm) (List.map (⇑eY) x) t ≤ 60 * (descLen (desc eS eY tm) + 1) * ((MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg x) t).space + 1) + 6 * (encNat (x.length + 1)).length + 2 * (encNat t).length + List.foldr max 0 (List.map (⇑eY) x)

The space of the universal machine on the description of a machine: linear in the description times the space of the machine, plus the logarithms of the length of the input and of the number of steps, plus the largest symbol of the input.