From 6124de0d374015ab17773ca1709e1f5fe39c8cbc Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Thu, 25 Jun 2026 18:56:31 +0200
Subject: [PATCH 1/4] Add NTMs

---
 Cslib.lean                                    |  2 +
 .../Machines/Turing/SingleTape/Defs.lean      | 52 +++++++++++++++
 .../Turing/SingleTape/NonDeterministic.lean   | 65 +++++++++++++++++++
 3 files changed, 119 insertions(+)
 create mode 100644 Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
 create mode 100644 Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean

diff --git a/Cslib.lean b/Cslib.lean
index 8932852ba..3990d0ef7 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -34,7 +34,9 @@ public import Cslib.Computability.Languages.MyhillNerode
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+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
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
new file mode 100644
index 000000000..240f09946
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
@@ -0,0 +1,52 @@
+/-
+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. -/
+inductive TrLabel (Symbol : Type*)
+  /-- Read `x` from the tape. -/
+  | read (x : Symbol)
+  /-- Write `x` on the tape. -/
+  | write (x : Symbol)
+  /-- Move the head of the tape. -/
+  | move (d : Turing.Dir)
+  /-- Do nothing. -/
+  | skip
+
+/-- Applies a transition label to a tape, returning `none` if it is not possible. -/
+def TrLabel.applyToTape [DecidableEq Symbol] (μ : TrLabel Symbol) (tape : Turing.BiTape Symbol) :
+    Option (Turing.BiTape Symbol) :=
+  match μ with
+  | read x => if x = tape.head then some tape else none
+  | write x => some (tape.write x)
+  | move d => some (tape.move d)
+  | skip => some tape
+
+/-- 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
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
new file mode 100644
index 000000000..0f764245f
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
@@ -0,0 +1,65 @@
+/-
+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.Relation.Defs
+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 (TrLabel 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*}
+
+namespace SingleTapeNTM
+
+variable [DecidableEq Symbol]
+
+/-- An NTM yields a small-step operational semantics on configurations, which codifies an execution
+step. -/
+def Red (m : SingleTapeNTM State Symbol)
+    (c c' : Cfg State Symbol) : Prop :=
+  ∃ μ, m.Tr c.state μ c'.state ∧ μ.applyToTape c.tape = c'.tape
+
+@[scoped grind =]
+theorem red_tr {m : SingleTapeNTM State Symbol} :
+    m.Red c c' ↔ ∃ μ, m.Tr c.state μ c'.state ∧ μ.applyToTape c.tape = c'.tape := by rfl
+
+/-- Multistep execution of an NTM, defined as the reflexive and transitive closure of one-step
+execution.
+-/
+@[scoped grind =]
+def 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 SingleTapeNTM
+
+end Cslib.Computability.Turing.SingleTape

From 80ca24eefe0b89516a6ae465e5b06bf1a457fec8 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 26 Jun 2026 13:28:05 +0200
Subject: [PATCH 2/4] Add mtr characterisation and transducer

---
 .../Machines/Turing/SingleTape/Defs.lean      | 30 +++++++++---
 .../Turing/SingleTape/NonDeterministic.lean   | 49 ++++++++++++++++++-
 2 files changed, 70 insertions(+), 9 deletions(-)

diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
index 240f09946..5cac8d41b 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
@@ -25,16 +25,32 @@ inductive TrLabel (Symbol : Type*)
   /-- Do nothing. -/
   | skip
 
-/-- Applies a transition label to a tape, returning `none` if it is not possible. -/
-def TrLabel.applyToTape [DecidableEq Symbol] (μ : TrLabel Symbol) (tape : Turing.BiTape Symbol) :
+/-- Applies a transition label to a tape, returning `none` if it is not possible.
+The input is taken as an `Option` to make the function composable. -/
+def TrLabel.applyToTape [DecidableEq Symbol]
+    (otape : Option (Turing.BiTape Symbol)) (μ : TrLabel Symbol) :
     Option (Turing.BiTape Symbol) :=
-  match μ with
-  | read x => if x = tape.head then some tape else none
-  | write x => some (tape.write x)
-  | move d => some (tape.move d)
-  | skip => some tape
+  match μ, otape with
+  | read x, some tape => if x = tape.head then some tape else none
+  | write x, some tape => some (tape.write x)
+  | move d, some tape => some (tape.move d)
+  | skip, some tape => some tape
+  | _, _ => none
+
+@[scoped grind →]
+theorem TrLabel.applyToTape_isSome [DecidableEq Symbol] {μ : TrLabel Symbol}
+    {ot : Option (Turing.BiTape Symbol)} (h : (μ.applyToTape ot).isSome) : ot.isSome := by
+  have ⟨t', ht'⟩ := Option.isSome_iff_exists.mp h
+  simp only [applyToTape] at ht'
+  grind [applyToTape]
+
+@[scoped grind →]
+theorem TrLabel.applyToTape_foldl_isSome [DecidableEq Symbol] {μs : List (TrLabel Symbol)}
+    {ot : Option (Turing.BiTape Symbol)} (h : (μs.foldl applyToTape ot).isSome) : ot.isSome := by
+  induction μs generalizing ot <;> grind
 
 /-- Configuration of a single-tape Turing machine. -/
+@[ext]
 structure Cfg (State Symbol : Type*) where
   /-- The state that the machine is in. -/
   state : State
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
index 0f764245f..0a21bd9ec 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Relation.Defs
 public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 
@@ -51,15 +52,59 @@ theorem red_tr {m : SingleTapeNTM State Symbol} :
 /-- Multistep execution of an NTM, defined as the reflexive and transitive closure of one-step
 execution.
 -/
-@[scoped grind =]
 def MRed (m : SingleTapeNTM State Symbol) := Relation.ReflTransGen m.Red
 
+open scoped LTS LTS.MTr TrLabel
+
+/-- Characterisation of executions in terms of multistep transitions. -/
+@[scoped grind =]
+theorem mRed_mTr {m : SingleTapeNTM State Symbol} :
+    m.MRed c c' ↔ ∃ μs, m.MTr c.state μs c'.state ∧
+    μs.foldl TrLabel.applyToTape (some c.tape) = c'.tape := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    induction h using Relation.ReflTransGen.head_induction_on
+    case refl =>
+      exists []
+      grind
+    case head _ c cb hred hmred ih =>
+      rcases ih with ⟨μs, hmtr, ih⟩
+      have ⟨μ, _⟩ := red_tr.mp hred
+      exists μ :: μs
+      grind
+  case mpr =>
+    rcases h with ⟨μs, hmtr, h⟩
+    induction μs generalizing c
+    case nil =>
+      rw [show c = c' by grind [Cfg.ext]]
+      apply Relation.ReflTransGen.refl
+    case cons μ μs ih =>
+      cases hmtr
+      case stepL sb htr hmtr =>
+        have hat : ∀ (μ : TrLabel Symbol) t, (μ.applyToTape t).isSome → t.isSome := by grind
+        have ⟨tb, htb⟩ : ∃ tb, μ.applyToTape c.tape = some tb := by grind [Option.isSome_iff_exists]
+        let cb := {state := sb, tape := tb : Cfg State Symbol}
+        have hmred : m.MRed cb c' := by grind
+        apply Relation.ReflTransGen.head (b := cb) (by grind)
+        simp only [MRed] at hmred
+        grind
+
 /-- 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'
 
+/-- An NTM is a transducer of finite lists of symbols. -/
+instance : Transducer (SingleTapeNTM State Symbol) Symbol Symbol where
+    Translates (m : SingleTapeNTM State Symbol) (xs ys : List Symbol) :=
+  ∃ s ∈ m.start, ∃ c',
+    c'.state ∈ m.accept ∧
+    m.MRed (Cfg.mk₁ s xs) c' ∧
+    /- The following condition on output deviates from textbooks, in order to have the same
+    criterion as for deterministic TMs. We might want to revisit this in the future.
+    -/
+    c'.tape = Turing.BiTape.mk₁ ys
+
 end SingleTapeNTM
 
 end Cslib.Computability.Turing.SingleTape

From 4292d4d6536abbfe0d608d6dbb4c48266d9a64f9 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Tue, 30 Jun 2026 20:26:16 +0200
Subject: [PATCH 3/4] yields and AcceptsInSteps

---
 .../Turing/SingleTape/NonDeterministic.lean   | 33 ++++++++++++-------
 references.bib                                |  8 +++++
 2 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
index 0a21bd9ec..4af74985d 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
@@ -7,6 +7,7 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Foundations.Relation.Defs
+public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Foundations.Data.BiTape
@@ -16,6 +17,10 @@ public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 
 Nondeterministic Turing Machines (NTMs), defined as nondeterministic automata (`NA`) that act on a
 bidirectional tape (`BiTape`).
+
+## References
+
+* [M. Sipser, *Introduction to Theory of Computation*][Sipser2013]
 -/
 
 @[expose] public section
@@ -40,26 +45,26 @@ namespace SingleTapeNTM
 variable [DecidableEq Symbol]
 
 /-- An NTM yields a small-step operational semantics on configurations, which codifies an execution
-step. -/
-def Red (m : SingleTapeNTM State Symbol)
+step. This formalises the 'yields' relation from [Sipser2013]. -/
+def Yields (m : SingleTapeNTM State Symbol)
     (c c' : Cfg State Symbol) : Prop :=
   ∃ μ, m.Tr c.state μ c'.state ∧ μ.applyToTape c.tape = c'.tape
 
 @[scoped grind =]
-theorem red_tr {m : SingleTapeNTM State Symbol} :
-    m.Red c c' ↔ ∃ μ, m.Tr c.state μ c'.state ∧ μ.applyToTape c.tape = c'.tape := by rfl
+theorem yields_tr {m : SingleTapeNTM State Symbol} :
+    m.Yields c c' ↔ ∃ μ, m.Tr c.state μ c'.state ∧ μ.applyToTape c.tape = c'.tape := by rfl
 
 /-- Multistep execution of an NTM, defined as the reflexive and transitive closure of one-step
 execution.
 -/
-def MRed (m : SingleTapeNTM State Symbol) := Relation.ReflTransGen m.Red
+def MYields (m : SingleTapeNTM State Symbol) := Relation.ReflTransGen m.Yields
 
 open scoped LTS LTS.MTr TrLabel
 
 /-- Characterisation of executions in terms of multistep transitions. -/
 @[scoped grind =]
-theorem mRed_mTr {m : SingleTapeNTM State Symbol} :
-    m.MRed c c' ↔ ∃ μs, m.MTr c.state μs c'.state ∧
+theorem mYields_mTr {m : SingleTapeNTM State Symbol} :
+    m.MYields c c' ↔ ∃ μs, m.MTr c.state μs c'.state ∧
     μs.foldl TrLabel.applyToTape (some c.tape) = c'.tape := by
   apply Iff.intro <;> intro h
   case mp =>
@@ -69,7 +74,7 @@ theorem mRed_mTr {m : SingleTapeNTM State Symbol} :
       grind
     case head _ c cb hred hmred ih =>
       rcases ih with ⟨μs, hmtr, ih⟩
-      have ⟨μ, _⟩ := red_tr.mp hred
+      have ⟨μ, _⟩ := yields_tr.mp hred
       exists μ :: μs
       grind
   case mpr =>
@@ -84,22 +89,26 @@ theorem mRed_mTr {m : SingleTapeNTM State Symbol} :
         have hat : ∀ (μ : TrLabel Symbol) t, (μ.applyToTape t).isSome → t.isSome := by grind
         have ⟨tb, htb⟩ : ∃ tb, μ.applyToTape c.tape = some tb := by grind [Option.isSome_iff_exists]
         let cb := {state := sb, tape := tb : Cfg State Symbol}
-        have hmred : m.MRed cb c' := by grind
+        have hmyields : m.MYields cb c' := by grind
         apply Relation.ReflTransGen.head (b := cb) (by grind)
-        simp only [MRed] at hmred
+        simp only [MYields] at hmyields
         grind
 
 /-- An NTM is an acceptor of finite lists of symbols. -/
 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'
+  ∃ s ∈ m.start, ∃ c', c'.state ∈ m.accept ∧ m.MYields (Cfg.mk₁ s xs) c'
+
+/-- The NTM `m` accepts `xs` in `n` execution steps. -/
+def AcceptsInSteps (m : SingleTapeNTM State Symbol) (n : ℕ) (xs : List Symbol) : Prop :=
+  ∃ s ∈ m.start, ∃ c', c'.state ∈ m.accept ∧ Relation.RelatesInSteps m.Yields (Cfg.mk₁ s xs) c' n
 
 /-- An NTM is a transducer of finite lists of symbols. -/
 instance : Transducer (SingleTapeNTM State Symbol) Symbol Symbol where
     Translates (m : SingleTapeNTM State Symbol) (xs ys : List Symbol) :=
   ∃ s ∈ m.start, ∃ c',
     c'.state ∈ m.accept ∧
-    m.MRed (Cfg.mk₁ s xs) c' ∧
+    m.MYields (Cfg.mk₁ s xs) c' ∧
     /- The following condition on output deviates from textbooks, in order to have the same
     criterion as for deterministic TMs. We might want to revisit this in the future.
     -/
diff --git a/references.bib b/references.bib
index 984dc6e23..18281428d 100644
--- a/references.bib
+++ b/references.bib
@@ -476,3 +476,11 @@ @mastersthesis{Calisto2022
   school       = {Universidade do Minho},
   year         = {2022}
 }
+
+@book{Sipser2013,
+  author    = {Sipser, Michael},
+  title     = {Introduction to the Theory of Computation},
+  edition   = {3rd},
+  publisher = {Cengage Learning},
+  year      = {2013}
+}
\ No newline at end of file

From a74d3e826a923035345cb10453ead44aa53f8102 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Tue, 30 Jun 2026 20:29:54 +0200
Subject: [PATCH 4/4] AcceptsInAtMostSteps

---
 .../Machines/Turing/SingleTape/NonDeterministic.lean        | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
index 4af74985d..ffd15a590 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
@@ -100,9 +100,13 @@ instance : Acceptor (SingleTapeNTM State Symbol) Symbol where
   ∃ s ∈ m.start, ∃ c', c'.state ∈ m.accept ∧ m.MYields (Cfg.mk₁ s xs) c'
 
 /-- The NTM `m` accepts `xs` in `n` execution steps. -/
-def AcceptsInSteps (m : SingleTapeNTM State Symbol) (n : ℕ) (xs : List Symbol) : Prop :=
+def AcceptsInSteps (m : SingleTapeNTM State Symbol) (xs : List Symbol) (n : ℕ) : Prop :=
   ∃ s ∈ m.start, ∃ c', c'.state ∈ m.accept ∧ Relation.RelatesInSteps m.Yields (Cfg.mk₁ s xs) c' n
 
+/-- The NTM `m` accepts `xs` in at most `n` execution steps. -/
+def AcceptsInAtMostSteps (m : SingleTapeNTM State Symbol) (xs : List Symbol) (n : ℕ) : Prop :=
+  ∃ k ≤ n, m.AcceptsInSteps xs k
+
 /-- An NTM is a transducer of finite lists of symbols. -/
 instance : Transducer (SingleTapeNTM State Symbol) Symbol Symbol where
     Translates (m : SingleTapeNTM State Symbol) (xs ys : List Symbol) :=