Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: event: ACT@UCR

Topic: May 6th: Sarah Rovner-Frydman


view this post on Zulip John Baez (May 05 2020 at 05:26):

In the sixth talk of the ACT@UCR seminar, the irrepressible Sarah Rovner-Frydman (better known here as @sarahzrf) will tell us about a new approach to separation logic, a way to reason about programs.

She'll give her talk on Wednesday May 6th at 5 pm UTC, which is 10 am in California, or 1 pm on the east coast of the United States, or 6 pm in England. It will be held online via Zoom, here:

https://ucr.zoom.us/j/607160601

Afterwards we'll discuss her talk here!

• May 6, Sarah Rovner-Frydman: Separation logic through a new lens.

Abstract. Separation logic aims to reason compositionally about the behavior of programs that manipulate shared resources. When working with separation logic, it is often necessary to manipulate information about program state in patterns of deconstruction and reconstruction. This achieves a kind of "focusing" effect which is somewhat reminiscent of using optics in a functional programming language. We make this analogy precise by showing that several interrelated techniques in the literature for managing these patterns of manipulation can be derived as instances of the general definition of profunctor optics. In doing so, we specialize the machinery of profunctor optics from categories to posets and to sets. This simplification makes most of this machinery look more familiar, and it reveals that much of it was already hiding in separation logic in plain sight.

view this post on Zulip Jules Hedges (May 05 2020 at 10:12):

Yay! I saw heaps of talks on separation logic back in the day because London is its world capital (it was invented at Queen Mary where I did my PhD, but everybody involved did a mass exodus for UCL and Monoidics before I arrived), it will be very nice to see it in a totally different language

view this post on Zulip Reid Barton (May 05 2020 at 12:03):

Between the topic and body of the announcement there are three different dates suggested for the talk...

view this post on Zulip Oscar Cunningham (May 05 2020 at 12:15):

Well 'Wednesday' is also mentioned, which suggests the 6th. Which is also where it is on the calendar.

view this post on Zulip sarahzrf (May 05 2020 at 14:02):

Wednesday is correct

view this post on Zulip sarahzrf (May 05 2020 at 14:02):

@John Baez please fix your typos ;_;

view this post on Zulip John Baez (May 05 2020 at 14:11):

Sorry for any typos - I'll fix 'em. ACT@UCR mseeting are always on Wednesdays and I always announce them on the they're being held.

view this post on Zulip John Baez (May 05 2020 at 14:13):

I guess I was falling asleep.

view this post on Zulip Emily Pillmore (May 05 2020 at 17:01):

Go Sarah!

view this post on Zulip John Baez (May 05 2020 at 17:14):

Btw, there's a way to really delete a comment, by clicking the drop-down menu obtained via the downarrow that appears to the right of your comment when you move your mouse near the date.

view this post on Zulip Emily Pillmore (May 05 2020 at 17:17):

ah, she is hidden. Thanks @John Baez

view this post on Zulip Emily Pillmore (May 05 2020 at 17:18):

Can't wait for tomorrow :)

I thought it was today, for some reason. Mixed up with the CUNY seminar i guess

view this post on Zulip John Baez (May 05 2020 at 18:00):

The fact that I gave the wrong date might have helped. :crazy:

view this post on Zulip sarahzrf (May 06 2020 at 13:51):

the power in my house just flickered D:

view this post on Zulip sarahzrf (May 06 2020 at 13:51):

if i'm mysteriously unreachable this afternoon, assume it went out :((

view this post on Zulip sarahzrf (May 06 2020 at 13:52):

although

  1. i doubt it will? it doesn't seem to be flickering more yet
  2. if it does go out, i'll try to get in contact via mobile internet

view this post on Zulip John Baez (May 06 2020 at 16:45):

Hi - I'm on Zoom, I hope you're here.

view this post on Zulip sarahzrf (May 06 2020 at 16:48):

I'll join in one minute :grimacing:

view this post on Zulip John Baez (May 06 2020 at 16:52):

Sarah's slides are here:

view this post on Zulip Emily Pillmore (May 06 2020 at 17:02):

I am viewing sarahzrf's screen

view this post on Zulip Emily Pillmore (May 06 2020 at 18:00):

I have a meeting, but great job @sarahzrf!

view this post on Zulip John Baez (May 06 2020 at 18:15):

Hi....

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:15):

Regarding Bartosz' prism question, references to "separating disjunction" are very rare, I've only seen it mentioned in this talk https://math.unice.fr/tacl/assets/2019/contributed/s2/3/4-docherty-pym.pdf, where they suggest it's a form of CLL's "par"

view this post on Zulip John Baez (May 06 2020 at 18:15):

I could kick things off with a really dumb question while we wait for the smart people to show up.

view this post on Zulip John Baez (May 06 2020 at 18:15):

What's a Tambara module?

view this post on Zulip John Baez (May 06 2020 at 18:15):

It sounds like a profunctor between monoidal categories such that... something.

view this post on Zulip Christian Williams (May 06 2020 at 18:16):

Yeah, that was great! I haven't learned much about lenses yet, and I just think about them as some kind of "modular data access/manipulation". How can you use that interpretation here? Or more specifically, what do the "lens laws" say in the context of separation logic?

