cslib

Stream: computer science

[Fabrizio Montesi]

Hi all,

Following the discussion in #mathlib4 > Labelled Transition Systems (LTS), last month I created a mathlib-based 'cs library' and started porting reusable definitions from the more specialised formalisation projects at our research group. It has a rather general name for now (cslib), as discussed in the original topic here on Zulip, since the point is to provide general definitions and theorems that can be used in other CS libraries. The initial code and documentation pipeline are now in place:

• Code: https://github.com/cs-lean/cslib
• Docs: https://cs-lean.github.io/

One aim is to provide model/language-agnostic APIs, which could be interesting for (including but not limited to) concurrency theory, compilers, database theory, distributed algorithms, logic, model checking, programming languages, etc. So we've started by formalising a big part of the textbook 'Introduction to Bisimulation and Coinduction' by Sangiorgi. See, for example, https://cs-lean.github.io/Cslib/Semantics/LTS/Basic.html and https://cs-lean.github.io/Cslib/Semantics/LTS/Bisimulation.html.
As textbook exercises, there are definitions of Milner's CCS (as defined in the intro to bisimulation textbook, including a proof that bisimilarity is a congruence) and Girard's linear logic. There are also some well-known results, like some characterisations of weak bisimilarity and the equality of bisimilarity and trace equivalence for deterministic LTSs.

