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: Planning my talk

sarahzrf (Apr 06 2020 at 00:11):

Hey! I have only a little bit of experience giving talks, and I could use some advice and/or feedback on how to structure mine. It's on separation logic, optics as specialized to (0, 1)-category theory, and the application of the latter to the former, but I figure I can't expect the audience of this seminar to have much of a background in program verification or separation logic. Since this is probably a ubiquitous issue when giving talks in this kind of setting, does anyone have some experience / thought on how to deal with this kind of thing?

John Baez (Apr 06 2020 at 00:14):

My main advice is: don't talk about what's really exciting to you now; explain the basics really clearly, so that people may be interested enough to learn more later. This always requires a painful act of renunciation.

Less is more.

sarahzrf (Apr 06 2020 at 00:14):

Right now my main thoughts as to what my options are include things like

• Make the topic of the talk less just "the application of optics to separation logic" and more "here's how to formulate separation logic categorically—check out all this (0, 1)-categorical structure!"
• Broaden the focus from "the application of optics to separation logic" to "manifestations of optics in (0, 1)-category theory"
• Handwave a lot of the separation logic

sarahzrf (Apr 06 2020 at 00:14):

aww :)

John Baez (Apr 06 2020 at 00:16):

Explaining what the heck "separation logic" is would be really helpful. I've seen you define it once, I think, but I still don't get it. I'm probably kind of typical.

sarahzrf (Apr 06 2020 at 00:16):

yeah, i figured

Mike Stay (Apr 06 2020 at 00:16):

If you're presenting a paper, you should treat the talk like an advertisement to go read the actual paper.

sarahzrf (Apr 06 2020 at 00:16):

i don't have a paper! (yet)

sarahzrf (Apr 06 2020 at 00:16):

i'd like to write one eventually, but

Mike Stay (Apr 06 2020 at 00:16):

Like John said, don't try to cram all the info in the paper into the talk.

John Baez (Apr 06 2020 at 00:17):

So, to get the idea of "separation logic" across you probably need to say it twice, in two different simple ways, omitting everything scary or technical.

sarahzrf (Apr 06 2020 at 00:17):

i do have some notes i wrote up, but they're not super well structured and they're rather incomplete

John Baez (Apr 06 2020 at 00:17):

Well, then you can treat your talk as a preview of a paper that will appear someday.

sarahzrf (Apr 06 2020 at 00:18):

ehh, i dunno, whatever paper i eventually write will most likely be aimed at people who are familiar with separation logic and maybe not category theory... :)

sarahzrf (Apr 06 2020 at 00:18):

perhaps that's a misunderstanding of what you mean

John Baez (Apr 06 2020 at 00:18):

I almost always talk about stuff I've written up, so people can go get the details somewhere. That frees me up to explain the basics, handwaving whenever that's the best approach.

John Baez (Apr 06 2020 at 00:19):

I didn't mean that the talk is for the same audience as the paper.

John Baez (Apr 06 2020 at 00:19):

I mean the paper contains the results in the talk, plus perhaps tons more.

John Baez (Apr 06 2020 at 00:20):

But anyway, the main thing is to make the talk clear and enjoyable to lots of kinds of people, not to pack it with detail.

sarahzrf (Apr 06 2020 at 00:23):

hmm, well

sarahzrf (Apr 06 2020 at 00:25):

to be concrete, the stuff i have that id be putting into my paper is roughly...

"there's this set of related techniques/concepts used in separation logic, and if you squint, you'll find that they actually all unify and drop out of the notion of optics if you instantiate it with the right parameters. plus, here's a contribution or two to that set of techniques that i got by working in this paradigm"

sarahzrf (Apr 06 2020 at 00:29):

it's also very much applied category theory, since it's a framework built on general categorical definitions that lets you plug in all kinds of general categorical facts to get useful tools

sarahzrf (Apr 06 2020 at 00:32):

i got sooooooooo much mileage out of $\exists \dashv \Delta \dashv \forall$

John Baez (Apr 06 2020 at 00:35):

:+1:

