feat: new design for automata theory, results on regular languages, and deterministic labelled transition systems

Cslib.lean

@@ -1,13 +1,16 @@
+import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.DA
-import Cslib.Computability.Automata.DFA
-import Cslib.Computability.Automata.DFAToNFA
-import Cslib.Computability.Automata.EpsilonNFA
-import Cslib.Computability.Automata.EpsilonNFAToNFA
+import Cslib.Computability.Automata.DAToNA
+import Cslib.Computability.Automata.EpsilonNA
+import Cslib.Computability.Automata.EpsilonNAToNA
 import Cslib.Computability.Automata.NA
-import Cslib.Computability.Automata.NFA
-import Cslib.Computability.Automata.NFAToDFA
+import Cslib.Computability.Automata.NAToDA
+import Cslib.Computability.Automata.OmegaAcceptor
+import Cslib.Computability.Automata.Prod
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Computability.Languages.OmegaRegularLanguage
+import Cslib.Computability.Languages.RegularLanguage
 import Cslib.Foundations.Control.Monad.Free
 import Cslib.Foundations.Control.Monad.Free.Effects
 import Cslib.Foundations.Control.Monad.Free.Fold
@@ -21,6 +24,9 @@ import Cslib.Foundations.Data.Relation
 import Cslib.Foundations.Lint.Basic
 import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Foundations.Semantics.LTS.Bisimulation
+import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Foundations.Semantics.LTS.FLTSToLTS
+import Cslib.Foundations.Semantics.LTS.LTSToFLTS
 import Cslib.Foundations.Semantics.LTS.Simulation
 import Cslib.Foundations.Semantics.LTS.TraceEq
 import Cslib.Foundations.Semantics.ReductionSystem.Basic

Cslib/Computability/Automata/Acceptor.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Languages.Language
+
+namespace Cslib.Automata
+
+/-- An `Acceptor` is a machine that recognises strings (lists of symbols in an alphabet). -/
+class Acceptor (A : Type _) (Symbol : outParam (Type _)) where
+  /-- Predicate that establishes whether a string `xs` is accepted. -/
+  Accepts (a : A) (xs : List Symbol) : Prop
+
+namespace Acceptor
+
+variable {Symbol : Type _}
+
+/-- The language of an `Acceptor` is the set of strings it `Accepts`. -/
+@[scoped grind .]
+def language [Acceptor A Symbol] (a : A) : Language Symbol :=
+  { xs | Accepts a xs }
+
+/-- A string is in the language of an acceptor iff the acceptor accepts it. -/
+@[scoped grind =]
+theorem mem_language [Acceptor A Symbol] (a : A) (xs : List Symbol) :
+  xs ∈ language a ↔ Accepts a xs := Iff.rfl
+
+end Acceptor
+
+end Cslib.Automata

Cslib/Computability/Automata/DA.lean

@@ -1,24 +1,94 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
+Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.NA
+import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Computability.Automata.Acceptor
+import Cslib.Computability.Automata.OmegaAcceptor
+import Cslib.Computability.Languages.OmegaLanguage
 
+/-! # Deterministic Automata
 
+A Deterministic Automaton (`DA`) is an automaton defined by a transition function equipped with an
+initial state.
 
-/-! # Deterministic Automaton
+Automata with different accepting conditions are then defined as extensions of `DA`.
+These include, for example, a generalised version of DFA as found in the literature (without
+finiteness assumptions), deterministic Buchi automata, and deterministic Muller automata.
 
-A Deterministic Automaton (DA) is an automaton defined by a transition function.
+## References
+
+* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
+  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
-namespace Cslib
+namespace Cslib.Automata
 
-structure DA (State : Type _) (Symbol : Type _) where
+structure DA (State Symbol : Type*) extends FLTS State Symbol where
   /-- The initial state of the automaton. -/
   start : State
-  /-- The transition function of the automaton. -/
-  tr : State → Symbol → State
 
-end Cslib
+namespace DA
+
+variable {State : Type _} {Symbol : Type _}
+
+/-- A deterministic automaton that accepts finite strings (lists of symbols). -/
+structure FinAcc (State Symbol : Type*) extends DA State Symbol where
+  /-- The accept states. -/
+  accept : Set State
+
+namespace FinAcc
+
+/-- A `DA.FinAcc` 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. -/
+@[scoped grind =]
+instance : Acceptor (DA.FinAcc State Symbol) Symbol where
+  Accepts (a : DA.FinAcc State Symbol) (xs : List Symbol) := a.mtr a.start xs ∈ a.accept
+
+end FinAcc
+
+/-- Helper function for defining `run` below. -/
+@[simp, scoped grind =]
+def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State
+  | 0 => da.start
+  | n + 1 => da.tr (run' da xs n) (xs n)
+
+/-- Infinite run. -/
+@[scoped grind =]
+def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
+
+open List Filter
+
+/-- Deterministic Buchi automaton. -/
+structure Buchi (State Symbol : Type*) extends DA State Symbol where
+  /-- The accept states -/
+  accept : Set State
+
+namespace Buchi
+
+@[scoped grind =]
+instance : ωAcceptor (Buchi State Symbol) Symbol where
+  Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) := ∃ᶠ k in atTop, a.run xs k ∈ a.accept
+
+end Buchi
+
+/-- Deterministic Muller automaton. -/
+structure Muller (State Symbol : Type*) extends DA State Symbol where
+  /-- The accepting set of sets of states. -/
+  accept : Set (Set State)
+
+namespace Muller
+
+@[scoped grind =]
+instance : ωAcceptor (Muller State Symbol) Symbol where
+  Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) := (a.run xs).infOcc ∈ a.accept
+
+end Muller
+
+end DA
+
+end Cslib.Automata

Cslib/Computability/Automata/DAToNA.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DA
+import Cslib.Computability.Automata.NA
+import Cslib.Foundations.Semantics.LTS.FLTSToLTS
+
+/-! # Translation of Deterministic Automata into Nonodeterministic Automata.
+
+This is the general version of the standard translation of DFAs into NFAs. -/
+
+namespace Cslib.Automata.DA
+
+variable {State : Type _} {Symbol : Type _}
+
+section NA
+
+/-- `DA` is a special case of `NA`. -/
+@[scoped grind =]
+def toNA (a : DA State Symbol) : NA State Symbol :=
+  { a.toLTS with start := {a.start} }
+
+instance : Coe (DA State Symbol) (NA State Symbol) where
+  coe := toNA
+
+namespace FinAcc
+
+/-- `DA.FinAcc` is a special case of `NA.FinAcc`. -/
+@[scoped grind =]
+def toNAFinAcc (a : DA.FinAcc State Symbol) : NA.FinAcc State Symbol :=
+  { a.toNA with accept := a.accept }
+
+open Acceptor in
+open scoped FLTS NA.FinAcc in
+/-- The `NA` constructed from a `DA` has the same language. -/
+@[scoped grind _=_]
+theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
+    language a.toNAFinAcc = language a := by
+  ext xs
+  constructor
+  · grind
+  · intro _
+    use a.start
+    grind
+
+end FinAcc
+
+end NA
+
+end Cslib.Automata.DA