Labelled Transition Systems (LTS)

Stream: mathlib4

[Fabrizio Montesi]

Hi all, CS researcher from Denmark here. :wave:

I'm looking for feedback on a potential mathlib contribution.

As part of a larger CS project , I made a library for labelled transition systems (LTSs). These are used a lot in theory of CS, especially in concurrency theory, programming languages, and logic. They come with interesting relations, like 'bisimulations', which relate states that are behaviourally equivalent. You can think of them as state machines or directed graphs with minimal assumptions (the set of states doesn't need to be finite, the transition relation doesn't need to be deterministic, etc.).

You can see my current attempt at integrating it with mathlib here: https://github.com/leanprover-community/mathlib4/compare/master...fmontesi:mathlib4:lts

Essentially, I've formalised the fundamental concepts of LTSs and bisimulation (arguably the most established equivalence relation for them) from the reference textbook [Introduction to Bisimulation and Coinduction, Sangiorgi, 2011].

I tried my best to understand and follow the guidelines, but it's my first time navigating all of this. Hopefully I managed. :-)

[Fabrizio Montesi]

One convention that I'm not following on purpose is that I'm calling a couple of type parameters State and Label respectively, instead of \alpha and \beta. I find the resulting code easier to read because I have a clear intuition as to what each type represents, but if this is not ok for mathlib contribs I'm happy to talk about it ofc.

[Wojciech Różowski]

Hello Fabrizio,

I'm glad to see someone formalising Labelled Transition Systems in Lean! I have a brief suggestion that might interest you.

I'm currently working part-time on a project to support coinductive predicates and relations in Lean. It uses lattice theory under the hood but allows you to automatically derive sound coinduction proof principles for a given predicate.

Here's an example of defining language equivalence on DFAs:

def DFA (Q : Type) (A : Type) : Type := Q → (Bool × (A → Q))

def language_equivalent (automaton : DFA Q A) (q₁ q₂ : Q)  : Prop :=
    let ⟨o₁, t₁⟩ := automaton q₁
    let ⟨o₂, t₂⟩ := automaton q₂
    o₁ = o₂ ∧ (∀ a : A, language_equivalent automaton (t₁ a) (t₂ a))
greatest_fixpoint

This automatically gives you a proof principle for language equivalence:

/--
info: language_equivalent.fixpoint_induct {Q A : Type} (automaton : DFA Q A) (x : Q → Q → Prop)
 (y :
   ∀ (x_1 x_2 : Q),
     x x_1 x_2 →
       (automaton x_1).fst = (automaton x_2).fst ∧ ∀ (a : A), x ((automaton x_1).snd a) ((automaton x_2).snd a))
 (x✝ x✝¹ : Q) : x x✝ x✝¹ → language_equivalent automaton x✝ x✝¹
-/

I'm fairly confident you could use this to define bisimulations for LTSes and get the corresponding proof principles for free. The feature is under active development—mutual and mixed (co)induction aren't supported yet (which could help with things like weak bisimulation). Also, the autogenerated lemma name fixpoint_induct may change soon to avoid clashes with partial_fixpoint.

For simple cases, the greatest_fixpoint hint could already be helpful in your setting.

Let me know if you have any questions—I’d be happy to share more details or hear your feedback about the feature!

[Patrick Massot]

Do you have mathematical applications in mind?

[Fabrizio Montesi]

Wojciech Różowski said:

Hello Fabrizio,

I'm glad to see someone formalising Labelled Transition Systems in Lean! I have a brief suggestion that might interest you.

I'm currently working part-time on a project to support coinductive predicates and relations in Lean. It uses lattice theory under the hood but allows you to automatically derive sound coinduction proof principles for a given predicate.

Here's an example of defining language equivalence on DFAs:

def DFA (Q : Type) (A : Type) : Type := Q → (Bool × (A → Q))

def language_equivalent (automaton : DFA Q A) (q₁ q₂ : Q)  : Prop :=
    let ⟨o₁, t₁⟩ := automaton q₁
    let ⟨o₂, t₂⟩ := automaton q₂
    o₁ = o₂ ∧ (∀ a : A, language_equivalent automaton (t₁ a) (t₂ a))
greatest_fixpoint

This automatically gives you a proof principle for language equivalence:

