The cost of a step of the simulation

States, symbols and moves are encoded in unary (Turing.MultiTapeTM.encUnary), head positions on the work tapes as integers (Turing.MultiTapeTM.encInt), the position of the input head in binary (Turing.MultiTapeTM.encNat), and a structure as the framed tuple of its fields.

Reading, writing and moving on a zipper are tidily computable in linear time and space. A step of the simulation (Turing.MultiTapeTM.Universal.step_inO) takes space linear in the length L of the encoded context (the description, the input and the configuration), and time (K + E + p + 1) * (L + 1) ^ 2 for K work tapes, E transitions and the input head at p: reading and changing a work tape is linear, comparing the key with a transition is quadratic, and finding the input symbol counts down from p.

Main definitions

• Turing.MultiTapeTM.Universal.eDesc, .eCfg: the encodings of descriptions and configurations.
• Turing.MultiTapeTM.Universal.stepTime: the time bound of a step.

Main results

• Turing.MultiTapeTM.Universal.step_inO: a step is tidily computable within the time stepTime and linear space.

Encodings

def Turing.MultiTapeTM.Universal.encSign : SignType ↪ List Bool

Moves, by their sign.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eSym : Option ℕ ↪ List Bool

Symbols and blanks.

def Turing.MultiTapeTM.Universal.eKey : Key ↪ List Bool

Keys of transitions, as their fields.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.TapeAct : Type

An action on a work tape.

def Turing.MultiTapeTM.Universal.encUnit : Unit ↪ List Bool

The unit type, encoded by the empty word.

@[simp]

theorem Turing.MultiTapeTM.Universal.encUnit_apply (u : Unit) : encUnit u = []

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eTA : Option (Option ℕ) × SignType ↪ List Bool

Actions on a work tape.

def Turing.MultiTapeTM.Universal.eAct : Act ↪ List Bool

Actions, as their fields.

def Turing.MultiTapeTM.Universal.eDesc : Desc ↪ List Bool

Descriptions, as their fields.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eTapeFields : ℤ × List (Option ℕ) × List (Option ℕ) ↪ List Bool

The fields of a work tape.

def Turing.MultiTapeTM.Universal.eTape : Tape ↪ List Bool

Work tapes, as their fields.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eCfgFields : Option ℕ × ℕ × List Tape ↪ List Bool

The fields of a configuration.

def Turing.MultiTapeTM.Universal.eCfg : SCfg ↪ List Bool

Configurations, as their fields.

@[simp]

theorem Turing.MultiTapeTM.Universal.eKey_apply (k : Key) : eKey k = (encPair encUnary (encPair eSym (encList eSym))) (k.state, k.input, k.work)

@[simp]

theorem Turing.MultiTapeTM.Universal.eAct_apply (a : Act) : eAct a = (encPair encSign (encPair (encList eTA) (encPair eSym eSym))) (a.inputTape, a.workTapes, a.output, a.state)

@[simp]

theorem Turing.MultiTapeTM.Universal.eDesc_apply (d : Desc) : eDesc d = (encPair encUnary (encPair encUnary (encList (encPair eKey eAct)))) (d.tapes, d.q₀, d.table)

@[simp]

theorem Turing.MultiTapeTM.Universal.eTape_apply (t : Tape) : eTape t = eTapeFields (t.head, t.left, t.right)

@[simp]

theorem Turing.MultiTapeTM.Universal.eCfg_apply (c : SCfg) : eCfg c = eCfgFields (c.state, c.inputPos, c.workTapes)

theorem Turing.MultiTapeTM.Universal.state_inO : ComputableTidilyInO SCfg.state eCfg eSym (fun (c : SCfg) => (eCfg c).length) fun (c : SCfg) => (eCfg c).length

The state of a configuration, in linear time.

Reading, writing and moving on a work tape, in linear time

Applying actions to all work tapes

def Turing.MultiTapeTM.Universal.applyStep (s : List TapeAct × List Tape) (t : Tape) : List TapeAct × List Tape

One step of applying actions to the work tapes in order: the remaining actions, and the tapes done so far.

Sizes

All work tapes