view this post on Zulip Mario Román (May 06 2020 at 18:19):

I think connecting optics with separation logic like that was very cool, and I liked a lot the examples! Maybe not only prisms but have you considered other actions to see if any gave some nice example?

(Or even, is there any problem with defining optics in a bicategory? The optics themselves look fine, maybe we need to rewrite the Tambara modules?)

view this post on Zulip sarahzrf (May 06 2020 at 18:21):

John Baez said:

What's a Tambara module?

It's a profunctor between actegories (categories w/ an action of a monoidal category) equipped w/ a transformation P(A, B) → P(M . A, M . B), subject to a boatload of laws (which are all automatic in the proset case of course :grinning_face_with_smiling_eyes:)

view this post on Zulip sarahzrf (May 06 2020 at 18:21):

so a "context-respecting relation"

view this post on Zulip Hendrik Boom (May 06 2020 at 18:21):

The string-wrapping monoid reminded me of a programming construction that's not a formal language application.
A frequent coding pattern is to set up a context, then to do work in that context, and afterward to take it down.
Typical examples are opening and later closing a file, or allocating memory to use during the work, and later releasing the memory.
So common is this that some programming languages have functions that do this wrapping. Racket, for example, has a function call-with-output-file, that opens and closes a file all around calling one of its arguments for the "work".

view this post on Zulip John Baez (May 06 2020 at 18:21):

sarahzrf said:

John Baez said:

What's a Tambara module?

It's a profunctor between actegories (categories w/ an action of a monoidal category) equipped w/ a transformation P(A, B) → P(M . A, M . B), subject to a boatload of laws (which are all automatic in the proset case of course :grinning_face_with_smiling_eyes:)

view this post on Zulip John Baez (May 06 2020 at 18:22):

Now is probably not the time, but sometime I'd like to see this boatload of laws compressed to something elegant. I think Street and someone already did it...

Anyway, you have a pile of more relevant questions.

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:22):

Hendrik Boom said:

The string-wrapping monoid reminded me of a programming construction that's not a formal language application.
A frequent coding pattern is to set up a context, then to do work in that context, and afterward to take it down.
Typical examples are opening and later closing a file, or allocating memory to use during the work, and later releasing the memory.
So common is this that some programming languages have functions that do this wrapping. Racket, for example, has a function call-with-output-file, that opens and closes a file all around calling one of its arguments for the "work".

in FP they usually call it "bracket combinator"

view this post on Zulip sarahzrf (May 06 2020 at 18:23):

Christian Williams said:

Yeah, that was great! I haven't learned much about lenses yet, and I just think about them as some kind of "modular data access/manipulation". How can you use that interpretation here? Or more specifically, what do the "lens laws" say in the context of separation logic?

for that interpretation: it depends on what kind of optic, but for the kind i showed in the talk that give rise to ramification, they correspond to "linear lenses", where you're obligated to re-put once you get
i'm afraid i haven't looked very closely at the stuff on lawfulness for generalized optics, or at least not in this context :T

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:24):

@sarahzrf have you looked into concurrent separation logics? There's a bunch of extra stuff there like ghost state, resource STSs, parallel composition rule..

view this post on Zulip Bruno Gavranović (May 06 2020 at 18:24):

sarahzrf said:

Christian Williams said:

Yeah, that was great! I haven't learned much about lenses yet, and I just think about them as some kind of "modular data access/manipulation". How can you use that interpretation here? Or more specifically, what do the "lens laws" say in the context of separation logic?

for that interpretation: it depends on what kind of optic, but for the kind i showed in the talk that give rise to ramification, they correspond to "linear lenses"

Oh that's very interesting!

view this post on Zulip sarahzrf (May 06 2020 at 18:25):

John Baez said:

Now is probably not the time, but sometime I'd like to see this boatload of laws compressed to something elegant. I think Street and someone already did it...

Anyway, you have a pile of more relevant questions.

here's the more elegant version: lax-equivariant functor C → PSh(D), where PSh(D) inherits an action from D

view this post on Zulip sarahzrf (May 06 2020 at 18:27):

bicategory of M-tambara modules is to bicategory of M-actegories as Prof is to Cat: they're related by a presheaf pseudomonad (or rather, they should be)

view this post on Zulip Jade Master (May 06 2020 at 18:27):

I noticed that separation logic deals with a lot of resources. Do you know of any connection with linear logic?

view this post on Zulip sarahzrf (May 06 2020 at 18:27):

there's some paper about "relative pseudomonads" that i havent actually read

view this post on Zulip John Baez (May 06 2020 at 18:28):

Mike Shulman was saying it looked like linear logic.... it very much does.

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:28):

Jade Master said:

I noticed that separation logic deals with a lot of resources. Do you know of any connection with linear logic?

it is substructural like linear, but slightly different, the authors originally introduced it as a variant of bunched logic IIRC

view this post on Zulip John Baez (May 06 2020 at 18:29):

It seems to me naively that linear logic cares about resources but not where they are located, while separation logic is more fine-grained in that it cares about where they are, in some rather abstract sense of "where they are".

view this post on Zulip eric brunner (May 06 2020 at 18:29):