/--
info: language_equivalent.fixpoint_induct {Q A : Type} (automaton : DFA Q A) (x : Q → Q → Prop)
 (y :
   ∀ (x_1 x_2 : Q),
     x x_1 x_2 →
       (automaton x_1).fst = (automaton x_2).fst ∧ ∀ (a : A), x ((automaton x_1).snd a) ((automaton x_2).snd a))
 (x✝ x✝¹ : Q) : x x✝ x✝¹ → language_equivalent automaton x✝ x✝¹
-/

I'm fairly confident you could use this to define bisimulations for LTSes and get the corresponding proof principles for free. The feature is under active development—mutual and mixed (co)induction aren't supported yet (which could help with things like weak bisimulation). Also, the autogenerated lemma name fixpoint_induct may change soon to avoid clashes with partial_fixpoint.

For simple cases, the greatest_fixpoint hint could already be helpful in your setting.

Let me know if you have any questions—I’d be happy to share more details or hear your feedback about the feature!

Hey Wojciech, that looks interesting indeed! I haven't encountered particular problems while doing the metatheory of LTSs yet, but your work might simplify some proofs and be of great help with proving results about particular LTSs in the future (e.g., bisimilarity laws on given languages/semantics).

I'd be happy to see more when you like. :⁠-⁠)

In the meantime, regarding my specific LTS modules, do you see anything that'd prevent using your methods in the future?

[Fabrizio Montesi]

Patrick Massot said:

Do you have mathematical applications in mind?

Are you asking about the usefulness of LTSs or Wojciech's work on coinduction?

[Wojciech Różowski]

Hey Fabrizio,

Thanks—that sounds great! From what I’ve seen, your current setup looks good, and I think it could be adapted to use the greatest_fixpoint machinery without major issues. That's why your post got my attention :)

Personally, I’d find it particularly interesting to eventually see the feature used for bisimulations up to, where you could get stronger proof principles by incorporating algebraic structure. That seems like a promising direction!

By the way, are you planning to eventually formalise something like the semantics of CCS?

[Patrick Massot]

I meant LTSs. The question is why do you want this in mathlib. This is a honest question, I don't know the answer.

[Fabrizio Montesi]

Wojciech Różowski said:

Hey Fabrizio,

Thanks—that sounds great! From what I’ve seen, your current setup looks good, and I think it could be adapted to use the greatest_fixpoint machinery without major issues. That's why your post got my attention :)

Personally, I’d find it particularly interesting to eventually see the feature used for bisimulations up to, where you could get stronger proof principles by incorporating algebraic structure. That seems like a promising direction!

By the way, are you planning to eventually formalise something like the semantics of CCS?

We are formalising choreographic programming and other calculi in Lean, where this might be pretty useful, I'll get in touch when we get there.

I thought of formalising CCS. Maybe if I did, it'd be a good example to try your methods on and sync?

[Fabrizio Montesi]

Patrick Massot said:

I meant LTSs. The question is why do you want this in mathlib. This is a honest question, I don't know the answer.

LTSs are used widely in concurrency theory (including probabilistic models) and programming languages (to prove, e.g., the correctness of compilers, program optimisations, program equivalences when state transition systems have different structures). So I thought it'd make sense to have a common lib, since a lot of results about LTSs are general and heavily reused in a lot of work. LTSs can also be seen as generalisations of the transition functions you see in DFA and NFA (as already in mathlib). Finite graphs, DFAs, NFAs, etc. could be converted into LTSs and then checked for equivalence, for example (I still have to get to the plumbing for this, but it seems straightforward). You can also see bisimulation as a generalisation of graph isomorphism (the structures need not be isomorphic, just the observable behaviour given by the transitions).

[Fabrizio Montesi]

I know they're also used to reason about equivalences in modal logic, but I haven't touched that too much yet.

[Fabrizio Montesi]

Here a pretty nice read about bisimilarity if you're interested:

https://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf

[Fabrizio Montesi]

See for example section 5 about set theory. There are applications to type theory and systems as well IIRC.

[Bashar Hamade]

Fabrizio Montesi said:

Hi all, CS researcher from Denmark here. :wave:

I'm looking for feedback on a potential mathlib contribution.

