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.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.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.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.run_succ' (d : Desc) (x : List ℕ) (j : ℕ) : run d x (j + 1) = (step d x (run d x j)).1

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

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.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.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) * (space (tm.initCfg x) t + 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.