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: separation logic & day convolution

sarahzrf (Apr 02 2020 at 03:40):

also, nice depleted day convolution there in that blog post :sunglasses:

sarahzrf (Apr 02 2020 at 03:40):

it's separating conjunction now

sarahzrf (Apr 02 2020 at 03:40):

declaring it

Jade Master (Apr 02 2020 at 03:43):

Oh hmm.

Jade Master (Apr 02 2020 at 03:43):

Where is the depleted day convolution in that post?

sarahzrf (Apr 02 2020 at 03:44):

it's the monoidal structure on presheaves!

sarahzrf (Apr 02 2020 at 03:46):

congratulations to @Jade Master and @John Baez for their joint independent rediscovery of separation logic ^__^

Jade Master (Apr 02 2020 at 03:46):

??? lol

sarahzrf (Apr 02 2020 at 03:47):

well, ok, if i were less generous i might say that it's an essential insight that resources need not be possible to combine in general

Jade Master (Apr 02 2020 at 03:47):

I see what you mean about day convolution. The day convolution here kind of reminds me of Minkowski sum.

sarahzrf (Apr 02 2020 at 03:48):

i just looked up minkowski sum

sarahzrf (Apr 02 2020 at 03:48):

it's day convolution :gun:

Jade Master (Apr 02 2020 at 03:49):

That is a bold claim but I guess I believe you

Jade Master (Apr 02 2020 at 03:50):

I don't really understand how this stuff relates to separation logic.

sarahzrf (Apr 02 2020 at 03:50):

the standard general formulation of separation logic goes something like

sarahzrf (Apr 02 2020 at 03:50):

you have a partial commutative monoid (PCM for short)

sarahzrf (Apr 02 2020 at 03:50):

you think of its elements as "resources"

sarahzrf (Apr 02 2020 at 03:52):

its power set is a complete boolean algebra, whose elements you can see as "assertions about a resource"

sarahzrf (Apr 02 2020 at 03:53):

the operation of $P \ast Q = \{x \mid \exist a, b.\ x = a \cdot b \land a \in P \land b \in Q\}$ is called "separating conjunction" and it means "$P$ and $Q$ independently hold of disjoint parts of the resource"

Jade Master (Apr 02 2020 at 03:54):

I don't think that John (definitely not me) discovered this idea about Petri nets and quantales.

sarahzrf (Apr 02 2020 at 03:54):

well, i may have been being a bit tongue in cheek :halo:

sarahzrf (Apr 02 2020 at 03:54):

anyway, sometimes you also generalize this stuff to ordered PCMs

sarahzrf (Apr 02 2020 at 03:55):

and then youll probably want to work with downsets or upsets

sarahzrf (Apr 02 2020 at 03:56):

but anyway, most of what that post is saying is basically the same exact thing as what you do in separation logic, w/ the PCM specialized to an ordered, non-partial one built from a petri net

sarahzrf (Apr 02 2020 at 03:57):

whereas historically separation logic originated as specialized to the PCM of heap states

sarahzrf (Apr 02 2020 at 03:58):

if you model the state of memory in a program at a particular point as a finite partial function from some domain of "addresses" to some codomain of "values", then this PCM has such finite partial functions as elements, and its operation is union but defined only when the memories have disjoint domains

Jade Master (Apr 02 2020 at 03:59):

Okay cool.

sarahzrf (Apr 02 2020 at 04:00):

anyway, preordered PCMs are a special case of symmetric promonoidal preorders, which are indeed the fundamental structure you need in order to be able to put day convolution on presheaves (altho many presentations only look at the case where you have a full monoidal product)

Jade Master (Apr 02 2020 at 04:03):

What does promonoidal mean?

sarahzrf (Apr 02 2020 at 04:03):

monoid object in Prof

sarahzrf (Apr 02 2020 at 04:04):

so multiplying two objects only gets you a presheaf out

Jade Master (Apr 02 2020 at 04:04):

Oh yeah. Like a partial monoid on a preorder

sarahzrf (Apr 02 2020 at 04:05):

a partial monoid gives this by just being either representable or empty and never anything more interesting

Jade Master (Apr 02 2020 at 04:05):

All this day convoluting is really useful in seperation logic. Wow.

sarahzrf (Apr 02 2020 at 04:05):

:>

sarahzrf (Apr 02 2020 at 04:06):

a slick way of setting up the fully general day convolution is like—so, in any monoidal category, if you have a comonoid structure on some object A and a monoid structure on B, you can make Hom(A, B) a monoid like this image.png