As part of a larger CS project , I made a library for labelled transition systems (LTSs). These are used a lot in theory of CS, especially in concurrency theory, programming languages, and logic. They come with interesting relations, like 'bisimulations', which relate states that are behaviourally equivalent. You can think of them as state machines or directed graphs with minimal assumptions (the set of states doesn't need to be finite, the transition relation doesn't need to be deterministic, etc.).

You can see my current attempt at integrating it with mathlib here: https://github.com/leanprover-community/mathlib4/compare/master...fmontesi:mathlib4:lts

Essentially, I've formalised the fundamental concepts of LTSs and bisimulation (arguably the most established equivalence relation for them) from the reference textbook [Introduction to Bisimulation and Coinduction, Sangiorgi, 2011].

I tried my best to understand and follow the guidelines, but it's my first time navigating all of this. Hopefully I managed. :-)

Hello there, this is really great to hear . My first ever project was formalising LTS concepts for my Lean seminar project , but sadly I got caught up with lots of other stuff and did not add really much to it , but always wanted to do more..it was my first steps into actually learning lean (natural numbers game and mathematics-in-lean aside)

[Bashar Hamade]

here is what I did in collaboration with @Rida Hamadani :
https://github.com/Calculean/LeanCCS
Like I mentioned, I barely did any work , but would love to work with fellow researchers further in the future

[Fabrizio Montesi]

Nice! My library is intended to provide rails for works like that.

[Shreyas Srinivas]

Fabrizio : If I had to guess, Patrick wants to know how mathematicians would use the library. I think those of us who work on and use automata should try to build this library outside mathlib. Much of this theory is of interest to TCS folks and not necessarily math department folks.

[Bashar Hamade]

I'd say so too , like it is nice to have a formalized library for LTS and its applications, but it does not necessarily tie in with mathlib .

[Shreyas Srinivas]

Perhaps another way to put it is like this : if another part of mathlib might eventually depend on LTS, then it might be sensible to add it to mathlib. I don’t see that as particularly likely.

[Patrick Massot]

This is indeed a very important criterion. But there is also a very pragmatic one: I guess no Mathlib maintainer will be competent to review contributions in this area.

[Patrick Massot]

And really there is a lot of room for a computer science lib. You can do great work with Lean outside of mathematics and Mathlib.

[Shreyas Srinivas]

I would go so far as to say that track B theorists* should have a library of their own.

*for those out of the loop: that’s the logic, model checking, and automata side of CS theory according to European TCS conferences

[Fabrizio Montesi]

Oh, I thought logic and computation were in scope of mathlib because of the many things already in (see pic).5b290aab-2032-45f8-8c7f-693726f08110.jpg

[Fabrizio Montesi]

I'd be happy to start or contribute to a cslib, so that's not a problem. I just wanna figure out the best plan, library-organisation wise.

[Patrick Massot]

The many CS science things in mathlib is a historical accident. There used to be no other library at all, and it's currently very difficult to remove anything from Mathlib.

[Fabrizio Montesi]

I see, thanks for the info. Is this noted anywhere? I couldn't find anything about this when I first searched. It might be good to have a note for newcomers to read.

[Fabrizio Montesi]

Shreyas Srinivas said:

Perhaps another way to put it is like this : if another part of mathlib might eventually depend on LTS, then it might be sensible to add it to mathlib. I don’t see that as particularly likely.

I mean, graph theory might somewhat use it in the future, but I honestly think that if a cslib existed, it'd be a better place for this.

[Rida Hamadani]

I disagree, graph theory definitely belongs to mathlib instead of a cslib, if you prove any graph theory results please PR them (feel free to request my review for any graph theory), we have a very active graph theory library in mathlib.

[Rida Hamadani]

I think the computability library of mathlib can be ported to a cslib however

[Andrew Yang]

A small portion of computability library might be useful to other areas of math. At least recursively enumerable functions are useful to Hilbert 10th problem.

[Fabrizio Montesi]

Rida Hamadani said:

I disagree, graph theory definitely belongs to mathlib instead of a cslib, if you prove any graph theory results please PR them (feel free to request my review for any graph theory), we have a very active graph theory library in mathlib.

Good point. I've been thinking a bit about graph theory.

Here's a mini summary of the connections I see:

