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.
Jacques Carette (Mar 26 2024 at 12:44):(I did a quick search first, and couldn't find anything obvious.) I'm firmly thinking in the context of [[computational trilogy]] here: is there a categorical setting that gives rise to separation logic? In other words, is there a way to extend the related concepts table found at [[regular logic]] to have 'separation logic' under the 'internal logic' column?
Ryan Wisnesky (Mar 26 2024 at 16:44):I know the usual suspects are working on the problem, there was e.g. a result in POPL 24, "Towards a Categorical Model of the Lilac Separation Logic "
Jacques Carette (Mar 26 2024 at 16:48):Are you sure of the title and publication venue? Scholar can't find a paper with that title, and the POPL 24 page also lists no such paper.
Ryan Wisnesky (Mar 26 2024 at 16:52): Ryan Wisnesky (Mar 26 2024 at 16:53):might a POPL workshop? LAFI?
Jacques Carette (Mar 26 2024 at 16:53):Thanks - weird that Scholar has not picked it up - and that it's neither on Amal's or Steven's web page! Yes, that's a POPL affiliated workshop.
Jacques Carette (Mar 26 2024 at 16:59):And the paper is an extended abstract with no results - everything categorical is in 2 short paragraphs right before the conclusion. Plus they mix in probabilities, which is a distraction.
And, at the end of the day, not what I'm looking for: they establish that you can have semantics in a category of sheaves over a category of renamings (nice!), but this is not an "internal logic" kind of result. There is still quite a lot of work to do to extract the 'axiomatic' presentation.
Ryan Wisnesky (Mar 26 2024 at 17:02):does it have to be separation logic or can it be substructural logics in general? the latter should have more work
Jacques Carette (Mar 26 2024 at 17:09):I'm interested in what 'separation' might mean categorically. So I'm most interested in 'star', 'magic wand' and the 'frame rule'. I don't care about heaps in particular, I'm happy to generalize to any kind of linear / affine resource.
Ryan Wisnesky (Mar 26 2024 at 17:11):there's certainly a lot of work on categorical models of linear logic; for sub-structural in general presumably you'll have more luck than for separation logic, for example https://link.springer.com/chapter/10.1007/978-3-030-43520-2_12
Chris Barrett (Mar 26 2024 at 17:31):I'm not sure what the "start" rule is, but there has been work on categorical models of the logic of bunched implications, upon which seperation logic is based. These appear to be cleanly modelled using a CCC with an additional symmetric monoidal closed structure, giving a category which is closed in two ways (the monoidal implication models the magic wand).
Jacques Carette (Mar 26 2024 at 17:39):(Typo: 'star', not 'start'; edited).
Indeed, that's the kind of work that I'm looking for! Anything written up?
Chris Barrett (Mar 26 2024 at 17:52):This looks like a good reference: https://ncatlab.org/nlab/files/Biering-BunchedLogic.pdf
I must admit, though: I'm interested in this topic myself, but I've never been entirely clear on how the logic of bunched implications relates to separation logic proper (aside from the obvious "they use the same connectives"). It looks like this work tries to clarify that point, so maybe I should look more closely at it myself!
Max New (Mar 26 2024 at 21:24):This paper is the most up to date that I'm aware of on the categorical logic of separation logic in that it is not just a BI-hyperdoctrine but also includes a persistence modality.
Jacques Carette (Mar 26 2024 at 21:27):Not at all surprised to see the name 'Birkedal' attached to this. Thanks @Max New .
Max New (Mar 26 2024 at 21:27):But there's a big difference between separation logic and regular logic which is that a regular category (which is essentially sufficient conditions for the subobject hyperdoctrine to be regular) is a property of a category, but separation logic is not property but structure since you can have multiple interpretations of the separating conjunction (like we can have multiple monoidal structures). Further, there is less focus on models where the logic is interpreted as subobjects, instead, as in the linked paper, the starting point will be something like an ordered partial commutative monoid.
Max New (Mar 26 2024 at 21:28):honestly I find the categorical logic of separation logic and Hoare logic to be surprisingly under developed but I should probably stop giving away research ideas for free
Jacques Carette (Mar 26 2024 at 21:30):Thanks for confirming my suspicion that this area of categorical logic is under developed. (I can promise you that I won't do anything about it!)
Sam Staton (Mar 27 2024 at 06:55):Hi, if you don't know it, Peter has written a nice survey From categorical logic to facebook engineering -- categorical logic was there from the beginning.
I'm not sure what you mean is surprisingly undeveloped, @Max New, perhaps you mean the categorical treatment of program logic generally, as opposed to bunched logic (which I think of as basically about Day convolution)?
Max New (Mar 27 2024 at 11:02):Yeah let me clarify: the semantics of the logic of BI were being done categorically using Day convolution from the beginning and we should probably brag about this more. But there's been a ton of extensions to separation logic since then and few of those have actually extended the categorical analysis, with the Bizjak-Birkedal paper being a notable attempt to "catch up" with practice, whereas originally categorical logic was at the forefront.
But what I think is really underdeveloped about it is incorporating the whole program logic: the logic and the language it is over in a categorical semantics. And I mean it's underdeveloped in that a lot of it is fairly obvious to anyone who understands Bart Jacobs' chapters on Predicate Logic and yet I don't know of a reference that does it.
Jacques Carette (Mar 27 2024 at 15:23):Thanks @Sam Staton that survey was exactly what I was looking for. It was at the absolute perfect level for me to understand the main points, and gives me pointers to things I can look up if I want to go deeper.
Max New (Mar 27 2024 at 16:03):@Jacques Carette this thread also reminds me how much I hate that table. Everything starting with star-autonomous category should clearly be in a different table
Jean-Baptiste Vienney (Mar 27 2024 at 16:18):I think this is all my fault, I think I've added more or less all these lines. If there is a table of logics and associated categorical doctrines, the fragments and extension of linear logic should clearly be in this table. Also, all the variants of lambda-calculus. But I think the beginning of the table is all about fragments of first-order classical logic or theories in first-order classical logic, right?
So maybe we should make a table for existential/classical logical systems and a table for constructive/computational logical systems (including linear logic and lambda calculuses)?
Jean-Baptiste Vienney (Mar 27 2024 at 16:23):I agree there is a clear distinction between these two worlds although I don't know much about the computational interpretation of classical logic, and we can also do mathematics with the linear / cartesian closed stuff.
Max New (Mar 27 2024 at 16:58):Yes I agree the rows you added make sense to have somewhere just not in this same table
Jean-Baptiste Vienney (Mar 27 2024 at 17:15):Hmm, but the name of the table is categories and logic table, so I don't know what should be its new name...
Max New (Mar 27 2024 at 17:19):the original fields could be called "categories and predicate logic"
Jean-Baptiste Vienney (Mar 28 2024 at 04:37):I'll remove these lines from the table and try to make another one (and add further lines into it!) named something like "linear logic, lambda-calculus and categories". Just give me a few days and I'll do it when I have some time.
Bob Atkey (Apr 12 2024 at 13:22):Most of the links above point to work on categorical semantics of Bunched Implications, which includes the crucial separating conjunction connective, but do not include Separation Logic and the Frame rule. The concept of local action identified by Calcagno, O'Hearn and Yang is missing in an account that only covers Bunched Implications, but is essential to Separation Logic.
Paul-André Melliès and Noam Zeilberger's "Functors are Type Refinement Systems" describes Hoare Logic and Separation Logic as refinements of state transformers (Section 5). They note that the frame rule is not automatic for all possible transformers.
Another approach would be to consider Separation Logic as a kind of Dynamic Logic by having a modality graded by programs . The frame rule would then correspond to the fact that this modality should be strong wrt the separating conjunction (), but not wrt the normal conjunction (this is noted by Melliès and Zeilberger at the end of Section 5 and attributed to O'Hearn and Yang). IIRC, the Iris logic has a non-graded "state update" modality that is lax and strong wrt separating conjunction.