sarahzrf (Apr 02 2020 at 04:06):

now, Prof is monoidal under product of categories

sarahzrf (Apr 02 2020 at 04:07):

so if we have a comonoid object C in it and a monoid object D in it, we can turn Prof(C, D) into a monoidal category

Jade Master (Apr 02 2020 at 04:07):

The day convolution is the is the "separating conjunction" here?

sarahzrf (Apr 02 2020 at 04:07):

yeah

sarahzrf (Apr 02 2020 at 04:08):

now note that presheaves and copresheaves correspond to profunctors to or from 1 (um, i cant remember which is which), which is of course both a monoid and a comonoid

sarahzrf (Apr 02 2020 at 04:09):

so you can make the category of presheaves or copresheaves monoidal by making your category a monoid or comonoid object in Prof (i may have that backward)

sarahzrf (Apr 02 2020 at 04:10):

uh, i guess really i mean pseudomonoid/pseudocomonoid, whateverrrr

Jade Master (Apr 02 2020 at 04:10):

You would also need set to be a (co)monoid right?

Jade Master (Apr 02 2020 at 04:10):

(yes pseudo_

sarahzrf (Apr 02 2020 at 04:10):

nope, remember Set isn't showing up as a domain or codomain in Prof

sarahzrf (Apr 02 2020 at 04:10):

sarahzrf said:

now note that presheaves and copresheaves correspond to profunctors to or from 1 (um, i cant remember which is which), which is of course both a monoid and a comonoid

Jade Master (Apr 02 2020 at 04:11):

!

sarahzrf (Apr 02 2020 at 04:12):

if you have a bona fide monoidal structure on your category, you get a pseudomonoid and pseudocomonoid in Prof, since you can turn functors into profunctors in 2 directions

sarahzrf (Apr 02 2020 at 04:12):

and so you can get a day convolution on both presheaves and copresheaves

Jade Master (Apr 02 2020 at 04:12):

Day convolution is the profunctor composition of the first monoidal structure with the second right?

sarahzrf (Apr 02 2020 at 04:13):

look @ that string diagram i posted :V

Jade Master (Apr 02 2020 at 04:13):

Ah wait that doesn't make sense

Jade Master (Apr 02 2020 at 04:13):

yeah sorry one sec.

sarahzrf (Apr 02 2020 at 04:13):

(that's associativity, not the definition of the operation, but)

sarahzrf (Apr 02 2020 at 04:15):

anyway, if you start out with a pseudomonoid or pseudocomonoid C in Prof, iirc you only get day convolution on presheaves or copresheaves, since you can only rig up C's half of that diagram on either the top or the bottom, not both ways

sarahzrf (Apr 02 2020 at 04:16):

actually i guess this simplifies a bit if you're convolving specifically presheaves/copresheaves since in string diagram terms the monoid/comonoid structure on the tensor unit becomes totally implicit

sarahzrf (Apr 02 2020 at 04:18):

(i dont actually know if this monoidal category structure on Prof(C, D) is standard and/or also referred to as "day convolution", but it would make sense to me if it was)

Jade Master (Apr 02 2020 at 04:21):

I don't see how the term with the hom of C is showing up in the day convolution from this. I'm probably missing something obvious.

sarahzrf (Apr 02 2020 at 04:21):

hom of C?

sarahzrf (Apr 02 2020 at 04:22):

OH

sarahzrf (Apr 02 2020 at 04:22):

shit, sorry!!

sarahzrf (Apr 02 2020 at 04:22):

those aren't cups and caps

sarahzrf (Apr 02 2020 at 04:23):

notice the white dot in the middle & that they're forking—Y shaped

sarahzrf (Apr 02 2020 at 04:23):

that's the monoid & comonoid operations

sarahzrf (Apr 02 2020 at 04:23):

i could, probably stand to annotate better :|

Jade Master (Apr 02 2020 at 04:23):

Yeah I knew that.

sarahzrf (Apr 02 2020 at 04:23):

wait then what do you mean by hom of C?

Jade Master (Apr 02 2020 at 04:23):

https://ncatlab.org/nlab/show/Day+convolution

Jade Master (Apr 02 2020 at 04:24):

The definition here has this C(c1 x c2,c) term.

sarahzrf (Apr 02 2020 at 04:24):

oic, i thought you meant there was a hom in what i'd written >.<

sarahzrf (Apr 02 2020 at 04:25):

that's because the formula there is for when the pseudo[co?]monoid structure on C in Prof comes from a pseudomonoid structure in Cat

sarahzrf (Apr 02 2020 at 04:25):

you get a profunctor from a functor by putting it on one side of Hom

Jade Master (Apr 02 2020 at 04:27):

Yes. A monoidal category is the same as a pseudomonoid in Cat I'm pretty sure

Jade Master (Apr 02 2020 at 04:27):

Oh I see. You're doing a version starting with a promonoidal category.

sarahzrf (Apr 02 2020 at 04:27):

i meant "monoidal category", im not more sure of that than you are, i just wanted to repeat "pseudomonoid" for prosody

Jade Master (Apr 02 2020 at 04:27):

Cool I get what's going on now.

sarahzrf (Apr 02 2020 at 04:28):

:)

Jade Master (Apr 02 2020 at 04:28):

Thanks.

sarahzrf (Apr 02 2020 at 04:28):

sorry for the scrambled explanation

Jade Master (Apr 02 2020 at 04:29):

It's a nice way to understand Day convolution.

sarahzrf (Apr 02 2020 at 04:36):

well, to remember the definition maybe :shrug:

sarahzrf (Apr 02 2020 at 04:36):

im not sure how enlightening it is as to what day convolution means

sarahzrf (Apr 02 2020 at 04:37):

personally i think the day i learned that separating conjunction was an instance of day convolution was the day that day convolution clicked for me, or at least started to click

Jade Master (Apr 02 2020 at 04:38):

Yeah. This is pretty cool.

sarahzrf (Apr 02 2020 at 04:38):

(i saw the classic, expanded definition of separating conjunction in the case where the PCM is memories considerably before i ever heard the word "coend")

sarahzrf (Apr 02 2020 at 04:41):

anyway, the fact that day convolution generally admits a closed structure is sick as hell

sarahzrf (Apr 02 2020 at 04:42):

i dont know of any particular name for it other than "the closed structure for day convolution", so i kinda prefer to use the name from separation logic, which is magic wand

sarahzrf (Apr 02 2020 at 04:43):

because the connective is written like image.png

Jade Master (Apr 02 2020 at 04:45):

What is the seperation logic interpretation of the internal hom?

sarahzrf (Apr 02 2020 at 04:45):

was about to write it down :halo:

sarahzrf (Apr 02 2020 at 04:46):

in the (0, 0)-case, it's like $P -* Q = \{x \mid \forall y, a.\ y \in P \to x \cdot y = a \to a \in Q \}$

sarahzrf (Apr 02 2020 at 04:47):

in other words: P wand Q holds of a resource if whenever you can merge it with a resource satisfying P, you get something satisfying Q

sarahzrf (Apr 02 2020 at 04:48):

a resource satisfying P wand Q is a resource satisfying Q missing a resource satisfying P

sarahzrf (Apr 02 2020 at 04:48):

i once saw a really great illustration of this but im not sure whether id be able to find it again—give me one sec

sarahzrf (Apr 02 2020 at 04:50):

okay i found my screenshot of the illustration but id be hard pressed to find where it came from, which is a pity since i remember there being more great illustrations :(

sarahzrf (Apr 02 2020 at 04:50):

image.png

Jade Master (Apr 02 2020 at 04:52):

what does . and $\cdot$ mean?

sarahzrf (Apr 02 2020 at 04:53):

. just goes after the variables in a quantifier

sarahzrf (Apr 02 2020 at 04:53):

\cdot is the PCM operation

sarahzrf (Apr 02 2020 at 04:54):

that illustration is nice, but the kerning is shit

Jade Master (Apr 02 2020 at 04:56):

I don't understand the illustration but I get what the magic wand is now.

sarahzrf (Apr 02 2020 at 04:56):

oh ;_;

sarahzrf (Apr 02 2020 at 04:56):

hmm, guess different visualizations work for different ppl

sarahzrf (Apr 02 2020 at 04:57):

:shrug:

sarahzrf (Apr 02 2020 at 04:57):

idea is supposed to be that things are marked with assertions that describe em

sarahzrf (Apr 02 2020 at 04:57):

so we have this resource labelled P -* Q because it satisfies that

sarahzrf (Apr 02 2020 at 04:58):

and the property it has which means that is that we can stick together any of these other pieces labelled P and then the whole composite can be circled and labeled Q

Jade Master (Apr 02 2020 at 04:58):

Should there be a there exists in the quantifier you wrote?

sarahzrf (Apr 02 2020 at 04:58):

no

sarahzrf (Apr 02 2020 at 04:59):

you're thinking for a?

Jade Master (Apr 02 2020 at 04:59):

Yeah. Like is it a "for all y and for all a"?

sarahzrf (Apr 02 2020 at 04:59):

yeah

sarahzrf (Apr 02 2020 at 04:59):

we don't want to require that something satisfying P -* Q be possible to merge with everything satisfying P, just that if it can be merged with a given thing satisfying P, then blah blah

sarahzrf (Apr 02 2020 at 04:59):

so we need to ∀ the a

Jade Master (Apr 02 2020 at 05:00):

Should the first implication not be there?

sarahzrf (Apr 02 2020 at 05:00):

why not

Jade Master (Apr 02 2020 at 05:03):

Is it " for all y and a with y in P, x times y = a implies that a is in Q"

sarahzrf (Apr 02 2020 at 05:03):

yeah

sarahzrf (Apr 02 2020 at 05:03):

sorry, you write enough coq or haskell and you get totally used to chained arrows

Jade Master (Apr 02 2020 at 05:03):

What you have written is " for all y and a with y in P implies x times y = a implies that a is in Q"

sarahzrf (Apr 02 2020 at 05:03):

that's how you would write what you said!!!

sarahzrf (Apr 02 2020 at 05:03):

formally!!

Jade Master (Apr 02 2020 at 05:04):

:thinking:

sarahzrf (Apr 02 2020 at 05:04):

unless you put the quantifier into the forall

sarahzrf (Apr 02 2020 at 05:04):

i couldve just done that i guess

sarahzrf (Apr 02 2020 at 05:04):

but that's shorthand for what i wrote anyway!

sarahzrf (Apr 02 2020 at 05:05):

:curry:

Jade Master (Apr 02 2020 at 05:05):

I'm a logic noob. Is it like for all y and a with y in P is the context and x times y = a is the assumption

sarahzrf (Apr 02 2020 at 05:06):

you can say "for all a and y", and then you can add an assumption with "blah blah implies ..."

sarahzrf (Apr 02 2020 at 05:06):

"y in P" is a premise here

sarahzrf (Apr 02 2020 at 05:06):

we have 2 premises: y in P and x \cdot y = a

Jade Master (Apr 02 2020 at 05:07):

It's not like the first premise implies the second?

sarahzrf (Apr 02 2020 at 05:07):

no, → is pretty much universally right-associative

Jade Master (Apr 02 2020 at 05:07):

So why should there be an implication?

sarahzrf (Apr 02 2020 at 05:07):

for pretty much this reason

sarahzrf (Apr 02 2020 at 05:07):

you could also put this as $y \in P \land x \cdot y = a \to a \in Q$

Jade Master (Apr 02 2020 at 05:07):

That's by convention?

sarahzrf (Apr 02 2020 at 05:07):

yeah

Jade Master (Apr 02 2020 at 05:08):

Ok

sarahzrf (Apr 02 2020 at 05:08):

but it's about as standard of a convention as multiplication binding tighter than addition, where a convention is followed, has been my experience

sarahzrf (Apr 02 2020 at 05:09):

like i said tho, u write enough coq and u just get used to stating "suppose n > m, and m is prime, and blah, then foo" as n > m -> prime m -> blah -> foo

Jade Master (Apr 02 2020 at 05:09):

I remember pemdas but there's no i for implication in it :upside_down:

sarahzrf (Apr 02 2020 at 05:09):

pemdis

Jade Master (Apr 02 2020 at 05:10):

When you want someone to write something down

Jade Master (Apr 02 2020 at 05:11):

sarahzrf said:

and the property it has which means that is that we can stick together any of these other pieces labelled P and then the whole composite can be circled and labeled Q

sarahzrf (Apr 02 2020 at 05:12):

holy shit that was a trainwreck of a sentence

sarahzrf (Apr 02 2020 at 05:12):

i swear it's grammatical

sarahzrf (Apr 02 2020 at 05:12):

"and the property it has which means that, is that we can..."

Jade Master (Apr 02 2020 at 05:13):

Is it like $(P -* Q) * P\subseteq Q$

sarahzrf (Apr 02 2020 at 05:13):

not =

sarahzrf (Apr 02 2020 at 05:13):

but ⊢

sarahzrf (Apr 02 2020 at 05:13):

it's a closed structure!

sarahzrf (Apr 02 2020 at 05:13):

of course we have an evaluation map, but of course it's not an iso in general

sarahzrf (Apr 02 2020 at 05:14):

er, sorry, i misread the 2nd Q there as a P

sarahzrf (Apr 02 2020 at 05:14):

did you intend to write that, or was it a typo

Jade Master (Apr 02 2020 at 05:14):

Yeah P makes more sense

Jade Master (Apr 02 2020 at 05:14):

...editing...

sarahzrf (Apr 02 2020 at 05:15):

sdfjkj still wrong

John Baez (Apr 02 2020 at 05:15):

Jade wrote:

I don't think that John (definitely not me) discovered this idea about Petri nets and quantales.

Yeah, in that blog article of mine I was reporting on this:

• Uffe Engberg and Glynn Winskel, Petri nets as models of linear logic, in Colloquium on Trees in Algebra and Programming, Springer, Berlin, 1990, pp. 147-161.

To anyone who wants a summary: they're getting a model of linear logic from a Petri net, simply by taking the free commutative monoidal category on it, then demoting that to a commutative monoidal poset, and then forming the poset of downsets in that, which is a commutative quantale (i.e., a commutative monoid in the category of cocomplete posets, also known as suplattices).

I think some of this was my own reinterpretation of what they are doing. I prefer the category theory to the linear logic.

We could summarize all this by saying: start with a Petri net, form the free commutative monoidal poset on that. A poset is a Bool-enriched category, the poset of downsets on a poset P is the category of Bool-enriched presheaves on P, and the method of transferring a monoidal structure from a monoidal poset to its poset of downsets is the Boole-enriched version of Day convolution.

sarahzrf (Apr 02 2020 at 05:16):

it's (P -* Q) * P ⊢ Q

sarahzrf (Apr 02 2020 at 05:17):

"a poset is a bool-enriched category" heyting is turning over in his grave :cry:

sarahzrf (Apr 02 2020 at 05:17):

also it's definitely not \in, that doesn't make sense—maybe you mean \subseteq

sarahzrf (Apr 02 2020 at 05:17):

which is indeed what i mean by ⊢

Jade Master (Apr 02 2020 at 05:18):

lol okay thank you for teaching me logic :)

sarahzrf (Apr 02 2020 at 05:18):

but when i said it was still wrong, i meant you replaced the wrong Q with a P :sweat_smile:

sarahzrf (Apr 02 2020 at 05:19):

ok nice :thumbs_up:

sarahzrf (Apr 02 2020 at 05:20):

so if you satisfy (P -* Q) * P, you definitely satisfy Q, because you have a portion which satisfies P and you have a portion which, when combined with something that satisfies P, gives something that satisfies Q

sarahzrf (Apr 02 2020 at 05:20):

but the converse doesn't hold

sarahzrf (Apr 02 2020 at 05:20):

first: for an arbitrary P and Q, there may be resources satisfying Q that have no subpart satisfying P

sarahzrf (Apr 02 2020 at 05:21):

and second: even if you can separate a resource that satisfies Q into a portion which satisfies P and another one, that doesnt mean the other one satisfies P -* Q

sarahzrf (Apr 02 2020 at 05:22):

because P -* Q means Q needs to still hold if you replace the P portion with any other P portion that will fit

sarahzrf (Apr 02 2020 at 05:22):

whereas maybe Q holding of the overall resource relies on it being this particular P portion

sarahzrf (Apr 02 2020 at 05:25):

anyway, the fact that we have an adjunction is of course
P ⊢ Q -* R
<->
P * Q ⊢ R

sarahzrf (Apr 02 2020 at 05:26):

i.e.:
anything satisfying P will satisfy R once a Q thing is merged with it
IFF
anything separately satisfying P and Q satisfies R

sarahzrf (Apr 06 2020 at 03:04):

thinkin about the case where we have the monoidal product of concatenation on the set $A^*$ of finite sequences of elements of some set $A$

sarahzrf (Apr 06 2020 at 03:05):

then day convolution in the powerset is concatenation of languages, and its adjoint is this thing https://en.wikipedia.org/wiki/Quotient_of_a_formal_language

sarahzrf (Apr 06 2020 at 03:06):

you can make statements like

sarahzrf (Apr 06 2020 at 03:09):

$P \otimes Q \land P' \otimes Q' \dashv\vdash \exists s \in A^*.\\ (P \land P' \otimes y(s)) \otimes (Q \land (y(s) \hat\multimap Q')) \lor\\ (P \land (y(s) \multimap P')) \otimes (Q \land y(s) \otimes Q')$

sarahzrf (Apr 06 2020 at 03:10):

okay maybe that's not very readable :sweat_smile:

sarahzrf (Apr 06 2020 at 03:14):

for whatever it's worth, by $\exists$ i mean a sup and by $\hat\multimap$ i mean the other adjoint to $\otimes$, which is not symmetric since string concat is not