Extending a machine with additional work tapes

extendTapes tm e, for an embedding e : Fin k ↪ Fin k', runs tm inside a machine with more work tapes. The tapes selected by e are used by tm: target tape e j plays the role of source tape j. The remaining tapes are left unchanged.

The configuration map embed e cfg extraTapes extraPos places cfg on the selected tapes and initialises the remaining tapes from extraTapes and extraPos.

The main lemmas show that one step and an entire run path of the larger machine mirror the corresponding step and run path of tm.

Main definitions

• Turing.MultiTapeTM.partialInv: the partial inverse of the tape embedding.
• Turing.MultiTapeTM.extendTapes: the machine with reindexed work tapes.
• Turing.MultiTapeTM.embed: the corresponding configuration map.
• Turing.MultiTapeTM.embedHom: the configuration map as a step-preserving map, which maps run paths.
• Turing.MultiTapeTM.tapeEmb: the embedding placing the only tape of a one-tape machine on tape i, and Turing.MultiTapeTM.noTapes: the embedding of a machine without work tapes.

Main results

• Turing.MultiTapeTM.step_embed: the one-step mirroring lemma.
• Turing.MultiTapeTM.space_map_embedHom_le: the space bound for a mapped path.
• Turing.MultiTapeTM.oneTapeCfg: the one-tape view of a configuration.
• Turing.MultiTapeTM.runFrom_tapeEmb: the run of a one-tape machine placed on work tape i.
• Turing.MultiTapeTM.TransformsTapes.tapeEmb: a one-tape specification, read on tape i.
• Turing.MultiTapeTM.runFrom_noTapes: the run of a machine without work tapes, placed in a machine with k of them.

