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.
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.
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
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...
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.
sarahzrf (May 05 2020 at 14:02):Wednesday is correct
sarahzrf (May 05 2020 at 14:02):@John Baez please fix your typos ;_;
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.
John Baez (May 05 2020 at 14:13):I guess I was falling asleep.
Emily Pillmore (May 05 2020 at 17:01):Go Sarah!
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.
Emily Pillmore (May 05 2020 at 17:17):ah, she is hidden. Thanks @John Baez
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
John Baez (May 05 2020 at 18:00):The fact that I gave the wrong date might have helped. :crazy:
sarahzrf (May 06 2020 at 13:51):the power in my house just flickered D:
sarahzrf (May 06 2020 at 13:51):if i'm mysteriously unreachable this afternoon, assume it went out :((
sarahzrf (May 06 2020 at 13:52):although
John Baez (May 06 2020 at 16:45):Hi - I'm on Zoom, I hope you're here.
sarahzrf (May 06 2020 at 16:48):I'll join in one minute :grimacing:
John Baez (May 06 2020 at 16:52):Sarah's slides are here:
Emily Pillmore (May 06 2020 at 17:02):I am viewing sarahzrf's screen
Emily Pillmore (May 06 2020 at 18:00):I have a meeting, but great job @sarahzrf!
John Baez (May 06 2020 at 18:15):Hi....
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"
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.
John Baez (May 06 2020 at 18:15):What's a Tambara module?
John Baez (May 06 2020 at 18:15):It sounds like a profunctor between monoidal categories such that... something.
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?
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?)
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:)
sarahzrf (May 06 2020 at 18:21):so a "context-respecting relation"
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".
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:)
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.
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"
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
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..
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!
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
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)
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?
sarahzrf (May 06 2020 at 18:27):there's some paper about "relative pseudomonads" that i havent actually read
John Baez (May 06 2020 at 18:28):Mike Shulman was saying it looked like linear logic.... it very much does.
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
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".
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.
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
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 :)
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. "
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.
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.
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
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.
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
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
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
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?
Hendrik Boom (May 06 2020 at 18:33):Or which observer sees the state?
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)
sarahzrf (May 06 2020 at 18:34):along with the integration with hoare logic
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
sarahzrf (May 06 2020 at 18:34):BI has models in closed monoidal heyting algebras
John Baez (May 06 2020 at 18:35):Wooh, acronym city! :slight_smile:
sarahzrf (May 06 2020 at 18:35):PCM = partial commutative monoid
Alex Gryzlov (May 06 2020 at 18:35):I guess the theory isn't advanced enough
sarahzrf (May 06 2020 at 18:35):when i talk about "state fragments" or "resources", this is generally formalized as a PCM
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
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
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
sarahzrf (May 06 2020 at 18:38):anyway, BI is fairly similar to multiplicative intuitionistic linear logic—the biggest difference is that it has →
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
John Baez (May 06 2020 at 18:39):Let's see, I thought "MILL" was about symmetric monoidal closed categories... is that right?
John Baez (May 06 2020 at 18:40):Okay, our messages crossed in the night.
sarahzrf (May 06 2020 at 18:40):oops! i indeed forgot a symmetric in front of both "monoidal"s up there
sarahzrf (May 06 2020 at 18:40):\>.<
Alex Gryzlov (May 06 2020 at 18:40):I think you get ordered logic if you drop "symmetric" part :)
sarahzrf (May 06 2020 at 18:40):sounds right
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.
John Baez (May 06 2020 at 18:42):So anyway, what's this extra "→" thing that BI has?
John Baez (May 06 2020 at 18:42):Can you describe in categorical terms?
Alex Gryzlov (May 06 2020 at 18:43):regular (non-linear) implication
John Baez (May 06 2020 at 18:43):Oh, so you need a cartesian structure too, for this → thing to be adjoint to that?
Alex Gryzlov (May 06 2020 at 18:43):yeah I think so
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
sarahzrf (May 06 2020 at 18:45):and god dammit i meant MAILL not MILL
sarahzrf (May 06 2020 at 18:49):@Mike Shulman by the way, regarding the thing you asked:
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
Alex Gryzlov (May 06 2020 at 18:52):basically, linear logic contexts are multisets, and BI contexts are trees
Alex Gryzlov (May 06 2020 at 18:52):though I wonder how LNL models factor into this
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?
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
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"
sarahzrf (May 06 2020 at 18:55):@John Baez yeah A is for additive
sarahzrf (May 06 2020 at 18:55):⊕ and & are "additive" connectives in linear logic, with [co]cartesian categorical semantics
Alex Gryzlov (May 06 2020 at 18:56):this multiplicative/additive terminology is due to Girard I think
Alex Gryzlov (May 06 2020 at 18:56):I think the intuition behind it is that additive connectives require "adding up" contexts
sarahzrf (May 06 2020 at 18:57):no, that's backwards!
sarahzrf (May 06 2020 at 18:57):it's multiplicative connectives that accumulate contexts
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
sarahzrf (May 06 2020 at 18:58):maybe that's wrong :thinking: not sure why i thought that actually
Alex Gryzlov (May 06 2020 at 18:59):oh yeah sorry, it's rather the intuition of which distributes over which
sarahzrf (May 06 2020 at 19:00)::face_palm: i KNEW that at one point
sarahzrf (May 06 2020 at 19:00):right, and "exponentials turn additives into multiplicatives"
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...
Amar Hadzihasanovic (May 06 2020 at 19:01):The other “explanations” are retrofitted.
Amar Hadzihasanovic (May 06 2020 at 19:02):Girard first discovered the coherence space model and reconstructed linear logic from it.
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
sarahzrf (May 06 2020 at 19:04):hahaha
sarahzrf (May 06 2020 at 19:04):man i didn't have time
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
sarahzrf (May 06 2020 at 19:06):i can only fit so much into an hour
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!
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)
sarahzrf (May 06 2020 at 19:18):as for other actions— is always strong monoidal, so you can compose it with any action of to get an action—then in concrete representations, this can give rise to a ∀ if you rig things up right, since Δ ⊣ ∀
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!
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
sarahzrf (May 06 2020 at 19:24):i never did finish it tho >.<
sarahzrf (May 06 2020 at 19:25):who's "we" in "our seminar"?
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 :>
sarahzrf (May 06 2020 at 19:28):not that i finished that either
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.
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 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?
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?
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"
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 , where you're binding a variable in the postcondition to refer to the value that the expression results in
sarahzrf (May 06 2020 at 19:35):but i don't have much experience with that :shrug:
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
sarahzrf (May 06 2020 at 19:35):i didn't want to alienate people who only knew python ;)
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
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
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"
Jules Hedges (May 06 2020 at 19:39):It could be I'm misremembering, it was a few years ago...
sarahzrf (May 06 2020 at 19:40):is it possible that they were annotating C programs with pre/post conditions?
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
Jules Hedges (May 06 2020 at 19:41):On reflection, almost certainly yeah
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
sarahzrf (May 06 2020 at 19:42):but nobody does that anymore afaik
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 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
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".
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
Mike Shulman (May 06 2020 at 19:49):What does that mean?
sarahzrf (May 06 2020 at 19:49):well, i don't know if those are established terms :sweat_smile:
sarahzrf (May 06 2020 at 19:50):i just mean as opposed to the lax version
Mike Shulman (May 06 2020 at 19:50):Where F is what?
sarahzrf (May 06 2020 at 19:50):er, the functor to 2
Mike Shulman (May 06 2020 at 19:50):I would include that in my definition of "actegory-functor".
sarahzrf (May 06 2020 at 19:51)::thinking:
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.
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
sarahzrf (May 06 2020 at 19:51):what do you mean by "this sort of structural thing"?
Mike Shulman (May 06 2020 at 19:52):Defining structures internal to the 2-category of actegories.
sarahzrf (May 06 2020 at 19:52):oh, like, the morphisms suitable for saying that an object classifies something?
Mike Shulman (May 06 2020 at 19:52):yeah.
sarahzrf (May 06 2020 at 19:53):hmmm, alright
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
sarahzrf (May 06 2020 at 19:54):i guess that's exactly the kind of issue you had in mind?
Mike Shulman (May 06 2020 at 19:55):yeah.
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
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
sarahzrf (May 06 2020 at 22:48):i dunno, i think formulas in separation logic are resources too
sarahzrf (May 06 2020 at 22:48):but i haven't looked at the docherty-pym talk yet
sarahzrf (May 06 2020 at 22:48):i was actually just about to... let me have a look :eyes:
sarahzrf (May 06 2020 at 22:50):hmm, intinsic vs descriptive sounds like synthetic vs analytic to me :)
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
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
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
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
sarahzrf (May 06 2020 at 23:07):what's αλ calc like?
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
sarahzrf (May 06 2020 at 23:08):cool
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...
sarahzrf (May 06 2020 at 23:09):any relation perhaps? :o
Alex Gryzlov (May 06 2020 at 23:12):I dunno about prosets, but Hoare type theory is a thing, invented by my boss :)
sarahzrf (May 06 2020 at 23:12):i have the hoare type theory paper saved, actually
sarahzrf (May 06 2020 at 23:12):i started reading it and did not get very far before getting distracted 🤪
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
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
sarahzrf (May 06 2020 at 23:14):hmm, whom of these is your boss? :)
image.png
Alex Gryzlov (May 06 2020 at 23:14):Nanevski, also Mietek is my colleague :)
sarahzrf (May 06 2020 at 23:15):oh i know him from freenode :)
Alex Gryzlov (May 06 2020 at 23:15):that's why I mentioned him, I'm also there
sarahzrf (May 06 2020 at 23:15):ooh wait, what's your nick?
Alex Gryzlov (May 06 2020 at 23:16):clayrat
sarahzrf (May 06 2020 at 23:16):...don't recognize it :shrug:
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...
sarahzrf (May 06 2020 at 23:17):well, this is a tangent
Alex Gryzlov (May 06 2020 at 23:21):ah cool, thanks!
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?
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
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:
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
sarahzrf (May 07 2020 at 06:44):but damn it's too late at night for me to think that one through
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
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.
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).
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
sarahzrf (May 24 2020 at 16:49):proof theory is not so new, right?
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.
sarahzrf (May 24 2020 at 17:05):well, traditional logicians are losers :laughing:
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.