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). Its time bound separates the configuration length from description lookup and input scanning: for K work tapes, E transitions, description length D, encoded input length N, input position p and binary position length P, the bound is (K + E + 1) * (D + 1) * (L + 1) + (N + 1) * (P + 1) ^ 2. The first word in a transition comparison comes from the description, so its length is bounded by D, even when the simulated configuration is large. The input scanner streams the encoded list with a binary countdown, whose arithmetic is charged to P. The configuration is still copied each round; this bound does not implement the buffered Hennie–Stearns simulation.

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.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 + ((encNat q.1).length + 1) ^ 2) fun (q : ℕ × Option ℕ × SignType) => ((encPair encNat (encPair eSym encSign)) q).length + 1

Moving the input head, charging binary arithmetic only to the encoded position length.

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) : ℕ

A step without input lookup: tape passes and description comparisons are linear in context length; only binary input-head arithmetic is quadratic in its own encoded length.

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 step bound separates linear configuration passes from a streaming input lookup with binary countdown arithmetic. In particular, the whole configuration length is never squared.

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.