refactor(MultiTapeTM): Make the deterministic machine a nondeterministic one

Cslib.lean

@@ -46,7 +46,9 @@ 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.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

Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean

@@ -0,0 +1,236 @@
+/-
+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, moving a head by at most one
+    cell (`workTapePos_apply_le`) and changing no cell but the one under it
+    (`workTapes_apply_eq_of_ne`)
+* `Cfg.stepWith`, `Cfg.StepWith`: one step, choosing an action by a function or by a relation,
+    agreeing via `Cfg.stepWith_iff` when the relation is the function's graph
+* `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in
+* `spaceUsedOfCfgs`: work tape cells touched along a list of configurations, with the bounds
+    `spaceUsedOfCfgs_le` and `spaceUsedOfCfgs_mono`
+-/
+
+@[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
+
+/-- One step from `cfg`, choosing an action with `f`. A halted configuration idles. -/
+@[simp]
+def Cfg.stepWith (cfg : Cfg k Symbol State input) (f : State → Action k Symbol State) :
+    Cfg k Symbol State input :=
+  match cfg.state with
+  | none => cfg
+  | some q => (f q).apply cfg
+
+/-- One step from `cfg`, choosing any action permitted by `R`. A halted configuration idles. -/
+def Cfg.StepWith (cfg cfg' : Cfg k Symbol State input)
+    (R : State → Action k Symbol State → Prop) : Prop :=
+  match cfg.state with
+  | none => cfg' = cfg
+  | some q => ∃ a, R q a ∧ cfg' = a.apply cfg
+
+/-- Choosing from the graph of a function is choosing that function's value: there is exactly one
+step. This is what makes a machine deterministic, said without mentioning one. -/
+theorem Cfg.stepWith_iff {cfg cfg' : Cfg k Symbol State input} {f : State → Action k Symbol State}
+    {R : State → Action k Symbol State → Prop} (h : ∀ q a, R q a ↔ a = f q) :
+    cfg.StepWith cfg' R ↔ cfg' = cfg.stepWith f := by
+  cases hq : cfg.state <;> simp [Cfg.StepWith, Cfg.stepWith, hq, h]
+
+/-- 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
+
+/-- An action only changes the cell its head is on, so a cell elsewhere is left alone. -/
+lemma workTapes_apply_eq_of_ne (a : Action k Symbol State) (cfg : Cfg k Symbol State input)
+    (j : Fin k) (z : ℤ) (hz : z ≠ cfg.workTapePos j) :
+    (a.apply cfg).workTapes j z = cfg.workTapes j z := by
+  rcases hw : (a.workActions j).1 <;> simp_all
+
+/-- 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
+
+/-- Each configuration contributes at most one cell per tape, so space is bounded by length. -/
+theorem spaceUsedOfCfgs_le (cfgs : List (Cfg k Symbol State input)) :
+    spaceUsedOfCfgs cfgs ≤ k * cfgs.length := by
+  calc spaceUsedOfCfgs cfgs
+      ≤ ∑ _i : Fin k, cfgs.length :=
+        Finset.sum_le_sum fun i _ => (List.toFinset_card_le _).trans (by simp)
+    _ = k * cfgs.length := by simp
+
+/-- Passing through more configurations touches more cells. -/
+theorem spaceUsedOfCfgs_mono {c d : List (Cfg k Symbol State input)} (h : c.Sublist d) :
+    spaceUsedOfCfgs c ≤ spaceUsedOfCfgs d :=
+  Finset.sum_le_sum fun i _ => Finset.card_le_card <| by
+    intro z hz
+    simp only [visitedOfCfgs, List.mem_toFinset] at hz ⊢
+    exact (h.map _).subset hz
+
+end Turing