There are already two formalisation efforts based on the library (https://www.chords.dev/, where among other things we're making a choreographic programming language with a certified compiler, and the code of a course we teach at our uni), which are in sync with the library. We hope that more can find this useful, and in particular see value in keeping some sort of API compatibility when it comes to similar things.

It might be that there are benefits in merging this with other efforts (I've noticed a parallel channel #CSLib has started since the discussion in #mathlib4 > Labelled Transition Systems (LTS); I'll try to look into it), connecting to other libs (#iris-lean?), refocusing this (more aimed at programming, logic, and semantics?), and/or putting it under leanprover-community (mentioned this to @Mario Carneiro some time ago). So, comments are welcome and, if you're interested, please do reach out. :) For now, we're at the stage of 'getting stuff out there' whenever we find some time (currently not a whole lot given the upcoming summer holidays!).

[Wrenna Robson]

Super exciting!

[Eric Taucher]

To admins: Should this topic be moved to the channel CSLIb? (#CSLib )

[Shreyas Srinivas]

When you say “distributed algorithms” what sort of algorithms do you have in mind?

[Fabrizio Montesi]

Shreyas Srinivas said:

When you say “distributed algorithms” what sort of algorithms do you have in mind?

Could include consensus, commit protocols, leader election, replication, distributed data structures (e.g., CRDTs, distributed hashmaps, Key-Value stores), study of lock-free and wait-free algorithms, etc.

[Shreyas Srinivas]

Ah, so you are looking at asynchronous fully connected networks

[Fabrizio Montesi]

well observed, in distributed algorithms that covers a lot. (but i wouldn't limit the library only to that, necessarily.)

[Kevin Buzzard]

Eric Taucher said:

To admins: Should this topic be moved to the channel CSLIb? (#CSLib )

This seems to be about something completely different but with the same name?

[Eric Taucher]

Kevin Buzzard said:

This seems to be about something completely different but with the same name?

Thanks for looking at the question.

Should the name then be changed?

I am not an expert in this but if it confused me might confuse others latter down the line.

[Kevin Buzzard]

The Amazon/DeepMind-backed CSLib is the topic of the #CSLib channel; here are slides about that project.

[Shreyas Srinivas]

@Eric : I think the name “CSLib” cannot be exclusive to any group, because, in its meaning, the name casts too wide a net. Unless there is a very board academic consensus across multiple CS subfields, it should be upto the respective groups to call their libraries CSLib if they so choose. As far as I can tell, this name has been floating around multiple groups and even channels on this Zulip.

[Eric Wieser]

Ultimately only one group should claim import CSLib, but reservoir's structure allows foo/cslib and bar/cslib to both exist as lakefile dependencies

[Eric Wieser]

FWIW, it seems like python didn't attempt to regulate multiple packages claiming the same incompatible import, instead leaving clashing packages to resolve things between themselves.

[Shreyas Srinivas]

Ideally what is called #CSLib should have been named differently to not give the impression that it claims primacy by fiat over all CS libraries in lean. Given its stated scope it might have been nicer to call it BasicsOfCS or UndergradCS.

[Eric Wieser]

I think starting mathlib off as UndergradMath would have been a needless obstacle for growth / created annoying renaming work down the line

[Shreyas Srinivas]

I have discussed this elsewhere and prefer DMs to continue further detailed discussions. There is much more shared basic conceptual content among math folks than CS folks. Given these huge gaps, various subfields specific libraries launched in consultation with the respective communities would serve both research and pedagogy better.

[Chris Henson]

I second the recommendation to change the name to avoid confusion. Is there a more descriptive name that would indicate the scope of the library?

As an example, I was wondering if contributions related to lambda calculi would be welcome. I am working in this area and would upstream if desired, though there would need to be some discussion about what representations (locally nameless, intrinsic/extrinsic, etc.) are preferred.

[Shreyas Srinivas]

A sort of “network of libraries” where shared content permeates to a CSUtils library would work better for CS than mathlib’s monorepo approach

[Shreyas Srinivas]

In any case, unless a large number of leading researchers and associations like ACM SIGs in all subfields of CS publicly signed on to the initiative, calling something CSlib sounds a bit off. It makes a claim to a mathlib-like special role without involving everyone. The situation in CS is different from math. Some areas of CS are already heavily invested in formal methods and ITPs. In other subfields, different researchers are starting to take up formalisation in ways that suit their area. The situation is a bit different from when mathlib started

[Fabrizio Montesi]

Chris Henson said:

As an example, I was wondering if contributions related to lambda calculi would be welcome. I am working in this area and would upstream if desired, though there would need to be some discussion about what representations (locally nameless, intrinsic/extrinsic, etc.) are preferred.

Yes, definitely welcome. I think we should have a syntax*, which people can then use as basis to formalise all sorts of different evaluation strategies and theorems about them. We should try to have generic signatures for what a 'reduction semantics' is, etc., just like for LTSs. In fact, the LTS.toRel def we already have is designed for the usual 'a reduction semantics is an LTS with only \tau-labels'.

*: There are multiple ways even to define syntax, as you note. I think the different approaches could live in the same library. For example, the standard pen-and-paper with free/bound names and alpha-renaming, the abstract syntax approach, etc. Thus enabling people to show transformations between those.

[Fabrizio Montesi]

Chris Henson said:

Is there a more descriptive name that would indicate the scope of the library?

I don't know yet. Depends a bit on whether there are other research groups/people in the community that see value in sharing and working on compatible APIs/types for CS formalisations. I'm in the process of reaching out to other research groups.

[Fabrizio Montesi]

For now I'm loosely following the ACM classification system in the namespaces within the lib. (It's not really a perfect match for a library nor really up to date, hence the 'loosely'.)

[Fabrizio Montesi]

To admins: Could we get a 'Computer Science' channel for discussions about this and other CS-related topics, not necessarily linked to a specific library/project?

I'd like this topic and #general > Lambda calculus to be moved there, too.

[Fabrizio Montesi]

@Chris Henson @Thomas Waring @Kenny Lau: mathlib has a new definition for Rel (sets of pairs), which doesn't work with what we have, so our files won't compile with current mathlib until we address this.

What we have (the standard type for relations) is what is called Relation (that's unchanged), but Relation doesn't have a definition so we don't get dot-notation.
So I'm creating a file Cslib.Data.Relation with:

def Relation (α β : Type*) := α → β → Prop

and I'm essentially adding all the definitions we need. However, I cannot use the dot-notation for useful things like Relation.comp like this. So I gotta define Relation.comp as the old Rel.comp, etc...

I'm starting to wonder if this is gonna be very confusing. Maybe I should just bite the bullet create a new type FRel (for functional relation) or CRel (for Curried Relation), still under Cslib.Data, and import there everything we need from the old Rel?

Thoughts are very welcome. We're gonna use this a lot, probably, because of all term equivalences, reduction relations, restrictions of LTSs, etc.

[Fabrizio Montesi]

Fabrizio Montesi said:

To admins: Could we get a 'Computer Science' channel for discussions about this and other CS-related topics, not necessarily linked to a specific library/project?

I'd like this topic and #general > Lambda calculus to be moved there, too.

Pinging this since we're starting to have a few parallel discussions, which would amount to at least 5 topics (General definitions for CS, Lambda Calculus, SKI calculus, Labelled Transition Systems, Notation for formal languages).

[Eric Wieser]

are you looking for docs#Relation.Comp ?

[Fabrizio Montesi]

Eric Wieser said:

are you looking for docs#Relation.Comp ?

Lean complains when I try to do r.Comp s (if r and s are Relations as I defined above).

[Eric Wieser]

I would be in favor of adding abbrev Relation (α β : Type*) := α → β → Prop to mathlib and adjusting the definition of the rest of the Relation file accordingly

[Eric Wieser]

Though I could also see the argument for reverting the changes to Rel in mathlib and introducing CurriedRel in mathlib in its place

[Eric Wieser]

The change was made without much discussion, presumably on the premise that no one was using it anyway. Given it's being used after all, a revert seems reasonable

[Thomas Waring]

FWIW in my branch (development of SKI combinatory logic) I've been defining transitions as SKI → SKI → Prop, and using the API at Mathlib.Logic.Relation pretty heavily

[Fabrizio Montesi]

Thomas Waring said:

FWIW in my branch (development of SKI combinatory logic) I've been defining transitions as SKI → SKI → Prop, and using the API at Mathlib.Logic.Relation pretty heavily

One more reason for which we should settle this matter.

[Fabrizio Montesi]

Eric Wieser said:

The change was made without much discussion, presumably on the premise that no one was using it anyway. Given it's being used after all, a revert seems reasonable

We're downstream, so it was very hard to know. But having a good API for relations is really important in CS. I'd be very happy with either:

• Calling SRel (set-based Rel) the current Rel, restore the previous Rel, and merge all the useful stuff from Relation into Rel.
• Adding the abbreviation to Relation, renaming it to Data.CRel (Curried Rel), and make all defs that do exactly the same thing as in Rel have the same name (so Comp becomes comp, etc.).

[Eric Wieser]

Note that comp is currently Comp because it returns a _ -> _ -> Prop rather than a Relation _ _

[Eric Wieser]

My guess is that @Mario Carneiro and @Yaël Dillies will have opinions here

[Patrick Massot]

Eric Wieser said:

The change was made without much discussion, presumably on the premise that no one was using it anyway. Given it's being used after all, a revert seems reasonable

It seems to me this was discussed a lot and was frozen for a very long time.

[Thomas Waring]

Eric Wieser said:

The change was made without much discussion, presumably on the premise that no one was using it anyway. Given it's being used after all, a revert seems reasonable

FWIW I found the justification in the pull request #25587 convincing

[Thomas Waring]

I have opened a pull request of my development of the SKI calculus — comments, edits & general advice are very welcome & appreciated :-)

Ping @Fabrizio Montesi @Chris Henson

[Yaël Dillies]

I would be okay with a rename of Rel to SetRel or alike, but I do believe having abbrev Rel (α β : Type*) := α → β → Prop is mostly a distraction. A bit like how we don't have abbrev Sequence (α : Type*) := ℕ → α

[Fabrizio Montesi]

Thomas Waring said:

Eric Wieser said:

The change was made without much discussion, presumably on the premise that no one was using it anyway. Given it's being used after all, a revert seems reasonable

FWIW I found the justification in the pull request #25587 convincing

I think @Yaël Dillies did a pretty good job there, too, hence my second proposal. I just want curried relations to have good support, dot-notation, etc.

[Fabrizio Montesi]

Yaël Dillies said:

I would be okay with a rename of Rel to SetRel or alike, but I do believe having abbrev Rel (α β : Type*) := α → β → Prop is mostly a distraction. A bit like how we don't have abbrev Sequence (α : Type*) := ℕ → α

I couldn't figure out how to get good dot-notation support without an abbrev. But I'm no expert on lean notation. Suggestions welcome. :grinning_face_with_smiling_eyes:

[Yaël Dillies]

Why do you want dot notation? Can I convince you to use notation instead? :slight_smile:

[Yaël Dillies]

(there are perfectly valid answers to the first question, but I'm hoping your answer isn't "I want to write r.comp s")

[Fabrizio Montesi]

Yaël Dillies said:

(there are perfectly valid answers to the first question, but I'm hoping your answer isn't "I want to write r.comp s")

I do use r.inv and r.comp s, as well as r.upTo s (our lib lingo for s.comp (r.comp s)). Is that bad?

[Fabrizio Montesi]

Also, we already use ~[r] (and many variants of it) for 'equivalent according to r', which doesn't mean 'related by r', but that's another story (we could just find other notation for 'are related by r').

[Fabrizio Montesi]

(~ is standard notation for bisimilarity on transition relations)

[Yaël Dillies]

Fabrizio Montesi said:

Also, we already use ~[r] (and many variants of it) for 'equivalent according to r', which doesn't mean 'related by r', but that's another story (we could just find other notation for 'are related by r').

That's okay. You can simply not open Rel and there won't be a notation clash

[Yaël Dillies]

Fabrizio Montesi said:

I do use r.inv and r.comp s, as well as r.upTo s (our lib lingo for s.comp (r.comp s)). Is that bad?

I don't know about r.inv, but you should probably introduce notation r ○ s for r.comp s

[Fabrizio Montesi]

Agreed. Still stuck on dot-notation for the rest though. So regardless of which name we use for 'standard' relations, I'd still like to have an abbrev for it. (Unless there's a good alternative?)

[Fabrizio Montesi]

@Yaël Dillies have I convinced you that we could really use an abbrev for the standard relation type? :grinning_face_with_smiling_eyes:

[Notification Bot]

This topic was moved here from #general > cslib by Bryan Gin-ge Chen.

[Ching-Tsun Chou]

I just discovered this thread. (Thanks for creating the CS channel!) It may be worth mentioning that I have been formalizing some automata theory in Lean:
https://github.com/ctchou/AutomataTheory
My current goal is to prove the closure of ω-regular languages under complementation, which I think I will reach in a month or two.

[Fabrizio Montesi]

Looks interesting, and definitely in scope. How does it relate to the automata already in Mathlib? Also, this might interest you: https://cs-lean.github.io/Cslib/Semantics/LTS/Basic.html

[Ching-Tsun Chou]

Currently not related and some results are duplicated. My main interest is to formalize some of the theory of automata on infinite words, while the automata theory in mathlib is concerned only with finite words. I also found the automata theory in mathlib not very convenient for my purpose. For example, the meaning of accepting states in automata on infinite words is very different from that in automata on finite words and the two need to be treated in different ways in some automata constructions. So it is more convenient for me to not include accepting states as part of an automaton as is done in mathlib's automata theory. I also try to treat the two types of automata in as uniform a way as possible and in many cases the same automata construction is used to prove the same or similar properties of automata on finite words and autamota on infinite words. For example, the same "loop" construction on automata is used to show that regular languages are closed under Kleene star and the ω-power of a regular language is an ω-regular language, even though the former result is already in mathlib.

[Fabrizio Montesi]

It looks like some of your definitions/theorems could actually be written for LTS, and thus apply to any transition system.

[Ching-Tsun Chou]

I wouldn't be surprised. After all, an automaton is a type of LTS. But at present I'm more interested in proving results at the level of languages, such as various closure properties of regular and ω-regular languages. Those properties are robust and do not depend on the details of the automata or LTS that are used to define them. (For example, the notion of regular languages can be defined using either deterministic or nondeterministic automata and the latter can support or not support epsilon transitions and have a single initial state or allow multiple initial states.). Of course, one has to pick a particular definition and work with it. But the particular details of the definition are not ultimately interesting.

[Ching-Tsun Chou]

It seems to me that this is a general difficulty in formalizing the mathematics in computer science. In any computational model, there are often a lot of details which are ultimately uninteresting and arbitrary but which must be pinned down so that formal reasoning can proceed. For example, to formalize the undecidability of the halting problem, one has to pin down the details of the Turing machines that one use: What is the alphabet? Is the machine deterministic or nondeterministic? How many tapes? What is the encoding of TMs for feeding them into a universal TM? And so on and on. None of those details is ultimately interesting, but they must be pinned down before any formal proof can proceed.

[Notification Bot]

5 messages were moved from this topic to #computer science > Linear logic by Fabrizio Montesi.

[Tanner Duve]

would cslib maintainers be interested if I added something like the "Imp" language defined in Software Foundations (similarly WHILE defined in Hitchhikers Guide to Logical Verification), along with operational and denotational semantics? I think this would be good for the pedagogical/university curriculum aspect of cslib.

[Fabrizio Montesi]

Yes! Please split it in multiple PRs when reasonable though, for the sake of reviewing. For example, a first PR for IMP with just syntax and operational semantics would be nice.

[Tanner Duve]

Sounds good! Yeah I figured the PRs could be something like 1. syntax + big step semantics 2. small step semantics and 3. fixed points/lattice stuff and denotational semantics

[Chris Henson]

I think this would be good to have! I was thinking of doing some denotational semantics as well, but I think I'd like to do this in a well-scoped style. It would be nice to show that Mathlib's docs#OmegaCompletePartialOrder works for semantics of PCF for instance.

[Chris Henson]

Actually I should ask, will you have binding for this? If so what style of formalization were you thinking?

[Tanner Duve]

Software Foundations just defines an environment of type String -> Int and the Imp language has an assign x v command that just updates the environment to map x to v, but there is nothing like anonymous functions or let .. in statements

[Tanner Duve]

So I don't think bindings are used here?

[Mahdi Ghadimi]

Hi all! i don't know if this is a right place to ask but I'm a 3rd year CS student really passionate about formal methods and PL theory. The project looks awesome and I'd love to help out.

I have a background in theory of computation, automata, etc., and I'm eager to get my hands dirty. Are there any newcomer-friendly areas where I could start digging in? Any guidance would be greatly appreciated.

[Fabrizio Montesi]

Some areas:

• We're discussing, porting, and proving results about automata theory.
• We're also soon gonna be ready to accept contributions on verified algorithms written in lean (verifying time and space complexity).
• We have some lambda calculi, a process calculus, SKI, and a few logics (one in, one in a PR). Could be a good moment to start exploring encodings between them or (this one would be pretty nice) proving adequacy results, e.g., that the lambda calculus formulated with de Brujin indexes correctly captures alpha-equivalence.

Then we have areas that need to be kickstarted, like DB theory and more.

Happy to provide pointers for any of these, or if you have anything that interests you, please feel free to mention topics. :⁠-⁠)

[Mahdi Ghadimi]

Thank you for reply! really appreciate it

I'd love to start by implementing famous automatons. as i think it would be a way to get familiar with Lean, since i have experience with other theorem provers but am new to Lean.
(first time trying to contribute to a project aswell, sorry if i seem clueless)

if there's a particular automaton type you'd recommend starting with, or if you have any specific implementation preferences, please let me know. Otherwise, i'll begin with a Mealy machine and share progress for feedback.

[Ching-Tsun Chou]

You should know that I have formalized quite a bit of automata theory in Lean:
https://github.com/ctchou/AutomataTheory
I'll probably try to adapt it for cslib.

[Juanjo Madrigal]

Same here! :wave: I'm Juanjo from Madrid, mathematician turned into programmer, and I find this CSLib initiative really interesting, so I would love to contribute.

I've seen some threads and discussion about the verification of algorithms; I'll read further and try to formalize some. As @Mahdi Ghadimi says, any guidance is much appreciated. Thank you!

[chris477]

Fabrizio Montesi schrieb:

• We're also soon gonna be ready to accept contributions on verified algorithms written in lean (verifying time and space complexity).

I'm interested in space complexity per se, but I was not able to find any definitions in that area. Could you provide a pointer, or is it not public yet?

[Fabrizio Montesi]

Some work is starting to pop up :) cslib#165, cc @Sorrachai Yingchareonthawornchai

[Shreyas Srinivas]

Is this the one where you manually annotate operations with a tick function? I

[Shreyas Srinivas]

I still recommend following the approach of the debate repository over this. Anything that requires manually choosing when to call a tick operator is not going to scale well (meaning there will be more and more complex specs which have to be carefully manually checked)