From 2b62c21fb85001aca39c6132ecafe38f7379ddc0 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Wed, 19 Aug 2026 11:50:09 +0300 Subject: [PATCH 1/3] refactor(MultiTapeTM): Put the output tape into the configuration The configuration gains an `output` field holding the symbols emitted so far, `step` appends to it and `initCfg` starts it empty. The output of a run can then be read off its final configuration, so `outputString` and its lemmas are replaced by `step_output` and existing facts about `configs`, and `ComputesInTimeAndSpace` reads the output from the configuration it already mentions. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 66 ++++++------------- 1 file changed, 19 insertions(+), 47 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 625b932b2..4849b1e07 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -29,7 +29,8 @@ The multi-tape Turing machine uses a read-only input tape, `k` work tapes and a tape. The input head can move freely on the input, but any move attempt beyond one cell outside the input results in no movement. -The transition function can optionally output one symbol, which models the write-only output tape. +The transition function can optionally output one symbol, which is appended to the output tape held +in the configuration, so the output of a run can be read off its final configuration. Because of these restrictions, we ignore the input and output tapes for space usage of the machine. The space usage is defined as the total number of cells the work tape heads visited during execution. @@ -67,7 +68,8 @@ the sub-linear space modifications from chapter 2.5 with the following changes: We define a number of structures and concepts related to multi-tape Turing machine computation: * `MultiTapeTM`: the TM itself -* `Cfg`: the configuration of a TM: the internal state, the work tape contents and head positions +* `Cfg`: the configuration of a TM: the internal state, the work tape contents and head positions, + and the output tape * `spaceUsed`: the number of work tape cells touched by the heads until a certain step * `TransitionRelation`: the transition relation from one configuration to the next * `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure @@ -158,6 +160,8 @@ structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where workTapes : Fin k → ℤ → Option Symbol /-- the positions of the heads on the work tapes -/ workTapePos : Fin k → ℤ + /-- the contents of the write-only output tape -/ + output : List Symbol deriving Inhabited /-- Attempt to move the input tape head. @@ -230,7 +234,7 @@ def step (cfg : Cfg k Symbol State input) : Cfg k Symbol State input := -- in the halting state, we stay at the configuration | none => cfg | some q => - let {inputMove, workActions, q', ..} := tm.tr q cfg.inputSymbol cfg.workTapeSymbols + let {inputMove, workActions, q', outS, ..} := tm.tr q cfg.inputSymbol cfg.workTapeSymbols { state := q', inputPos := moveInputPos cfg.inputPos inputMove, @@ -238,6 +242,7 @@ def step (cfg : Cfg k Symbol State input) : Cfg k Symbol State input := | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s workTapePos i := (cfg.workTapePos i) + (workActions i).2 + output := cfg.output ++ outS.toList } /-- The symbol (optionally) output when executing one step starting from configuration `cfg`. -/ @@ -249,7 +254,7 @@ def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := /-- The initial configuration corresponding to an input string. -/ @[simp] def initCfg (input : List Symbol) : Cfg k Symbol State input := - ⟨some tm.q₀, 1, fun _ _ => none, fun _ => 0⟩ + ⟨some tm.q₀, 1, fun _ _ => none, fun _ => 0, []⟩ @[simp] lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : @@ -352,54 +357,21 @@ which maps a configuration to its next configuration. @[scoped grind =] def TransitionRelation (c₁ c₂ : Cfg k Symbol State input) : Prop := tm.step c₁ = c₂ -/-- The string output by the Turing machine `tm` starting in configuration `cfg₀`, executing for -`t` steps. It is the concatenation of the symbols (optionally) emitted at each of the first `t` -steps. -/ -def outputString - (tm : MultiTapeTM k Symbol State) - (cfg₀ : Cfg k Symbol State input) (t : ℕ) : List Symbol := - (List.range t).flatMap fun t' => (tm.outputSymbol (tm.configs cfg₀ t')).toList - -/-- The output produced in `t + 1` steps is the output produced in `t` steps followed by the symbol -(optionally) emitted at step `t`. -/ -lemma outputString_succ - (tm : MultiTapeTM k Symbol State) - (cfg : Cfg k Symbol State input) (t : ℕ) : - tm.outputString cfg (t + 1) = - tm.outputString cfg t ++ (tm.outputSymbol (tm.configs cfg t)).toList := by - simp [outputString, List.range_succ, List.flatMap_append] - -/-- From a halting configuration, a TM does not output anything. -/ -lemma outputString_halt - (tm : MultiTapeTM k Symbol State) - (cfg : Cfg k Symbol State input) - (h_halt : cfg.state = none) - (t : ℕ) : - tm.outputString cfg t = [] := by - induction t with - | zero => simp [outputString] - | succ t ih => simp [outputString_succ, ih, h_halt] - -lemma outputString_add_eq_append - (tm : MultiTapeTM k Symbol State) - (cfg : Cfg k Symbol State input) (t₁ t₂ : ℕ) : - tm.outputString cfg (t₁ + t₂) = - tm.outputString cfg t₁ ++ tm.outputString (tm.configs cfg t₁) t₂ := by - induction t₂ with - | zero => simp [outputString] - | succ t ih => - rw [show (t₁ + (t + 1)) = (t₁ + t) + 1 by omega] - simp [outputString_succ, ih, configs, ← Function.iterate_add_apply, Nat.add_comm] +/-- One step appends the symbol (optionally) emitted by that step to the output tape. -/ +@[simp] +lemma step_output (cfg : Cfg k Symbol State input) : + (tm.step cfg).output = cfg.output ++ (tm.outputSymbol cfg).toList := by + unfold step outputSymbol + cases cfg.state <;> simp /-- The output does not change after the machine has halted. -/ -lemma outputString_eq_of_halt +lemma output_configs_eq_of_halt (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) (hhalt : (tm.configs cfg τ).state = none) : - tm.outputString cfg t = tm.outputString cfg τ := by + (tm.configs cfg t).output = (tm.configs cfg τ).output := by conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm] - rw [outputString_add_eq_append, outputString_halt _ _ hhalt] - simp + rw [configs_add, configs_of_halts _ hhalt] /-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps and uses exactly `s` space. @@ -409,7 +381,7 @@ def ComputesInTimeAndSpace (input output : List Symbol) (t s : ℕ) : Prop := (tm.configs (tm.initCfg input) t).state = none ∧ - tm.outputString (tm.initCfg input) t = output ∧ + (tm.configs (tm.initCfg input) t).output = output ∧ tm.spaceUsed (tm.initCfg input) t = s /-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of From 794c978767ce0a9f5326fe8a5225009f67f0893e Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Wed, 19 Aug 2026 12:28:29 +0300 Subject: [PATCH 2/3] refactor(MultiTapeTM): Rename `configs` to `runFrom` `configs` returns the single configuration reached after `t` steps, not a sequence of configurations, so the plural name did not match the type. It also depends on `tm` only through its step function. Renamed to `runFrom`, along with its five lemmas. Pure rename, no change to any statement or proof. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 94 +++++++++---------- .../Machines/Turing/MultiTape/TapeLemmas.lean | 22 ++--- 2 files changed, 58 insertions(+), 58 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 4849b1e07..6ed856d1f 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -83,7 +83,7 @@ We define a number of structures and concepts related to multi-tape Turing machi There are two ways to talk about the behaviour of a multi-tape Turing machine, and they are proven to be equivalent. -* `MultiTapeTM.configs`: a sequence of configurations by execution step +* `MultiTapeTM.runFrom`: the configuration reached after a given number of execution steps * `RelatesInSteps tm.TransitionRelation cfg cfg' t`: a proof that `tm` transforms the configuration `cfg` into `cfg'` in exactly `t` steps @@ -262,37 +262,37 @@ lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : unfold step rw [h] -/-- The sequence of configurations of the Turing machine starting from `cfg`. +/-- The configuration reached by running the Turing machine for `t` steps from `cfg`. If the Turing machine halts, it will stay at the halting configuration. -/ -def configs (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg +def runFrom (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg @[simp] -lemma configs_zero {cfg : Cfg k Symbol State input} : - tm.configs cfg 0 = cfg := by - simp [configs] - -lemma configs_succ_eq_step {cfg : Cfg k Symbol State input} {t : ℕ} : - tm.configs cfg (t + 1) = tm.configs (tm.step cfg) t := by - simp [configs, Function.iterate_succ_apply] - -lemma configs_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : - tm.configs cfg (t + 1) = tm.step (tm.configs cfg t) := by - simp [configs, Function.iterate_succ_apply'] - -/-- Running `a + d` steps equals running `a` steps from the configuration reached after `d`. -/ -lemma configs_add (cfg : Cfg k Symbol State input) (a b : ℕ) : - tm.configs cfg (a + b) = tm.configs (tm.configs cfg a) b := by - unfold configs +lemma runFrom_zero {cfg : Cfg k Symbol State input} : + tm.runFrom cfg 0 = cfg := by + simp [runFrom] + +lemma runFrom_succ_eq_step {cfg : Cfg k Symbol State input} {t : ℕ} : + tm.runFrom cfg (t + 1) = tm.runFrom (tm.step cfg) t := by + simp [runFrom, Function.iterate_succ_apply] + +lemma runFrom_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : + tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := by + simp [runFrom, Function.iterate_succ_apply'] + +/-- Running `a + b` steps equals running `b` steps from the configuration reached after `a`. -/ +lemma runFrom_add (cfg : Cfg k Symbol State input) (a b : ℕ) : + tm.runFrom cfg (a + b) = tm.runFrom (tm.runFrom cfg a) b := by + unfold runFrom rw [Nat.add_comm, Function.iterate_add_apply] -/-- The sequence of configurations from a halting state is constant. -/ +/-- Running from a halting configuration stays at that configuration. -/ @[simp] -lemma configs_of_halts (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : - tm.configs cfg n = cfg := by +lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : + tm.runFrom cfg n = cfg := by induction n with | zero => rfl | succ d ih => - rw [configs_succ_eq_step', ih, step_of_halt h] + rw [runFrom_succ_eq_step', ih, step_of_halt h] @[simp] lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) : @@ -317,7 +317,7 @@ section Space /-- The set of positions visited by the head of work tape `i` in the computation starting from configuration `cfg` up to step `t`. -/ def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : Finset ℤ := - (Finset.range (t + 1)).image fun t' => (tm.configs cfg t').workTapePos i + (Finset.range (t + 1)).image fun t' => (tm.runFrom cfg t').workTapePos i /-- The number of work tape cells touched by the head of tape `i` in the computation starting from @@ -365,13 +365,13 @@ lemma step_output (cfg : Cfg k Symbol State input) : cases cfg.state <;> simp /-- The output does not change after the machine has halted. -/ -lemma output_configs_eq_of_halt +lemma runFrom_output_eq_of_halt (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) - (hhalt : (tm.configs cfg τ).state = none) : - (tm.configs cfg t).output = (tm.configs cfg τ).output := by + (hhalt : (tm.runFrom cfg τ).state = none) : + (tm.runFrom cfg t).output = (tm.runFrom cfg τ).output := by conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm] - rw [configs_add, configs_of_halts _ hhalt] + rw [runFrom_add, runFrom_of_halt _ hhalt] /-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps and uses exactly `s` space. @@ -380,8 +380,8 @@ def ComputesInTimeAndSpace (tm : MultiTapeTM k Symbol State) (input output : List Symbol) (t s : ℕ) : Prop := - (tm.configs (tm.initCfg input) t).state = none ∧ - (tm.configs (tm.initCfg input) t).output = output ∧ + (tm.runFrom (tm.initCfg input) t).state = none ∧ + (tm.runFrom (tm.initCfg input) t).output = output ∧ tm.spaceUsed (tm.initCfg input) t = s /-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of @@ -425,19 +425,19 @@ def DecidableInTimeAndSpace /-- This lemma translates between the relational notion and the iterated step notion. The latter can be more convenient especially for deterministic machines as we have here. -/ @[scoped grind =] -lemma relatesInSteps_iff_configs_eq +lemma relatesInSteps_iff_runFrom_eq (tm : MultiTapeTM k Symbol State) (cfg₁ cfg₂ : Cfg k Symbol State input) (t : ℕ) : - RelatesInSteps tm.TransitionRelation cfg₁ cfg₂ t ↔ tm.configs cfg₁ t = cfg₂ := by - unfold configs + RelatesInSteps tm.TransitionRelation cfg₁ cfg₂ t ↔ tm.runFrom cfg₁ t = cfg₂ := by + unfold runFrom induction t generalizing cfg₁ cfg₂ with | zero => simp | succ t ih => rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply'] constructor · grind - · intro h_configs + · intro h_runFrom use tm.step^[t] cfg₁ grind @@ -445,8 +445,8 @@ lemma relatesInSteps_iff_configs_eq if its state is `none` at step `t` and non-none at step `t - 1`. Note that every Turing machine hast to perform at least one step to halt. -/ def haltsAtStep (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : Bool := - (tm.configs (tm.initCfg input) t).state.isNone && - !(tm.configs (tm.initCfg input) (t - 1)).state.isNone + (tm.runFrom (tm.initCfg input) t).state.isNone && + !(tm.runFrom (tm.initCfg input) (t - 1)).state.isNone /-- If a Turing machine halts, the time step is uniquely determined. -/ lemma halting_step_unique @@ -462,39 +462,39 @@ lemma halting_step_unique cases d with | zero => rfl | succ d => - have halts₁ : (tm.configs (tm.initCfg input) t₁).state = none := by + have halts₁ : (tm.runFrom (tm.initCfg input) t₁).state = none := by simp [haltsAtStep] at h_halts₁ exact h_halts₁.left - have halts₂ : (tm.configs (tm.initCfg input) (d + t₁)).state ≠ none := by - grind [haltsAtStep, configs] + have halts₂ : (tm.runFrom (tm.initCfg input) (d + t₁)).state ≠ none := by + grind [haltsAtStep, runFrom] refine absurd ?_ halts₂ - rw [Nat.add_comm, configs_add, tm.configs_of_halts _ halts₁] + rw [Nat.add_comm, runFrom_add, tm.runFrom_of_halt _ halts₁] exact halts₁ /-- If a deterministic machine repeats a non-halting configuration, it never halts, because the sequence between the two configurations will loop forever. Note that this can be applied to two arbitrary and different time steps `t` and `t + Δ` -using `tm.configs_add`. -/ +using `tm.runFrom_add`. -/ lemma not_halts_of_repeat_nonhalt (cfg : Cfg k Symbol State input) (h_not_halt : cfg.state ≠ none) (t : ℕ) - (heq : tm.configs cfg (t + 1) = cfg) : - ∀ t', (tm.configs cfg t').state ≠ none := by + (heq : tm.runFrom cfg (t + 1) = cfg) : + ∀ t', (tm.runFrom cfg t').state ≠ none := by intro t' -- The configuration will repeat every `t + 1` steps. - have hloop : ∀ n, tm.configs cfg (n * (t + 1)) = cfg := by + have hloop : ∀ n, tm.runFrom cfg (n * (t + 1)) = cfg := by intro n induction n with | zero => simp | succ n ih => - rw [show (n + 1) * (t + 1) = n * (t + 1) + (t + 1) by grind, tm.configs_add, ih, heq] + rw [show (n + 1) * (t + 1) = n * (t + 1) + (t + 1) by grind, tm.runFrom_add, ih, heq] by_contra hnh -- Assuming the machine halts at step `t'`, it is also halted at step `t' * (t + 1)` - have h₁ : (tm.configs cfg (t' * (t + 1))).state = none := by + have h₁ : (tm.runFrom cfg (t' * (t + 1))).state = none := by have hle : t' ≤ t' * (t + 1) := by grind obtain ⟨tΔ , htΔ⟩ := Nat.exists_eq_add_of_le hle - rw [htΔ, tm.configs_add] + rw [htΔ, tm.runFrom_add] simp [hnh] simp [hloop t', h_not_halt] at h₁ diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 39ec30f56..15145637a 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -42,11 +42,11 @@ lemma step_workTapes_eq_of_ne rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions j).1 <;> simp_all lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : - z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.configs cfg t').workTapePos i = z := by + z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by simp [visitedByTapeHead] lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : - (tm.configs cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i := + (tm.runFrom cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i := tm.mem_visitedByTapeHead.mpr ⟨t, by omega, rfl⟩ /-- The set of positions visited by a tape head is monotone in the number of steps. -/ @@ -59,14 +59,14 @@ lemma visitedByTapeHead_mono (cfg : Cfg k Symbol State input) (i : Fin k) {t t' `i` and the one after `t` steps is part of the "visited set" at step `t`. -/ lemma uIcc_workTapePos_subset_visitedByTapeHead (cfg : Cfg k Symbol State input) (i : Fin k) (t : ℕ) : - Finset.uIcc (cfg.workTapePos i) ((tm.configs cfg t).workTapePos i) + Finset.uIcc (cfg.workTapePos i) ((tm.runFrom cfg t).workTapePos i) ⊆ tm.visitedByTapeHead cfg t i := by induction t with - | zero => simpa [configs] using tm.mem_visitedByTapeHead_self cfg 0 i + | zero => simpa [runFrom] using tm.mem_visitedByTapeHead_self cfg 0 i | succ t ih => intro z hz - have hstep : |(tm.configs cfg (t + 1)).workTapePos i - (tm.configs cfg t).workTapePos i| ≤ 1 := - configs_succ_eq_step' (tm := tm) ▸ tm.workTapePos_step_le _ i + have hstep : |(tm.runFrom cfg (t + 1)).workTapePos i - (tm.runFrom cfg t).workTapePos i| ≤ 1 := + runFrom_succ_eq_step' (tm := tm) ▸ tm.workTapePos_step_le _ i have hmono := tm.visitedByTapeHead_mono cfg i (Nat.le_succ t) have hself := tm.mem_visitedByTapeHead_self cfg (t + 1) i grind [Finset.mem_uIcc] @@ -76,13 +76,13 @@ lemma mem_visitedByTapeHead_of_workTapes_ne (j : Fin k) (t : ℕ) (z : ℤ) - (h : (tm.configs cfg t).workTapes j z ≠ cfg.workTapes j z) : + (h : (tm.runFrom cfg t).workTapes j z ≠ cfg.workTapes j z) : z ∈ tm.visitedByTapeHead cfg t j := by induction t with - | zero => exact absurd (by simp [configs]) h + | zero => exact absurd (by simp [runFrom]) h | succ t ih => - rw [configs_succ_eq_step'] at h - by_cases hz : z = (tm.configs cfg t).workTapePos j + rw [runFrom_succ_eq_step'] at h + by_cases hz : z = (tm.runFrom cfg t).workTapePos j · exact hz ▸ tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) (tm.mem_visitedByTapeHead_self cfg t j) · rw [tm.step_workTapes_eq_of_ne _ j z hz] at h @@ -109,7 +109,7 @@ lemma content_natAbs_le_spaceUsedByTape {i : Fin k} (t : ℕ) (z : ℤ) - (h : (tm.configs (tm.initCfg input) t).workTapes i z ≠ none) : + (h : (tm.runFrom (tm.initCfg input) t).workTapes i z ≠ none) : z.natAbs ≤ tm.spaceUsedByTape (tm.initCfg input) t i := by -- The work tapes start out blank, so any non-blank cell has been visited by the head; the -- initial head position is `0`, so the displacement bound is a bound on the position itself. From 3f015fbe21be9a97cb87d9495547d001520cdea3 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Wed, 19 Aug 2026 14:17:47 +0300 Subject: [PATCH 3/3] docs(MultiTapeTM): address review comments Keep the design section free of storage details, list the output tape among a configuration's components, and drop the stale `BiTape` mention. Co-Authored-By: Claude Opus 5 (1M context) --- .../Machines/Turing/MultiTape/Deterministic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 6ed856d1f..3d460e45a 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -29,8 +29,7 @@ The multi-tape Turing machine uses a read-only input tape, `k` work tapes and a tape. The input head can move freely on the input, but any move attempt beyond one cell outside the input results in no movement. -The transition function can optionally output one symbol, which is appended to the output tape held -in the configuration, so the output of a run can be read off its final configuration. +The transition function can optionally output one symbol, which models the write-only output tape. Because of these restrictions, we ignore the input and output tapes for space usage of the machine. The space usage is defined as the total number of cells the work tape heads visited during execution. @@ -116,7 +115,7 @@ structure TransitionOut (k : ℕ) (Symbol State : Type*) where /-- A multi-tape Turing machine with `k` work tapes over the alphabet of `Option Symbol` (where `none` -is the blank `BiTape` symbol). Note that it is not required that `Symbol` or `State` are finite +is the blank tape symbol). Note that it is not required that `Symbol` or `State` are finite to keep the definition more general. The restriction will be introduced once we start talking about computability by Turing machines in general. -/ @@ -148,7 +147,8 @@ The configurations of a Turing machine is relative to the input of the machine a - an `Option`al state (or none for the halting state), - the position of the input head (shifted by one), - the contents of the work tape, -- the positions of the work tape heads. +- the positions of the work tape heads, +- the contents of the write-only output tape -/ @[ext] structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where