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/4] 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/4] 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/4] 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 From e9426ed54f546d2cd54aba5ec6cadac58e7dfb4f Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Wed, 19 Aug 2026 14:18:43 +0300 Subject: [PATCH 4/4] feat(MultiTapeTM): Nondeterministic multi-tape Turing machines A nondeterministic machine replaces the transition function by a transition relation. Configurations and the effect of an action move to a shared `MultiTape/Configuration.lean`; no existing statement changes meaning. A computation path is a `RelSeries` of the step relation starting at the initial configuration, so Mathlib supplies its length, the configurations it passes through, and the one it ends at. `MultiTapeTM.toNTM` embeds the deterministic machine and `toNTM_computes` shows the embedding preserves computation in bounded time and space. Co-Authored-By: Claude Opus 5 (1M context) --- Cslib.lean | 3 + .../Turing/MultiTape/Configuration.lean | 187 ++++++++++++++++++ .../Turing/MultiTape/Deterministic.lean | 144 ++------------ .../DeterministicToNondeterministic.lean | 94 +++++++++ .../Turing/MultiTape/Nondeterministic.lean | 139 +++++++++++++ 5 files changed, 441 insertions(+), 126 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean diff --git a/Cslib.lean b/Cslib.lean index a4d250711..81c530887 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -44,7 +44,10 @@ public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Languages.SafetyLiveness +public import Cslib.Computability.Machines.Turing.MultiTape.Configuration public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.DeterministicToNondeterministic +public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas public import Cslib.Computability.Machines.Turing.SingleTape.Defs public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean new file mode 100644 index 000000000..27ea589ae --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -0,0 +1,187 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Aviv Bar Natan +-/ + +module + +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Algebra.Order.Group.Abs +public import Mathlib.Algebra.Order.Group.Int +public import Mathlib.Data.Finset.Dedup +public import Mathlib.Data.Finset.Max +public import Mathlib.Data.Int.Interval +public import Mathlib.Data.Sign.Defs +public import Cslib.Init + +/-! +# Configurations of Multi-Tape Turing Machines + +Configurations of a multi-tape Turing machine with a read-only input tape, `k` work tapes and one +write-only output tape, together with what a single transition does to one and the space measure +read off a list of them. + +## Design + +Nothing here mentions a machine. A step is described in two parts: an `Action`, recording +which way the input head moves, what is written and where the work heads move, which symbol is +emitted and which state follows; and `Action.apply`, which carries it out on a +configuration. + +The output tape is part of the configuration, so the string emitted along a run can be read off +the configuration the run ends in. + +## Important Declarations + +* `Cfg`: the configuration: the internal state, the tape contents and head positions, and the + output tape +* `Action`: what a machine does in one step +* `Action.apply`: the effect of one action on a configuration +* `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in +* `spaceUsedOfCfgs`: work tape cells touched along a list of configurations +-/ + +@[expose] public section + +namespace Turing + +variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} + +/-- What a machine does in one step. -/ +structure Action (k : ℕ) (Symbol State : Type*) where + /-- The movement (attempt) of the input head. -/ + inputMove : SignType + /-- Actions on the work tapes: optionally a symbol to write and the head movement. -/ + workActions : Fin k → (Option (Option Symbol)) × SignType + /-- An optional symbol to output. -/ + outS : Option Symbol + /-- The successor state or none to halt. -/ + q' : Option State + +/-- +The configurations of a Turing machine is relative to the input of the machine and consist of: +- 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 contents of the write-only output tape +-/ +@[ext] +structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where + /-- the state of the TM (or none for the halting state) -/ + state : Option State + /-- the position of the input head, shifted by one -/ + inputPos : Fin (input.length + 2) + /-- the work tapes -/ + 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. +The machine can only read one empty cell outside of the input, +any attempted movement beyond that results in no movement. + +The addition is performed in `ℤ` before clamping. Performing it in `Fin (n + 2)` would wrap an +outward boundary move to the opposite end of the input. -/ +@[scoped grind =] +def moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : Fin (n + 2) := + let p := ((pos.val : ℤ) + (m.cast : ℤ)).toNat + if h : p < n + 2 then ⟨p, h⟩ else ⟨n + 1, by omega⟩ + +@[simp] +lemma moveInputPos_zero {n : ℕ} (pos : Fin (n + 2)) : + moveInputPos pos 0 = pos := by + apply Fin.ext + simp [moveInputPos, pos.isLt] + +@[simp] +lemma moveInputPos_leftBoundary {n : ℕ} : + moveInputPos (0 : Fin (n + 2)) (-1) = 0 := by + apply Fin.ext + simp [moveInputPos] + +@[simp] +lemma moveInputPos_rightBoundary {n : ℕ} : + moveInputPos (⟨n + 1, by omega⟩ : Fin (n + 2)) 1 = ⟨n + 1, by omega⟩ := by + unfold moveInputPos + rw [dite_eq_right (by simp; omega)] + +/-- A left move away from the left input boundary decrements the native input position. -/ +lemma moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) : + moveInputPos p .neg = ⟨p.val - 1, by have := p.isLt; omega⟩ := by + have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => h (Fin.ext hz)) + unfold moveInputPos + apply Fin.ext + rw [dite_eq_left] <;> simp <;> omega + +/-- A right move away from the right input boundary increments the native input position. -/ +lemma moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : p.val ≠ n + 1) : + moveInputPos p .pos = ⟨p.val + 1, by have := p.isLt; omega⟩ := by + unfold moveInputPos + rw [dite_eq_left] + · apply Fin.ext + simp + · simp + omega + +/-- The symbol currently under the input tape head. -/ +def Cfg.inputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := + if h₁ : cfg.inputPos = 0 then none + else if h₂ : cfg.inputPos = input.length + 1 then none + else input[cfg.inputPos.val - 1]'(by grind) + +@[simp] +lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ) + (h₁ : cfg.inputPos.val = 1 + p) + (h₂ : p < input.length) : + cfg.inputSymbol = some input[p] := by + grind [Cfg.inputSymbol] + +/-- The symbol read by work tape `i`. -/ +def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol := + cfg.workTapes i (cfg.workTapePos i) + +/-- A configuration is halted when it has no state to continue from. -/ +abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none + +/-- The initial configuration for a starting state and an input string. -/ +@[simp] +def Cfg.init (q₀ : State) (input : List Symbol) : Cfg k Symbol State input := + ⟨some q₀, 1, fun _ _ => none, fun _ => 0, []⟩ + +/-- +The effect of an action on a configuration: move the input head, write and move on the work tapes, +append the emitted symbol to the output tape, and go to the successor state. This is the part of a +step that does not depend on how the action was chosen. +-/ +@[simp] +def Action.apply (out : Action k Symbol State) (cfg : Cfg k Symbol State input) : + Cfg k Symbol State input where + state := out.q' + inputPos := moveInputPos cfg.inputPos out.inputMove + workTapes i := match (out.workActions i).1 with + | none => cfg.workTapes i + | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s + workTapePos i := cfg.workTapePos i + (out.workActions i).2 + output := cfg.output ++ out.outS.toList + +/-- A work tape head moves by at most one cell when an action is applied. -/ +lemma workTapePos_apply_le (out : Action k Symbol State) + (cfg : Cfg k Symbol State input) (i : Fin k) : + |(out.apply cfg).workTapePos i - cfg.workTapePos i| ≤ 1 := by + simp only [Action.apply, add_sub_cancel_left, abs_le, SignType.cast] + grind + +/-- The work tape cells visited by the head of tape `i` along a list of configurations. -/ +def visitedOfCfgs (cfgs : List (Cfg k Symbol State input)) (i : Fin k) : Finset ℤ := + (cfgs.map (·.workTapePos i)).toFinset + +/-- The number of work tape cells touched by the heads along a list of configurations. -/ +def spaceUsedOfCfgs (cfgs : List (Cfg k Symbol State input)) : ℕ := + ∑ i, (visitedOfCfgs cfgs i).card + +end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 3d460e45a..ea4c0fd67 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -6,14 +6,10 @@ Authors: Christian Reitwiessner module -public import Mathlib.Data.Finset.Max -public import Mathlib.Data.Int.Interval -public import Mathlib.Algebra.Order.Group.Abs -public import Mathlib.Algebra.Order.Group.Int public import Mathlib.Algebra.Order.BigOperators.Group.Finset public import Mathlib.Computability.Language -public import Mathlib.Data.Sign.Defs public import Cslib.Foundations.Data.RelatesInSteps +public import Cslib.Computability.Machines.Turing.MultiTape.Configuration /-! # Deterministic Multi-Tape Turing Machines @@ -67,8 +63,6 @@ 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, - 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 @@ -102,17 +96,6 @@ namespace Turing variable {k : ℕ} {State Symbol : Type*} -/-- The output of the transition function. -/ -structure TransitionOut (k : ℕ) (Symbol State : Type*) where - /-- The movement (attempt) of the input head. -/ - inputMove : SignType - /-- Actions on the work tapes: optionally a symbol to write and the head movement. -/ - workActions : Fin k → (Option (Option Symbol)) × SignType - /-- An optional symbol to output. -/ - outS : Option Symbol - /-- The successor state or none to halt. -/ - q' : Option State - /-- A multi-tape Turing machine with `k` work tapes over the alphabet of `Option Symbol` (where `none` is the blank tape symbol). Note that it is not required that `Symbol` or `State` are finite @@ -126,7 +109,7 @@ structure MultiTapeTM (k : ℕ) (Symbol State : Type*) where symbols to a movement for the input head, actions on the work tape, optionally a symbol to output and the successor state -/ tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : - TransitionOut k Symbol State + Action k Symbol State namespace MultiTapeTM @@ -135,115 +118,19 @@ variable {tm : MultiTapeTM k Symbol State} section Cfg /-! -## Configurations of a Turing Machine - -This section defines the configurations of a Turing machine, -the step function that lets the machine transition from one configuration to the next, -the resulting sequence of configurations and the initial configuration. --/ +## Stepping a Turing Machine -/-- -The configurations of a Turing machine is relative to the input of the machine and consist of: -- 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 contents of the write-only output tape +This section defines the step function that lets the machine transition from one configuration to +the next, and the configuration reached after a number of steps. Configurations themselves are +defined in `Cslib.Computability.Machines.Turing.MultiTape.Configuration`. -/ -@[ext] -structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where - /-- the state of the TM (or none for the halting state) -/ - state : Option State - /-- the position of the input head, shifted by one -/ - inputPos : Fin (input.length + 2) - /-- the work tapes -/ - 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. -The machine can only read one empty cell outside of the input, -any attempted movement beyond that results in no movement. - -The addition is performed in `ℤ` before clamping. Performing it in `Fin (n + 2)` would wrap an -outward boundary move to the opposite end of the input. -/ -@[scoped grind =] -def moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : Fin (n + 2) := - let p := ((pos.val : ℤ) + (m.cast : ℤ)).toNat - if h : p < n + 2 then ⟨p, h⟩ else ⟨n + 1, by omega⟩ - -@[simp] -lemma moveInputPos_zero {n : ℕ} (pos : Fin (n + 2)) : - moveInputPos pos 0 = pos := by - apply Fin.ext - simp [moveInputPos, pos.isLt] - -@[simp] -lemma moveInputPos_leftBoundary {n : ℕ} : - moveInputPos (0 : Fin (n + 2)) (-1) = 0 := by - apply Fin.ext - simp [moveInputPos] - -@[simp] -lemma moveInputPos_rightBoundary {n : ℕ} : - moveInputPos (⟨n + 1, by omega⟩ : Fin (n + 2)) 1 = ⟨n + 1, by omega⟩ := by - unfold moveInputPos - rw [dite_eq_right (by simp; omega)] - -/-- A left move away from the left input boundary decrements the native input position. -/ -lemma moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) : - moveInputPos p .neg = ⟨p.val - 1, by have := p.isLt; omega⟩ := by - have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => h (Fin.ext hz)) - unfold moveInputPos - apply Fin.ext - rw [dite_eq_left] <;> simp <;> omega - -/-- A right move away from the right input boundary increments the native input position. -/ -lemma moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : p.val ≠ n + 1) : - moveInputPos p .pos = ⟨p.val + 1, by have := p.isLt; omega⟩ := by - unfold moveInputPos - rw [dite_eq_left] - · apply Fin.ext - simp - · simp - omega - -/-- The symbol currently under the input tape head. -/ -def Cfg.inputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := - if h₁ : cfg.inputPos = 0 then none - else if h₂ : cfg.inputPos = input.length + 1 then none - else input[cfg.inputPos.val - 1]'(by grind) - -@[simp] -lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ) - (h₁ : cfg.inputPos.val = 1 + p) - (h₂ : p < input.length) : - cfg.inputSymbol = some input[p] := by - grind [Cfg.inputSymbol] - -/-- The symbol read by work tape `i`. -/ -def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol := - cfg.workTapes i (cfg.workTapePos i) /-- The step function corresponding to a `MultiTapeTM`. -/ def step (cfg : Cfg k Symbol State input) : Cfg k Symbol State input := match cfg.state with -- in the halting state, we stay at the configuration | none => cfg - | some q => - let {inputMove, workActions, q', outS, ..} := tm.tr q cfg.inputSymbol cfg.workTapeSymbols - { - state := q', - inputPos := moveInputPos cfg.inputPos inputMove, - workTapes i := match (workActions i).1 with - | 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 - } + | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).apply cfg /-- The symbol (optionally) output when executing one step starting from configuration `cfg`. -/ def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := @@ -253,8 +140,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, []⟩ +def initCfg (input : List Symbol) : Cfg k Symbol State input := Cfg.init tm.q₀ input @[simp] lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : @@ -305,9 +191,7 @@ lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : unfold step cases hstate : c.state with | none => simp - | some q => - simp only [add_sub_cancel_left, abs_le, SignType.cast] - grind + | some q => exact workTapePos_apply_le _ c i end Cfg @@ -345,6 +229,14 @@ lemma spaceUsedByTape_le_spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) (i tm.spaceUsedByTape cfg t i ≤ tm.spaceUsed cfg t := Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i) +/-- The space used up to step `t` is the space touched by the configurations up to step `t`. -/ +lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : + tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := by + unfold spaceUsed spaceUsedByTape spaceUsedOfCfgs + refine Finset.sum_congr rfl fun i _ => congrArg Finset.card ?_ + ext z + simp [visitedByTapeHead, visitedOfCfgs, Nat.lt_succ_iff] + end Space open Cfg @@ -361,7 +253,7 @@ def TransitionRelation (c₁ c₂ : Cfg k Symbol State input) : Prop := tm.step @[simp] lemma step_output (cfg : Cfg k Symbol State input) : (tm.step cfg).output = cfg.output ++ (tm.outputSymbol cfg).toList := by - unfold step outputSymbol + unfold step outputSymbol Action.apply cases cfg.state <;> simp /-- The output does not change after the machine has halted. -/ diff --git a/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean new file mode 100644 index 000000000..091a3615f --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean @@ -0,0 +1,94 @@ +/- +Copyright (c) 2026 Aviv Bar Natan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aviv Bar Natan +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic + +/-! +# Deterministic Multi-Tape Turing Machines are Nondeterministic + +Embeds `MultiTapeTM` into `MultiTapeNTM` and shows the embedding preserves computation. + +`toNTM` permits exactly the transition `tr` prescribes: nondeterminism is the possibility of +several, so having exactly one is the special case. A deterministic computation is then witnessed +by the machine's own run. Both models idle once the machine has halted, so that run has exactly +`t` steps for every `t` and its measures match `runFrom` and `spaceUsed` directly, with no +reasoning about the step at which the machine halted. + +## Important Declarations + +* `MultiTapeTM.toNTM`: every deterministic machine is a nondeterministic one +* `MultiTapeTM.toNTMComputationPath`: the machine's own run, as a computation of `toNTM` +* `MultiTapeTM.toNTM_computes`: every deterministic computation is a nondeterministic one +-/ + +@[expose] public section + +namespace Turing + +variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} + +/-- Every deterministic machine is a nondeterministic one whose relation is a singleton. -/ +def MultiTapeTM.toNTM (tm : MultiTapeTM k Symbol State) : MultiTapeNTM k Symbol State where + q₀ := tm.q₀ + Tr q input work out := out = tm.tr q input work + +namespace MultiTapeTM + +variable {tm : MultiTapeTM k Symbol State} {t : ℕ} + +@[simp] +lemma toNTM_initCfg (tm : MultiTapeTM k Symbol State) (input : List Symbol) : + tm.toNTM.initCfg input = tm.initCfg input := rfl + +/-- Each step of `tm` is a step of its nondeterministic reading. This holds at a halted +configuration too, where both models idle. -/ +theorem toNTM_step (c : Cfg k Symbol State input) : tm.toNTM.Step c (tm.step c) := by + cases hq : c.state <;> simp [MultiTapeNTM.Step, step, toNTM, hq] + +/-- The machine's own run for `t` steps, as a computation of its nondeterministic reading: the +configuration reached after each step. -/ +def toNTMComputationPath (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : + tm.toNTM.ComputationPath input where + length := t + toFun i := tm.runFrom (tm.initCfg input) i + step i := by + simp only [Fin.val_castSucc, Fin.val_succ, runFrom_succ_eq_step'] + exact toNTM_step _ + head_eq := rfl + +@[simp] +lemma toNTMComputationPath_length : (tm.toNTMComputationPath input t).length = t := rfl + +@[simp] +lemma toNTMComputationPath_last : + (tm.toNTMComputationPath input t).last = tm.runFrom (tm.initCfg input) t := rfl + +@[simp] +lemma toNTMComputationPath_toList : + (tm.toNTMComputationPath input t).toList + = (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) := by + rw [RelSeries.toList, ← List.map_coe_finRange_eq_range, List.map_map] + exact List.ofFn_eq_map + +@[simp] +lemma toNTMComputationPath_space : + (tm.toNTMComputationPath input t).space = tm.spaceUsed (tm.initCfg input) t := by + simp [MultiTapeNTM.ComputationPath.space, spaceUsed_eq_spaceUsedOfCfgs] + +/-- Every deterministic computation is a nondeterministic one, witnessed by the machine's own +run. -/ +theorem toNTM_computes {output : List Symbol} {t s : ℕ} + (h : tm.ComputesInTimeAndSpace input output t s) : + tm.toNTM.ComputesInTimeAndSpace input output t s := + ⟨tm.toNTMComputationPath input t, h.1, h.2.1, toNTMComputationPath_length, + toNTMComputationPath_space.trans h.2.2⟩ + +end MultiTapeTM + +end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean new file mode 100644 index 000000000..64f72a50c --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -0,0 +1,139 @@ +/- +Copyright (c) 2026 Aviv Bar Natan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aviv Bar Natan +-/ + +module + +public import Mathlib.Data.List.Chain +public import Mathlib.Order.RelSeries +public import Cslib.Computability.Machines.Turing.MultiTape.Configuration + +/-! +# Nondeterministic Multi-Tape Turing Machines + +Defines nondeterministic Turing machines with a read-only input tape, `k` work tapes and one +write-only output tape, and what it means for one to compute an output within a time and space +bound. + +## Design + +Following [Papadimitriou94], chapter 2.7, a nondeterministic machine is a Turing machine whose +transition function is replaced by a transition relation: `Tr q input work action` holds when +`action` is one of the actions permitted in that situation. + +A halted configuration steps to itself, so once a machine has halted it has a run of every length. +A time bound is therefore an upper bound, with no separate account of the step at which it halted. + +The transition relation may be empty at a running configuration, so a machine can get stuck. Every +notion below asks for a computation ending in a halted configuration, so a stuck one is not a +witness. + +## Important Declarations + +* `MultiTapeNTM`: the machine, an initial state and a transition relation +* `Step`: the one-step relation on configurations +* `ComputationPath`: a run of the machine: a series of configurations from the initial one, each + reached from the previous by a step +* `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint +* `Computes`, `ComputesInTime`, `ComputesInSpace`, `ComputesInTimeAndSpace`: its instances, whose + bounds all refer to a single computation + +## References + +* [C. Papadimitriou, *Computational Complexity*][Papadimitriou94] +* [M. Sipser, *Introduction to the Theory of Computation*][Sipser2013] +-/ + +@[expose] public section + +namespace Turing + +variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} + +/-- +A nondeterministic multi-tape Turing machine with `k` work tapes over the alphabet of +`Option Symbol` (where `none` is the blank symbol). Neither `Symbol` nor `State` is required to be +finite. +-/ +structure MultiTapeNTM (k : ℕ) (Symbol State : Type*) where + /-- initial state -/ + q₀ : State + /-- transition relation: which combinations of state, current input symbol, tuple of work head + symbols and resulting actions are valid transitions -/ + Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) + (action : Action k Symbol State) : Prop + +namespace MultiTapeNTM + +variable {ntm : MultiTapeNTM k Symbol State} + +/-- The one-step relation on configurations. A halted configuration steps to itself; a running one +steps by any permitted transition. -/ +@[scoped grind =] +def Step (ntm : MultiTapeNTM k Symbol State) (c₁ c₂ : Cfg k Symbol State input) : Prop := + match c₁.state with + | none => c₂ = c₁ + | some q => ∃ out, ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols out ∧ c₂ = out.apply c₁ + +/-- A halted configuration steps only to itself. -/ +lemma step_of_halt {c c' : Cfg k Symbol State input} (h : c.Halted) : + ntm.Step c c' ↔ c' = c := by + simp [Step, h] + +/-- The initial configuration corresponding to an input string. -/ +@[simp] +def initCfg (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : + Cfg k Symbol State input := + Cfg.init ntm.q₀ input + +/-- A computation path of `ntm` on `input`: a series of configurations starting at the initial one, +in which each is reached from the previous by a step. `RelSeries` supplies the series itself, so +`length` is the number of steps taken, `toList` the configurations passed through, and `last` the +one it ends at. +Note that it is not required that the machine terminates at the final configuration of the path. -/ +structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) + extends RelSeries {(c₁, c₂) : Cfg k Symbol State input × _ | ntm.Step c₁ c₂} where + /-- a computation starts at the initial configuration -/ + head_eq : toRelSeries.head = ntm.initCfg input + +namespace ComputationPath + +variable {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} + +/-- The number of work tape cells touched. -/ +def space (p : ntm.ComputationPath input) : ℕ := spaceUsedOfCfgs p.toList + +end ComputationPath + +/-- `ntm` has a computation on `input` that starts at the initial configuration, halts, emits +`output` and satisfies `P`. The notions below are its instances, so their constraints all refer to +a single computation. -/ +def ComputesSuchThat (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) + (P : ntm.ComputationPath input → Prop) : Prop := + ∃ p : ntm.ComputationPath input, p.last.Halted ∧ p.last.output = output ∧ P p + +/-- `ntm` computes `output` from `input`, with no bound on resources. -/ +def Computes (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) : Prop := + ntm.ComputesSuchThat input output fun _ => True + +/-- `ntm` computes `output` from `input` in exactly `t` steps. -/ +def ComputesInTime (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (t : ℕ) : + Prop := + ntm.ComputesSuchThat input output fun p => p.length = t + +/-- `ntm` computes `output` from `input` touching exactly `s` work tape cells. -/ +def ComputesInSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (s : ℕ) : + Prop := + ntm.ComputesSuchThat input output fun p => p.space = s + +/-- `ntm` computes `output` from `input` in `t` steps and `s` work tape cells, by a single +computation. Nondeterministic analogue of `MultiTapeTM.ComputesInTimeAndSpace`. -/ +def ComputesInTimeAndSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) + (t s : ℕ) : Prop := + ntm.ComputesSuchThat input output fun p => p.length = t ∧ p.space = s + +end MultiTapeNTM + +end Turing