def Turing.MultiTapeTM.partialInv {k k' : ℕ} (e : Fin k ↪ Fin k') (l : Fin k') : Option (Fin k)

The computable analogue of Function.partialInv for an embedding e: partialInv e l = some j when e j = l (such j is unique by injectivity), and none when l lies outside the range of e.

theorem Turing.MultiTapeTM.partialInv_isPartialInv {k k' : ℕ} (e : Fin k ↪ Fin k') : Function.IsPartialInv (⇑e) (partialInv e)

partialInv e is a partial inverse of e.

noncomputable def Turing.MultiTapeTM.extendTapes {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') : MultiTapeTM k' Symbol State

tm run on the tapes selected by the embedding e, leaving other tapes untouched: work tape e j plays the role of tm's tape j, and any tape outside range e is never written and never moves.

@[simp]

theorem Turing.MultiTapeTM.extendTapes_q₀ {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') : (tm.extendTapes e).q₀ = tm.q₀

def Turing.MultiTapeTM.embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : Cfg k' Symbol State input

A configuration of tm, embedded: tape j goes to tape e j, the tapes outside range e carry the given extraTapes contents and extraPos head positions.

@[simp]

theorem Turing.MultiTapeTM.partialInv_embed {k k' : ℕ} (e : Fin k ↪ Fin k') (j : Fin k) : partialInv e (e j) = some j

The partial inverse recovers the source tape of an embedded tape.

theorem Turing.MultiTapeTM.partialInv_eq_none {k k' : ℕ} (e : Fin k ↪ Fin k') {l : Fin k'} (hl : l ∉ Set.range ⇑e) : partialInv e l = none

Outside the range of e, the partial inverse is undefined.

theorem Turing.MultiTapeTM.partialInv_eq_some {k k' : ℕ} (e : Fin k ↪ Fin k') {l : Fin k'} {j : Fin k} (h : partialInv e l = some j) : e j = l

If the partial inverse is some j, then e j = l.

@[simp]

theorem Turing.MultiTapeTM.embed_inputSymbol {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (embed e cfg extraTapes extraPos).inputSymbol = cfg.inputSymbol

@[simp]

theorem Turing.MultiTapeTM.embed_workTapes_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (j : Fin k) : (embed e cfg extraTapes extraPos).workTapes (e j) = cfg.workTapes j

@[simp]

theorem Turing.MultiTapeTM.embed_workTapePos_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (j : Fin k) : (embed e cfg extraTapes extraPos).workTapePos (e j) = cfg.workTapePos j

@[simp]

theorem Turing.MultiTapeTM.embed_workTapeSymbols_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (j : Fin k) : (embed e cfg extraTapes extraPos).workTapeSymbols (e j) = cfg.workTapeSymbols j

theorem Turing.MultiTapeTM.step_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : Function.Semiconj (fun (x : Cfg k Symbol State input) => embed e x extraTapes extraPos) step step

Reindexing is a step-semiconjugation: the reindexed machine acts on the embedded tapes exactly as tm does, and never touches the extra tapes.

noncomputable def Turing.MultiTapeTM.embedHom {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (tm.stepRel input).Hom ((tm.extendTapes e).stepRel input)

embed as a homomorphism of step relations: each step c → c' of tm becomes the step embed c → embed c' of the reindexed machine, so a run path of tm maps to a run path of the reindexed machine, with the extra tapes held fixed. stepHom builds it from step_embed, which says that embed commutes with the step functions.

@[simp]

theorem Turing.MultiTapeTM.embedHom_apply {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (x✝ : Cfg k Symbol State input) : (tm.embedHom e extraTapes extraPos) x✝ = embed e x✝ extraTapes extraPos

theorem Turing.MultiTapeTM.space_map_embedHom_le {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (p : tm.RunPath input) : (p.map (tm.embedHom e extraTapes extraPos)).space ≤ p.space + (k' - k)

Space bound for a reindexed path. The embedded tapes visit what the original path visits, while each of the remaining k' - k tapes never moves and contributes one cell.

Placing a one-tape machine on a single work tape

def Turing.MultiTapeTM.tapeEmb {k : ℕ} (i : Fin k) : Fin 1 ↪ Fin k

The embedding that places the only work tape of a one-tape machine on tape i.

@[simp]

theorem Turing.MultiTapeTM.tapeEmb_apply {k : ℕ} (i : Fin k) (j : Fin 1) : (tapeEmb i) j = i

@[simp]

theorem Turing.MultiTapeTM.range_tapeEmb {k : ℕ} (i : Fin k) : Set.range ⇑(tapeEmb i) = {i}

@[simp]

theorem Turing.MultiTapeTM.partialInv_tapeEmb {k : ℕ} (i l : Fin k) : partialInv (tapeEmb i) l = if l = i then some 0 else none

Tape i is the image of the only tape of a one-tape machine, and no other tape is.

theorem Turing.MultiTapeTM.embed_tapeEmb {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (i : Fin k) (cfg : Cfg 1 Symbol State input) (tapes : Fin k → ℤ → Option Symbol) (heads : Fin k → ℤ) : embed (tapeEmb i) cfg tapes heads = { state := cfg.state, inputPos := cfg.inputPos, workTapes := Function.update tapes i (cfg.workTapes 0), workTapePos := Function.update heads i (cfg.workTapePos 0), output := cfg.output }

A one-tape configuration placed on tape i leaves every other tape as it was.

def Turing.MultiTapeTM.oneTapeCfg {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (i : Fin k) (cfg : Cfg k Symbol State input) : Cfg 1 Symbol State input

The one-tape view of a configuration of a machine with k work tapes: the tape and head of tape i, with everything else as it is.

theorem Turing.MultiTapeTM.embed_oneTapeCfg {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (i : Fin k) (cfg : Cfg k Symbol State input) : embed (tapeEmb i) (oneTapeCfg i cfg) cfg.workTapes cfg.workTapePos = cfg

A configuration is its own one-tape view on tape i, placed back on tape i.

theorem Turing.MultiTapeTM.runFrom_tapeEmb {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (tm : MultiTapeTM 1 Symbol State) (i : Fin k) (cfg : Cfg k Symbol State input) (n : ℕ) : runFrom cfg n = embed (tapeEmb i) (runFrom (oneTapeCfg i cfg) n) cfg.workTapes cfg.workTapePos

Running a one-tape machine on work tape i. The run is the run on the one-tape view of the configuration, placed back on tape i; every other tape and head keeps its starting value. Combine with embed_tapeEmb to read off the resulting configuration.

theorem Turing.MultiTapeTM.TransformsTapes.tapeEmb {Symbol : Type u_1} {State : Type u_2} {k : ℕ} {tm : MultiTapeTM 1 Symbol State} {P : List Symbol → (Fin 1 → List Symbol) → Prop} {Q : List Symbol → (Fin 1 → List Symbol) → (Fin 1 → List Symbol) → List Symbol → Prop} {t s : ℕ} (h : tm.TransformsTapes P Q t s) (i : Fin k) : (tm.extendTapes (MultiTapeTM.tapeEmb i)).TransformsTapes (fun (input : List Symbol) (ws : Fin k → List Symbol) => P input fun (x : Fin 1) => ws i) (fun (input : List Symbol) (ws ws' : Fin k → List Symbol) (emitted : List Symbol) => ∃ (v : Fin 1 → List Symbol), Q input (fun (x : Fin 1) => ws i) v emitted ∧ ws' = Function.update ws i (v 0)) t (s + (k - 1))

A one-tape specification on tape i. A one-tape machine placed on tape i transforms the word on that tape as it did on its own tape and leaves every other word alone; each remaining tape costs one cell.

def Turing.MultiTapeTM.noTapes (k : ℕ) : Fin 0 ↪ Fin k

The embedding of a machine without work tapes into a machine with k of them.

@[simp]

theorem Turing.MultiTapeTM.partialInv_noTapes {k : ℕ} (l : Fin k) : partialInv (noTapes k) l = none

No tape is in the range of noTapes.

def Turing.MultiTapeTM.noTapesCfg {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (cfg : Cfg k Symbol State input) : Cfg 0 Symbol State input

The view of a configuration as a configuration of a machine without work tapes.

theorem Turing.MultiTapeTM.embed_noTapes {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (cfg : Cfg 0 Symbol State input) (tapes : Fin k → ℤ → Option Symbol) (heads : Fin k → ℤ) : embed (noTapes k) cfg tapes heads = { state := cfg.state, inputPos := cfg.inputPos, workTapes := tapes, workTapePos := heads, output := cfg.output }

A configuration without work tapes, placed in a machine with k of them, only contributes its state, its input head and its output.

theorem Turing.MultiTapeTM.embed_noTapesCfg {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (cfg : Cfg k Symbol State input) : embed (noTapes k) (noTapesCfg cfg) cfg.workTapes cfg.workTapePos = cfg

A configuration is its tapeless view, placed back on its tapes.

theorem Turing.MultiTapeTM.runFrom_noTapes {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (tm : MultiTapeTM 0 Symbol State) (cfg : Cfg k Symbol State input) (n : ℕ) : runFrom cfg n = { state := (runFrom (noTapesCfg cfg) n).state, inputPos := (runFrom (noTapesCfg cfg) n).inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos, output := (runFrom (noTapesCfg cfg) n).output }

Running a machine without work tapes inside a machine with k of them. Only the state, the input head and the output change; every work tape and work head keeps its starting value.