feat (Computability/Automata): Automata theory based on LTS, including DFA, NFA, EpsilonNFA, and translations between them, plus supporting theorems generalised to LTS #83

fmontesi · 2025-10-06T10:44:58Z

No description provided.

…lication to automata theory to prove the subset construction correct

…ectness

github-actions · 2025-10-06T10:46:45Z

Cslib.lean

-import Cslib.Foundations.Semantics.Lts.Bisimulation
-import Cslib.Foundations.Semantics.Lts.TraceEq
+import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.Bisimulation


[imports (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

import Cslib.Foundations.Semantics.LTS.Bisimulation

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.NA

import Cslib.Computability.Automata.NFA

import Cslib.Computability.Automata.NFAToDFA

import Cslib.Foundations.Control.Monad.Free

import Cslib.Foundations.Control.Monad.Free.Effects

import Cslib.Foundations.Control.Monad.Free.Fold

import Cslib.Foundations.Data.FinFun

import Cslib.Foundations.Data.HasFresh

import Cslib.Foundations.Data.Relation

import Cslib.Foundations.Semantics.LTS.Bisimulation

github-actions · 2025-10-06T10:46:46Z

Cslib.lean

+import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.Bisimulation
+import Cslib.Foundations.Semantics.LTS.TraceEq
 import Cslib.Foundations.Data.Relation


[imports (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

import Cslib.Foundations.Data.Relation

import Cslib.Foundations.Semantics.LTS.Simulation

import Cslib.Foundations.Data.Relation

github-actions · 2025-10-06T10:46:46Z

Cslib.lean

 import Cslib.Languages.CombinatoryLogic.Defs
 import Cslib.Languages.CombinatoryLogic.Basic


[imports (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

import Cslib.Languages.CombinatoryLogic.Defs

import Cslib.Languages.CombinatoryLogic.Basic

import Cslib.Foundations.Semantics.ReductionSystem.Basic

import Cslib.Foundations.Syntax.HasAlphaEquiv

import Cslib.Foundations.Syntax.HasSubstitution

import Cslib.Foundations.Syntax.HasWellFormed

import Cslib.Languages.CCS.Basic

import Cslib.Languages.CCS.BehaviouralTheory

import Cslib.Languages.CCS.Semantics

chenson2018

I think we should settle early on a style preference for explicit and scoped grind.

I made several grind suggestions, but I am still bothered by a few places where grind fails unexpectedly, as noted in your TODO. As I note in a comment, I think at least some of it it is because of failure to how structures extend each other.

chenson2018 · 2025-10-06T14:35:09Z

Cslib/Computability/Automata/DA.lean

+
+A Deterministic Automaton (DA) is an automaton defined by a transition function.
+-/
+structure DA (State : Type _) (Symbol : Type _) where


Suggested change

structure DA (State : Type _) (Symbol : Type _) where

structure DA (State Symbol : Type*) where

I still don't get what the advantage of Type* is given that Type _ (even by listing the identifiers before it) does the same thing and seems native?

My opinion is that it is more readable and as a side benefit more compact. As is, you have to twice interpret an annotation and _, whereas with Type* you get one piece of syntax that says "all these types are in arbitrary universes". As this is a very stable piece of Mathlib syntax, I do not find an advantage in the native spelling.

Not a deal breaker for me, this can be considered personal preference.

I see what you mean, although I still find (State : Type _) (Symbol : Type _) to be less ambiguous. I'll mull over it.

chenson2018 · 2025-10-06T14:37:14Z

Cslib/Computability/Automata/DFA.lean

+/-- A Deterministic Finite Automaton (DFA) consists of a labelled transition function
+`tr` over finite sets of states and labels (called symbols), a starting state `start` and a finite
+set of accepting states `accept`. -/
+structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where


Suggested change

structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where

structure DFA (State Symbol : Type*) extends DA State Symbol where

Cslib/Computability/Automata/DFA.lean

Cslib/Computability/Automata/DFAToNFA.lean

Cslib/Computability/Automata/EpsilonNFAToNFA.lean

Cslib/Computability/Automata/DFAToNFA.lean

fmontesi · 2025-10-06T18:25:33Z

I think we should settle early on a style preference for explicit and scoped grind.

I made several grind suggestions, but I am still bothered by a few places where grind fails unexpectedly, as noted in your TODO. As I note in a comment, I think at least some of it it is because of failure to how structures extend each other.

Yeah, I've been putting grind annotations in many places because we haven't got a convention yet. Let's settle on explicit and scoped then, I've been using that in another project and seems to work well.

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

fmontesi · 2025-10-06T19:02:35Z

Thanks @chenson2018, I think I'm done with all the changes that make immediate sense. :-)

ctchou · 2025-10-06T18:20:45Z

Cslib/Computability/Automata/DA.lean

+  /-- The set of accepting states of the automaton. -/
+  accept : Set State


Could you move the accept condition to DFA? I want to define (for example) deterministic Muller automata by extending DA, but such automata have an acceptance condition of type: accept : Set (Set State).

ctchou · 2025-10-06T18:25:13Z

Cslib/Computability/Automata/NA.lean

+structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where
+  /-- The set of initial states of the automaton. -/
+  start : Set State
+  /-- The set of accepting states of the automaton. -/


Could you move the accept condition to NFA and \epsilonNFA? Automata on infinite words have acceptance conditions of types like Set (Set State) (Muller condition) and Set (Set State × Set State)) (Rabin condition).

ctchou · 2025-10-06T18:36:42Z

Cslib/Computability/Automata/NFAToDFA.lean

+
+/-- Converts an `NFA` into a `DFA` using the subset construction. -/
+@[grind]
+def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := {


Perhaps you can separate out the start and tr components to a NAtoDA.lean, so that other extensions of NA and DA for omega-automata can also use the results? Note that all the heavy-lifting in the proof of the subset construction involve only the start and tr components anyway.

ctchou · 2025-10-06T18:42:38Z

Cslib/Computability/Automata/EpsilonNFA.lean

+Internally, ε (`Option.none`) is treated as the `τ` label of the underlying transition system,
+allowing for reusing the definitions and results on saturated transitions of `LTS` to deal with
+ε-closure. -/
+structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) where


Instead of extending NA to obtain εNFA, it may be cleaner to have an εNA (namely, an NA that supports ε-transitions) and extend εNA to obtain εNFA. My comments about separating out the main part of the subset construction from NFA to NA also applies, mutatis mutandis, here. I think such a design would be more orthogonal than the current one.

I agree with both comments, though I'd have to test grind (seems to be obstructed a bit by structure extensions sometimes). I'll implement them in a separate PR when I have some time for this again, since it seems like a backwards compatible extension to what is here. (Or, if you like, feel free to submit one.)

…ata in the future

chenson2018

Changes look good to me, what is remains is minor. I will leave approval to you all since it looks like you're still settling on where certain fields go.

fmontesi added 16 commits September 29, 2025 10:09

feat: introduce NA for discussion

8561629

chore: rename Dfa to DFA and Lts to LTS

cae4e0d

feat: introduce DA, plus some documentation for automata

69b0c1e

feat: move general defs and theorems from DFA to DA

b1e5014

feat: add LTS.setImage, the image of a set of states

362ec6a

chore: rename LTS.Image and LTS.OutgoingLabels with lowercase initials

40585d4

chore: fix casing of Sum.isLeft/RightP

33f0331

feat (LTS): union of two LTSs with the same state and label types

f113731

feat: extension of LTS theory to deal with image transitions, and app…

bd0b568

…lication to automata theory to prove the subset construction correct

docs: alternative shapes for transitions in NA

898d941

feat: add NFA and EpsilonNA

fee5bad

feat: EpsilonNA.toNAWithoutEpsilon

d00c2fb

feat (EpsilonNA): conversion of EpsilonNA into NA, with proof of corr…

a76afcb

…ectness

chore: Split automata theory translations into multiple files

bdf5285

chore: renaming to toNFA`

75f0bf0

chore: spacing

a4eb319

fmontesi requested a review from chenson2018 as a code owner October 6, 2025 10:44

github-actions bot reviewed Oct 6, 2025

View reviewed changes

chenson2018 previously requested changes Oct 6, 2025

View reviewed changes

fmontesi and others added 10 commits October 6, 2025 20:26

Update Cslib/Computability/Automata/DFA.lean

87336de

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Update Cslib/Computability/Automata/DFAToNFA.lean

c71741a

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Update Cslib/Computability/Automata/EpsilonNFAToNFA.lean

740c26c

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Update Cslib/Computability/Automata/EpsilonNFAToNFA.lean

f915549

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Update Cslib/Computability/Automata/DFAToNFA.lean

b1f9cb2

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Update Cslib/Computability/Automata/DFAToNFA.lean

81cb3a1

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Apply suggestion from @chenson2018

2b5ac8f

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Apply suggestion from @chenson2018

066a62b

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Apply suggestion from @chenson2018

0ff5f1a

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Apply suggestion from @chenson2018

a48173f

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

fmontesi added 2 commits October 6, 2025 20:52

grind annotations

4b17e09

scope all the grinds

ec94a20

ctchou reviewed Oct 6, 2025

View reviewed changes

Move accept conditions around for better extensibility to omega autom…

9a01e84

…ata in the future

chenson2018 reviewed Oct 6, 2025

View reviewed changes

ctchou mentioned this pull request Oct 6, 2025

feat: An initial version of Buchi and Muller automata #85

Open

fmontesi merged commit e9cfac9 into main Oct 7, 2025
4 checks passed

-import Cslib.Foundations.Semantics.LTS.Bisimulation
+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.NA
+import Cslib.Computability.Automata.NFA
+import Cslib.Computability.Automata.NFAToDFA
+import Cslib.Foundations.Control.Monad.Free
+import Cslib.Foundations.Control.Monad.Free.Effects
+import Cslib.Foundations.Control.Monad.Free.Fold
+import Cslib.Foundations.Data.FinFun
+import Cslib.Foundations.Data.HasFresh
+import Cslib.Foundations.Data.Relation
+import Cslib.Foundations.Semantics.LTS.Bisimulation

	import Cslib.Foundations.Data.Relation
	import Cslib.Foundations.Semantics.LTS.Simulation
	import Cslib.Foundations.Data.Relation

		import Cslib.Languages.CombinatoryLogic.Defs
		import Cslib.Languages.CombinatoryLogic.Basic

-import Cslib.Languages.CombinatoryLogic.Defs
-import Cslib.Languages.CombinatoryLogic.Basic
+import Cslib.Foundations.Semantics.ReductionSystem.Basic
+import Cslib.Foundations.Syntax.HasAlphaEquiv
+import Cslib.Foundations.Syntax.HasSubstitution
+import Cslib.Foundations.Syntax.HasWellFormed
+import Cslib.Languages.CCS.Basic
+import Cslib.Languages.CCS.BehaviouralTheory
+import Cslib.Languages.CCS.Semantics

	structure DA (State : Type _) (Symbol : Type _) where
	structure DA (State Symbol : Type*) where

	structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
	structure DFA (State Symbol : Type*) extends DA State Symbol where

		/-- The set of accepting states of the automaton. -/
		accept : Set State

feat (Computability/Automata): Automata theory based on LTS, including DFA, NFA, EpsilonNFA, and translations between them, plus supporting theorems generalised to LTS #83

feat (Computability/Automata): Automata theory based on LTS, including DFA, NFA, EpsilonNFA, and translations between them, plus supporting theorems generalised to LTS #83

Conversation

fmontesi commented Oct 6, 2025

Uh oh!

github-actions bot Oct 6, 2025

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 6, 2025

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 6, 2025

Choose a reason for hiding this comment

Uh oh!

chenson2018 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

fmontesi commented Oct 6, 2025

Uh oh!

fmontesi commented Oct 6, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chenson2018 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants