feat(Automata, LTS, and Turing): saturated multistep transitions, mapLabel for LTS, and Nondeterministic Turing Machines (NTM)

Cslib.lean

@@ -31,7 +31,9 @@ public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
-public import Cslib.Computability.Machines.SingleTapeTuring.Basic
+public import Cslib.Computability.Machines.Turing.SingleTape.Defs
+public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
@@ -80,6 +82,7 @@ public import Cslib.Foundations.Semantics.LTS.Divergence
 public import Cslib.Foundations.Semantics.LTS.Execution
 public import Cslib.Foundations.Semantics.LTS.HasTau
 public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic
+public import Cslib.Foundations.Semantics.LTS.Map
 public import Cslib.Foundations.Semantics.LTS.Notation
 public import Cslib.Foundations.Semantics.LTS.OmegaExecution
 public import Cslib.Foundations.Semantics.LTS.Relation

Cslib/Computability/Automata/EpsilonNA/Basic.lean

@@ -46,9 +46,8 @@ namespace FinAcc
 that trace from the start state. -/
 @[scoped grind =]
 instance : Acceptor (FinAcc State Symbol) Symbol where
-  Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
-    ∃ s ∈ a.εClosure a.start, ∃ s' ∈ a.accept,
-    a.saturate.MTr s (xs.map (some ·)) s'
+    Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
+  ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.SMTr s (xs.map Option.some) s'
 
 end FinAcc
 

Cslib/Computability/Automata/EpsilonNA/ToNA.lean

@@ -7,32 +7,13 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Computability.Automata.EpsilonNA.Basic
+public import Cslib.Foundations.Semantics.LTS.Map
 
 /-! # Translation of εNA into NA -/
 
 @[expose] public section
 