• Any labelled digraph (directed graph with labelled edges) is also an LTS.
• Any DFA is also a labelled digraph, and thus an LTS; plus information on start and accepting states, which an LTS doesn't necessarily have.
• Any NFA is also an LTS, with the same remark as above.
• Any Turing Machine is also an LTS, with the same remark.
• Instantiate the Label type for LTS and you can get machines with weighted transitions, probabilistic processes, etc. (For some probabilistic processes/objects, a generalisation of LTSs is needed.)

There are probably more connections.

So LTSs can provide a sort of very general interface for many definitions and results. Things like defining paths, equivalences that ignore structure (like the bisimulation and trace equivalence included in my PR), etc.

I don't know if they'll be used elsewhere in mathlib yet. But if I put them in a 'cslib' instead, that cslib will surely depend on mathlib, and mathlib will thus not be able to use cslib. I don't know where that would leave graph theory.

[Shreyas Srinivas]

I wouldn’t call it cslib either. I prefer “Model Checking Lib” or something similar. All the connections you describe are firmly within the realm of Theoretical CS

[Fabrizio Montesi]

Model Checking would be too narrow. I for one am not using LTSs for model checking in Lean (yet!), but primarily for semantics and certified compilers for now.

[Fabrizio Montesi]

Also, I'd expect a variety of logics (modal logic, linear logic), other equivalences, and calculi (lambda, pi, etc.) to be in the same lib.

[Shreyas Srinivas]

I think that’s included in model checking theory

[Shreyas Srinivas]

It would include various logics, automata, and formulations of games for bisimulations

[Rida Hamadani]

i think blib(for theory b) would be a cute name!

[Fabrizio Montesi]

Shreyas Srinivas said:

I think that’s included in model checking theory

Model checking is usually about verification, and also against finite-state models. It'd be too surprising/specific for people working in some of the topics I mentioned.

[Fabrizio Montesi]

Rida Hamadani said:

i think blib(for theory b) would be a cute name!

Hehe, nice :⁠-⁠)

[Fabrizio Montesi]

Could also be plib (pl theory lib). Although I'm not sure yet as to why one would keep algo theory separate from pl theory? There are important interplays, no?

[Shreyas Srinivas]

PL theory and algo theory are researched by two entirely different communities with \epsilon intersection between them. They don't even speak the same language.

[Shreyas Srinivas]

Also, I doubt that there will be appetite for a PL-Lib, primarily because there are already a bazillion formalisations for every tiny variant of lambda calculi and semantics in Coq and Agda.

[Shreyas Srinivas]

LTSlib would be a good idea.

[Fabrizio Montesi]

Shreyas Srinivas said:

Also, I doubt that there will be appetite for a PL-Lib, primarily because there are already a bazillion formalisations for every tiny variant of lambda calculi and semantics in Coq and Agda.

Many of those are very frustrating for pl researchers because they're incompatible, at least in Coq/Rocq.

I could definitely make an ltslib, but then I'll create a series of libraries in the near future... Mmmh...

[Shreyas Srinivas]

Case in point : There is already an effort underway to port all of iris to lean (not just the Mosel proof mode as was the case before)

[Shreyas Srinivas]

I don't think we're on topic anymore. But to be brief, you won't be able to please PL researchers with a uniform library if they haven't already invented one in Rocq/Coq. That's essentially what Iris did for separation logics. There are so many libraries for PL because there are correspondingly many conceptually different ideas, even if the difference is not vast. There is sufficient common ground on LTSes among PL and model checking communities to justify a library.

[Shreyas Srinivas]

Also since we are on the topic of coinduction, have you checked out what mathlib already has in docs#Computation.corec ?

[Shreyas Srinivas]

There are definitions of even bisimulations. I would suggest not reinventing these definitions unless strictly necessary

[Shreyas Srinivas]

you can use them by defining runs of LTSes in terms of docs#Computation

[Chris Henson]

Shreyas Srinivas said:

Also, I doubt that there will be appetite for a PL-Lib, primarily because there are already a bazillion formalisations for every tiny variant of lambda calculi and semantics in Coq and Agda.

It is a niche, but I am personally very interested in formalizing lambda calculi in Lean! I am currently working on formalizing various categorical and denotational semantics. One appeal to me of this is that there is already a lot of mathematical machinery (categories, CPOs, etc.) built up in a central location with Mathlib.

[Shreyas Srinivas]