sarahzrf (Apr 06 2020 at 00:39):

but im not sure this is what i want my talk to be, given that i doubt most of the listeners will have any reason to care about unifying these techniques they've never heard of in this system they don't know about :sweat_smile:

John Baez (Apr 06 2020 at 00:42):

If your talk is good, by the end of it they will care about this. But they won't at first.

sarahzrf (Apr 06 2020 at 00:43):

sure!

sarahzrf (Apr 06 2020 at 00:43):

the problem is that i have a rather limited amount of time

sarahzrf (Apr 06 2020 at 00:45):

one the things is that the problem which separation logic solves is i think rather obscure if you don't already have a background in imperative programming

sarahzrf (Apr 06 2020 at 00:46):

or, well, maybe it's not, but i need to figure out how to communicate that—which is exactly why i made this topic

John Baez (Apr 06 2020 at 00:47):

An hour! That's a huge amount of time for a talk. Pity the people who give 20-minute talks at AMS meetings.

sarahzrf (Apr 06 2020 at 00:48):

:scream:

John Baez (Apr 06 2020 at 00:49):

Of course you still need to make every minute count, and ruthlessly strip down the information you present - only what's absolutely crucial to making the talk understandable and fun.

John Baez (Apr 06 2020 at 00:50):

If you do a good job you'll get a bunch of fans who will want to ask you more questions here after your talk (and also live, on Zoom).

sarahzrf (Apr 06 2020 at 00:50):

:flushed:

sarahzrf (Apr 06 2020 at 00:51):

god maybe accepting this was a bad idea i have so much other shit to do this month :sob:

John Baez (Apr 06 2020 at 01:05):

You can also give a bad talk if you want - it takes less work, and that's what most people do. :upside_down:

sarahzrf (Apr 06 2020 at 01:43):

will consider it :triumph:

sarahzrf (Apr 06 2020 at 06:41):

the really important thing for separation logic is the notion of aliasing

sarahzrf (Apr 06 2020 at 06:42):

and unfortunately, ppl who have only a passing knowledge of programming are often the ones who get tripped up by that exact point

sarahzrf (Apr 06 2020 at 06:42):

e.g., saying in python

list1 = [1, 2, 3, 4]
list2 = list1
list1[2] = 5
print(list2)

and getting confused

sarahzrf (Apr 06 2020 at 06:43):

well, as long as you're working with forests and trees, separation logic is great

sarahzrf (Apr 06 2020 at 06:43):

it's cyclic graphs that become a problem

sarahzrf (Apr 06 2020 at 06:43):

;)

sarahzrf (Apr 06 2020 at 06:43):

no, separation logic is a tool for reasoning about the behavior of programs in languages that can involve aliasing

sarahzrf (Apr 06 2020 at 06:44):

my work is maybe not about what you're expecting!

sarahzrf (Apr 06 2020 at 06:45):

although i've wondered if it might be possible to develop in the kind of direction you may be thinking of

sarahzrf (Apr 06 2020 at 06:46):

hold on, what's your existing familiarity with separation logic, then?

sarahzrf (Apr 06 2020 at 06:46):

so you haven't worked with it or anything?

sarahzrf (Apr 06 2020 at 06:46):

kk

sarahzrf (Apr 06 2020 at 06:47):

well, you may or may not be right, but regardless, aliasing is the problem that motivates separation logic

sarahzrf (Apr 06 2020 at 06:47):

right, ok :thinking:

sarahzrf (Apr 06 2020 at 06:47):

i think maybe i'd put the birds eye view to someone who knows some category theory as like

sarahzrf (Apr 06 2020 at 06:49):

"if we make things monoidal instead of cartesian, we can capture issues of 'ownership' and 'resources', and this allows us to make formal the kind of reasoning we do very naturally that would otherwise be plagued by pathological edge cases"

sarahzrf (Apr 06 2020 at 06:50):

most people tend to kind of implicitly take for granted that things don't alias

sarahzrf (Apr 06 2020 at 06:50):

then they get caught by surprise when their code gets run with aliased arguments and they realize their reasoning was wrong