-namespace Cslib
-
-/-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
-ε-transitions. -/
-@[local grind =]
-def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
-  Tr s μ s' := lts.Tr s (some μ) s'
-
-@[local grind .]
-private lemma LTS.noε_saturate_tr
-  {lts : LTS State (Option Label)} {h : μ = some μ'} :
-  lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
-  grind
-
-@[scoped grind =]
-lemma LTS.noε_saturate_mTr {lts : LTS State (Option Label)} :
-  lts.saturate.MTr s (μs.map some) = lts.saturate.noε.MTr s μs := by
-  ext s'
-  induction μs generalizing s <;> grind [<= LTS.MTr.stepL]
-
-namespace Automata.εNA.FinAcc
+namespace Cslib.Automata.εNA.FinAcc
 
 variable {State Symbol : Type*}
 
@@ -41,21 +22,39 @@ variable {State Symbol : Type*}
 def toNAFinAcc (a : εNA.FinAcc State Symbol) : NA.FinAcc State Symbol where
   start := a.εClosure a.start
   accept := a.accept
-  Tr := a.saturate.noε.Tr
+  toLTS := a.saturate.mapLabel Option.some
 
 open Acceptor in
-open scoped NA.FinAcc in
+open scoped NA.FinAcc LTS LTS.MTr LTS.STr LTS.SMTr in
 /-- Correctness of `toNAFinAcc`. -/
-@[scoped grind _=_]
-theorem toNAFinAcc_language_eq {ena : εNA.FinAcc State Symbol} :
-    language ena.toNAFinAcc = language ena := by
+@[scoped grind =]
+theorem toNAFinAcc_language_eq {a : εNA.FinAcc State Symbol} :
+    language a.toNAFinAcc = language a := by
   ext xs
-  have : ∀ s s', ena.saturate.MTr s (xs.map some) s' = ena.saturate.noε.MTr s xs s' := by
-    simp [LTS.noε_saturate_mTr]
-  #adaptation_note
-  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
-  grind [Accepts]
-
-end Automata.εNA.FinAcc
-
-end Cslib
+  apply Iff.intro <;> intro h <;> rcases h with ⟨s, hs, s', hs', h⟩
+  case mp =>
+    have h_start : ∃ sStart ∈ a.start, a.τSTr sStart s := by
+      simp only [toNAFinAcc, εClosure, LTS.τClosure, LTS.setImage, Set.mem_iUnion,
+        exists_prop] at hs
+      rcases hs with ⟨sStart, h_sStart, hs⟩
+      exists sStart
+      apply And.intro h_sStart
+      simp only [LTS.image, LTS.saturate, Set.mem_setOf_eq] at hs
+      grind only [LTS.sTr_τSTr_iff]
+    rcases h_start with ⟨sStart, h_sStart, h_start⟩
+    exists sStart
+    apply And.intro (by grind)
+    exists s'
+    apply And.intro (by grind)
+    apply LTS.SMTr.comp (μs₁ := []) (s₂ := s) <;> grind
+  case mpr =>
+    cases xs with
+    | nil =>
+      exists s'
+      simp only [toNAFinAcc, LTS.saturate, LTS.τClosure]
+      grind [cases LTS.SMTr]
+    | cons x xs =>
+      exists s
+      grind
+
+end Cslib.Automata.εNA.FinAcc

Cslib/Computability/Machines/Turing/SingleTape/Defs.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Bolton Bailey
+-/
+
+module
+
+public import Cslib.Foundations.Data.BiTape
+
+/-! # Basic definitions for Turing Machines (TMs) -/
+
+@[expose] public section
+
+namespace Cslib.Computability.Turing.SingleTape
+
+/-- The transition labels used by a single-tape Turing Machine. -/
+structure TrLabel (State Symbol : Type*) where
+  /-- Symbol to read from the tape. -/
+  read : Option Symbol
+  /-- Symbol to write on the tape. -/
+  write : Option Symbol
+  /-- Head movement of the tape. -/
+  move : Option Turing.Dir
+
+/-- Configuration of a single-tape Turing machine. -/
+structure Cfg (State Symbol : Type*) where
+  /-- The state that the machine is in. -/
+  state : State
+  /-- Tape of the machine (memory). -/
+  tape : Turing.BiTape Symbol
+
+/-- Helper builder for a configuration with a given tape content. -/
+def Cfg.mk₁ (s : State) (xs : List Symbol) : Cfg State Symbol where
+  state := s
+  tape := Turing.BiTape.mk₁ xs
+
+/-- The space used by a configuration is the space used by its tape. -/
+def Cfg.spaceUsed (cfg : Cfg State Symbol) : ℕ := cfg.tape.spaceUsed
+
+end Cslib.Computability.Turing.SingleTape

Cslib/Computability/Machines/SingleTapeTuring/Basic.lean → Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean

@@ -62,11 +62,12 @@ We also provide ways of constructing polynomial-runtime TMs
 
 @[expose] public section
 
-open Cslib Relation
+open Relation
 
-namespace Turing
+namespace Cslib.Turing
 
 open BiTape StackTape
+open _root_.Turing
 
 variable {Symbol : Type}
 
@@ -503,4 +504,4 @@ end PolyTimeComputable
 
 end SingleTapeTM
 
-end Turing
+end Cslib.Turing

Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Foundations.Data.Relation
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Foundations.Data.BiTape
+public import Cslib.Computability.Machines.Turing.SingleTape.Defs
+
+/-! # Single-Tape Nondeterministic Turing Machines (NTMs)
+
+Nondeterministic Turing Machines (NTMs), defined as nondeterministic automata (`NA`) that act on a
+bidirectional tape (`BiTape`).
+-/
+
+@[expose] public section
+
+namespace Cslib.Computability.Turing.SingleTape
+
+open Automata
+
+/-- A (single-tape) Nondeterministic Turing Machine (NTM) is a nondeterministic automaton equipped
+with a set of accepting halting states. -/
+structure SingleTapeNTM (State Symbol : Type*)
+    extends NA State (SingleTape.TrLabel State Symbol) where
+  /-- The set of accepting states. -/
+  accept : Set State
+  /-- Proof that all accepting states are halting states. -/
+  accept_halting (hmem : s ∈ accept) : ¬∃ μ s', Tr s μ s'
+
+variable {State Symbol : Type*}
+
+/-- An NTM yields a small-step operational semantics on configurations, which codifies an execution
+step. -/
+@[scoped grind =]
+def SingleTapeNTM.Red (m : SingleTapeNTM State Symbol)
+    (c c' : Cfg State Symbol) : Prop :=
+  ∃ μ, m.Tr c.state μ c'.state ∧ -- The controller can perform the move
+    μ.read = c.tape.head ∧ -- The tape has the expected symbol to be read
+    c'.tape = (c.tape.write μ.write).optionMove μ.move -- Write effect on the tape
+
+/-- Multistep execution of an NTM, defined as the reflexive and transitive closure of one-step
+execution.
+-/
+@[scoped grind =]
+def SingleTapeNTM.MRed (m : SingleTapeNTM State Symbol) :=
+  Relation.ReflTransGen m.Red
+
+/-- An NTM is an acceptor of finite lists of symbols. -/
+@[simp, scoped grind =]
+instance : Acceptor (SingleTapeNTM State Symbol) Symbol where
+  Accepts (m : SingleTapeNTM State Symbol) (xs : List Symbol) :=
+    ∃ s ∈ m.start, ∃ c', c'.state ∈ m.accept ∧ m.MRed (Cfg.mk₁ s xs) c'
+
+end Cslib.Computability.Turing.SingleTape

Cslib/Foundations/Data/BiTape.lean

@@ -38,13 +38,13 @@ will not collide.
 
 @[expose] public section
 
-namespace Turing
+namespace Cslib.Turing
 
 /--
 A structure for bidirectionally-infinite Turing machine tapes
 that eventually take on blank `none` values
 -/
-structure BiTape (Symbol : Type) where
+structure BiTape (Symbol : Type*) where
   /-- The symbol currently under the tape head -/
   head : Option Symbol
   /-- The contents to the left of the head -/
@@ -54,7 +54,7 @@ structure BiTape (Symbol : Type) where
 
 namespace BiTape
 
-variable {Symbol : Type}
+variable {Symbol : Type*}
 
 /-- The empty `BiTape` -/
 def nil : BiTape Symbol := ⟨none, ∅, ∅⟩
@@ -92,6 +92,8 @@ Move the head right by shifting the right StackTape under the head.
 def moveRight (t : BiTape Symbol) : BiTape Symbol :=
   ⟨t.right.head, StackTape.cons t.head t.left, t.right.tail⟩
 
+open _root_.Turing
+
 /--
 Move the head to the left or right, shifting the tape underneath it.
 -/
@@ -102,7 +104,7 @@ def move (t : BiTape Symbol) : Dir → BiTape Symbol
 /--
 Optionally perform a `move`, or do nothing if `none`.
 -/
-def optionMove : BiTape Symbol → Option Dir → BiTape Symbol
+def optionMove : BiTape Symbol → Option Turing.Dir → BiTape Symbol
   | t, none => t
   | t, some d => t.move d
 
@@ -138,11 +140,11 @@ lemma spaceUsed_mk₁ (l : List Symbol) :
   | nil => simp [mk₁, spaceUsed, nil, StackTape.length_nil]
   | cons h t => simp [mk₁, spaceUsed, StackTape.length_nil, StackTape.length_mapSome]; omega
 
-lemma spaceUsed_move (t : BiTape Symbol) (d : Dir) :
+lemma spaceUsed_move (t : BiTape Symbol) (d : Turing.Dir) :
     (t.move d).spaceUsed ≤ t.spaceUsed + 1 := by
   cases d <;> grind [moveLeft, moveRight, move,
     spaceUsed, StackTape.length_tail_le, StackTape.length_cons_le]
 
 end BiTape
 
-end Turing
+end Cslib.Turing

Cslib/Foundations/Data/StackTape.lean

@@ -38,15 +38,15 @@ advantages and disadvantages.
 
 @[expose] public section
 
-namespace Turing
+namespace Cslib.Turing
 
 /--
 An infinite tape representation using a list of `Option` values,
 where the list is eventually `none`.
 
 Represented as a `List (Option Symbol)` that does not end with `none`.
 -/
-structure StackTape (Symbol : Type) where
+structure StackTape (Symbol : Type*) where
   /-- The underlying list representation -/
   toList : List (Option Symbol)
   /--
@@ -59,7 +59,7 @@ attribute [scoped grind! .] StackTape.toList_getLast?_ne_some_none
 
 namespace StackTape
 
-variable {Symbol : Type}
+variable {Symbol : Type*}
 
 /-- The empty `StackTape` -/
 @[scoped grind]
@@ -178,4 +178,4 @@ end Length
 
 end StackTape
 
-end Turing
+end Cslib.Turing