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.
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.
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
Between the topic and body of the announcement there are three different dates suggested for the talk...
Well 'Wednesday' is also mentioned, which suggests the 6th. Which is also where it is on the calendar.
Wednesday is correct
@John Baez please fix your typos ;_;
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.
I guess I was falling asleep.
Go Sarah!
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.
ah, she is hidden. Thanks @John Baez
Can't wait for tomorrow :)
I thought it was today, for some reason. Mixed up with the CUNY seminar i guess
The fact that I gave the wrong date might have helped. :crazy:
the power in my house just flickered D:
if i'm mysteriously unreachable this afternoon, assume it went out :((
although
Hi - I'm on Zoom, I hope you're here.
I'll join in one minute :grimacing:
Sarah's slides are here:
I am viewing sarahzrf's screen
I have a meeting, but great job @sarahzrf!
Hi....
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"
I could kick things off with a really dumb question while we wait for the smart people to show up.
What's a Tambara module?
It sounds like a profunctor between monoidal categories such that... something.
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?
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?)
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:)
so a "context-respecting relation"
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".
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:)
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.
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"
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
@sarahzrf have you looked into concurrent separation logics? There's a bunch of extra stuff there like ghost state, resource STSs, parallel composition rule..
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!
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
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)
I noticed that separation logic deals with a lot of resources. Do you know of any connection with linear logic?
there's some paper about "relative pseudomonads" that i havent actually read
Mike Shulman was saying it looked like linear logic.... it very much does.
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
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".
i greatly enjoyed the talk, the string example was lovely and that there is work in progress in coq too.
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
I'm currently working on a Coq framework for lock-free CSL, that's why I'm asking :)
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. "
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.
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.
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
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.
if you understand an atom in linear logic as having a spatial meaning, you'll see similar phenomena, i think
An overview of the history of the development is given here: https://link.springer.com/article/10.1007/s13347-018-0312-8#Sec4
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
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?
Or which observer sees the state?
well, you can sort of understand the term "separation logic" as referring to a particular semantics for the logic of bunched implications (BI)
along with the integration with hoare logic
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
BI has models in closed monoidal heyting algebras
Wooh, acronym city! :slight_smile:
PCM = partial commutative monoid
I guess the theory isn't advanced enough
when i talk about "state fragments" or "resources", this is generally formalized as a PCM
so a given piece of state / a given resource X can be fragmented into A and B if A ⊕ B = X
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
"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
anyway, BI is fairly similar to multiplicative intuitionistic linear logic—the biggest difference is that it has →
actually yeah i believe models of MILL are closed monoidal lattices or closed monoidal distributive lattices or somethign
Let's see, I thought "MILL" was about symmetric monoidal closed categories... is that right?
Okay, our messages crossed in the night.
oops! i indeed forgot a symmetric in front of both "monoidal"s up there
\>.<
I think you get ordered logic if you drop "symmetric" part :)
sounds right
If we "deplete", what I was saying was "commutative monoidal closed posets", though I don't think people tend to say that phrase.
So anyway, what's this extra "→" thing that BI has?
Can you describe in categorical terms?
regular (non-linear) implication
Oh, so you need a cartesian structure too, for this → thing to be adjoint to that?
yeah I think so
ah, sorry, i said "BI has models in closed monoidal heyting algebras" earlier but i guess you missed it
and god dammit i meant MAILL not MILL
@Mike Shulman by the way, regarding the thing you asked:
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
basically, linear logic contexts are multisets, and BI contexts are trees
though I wonder how LNL models factor into this
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?
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
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"
@John Baez yeah A is for additive
⊕ and & are "additive" connectives in linear logic, with [co]cartesian categorical semantics
this multiplicative/additive terminology is due to Girard I think
I think the intuition behind it is that additive connectives require "adding up" contexts
no, that's backwards!
it's multiplicative connectives that accumulate contexts
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
maybe that's wrong :thinking: not sure why i thought that actually
oh yeah sorry, it's rather the intuition of which distributes over which
:face_palm: i KNEW that at one point
right, and "exponentials turn additives into multiplicatives"
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...
The other “explanations” are retrofitted.
Girard first discovered the coherence space model and reconstructed linear logic from it.
@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
hahaha
man i didn't have time
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
i can only fit so much into an hour
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!
(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)
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 Δ ⊣ ∀
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!
oh dammit that birkedal paper is literally one of the main places ive learned abt models of separation logic ahahaha
i never did finish it tho >.<
who's "we" in "our seminar"?
oh, and "First Steps toward Synthetic Guarded Domain Theory" is where i learned to love the topos of trees :>
not that i finished that either
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.
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?
@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?
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"
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
but i don't have much experience with that :shrug:
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
i didn't want to alienate people who only knew python ;)
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
wait, wha? i usually think of the term "separation logic" as being inclusive of the tie-in to hoare logic
like i would say that the frame rule is basically the heart & soul of "separation logic" as opposed to "bunched implications"
It could be I'm misremembering, it was a few years ago...
is it possible that they were annotating C programs with pre/post conditions?
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
On reflection, almost certainly yeah
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
but nobody does that anymore afaik
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
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".
hmm... actually i think there's one subtlety here—you need to know that the functor is strong equivariant, not just lax equivariant
What does that mean?
well, i don't know if those are established terms :sweat_smile:
i just mean as opposed to the lax version
Where F is what?
er, the functor to 2
I would include that in my definition of "actegory-functor".
:thinking:
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.
well, a fair number of useful things are only lax, and tambara modules are lax as functors to presheaves
what do you mean by "this sort of structural thing"?
Defining structures internal to the 2-category of actegories.
oh, like, the morphisms suitable for saying that an object classifies something?
yeah.
hmmm, alright
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
i guess that's exactly the kind of issue you had in mind?
yeah.
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
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
i dunno, i think formulas in separation logic are resources too
but i haven't looked at the docherty-pym talk yet
i was actually just about to... let me have a look :eyes:
hmm, intinsic vs descriptive sounds like synthetic vs analytic to me :)
it sounds to me like they're suggesting that LL is intrinsic but not descriptive, whereas BI is both image.png
i am rather suspicious that this is just a mangled version of "promonoidal proset" or maybe "copromonoidal proset" image.png
yeah, BI has a curry-howard version in alpha-lambda calculus, though I've never seen it used anywhere
OTOH there's https://protz.github.io/mezzo/ but I'm not sure how closely it follows the rules of BI/SL
what's αλ calc like?
basically LC with tree-shaped contexts, take a look at http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/BunchedTyping.pdf
cool
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...
any relation perhaps? :o
I dunno about prosets, but Hoare type theory is a thing, invented by my boss :)
i have the hoare type theory paper saved, actually
i started reading it and did not get very far before getting distracted 🤪
would be fun to try plotting a distribution of how far i typically get into a paper before switching focus :sob: adhd is fun
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
hmm, whom of these is your boss? :)
image.png
Nanevski, also Mietek is my colleague :)
oh i know him from freenode :)
that's why I mentioned him, I'm also there
ooh wait, what's your nick?
clayrat
...don't recognize it :shrug:
well, i think i knew the name mietek mostly from #haskell, so if you didn't hang out there...
well, this is a tangent
ah cool, thanks!
@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?
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
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:
...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
but damn it's too late at night for me to think that one through
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
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.
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).
sure, but i'm sure that people have cared about more than consequence relations since before linear logic
proof theory is not so new, right?
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.
well, traditional logicians are losers :laughing:
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.