From 1ef9de20bca68e3f9e016531b08aac96168fe100 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 15 Aug 2026 01:46:24 +0300 Subject: [PATCH] feat(MultiTapeTM): Nondeterministic multi-tape Turing machines A nondeterministic multi-tape Turing machine is a `MultiTapeTM` whose transition function is replaced by a transition relation. Configurations, transition outputs and the effect of a single step move to a shared `MultiTape/Basic.lean`; no existing statement changes meaning. The semantics is a labelled transition system on configurations, a step labelled by the symbol it emits. A `Computation` is a chain of such transitions, with time, output and space read off it. `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 + .../Machines/Turing/MultiTape/Basic.lean | 206 ++++++++++++++++++ .../Turing/MultiTape/Deterministic.lean | 139 ++---------- .../DeterministicToNonDeterministic.lean | 122 +++++++++++ .../Turing/MultiTape/NonDeterministic.lean | 181 +++++++++++++++ 5 files changed, 533 insertions(+), 118 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Basic.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 982b94f5d..e9625ff09 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.Basic 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/Basic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Basic.lean new file mode 100644 index 000000000..a5baf816d --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Basic.lean @@ -0,0 +1,206 @@ +/- +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 Cslib.Init +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.Data.Sign.Defs + +/-! +# 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 step does to one and the measures read off a +run. + +Nothing here mentions a machine. A step is described in two parts: a `TransitionOut`, 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 `TransitionOut.apply`, which carries it out on a +configuration. + +## Important Declarations + +* `Cfg`: the configuration of a machine: the internal state, the tape contents and head positions +* `TransitionOut`: what a machine does in one step +* `TransitionOut.apply`: the effect of one step 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 +* `outputOfLabels`: the string emitted along a run, from the symbols emitted at each step +-/ + +@[expose] public section + +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 + + +/-- +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. +-/ +@[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 → ℤ +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] + +/-- A configuration has halted. Reducible, so that a hypothesis of this form is usable directly as +the underlying equation. -/ +abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none + +/-- The configuration a machine starts in: blank work tapes, every head at the origin, and the +input head on the first input cell. -/ +@[simp] +def Cfg.init (q₀ : State) (input : List Symbol) : Cfg k Symbol State input := + ⟨some q₀, 1, fun _ _ => none, fun _ => 0⟩ + +/-- 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 effect of a transition on a configuration: move the input head, write and move on the work +tapes, and go to the successor state. This is the part of a step that does not depend on how the +transition was chosen. +-/ +@[simp] +def TransitionOut.apply (out : TransitionOut k Symbol State) (cfg : Cfg k Symbol State input) : + Cfg k Symbol State input := + { + 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 + } + +/-- A work tape head moves by at most one cell when a transition is applied. -/ +lemma workTapePos_apply_le (out : TransitionOut k Symbol State) (cfg : Cfg k Symbol State input) + (i : Fin k) : + |(out.apply cfg).workTapePos i - cfg.workTapePos i| ≤ 1 := by + simp only [TransitionOut.apply, add_sub_cancel_left, abs_le, SignType.cast] + grind + +/-- The positions visited by the head of work 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 along a list of configurations. + +This is the space measure once the visited configurations are known, independently of how they were +produced. +-/ +def spaceUsedOfCfgs (cfgs : List (Cfg k Symbol State input)) : ℕ := + ∑ i, (visitedOfCfgs cfgs i).card + +/-- +The string emitted along a run, from the symbols emitted at each of its steps: the labels with the +silent steps dropped. +-/ +def outputOfLabels (labels : List (Option Symbol)) : List Symbol := labels.flatMap Option.toList + +@[simp] +lemma outputOfLabels_nil : outputOfLabels ([] : List (Option Symbol)) = [] := rfl + +@[simp] +lemma outputOfLabels_append (labels₁ labels₂ : List (Option Symbol)) : + outputOfLabels (labels₁ ++ labels₂) = outputOfLabels labels₁ ++ outputOfLabels labels₂ := by + simp [outputOfLabels] + +@[simp] +lemma outputOfLabels_singleton (o : Option Symbol) : outputOfLabels [o] = o.toList := by + simp [outputOfLabels] + +end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 625b932b2..7f35b033e 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.Basic /-! # Deterministic Multi-Tape Turing Machines @@ -23,6 +19,10 @@ output tape. The tapes contain symbols from `Option Symbol` for a finite alphabet `Symbol` (where `none` is the blank symbol). +Configurations, the output type of a transition and the effect of a transition on a configuration +are in `Cslib.Computability.Machines.Turing.MultiTape.Basic`; this file adds the machine itself and +its semantics. + ## Design The multi-tape Turing machine uses a read-only input tape, `k` work tapes and a write-only output @@ -67,10 +67,12 @@ 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 -* `spaceUsed`: the number of work tape cells touched by the heads until a certain step +* `step`, `configs`: one execution step, and the sequence of configurations it generates * `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 +* `spaceUsed_eq_spaceUsedOfCfgs`: that measure, read off the configurations visited rather than + the step index +* `outputString`: the string emitted over the first `t` steps * `ComputesInTimeAndSpace`: a proof that a specific TM computes an output from an input in a certain number of steps and using a certain number of tape cells * `ComputableInTimeAndSpace`: a proof that there is a multi-tape TM that computes a function @@ -101,17 +103,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 `BiTape` symbol). Note that it is not required that `Symbol` or `State` are finite @@ -141,104 +132,12 @@ the step function that lets the machine transition from one configuration to the the resulting sequence of configurations and the initial configuration. -/ -/-- -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. --/ -@[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 → ℤ -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', ..} := 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 - } + | 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 := @@ -248,8 +147,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) : @@ -300,9 +198,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 @@ -327,6 +223,13 @@ The number of work tape cells touched by a computation starting from configurati -/ def spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ := ∑ i, tm.spaceUsedByTape cfg t i +/-- The space measure, read off the list of configurations visited rather than the step index. +This is the form shared with the nondeterministic machine, which has no step index to measure at. -/ +lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : + tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.configs cfg)) := by + simp only [spaceUsed, spaceUsedByTape, visitedByTapeHead, spaceUsedOfCfgs, visitedOfCfgs] + exact Finset.sum_congr rfl fun i _ => by congr 1; ext p; simp + /-- A zero-tape Turing machine uses zero space. -/ @[simp] lemma spaceUsed_zero_tapes_eq_zero (cfg : Cfg k Symbol State input) (t : ℕ) (h_zero : k = 0) : @@ -358,7 +261,7 @@ 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 + outputOfLabels ((List.range t).map fun t' => tm.outputSymbol (tm.configs cfg₀ t')) /-- The output produced in `t + 1` steps is the output produced in `t` steps followed by the symbol (optionally) emitted at step `t`. -/ @@ -367,7 +270,7 @@ lemma outputString_succ (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] + simp [outputString, List.range_succ] /-- From a halting configuration, a TM does not output anything. -/ lemma outputString_halt diff --git a/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNonDeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNonDeterministic.lean new file mode 100644 index 000000000..a777169a8 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNonDeterministic.lean @@ -0,0 +1,122 @@ +/- +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.NonDeterministic + +/-! +# Deterministic Multi-Tape Turing Machines are Nondeterministic + +Embeds `MultiTapeTM` into `MultiTapeNTM` and shows the embedding preserves computation. + +`toNTM` relates a situation to exactly the transition `tr` prescribes: nondeterminism is the +possibility of several, so having exactly one is the special case. Every step of `tm` is then a +transition of `tm.toNTM.lts` (`toNTM_lts_tr`), and `run` assembles those steps into a +`MultiTapeNTM.Computation` — the machine's own run, valid by construction. + +What remains is to read the four measures off that run. Both models idle once the machine has +halted, so `run` reaches exactly `t` steps for every `t` and the measures match `configs`, +`outputString` and `spaceUsed` on the nose, with no reasoning about halting times. + +## Important Declarations + +* `MultiTapeTM.toNTM`: every deterministic machine is a nondeterministic one +* `MultiTapeTM.run`: the machine's own run, as a computation of its nondeterministic reading +* `MultiTapeTM.toNTM_computes`: every deterministic computation is a nondeterministic one +-/ + +@[expose] public section + +open Cslib + +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} + +@[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 transition of `tm.toNTM.lts`, labelled by the symbol `tm` emits. This +holds at a halted configuration too, where both models idle. -/ +theorem toNTM_lts_tr (c : Cfg k Symbol State input) : + (tm.toNTM.lts input).Tr c (tm.outputSymbol c) (tm.step c) := by + cases hq : c.state with + | none => simp [MultiTapeNTM.lts, hq] + | some q => simp [MultiTapeNTM.lts, toNTM, outputSymbol, step, hq] + +/-- The run of `tm` from `c` for `t` steps, as a computation of `tm.toNTM`. -/ +def run (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) : + ℕ → tm.toNTM.Computation input c + | 0 => .nil + | n + 1 => .cons (tm.outputSymbol c) (toNTM_lts_tr c) (tm.run (tm.step c) n) + +@[simp] +lemma run_final (c : Cfg k Symbol State input) (t : ℕ) : + (tm.run c t).final = tm.configs c t := by + induction t generalizing c with + | zero => simp [run, MultiTapeNTM.Computation.final] + | succ n ih => rw [run, MultiTapeNTM.Computation.final, ih, configs_succ_eq_step] + +@[simp] +lemma run_labels (c : Cfg k Symbol State input) (t : ℕ) : + (tm.run c t).labels = (List.range t).map fun j => tm.outputSymbol (tm.configs c j) := by + induction t generalizing c with + | zero => simp [run, MultiTapeNTM.Computation.labels] + | succ n ih => + rw [run, MultiTapeNTM.Computation.labels, ih, List.range_succ_eq_map] + simp [configs_succ_eq_step] + +@[simp] +lemma run_visited (c : Cfg k Symbol State input) (t : ℕ) : + (tm.run c t).visited = (List.range (t + 1)).map (tm.configs c) := by + induction t generalizing c with + | zero => simp [run, MultiTapeNTM.Computation.visited] + | succ n ih => + rw [run, MultiTapeNTM.Computation.visited, ih, List.range_succ_eq_map (n := n + 1)] + simp [configs_succ_eq_step] + +@[simp] +lemma run_halts (c : Cfg k Symbol State input) (t : ℕ) : + (tm.run c t).Halts ↔ (tm.configs c t).Halted := by + simp [MultiTapeNTM.Computation.Halts] + +@[simp] +lemma run_time (c : Cfg k Symbol State input) (t : ℕ) : (tm.run c t).time = t := by + simp [MultiTapeNTM.Computation.time] + +@[simp] +lemma run_output (c : Cfg k Symbol State input) (t : ℕ) : + (tm.run c t).output = tm.outputString c t := by + simp [MultiTapeNTM.Computation.output, outputString] + +@[simp] +lemma run_space (c : Cfg k Symbol State input) (t : ℕ) : + (tm.run c t).space = tm.spaceUsed c t := by + simp [MultiTapeNTM.Computation.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.run (tm.initCfg input) t, by simpa using h.1, by simpa using h.2.1, by simp, + by simpa using 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..d82273e9d --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/NonDeterministic.lean @@ -0,0 +1,181 @@ +/- +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.Foundations.Semantics.LTS.Execution +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# 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 `MultiTapeTM` whose +transition function is replaced by a transition relation: `Tr q input work out` holds when `out` is +one of the transitions permitted in that situation. Configurations, transition outputs and +`TransitionOut.apply` are shared with the deterministic machine. + +The semantics is the labelled transition system `lts` on configurations, a step being labelled by +the symbol it emits. The label is where that symbol has to live, since two transitions may lead to +the same successor while emitting different symbols. A halted configuration steps to itself +emitting nothing, as `MultiTapeTM.step` does. + +A `Computation` is a chain of such transitions, with `final`, `time`, `output` and `visited` read +off it by recursion and `space` counting the cells `visited` touches. Space depends on the whole +trajectory and output on the labels, so a computation records both. + +The transition relation may be empty at a running configuration. Every notion below asks for a +computation whose final configuration has halted, so one that cannot continue is not a witness. + +## Important Declarations + +* `MultiTapeNTM`: the machine, an initial state and a transition relation +* `lts`: the labelled transition system on configurations, labelled by the emitted symbol +* `Step`: its underlying unlabelled relation +* `Computation`: a chain of transitions, with `time`, `space`, `output` and `Halts` +* `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 + +open Cslib + +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 transitions are permitted for a state, the current input symbol + and a tuple of work head symbols -/ + Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : + TransitionOut k Symbol State → Prop + +namespace MultiTapeNTM + +variable {ntm : MultiTapeNTM k Symbol State} + +/-- The labelled transition system on configurations. A halted configuration steps to itself +emitting nothing; a running one steps by any permitted transition. -/ +def lts (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : + LTS (Cfg k Symbol State input) (Option Symbol) where + Tr c₁ o c₂ := match c₁.state with + | none => o = none ∧ c₂ = c₁ + | some q => + ∃ out, ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols out ∧ out.outS = o ∧ c₂ = out.apply c₁ + +/-- A halted configuration idles, emitting nothing, exactly as `MultiTapeTM.step` does. -/ +theorem lts_tr_of_halt {c₁ c₂ : Cfg k Symbol State input} {o : Option Symbol} + (h_halt : c₁.Halted) : (ntm.lts input).Tr c₁ o c₂ ↔ o = none ∧ c₂ = c₁ := by + simp [lts, h_halt] + +/-- The one-step relation on configurations, forgetting the emitted symbol. Nondeterministic +analogue of `MultiTapeTM.TransitionRelation`. -/ +@[scoped grind =] +abbrev Step (c₁ c₂ : Cfg k Symbol State input) : Prop := (ntm.lts input).UnlabelledTr c₁ c₂ + +/-- A halted configuration steps only to itself. -/ +theorem step_of_halt {c c' : Cfg k Symbol State input} (h_halt : c.Halted) : + ntm.Step c c' ↔ c' = c := by + simp [Step, LTS.UnlabelledTr, lts_tr_of_halt h_halt] + +/-- The initial configuration corresponding to an input string. -/ +@[simp] +def initCfg (input : List Symbol) : Cfg k Symbol State input := Cfg.init ntm.q₀ input + +/-- A computation of `ntm` from configuration `c`: a chain of transitions of `lts`, in the style of +`SimpleGraph.Walk`. -/ +inductive Computation (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : + Cfg k Symbol State input → Type _ + /-- The empty computation, which does nothing. -/ + | nil {c : Cfg k Symbol State input} : ntm.Computation input c + /-- Extend a computation by one transition at its front. -/ + | cons {c₁ c₂ : Cfg k Symbol State input} (o : Option Symbol) + (h : (ntm.lts input).Tr c₁ o c₂) (rest : ntm.Computation input c₂) : + ntm.Computation input c₁ + +namespace Computation + +variable {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} + {c : Cfg k Symbol State input} + +/-- The configuration the computation ends in. -/ +def final {c : Cfg k Symbol State input} : ntm.Computation input c → Cfg k Symbol State input + | .nil => c + | .cons _ _ rest => rest.final + +/-- The symbol emitted at each step, in order. -/ +def labels {c : Cfg k Symbol State input} : ntm.Computation input c → List (Option Symbol) + | .nil => [] + | .cons o _ rest => o :: rest.labels + +/-- The configurations passed through, starting with `c`. -/ +def visited {c : Cfg k Symbol State input} : + ntm.Computation input c → List (Cfg k Symbol State input) + | .nil => [c] + | .cons _ _ rest => c :: rest.visited + +/-- The number of steps taken. -/ +def time (p : ntm.Computation input c) : ℕ := p.labels.length + +/-- The string emitted. -/ +def output (p : ntm.Computation input c) : List Symbol := outputOfLabels p.labels + +/-- The number of work tape cells touched. -/ +def space (p : ntm.Computation input c) : ℕ := spaceUsedOfCfgs p.visited + +/-- The computation ended in the halting state. -/ +abbrev Halts (p : ntm.Computation input c) : Prop := p.final.Halted + +end Computation + +/-- `ntm` has a computation on `input` that 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.Computation input (ntm.initCfg input) → Prop) : Prop := + ∃ p : ntm.Computation input (ntm.initCfg input), p.Halts ∧ p.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.time = 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.time = t ∧ p.space = s + +end MultiTapeNTM + +end Turing