Linear logic

Stream: computer science

[Fabrizio Montesi]

The formalisation of linear logic is starting to shape up: https://github.com/cs-lean/cslib/tree/main/Cslib/Logic/LinearLogic/CLL
Thanks to @Maximiliano Onofre-Martínez for the first logical equivalences. :)

[Fabrizio Montesi]

One issue I'm seeing is with notation. Since the type of Propositions is parameterised over the type of Atoms, I have to explicitly call constructors like this:

theorem quest_zero_eqv_bot : (@quest Atom 0) ≡ ⊥ := by

Quest would have ? as notation. I guess we'd need some quotation that starts by taking in the 'Atom' parameter and then puts it everywhere it's needed...?

[Bhavik Mehta]

If it is useful, I have a finished formalisation of the phase semantics of propositional linear logic and its soundness and completeness

[Fabrizio Montesi]

Bhavik Mehta said:

If it is useful, I have a finished formalisation of the phase semantics of propositional linear logic and its soundness and completeness

I'm not an expert in the phase semantics of LL, but I think it'd be very interesting to have.

[Bhavik Mehta]

It was essentially a complete formalisation of the first chapter of this https://www.sciencedirect.com/science/article/pii/0304397587900454, done in the usual mathlib style. I don't know if the cslib style aligns nicely with that?

[Fabrizio Montesi]

It should. If you see places where we don't, PRs to align are welcome. (Also PRs to activate checks done in Mathlib.)

We depend on mathlib heavily (also downstream from cslib), so facilitating understanding from upstream and the possibility of upstreaming useful things to mathlib is good.

[Shreyas Srinivas]

You might want to check how we develop Iris for a more "CS-style" approach, whatever that means.

[Shreyas Srinivas]

Basically Iris is an instance of a typeclass of affine logics with a wand and separated conjunction operator.

[Shreyas Srinivas]

There are several kinds of linear logic, so you might want to have separate instances of linear logic for this type class. Mathlib style formalisation has its upsides and downsides. Computer scientists work differently from mathematicians.

[Fabrizio Montesi]

I will have a look for sure, thanks. My intention was to make typeclasses for different kinds of sequents (one sided, two sided, ...) and then get into more specific stuff (affine, linear, etc.). There are many concepts to cover.

[Tanner Duve]

Hi! Just made a PR here defining the phase semantics of linear logic, following Girard. It remains to show that these semantics are sound and complete but I wanted to open this PR first since it has useful definitions and lemmas/theorems.

[Notification Bot]

A message was moved here from #computer science > Phase Semantics by Tanner Duve.

[Bhavik Mehta]

I mentioned this elsewhere a few weeks ago but I have a formalisation of the soundness and completeness of this semantics too

[Tanner Duve]

oh nice, just saw your older message. we may have defined some things slightly differently but maybe we can combine the two and you can PR your soundness/completeness proofs

[Fabrizio Montesi]

I'd love to get these. Let me know if you need support to sync on your definitions.

[Notification Bot]

5 messages were moved here from #computer science > cslib by Fabrizio Montesi.

[Fabrizio Montesi]

Moving the latest discussion on phase semantics to keep better track of it. Let me know if you'd like a dedicated 'Phase semantics of linear logic' topic.

[Bhavik Mehta]

Here's the implementation I wrote a couple years ago, I just updated it to current lean+mathlib: https://gist.github.com/b-mehta/62c9ca52657eb141a1cb497de0d7b878. As I mentioned in the past, it's a fairly direct translation of the relevant section of https://www.sciencedirect.com/science/article/pii/0304397587900454 into mathlib style (it was originally written with a mind to going into mathlib archive, but by the end I decided it probably wasn't appropriate material for that)