From 6124de0d374015ab17773ca1709e1f5fe39c8cbc Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 25 Jun 2026 18:56:31 +0200 Subject: [PATCH 1/2] 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 Date: Fri, 26 Jun 2026 13:28:05 +0200 Subject: [PATCH 2/2] 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