sarahzrf (Apr 06 2020 at 06:50):

oof

sarahzrf (Apr 06 2020 at 06:51):

how so?

sarahzrf (Apr 06 2020 at 06:52):

hmm

sarahzrf (Apr 06 2020 at 06:52):

well, how about the next two lines i wrote? :)

sarahzrf (Apr 06 2020 at 06:53):

thats not what i mean, tho

sarahzrf (Apr 06 2020 at 06:54):

i mean aliasing in the sense of "multiple pointers to the same thing going by different names"

sarahzrf (Apr 06 2020 at 06:54):

except that even then the concept is more general, since languages like python dont have "pointers" per se but they certainly have aliasing

sarahzrf (Apr 06 2020 at 06:54):

:thumbs_up:

sarahzrf (Apr 06 2020 at 06:57):

it will look like a cospan 🤯

sarahzrf (Apr 06 2020 at 06:58):

(i doubt there's any deeper significance lol)

sarahzrf (Apr 06 2020 at 07:00):

i saw his talk ;p

sarahzrf (Apr 06 2020 at 07:01):

most discrete spaces arent :)

sarahzrf (Apr 06 2020 at 07:01):

classically, anyway

sarahzrf (Apr 06 2020 at 07:03):

it only comes into play insofar as separating conjunction (the aforementioned "monoidal instead of cartesian") is a case of day convolution

sarahzrf (Apr 06 2020 at 07:03):

but that's largely irrelevant

sarahzrf (Apr 06 2020 at 07:04):

optics come in like

sarahzrf (Apr 06 2020 at 07:04):

well, i start with a very general categorical formulation of optics

sarahzrf (Apr 06 2020 at 07:04):

then if you specialize it to (0, 1)-categories, it becomes a bit degenerate

sarahzrf (Apr 06 2020 at 07:05):

you now have preordered sets where you used to have full categories, and optics used to be elements of the hom-sets of those categories

sarahzrf (Apr 06 2020 at 07:05):

but now you can just ask "does this inequality hold in the optic preorder"

sarahzrf (Apr 06 2020 at 07:05):

this corresponds to being able to take certain kinds of steps when making a deduction

sarahzrf (Apr 06 2020 at 07:06):

which indeed feel a lot like "focusing in"

sarahzrf (Apr 06 2020 at 07:07):

the most basic case of all of this, which corresponds roughly to the notion of "linear lenses" in 1-categories, ends up reproducing the kind of "focusing-in" proof steps described in one source as "ramification"

sarahzrf (Apr 06 2020 at 07:09):

you're right! i'm being unhelpfully fancy with my wording

sarahzrf (Apr 06 2020 at 07:09):

a (0, 1)-category is just a thin category / preordered set

sarahzrf (Apr 06 2020 at 07:09):

but calling it that is suggestive of how you're going to use it

sarahzrf (Apr 06 2020 at 07:10):

i made this point elsewhere in this chat—if i talk about "a presheaf on this thin category C", i presumably mean a functor to Set, but if i talk about "a presheaf on this (0, 1)-category C", i presumably mean a monotone function to Ω (classically, 2)

sarahzrf (Apr 06 2020 at 07:11):

not mine! :)

sarahzrf (Apr 06 2020 at 07:11):

one sec

sarahzrf (Apr 06 2020 at 07:12):

here's a nice source on them categorical_update.pdf

sarahzrf (Apr 06 2020 at 07:12):

but i can give a summary of the idea

sarahzrf (Apr 06 2020 at 07:13):

kk

sarahzrf (Apr 06 2020 at 07:13):

is that the grothendieck construction one?

sarahzrf (Apr 06 2020 at 07:14):

yeah that one got my wheels turning

sarahzrf (Apr 06 2020 at 07:14):

i have on the backburner some thoughts about 2-optics

sarahzrf (Apr 06 2020 at 07:14):

which i really need to make my work a bit more applicable

sarahzrf (Apr 06 2020 at 07:14):

that probably sounds funny, but

