Documentation

Complexity.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes

Specifications on the selected tapes #

The additions of cslib PR #1111 and of Christian Reitwiessner's branch crei/tidy-universal to Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes.

Main results #

Specifications on the selected tapes #

source
theorem Turing.MultiTapeTM.embed_wordsCfg {k k' : ℕ} {Symbol : Type u_1} {State : Type u_3} {input : List Symbol} (e : Fin k ↪ Fin k') {q : Option State} {v : Fin k → List Symbol} {ws ws' : Fin k' → List Symbol} {out : List Symbol} (h : ∀ (j : Fin k), ws' (e j) = v j) (hx : ∀ l ∉ Set.range ⇑e, ws' l = ws l) :
(embed e (wordsCfg input q v out) (fun (l : Fin k') => tapeOfList (ws l)) fun (x : Fin k') => 0) = wordsCfg input q ws' out

Placing the words v on the tapes selected by e and the words ws on the others gives the wordsCfg configuration of any ws' that agrees with v through e and with ws elsewhere.

source
theorem Turing.MultiTapeTM.TransformsTapes.extendTapes {k k' : ℕ} {Symbol : Type u_1} {State : Type u_3} {tm : MultiTapeTM k Symbol State} {P : List Symbol → (Fin k → List Symbol) → Prop} {Q : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} {t s : ℕ} (h : tm.TransformsTapes P Q t s) (e : Fin k ↪ Fin k') :
(tm.extendTapes e).TransformsTapes (fun (input : List Symbol) (ws : Fin k' → List Symbol) => P input fun (j : Fin k) => ws (e j)) (fun (input : List Symbol) (ws ws' : Fin k' → List Symbol) (emitted : List Symbol) => Q input (fun (j : Fin k) => ws (e j)) (fun (j : Fin k) => ws' (e j)) emitted ∧ ∀ l ∉ Set.range ⇑e, ws' l = ws l) t (s + (k' - k))

A specification on the tapes selected by e. tm.extendTapes e transforms the words on the selected tapes as tm does and leaves every other word alone; each other tape costs one cell.

source
theorem Turing.MultiTapeTM.TransformsTapes.extendTapes_update {m K : ℕ} {Symbol : Type u_1} {S : Type u_2} {tm : MultiTapeTM m Symbol S} {I : List Symbol → Prop} {i o : Fin m} {w out y : List Symbol} {t s : ℕ} (h : tm.TransformsTapes (fun (inp : List Symbol) (ws : Fin m → List Symbol) => I inp ∧ ws = Function.update (fun (x : Fin m) => []) i w) (fun (x : List Symbol) (ws ws' : Fin m → List Symbol) (em : List Symbol) => ws' = Function.update ws o out ∧ em = y) t s) (e : Fin m ↪ Fin K) :
(tm.extendTapes e).TransformsTapes (fun (inp : List Symbol) (ws : Fin K → List Symbol) => I inp ∧ ws = Function.update (fun (x : Fin K) => []) (e i) w) (fun (x : List Symbol) (ws ws' : Fin K → List Symbol) (em : List Symbol) => ws' = Function.update ws (e o) out ∧ em = y) t (s + (K - m))

A specification that starts with the word w on tape i and every other tape blank and writes out to tape o, on the tapes selected by e.

Space of reindexed runs #

source
theorem Turing.MultiTapeTM.space_embed_le {k k' : ℕ} {Symbol : Type u_1} {State : Type u_3} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (n : ℕ) :
space (embed e cfg extraTapes extraPos) n ≤ space cfg n + (k' - k)

Space bound for a reindexed run. The embedded tapes contribute the space used by tm, while each of the remaining k' - k tapes never moves and contributes at most one cell.

source
theorem Turing.MultiTapeTM.space_tapeEmb_le {Symbol : Type u_1} {State : Type u_3} {input : List Symbol} {k : ℕ} (tm : MultiTapeTM 1 Symbol State) (i : Fin k) (cfg : Cfg k Symbol State input) (n : ℕ) :
space cfg n ≤ space (oneTapeCfg i cfg) n + (k - 1)

Space bound for a one-tape machine placed on tape i: the space of the one-tape run, plus one cell for each tape the machine does not use.

source
theorem Turing.MultiTapeTM.space_noTapes_le {Symbol : Type u_1} {State : Type u_3} {input : List Symbol} {k : ℕ} (tm : MultiTapeTM 0 Symbol State) (cfg : Cfg k Symbol State input) (n : ℕ) :
space cfg n ≤ k

Space bound for a machine without work tapes: one cell for each tape it does not use.