i greatly enjoyed the talk, the string example was lovely and that there is work in progress in coq too.

view this post on Zulip sarahzrf (May 06 2020 at 18:29):

Alex Gryzlov said:

sarahzrf have you looked into concurrent separation logics? There's a bunch of extra stuff there like ghost state, resource STSs, parallel composition rule..

ish—i've been working with VST, and i've learned about ghost state & shares to some extent, but i'm not extensively familiar with their use for concurrency itself, and the other stuff you mention, not really

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:30):

I'm currently working on a Coq framework for lock-free CSL, that's why I'm asking :)

view this post on Zulip Bruno Gavranović (May 06 2020 at 18:30):

John Baez said:

It seems to me naively that linear logic cares about resources but not where they are located, while separation logic is more fine-grained in that it cares about where they are, in some rather abstract sense of "where they are".

Right, this is what wikipedia says "Separation logic supports the developing field of research described by Peter O'Hearn and others as local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. "

view this post on Zulip Gershom (May 06 2020 at 18:31):

Alex Gryzlov said:

Jade Master said:

I noticed that separation logic deals with a lot of resources. Do you know of any connection with linear logic?

it is substructural like linear, but slightly different, the authors originally introduced it as a variant of bunched logic IIRC

Right, and bunched logic is a sort of extension/variant of linear logic. Not sure about categorical models for it, in general.

view this post on Zulip Jon Aytac (May 06 2020 at 18:31):

Someone asked a question (in chat) at the very beginning about vanilla Hoare Logic's relation to transition systems. Hoare Logic can be thought of as an enrichment of the monoid M of commands in Rel(Pos) . The calculus of weakest preconditions gives a cartesian lifting by which Hoare -> M is a cloven fibration- so this gives a doctrine. For labelled transition systems, M is the monoid of labels. There's an adjunction of this category of transition systems with the topos of trees, in which one can construct a higher order modal hyperdoctrine. But there's no separation there. In the literature, a (partial) monoidal closed structure models the separating conjunction and magic wand to give a mess called bunched implication hyperdoctrine.

view this post on Zulip sarahzrf (May 06 2020 at 18:31):

John Baez said:

It seems to me naively that linear logic cares about resources but not where they are located, while separation logic is more fine-grained in that it cares about where they are, in some rather abstract sense of "where they are".

that really only derives from having "X is at Y" as a primitive proposition

view this post on Zulip John Baez (May 06 2020 at 18:31):

Coming from physics, where "locality" is a big deal (in field theory), it's interesting to me to imagine logics that take "locality" seriously - not just what's true but where it's true, or where you have resources.

view this post on Zulip sarahzrf (May 06 2020 at 18:31):

if you understand an atom in linear logic as having a spatial meaning, you'll see similar phenomena, i think

view this post on Zulip Gershom (May 06 2020 at 18:32):

An overview of the history of the development is given here: https://link.springer.com/article/10.1007/s13347-018-0312-8#Sec4

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:32):

Gershom said:

Alex Gryzlov said:

Jade Master said:

I noticed that separation logic deals with a lot of resources. Do you know of any connection with linear logic?

it is substructural like linear, but slightly different, the authors originally introduced it as a variant of bunched logic IIRC

Right, and bunched logic is a sort of extension/variant of linear logic. Not sure about categorical models for it, in general.

I don't know the proper name for it, but IIRC it's modeled by a category with two monoidal structures

view this post on Zulip John Baez (May 06 2020 at 18:32):

Hmm, are you suggesting you can build up some concept of locality from linear logic, or even build up separation logic within linear logic, @sarahzrf?

view this post on Zulip Hendrik Boom (May 06 2020 at 18:33):

Or which observer sees the state?

view this post on Zulip sarahzrf (May 06 2020 at 18:33):

well, you can sort of understand the term "separation logic" as referring to a particular semantics for the logic of bunched implications (BI)

view this post on Zulip sarahzrf (May 06 2020 at 18:34):

along with the integration with hoare logic

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:34):

it's interesting that in practice BI isn't really used much in more advanced versions of SL and people just work directly with underlying PCMs

view this post on Zulip sarahzrf (May 06 2020 at 18:34):

BI has models in closed monoidal heyting algebras

view this post on Zulip John Baez (May 06 2020 at 18:35):

Wooh, acronym city! :slight_smile:

view this post on Zulip sarahzrf (May 06 2020 at 18:35):

PCM = partial commutative monoid

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:35):

I guess the theory isn't advanced enough

view this post on Zulip sarahzrf (May 06 2020 at 18:35):

when i talk about "state fragments" or "resources", this is generally formalized as a PCM

view this post on Zulip sarahzrf (May 06 2020 at 18:36):

so a given piece of state / a given resource X can be fragmented into A and B if A ⊕ B = X

view this post on Zulip sarahzrf (May 06 2020 at 18:37):

the archetypal example is partial functions from some domain of "memory addresses" to values, with union as the operation, defined only when the domains are disjoint

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:37):

"resource" is a bit of overloaded term here because in CSL it also means a predicate on the state that can be temporarily broken inside critical sections

view this post on Zulip sarahzrf (May 06 2020 at 18:38):