theorem Turing.MultiTapeTM.Universal.applyTapes_inO : ComputableTidilyInO (fun (p : List Tape × List TapeAct) => applyTapes p.1 p.2) (encPair (encList eTape) (encList eTA)) (encList eTape) (fun (p : List Tape × List TapeAct) => (p.1.length + 1) * (((encPair (encList eTape) (encList eTA)) p).length + 1)) fun (p : List Tape × List TapeAct) => ((encPair (encList eTape) (encList eTA)) p).length

Applying actions to the work tapes, within time the number of work tapes times the length of the arguments, and linear space.

theorem Turing.MultiTapeTM.Universal.reads_inO : ComputableTidilyInO (fun (ts : List Tape) => List.map Tape.read ts) (encList eTape) (encList eSym) (fun (ts : List Tape) => (ts.length + 1) * (((encList eTape) ts).length + 1)) fun (ts : List Tape) => ((encList eTape) ts).length

The symbols under the heads of the work tapes, within time the number of work tapes times their length, and linear space.

The input head

theorem Turing.MultiTapeTM.Universal.inputSymbol_inO : ComputableTidilyInO (fun (q : List ℕ × ℕ) => inputSymbol q.1 q.2) (encPair (encList encUnary) encNat) eSym (fun (q : List ℕ × ℕ) => (q.2 + 1) * (((encPair (encList encUnary) encNat) q).length + 1) ^ 2) fun (q : List ℕ × ℕ) => ((encPair (encList encUnary) encNat) q).length

The symbol at a position of the input, given in binary, within time the position times the square of the length of the arguments, and linear space.

theorem Turing.MultiTapeTM.Universal.moveInput_inO : ComputableTidilyInO (fun (q : ℕ × Option ℕ × SignType) => moveInput q.1 q.2.1 q.2.2) (encPair encNat (encPair eSym encSign)) encNat (fun (q : ℕ × Option ℕ × SignType) => (((encPair encNat (encPair eSym encSign)) q).length + 1) ^ 2) fun (q : ℕ × Option ℕ × SignType) => ((encPair encNat (encPair eSym encSign)) q).length + 1

Moving the input head, given in binary.

A step without the input

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.WCtx : Type

The context of a step without the input: the description, the configuration and the symbol under the input head.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eWCtx : WCtx ↪ List Bool

The encoding of contexts without the input.

def Turing.MultiTapeTM.Universal.wKey (c : WCtx) : Key

The key of the transition to take.

def Turing.MultiTapeTM.Universal.wFound (c : WCtx) : Option (Key × Act)

The transition to take, if any.

def Turing.MultiTapeTM.Universal.defaultEntry : Key × Act

The default transition, never taken.

def Turing.MultiTapeTM.Universal.wAct (c : WCtx) : Act

The action of the transition to take.

theorem Turing.MultiTapeTM.Universal.stepWith_eq (c : WCtx) : stepWith c.1.1 c.1.2 c.2 = if c.1.2.state.isSome = true then if (wFound c).isSome = true then ({ state := (wAct c).state, inputPos := moveInput c.1.2.inputPos c.2 (wAct c).inputTape, workTapes := applyTapes c.1.2.workTapes (wAct c).workTapes }, (wAct c).output) else ({ state := none, inputPos := c.1.2.inputPos, workTapes := c.1.2.workTapes }, none) else (c.1.2, none)

def Turing.MultiTapeTM.Universal.wTime (c : WCtx) : ℕ

The time bound of a step without the input: the number of work tapes and of transitions, times the square of the length of the context.

theorem Turing.MultiTapeTM.Universal.stepWith_inO : ComputableTidilyInO (fun (c : WCtx) => stepWith c.1.1 c.1.2 c.2) eWCtx (encPair eCfg eSym) wTime fun (c : WCtx) => (eWCtx c).length

One step of the simulation without the input, within the time wTime and linear space.

A step

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.Ctx : Type

The context of a step: the description, the input and the configuration.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eCtx : Ctx ↪ List Bool

The encoding of contexts.

def Turing.MultiTapeTM.Universal.stepTime (c : Ctx) : ℕ

The time bound of a step: the number of work tapes, of transitions and the position of the input head, times the square of the length of the context.

theorem Turing.MultiTapeTM.Universal.step_inO : ComputableTidilyInO (fun (c : Ctx) => step c.1.1 c.1.2 c.2) eCtx (encPair eCfg eSym) stepTime fun (c : Ctx) => (eCtx c).length

One step of the simulation, on contexts, within the time stepTime and linear space: the symbol under the input head, and the step without the input.