From cbfaa3b4fcb59254ab11bfed189fa73a2b15f897 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Fri, 28 Aug 2026 20:15:29 +0300 Subject: [PATCH] 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 the list of configurations it passes through together with a proof that they form a chain of steps from the initial configuration to the one it ends at, so `List.IsChainFromTo` carries the whole validity condition. `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 | 146 ++------------ .../DeterministicToNondeterministic.lean | 107 ++++++++++ .../Turing/MultiTape/Nondeterministic.lean | 144 ++++++++++++++ .../Machines/Turing/MultiTape/TapeLemmas.lean | 2 +- 6 files changed, 461 insertions(+), 128 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 34a0d27be..bca054324 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,7 +46,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..93e8aa70f --- /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.Basic.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. -/ + inputTape : SignType + /-- Actions on the work tapes: optionally a symbol to write and the head movement. -/ + workTapes : Fin k → (Option (Option Symbol)) × SignType + /-- An optional symbol to output. -/ + output : Option Symbol + /-- The successor state or none to halt. -/ + state : 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 (action : Action k Symbol State) (cfg : Cfg k Symbol State input) : + Cfg k Symbol State input where + state := action.state + inputPos := moveInputPos cfg.inputPos action.inputTape + workTapes i := match (action.workTapes i).1 with + | none => cfg.workTapes i + | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s + workTapePos i := cfg.workTapePos i + (action.workTapes i).2 + output := cfg.output ++ action.output.toList + +/-- A work tape head moves by at most one cell when an action is applied. -/ +lemma workTapePos_apply_le (action : Action k Symbol State) + (cfg : Cfg k Symbol State input) (i : Fin k) : + |(action.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 cc54495a3..67e41af37 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.Basic.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,126 +118,29 @@ 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 := match cfg.state with | none => none - | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).outS + | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).output /-- 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] + 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..85af9cffa --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean @@ -0,0 +1,107 @@ +/- +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 action := action = 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 configurations the machine passes through form a chain of steps. -/ +lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : + ((List.range (t + 1)).map (tm.runFrom cfg)).IsChain tm.toNTM.Step := by + rw [List.isChain_iff_getElem] + intro i hi + simp only [List.getElem_map, List.getElem_range] + rw [runFrom_succ_eq_step'] + exact toNTM_step _ + +/-- 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 + cfgs := (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) + last := tm.runFrom (tm.initCfg input) t + isChainFromTo := + { isChain := isChain_map_range _ t + ne_nil := by simp + head_eq := by + rw [List.head_map] + simp [toNTM] + getLast_eq := by + rw [← Option.some_inj, ← List.getLast?_eq_some_getLast, List.range_succ, List.map_append] + simp } + +@[simp] +lemma toNTMComputationPath_time : (tm.toNTMComputationPath input t).time = t := by + simp [MultiTapeNTM.ComputationPath.time, toNTMComputationPath] + +@[simp] +lemma toNTMComputationPath_cfgs : + (tm.toNTMComputationPath input t).cfgs + = (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) := rfl + +@[simp] +lemma toNTMComputationPath_last : + (tm.toNTMComputationPath input t).last = tm.runFrom (tm.initCfg input) t := rfl + +@[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.ComputesInExactTimeAndSpace input output t s := + ⟨tm.toNTMComputationPath input t, by simpa using h.1, by simpa using h.2.1, + toNTMComputationPath_time, 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..c0b859135 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -0,0 +1,144 @@ +/- +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 Cslib.Foundations.Data.List.IsChainFromTo +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`, `ComputesInExactTime`, `ComputesInExactSpace`, `ComputesInExactTimeAndSpace`: + 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 => + ∃ action, ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols action ∧ c₂ = action.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`: the configurations it passes through, forming a chain +of steps from the initial configuration to the one it ends at. -/ +structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) where + /-- the configurations passed through, starting with the initial one -/ + cfgs : List (Cfg k Symbol State input) + /-- the configuration the path ends at -/ + last : Cfg k Symbol State input + /-- consecutive configurations are joined by a step, from the initial configuration to `last` -/ + isChainFromTo : cfgs.IsChainFromTo ntm.Step (ntm.initCfg input) last + +namespace ComputationPath + +variable {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} + +/-- The number of steps taken, the time the computation takes. -/ +def time (p : ntm.ComputationPath input) : ℕ := p.cfgs.length - 1 + +/-- The number of work tape cells touched. -/ +def space (p : ntm.ComputationPath input) : ℕ := spaceUsedOfCfgs p.cfgs + +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 ComputesInExactTime (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (t : ℕ) : + Prop := + ntm.ComputesSuchThat input output fun p => p.time = t + +/-- `ntm` computes `output` from `input` touching exactly `s` work tape cells. -/ +def ComputesInExactSpace (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 ComputesInExactTimeAndSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) + (t s : ℕ) : Prop := + ntm.ComputesSuchThat input output fun p => p.time = t ∧ p.space = s + +end MultiTapeNTM + +end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 15145637a..36a37ec89 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -39,7 +39,7 @@ lemma step_workTapes_eq_of_ne cases hst : cfg.state with | none => simp_all | some q => - rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions j).1 <;> simp_all + rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workTapes j).1 <;> simp_all lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by