anyway, BI is fairly similar to multiplicative intuitionistic linear logic—the biggest difference is that it has →

view this post on Zulip sarahzrf (May 06 2020 at 18:39):

actually yeah i believe models of MILL are closed monoidal lattices or closed monoidal distributive lattices or somethign

view this post on Zulip John Baez (May 06 2020 at 18:39):

Let's see, I thought "MILL" was about symmetric monoidal closed categories... is that right?

view this post on Zulip John Baez (May 06 2020 at 18:40):

Okay, our messages crossed in the night.

view this post on Zulip sarahzrf (May 06 2020 at 18:40):

oops! i indeed forgot a symmetric in front of both "monoidal"s up there

view this post on Zulip sarahzrf (May 06 2020 at 18:40):

\>.<

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:40):

I think you get ordered logic if you drop "symmetric" part :)

view this post on Zulip sarahzrf (May 06 2020 at 18:40):

sounds right

view this post on Zulip John Baez (May 06 2020 at 18:41):

If we "deplete", what I was saying was "commutative monoidal closed posets", though I don't think people tend to say that phrase.

view this post on Zulip John Baez (May 06 2020 at 18:42):

So anyway, what's this extra "→" thing that BI has?

view this post on Zulip John Baez (May 06 2020 at 18:42):

Can you describe in categorical terms?

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:43):

regular (non-linear) implication

view this post on Zulip John Baez (May 06 2020 at 18:43):

Oh, so you need a cartesian structure too, for this → thing to be adjoint to that?

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:43):

yeah I think so

view this post on Zulip sarahzrf (May 06 2020 at 18:44):

ah, sorry, i said "BI has models in closed monoidal heyting algebras" earlier but i guess you missed it

view this post on Zulip sarahzrf (May 06 2020 at 18:45):

and god dammit i meant MAILL not MILL

view this post on Zulip sarahzrf (May 06 2020 at 18:49):

@Mike Shulman by the way, regarding the thing you asked:

image.png

view this post on Zulip sarahzrf (May 06 2020 at 18:49):

then: there's concepts in hoare logic of "weakest precondition" and "strongest postcondition", which are exactly functors wp_C, sp_C that represent/corepresent H_C—so that makes this a cloven bifibration

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:52):

basically, linear logic contexts are multisets, and BI contexts are trees

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:52):

though I wonder how LNL models factor into this

view this post on Zulip John Baez (May 06 2020 at 18:53):

I need category theory to make me happy. I'm extremely happy with "MILL = commutative closed monoidal posets", "MAILL = closed monoidal Heyting algebras".

I guess the "A" means something like "additive", since we're throwing in coproducts... well, and products too I guess?

view this post on Zulip sarahzrf (May 06 2020 at 18:53):

Jon Aytac said:

Someone asked a question (in chat) at the very beginning about vanilla Hoare Logic's relation to transition systems. Hoare Logic can be thought of as an enrichment of the monoid M of commands in Rel(Pos) . The calculus of weakest preconditions gives a cartesian lifting by which Hoare -> M is a cloven fibration- so this gives a doctrine. For labelled transition systems, M is the monoid of labels. There's an adjunction of this category of transition systems with the topos of trees, in which one can construct a higher order modal hyperdoctrine. But there's no separation there. In the literature, a (partial) monoidal closed structure models the separating conjunction and magic wand to give a mess called bunched implication hyperdoctrine.

ooooh i missed this post and it sounds fascinating, do you have something i can read? ive seen bits and pieces of like half of the things you mention but i dont think ive seen how they all fit together like that

view this post on Zulip sarahzrf (May 06 2020 at 18:55):

tangential amusing story: one time i read part of a paper called "A General Framework for Sound and Complete Floyd-Hoare Logics" and it independently reinvented Ω-Prof/Rel(Pos)/(0, 1)-Prof / whatever you wanna call it, but it called it the "Hoare category"

view this post on Zulip sarahzrf (May 06 2020 at 18:55):

@John Baez yeah A is for additive

view this post on Zulip sarahzrf (May 06 2020 at 18:55):

⊕ and & are "additive" connectives in linear logic, with [co]cartesian categorical semantics

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:56):

this multiplicative/additive terminology is due to Girard I think

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:56):

I think the intuition behind it is that additive connectives require "adding up" contexts

view this post on Zulip sarahzrf (May 06 2020 at 18:57):

no, that's backwards!

view this post on Zulip sarahzrf (May 06 2020 at 18:57):

it's multiplicative connectives that accumulate contexts

view this post on Zulip sarahzrf (May 06 2020 at 18:57):

also, did people not classify sequent calculus rules as additive or multiplicative style before linear logic? i thought the classification of the connectives was named after the classification of rules

view this post on Zulip sarahzrf (May 06 2020 at 18:58):

maybe that's wrong :thinking: not sure why i thought that actually

view this post on Zulip Alex Gryzlov (May 06 2020 at 18:59):

oh yeah sorry, it's rather the intuition of which distributes over which

view this post on Zulip sarahzrf (May 06 2020 at 19:00):

:face_palm: i KNEW that at one point

view this post on Zulip sarahzrf (May 06 2020 at 19:00):

