From d127bd91036ae25543238ac850d3740eb828fa57 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 14 May 2026 14:28:40 +0200 Subject: [PATCH 01/10] TM on NA --- .../SingleTapeTuring/NonDeterministic.lean | 52 +++++++++++++++++++ Cslib/Foundations/Data/BiTape.lean | 2 +- Cslib/Foundations/Data/StackTape.lean | 2 +- 3 files changed, 54 insertions(+), 2 deletions(-) create mode 100644 Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean diff --git a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean b/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean new file mode 100644 index 000000000..fd5e0b6d0 --- /dev/null +++ b/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.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 +-/ + +module + +public import Cslib.Computability.Automata.NA.Basic +public import Cslib.Foundations.Data.BiTape +public import Cslib.Foundations.Semantics.LTS.HasTau + +/-! # Nondeterministic Single-Tape Turing Machines -/ + +@[expose] public section + +namespace Cslib.Computability.Turing + +open Automata Turing + +inductive Direction + | left | right + +-- # Alternative 1: everything is visible and the tape is kept separate from states, +-- a-la reactive turing machines + +structure NA.TM (State Symbol : Type*) [HasTau Symbol] + extends NA State (Symbol × Symbol × Direction) + +structure SingleTapeNDTM (State Symbol : Type*) [HasTau Symbol] where + a : NA.TM State Symbol + tape : Turing.BiTape Symbol + +variable {Symbol} [HasTau Symbol] + +-- Define the effect of a transition on the tape + +-- Define the semantics of a tape under a fixed TM, or a relation between TMs where the `a` remains +-- unaltered. + +-- # Alternative 2: states contain the tape, transitions are labelled by the symbol being read + +namespace Alternative2 + +open Automata Turing + +structure NA.TM (State Symbol : Type*) [HasTau Symbol] + extends NA (State × Turing.BiTape Symbol) Symbol + +end Alternative2 + +end Cslib.Computability.Turing diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index ba7160556..ab1645d55 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -44,7 +44,7 @@ namespace 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 -/ diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index f495d897a..b196e228f 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -46,7 +46,7 @@ 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) /-- From 85c2b86e480edb1c481a78406ef941cfdb928687 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sat, 16 May 2026 14:21:28 +0200 Subject: [PATCH 02/10] NTM v2 --- .../SingleTapeTuring/NonDeterministic.lean | 52 ++++++++++--------- Cslib/Foundations/Data/BiTape.lean | 2 +- Cslib/Foundations/Data/StackTape.lean | 2 +- 3 files changed, 30 insertions(+), 26 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean b/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean index fd5e0b6d0..a3aa90e54 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean @@ -14,39 +14,43 @@ public import Cslib.Foundations.Semantics.LTS.HasTau @[expose] public section -namespace Cslib.Computability.Turing +namespace Cslib.Computability.Turing.NTM open Automata Turing -inductive Direction - | left | right +-- inductive Move +-- | stay | left | right --- # Alternative 1: everything is visible and the tape is kept separate from states, --- a-la reactive turing machines +structure Controller.TrLabel (State Symbol : Type*) where + read : Option Symbol + write : Option Symbol + move : Option Turing.Dir -- Might wanna use a larger inductive here (see Move) -structure NA.TM (State Symbol : Type*) [HasTau Symbol] - extends NA State (Symbol × Symbol × Direction) +structure Controller (State Symbol : Type*) + extends NA State (Controller.TrLabel State Symbol) -structure SingleTapeNDTM (State Symbol : Type*) [HasTau Symbol] where - a : NA.TM State Symbol +structure Cfg (State Symbol : Type*) where + state : State tape : Turing.BiTape Symbol -variable {Symbol} [HasTau Symbol] +structure SingleTapeNTM (State Symbol : Type*) where + /-- The controller automaton of the machine. -/ + controller : Controller State Symbol + /-- The set of accepting (halting) states. -/ + accept : Set State --- Define the effect of a transition on the tape +-- Transition relation for configurations +-- Due to the way BiTape is written, Symbol cannot be universe-polymorphic. To be fixed. +def SingleTapeNTM.Tr {Symbol} (m : SingleTapeNTM State Symbol) + (c c' : Cfg State Symbol) : Prop := + c.state ∉ m.accept ∧ + ∃ μ, m.controller.Tr c.state μ c'.state ∧ + μ.read = c.tape.head ∧ c'.tape = (c.tape.write μ.write).optionMove μ.move --- Define the semantics of a tape under a fixed TM, or a relation between TMs where the `a` remains --- unaltered. +def SingleTapeNTM.MTr {Symbol} (m : SingleTapeNTM State Symbol) := Relation.ReflTransGen m.Tr --- # Alternative 2: states contain the tape, transitions are labelled by the symbol being read +def SingleTapeNTM.Accepts {Symbol} (m : SingleTapeNTM State Symbol) + (xs : List Symbol) : Prop := + ∃ s ∈ m.controller.start, ∃ c', m.MTr (Cfg.mk s (Turing.BiTape.mk₁ xs)) c' -namespace Alternative2 - -open Automata Turing - -structure NA.TM (State Symbol : Type*) [HasTau Symbol] - extends NA (State × Turing.BiTape Symbol) Symbol - -end Alternative2 - -end Cslib.Computability.Turing +end Cslib.Computability.Turing.NTM diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index ab1645d55..8cfbe8157 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -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, ∅, ∅⟩ diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index b196e228f..a662b3574 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -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] From ce3adece5abdcd8c0fed49a7c70538e595cdaeb7 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sat, 16 May 2026 18:38:30 +0200 Subject: [PATCH 03/10] NTM from NA --- .../SingleTapeTuring/NonDeterministic.lean | 42 ++++++++++++------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean b/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean index a3aa90e54..61756fe28 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean @@ -10,7 +10,11 @@ public import Cslib.Computability.Automata.NA.Basic public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Semantics.LTS.HasTau -/-! # Nondeterministic Single-Tape Turing Machines -/ +/-! # Nondeterministic Single-Tape Turing Machines + +Nondeterministic Turing Machines (NTMs) defined as the composition of a nondeterministic controller +(an `NA`) with a bidirectional tape (`BiTape`). +-/ @[expose] public section @@ -21,36 +25,46 @@ open Automata Turing -- inductive Move -- | stay | left | right +/-- The transition labels used by a controller. -/ structure Controller.TrLabel (State Symbol : Type*) where - read : Option Symbol + read : Symbol write : Option Symbol move : Option Turing.Dir -- Might wanna use a larger inductive here (see Move) +/-- The automaton that defines the behaviour of an NTM. -/ structure Controller (State Symbol : Type*) - extends NA State (Controller.TrLabel State Symbol) + extends NA State (Controller.TrLabel State Symbol) where +/-- Configuration of a Turing machine. -/ structure Cfg (State Symbol : Type*) where state : State tape : Turing.BiTape Symbol +/-- Single-tape Nondeterministic Turing Machine. -/ structure SingleTapeNTM (State Symbol : Type*) where - /-- The controller automaton of the machine. -/ + /-- The controller of the machine. -/ controller : Controller State Symbol /-- The set of accepting (halting) states. -/ accept : Set State + /-- Proof that all accepting states are halting states. -/ + controller_halts (hmem : s ∈ accept) : ¬∃ μ s', controller.Tr s μ s' --- Transition relation for configurations --- Due to the way BiTape is written, Symbol cannot be universe-polymorphic. To be fixed. -def SingleTapeNTM.Tr {Symbol} (m : SingleTapeNTM State Symbol) +/-- The 'yields' relation, a binary relation on configurations that codifies an execution step. -/ +def SingleTapeNTM.Yields {Symbol} (m : SingleTapeNTM State Symbol) (c c' : Cfg State Symbol) : Prop := - c.state ∉ m.accept ∧ - ∃ μ, m.controller.Tr c.state μ c'.state ∧ - μ.read = c.tape.head ∧ c'.tape = (c.tape.write μ.write).optionMove μ.move + ∃ μ, m.controller.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 -def SingleTapeNTM.MTr {Symbol} (m : SingleTapeNTM State Symbol) := Relation.ReflTransGen m.Tr +/-- The extended 'yields' relation, obtained by closing `Yields` for reflexivity and transitivity. +-/ +def SingleTapeNTM.MYields {Symbol} (m : SingleTapeNTM State Symbol) := + Relation.ReflTransGen m.Yields -def SingleTapeNTM.Accepts {Symbol} (m : SingleTapeNTM State Symbol) - (xs : List Symbol) : Prop := - ∃ s ∈ m.controller.start, ∃ c', m.MTr (Cfg.mk s (Turing.BiTape.mk₁ xs)) c' +/-- An NTM is an acceptor of finite lists of symbols. -/ +@[simp, scoped grind =] +instance {Symbol} : Acceptor (SingleTapeNTM State Symbol) Symbol where + Accepts (m : SingleTapeNTM State Symbol) (xs : List Symbol) := + ∃ s ∈ m.controller.start, ∃ c', m.MYields {state := s, tape := Turing.BiTape.mk₁ xs} c' end Cslib.Computability.Turing.NTM From ab47fad7b65b638dd0cb154b73c08880afe48cca Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 18 May 2026 09:04:07 +0200 Subject: [PATCH 04/10] NTM --- .../SingleTapeTuring/NonDeterministic.lean | 56 +++++++++---------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean b/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean index 61756fe28..9ceb392f2 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean @@ -6,14 +6,15 @@ 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.Foundations.Semantics.LTS.HasTau -/-! # Nondeterministic Single-Tape Turing Machines +/-! # Single-Tape Nondeterministic Turing Machines (NTMs) -Nondeterministic Turing Machines (NTMs) defined as the composition of a nondeterministic controller -(an `NA`) with a bidirectional tape (`BiTape`). +Nondeterministic Turing Machines (NTMs), defined as nondeterministic automata (`NA`) that act on a +bidirectional tape (`BiTape`). -/ @[expose] public section @@ -22,49 +23,48 @@ namespace Cslib.Computability.Turing.NTM open Automata Turing --- inductive Move --- | stay | left | right - /-- The transition labels used by a controller. -/ -structure Controller.TrLabel (State Symbol : Type*) where - read : Symbol +structure SingleTapeNTM.TrLabel (State Symbol : Type*) where + read : Option Symbol write : Option Symbol move : Option Turing.Dir -- Might wanna use a larger inductive here (see Move) -/-- The automaton that defines the behaviour of an NTM. -/ -structure Controller (State Symbol : Type*) - extends NA State (Controller.TrLabel State Symbol) where +/-- 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 (SingleTapeNTM.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' -/-- Configuration of a Turing machine. -/ +/-- Configuration of a single-tape Turing machine. -/ structure Cfg (State Symbol : Type*) where + /-- Current state in the machine's controller. -/ state : State + /-- Current memory of the machine. -/ tape : Turing.BiTape Symbol -/-- Single-tape Nondeterministic Turing Machine. -/ -structure SingleTapeNTM (State Symbol : Type*) where - /-- The controller of the machine. -/ - controller : Controller State Symbol - /-- The set of accepting (halting) states. -/ - accept : Set State - /-- Proof that all accepting states are halting states. -/ - controller_halts (hmem : s ∈ accept) : ¬∃ μ s', controller.Tr s μ s' - -/-- The 'yields' relation, a binary relation on configurations that codifies an execution step. -/ -def SingleTapeNTM.Yields {Symbol} (m : SingleTapeNTM State Symbol) +/-- An NTM yields a small-step operational semantics on configurations, which codifies an execution +step. -/ +@[scoped grind =] +def SingleTapeNTM.Red {Symbol} (m : SingleTapeNTM State Symbol) (c c' : Cfg State Symbol) : Prop := - ∃ μ, m.controller.Tr c.state μ c'.state ∧ -- The controller can perform the move + ∃ μ, 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 -/-- The extended 'yields' relation, obtained by closing `Yields` for reflexivity and transitivity. +/-- Multistep execution of an NTM, defined as the reflexive and transitive closure of one-step +execution. -/ -def SingleTapeNTM.MYields {Symbol} (m : SingleTapeNTM State Symbol) := - Relation.ReflTransGen m.Yields +@[scoped grind =] +def SingleTapeNTM.MRed {Symbol} (m : SingleTapeNTM State Symbol) := + Relation.ReflTransGen m.Red /-- An NTM is an acceptor of finite lists of symbols. -/ @[simp, scoped grind =] instance {Symbol} : Acceptor (SingleTapeNTM State Symbol) Symbol where Accepts (m : SingleTapeNTM State Symbol) (xs : List Symbol) := - ∃ s ∈ m.controller.start, ∃ c', m.MYields {state := s, tape := Turing.BiTape.mk₁ xs} c' + ∃ s ∈ m.start, ∃ c', m.MRed {state := s, tape := Turing.BiTape.mk₁ xs} c' end Cslib.Computability.Turing.NTM From eba89351e91f12f109dc05903f4bf4dfbe4d76e8 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 21 May 2026 14:33:38 +0200 Subject: [PATCH 05/10] OptionDA --- .../Machines/Turing/SingleTape/Defs.lean | 41 +++ .../SingleTape/Deterministic.lean} | 293 ++++++++++-------- .../SingleTape}/NonDeterministic.lean | 29 +- Cslib/Foundations/Data/BiTape.lean | 22 +- Cslib/Foundations/Semantics/LTS/HasTau.lean | 26 ++ 5 files changed, 247 insertions(+), 164 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/SingleTape/Defs.lean rename Cslib/Computability/Machines/{SingleTapeTuring/Basic.lean => Turing/SingleTape/Deterministic.lean} (67%) rename Cslib/Computability/Machines/{SingleTapeTuring => Turing/SingleTape}/NonDeterministic.lean (63%) diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean new file mode 100644 index 000000000..f40cd0e67 --- /dev/null +++ b/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 + +@[expose] public section + +/-! # Basic definitions for Turing Machines (TMs) -/ + +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 diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean similarity index 67% rename from Cslib/Computability/Machines/SingleTapeTuring/Basic.lean rename to Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean index 477ab60b1..9d673037b 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean @@ -1,20 +1,21 @@ /- Copyright (c) 2026 Bolton Bailey. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Bolton Bailey, Pim Spelier, Daan van Gent +Authors: Bolton Bailey, Pim Spelier, Daan van Gent, Fabrizio Montesi -/ module +public import Cslib.Computability.Automata.NA.Basic public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Data.RelatesInSteps public import Mathlib.Algebra.Polynomial.Eval.Defs +public import Cslib.Computability.Machines.Turing.SingleTape.Defs /-! -# Single-Tape Turing Machines +# Single-Tape Deterministic Turing Machines -Defines a single-tape Turing machine for computing functions on `List Symbol` -for finite alphabet `Symbol`. +Defines a single-tape Turing machine for computing functions on `List Symbol`. ## Design @@ -62,147 +63,163 @@ We also provide ways of constructing polynomial-runtime TMs @[expose] public section -open Cslib Relation - -namespace Turing - -open BiTape StackTape - -variable {Symbol : Type} +namespace Cslib.Computability.Turing.SingleTape + +open Cslib Relation Automata Turing.BiTape Turing.StackTape + +-- /-- +-- A single-tape Turing machine +-- over the alphabet of `Option Symbol` (where `none` is the blank `BiTape` symbol). +-- -/ +-- structure SingleTapeTM Symbol [Inhabited Symbol] [Fintype Symbol] where +-- /-- type of state labels -/ +-- (State : Type) +-- /-- finiteness of the state type -/ +-- [stateFintype : Fintype State] +-- /-- Initial state -/ +-- (q₀ : State) +-- /-- Transition function, mapping a state and a head symbol to a `Stmt` to invoke, +-- and optionally the new state to transition to afterwards (`none` for halt) -/ +-- (tr : State → Option Symbol → SingleTapeTM.Stmt Symbol × Option State) + +/-- Single-tape Deterministic Turing Machine (DTM, or just TM for short) over the alphabet of +`Option Symbol` (where `none` is the blank `BiTape` symbol). -/ +structure SingleTapeTM (State Symbol : Type*) + extends LTS State (SingleTape.TrLabel State Symbol) where + [is_deterministic : LTS.Deterministic {Tr := Tr}] + /-- The start state. -/ + start : State + /-- 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' namespace SingleTapeTM -/-- -A Turing machine "statement" is just a `Option`al command to move left or right, -and write a symbol (i.e. an `Option Symbol`, where `none` is the blank symbol) on the `BiTape` --/ -structure Stmt (Symbol : Type) where - /-- The symbol to write at the current head position -/ - symbol : Option Symbol - /-- The direction to move the tape head -/ - movement : Option Dir -deriving Inhabited - -end SingleTapeTM - -/-- -A single-tape Turing machine -over the alphabet of `Option Symbol` (where `none` is the blank `BiTape` symbol). --/ -structure SingleTapeTM Symbol [Inhabited Symbol] [Fintype Symbol] where - /-- type of state labels -/ - (State : Type) - /-- finiteness of the state type -/ - [stateFintype : Fintype State] - /-- Initial state -/ - (q₀ : State) - /-- Transition function, mapping a state and a head symbol to a `Stmt` to invoke, - and optionally the new state to transition to afterwards (`none` for halt) -/ - (tr : State → Option Symbol → SingleTapeTM.Stmt Symbol × Option State) - -namespace SingleTapeTM +variable {State Symbol : Type*} section Cfg -/-! -## Configurations of a Turing Machine - -This section defines the configurations of a Turing machine, -the step function that lets the machine transition from one configuration to the next, -and the intended initial and final configurations. +/-- An NTM yields a small-step operational semantics on configurations, which codifies an execution +step. -/ +@[scoped grind =] +def Red (m : SingleTapeTM 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. -/ - -variable [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) - -instance : Inhabited tm.State := ⟨tm.q₀⟩ - -instance : Fintype tm.State := tm.stateFintype - -instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance +@[scoped grind =] +def MRed (m : SingleTapeTM State Symbol) := Relation.ReflTransGen m.Red /-- -The configurations of a Turing machine consist of: -an `Option`al state (or none for the halting state), -and a `BiTape` representing the tape contents. --/ -structure Cfg : Type where - /-- the state of the TM (or none for the halting state) -/ - state : Option tm.State - /-- the BiTape contents -/ - BiTape : BiTape Symbol -deriving Inhabited - -/-- The step function corresponding to a `SingleTapeTM`. -/ -@[simp] -def step : tm.Cfg → Option tm.Cfg - | ⟨none, _⟩ => - -- If in the halting state, there is no next configuration - none - | ⟨some q', t⟩ => - -- If in state q', perform look up in the transition function - match tm.tr q' t.head with - -- and enter a new configuration with state q'' (or none for halting) - -- and tape updated according to the Stmt - | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩ +The initial configuration of a deterministic Turing Machine, which consists of the start state of +the machine and the input list of symbols. -/-- -The initial configuration corresponding to a list in the input alphabet. Note that the entries of the tape constructed by `BiTape.mk₁` are all `some` values. This is to ensure that distinct lists map to distinct initial configurations. -/ -def initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨some tm.q₀, BiTape.mk₁ s⟩ - -/-- The final configuration corresponding to a list in the output alphabet. -(We demand that the head halts at the leftmost position of the output.) --/ -def haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨none, BiTape.mk₁ s⟩ - -/-- -The space used by a configuration is the space used by its tape. --/ -def Cfg.space_used (tm : SingleTapeTM Symbol) (cfg : tm.Cfg) : ℕ := cfg.BiTape.space_used +def initCfg (m : SingleTapeTM State Symbol) (xs : List Symbol) : Cfg State Symbol := + Cfg.mk₁ m.start xs + +/-- A TM is an acceptor of finite lists of symbols. -/ +@[simp, scoped grind =] +instance : Acceptor (SingleTapeTM State Symbol) Symbol where + Accepts (m : SingleTapeTM State Symbol) (xs : List Symbol) := + ∃ c', c'.state ∈ m.accept ∧ m.MRed (m.initCfg xs) c' + +-- /-! +-- ## Configurations of a Turing Machine + +-- This section defines the configurations of a Turing machine, +-- the step function that lets the machine transition from one configuration to the next, +-- and the intended initial and final configurations. +-- -/ + +-- variable [Inhabited Symbol] [Fintype Symbol] (m : SingleTapeTM State Symbol) + +-- instance : Inhabited tm.State := ⟨tm.q₀⟩ + +-- instance : Fintype tm.State := tm.stateFintype + +-- instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance + +-- /-- +-- The configurations of a Turing machine consist of: +-- an `Option`al state (or none for the halting state), +-- and a `BiTape` representing the tape contents. +-- -/ +-- structure Cfg : Type where +-- /-- the state of the TM (or none for the halting state) -/ +-- state : Option tm.State +-- /-- the BiTape contents -/ +-- BiTape : BiTape Symbol +-- deriving Inhabited + +-- /-- The step function corresponding to a `SingleTapeTM`. -/ +-- @[simp] +-- def step : tm.Cfg → Option tm.Cfg +-- | ⟨none, _⟩ => +-- -- If in the halting state, there is no next configuration +-- none +-- | ⟨some q', t⟩ => +-- -- If in state q', perform look up in the transition function +-- match tm.tr q' t.head with +-- -- and enter a new configuration with state q'' (or none for halting) +-- -- and tape updated according to the Stmt +-- | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩ + + + +-- /-- The final configuration corresponding to a list in the output alphabet. +-- (We demand that the head halts at the leftmost position of the output.) +-- -/ +-- def haltCfg (m : SingleTapeTM State Symbol) (xs : List Symbol) : Cfg State Symbol := +-- ⟨none, Turing.BiTape.mk₁ xs⟩ @[scoped grind =] -lemma Cfg.space_used_initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : - (tm.initCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s - -@[scoped grind =] -lemma Cfg.space_used_haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : - (tm.haltCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s - -lemma Cfg.space_used_step {tm : SingleTapeTM Symbol} (cfg cfg' : tm.Cfg) - (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by - obtain ⟨_ | q, tape⟩ := cfg - · simp [step] at hstep - · simp only [step] at hstep - generalize hM : tm.tr q tape.head = result at hstep - obtain ⟨⟨wr, dir⟩, q''⟩ := result - cases hstep; cases dir with - | none => simp [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] - | some d => simpa [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] using - BiTape.space_used_move (tape.write wr) d +lemma spaceUsed_initCfg (m : SingleTapeTM State Symbol) (xs : List Symbol) : + (m.initCfg xs).spaceUsed = max 1 xs.length := Turing.BiTape.spaceUsed_mk₁ xs + +-- @[scoped grind =] +-- lemma Cfg.spaceUsed_haltCfg (m : SingleTapeTM State Symbol) (xs : List Symbol) : +-- (m.haltCfg s).spaceUsed = max 1 xs.length := Turing.BiTape.spaceUsed_mk₁ xs + +lemma spaceUsed_red {m : SingleTapeTM State Symbol} (c c' : Cfg State Symbol) + (hstep : m.Red c c') : c'.spaceUsed ≤ c.spaceUsed + 1 := by + rcases hstep with ⟨μ, hstep₁, hstep₂, hstep₃⟩ + rcases c' with ⟨s', tape'⟩ + simp only at hstep₁ hstep₂ hstep₃ + cases hm : μ.move with + | none => grind [write, optionMove, = Cfg.spaceUsed] + | some dir => + simpa [hstep₃, Cfg.spaceUsed, Turing.BiTape.optionMove, Turing.BiTape.spaceUsed_write, hm] using + Turing.BiTape.spaceUsed_move (c.tape.write μ.write) dir end Cfg open Cfg -variable [Inhabited Symbol] [Fintype Symbol] +-- variable [Inhabited Symbol] [Fintype Symbol] -/-- -The `TransitionRelation` corresponding to a `SingleTapeTM Symbol` -is defined by the `step` function, -which maps a configuration to its next configuration, if it exists. --/ -@[scoped grind =] -def TransitionRelation (tm : SingleTapeTM Symbol) (c₁ c₂ : tm.Cfg) : Prop := tm.step c₁ = some c₂ +-- /-- +-- The `TransitionRelation` corresponding to a `SingleTapeTM Symbol` +-- is defined by the `step` function, +-- which maps a configuration to its next configuration, if it exists. +-- -/ +-- @[scoped grind =] +-- def TransitionRelation (m : SingleTapeTM State Symbol) (c₁ c₂ : tm.Cfg) : Prop := tm.step c₁ = some c₂ /-- A proof of `tm` outputting `l'` on input `l`. -/ -def Outputs (tm : SingleTapeTM Symbol) (l l' : List Symbol) : Prop := - ReflTransGen tm.TransitionRelation (initCfg tm l) (haltCfg tm l') +def Outputs (m : SingleTapeTM State Symbol) (l l' : List Symbol) : Prop := + ∃ s ∈ m.accept, m.MRed (initCfg m l) (Cfg.mk₁ s l') -/-- A proof of `tm` outputting `l'` on input `l` in at most `m` steps. -/ -def OutputsWithinTime (tm : SingleTapeTM Symbol) (l l' : List Symbol) (m : ℕ) := - RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (haltCfg tm l') m +/-- A proof of `tm` outputting `l'` on input `l` in at most `n` steps. -/ +def OutputsWithinTime (m : SingleTapeTM State Symbol) (l l' : List Symbol) (n : ℕ) := + ∃ s ∈ m.accept, RelatesWithinSteps m.Red (initCfg m l) (Cfg.mk₁ s l') n /-- This lemma bounds the size blow-up of the output of a Turing machine. @@ -211,20 +228,30 @@ This is important for guaranteeing that composition of polynomial time Turing ma remains polynomial time, as the input to the second machine is bounded by the output length of the first machine. -/ -lemma output_length_le_input_length_add_time (tm : SingleTapeTM Symbol) (l l' : List Symbol) (t : ℕ) - (h : tm.OutputsWithinTime l l' t) : +lemma output_length_le_input_length_add_time (m : SingleTapeTM State Symbol) (l l' : List Symbol) (t : ℕ) + (h : m.OutputsWithinTime l l' t) : l'.length ≤ max 1 l.length + t := by - obtain ⟨steps, hsteps_le, hevals⟩ := h - grind [hevals.apply_le_apply_add (Cfg.space_used tm) - fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)] + obtain ⟨s, hs, steps, hsteps_le, hevals⟩ := h + + -- have := fun a b hstep ↦ spaceUsed_red a b hevals + grind [fun a b hstep ↦ Cfg.spaceUsed_step a b (Option.mem_def.mp hstep)] + grind [hevals.apply_le_apply_add (Cfg.spaceUsed m) + fun a b hstep ↦ Cfg.spaceUsed_step a b (Option.mem_def.mp hstep)] section Computers +inductive id.IdState +| read | accept | reject + /-- A Turing machine computing the identity. -/ -def idComputer : SingleTapeTM Symbol where - State := PUnit - q₀ := PUnit.unit - tr _ b := ⟨⟨b, none⟩, none⟩ +def id : SingleTapeTM id.IdState Symbol where + start := .read + tr s μ := match s, μ with + | .read, ⟨some x, none, some .right⟩ => .read + | .read, ⟨none, none, none⟩ => .accept + | _, _ => .reject + -- accept + -- tr _ b := ⟨⟨b, none⟩, none⟩ /-- A Turing machine computing the composition of two other Turing machines. @@ -233,7 +260,7 @@ If f and g are computed by Turing machines `tm1` and `tm2` then we can construct a Turing machine which computes g ∘ f by first running `tm1` and then, when `tm1` halts, transitioning to the start state of `tm2` and running `tm2`. -/ -def compComputer (tm1 tm2 : SingleTapeTM Symbol) : SingleTapeTM Symbol where +def comp (tm1 tm2 : SingleTapeTM Symbol) : SingleTapeTM Symbol where -- The states of the composed machine are the disjoint union of the states of the input machines. State := tm1.State ⊕ tm2.State -- The start state is the start state of the first input machine. @@ -390,7 +417,7 @@ variable [Inhabited Symbol] [Fintype Symbol] a proof it outputs `f` in at most `time(input.length)` steps. -/ structure TimeComputable (f : List Symbol → List Symbol) where /-- the underlying bundled SingleTapeTM -/ - tm : SingleTapeTM Symbol + m : SingleTapeTM State Symbol /-- a bound on runtime -/ time_bound : ℕ → ℕ /-- proof this machine outputs `f` in at most `time_bound(input.length)` steps -/ @@ -507,4 +534,4 @@ end PolyTimeComputable end SingleTapeTM -end Turing +end Cslib.Computability.Turing.SingleTape diff --git a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean similarity index 63% rename from Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean rename to Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean index 9ceb392f2..3e70794ea 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/NonDeterministic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean @@ -9,7 +9,7 @@ module public import Cslib.Foundations.Data.Relation public import Cslib.Computability.Automata.NA.Basic public import Cslib.Foundations.Data.BiTape -public import Cslib.Foundations.Semantics.LTS.HasTau +public import Cslib.Computability.Machines.Turing.SingleTape.Defs /-! # Single-Tape Nondeterministic Turing Machines (NTMs) @@ -19,36 +19,25 @@ bidirectional tape (`BiTape`). @[expose] public section -namespace Cslib.Computability.Turing.NTM +namespace Cslib.Computability.Turing.SingleTape open Automata Turing -/-- The transition labels used by a controller. -/ -structure SingleTapeNTM.TrLabel (State Symbol : Type*) where - read : Option Symbol - write : Option Symbol - move : Option Turing.Dir -- Might wanna use a larger inductive here (see Move) - /-- 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 (SingleTapeNTM.TrLabel State Symbol) where + 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' -/-- Configuration of a single-tape Turing machine. -/ -structure Cfg (State Symbol : Type*) where - /-- Current state in the machine's controller. -/ - state : State - /-- Current memory of the machine. -/ - tape : Turing.BiTape Symbol +variable {State Symbol : Type*} /-- An NTM yields a small-step operational semantics on configurations, which codifies an execution step. -/ @[scoped grind =] -def SingleTapeNTM.Red {Symbol} (m : SingleTapeNTM State Symbol) +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 @@ -58,13 +47,13 @@ def SingleTapeNTM.Red {Symbol} (m : SingleTapeNTM State Symbol) execution. -/ @[scoped grind =] -def SingleTapeNTM.MRed {Symbol} (m : SingleTapeNTM State Symbol) := +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 {Symbol} : Acceptor (SingleTapeNTM State Symbol) Symbol where +instance : Acceptor (SingleTapeNTM State Symbol) Symbol where Accepts (m : SingleTapeNTM State Symbol) (xs : List Symbol) := - ∃ s ∈ m.start, ∃ c', m.MRed {state := s, tape := Turing.BiTape.mk₁ xs} c' + ∃ s ∈ m.start, ∃ c', c'.state ∈ m.accept ∧ m.MRed (Cfg.mk₁ s xs) c' -end Cslib.Computability.Turing.NTM +end Cslib.Computability.Turing.SingleTape diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 8cfbe8157..ae368147d 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -33,7 +33,7 @@ will not collide. * `BiTape`: A tape with a head symbol and left/right contents stored as `StackTape` * `BiTape.move`: Move the tape head left or right * `BiTape.write`: Write a symbol at the current head position -* `BiTape.space_used`: The space used by the tape +* `BiTape.spaceUsed`: The space used by the tape -/ @[expose] public section @@ -126,22 +126,22 @@ The space used by a `BiTape` is the number of symbols between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`. -/ @[scoped grind] -def space_used (t : BiTape Symbol) : ℕ := 1 + t.left.length + t.right.length +def spaceUsed (t : BiTape Symbol) : ℕ := 1 + t.left.length + t.right.length @[simp, grind =] -lemma space_used_write (t : BiTape Symbol) (a : Option Symbol) : - (t.write a).space_used = t.space_used := by rfl +lemma spaceUsed_write (t : BiTape Symbol) (a : Option Symbol) : + (t.write a).spaceUsed = t.spaceUsed := by rfl -lemma space_used_mk₁ (l : List Symbol) : - (mk₁ l).space_used = max 1 l.length := by +lemma spaceUsed_mk₁ (l : List Symbol) : + (mk₁ l).spaceUsed = max 1 l.length := by cases l with - | nil => simp [mk₁, space_used, nil, StackTape.length_nil] - | cons h t => simp [mk₁, space_used, StackTape.length_nil, StackTape.length_map_some]; omega + | nil => simp [mk₁, spaceUsed, nil, StackTape.length_nil] + | cons h t => simp [mk₁, spaceUsed, StackTape.length_nil, StackTape.length_map_some]; omega -lemma space_used_move (t : BiTape Symbol) (d : Dir) : - (t.move d).space_used ≤ t.space_used + 1 := by +lemma spaceUsed_move (t : BiTape Symbol) (d : Dir) : + (t.move d).spaceUsed ≤ t.spaceUsed + 1 := by cases d <;> grind [move_left, move_right, move, - space_used, StackTape.length_tail_le, StackTape.length_cons_le] + spaceUsed, StackTape.length_tail_le, StackTape.length_cons_le] end BiTape diff --git a/Cslib/Foundations/Semantics/LTS/HasTau.lean b/Cslib/Foundations/Semantics/LTS/HasTau.lean index 9deb34d44..d315ae77c 100644 --- a/Cslib/Foundations/Semantics/LTS/HasTau.lean +++ b/Cslib/Foundations/Semantics/LTS/HasTau.lean @@ -128,11 +128,37 @@ theorem saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label theorem mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) : s ∈ lts.saturate.image s HasTau.τ := STr.refl +/-- `setImage` on `HasTau.τ` preserves membership. -/ +@[scoped grind .] +lemma mem_saturate_setImage_τ [HasTau Label] (lts : LTS State Label) (h : s ∈ S) : + s ∈ lts.saturate.setImage S HasTau.τ := by + simp only [setImage, Set.mem_iUnion, exists_prop] + exists s + grind + +/-- Monotonicity of `setImage` on `HasTau.τ`. -/ +@[scoped grind .] +lemma subset_saturate_setImage_τ [HasTau Label] (lts : LTS State Label) : + S ⊆ lts.saturate.setImage S HasTau.τ := by + simp only [Subset, LE.le, Set.Subset, setImage, Set.mem_iUnion, exists_prop] + intro s h + grind + /-- The `τ`-closure of a set of states `S` is the set of states reachable by any state in `S` by performing only `τ`-transitions. -/ def τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State := lts.saturate.setImage S HasTau.τ +/-- `τClosure` preserves membership. -/ +@[scoped grind .] +lemma τClosure_mem [HasTau Label] (lts : LTS State Label) (h : s ∈ S) : + s ∈ lts.τClosure S := by grind [= τClosure] + +/-- Monotonicity of `setImage` on `HasTau.τ`. -/ +@[scoped grind .] +lemma τClosure_subset [HasTau Label] (lts : LTS State Label) : + S ⊆ lts.τClosure S := by grind + end LTS end Cslib From f7e8d847feb09b02776646e5de440233336e58c6 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 21 May 2026 14:35:05 +0200 Subject: [PATCH 06/10] OptionDA take 2 --- Cslib/Computability/Automata/DA/OptionDA.lean | 167 ++++++++++++++++++ 1 file changed, 167 insertions(+) create mode 100644 Cslib/Computability/Automata/DA/OptionDA.lean diff --git a/Cslib/Computability/Automata/DA/OptionDA.lean b/Cslib/Computability/Automata/DA/OptionDA.lean new file mode 100644 index 000000000..12b6c92da --- /dev/null +++ b/Cslib/Computability/Automata/DA/OptionDA.lean @@ -0,0 +1,167 @@ +/- +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.Computability.Automata.DA.Basic +public import Cslib.Computability.Automata.EpsilonNA.Basic +public import Cslib.Computability.Automata.EpsilonNA.ToNA +public import Cslib.Computability.Automata.NA.ToDA + +/-! # OptionDA: DA with a single halting accept state + +An `OptionDA` is a deterministic automaton with a unique accepting and halting state, codified as +`none : Option State`. Any `DA.FinAcc` can be converted into an `OptionDA` by (i) adding an +ε-transition from every accepting state to the `none` halting state, and then (ii) by transforming +the resulting `εNA` into an `OptionDA`. +-/ + +@[expose] public section + +namespace Cslib.Automata + +/-- A deterministic automaton with a single accepting, halting state, modelled as the `none` value +of `Option Symbol`. -/ +structure OptionDA (State Symbol : Type*) where + /-- The transition function of the automaton. -/ + tr : State → Symbol → Option State + /-- The initial state of the automaton. -/ + start : State + +variable {State Symbol : Type*} + +namespace OptionDA + +/-- Multistep transition function. -/ +def mtr (a : OptionDA State Symbol) : State → List Symbol → Option State + | s, [] => s + | s, x :: xs => a.tr s x >>= (a.mtr · xs) + +/-- An `OptionDA` accepts a string if its multistep transition function maps the start state and +the string to an accept state. + +This is the standard string recognition performed by DFAs in the literature. -/ +@[simp, scoped grind =] +instance : Acceptor (OptionDA State Symbol) Symbol where + Accepts (a : OptionDA State Symbol) (xs : List Symbol) := a.mtr a.start xs = .none + +end OptionDA + +/-- Converts a `DA.FinAcc` into an `εNA` with an additional `none` state that acts as the unique +accepting and halting state. Every accepting state of the original automaton gains an ε-transition +to `none`, and all other transitions are lifted by `some`. -/ +@[scoped grind =] +def DA.FinAcc.toOptionεNA (a : DA.FinAcc State Symbol) : εNA.FinAcc (Option State) Symbol where + start := {some a.start} + accept := {none} + Tr + -- Lift of original transitions + | some s, some x, some s' => s' = a.tr s x + -- Additional ε-transitions to the halting state. + | some s, none, none => s ∈ a.accept + | _, _, _ => False + +/-- The `none` state in `DA.toOptionεNA` is the only accept state. -/ +@[simp] +lemma DA.FinAcc.toOptionεNA_none_accept (a : DA.FinAcc State Symbol) : + a.toOptionεNA.accept = {none} := rfl + +/-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ +@[scoped grind .] +lemma DA.FinAcc.toOptionεNA_none_tr (a : DA.FinAcc State Symbol) + (μ : Option Symbol) (s : Option State) : ¬a.toOptionεNA.Tr none μ s := by grind + +/-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ +@[scoped grind .] +lemma DA.FinAcc.toOptionεNA_tr_none_iff {a : DA.FinAcc State Symbol} + (h : a.toOptionεNA.Tr s μ s') : μ = none ↔ s' = none := by cases hμ : μ <;> grind + +/-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ +@[scoped grind .] +lemma DA.FinAcc.toOptionεNA_ε_τSTr_none {a : DA.FinAcc State Symbol} + (h : a.toOptionεNA.τSTr s s') : s' = s ∨ s' = none := by + cases h with + | refl => simp + | tail s₁ h => + apply toOptionεNA_tr_none_iff at h + simp only [HasTau.τ, true_iff] at h + simp [h] + +/-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ +@[scoped grind .] +lemma DA.FinAcc.toOptionεNA_ε_sTr_none {a : DA.FinAcc State Symbol} + (h : a.toOptionεNA.STr s none s') : s' = s ∨ s' = none := by cases h <;> grind + +lemma DA.FinAcc.toOptionεNA_start_εClosure {a : DA.FinAcc State Symbol} (h : a.start ∈ a.accept) : + a.toOptionεNA.εClosure a.toOptionεNA.start = {some a.start, none} := by + rw [show a.toOptionεNA.start = {some a.start} by rfl] + simp [εNA.εClosure, LTS.τClosure, LTS.saturate, LTS.setImage, LTS.image, HasTau.τ] + ext s + apply Iff.intro <;> intro h + · grind + · simp only [Set.mem_setOf_eq] + simp at h + cases h with + | inl h' => + rw [h'] + apply LTS.STr.refl + | inr h' => + rw [h'] + simp [toOptionεNA] + sorry + +open Acceptor in +open scoped LTS εNA εNA.FinAcc in +/-- `DA.toOptionεNA` preserves the automaton's language. -/ +theorem DA.FinAcc.toOptionεNA_language_eq {a : DA.FinAcc State Symbol} : + language a.toOptionεNA = language a := by + ext xs + simp only [Acceptor.mem_language] + simp only [Accepts] + apply Iff.intro <;> intro h + case mp => + sorry + case mpr => + induction xs + case nil => + exists a.start + apply And.intro + case left => + grind + case right => + + sorry + case cons x xs => + sorry + +namespace NA.FinAcc + +def ofOptionFinAcc (a : NA.FinAcc (Option State) Symbol) : NA.FinAcc State Symbol where + start := { s | some s ∈ a.start } + Tr s x s' := a.Tr (some s) x (some s') + accept := { s | ∃ x, a.Tr (some s) x none } + +noncomputable def toOptionDA (a : NA.FinAcc State Symbol) : OptionDA (Set State) Symbol := + let da := a.toDAFinAcc + { start := da.start + tr S x := + let S' := da.tr S x + open Classical in if S' ∈ da.accept then none else some S' } + +end NA.FinAcc + +noncomputable def DA.FinAcc.toOptionDA (a : DA.FinAcc State Symbol) : + OptionDA (Set State) Symbol := + a.toOptionεNA.toNAFinAcc.ofOptionFinAcc.toOptionDA + +open Acceptor in +-- open scoped NA.FinAcc in +theorem DA.FinAcc.toOptionDA_language_eq {a : DA.FinAcc State Symbol} : + language a.toOptionDA = language a := by + simp [toOptionDA] + sorry + +end Cslib.Automata From 2ba81ef67bb0fdb1e2896d46d9d8202fc8149722 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 27 May 2026 19:24:34 +0200 Subject: [PATCH 07/10] some progress --- Cslib/Computability/Automata/DA/OptionDA.lean | 38 ++++++-- .../Automata/EpsilonNA/Basic.lean | 5 +- .../Automata/EpsilonNA/ToNA.lean | 78 ++++++++++++++-- Cslib/Foundations/Semantics/LTS/HasTau.lean | 90 ++++++++++++++++--- 4 files changed, 178 insertions(+), 33 deletions(-) diff --git a/Cslib/Computability/Automata/DA/OptionDA.lean b/Cslib/Computability/Automata/DA/OptionDA.lean index 12b6c92da..f7d0bd3bb 100644 --- a/Cslib/Computability/Automata/DA/OptionDA.lean +++ b/Cslib/Computability/Automata/DA/OptionDA.lean @@ -95,26 +95,30 @@ lemma DA.FinAcc.toOptionεNA_ε_τSTr_none {a : DA.FinAcc State Symbol} lemma DA.FinAcc.toOptionεNA_ε_sTr_none {a : DA.FinAcc State Symbol} (h : a.toOptionεNA.STr s none s') : s' = s ∨ s' = none := by cases h <;> grind +open scoped LTS εNA εNA.FinAcc + +/-- The ε-closure of the start state in `DA.toOptionεNA` consists of the start state and `none`. -/ +@[scoped grind =] lemma DA.FinAcc.toOptionεNA_start_εClosure {a : DA.FinAcc State Symbol} (h : a.start ∈ a.accept) : a.toOptionεNA.εClosure a.toOptionεNA.start = {some a.start, none} := by rw [show a.toOptionεNA.start = {some a.start} by rfl] - simp [εNA.εClosure, LTS.τClosure, LTS.saturate, LTS.setImage, LTS.image, HasTau.τ] + simp only [εNA.εClosure, LTS.τClosure, LTS.setImage, Set.mem_singleton_iff, LTS.image, + LTS.saturate, HasTau.τ, Set.iUnion_iUnion_eq_left] ext s - apply Iff.intro <;> intro h + apply Iff.intro <;> intro h' · grind · simp only [Set.mem_setOf_eq] - simp at h - cases h with + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at h' + cases h' with | inl h' => rw [h'] apply LTS.STr.refl | inr h' => rw [h'] - simp [toOptionεNA] - sorry + have htr : a.toOptionεNA.Tr (some a.start) none none := by grind + exact LTS.STr.single htr open Acceptor in -open scoped LTS εNA εNA.FinAcc in /-- `DA.toOptionεNA` preserves the automaton's language. -/ theorem DA.FinAcc.toOptionεNA_language_eq {a : DA.FinAcc State Symbol} : language a.toOptionεNA = language a := by @@ -129,10 +133,26 @@ theorem DA.FinAcc.toOptionεNA_language_eq {a : DA.FinAcc State Symbol} : case nil => exists a.start apply And.intro - case left => - grind + case left => grind case right => + have h' : a.start ∈ a.accept := by grind [FLTS.mtr] + exists none + constructor + · grind + · simp + have : (s : State) → s ∈ a.accept → a.toOptionεNA.saturate.Tr (some s) none none := by + intro s hs + sorry + -- simp [LTS.saturate] + -- apply LTS.MTr.stepL + simp [LTS.saturate] + + + simp [toOptionεNA] + + + grind sorry case cons x xs => sorry diff --git a/Cslib/Computability/Automata/EpsilonNA/Basic.lean b/Cslib/Computability/Automata/EpsilonNA/Basic.lean index e001d98c2..08241cc42 100644 --- a/Cslib/Computability/Automata/EpsilonNA/Basic.lean +++ b/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 s' end FinAcc diff --git a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean index d0299dc92..2dc30c248 100644 --- a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean +++ b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean @@ -41,20 +41,84 @@ 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 + Tr s μ s' := a.STr s (some μ) s' open Acceptor in -open scoped NA.FinAcc in +open scoped NA.FinAcc LTS 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 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] + cases xs + case nil => + apply Iff.intro <;> intro h + case mp => + rcases h with ⟨s, hs, s', hs', h⟩ + simp only [toNAFinAcc, εClosure, LTS.τClosure, LTS.setImage, LTS.saturate, Set.mem_iUnion, + exists_prop] at hs + rcases hs with ⟨sStart, hStart, hs⟩ + exists sStart + apply And.intro + case left => grind + case right => + exists s' + apply And.intro + case left => grind + case right => + simp only [List.pure_def, List.bind_eq_flatMap, List.flatMap_nil] + grind [LTS.SMTr.τ] + case mpr => + rcases h with ⟨s, hs, s', hs', h⟩ + simp only [List.pure_def, List.bind_eq_flatMap, List.flatMap_nil] at h + simp [Accepts] + exists s' + constructor + · simp [toNAFinAcc, εClosure, LTS.τClosure, LTS.saturate] + simp [LTS.setImage] + exists s + constructor + · grind + · simp [LTS.image] + cases h + grind + · exists s' + constructor + · grind + · grind + case cons x xs => + have : ∀ {s s'}, ena.toNAFinAcc.MTr s (x :: xs) s' = ena.SMTr s (x :: xs) s' := by + intro s s' + have := LTS.sMTr_mTr_not_nil (lts := ena.toLTS) (s := s) (s' := s') (μs := some x :: xs.map some) (by simp) + ext + apply Iff.intro <;> intro h + · simp + + · sorry + simp [Accepts] + apply Iff.intro <;> intro h + · rcases h with ⟨s, hs, s', hs', h⟩ + rw [this] at h + simp [toNAFinAcc] at hs + have h_start : ∃ sStart ∈ ena.start, ena.τSTr s sStart := by + sorry + rcases h_start with ⟨sStart, h_sStart, h_start⟩ + exists sStart + apply And.intro + · grind + · exists s' + apply And.intro + · grind + · grind + -- simp [LTS.noε_saturate_mTr] + -- #adaptation_note + -- /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + -- grind [Accepts] + -- have : ∀ s s', ena.MTr s (xs.map some) s' = ena.ε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 diff --git a/Cslib/Foundations/Semantics/LTS/HasTau.lean b/Cslib/Foundations/Semantics/LTS/HasTau.lean index d315ae77c..4054d926f 100644 --- a/Cslib/Foundations/Semantics/LTS/HasTau.lean +++ b/Cslib/Foundations/Semantics/LTS/HasTau.lean @@ -31,8 +31,8 @@ def τSTr [HasTau Label] (lts : LTS State Label) : State → State → Prop := /-- Saturated transition relation. -/ inductive STr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where -| refl : lts.STr s HasTau.τ s -| tr : lts.τSTr s1 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 s4 → lts.STr s1 μ s4 + | refl : lts.STr s HasTau.τ s + | tr : lts.τSTr s1 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 s4 → lts.STr s1 μ s4 /-- The `LTS` obtained by saturating the transition relation in `lts`. -/ @[scoped grind =] @@ -44,14 +44,14 @@ theorem saturate_tr_sTr [HasTau Label] {lts : LTS State Label} : lts.saturate.Tr = lts.STr := by rfl /-- Any transition is also a saturated transition. -/ -theorem STr.single [HasTau Label] (lts : LTS State Label) : +theorem STr.single [HasTau Label] {lts : LTS State Label} : lts.Tr s μ s' → lts.STr s μ s' := by intro h apply STr.tr .refl h .refl /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/ theorem sTr_τSTr [HasTau Label] (lts : LTS State Label) : - lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by + lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by apply Iff.intro <;> intro h case mp => cases h @@ -64,8 +64,8 @@ theorem sTr_τSTr [HasTau Label] (lts : LTS State Label) : case tail _ h1 h2 => exact STr.tr h1 h2 .refl /-- In a saturated LTS, the transition and saturated transition relations are the same. -/ -theorem saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label) - : lts.saturate.τSTr s = lts.τSTr s := by +theorem saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label) : + lts.saturate.τSTr s = lts.τSTr s := by ext s'' apply Iff.intro <;> intro h case mp => @@ -82,19 +82,19 @@ theorem saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label) /-- Saturated transitions labelled by τ can be composed. -/ @[scoped grind .] theorem STr.trans_τ - [HasTau Label] (lts : LTS State Label) - (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) : - lts.STr s1 HasTau.τ s3 := by + [HasTau Label] {lts : LTS State Label} + (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) : + lts.STr s1 HasTau.τ s3 := by rw [sTr_τSTr _] at h1 h2 rw [sTr_τSTr _] apply Relation.ReflTransGen.trans h1 h2 /-- Saturated transitions can be composed. -/ theorem STr.comp - [HasTau Label] (lts : LTS State Label) - (h1 : lts.STr s1 HasTau.τ s2) - (h2 : lts.STr s2 μ s3) - (h3 : lts.STr s3 HasTau.τ s4) : + [HasTau Label] {lts : LTS State Label} + (h1 : lts.STr s1 HasTau.τ s2) + (h2 : lts.STr s2 μ s3) + (h3 : lts.STr s3 HasTau.τ s4) : lts.STr s1 μ s4 := by rw [sTr_τSTr _] at h1 h3 cases h2 @@ -121,7 +121,7 @@ theorem saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label case tr hstr1 htr hstr2 => rw [saturate_τSTr_τSTr lts] at hstr1 hstr2 rw [←sTr_τSTr lts] at hstr1 hstr2 - exact STr.comp lts hstr1 htr hstr2 + exact STr.comp hstr1 htr hstr2 /-- In a saturated LTS, every state is in its τ-image. -/ @[scoped grind .] @@ -144,6 +144,11 @@ lemma subset_saturate_setImage_τ [HasTau Label] (lts : LTS State Label) : intro s h grind +/-- `setImage` preserves (non-)emptyness. -/ +@[scoped grind =] +lemma empty_saturate_setImage_τ [HasTau Label] (lts : LTS State Label) : + lts.saturate.setImage S HasTau.τ = ∅ ↔ S = ∅:= by grind + /-- The `τ`-closure of a set of states `S` is the set of states reachable by any state in `S` by performing only `τ`-transitions. -/ def τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State := @@ -159,6 +164,63 @@ lemma τClosure_mem [HasTau Label] (lts : LTS State Label) (h : s ∈ S) : lemma τClosure_subset [HasTau Label] (lts : LTS State Label) : S ⊆ lts.τClosure S := by grind +/-- Saturated multistep transition relation. -/ +inductive SMTr [HasTau Label] (lts : LTS State Label) : State → List Label → State → Prop where + | τ : lts.STr s HasTau.τ s' → lts.SMTr s [] s' + | stepL : lts.STr s1 μ s2 → lts.SMTr s2 μs s3 → lts.SMTr s1 (μ :: μs) s3 + +/-- The saturated multistep transition relation is reflexive. -/ +@[scoped grind .] +theorem SMTr.refl [HasTau Label] (lts : LTS State Label) (s : State) : + lts.SMTr s [] s := by grind [LTS.STr, LTS.SMTr] + +open scoped LTS.STr + +/-- The saturated multistep transition relation is transitive. -/ +@[scoped grind .] +theorem SMTr.comp [HasTau Label] {lts : LTS State Label} + (h₁ : lts.SMTr s₁ μs₁ s₂) (h₂ : lts.SMTr s₂ μs₂ s₃) : lts.SMTr s₁ (μs₁ ++ μs₂) s₃ := by + induction h₁ + case τ s₁ s₂ htr => + cases h₂ + case τ htr' => grind [SMTr] + case stepL _ _ _ μ s₂' μs hstr hmstr => + have hstr' : lts.STr s₁ μ s₂' := by + apply STr.comp htr hstr STr.refl + simp only [List.nil_append] + apply stepL hstr' hmstr + case stepL s₁ μ s₁' μs s₂ hstr hmstr ih => + apply stepL hstr (ih h₂) + +/-- A multistep transition implies a saturated multistep transition. -/ +@[scoped grind .] +theorem mTr_sMTr [HasTau Label] {lts : LTS State Label} + (h : lts.MTr s μs s') : lts.SMTr s μs s' := by + induction μs generalizing s s' + case nil => grind [LTS.STr, LTS.SMTr] + case cons x xs ih => + cases h + case stepL sb htr hmtr => exact SMTr.stepL (STr.single htr) (ih hmtr) + +/-- A saturated multistep transition with a nonempty label list implies a multistep transition. -/ +@[scoped grind .] +theorem sMTr_mTr_not_nil [HasTau Label] {lts : LTS State Label} + (hμs : μs ≠ []) (h : lts.SMTr s μs s') : lts.saturate.MTr s μs s' := by + induction μs generalizing s + case nil => contradiction + case cons x xs ih => + cases h + case stepL sb htr hmtr => + cases xs with + | nil => + cases hmtr + case τ h_τ => + exact LTS.MTr.stepL + (LTS.STr.comp LTS.STr.refl htr h_τ) + LTS.MTr.refl + | cons y ys => + exact LTS.MTr.stepL htr (ih (by simp) hmtr) + end LTS end Cslib From f9cef260756c76b90a1d3efa6215320867f07302 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 4 Jun 2026 13:46:33 +0200 Subject: [PATCH 08/10] Progress on toOptionDA --- Cslib/Computability/Automata/DA/OptionDA.lean | 210 +++++++++++++++--- .../Automata/EpsilonNA/Basic.lean | 2 +- .../Automata/EpsilonNA/ToNA.lean | 125 +++-------- .../Semantics/LTS/Bisimulation.lean | 24 +- Cslib/Foundations/Semantics/LTS/HasTau.lean | 69 +++--- Cslib/Foundations/Semantics/LTS/Map.lean | 39 ++++ 6 files changed, 302 insertions(+), 167 deletions(-) create mode 100644 Cslib/Foundations/Semantics/LTS/Map.lean diff --git a/Cslib/Computability/Automata/DA/OptionDA.lean b/Cslib/Computability/Automata/DA/OptionDA.lean index f7d0bd3bb..834c2781d 100644 --- a/Cslib/Computability/Automata/DA/OptionDA.lean +++ b/Cslib/Computability/Automata/DA/OptionDA.lean @@ -92,10 +92,40 @@ lemma DA.FinAcc.toOptionεNA_ε_τSTr_none {a : DA.FinAcc State Symbol} /-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ @[scoped grind .] -lemma DA.FinAcc.toOptionεNA_ε_sTr_none {a : DA.FinAcc State Symbol} +lemma DA.FinAcc.toOptionεNA_none_sTr_none {a : DA.FinAcc State Symbol} (h : a.toOptionεNA.STr s none s') : s' = s ∨ s' = none := by cases h <;> grind -open scoped LTS εNA εNA.FinAcc +@[scoped grind =] +lemma DA.FinAcc.toOptionεNA_mem_accept_tr_iff {a : DA.FinAcc State Symbol} : + s ∈ a.accept ↔ a.toOptionεNA.Tr s none none := by grind only [toOptionεNA] + +lemma pippo {a : DA.FinAcc State Symbol} : + a.toOptionεNA.STr (some s) (some μ) = a.toOptionεNA.Tr (some s) (some μ) := by + sorry + -- grind + +open scoped LTS LTS.STr LTS.SMTr FLTS εNA εNA.FinAcc + +@[scoped grind =] +lemma DA.FinAcc.toOptionεNA_mem_accept_sTr_iff {a : DA.FinAcc State Symbol} : + s ∈ a.accept ↔ a.toOptionεNA.STr s none none := by + apply Iff.intro <;> intro h + case mp => + grind only [toOptionεNA_mem_accept_tr_iff, LTS.STr.single] + case mpr => + cases h + case tr osb osb' h₁ h₂ h₃ => + rw [show osb' = none by grind only [toOptionεNA]] at h₂ + induction h₁ + case refl => grind only [= toOptionεNA_mem_accept_tr_iff] + case tail os os' h₁₁ h₁₂ ih => + have h_tr_os: a.toOptionεNA.Tr os none none := by + have : a.toOptionεNA.τSTr os os' := by + simp only [LTS.τSTr] + grind + simp only [toOptionεNA] + grind + exact ih h_tr_os /-- The ε-closure of the start state in `DA.toOptionεNA` consists of the start state and `none`. -/ @[scoped grind =] @@ -107,55 +137,171 @@ lemma DA.FinAcc.toOptionεNA_start_εClosure {a : DA.FinAcc State Symbol} (h : a ext s apply Iff.intro <;> intro h' · grind - · simp only [Set.mem_setOf_eq] - simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at h' - cases h' with + · cases h' with | inl h' => rw [h'] apply LTS.STr.refl | inr h' => rw [h'] - have htr : a.toOptionεNA.Tr (some a.start) none none := by grind + have htr : a.toOptionεNA.Tr (some a.start) none none := by grind only [toOptionεNA] exact LTS.STr.single htr +/-- Correspondence of transitions under `toOptionεNA`. -/ +@[scoped grind =] +theorem DA.FinAcc.toOptionεNA_tr_tr_iff {a : DA.FinAcc State Symbol} + : a.toOptionεNA.Tr (some s) (some μ) (some s') ↔ a.tr s μ = s' := by grind only [toOptionεNA] + +/-- Correspondence of transitions under `toOptionεNA`. -/ +@[scoped grind =] +theorem DA.FinAcc.toOptionεNA_sTr_tr_iff {a : DA.FinAcc State Symbol} : + a.toOptionεNA.STr (some s) (some μ) (some s') ↔ + a.toOptionεNA.Tr (some s) (some μ) (some s') := by + apply Iff.intro <;> intro h + case mp => + cases h + grind [toOptionεNA] + case mpr => + apply LTS.STr.single h + +/-- Correspondence of multistep transitions under `toOptionεNA`. -/ +@[scoped grind =] +theorem DA.FinAcc.toOptionεNA_mTr_mTr_iff {a : DA.FinAcc State Symbol} + : a.toOptionεNA.MTr (some s) (μs.map Option.some) (some s') ↔ a.mtr s μs = s' := by + induction μs generalizing s + case nil => grind + case cons x xs ih => + apply Iff.intro <;> intro h + case mp => + cases h + case stepL sb htr hmtr => + have h_tr_sb : a.tr s x = sb := by + simp only [toOptionεNA] at htr + grind only + grind only [FLTS.mtr, List.foldl_cons] + case mpr => + apply LTS.MTr.stepL (s2 := some (a.tr s x)) (by grind) (by grind) + +/-- Correspondence of saturated and normal multistep transitions under `toOptionεNA`. -/ +@[scoped grind =] +theorem DA.FinAcc.toOptionεNA_sMTr_mTr_iff {a : DA.FinAcc State Symbol} {μs : List Symbol} + (h : μs ≠ []) : a.toOptionεNA.SMTr (some s) (μs.map Option.some) (some s') ↔ + a.toOptionεNA.MTr (some s) (μs.map Option.some) (some s') := by + induction μs generalizing s with + | nil => contradiction + | cons μ μs ih => + simp only [List.map_cons] + apply Iff.intro <;> intro h' + case mp => + cases h' + case stepL os hstr hsmtr => + have hos : ∃ sb, os = some sb := by + sorry + rcases hos with ⟨sb, hos⟩ + + cases μs + case nil => grind + case cons μ' μs => + + simp [toOptionεNA] + + case mpr => + exact LTS.SMTr.fromMTr h' + +/-- Correspondence of multistep transitions under `toOptionεNA`. -/ +@[scoped grind =] +theorem DA.FinAcc.toOptionεNA_sMTr_mTr_iff {a : DA.FinAcc State Symbol} + : a.toOptionεNA.SMTr (some s) (μs.map Option.some) (some s') ↔ a.mtr s μs = s' := by + induction μs generalizing s + case nil => + simp [toOptionεNA] + grind + case cons x xs ih => + apply Iff.intro <;> intro h + case mp => + cases h + case stepL sb htr hmtr => + + -- have h_tr_sb : a.tr s x = sb := by + -- simp only [toOptionεNA] at htr + -- grind only + grind only [FLTS.mtr, List.foldl_cons] + case mpr => + apply LTS.MTr.stepL (s2 := some (a.tr s x)) (by grind) (by grind) + open Acceptor in /-- `DA.toOptionεNA` preserves the automaton's language. -/ +@[scoped grind =] theorem DA.FinAcc.toOptionεNA_language_eq {a : DA.FinAcc State Symbol} : language a.toOptionεNA = language a := by ext xs - simp only [Acceptor.mem_language] - simp only [Accepts] + simp only [Acceptor.mem_language, Accepts] apply Iff.intro <;> intro h case mp => + rcases h with ⟨s, hs, s', hs', h⟩ + cases hs' -- s' is none + revert hs + cases xs + case nil => + intro hs; cases hs + cases h + case refl.τ h => + grind [toOptionεNA_mem_accept_sTr_iff.mpr h] + case cons x xs => + intro hs; cases hs + cases h + case stepL os h_sTr h_sMTr => + + + simp only [toOptionεNA_none_accept, Set.mem_singleton_iff] at hs' + simp [hs'] at h + sorry case mpr => induction xs case nil => + simp only [FLTS.mtr_nil_eq] at h exists a.start - apply And.intro - case left => grind - case right => - have h' : a.start ∈ a.accept := by grind [FLTS.mtr] - exists none - constructor - · grind - · simp - have : (s : State) → s ∈ a.accept → a.toOptionεNA.saturate.Tr (some s) none none := by - intro s hs - sorry - -- simp [LTS.saturate] - -- apply LTS.MTr.stepL - - simp [LTS.saturate] - - - simp [toOptionεNA] - - - grind - sorry - case cons x xs => - sorry + apply And.intro (by grind) + exists none + apply And.intro (by simp) + apply LTS.SMTr.τ + apply LTS.STr.tr (s2 := some a.start) (s3 := none) <;> grind + case cons x xs ih => + exists a.start + apply And.intro (by grind) + exists none + apply And.intro (by simp) + simp only [FLTS.mtr, List.foldl_cons] at h + simp only [List.map_cons] + rw [← FLTS.mtr] at h + + -- rw [← List.foldl_cons] at h + grind + -- exists a.start + -- apply And.intro + -- case left => grind + -- case right => + -- have h' : a.start ∈ a.accept := by grind [FLTS.mtr] + -- exists none + -- constructor + -- · grind + -- · simp + -- have : (s : State) → s ∈ a.accept → a.toOptionεNA.saturate.Tr (some s) none none := by + -- intro s hs + -- sorry + -- -- simp [LTS.saturate] + -- -- apply LTS.MTr.stepL + + -- simp [LTS.saturate] + + + -- simp [toOptionεNA] + + + -- grind + -- sorry + -- case cons x xs => + -- sorry namespace NA.FinAcc diff --git a/Cslib/Computability/Automata/EpsilonNA/Basic.lean b/Cslib/Computability/Automata/EpsilonNA/Basic.lean index 08241cc42..a5fa79012 100644 --- a/Cslib/Computability/Automata/EpsilonNA/Basic.lean +++ b/Cslib/Computability/Automata/EpsilonNA/Basic.lean @@ -47,7 +47,7 @@ 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.start, ∃ s' ∈ a.accept, a.SMTr s xs s' + ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.SMTr s (xs.map Option.some) s' end FinAcc diff --git a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean index 2dc30c248..74c94d3c1 100644 --- a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean +++ b/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,85 +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 s μ s' := a.STr s (some μ) s' + toLTS := a.saturate.mapLabel Option.some open Acceptor in -open scoped NA.FinAcc LTS LTS.STr LTS.SMTr 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 - cases xs - case nil => - apply Iff.intro <;> intro h - case mp => - rcases h with ⟨s, hs, s', hs', h⟩ - simp only [toNAFinAcc, εClosure, LTS.τClosure, LTS.setImage, LTS.saturate, Set.mem_iUnion, + 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, hStart, hs⟩ + rcases hs with ⟨sStart, h_sStart, hs⟩ exists sStart - apply And.intro - case left => grind - case right => - exists s' - apply And.intro - case left => grind - case right => - simp only [List.pure_def, List.bind_eq_flatMap, List.flatMap_nil] - grind [LTS.SMTr.τ] - case mpr => - rcases h with ⟨s, hs, s', hs', h⟩ - simp only [List.pure_def, List.bind_eq_flatMap, List.flatMap_nil] at h - simp [Accepts] + 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' - constructor - · simp [toNAFinAcc, εClosure, LTS.τClosure, LTS.saturate] - simp [LTS.setImage] - exists s - constructor - · grind - · simp [LTS.image] - cases h - grind - · exists s' - constructor - · grind - · grind - case cons x xs => - have : ∀ {s s'}, ena.toNAFinAcc.MTr s (x :: xs) s' = ena.SMTr s (x :: xs) s' := by - intro s s' - have := LTS.sMTr_mTr_not_nil (lts := ena.toLTS) (s := s) (s' := s') (μs := some x :: xs.map some) (by simp) - ext - apply Iff.intro <;> intro h - · simp - - · sorry - simp [Accepts] - apply Iff.intro <;> intro h - · rcases h with ⟨s, hs, s', hs', h⟩ - rw [this] at h - simp [toNAFinAcc] at hs - have h_start : ∃ sStart ∈ ena.start, ena.τSTr s sStart := by - sorry - rcases h_start with ⟨sStart, h_sStart, h_start⟩ - exists sStart - apply And.intro - · grind - · exists s' - apply And.intro - · grind - · grind - -- simp [LTS.noε_saturate_mTr] - -- #adaptation_note - -- /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ - -- grind [Accepts] - -- have : ∀ s s', ena.MTr s (xs.map some) s' = ena.ε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 + simp only [toNAFinAcc, LTS.saturate, LTS.τClosure] + grind [cases LTS.SMTr] + | cons x xs => + exists s + grind -end Cslib +end Cslib.Automata.εNA.FinAcc diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 21ffd67eb..b8a506042 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -853,7 +853,7 @@ theorem IsSWBisimulation.follow_internal_fst obtain ⟨sb2', htrsb2', hrb'⟩ := h exists sb2' constructor - · simp only [sTr_τSTr] at htrsb htrsb2' + · simp only [sTr_τSTr_iff] at htrsb htrsb2' exact Relation.ReflTransGen.trans htrsb2 htrsb2' · exact hrb' @@ -874,7 +874,7 @@ theorem IsSWBisimulation.follow_internal_snd obtain ⟨sb2', htrsb2', hrb'⟩ := h exists sb2' constructor - · simp only [sTr_τSTr] at htrsb htrsb2' + · simp only [sTr_τSTr_iff] at htrsb htrsb2' exact Relation.ReflTransGen.trans htrsb2 htrsb2' · exact hrb' @@ -890,13 +890,13 @@ theorem isWeakBisimulation_iff_isSWBisimulation case left => intro s₁' htr specialize h hr μ - have h' := h.1 s₁' (STr.single lts₁ htr) + have h' := h.1 s₁' (STr.single htr) obtain ⟨s₂', htr2, hr2⟩ := h' exists s₂' case right => intro s₂' htr specialize h hr μ - have h' := h.2 s₂' (STr.single lts₂ htr) + have h' := h.2 s₂' (STr.single htr) obtain ⟨s₁', htr1, hr1⟩ := h' exists s₁' case mpr => @@ -910,15 +910,15 @@ theorem isWeakBisimulation_iff_isSWBisimulation constructor; constructor exact hr case tr sb sb' hstr1 htr hstr2 => - rw [←sTr_τSTr] at hstr1 hstr2 - simp only [sTr_τSTr] at hstr1 hstr2 + rw [←sTr_τSTr_iff] at hstr1 hstr2 + simp only [sTr_τSTr_iff] at hstr1 hstr2 obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_fst h hr hstr1 obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).left _ htr obtain ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_fst h hrb' hstr2 - rw [←sTr_τSTr] at hstr1' hstr1b + rw [←sTr_τSTr_iff] at hstr1' hstr1b exists s₁' constructor - · exact STr.comp lts₂ hstr1b hstr1b' hstr1' + · exact STr.comp hstr1b hstr1b' hstr1' · exact hrb2 case right => intro s₂' hstr @@ -928,15 +928,15 @@ theorem isWeakBisimulation_iff_isSWBisimulation constructor; constructor exact hr case tr sb sb' hstr1 htr hstr2 => - rw [←sTr_τSTr] at hstr1 hstr2 - simp only [sTr_τSTr] at hstr1 hstr2 + rw [←sTr_τSTr_iff] at hstr1 hstr2 + simp only [sTr_τSTr_iff] at hstr1 hstr2 obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_snd h hr hstr1 obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).right _ htr obtain ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_snd h hrb' hstr2 - rw [←sTr_τSTr] at hstr1' hstr1b + rw [←sTr_τSTr_iff] at hstr1' hstr1b exists s₁' constructor - · exact STr.comp lts₁ hstr1b hstr1b' hstr1' + · exact STr.comp hstr1b hstr1b' hstr1' · exact hrb2 theorem IsWeakBisimulation.isSwBisimulation diff --git a/Cslib/Foundations/Semantics/LTS/HasTau.lean b/Cslib/Foundations/Semantics/LTS/HasTau.lean index 4054d926f..abe6bf699 100644 --- a/Cslib/Foundations/Semantics/LTS/HasTau.lean +++ b/Cslib/Foundations/Semantics/LTS/HasTau.lean @@ -50,7 +50,7 @@ theorem STr.single [HasTau Label] {lts : LTS State Label} : apply STr.tr .refl h .refl /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/ -theorem sTr_τSTr [HasTau Label] (lts : LTS State Label) : +theorem sTr_τSTr_iff [HasTau Label] (lts : LTS State Label) : lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by apply Iff.intro <;> intro h case mp => @@ -64,14 +64,14 @@ theorem sTr_τSTr [HasTau Label] (lts : LTS State Label) : case tail _ h1 h2 => exact STr.tr h1 h2 .refl /-- In a saturated LTS, the transition and saturated transition relations are the same. -/ -theorem saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label) : - lts.saturate.τSTr s = lts.τSTr s := by - ext s'' +theorem saturate_τsTr_τSTr_iff [hHasTau : HasTau Label] (lts : LTS State Label) : + lts.saturate.τSTr = lts.τSTr := by + ext s s' apply Iff.intro <;> intro h case mp => induction h case refl => constructor - case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((sTr_τSTr _).mp h2) + case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((sTr_τSTr_iff _).mp h2) case mpr => cases h case refl => constructor @@ -85,8 +85,8 @@ theorem STr.trans_τ [HasTau Label] {lts : LTS State Label} (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) : lts.STr s1 HasTau.τ s3 := by - rw [sTr_τSTr _] at h1 h2 - rw [sTr_τSTr _] + rw [sTr_τSTr_iff _] at h1 h2 + rw [sTr_τSTr_iff _] apply Relation.ReflTransGen.trans h1 h2 /-- Saturated transitions can be composed. -/ @@ -96,17 +96,17 @@ theorem STr.comp (h2 : lts.STr s2 μ s3) (h3 : lts.STr s3 HasTau.τ s4) : lts.STr s1 μ s4 := by - rw [sTr_τSTr _] at h1 h3 + rw [sTr_τSTr_iff _] at h1 h3 cases h2 case refl => - rw [sTr_τSTr _] + rw [sTr_τSTr_iff _] apply Relation.ReflTransGen.trans h1 h3 case tr _ _ hτ1 htr hτ2 => exact STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3) /-- In a saturated LTS, the transition and saturated transition relations are the same. -/ theorem saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label) - (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by + (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by ext s' apply Iff.intro <;> intro h case mp => @@ -119,8 +119,8 @@ theorem saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label cases h case refl => constructor case tr hstr1 htr hstr2 => - rw [saturate_τSTr_τSTr lts] at hstr1 hstr2 - rw [←sTr_τSTr lts] at hstr1 hstr2 + rw [saturate_τsTr_τSTr_iff lts] at hstr1 hstr2 + rw [←sTr_τSTr_iff lts] at hstr1 hstr2 exact STr.comp hstr1 htr hstr2 /-- In a saturated LTS, every state is in its τ-image. -/ @@ -194,7 +194,7 @@ theorem SMTr.comp [HasTau Label] {lts : LTS State Label} /-- A multistep transition implies a saturated multistep transition. -/ @[scoped grind .] -theorem mTr_sMTr [HasTau Label] {lts : LTS State Label} +theorem SMTr.fromMTr [HasTau Label] {lts : LTS State Label} (h : lts.MTr s μs s') : lts.SMTr s μs s' := by induction μs generalizing s s' case nil => grind [LTS.STr, LTS.SMTr] @@ -202,24 +202,39 @@ theorem mTr_sMTr [HasTau Label] {lts : LTS State Label} cases h case stepL sb htr hmtr => exact SMTr.stepL (STr.single htr) (ih hmtr) +@[scoped grind =] +theorem sMTr_τSTr_iff [HasTau Label] {lts : LTS State Label} : + lts.τSTr s s' ↔ lts.SMTr s [] s' := by grind only [=_ sTr_τSTr_iff, SMTr] + /-- A saturated multistep transition with a nonempty label list implies a multistep transition. -/ -@[scoped grind .] -theorem sMTr_mTr_not_nil [HasTau Label] {lts : LTS State Label} - (hμs : μs ≠ []) (h : lts.SMTr s μs s') : lts.saturate.MTr s μs s' := by +@[scoped grind =] +theorem saturate_mTr_sMTr_not_nil_iff [HasTau Label] {lts : LTS State Label} + (hμs : μs ≠ []) : lts.saturate.MTr s μs s' ↔ lts.SMTr s μs s' := by induction μs generalizing s case nil => contradiction case cons x xs ih => - cases h - case stepL sb htr hmtr => - cases xs with - | nil => - cases hmtr - case τ h_τ => - exact LTS.MTr.stepL - (LTS.STr.comp LTS.STr.refl htr h_τ) - LTS.MTr.refl - | cons y ys => - exact LTS.MTr.stepL htr (ih (by simp) hmtr) + apply Iff.intro <;> intro h + case mp => + cases h + case stepL sb htr hmtr => + cases xs with + | nil => + cases hmtr + apply LTS.SMTr.stepL htr (by grind only [SMTr.fromMTr, MTr.refl]) + | cons x' xs' => + exact LTS.SMTr.stepL htr ((ih (by simp)).mp hmtr) + case mpr => + cases h + case stepL sb htr hmtr => + cases xs with + | nil => + cases hmtr + case τ h_τ => + exact LTS.MTr.stepL + (LTS.STr.comp LTS.STr.refl htr h_τ) + LTS.MTr.refl + | cons x' xs' => + exact LTS.MTr.stepL htr ((ih (by simp)).mpr hmtr) end LTS diff --git a/Cslib/Foundations/Semantics/LTS/Map.lean b/Cslib/Foundations/Semantics/LTS/Map.lean new file mode 100644 index 000000000..e5c4c6600 --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/Map.lean @@ -0,0 +1,39 @@ +/- +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.Semantics.LTS.Basic + + +/-! +# Map operation for LTS. +-/ + +@[expose] public section + +namespace Cslib.LTS + +section MapLabel + +/-- Constructs an LTS by mapping its labels into those of an existing LTS. -/ +def mapLabel (lts : LTS State Label₁) (f : Label₂ → Label₁) : LTS State Label₂ where + Tr s μ s' := lts.Tr s (f μ) s' + +@[scoped grind =] +theorem mapLabel_tr {lts : LTS State Label₁} {f : Label₂ → Label₁} : + (lts.mapLabel f).Tr s μ s' ↔ lts.Tr s (f μ) s' := by rfl + +@[scoped grind =] +theorem mapLabel_mTr {lts : LTS State Label₁} {f : Label₂ → Label₁} : + (lts.mapLabel f).MTr s μs s' ↔ lts.MTr s (μs.map f) s' := by + induction μs generalizing s with + | nil => grind + | cons μ μs ih => grind [=_ mapLabel_tr (f := f)] + +end MapLabel + +end Cslib.LTS From 1338139e2f2b26f7e64d7b21298e0c85d18d617c Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 4 Jun 2026 14:26:56 +0200 Subject: [PATCH 09/10] Add NTM in parallel to SingleTapeTM --- Cslib.lean | 5 +- Cslib/Computability/Automata/DA/OptionDA.lean | 333 ------------------ .../Turing/SingleTape/Deterministic.lean | 268 ++++++-------- .../Turing/SingleTape/NonDeterministic.lean | 2 +- Cslib/Foundations/Data/BiTape.lean | 15 +- Cslib/Foundations/Data/StackTape.lean | 4 +- 6 files changed, 121 insertions(+), 506 deletions(-) delete mode 100644 Cslib/Computability/Automata/DA/OptionDA.lean diff --git a/Cslib.lean b/Cslib.lean index c0269e0bb..1ff81659e 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Computability/Automata/DA/OptionDA.lean b/Cslib/Computability/Automata/DA/OptionDA.lean deleted file mode 100644 index 834c2781d..000000000 --- a/Cslib/Computability/Automata/DA/OptionDA.lean +++ /dev/null @@ -1,333 +0,0 @@ -/- -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.Computability.Automata.DA.Basic -public import Cslib.Computability.Automata.EpsilonNA.Basic -public import Cslib.Computability.Automata.EpsilonNA.ToNA -public import Cslib.Computability.Automata.NA.ToDA - -/-! # OptionDA: DA with a single halting accept state - -An `OptionDA` is a deterministic automaton with a unique accepting and halting state, codified as -`none : Option State`. Any `DA.FinAcc` can be converted into an `OptionDA` by (i) adding an -ε-transition from every accepting state to the `none` halting state, and then (ii) by transforming -the resulting `εNA` into an `OptionDA`. --/ - -@[expose] public section - -namespace Cslib.Automata - -/-- A deterministic automaton with a single accepting, halting state, modelled as the `none` value -of `Option Symbol`. -/ -structure OptionDA (State Symbol : Type*) where - /-- The transition function of the automaton. -/ - tr : State → Symbol → Option State - /-- The initial state of the automaton. -/ - start : State - -variable {State Symbol : Type*} - -namespace OptionDA - -/-- Multistep transition function. -/ -def mtr (a : OptionDA State Symbol) : State → List Symbol → Option State - | s, [] => s - | s, x :: xs => a.tr s x >>= (a.mtr · xs) - -/-- An `OptionDA` accepts a string if its multistep transition function maps the start state and -the string to an accept state. - -This is the standard string recognition performed by DFAs in the literature. -/ -@[simp, scoped grind =] -instance : Acceptor (OptionDA State Symbol) Symbol where - Accepts (a : OptionDA State Symbol) (xs : List Symbol) := a.mtr a.start xs = .none - -end OptionDA - -/-- Converts a `DA.FinAcc` into an `εNA` with an additional `none` state that acts as the unique -accepting and halting state. Every accepting state of the original automaton gains an ε-transition -to `none`, and all other transitions are lifted by `some`. -/ -@[scoped grind =] -def DA.FinAcc.toOptionεNA (a : DA.FinAcc State Symbol) : εNA.FinAcc (Option State) Symbol where - start := {some a.start} - accept := {none} - Tr - -- Lift of original transitions - | some s, some x, some s' => s' = a.tr s x - -- Additional ε-transitions to the halting state. - | some s, none, none => s ∈ a.accept - | _, _, _ => False - -/-- The `none` state in `DA.toOptionεNA` is the only accept state. -/ -@[simp] -lemma DA.FinAcc.toOptionεNA_none_accept (a : DA.FinAcc State Symbol) : - a.toOptionεNA.accept = {none} := rfl - -/-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ -@[scoped grind .] -lemma DA.FinAcc.toOptionεNA_none_tr (a : DA.FinAcc State Symbol) - (μ : Option Symbol) (s : Option State) : ¬a.toOptionεNA.Tr none μ s := by grind - -/-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ -@[scoped grind .] -lemma DA.FinAcc.toOptionεNA_tr_none_iff {a : DA.FinAcc State Symbol} - (h : a.toOptionεNA.Tr s μ s') : μ = none ↔ s' = none := by cases hμ : μ <;> grind - -/-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ -@[scoped grind .] -lemma DA.FinAcc.toOptionεNA_ε_τSTr_none {a : DA.FinAcc State Symbol} - (h : a.toOptionεNA.τSTr s s') : s' = s ∨ s' = none := by - cases h with - | refl => simp - | tail s₁ h => - apply toOptionεNA_tr_none_iff at h - simp only [HasTau.τ, true_iff] at h - simp [h] - -/-- The `none` state in `DA.toOptionεNA` has no outgoing transitions. -/ -@[scoped grind .] -lemma DA.FinAcc.toOptionεNA_none_sTr_none {a : DA.FinAcc State Symbol} - (h : a.toOptionεNA.STr s none s') : s' = s ∨ s' = none := by cases h <;> grind - -@[scoped grind =] -lemma DA.FinAcc.toOptionεNA_mem_accept_tr_iff {a : DA.FinAcc State Symbol} : - s ∈ a.accept ↔ a.toOptionεNA.Tr s none none := by grind only [toOptionεNA] - -lemma pippo {a : DA.FinAcc State Symbol} : - a.toOptionεNA.STr (some s) (some μ) = a.toOptionεNA.Tr (some s) (some μ) := by - sorry - -- grind - -open scoped LTS LTS.STr LTS.SMTr FLTS εNA εNA.FinAcc - -@[scoped grind =] -lemma DA.FinAcc.toOptionεNA_mem_accept_sTr_iff {a : DA.FinAcc State Symbol} : - s ∈ a.accept ↔ a.toOptionεNA.STr s none none := by - apply Iff.intro <;> intro h - case mp => - grind only [toOptionεNA_mem_accept_tr_iff, LTS.STr.single] - case mpr => - cases h - case tr osb osb' h₁ h₂ h₃ => - rw [show osb' = none by grind only [toOptionεNA]] at h₂ - induction h₁ - case refl => grind only [= toOptionεNA_mem_accept_tr_iff] - case tail os os' h₁₁ h₁₂ ih => - have h_tr_os: a.toOptionεNA.Tr os none none := by - have : a.toOptionεNA.τSTr os os' := by - simp only [LTS.τSTr] - grind - simp only [toOptionεNA] - grind - exact ih h_tr_os - -/-- The ε-closure of the start state in `DA.toOptionεNA` consists of the start state and `none`. -/ -@[scoped grind =] -lemma DA.FinAcc.toOptionεNA_start_εClosure {a : DA.FinAcc State Symbol} (h : a.start ∈ a.accept) : - a.toOptionεNA.εClosure a.toOptionεNA.start = {some a.start, none} := by - rw [show a.toOptionεNA.start = {some a.start} by rfl] - simp only [εNA.εClosure, LTS.τClosure, LTS.setImage, Set.mem_singleton_iff, LTS.image, - LTS.saturate, HasTau.τ, Set.iUnion_iUnion_eq_left] - ext s - apply Iff.intro <;> intro h' - · grind - · cases h' with - | inl h' => - rw [h'] - apply LTS.STr.refl - | inr h' => - rw [h'] - have htr : a.toOptionεNA.Tr (some a.start) none none := by grind only [toOptionεNA] - exact LTS.STr.single htr - -/-- Correspondence of transitions under `toOptionεNA`. -/ -@[scoped grind =] -theorem DA.FinAcc.toOptionεNA_tr_tr_iff {a : DA.FinAcc State Symbol} - : a.toOptionεNA.Tr (some s) (some μ) (some s') ↔ a.tr s μ = s' := by grind only [toOptionεNA] - -/-- Correspondence of transitions under `toOptionεNA`. -/ -@[scoped grind =] -theorem DA.FinAcc.toOptionεNA_sTr_tr_iff {a : DA.FinAcc State Symbol} : - a.toOptionεNA.STr (some s) (some μ) (some s') ↔ - a.toOptionεNA.Tr (some s) (some μ) (some s') := by - apply Iff.intro <;> intro h - case mp => - cases h - grind [toOptionεNA] - case mpr => - apply LTS.STr.single h - -/-- Correspondence of multistep transitions under `toOptionεNA`. -/ -@[scoped grind =] -theorem DA.FinAcc.toOptionεNA_mTr_mTr_iff {a : DA.FinAcc State Symbol} - : a.toOptionεNA.MTr (some s) (μs.map Option.some) (some s') ↔ a.mtr s μs = s' := by - induction μs generalizing s - case nil => grind - case cons x xs ih => - apply Iff.intro <;> intro h - case mp => - cases h - case stepL sb htr hmtr => - have h_tr_sb : a.tr s x = sb := by - simp only [toOptionεNA] at htr - grind only - grind only [FLTS.mtr, List.foldl_cons] - case mpr => - apply LTS.MTr.stepL (s2 := some (a.tr s x)) (by grind) (by grind) - -/-- Correspondence of saturated and normal multistep transitions under `toOptionεNA`. -/ -@[scoped grind =] -theorem DA.FinAcc.toOptionεNA_sMTr_mTr_iff {a : DA.FinAcc State Symbol} {μs : List Symbol} - (h : μs ≠ []) : a.toOptionεNA.SMTr (some s) (μs.map Option.some) (some s') ↔ - a.toOptionεNA.MTr (some s) (μs.map Option.some) (some s') := by - induction μs generalizing s with - | nil => contradiction - | cons μ μs ih => - simp only [List.map_cons] - apply Iff.intro <;> intro h' - case mp => - cases h' - case stepL os hstr hsmtr => - have hos : ∃ sb, os = some sb := by - sorry - rcases hos with ⟨sb, hos⟩ - - cases μs - case nil => grind - case cons μ' μs => - - simp [toOptionεNA] - - case mpr => - exact LTS.SMTr.fromMTr h' - -/-- Correspondence of multistep transitions under `toOptionεNA`. -/ -@[scoped grind =] -theorem DA.FinAcc.toOptionεNA_sMTr_mTr_iff {a : DA.FinAcc State Symbol} - : a.toOptionεNA.SMTr (some s) (μs.map Option.some) (some s') ↔ a.mtr s μs = s' := by - induction μs generalizing s - case nil => - simp [toOptionεNA] - grind - case cons x xs ih => - apply Iff.intro <;> intro h - case mp => - cases h - case stepL sb htr hmtr => - - -- have h_tr_sb : a.tr s x = sb := by - -- simp only [toOptionεNA] at htr - -- grind only - grind only [FLTS.mtr, List.foldl_cons] - case mpr => - apply LTS.MTr.stepL (s2 := some (a.tr s x)) (by grind) (by grind) - -open Acceptor in -/-- `DA.toOptionεNA` preserves the automaton's language. -/ -@[scoped grind =] -theorem DA.FinAcc.toOptionεNA_language_eq {a : DA.FinAcc State Symbol} : - language a.toOptionεNA = language a := by - ext xs - simp only [Acceptor.mem_language, Accepts] - apply Iff.intro <;> intro h - case mp => - rcases h with ⟨s, hs, s', hs', h⟩ - cases hs' -- s' is none - revert hs - cases xs - case nil => - intro hs; cases hs - cases h - case refl.τ h => - grind [toOptionεNA_mem_accept_sTr_iff.mpr h] - case cons x xs => - intro hs; cases hs - cases h - case stepL os h_sTr h_sMTr => - - - simp only [toOptionεNA_none_accept, Set.mem_singleton_iff] at hs' - simp [hs'] at h - - sorry - case mpr => - induction xs - case nil => - simp only [FLTS.mtr_nil_eq] at h - exists a.start - apply And.intro (by grind) - exists none - apply And.intro (by simp) - apply LTS.SMTr.τ - apply LTS.STr.tr (s2 := some a.start) (s3 := none) <;> grind - case cons x xs ih => - exists a.start - apply And.intro (by grind) - exists none - apply And.intro (by simp) - simp only [FLTS.mtr, List.foldl_cons] at h - simp only [List.map_cons] - rw [← FLTS.mtr] at h - - -- rw [← List.foldl_cons] at h - grind - -- exists a.start - -- apply And.intro - -- case left => grind - -- case right => - -- have h' : a.start ∈ a.accept := by grind [FLTS.mtr] - -- exists none - -- constructor - -- · grind - -- · simp - -- have : (s : State) → s ∈ a.accept → a.toOptionεNA.saturate.Tr (some s) none none := by - -- intro s hs - -- sorry - -- -- simp [LTS.saturate] - -- -- apply LTS.MTr.stepL - - -- simp [LTS.saturate] - - - -- simp [toOptionεNA] - - - -- grind - -- sorry - -- case cons x xs => - -- sorry - -namespace NA.FinAcc - -def ofOptionFinAcc (a : NA.FinAcc (Option State) Symbol) : NA.FinAcc State Symbol where - start := { s | some s ∈ a.start } - Tr s x s' := a.Tr (some s) x (some s') - accept := { s | ∃ x, a.Tr (some s) x none } - -noncomputable def toOptionDA (a : NA.FinAcc State Symbol) : OptionDA (Set State) Symbol := - let da := a.toDAFinAcc - { start := da.start - tr S x := - let S' := da.tr S x - open Classical in if S' ∈ da.accept then none else some S' } - -end NA.FinAcc - -noncomputable def DA.FinAcc.toOptionDA (a : DA.FinAcc State Symbol) : - OptionDA (Set State) Symbol := - a.toOptionεNA.toNAFinAcc.ofOptionFinAcc.toOptionDA - -open Acceptor in --- open scoped NA.FinAcc in -theorem DA.FinAcc.toOptionDA_language_eq {a : DA.FinAcc State Symbol} : - language a.toOptionDA = language a := by - simp [toOptionDA] - sorry - -end Cslib.Automata diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean index 32adcd53a..79c4ae530 100644 --- a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean @@ -1,21 +1,20 @@ /- Copyright (c) 2026 Bolton Bailey. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Bolton Bailey, Pim Spelier, Daan van Gent, Fabrizio Montesi +Authors: Bolton Bailey, Pim Spelier, Daan van Gent -/ module -public import Cslib.Computability.Automata.NA.Basic public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Data.RelatesInSteps public import Mathlib.Algebra.Polynomial.Eval.Defs -public import Cslib.Computability.Machines.Turing.SingleTape.Defs /-! -# Single-Tape Deterministic Turing Machines +# Single-Tape Turing Machines -Defines a single-tape Turing machine for computing functions on `List Symbol`. +Defines a single-tape Turing machine for computing functions on `List Symbol` +for finite alphabet `Symbol`. ## Design @@ -63,141 +62,102 @@ We also provide ways of constructing polynomial-runtime TMs @[expose] public section -namespace Cslib.Computability.Turing.SingleTape - -open Cslib Relation Automata Turing.BiTape Turing.StackTape - --- /-- --- A single-tape Turing machine --- over the alphabet of `Option Symbol` (where `none` is the blank `BiTape` symbol). --- -/ --- structure SingleTapeTM Symbol [Inhabited Symbol] [Fintype Symbol] where --- /-- type of state labels -/ --- (State : Type) --- /-- finiteness of the state type -/ --- [stateFintype : Fintype State] --- /-- Initial state -/ --- (q₀ : State) --- /-- Transition function, mapping a state and a head symbol to a `Stmt` to invoke, --- and optionally the new state to transition to afterwards (`none` for halt) -/ --- (tr : State → Option Symbol → SingleTapeTM.Stmt Symbol × Option State) - -/-- Single-tape Deterministic Turing Machine (DTM, or just TM for short) over the alphabet of -`Option Symbol` (where `none` is the blank `BiTape` symbol). -/ -structure SingleTapeTM (State Symbol : Type*) - extends LTS State (SingleTape.TrLabel State Symbol) where - [is_deterministic : LTS.Deterministic {Tr := Tr}] - /-- The start state. -/ - start : State - /-- 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' +open Relation + +namespace Cslib.Turing + +open BiTape StackTape +open _root_.Turing + +variable {Symbol : Type} namespace SingleTapeTM -variable {State Symbol : Type*} +/-- +A Turing machine "statement" is just a `Option`al command to move left or right, +and write a symbol (i.e. an `Option Symbol`, where `none` is the blank symbol) on the `BiTape` +-/ +structure Stmt (Symbol : Type) where + /-- The symbol to write at the current head position -/ + symbol : Option Symbol + /-- The direction to move the tape head -/ + movement : Option Dir +deriving Inhabited + +end SingleTapeTM + +/-- +A single-tape Turing machine +over the alphabet of `Option Symbol` (where `none` is the blank `BiTape` symbol). +-/ +structure SingleTapeTM Symbol [Inhabited Symbol] [Fintype Symbol] where + /-- type of state labels -/ + (State : Type) + /-- finiteness of the state type -/ + [stateFintype : Fintype State] + /-- Initial state -/ + (q₀ : State) + /-- Transition function, mapping a state and a head symbol to a `Stmt` to invoke, + and optionally the new state to transition to afterwards (`none` for halt) -/ + (tr : State → Option Symbol → SingleTapeTM.Stmt Symbol × Option State) + +namespace SingleTapeTM section Cfg -/-- An NTM yields a small-step operational semantics on configurations, which codifies an execution -step. -/ -@[scoped grind =] -def Red (m : SingleTapeTM 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. +/-! +## Configurations of a Turing Machine + +This section defines the configurations of a Turing machine, +the step function that lets the machine transition from one configuration to the next, +and the intended initial and final configurations. -/ -@[scoped grind =] -def MRed (m : SingleTapeTM State Symbol) := Relation.ReflTransGen m.Red + +variable [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) + +instance : Inhabited tm.State := ⟨tm.q₀⟩ + +instance : Fintype tm.State := tm.stateFintype + +instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance /-- -The initial configuration of a deterministic Turing Machine, which consists of the start state of -the machine and the input list of symbols. +The configurations of a Turing machine consist of: +an `Option`al state (or none for the halting state), +and a `BiTape` representing the tape contents. +-/ +structure Cfg : Type where + /-- the state of the TM (or none for the halting state) -/ + state : Option tm.State + /-- the BiTape contents -/ + BiTape : BiTape Symbol +deriving Inhabited + +/-- The step function corresponding to a `SingleTapeTM`. -/ +@[simp] +def step : tm.Cfg → Option tm.Cfg + | ⟨none, _⟩ => + -- If in the halting state, there is no next configuration + none + | ⟨some q', t⟩ => + -- If in state q', perform look up in the transition function + match tm.tr q' t.head with + -- and enter a new configuration with state q'' (or none for halting) + -- and tape updated according to the Stmt + | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩ +/-- +The initial configuration corresponding to a list in the input alphabet. Note that the entries of the tape constructed by `BiTape.mk₁` are all `some` values. This is to ensure that distinct lists map to distinct initial configurations. -/ -def initCfg (m : SingleTapeTM State Symbol) (xs : List Symbol) : Cfg State Symbol := - Cfg.mk₁ m.start xs - -/-- A TM is an acceptor of finite lists of symbols. -/ -@[simp, scoped grind =] -instance : Acceptor (SingleTapeTM State Symbol) Symbol where - Accepts (m : SingleTapeTM State Symbol) (xs : List Symbol) := - ∃ c', c'.state ∈ m.accept ∧ m.MRed (m.initCfg xs) c' - --- /-! --- ## Configurations of a Turing Machine - --- This section defines the configurations of a Turing machine, --- the step function that lets the machine transition from one configuration to the next, --- and the intended initial and final configurations. --- -/ - --- variable [Inhabited Symbol] [Fintype Symbol] (m : SingleTapeTM State Symbol) - --- instance : Inhabited tm.State := ⟨tm.q₀⟩ - --- instance : Fintype tm.State := tm.stateFintype - --- instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance - --- /-- --- The configurations of a Turing machine consist of: --- an `Option`al state (or none for the halting state), --- and a `BiTape` representing the tape contents. --- -/ --- structure Cfg : Type where --- /-- the state of the TM (or none for the halting state) -/ --- state : Option tm.State --- /-- the BiTape contents -/ --- BiTape : BiTape Symbol --- deriving Inhabited - --- /-- The step function corresponding to a `SingleTapeTM`. -/ --- @[simp] --- def step : tm.Cfg → Option tm.Cfg --- | ⟨none, _⟩ => --- -- If in the halting state, there is no next configuration --- none --- | ⟨some q', t⟩ => --- -- If in state q', perform look up in the transition function --- match tm.tr q' t.head with --- -- and enter a new configuration with state q'' (or none for halting) --- -- and tape updated according to the Stmt --- | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩ - - - --- /-- The final configuration corresponding to a list in the output alphabet. --- (We demand that the head halts at the leftmost position of the output.) --- -/ --- def haltCfg (m : SingleTapeTM State Symbol) (xs : List Symbol) : Cfg State Symbol := --- ⟨none, Turing.BiTape.mk₁ xs⟩ +def initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨some tm.q₀, BiTape.mk₁ s⟩ + +/-- The final configuration corresponding to a list in the output alphabet. +(We demand that the head halts at the leftmost position of the output.) +-/ +def haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨none, BiTape.mk₁ s⟩ -@[scoped grind =] -lemma spaceUsed_initCfg (m : SingleTapeTM State Symbol) (xs : List Symbol) : - (m.initCfg xs).spaceUsed = max 1 xs.length := Turing.BiTape.spaceUsed_mk₁ xs - --- @[scoped grind =] --- lemma Cfg.spaceUsed_haltCfg (m : SingleTapeTM State Symbol) (xs : List Symbol) : --- (m.haltCfg s).spaceUsed = max 1 xs.length := Turing.BiTape.spaceUsed_mk₁ xs - -lemma spaceUsed_red {m : SingleTapeTM State Symbol} (c c' : Cfg State Symbol) - (hstep : m.Red c c') : c'.spaceUsed ≤ c.spaceUsed + 1 := by - rcases hstep with ⟨μ, hstep₁, hstep₂, hstep₃⟩ - rcases c' with ⟨s', tape'⟩ - simp only at hstep₁ hstep₂ hstep₃ - cases hm : μ.move with - | none => grind [write, optionMove, = Cfg.spaceUsed] - | some dir => - simpa [hstep₃, Cfg.spaceUsed, Turing.BiTape.optionMove, Turing.BiTape.spaceUsed_write, hm] using - Turing.BiTape.spaceUsed_move (c.tape.write μ.write) dir /-- The space used by a configuration is the space used by its tape. -/ @@ -227,23 +187,23 @@ end Cfg open Cfg --- variable [Inhabited Symbol] [Fintype Symbol] +variable [Inhabited Symbol] [Fintype Symbol] --- /-- --- The `TransitionRelation` corresponding to a `SingleTapeTM Symbol` --- is defined by the `step` function, --- which maps a configuration to its next configuration, if it exists. --- -/ --- @[scoped grind =] --- def TransitionRelation (m : SingleTapeTM State Symbol) (c₁ c₂ : tm.Cfg) : Prop := tm.step c₁ = some c₂ +/-- +The `TransitionRelation` corresponding to a `SingleTapeTM Symbol` +is defined by the `step` function, +which maps a configuration to its next configuration, if it exists. +-/ +@[scoped grind =] +def TransitionRelation (tm : SingleTapeTM Symbol) (c₁ c₂ : tm.Cfg) : Prop := tm.step c₁ = some c₂ /-- A proof of `tm` outputting `l'` on input `l`. -/ -def Outputs (m : SingleTapeTM State Symbol) (l l' : List Symbol) : Prop := - ∃ s ∈ m.accept, m.MRed (initCfg m l) (Cfg.mk₁ s l') +def Outputs (tm : SingleTapeTM Symbol) (l l' : List Symbol) : Prop := + ReflTransGen tm.TransitionRelation (initCfg tm l) (haltCfg tm l') -/-- A proof of `tm` outputting `l'` on input `l` in at most `n` steps. -/ -def OutputsWithinTime (m : SingleTapeTM State Symbol) (l l' : List Symbol) (n : ℕ) := - ∃ s ∈ m.accept, RelatesWithinSteps m.Red (initCfg m l) (Cfg.mk₁ s l') n +/-- A proof of `tm` outputting `l'` on input `l` in at most `m` steps. -/ +def OutputsWithinTime (tm : SingleTapeTM Symbol) (l l' : List Symbol) (m : ℕ) := + RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (haltCfg tm l') m /-- This lemma bounds the size blow-up of the output of a Turing machine. @@ -252,32 +212,20 @@ This is important for guaranteeing that composition of polynomial time Turing ma remains polynomial time, as the input to the second machine is bounded by the output length of the first machine. -/ -lemma output_length_le_input_length_add_time (m : SingleTapeTM State Symbol) (l l' : List Symbol) (t : ℕ) - (h : m.OutputsWithinTime l l' t) : +lemma output_length_le_input_length_add_time (tm : SingleTapeTM Symbol) (l l' : List Symbol) (t : ℕ) + (h : tm.OutputsWithinTime l l' t) : l'.length ≤ max 1 l.length + t := by - obtain ⟨s, hs, steps, hsteps_le, hevals⟩ := h - - -- have := fun a b hstep ↦ spaceUsed_red a b hevals - grind [fun a b hstep ↦ Cfg.spaceUsed_step a b (Option.mem_def.mp hstep)] - grind [hevals.apply_le_apply_add (Cfg.spaceUsed m) obtain ⟨steps, hsteps_le, hevals⟩ := h grind [hevals.apply_le_apply_add (Cfg.spaceUsed tm) fun a b hstep ↦ Cfg.spaceUsed_step a b (Option.mem_def.mp hstep)] section Computers -inductive id.IdState -| read | accept | reject - /-- A Turing machine computing the identity. -/ -def id : SingleTapeTM id.IdState Symbol where - start := .read - tr s μ := match s, μ with - | .read, ⟨some x, none, some .right⟩ => .read - | .read, ⟨none, none, none⟩ => .accept - | _, _ => .reject - -- accept - -- tr _ b := ⟨⟨b, none⟩, none⟩ +def idComputer : SingleTapeTM Symbol where + State := PUnit + q₀ := PUnit.unit + tr _ b := ⟨⟨b, none⟩, none⟩ /-- A Turing machine computing the composition of two other Turing machines. @@ -286,7 +234,7 @@ If f and g are computed by Turing machines `tm1` and `tm2` then we can construct a Turing machine which computes g ∘ f by first running `tm1` and then, when `tm1` halts, transitioning to the start state of `tm2` and running `tm2`. -/ -def comp (tm1 tm2 : SingleTapeTM Symbol) : SingleTapeTM Symbol where +def compComputer (tm1 tm2 : SingleTapeTM Symbol) : SingleTapeTM Symbol where -- The states of the composed machine are the disjoint union of the states of the input machines. State := tm1.State ⊕ tm2.State -- The start state is the start state of the first input machine. @@ -441,7 +389,7 @@ section TimeComputable a proof it outputs `f` in at most `time(input.length)` steps. -/ structure TimeComputable (f : List Symbol → List Symbol) where /-- the underlying bundled SingleTapeTM -/ - m : SingleTapeTM State Symbol + tm : SingleTapeTM Symbol /-- a bound on runtime -/ timeBound : ℕ → ℕ /-- proof this machine outputs `f` in at most `timeBound(input.length)` steps -/ @@ -556,4 +504,4 @@ end PolyTimeComputable end SingleTapeTM -end Cslib.Computability.Turing.SingleTape +end Cslib.Turing diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean index 3e70794ea..c3f2971f4 100644 --- a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean @@ -21,7 +21,7 @@ bidirectional tape (`BiTape`). namespace Cslib.Computability.Turing.SingleTape -open Automata Turing +open Automata /-- A (single-tape) Nondeterministic Turing Machine (NTM) is a nondeterministic automaton equipped with a set of accepting halting states. -/ diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 6a4148843..b1729a43d 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -38,7 +38,7 @@ will not collide. @[expose] public section -namespace Turing +namespace Cslib.Turing /-- A structure for bidirectionally-infinite Turing machine tapes @@ -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 @@ -136,18 +138,13 @@ lemma spaceUsed_mk₁ (l : List Symbol) : (mk₁ l).spaceUsed = max 1 l.length := by cases l with | nil => simp [mk₁, spaceUsed, nil, StackTape.length_nil] - | cons h t => simp [mk₁, spaceUsed, StackTape.length_nil, StackTape.length_map_some]; omega - -lemma spaceUsed_move (t : BiTape Symbol) (d : Dir) : - (t.move d).spaceUsed ≤ t.spaceUsed + 1 := by - cases d <;> grind [move_left, move_right, move, | 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 diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 0ea09fd1e..18b884559 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -38,7 +38,7 @@ advantages and disadvantages. @[expose] public section -namespace Turing +namespace Cslib.Turing /-- An infinite tape representation using a list of `Option` values, @@ -178,4 +178,4 @@ end Length end StackTape -end Turing +end Cslib.Turing From 9721c9111e5265f2a585e5360cbf9ada2c3259a9 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 4 Jun 2026 14:53:43 +0200 Subject: [PATCH 10/10] fix header linter --- Cslib/Computability/Machines/Turing/SingleTape/Defs.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean index f40cd0e67..47aac95e5 100644 --- a/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean @@ -8,10 +8,10 @@ module public import Cslib.Foundations.Data.BiTape -@[expose] public section - /-! # Basic definitions for Turing Machines (TMs) -/ +@[expose] public section + namespace Cslib.Computability.Turing.SingleTape /-- The transition labels used by a single-tape Turing Machine. -/