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 configuration map is a homomorphism of step relations (embedHom), so each run path of tm maps to a run path of the larger machine.

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.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.

Equations

• Turing.MultiTapeTM.partialInv e l = if h : l ∈ Set.range ⇑e then some (e.invOfMemRange ⟨l, h⟩) else none

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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_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

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. Follows.stepHom builds it, since embed agrees with the adapter defining extendTapes.

Equations

• tm.embedHom e extraTapes extraPos = ⋯.stepHom (fun (x : Turing.Cfg k Symbol State input) => Turing.MultiTapeTM.embed e x extraTapes extraPos) ⋯ ⋯ ⋯

@[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.

Equations

• Turing.MultiTapeTM.tapeEmb i = { toFun := fun (x : Fin 1) => i, inj' := ⋯ }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Turing.MultiTapeTM.noTapes k = { toFun := Fin.elim0, inj' := ⋯ }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.