right, and "exponentials turn additives into multiplicatives"

view this post on Zulip Amar Hadzihasanovic (May 06 2020 at 19:00):

I think the terminology originally comes simply from the fact that in coherence spaces, multiplicatives give cartesian products of underlying sets and additives disjoint unions...

view this post on Zulip Amar Hadzihasanovic (May 06 2020 at 19:01):

The other “explanations” are retrofitted.

view this post on Zulip Amar Hadzihasanovic (May 06 2020 at 19:02):

Girard first discovered the coherence space model and reconstructed linear logic from it.

view this post on Zulip Alex Gryzlov (May 06 2020 at 19:04):

@sarahzrf it's a pity that you didn't mention the star ~ Day convolution link which I think you've previously discussed in some other stream around here

view this post on Zulip sarahzrf (May 06 2020 at 19:04):

hahaha

view this post on Zulip sarahzrf (May 06 2020 at 19:04):

man i didn't have time

view this post on Zulip sarahzrf (May 06 2020 at 19:06):

i've been mining depleted categorical structure out of separation logic on and off for the past 6 months and by now i have a goddamn truckload of it

view this post on Zulip sarahzrf (May 06 2020 at 19:06):

i can only fit so much into an hour

view this post on Zulip sarahzrf (May 06 2020 at 19:17):

Mario Román said:

I think connecting optics with separation logic like that was very cool, and I liked a lot the examples! Maybe not only prisms but have you considered other actions to see if any gave some nice example?

(Or even, is there any problem with defining optics in a bicategory? The optics themselves look fine, maybe we need to rewrite the Tambara modules?)

ack sorry i meant to reply to this earlier and then i got distracted and forgot

yeah i've considered a bunch of other actions :) that's one of the main points i hope to develop
re: bicategory, i've poked at trying to define it a little bit but i've never gotten around to pursuing the details fully... i dunno whether there's a problem or not!

view this post on Zulip sarahzrf (May 06 2020 at 19:18):

(to be precise, the generalization should be one such that you can recover the current definition by plugging in the delooping of a monoidal category)

view this post on Zulip sarahzrf (May 06 2020 at 19:18):

as for other actions—Δ:M[A,M]\Delta : \mathbf{M} \to [A, \mathbf{M}] is always strong monoidal, so you can compose it with any action of [A,M][A, \mathbf{M}] to get an action—then in concrete representations, this can give rise to a ∀ if you rig things up right, since Δ ⊣ ∀

view this post on Zulip Jon Aytac (May 06 2020 at 19:21):

sarahzrf said:

Jon Aytac said:

Someone asked a question (in chat) at the very beginning about vanilla Hoare Logic's relation to transition systems. Hoare Logic can be thought of as an enrichment of the monoid M of commands in Rel(Pos) . The calculus of weakest preconditions gives a cartesian lifting by which Hoare -> M is a cloven fibration- so this gives a doctrine. For labelled transition systems, M is the monoid of labels. There's an adjunction of this category of transition systems with the topos of trees, in which one can construct a higher order modal hyperdoctrine. But there's no separation there. In the literature, a (partial) monoidal closed structure models the separating conjunction and magic wand to give a mess called bunched implication hyperdoctrine.

ooooh i missed this post and it sounds fascinating, do you have something i can read?

For the last statement in the paragraph, as is often the case, Lars Birkedal has a nice paper on the topic: "BI Hyperdoctrines and Higher-Order Separation Logic" https://link.springer.com/content/pdf/10.1007%2F978-3-540-31987-0_17.pdf

The observations about the fibrational story of Hoare logic and temporal logic- it's a story we told ourselves in our seminar last year, but it feels like something I might have learned in Bart Jacobs book! The topos of forest comes from Joyal and Moerdjik's study of algebraic set theory, but was repurposed in the 90s to understand the categorical semantics for the synchronous calculus of communicating systems. More recently, it's been used by (natch) Lars Birkedal in "First Steps toward Synthetic Guarded Domain Theory" and elsewhere...

Anyways, I'm always interested in a fresh categorical understanding of separation logics, and tambara modules seems a cleaner route... sort of in two meetings at once this morning to be honest so I hope to have the opportunity to ask more pointed questions later.... many thanks!

view this post on Zulip sarahzrf (May 06 2020 at 19:24):

oh dammit that birkedal paper is literally one of the main places ive learned abt models of separation logic ahahaha

view this post on Zulip sarahzrf (May 06 2020 at 19:24):

i never did finish it tho >.<

view this post on Zulip sarahzrf (May 06 2020 at 19:25):

who's "we" in "our seminar"?

view this post on Zulip sarahzrf (May 06 2020 at 19:28):

oh, and "First Steps toward Synthetic Guarded Domain Theory" is where i learned to love the topos of trees :>

view this post on Zulip sarahzrf (May 06 2020 at 19:28):

not that i finished that either

view this post on Zulip Mike Shulman (May 06 2020 at 19:30):