sarahzrf (Apr 06 2020 at 07:15):

the issue is basically that right now, some of my definitions are too monomorphic for some actual use cases i have

sarahzrf (Apr 06 2020 at 07:15):

and having a bicategory instead of a monoidal category would fix that

sarahzrf (Apr 06 2020 at 07:17):

hey, john had a double category in his talk...

Fabrizio Genovese (Apr 06 2020 at 08:45):

Another perhaps useful suggestion is: Don't be afraid to make jokes. A talk is 50% interesting topics and 50% entertainment. Even if your contents are great you need more than that to keep people awake. Engage the public!

Fabrizio Genovese (Apr 06 2020 at 08:47):

I don't know how well this can work in virtual talks, but I've always found very useful to ask questions to the public. E.g. "Let's start with a survey! How many of you know have experience programming? Cool! How many of you have experience with functional programming? Great audience I see! How many of you have experience with theorem proving? Well, so now we know who are the unlucky ones!"

Fabrizio Genovese (Apr 06 2020 at 08:47):

This kind of thing gives you information about the average level of the people you talk to, while keeping them engaged. At that point it doesn't feel anymore like passively consuming some content, but like being actively part of a dynamic process

Todd Trimble (Apr 06 2020 at 11:07):

sarahzrf said:

i made this point elsewhere in this chat—if i talk about "a presheaf on this thin category C", i presumably mean a functor to Set, but if i talk about "a presheaf on this (0, 1)-category C", i presumably mean a monotone function to Ω (classically, 2)

You could just say monotone function to $\Omega$, then. I wouldn't necessarily trust people to pick up on your sense if you say "presheaf on this (0, 1)-category" -- that's a bit jargon-y.

My own advice echoes what John was saying earlier: start off really simply. Don't worry about how sophisticated your audience might be and that they might be bored by basics. (Yes, they probably are sophisticated in their own ways, but maybe not in your way.)

I don't want to say too much more, but just to say that many (most?) of us are into category theory because it simplifies mathematics, as opposed to making it look really sophisticated, which is maybe what the typical mathematician in the street thinks we're trying to prove by being category theorists. So, make it seem as simple as you can!

John Baez (Apr 06 2020 at 19:23):