Some of it is already there. Scott continuity for example

[Shreyas Srinivas]

Here are \omega-CPOs : https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/OmegaCompletePartialOrder.html

[Shreyas Srinivas]

Scott Continuity : https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/ScottContinuity.html#ScottContinuous

[Shreyas Srinivas]

But I don't think there is anything that takes these pieces to build a comprehensive library for denotational semantics

[Chris Henson]

Shreyas Srinivas said:

Some of it is already there. Scott continuity for example

Yes, I've been using these alongside my own definitions of lambda calculi to formalize some semantics. I also am planning to work on some metaprogramming to allow an easier time producing the boilerplate for locally nameless formalizations.

[Fabrizio Montesi]

@Shreyas Srinivas thanks for all your thoughts. I reply in a single mesg here. I think I see what you mean. I also think that there's space for a foundational pl library, since I wouldn't aim at covering use cases like Iris but more general definitions that are well established. LTS and behavioural equivalences are some of those. They spin off a big formalisation project in our group, and I imagine similarly things could spin off of iris to more general libs.

I just think that there should be some place where LTS and other general definitions about semantics, languages, and related pl topics (and I agree model checking would be a very good part) are kept compatible. Model checking is an important part, but not all. To be clear, I'm not trying to exclude it: I'd love a collab with ppl interested in model checking on this!

I agree we're getting off topic, and a bit into speculation land. I'll open another thread for this later.

Regarding your pointers: yes, I'd checked for similar things in mathlib. I don't think they're what I'm formulating here. A key point of my defs and theorems is that they're minimal and basically as in the pen-and-paper presentation (modulo the expected mods for a mechanisation). For a few things one can make appropriate 'to'-functions.

[Patrick Massot]

And all this discussion proves Mathlib is not a good place: Mathlib maintainers are simply not competent to handle those challenges. We need people who understand all those things maintaining a library about all that. PRing to Mathlib would simply need to tons of stalled PRs frustrating everybody.

[Fabrizio Montesi]

I definitely agree regarding the off-topic stuff (lambda calcs, model checking, logics, ...), which I think belongs to a separate CS lib of some sort.

I'm still in doubt about the main topic here, though (LTSs). Btw, I'm really appreciating this discussion, which I think contains the questions that should always be asked in such cases (thanks!).

In essence, I'm still uncertain that what I've formalised here is confined to CS. So I ask a few questions below, with the intent of excluding that we're not being blindsided by a nomenclature issue here. As an outsider and CS person, I was under the impression that contributions to 'Computability' were welcome, so I phrased my contribution in related terms. Maybe that's not good. (What I describe below might require renaming some symbols in my code and/or some additional work. That'd be fine.)

An LTS is essentially a ternary relation where the first and third sets are the same:

$$S \times L \times S$$

So forget about the name 'LTS' for a second.
It is essentially a labelled digraph (potentially infinite, and with potentially many edges with different labels between the same two nodes). I see there is already a specialised definition for unlabelled digraphs (Digraph). This would be a straight-up generalisation (provide an type L with a single element, and any Digraph can be transformed into an LTS).

Q1: Are such graphs not interesting in math?

Q2: Shouldn't we provide a common API in mathlib for them, which people who use such graphs to model whatever they're interested in can use? (And thus enable them contributing to mathlib general results they develop about such graphs.)

Another pov is extending mathlib to deal with ternary relations (I couldn't find much, but maybe I've missed something?). Here some of the things done in LTSs, like considering the binary relations that come out of fixing the second element of the triple (see, e.g., the 'congruence relation' here: https://en.wikipedia.org/wiki/Ternary_relation), could be easily made into a more general API.

Q3: Are ternary relations and the binary relations that arise from them already formalised, or not interesting in math?

The bisimulation and trace equivalence code I have are the first examples of equivalences one can define on such graphs/ternary relations.

Of course, if these needs/features are already covered by other parts of mathlib or there's agreement that they're not useful in this lib, I'm very happy to make another library. I just don't want this to get lost in a much broader discussion.

[Fabrizio Montesi]

I've received plenty of feedback here and in private mesg/convos. Both for and against, both with good reasons. For info here: for now I'm leaning against. I'll try to think about what kind of cs library this should go in or kickstart. Thank you all for the feedback so far. :)