Dropping by a bit late after teaching... MILL is a closed symmetric monoidal category/poset, MAILL adds finite products and coproducts, and BI additionally adds cartesian closure (and might leave out the coproducts, I don't remember). So a model of BI is a poset (or category) that's cartesian closed and also symmetric monoidal closed. The standard example is a presheaf category with a Day convolution symmetric monoidal structure, since presheaf categories are always also cartesian closed.

view this post on Zulip Mike Shulman (May 06 2020 at 19:31):

And back up on Tambara modules... a profunctor from A to B is equivalently a category equipped with a functor to the interval category 2=(01)2 = (0 \to 1) whose fibers are A and B respectively. Is a Tambara module similarly an actegory with an actegory-functor to 2, where 2 has the trivial action?

view this post on Zulip Mike Shulman (May 06 2020 at 19:33):

@sarahzrf Thanks for the pointer to the multiple-commands thing. What about if your "commands" have input and output types; could you then consider them as forming a category rather than a mere monoid and be looking at a lax functor out of that?

view this post on Zulip sarahzrf (May 06 2020 at 19:33):

Mike Shulman said:

Dropping by a bit late after teaching... MILL is a closed symmetric monoidal category/poset, MAILL adds finite products and coproducts, and BI additionally adds cartesian closure (and might leave out the coproducts, I don't remember). So a model of BI is a poset (or category) that's cartesian closed and also symmetric monoidal closed. The standard example is a presheaf category with a Day convolution symmetric monoidal structure, since presheaf categories are always also cartesian closed.

indeed, the canonical way to get models of separation logic is to take depleted copresheaves on a symmetric promonoidal proset, except typically restricted to the special case of "taking subsets of a partial commutative monoid"

view this post on Zulip sarahzrf (May 06 2020 at 19:34):

probably, re input and output types! if you work with effectful expressions rather than just commands, your hoare triples generally look like {P} e {x.Q}\{P\}\ e\ \{x.Q\}, where you're binding a variable in the postcondition to refer to the value that the expression results in

view this post on Zulip sarahzrf (May 06 2020 at 19:35):

but i don't have much experience with that :shrug:

view this post on Zulip Jules Hedges (May 06 2020 at 19:35):

This is probably the first talk on separation logic I've seen that didn't contain the words "heap" or "pointer".... I definitely ain't in London anymore

view this post on Zulip sarahzrf (May 06 2020 at 19:35):

i didn't want to alienate people who only knew python ;)

view this post on Zulip Jules Hedges (May 06 2020 at 19:38):

It often used to be presented as a method for reasoning about C and C++ specifically. Putting it in the context of Hoare logic is much nicer

view this post on Zulip sarahzrf (May 06 2020 at 19:39):

wait, wha? i usually think of the term "separation logic" as being inclusive of the tie-in to hoare logic

view this post on Zulip sarahzrf (May 06 2020 at 19:39):

like i would say that the frame rule is basically the heart & soul of "separation logic" as opposed to "bunched implications"

view this post on Zulip Jules Hedges (May 06 2020 at 19:39):

It could be I'm misremembering, it was a few years ago...

view this post on Zulip sarahzrf (May 06 2020 at 19:40):

is it possible that they were annotating C programs with pre/post conditions?

view this post on Zulip sarahzrf (May 06 2020 at 19:41):

when you're reasoning about whole programs, one thing you might do is intersperse code and assertions, like

{P}
C
{Q}
D
{R}

the idea being that {P} C {Q} and {Q} D {R} should both hold, and then implicitly you want to apply sequencing

view this post on Zulip Jules Hedges (May 06 2020 at 19:41):

On reflection, almost certainly yeah

view this post on Zulip sarahzrf (May 06 2020 at 19:42):

in fact, the notation {P} C {Q} was originally meant for this style—if you were writing a triple in isolation, you were meant to do P {C} Q

view this post on Zulip sarahzrf (May 06 2020 at 19:42):

but nobody does that anymore afaik

view this post on Zulip sarahzrf (May 06 2020 at 19:46):

Mike Shulman said:

And back up on Tambara modules... a profunctor from A to B is equivalently a category equipped with a functor to the interval category 2=(01)2 = (0 \to 1) whose fibers are A and B respectively. Is a Tambara module similarly an actegory with an actegory-functor to 2, where 2 has the trivial action?

having finally read this, it sounds right to me!
tbh one thing i've been kind of wanting to look into is seeing if there's some crank you can turn to get facts like that automatically—like does this drop out of being a proarrow equipment or something

view this post on Zulip Mike Shulman (May 06 2020 at 19:49):

I expect Tambara modules are also the codiscrete cofibrations in the 2-category of actegories, which is closer to a general crank. I don't know of a general 2-categorical way to talk about "objects over 2".

view this post on Zulip sarahzrf (May 06 2020 at 19:49):

hmm... actually i think there's one subtlety here—you need to know that the functor is strong equivariant, not just lax equivariant

view this post on Zulip Mike Shulman (May 06 2020 at 19:49):

What does that mean?

view this post on Zulip sarahzrf (May 06 2020 at 19:49):

well, i don't know if those are established terms :sweat_smile:

view this post on Zulip sarahzrf (May 06 2020 at 19:50):

i just mean MF(A)F(MA)M \cdot F(A) \cong F(M \cdot A) as opposed to the lax version

view this post on Zulip Mike Shulman (May 06 2020 at 19:50):

Where F is what?

view this post on Zulip sarahzrf (May 06 2020 at 19:50):

er, the functor to 2

view this post on Zulip Mike Shulman (May 06 2020 at 19:50):

I would include that in my definition of "actegory-functor".

view this post on Zulip sarahzrf (May 06 2020 at 19:51):

:thinking:

view this post on Zulip Mike Shulman (May 06 2020 at 19:51):

I suppose one can talk about lax, colax, and pseudo actegory-functors, but for this sort of structural thing you would nearly always want to use the pseudo ones.

view this post on Zulip sarahzrf (May 06 2020 at 19:51):

well, a fair number of useful things are only lax, and tambara modules are lax as functors to presheaves

view this post on Zulip sarahzrf (May 06 2020 at 19:51):

what do you mean by "this sort of structural thing"?

view this post on Zulip Mike Shulman (May 06 2020 at 19:52):

Defining structures internal to the 2-category of actegories.

view this post on Zulip sarahzrf (May 06 2020 at 19:52):

oh, like, the morphisms suitable for saying that an object classifies something?

view this post on Zulip Mike Shulman (May 06 2020 at 19:52):

yeah.

view this post on Zulip sarahzrf (May 06 2020 at 19:53):

hmmm, alright

view this post on Zulip sarahzrf (May 06 2020 at 19:54):

well, the thing i mentioned was just—you want the functor to 2 to be strong, or else the action on the collage could send objects in one fiber to objects in the other

view this post on Zulip sarahzrf (May 06 2020 at 19:54):

i guess that's exactly the kind of issue you had in mind?

view this post on Zulip Mike Shulman (May 06 2020 at 19:55):

yeah.

view this post on Zulip Max New (May 06 2020 at 20:55):

John Baez said:

Now is probably not the time, but sometime I'd like to see this boatload of laws compressed to something elegant. I think Street and someone already did it...

Anyway, you have a pile of more relevant questions.

I haven't found a reference, but I at one point (mostly) verified that a Tambara module structure is equivalent to an action of an identity profunctor "over" the actions of monoidal cats. So something like $M(m,n) * P(a,b) -> P(ma, nb)$. By a yoneda-like argument this can be recovered from its action on identity morphisms which is where the $P(a,b) -> P(ma,mb)$ comes from. The laws are then just the laws of an action of a monoid

view this post on Zulip Alex Gryzlov (May 06 2020 at 22:45):

John Baez said:

It seems to me naively that linear logic cares about resources but not where they are located, while separation logic is more fine-grained in that it cares about where they are, in some rather abstract sense of "where they are".

Actually that Docherty-Pym talk I've linked at the start of the thread explains it nicely: linear logic is intrinsic, in that its formulas themselves are resources, whereas separation logic merely describes how to deal with resources. There's a cool PL paper from this year that illustrates this point nicely by showing how to use separation logic as a metatheory for constructing a variant of a linear lambda calculus in a clean way: https://robbertkrebbers.nl/research/articles/intrinsic_sessions.pdf

view this post on Zulip sarahzrf (May 06 2020 at 22:48):

i dunno, i think formulas in separation logic are resources too

view this post on Zulip sarahzrf (May 06 2020 at 22:48):

but i haven't looked at the docherty-pym talk yet

view this post on Zulip sarahzrf (May 06 2020 at 22:48):

i was actually just about to... let me have a look :eyes:

view this post on Zulip sarahzrf (May 06 2020 at 22:50):

hmm, intinsic vs descriptive sounds like synthetic vs analytic to me :)

view this post on Zulip sarahzrf (May 06 2020 at 22:58):

it sounds to me like they're suggesting that LL is intrinsic but not descriptive, whereas BI is both image.png

view this post on Zulip sarahzrf (May 06 2020 at 23:01):

i am rather suspicious that this is just a mangled version of "promonoidal proset" or maybe "copromonoidal proset" image.png

view this post on Zulip Alex Gryzlov (May 06 2020 at 23:06):

yeah, BI has a curry-howard version in alpha-lambda calculus, though I've never seen it used anywhere

view this post on Zulip Alex Gryzlov (May 06 2020 at 23:07):

OTOH there's https://protz.github.io/mezzo/ but I'm not sure how closely it follows the rules of BI/SL

view this post on Zulip sarahzrf (May 06 2020 at 23:07):

what's αλ calc like?

view this post on Zulip Alex Gryzlov (May 06 2020 at 23:08):

basically LC with tree-shaped contexts, take a look at http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/BunchedTyping.pdf

view this post on Zulip sarahzrf (May 06 2020 at 23:08):

cool

view this post on Zulip sarahzrf (May 06 2020 at 23:09):

i was daydreaming a while back about if you could give denotational semantics to some kind of "separation type theory" in a 1-category of presheaves on a promonoidal proset...

view this post on Zulip sarahzrf (May 06 2020 at 23:09):

any relation perhaps? :o

view this post on Zulip Alex Gryzlov (May 06 2020 at 23:12):

I dunno about prosets, but Hoare type theory is a thing, invented by my boss :)