Yeah, the whole idea of taking stuff from category theory and redoing it for posets will be new to a bunch of people... like how presheaves turn into mere downsets, and so on. (Most people probably won't know what a "downset" is, either.)

sarahzrf (Apr 06 2020 at 23:12):

man, i need to write an abstract x_x

John Baez (Apr 07 2020 at 02:39):

It's fun to hear someone starting to grapple with life as an academic.

sarahzrf (Apr 07 2020 at 12:44):

<.<

sarahzrf (Apr 07 2020 at 20:46):

Question to anyone w/ an opinion: Do you think it'd be a good idea to duplicate any definitions or concepts i throw up, like maybe into a top half & a bottom half, one showing "if you like categorical generality and you've thought about posets this way, here's what the concept is" and one showing "if you wanna know what it looks like in practice, here's what you get when you expand it for this case"

sarahzrf (Apr 07 2020 at 20:46):

or is that liable to split attention

John Baez (Apr 07 2020 at 20:53):

That's a tough call. It sounds helpful but it might get tiresome if you do it more than 5 times.

sarahzrf (Apr 07 2020 at 20:56):

tiresome for me, or for the audience?

John Baez (Apr 07 2020 at 20:57):

One other possibility: an "analogy chart" that has two columns, one for concepts in category theory and one for their corresponding concepts in poset theory. This is mainly good if both concepts have names and you want to spend some time making people think about the big picture.

John Baez (Apr 07 2020 at 20:58):

Tiresome for the audience, I meant. Creating a talk is supposed to be tiresome for the person who creates it. :upside_down:

John Baez (Apr 07 2020 at 20:58):

You suffer so the audience suffers less.

sarahzrf (Apr 07 2020 at 20:59):

im a martyr

John Baez (Apr 07 2020 at 21:00):

That's the right attitude!

Matteo Capucci (he/him) (Apr 07 2020 at 21:00):

John Baez said:

One other possibility: an "analogy chart" that has two columns, one for concepts in category theory and one for their corresponding concepts in poset theory. This is mainly good if both concepts have names and you want to spend some time making people think about the big picture.

These "analogy charts" are my fav thing

John Baez (Apr 07 2020 at 21:02):

I love 'em, and I think that's why people like my Rosetta Stone paper... it's all about analogy charts.

sarahzrf (Apr 08 2020 at 03:29):

okay so i'm thinking that maybe some amount of

Broaden the focus from "the application of optics to separation logic" to "manifestations of optics in (0, 1)-category theory"

might be a good idea

John Baez (Apr 08 2020 at 06:14):

A (0,1)-category is just a preorder, right? - or maybe a poset? If so, it might be good to call 'em that, so people instantly know what you're talking about. While there are advantages to thinking of them as (0,1)-categories, I'm not sure it helps to say "(0,1)-categories" over and over.

I know this suggestion will be annoying....

sarahzrf (Apr 08 2020 at 06:21):

ze ro one ca te go ry = 7 syllables
pro set = 2 syllables
we have a winner

sarahzrf (Apr 15 2020 at 16:00):

any tips on the right balance between being comprehensible to ppl whose background is not in my area vs. not using more of people's time than necessary on standard material?

Fabrizio Genovese (Apr 15 2020 at 16:01):

For me being comprehensible >> wasting people time.

sarahzrf (Apr 15 2020 at 16:02):

i am inclined to think so

sarahzrf (Apr 15 2020 at 16:02):

and i do still enjoy explaining standard material, especially when it's cool

Fabrizio Genovese (Apr 15 2020 at 16:02):

Like, by several orders of magnitude. If people feel some material is standard they can do something else in the meantime (esp. considering that talks are now virtual) or skip/watch 2x on Youtube. The opposite doesn't hold, if you don't understand some "standard" material you are cursed for the rest of the talk

Fabrizio Genovese (Apr 15 2020 at 16:03):

So if you ask me being boring is waaaaay better than being obscure. :slight_smile:

sarahzrf (Apr 15 2020 at 16:04):

on the other hand, i havent written this paper yet, so if someone who does have the background is watching and wants to know the details and feels that their time is wasted, i can't just go "ok well just read the paper" :sob:

sarahzrf (Apr 15 2020 at 16:05):

guess i could just dump 3.6k lines of uncommented coq on them instead :upside_down:

sarahzrf (Apr 15 2020 at 16:07):

yknow maybe it would fit the seminar better to try to make the talk more about (0, 1)-optics more generally and less about what ive done with them in separation logic...

Fabrizio Genovese (Apr 15 2020 at 16:08):

You could just move the convo on zulip afterwards

Fabrizio Genovese (Apr 15 2020 at 16:08):

And then the amount of detail providable is limitless :D

Joe Moeller (Apr 15 2020 at 16:20):

I wouldn't expect talking about the CT without your original motivation would be good.

Joe Moeller (Apr 15 2020 at 16:22):

Selfishly, I could say that a goal you could have is to be able to say what your work says about separation logic in a way that I, a category theorist with very little logic background, could understand. Dually, I guess you could also aim to say it in a way where a logician with less CT background could understand why the CT was helpful. These goals are somewhat idealistic though.

sarahzrf (Apr 15 2020 at 16:23):

(for the record, separation logic is less a topic in "logic" than a topic in "program verification")

sarahzrf (Apr 15 2020 at 16:23):

(at least in terms of what you'll see when you look up work on it)

sarahzrf (Apr 15 2020 at 16:23):

(hmm, out of character moment for me...)

sarahzrf (Apr 15 2020 at 16:24):

yes, if/when this all goes down on paper i'd want to go for the latter

Joe Moeller (Apr 15 2020 at 16:24):

Right, it felt weird when I said logician, but maybe that indicates exactly how unfamiliar this info is to me.

sarahzrf (Apr 15 2020 at 16:24):

but right now my audience is not mostly people who already use separation logic