view this post on Zulip sarahzrf (May 06 2020 at 23:12):

i have the hoare type theory paper saved, actually

view this post on Zulip sarahzrf (May 06 2020 at 23:12):

i started reading it and did not get very far before getting distracted 🤪

view this post on Zulip sarahzrf (May 06 2020 at 23:13):

would be fun to try plotting a distribution of how far i typically get into a paper before switching focus :sob: adhd is fun

view this post on Zulip sarahzrf (May 06 2020 at 23:13):

it looked semi-relevant but i don't think i got far enough to know if it was the kind of thing i was thinking of

view this post on Zulip sarahzrf (May 06 2020 at 23:14):

hmm, whom of these is your boss? :)
image.png

view this post on Zulip Alex Gryzlov (May 06 2020 at 23:14):

Nanevski, also Mietek is my colleague :)

view this post on Zulip sarahzrf (May 06 2020 at 23:15):

oh i know him from freenode :)

view this post on Zulip Alex Gryzlov (May 06 2020 at 23:15):

that's why I mentioned him, I'm also there

view this post on Zulip sarahzrf (May 06 2020 at 23:15):

ooh wait, what's your nick?

view this post on Zulip Alex Gryzlov (May 06 2020 at 23:16):

clayrat

view this post on Zulip sarahzrf (May 06 2020 at 23:16):

...don't recognize it :shrug:

view this post on Zulip sarahzrf (May 06 2020 at 23:17):

well, i think i knew the name mietek mostly from #haskell, so if you didn't hang out there...

view this post on Zulip sarahzrf (May 06 2020 at 23:17):

well, this is a tangent

view this post on Zulip Alex Gryzlov (May 06 2020 at 23:21):

ah cool, thanks!

view this post on Zulip sarahzrf (May 07 2020 at 06:40):

@Mike Shulman i was watching thru the video of the talk to see it from a viewer perspective & hearing your question again i realize i think i partially missed your point—you were suggesting a single profunctor H : S ⇸ S, i'm guessing H(P, Q) is the set of commands such that {P} C {Q} holds?

view this post on Zulip sarahzrf (May 07 2020 at 06:41):

that should be basically the same as the hom-functor of the displayed category i described, but it never occurred to me to write that profunctor down directly

view this post on Zulip sarahzrf (May 07 2020 at 06:42):

actually, i think you get the total space of the displayed category equivalently to laxity of my functor to Prof if you equip H as a promonad :thinking:

view this post on Zulip sarahzrf (May 07 2020 at 06:43):

...and now i want the relation of "gives a valid hoare triple" between S × S and commands to induce some kind of galois connection and for that to somehow make the promonad version come from one side and the displayed category version come from the other

view this post on Zulip sarahzrf (May 07 2020 at 06:44):

but damn it's too late at night for me to think that one through

view this post on Zulip sarahzrf (May 07 2020 at 06:48):

very tangentially: i found this while googling to check how common of a concept promonads are: https://math.stackexchange.com/a/372457
and the description of profunctor composition in terms of their collages reeks to me of structured cospan -style open systems :o

view this post on Zulip Mike Shulman (May 07 2020 at 13:47):

sarahzrf said:

Mike Shulman i was watching thru the video of the talk to see it from a viewer perspective & hearing your question again i realize i think i partially missed your point—you were suggesting a single profunctor H : S ⇸ S, i'm guessing H(P, Q) is the set of commands such that {P} C {Q} holds?

Yes, that's what I meant.

view this post on Zulip Valeria de Paiva (May 24 2020 at 14:30):

sarahzrf said:

also, did people not classify sequent calculus rules as additive or multiplicative style before linear logic? i thought the classification of the connectives was named after the classification of rules

Because in "normal" logic additive and multiplicative formulations are equivalent. equiprovable, which is enough for people who only care about consequence relations. (ah, relevantists had been making the distinction too, but they were considered weird).

view this post on Zulip sarahzrf (May 24 2020 at 16:49):

sure, but i'm sure that people have cared about more than consequence relations since before linear logic

view this post on Zulip sarahzrf (May 24 2020 at 16:49):

proof theory is not so new, right?

view this post on Zulip Valeria de Paiva (May 24 2020 at 17:02):

sarahzrf said:

sure, but i'm sure that people have cared about more than consequence relations since before linear logic

well, it depends on whom do you ask. most traditional logicians nowadays still only care about consequence relations.

until the 70s no reputable mathematical logician would think about modal logic, let alone relevance or other "deviant" logics (the expression is Quine's, I believe). my evidence for this is that if you go to the index of the Handbook of Mathematical Logic (1977) there's no modal logic. at all. yes there's Kripke-Platek axioms, but no modal logic.
when Linear Logic started there was a problem convincing people that monoidal structures were logical.

view this post on Zulip sarahzrf (May 24 2020 at 17:05):

well, traditional logicians are losers :laughing:

view this post on Zulip Valeria de Paiva (May 24 2020 at 17:16):

sarahzrf said:

well, traditional logicians are losers :laughing:

a bit of history for you: separation logic came from Bunched Logic, (O'Hearn and Pym) and Bunched Logic was introduced in the Dagstuhl seminar that I organized in 1999 Linear Logic and Applications, https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=99341.