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: theory: applied category theory

Topic: 2 cultures of ACT

Jules Hedges (Apr 11 2020 at 10:04):

I'll bring up here what I was talking about on twitter last night. I recognise 2 quite different approaches to ACT and I think it's useful to identify them and give them names. I called them "deep" and "shallow" ACT provisionally, which didn't go down well. I'll call them "type A" and "type B" here

Jules Hedges (Apr 11 2020 at 10:05):

In type A ACT you take applied concepts and try to justify them as just an X in the category of Y. That's where the deep theory is, and I think that's what most people calling themselves ACTists aspire to do

Jules Hedges (Apr 11 2020 at 10:07):

In type B ACT you treat categories much more as a language, to deal with coherence for graphical calculi and have functors as interdisciplinary translations, etc. But under the hood you're entirely happy to have things that aren't categorified (or justified)

Jules Hedges (Apr 11 2020 at 10:08):

I recognised this cultural distinction in the conversation about #practice: applied ct > Implementing Open Dynamical Systems, and I think it was causing a bit of misunderstanding

Jules Hedges (Apr 11 2020 at 10:11):

Specifically, I believe that @James Fairbanks, @Philip Zucker and me are thinking about dynamical systems from the type B perspective, whereas @Sophie Libkind and @John Baez are thinking about dynamical systems from the type A perspective

Jules Hedges (Apr 11 2020 at 10:12):

(I don't claim this is a "universal" classification of ACT - in particular I don't know how to classify CQM/ZX people on this axis; but I think it's sometimes a useful distinction and this happens to be one of those times)

James Fairbanks (Apr 11 2020 at 11:14):

Yeah I read those tweets and totally agreed. I’m all about that type B. I think that is the AppliedACT that @Blake Pollard’s NIST meeting would have been about. CT is a tool for organizing and understanding diverse areas of math. ACT is a tool for organizing and understanding diverse areas of science, engineering, and computation. Once you can organize and understand diverse areas of modeling in a unified language, you can start to build new tools that leverage that understanding.

For example when you look at that table different types of Open Dynamical Systems you realize that any software tool you build for analyzing Markov Chains should have an analogue for Automatons or Ergodic Systems. People have spent a lot of time analyzing those different types of systems in divergent communities. The ACT perspective should show us how to put them back together by translating concepts from community to other.

James Fairbanks (Apr 11 2020 at 11:44):

Software design is all about getting the abstractions right. The CT perspective “when a mathematician sees a definition they ask ‘what are examples of this?’ A CTist asks ‘what is this an example of?’” Is really helpful for finding the right abstractions. One sense of “right abstraction” is that when I generalize two similar things I get the same generalization.

Since ACT is a machine for turning mathematical definitions into mathematical abstractions, it can be a powerful tool for software design.

Fabrizio Genovese (Apr 11 2020 at 12:10):

Jules Hedges said:

In type B ACT you treat categories much more as a language, to deal with coherence for graphical calculi and have functors as interdisciplinary translations, etc. But under the hood you're entirely happy to have things that aren't categorified (or justified)

I feel this is also the approach we at Statebox are pursuing, mostly. It can also result in things that may be deemed "heretic" from a pure point of view. For instance, we realized that much of the theory we were developing wasn't going to work as intended because we were desperately trying to preserve an adjunction (which is for sure the right thing to do theoretically). As soon as we dropped this, things worked flawlessly from an implementational perspective.

Matteo Capucci (he/him) (Apr 11 2020 at 12:31):

James Fairbanks said:

The CT perspective “when a mathematician sees a definition they ask ‘what are examples of this?’ A CTist asks ‘what is this an example of?’”

I think this is my favorite mathematical quote ever!

Matteo Capucci (he/him) (Apr 11 2020 at 12:36):

Just this morning, following a line of thought started several days ago, I was contemplating the fact ACT has to surrender to the rest of mathematics if it really wants to be relevant, which is a position I find here reflected by Type B ACT. Open dynamical systems as outlined by @David Jaz are a textbook example of this. David built a beautiful infrastructure to unify many different takes on 'dynamical systems', but each declination will be non-categorical, to some extent. Yet CT gives you a neat bird-eye view, and exposes some aspects each of the declinations oversees.

James Fairbanks (Apr 11 2020 at 12:51):

I think David Spivak said it at the AMS Riverside meeting this November.

Yeah, the interface of ACT and real math is going to be messy from a pure CT perspective. But that’s ok. And it will probably force some new abstractions in CT to rectify the situation.

Fabrizio Genovese (Apr 11 2020 at 13:09):

One nice starting point could be this: Hask, the category of Haskell types and functions is not really a category, but something very close to it. Did someone try to define precisely what the real "Hask category" is?

Jules Hedges (Apr 11 2020 at 13:35):

I think the key difference between these 2 points of view is whether or not you think that justification (ie. identifying something as just an X in the category of Y) of applied concepts is an end in its own right

Fabrizio Genovese (Apr 11 2020 at 13:53):

Yes. In my view this is useful only if it allows to say more than you could before, e.g. by using more complicated tools.

Jules Hedges (Apr 11 2020 at 13:58):

I'm trying to be careful not to gatekeep what is "useful", useful depends entirely on what your goals are. Neither of these 2 approaches is better, they're just different

Jules Hedges (Apr 11 2020 at 14:00):

In particular, academics can take a much longer view than a startup. The average case of justification isn't useful right now, but I can easily imagine it being useful in the future

Jules Hedges (Apr 11 2020 at 14:02):

I just happen to be an academic who's impatient and wants results yesterday

Joachim Kock (Apr 11 2020 at 14:04):

when a mathematician sees a definition they ask ‘what are examples of this?’ A CTist asks ‘what is this an example of?

I think David Spivak said it at the AMS Riverside meeting this November.

I remember it from the meeting on Categorical Aspects of Network Theory in Turin in 2015: somebody was stating a theorem during a talk, and David, from the front row, asked "What is this an example of?". I don't remember who was the speaker, but it was John who replied with the remark "'What is this an example of?' Most mathematicians ask the question 'what is an example of this?', but category theorists ask 'What is this an example of?'". (It was a great meeting, by the way -- in the good old days where you could go out and have a beer and a pizza.)

Fabrizio Genovese (Apr 11 2020 at 14:17):

Jules Hedges said:

In particular, academics can take a much longer view than a startup. The average case of justification isn't useful right now, but I can easily imagine it being useful in the future

Yes, I'm arguing that stometimes justification is not an end in its own right even in mathematics: It's a tricky matter, but even pure mathematics has a social component, and justification can be an end in its own right when a group of people deem it interesting for whatever reason. In this case, one may argue that it is useful for that group of people anyway! But I can think of very few examples of justifications that are goals on their own right and that get pursued anyway even if no one is interested in them...

Fabrizio Genovese (Apr 11 2020 at 14:18):

Fabrizio Genovese said:

Yes. In my view this is useful only if it allows to say more than you could before, e.g. by using more complicated tools.

This is obviously my own personal view. For me the real goal of mathematics is to build increasingly powerful and general abstraction, that unify previously unrelated concepts. :slight_smile:

Philip Zucker (Apr 11 2020 at 14:25):

I just like things that spit out numbers.

Philip Zucker (Apr 11 2020 at 14:26):

They don't even have to be the right numbers

Fabrizio Genovese (Apr 11 2020 at 14:26):

Does this include number theory? :P

Joachim Kock (Apr 11 2020 at 14:27):

Philip Zucker said:

I just like things that spit out numbers.

$X \mapsto X+1$

Jules Hedges (Apr 11 2020 at 14:27):

Course the abstraction from things to numbers is probably the biggest act of abstraction in history. Going from numbers to $(\infty,1)$-toposes for example is a comparatively much smaller step

Philip Zucker (Apr 11 2020 at 14:28):

Oh, good point. Let me amend my statement. No number theory. The naturals aren't numbers

Fabrizio Genovese (Apr 11 2020 at 14:28):

Jules Hedges said:

Course the abstraction from things to numbers is probably the biggest act of abstraction in history. Going from numbers to $(\infty,1)$-toposes for example is a comparatively much smaller step

I'd like to dispute this! I realised you are right, but for beaurocratic reasons! The examples I gave were technically pre-historic, of course!

Philip Zucker (Apr 11 2020 at 14:31):

Well, the first took a couple billion years, the second only a couple thousand. Probably the seeds of anything fancy we do are built into the capabilities to do the first

Fabrizio Genovese (Apr 11 2020 at 14:32):

Yes, going from things to numbers is harder than going from numbers to toposes, but I wanted to dispute that there are other feats of abstraction that are immensely harder than the former, imho

Fabrizio Genovese (Apr 11 2020 at 14:32):

Namely: Recursion in language and invention of writing.

Philip Zucker (Apr 11 2020 at 14:33):

Or walking, which is pretty impressive

Philip Zucker (Apr 11 2020 at 14:33):

Sorry, I'm in a cheeky mood this morning

(=_=) (Apr 11 2020 at 14:34):

Fabrizio Genovese said:

Namely: Recursion in language and invention of writing.

I thought you didn't believe in recursion in language... :wink:

Fabrizio Genovese (Apr 11 2020 at 14:34):

Wrt invention of writing, it's very interesting also because we were able to witness it in reasonably recent times: https://en.wikipedia.org/wiki/Sequoyah

(=_=) (Apr 11 2020 at 14:34):

Philip Zucker said:

Sorry, I'm in a cheeky mood this morning

As am I... :grinning:

Fabrizio Genovese (Apr 11 2020 at 14:35):

I don't believe that recursion in language is the dividing line between animal communication and human language (or that drawing said line there is useful, or that wanting to draw such line is useful in any way). I for sure believe it's one of the greatest feats of abstraction ever, and a very useful one!

(=_=) (Apr 11 2020 at 14:49):

Jules Hedges said:

I'll bring up here what I was talking about on twitter last night. I recognise 2 quite different approaches to ACT and I think it's useful to identify them and give them names. I called them "deep" and "shallow" ACT provisionally, which didn't go down well. I'll call them "type A" and "type B" here

I don't think they're that different. They're both trying to express concepts in CT terms. In "type B" ACT, when you "have things that aren't categorified", that often means you don't know how to express them yet (e.g. see my conversation with John here). That's when "type A" ACT comes in, and there can be some lag until the "justification" happens.

(=_=) (Apr 11 2020 at 15:34):

I'd also second Daniel Litt's view: type B ACT is just normal maths for people in "algebraic geometry, number theory, etc." CT is just another tool for them. Sometimes it's just not right for the job.

https://twitter.com/littmath/status/1248778381149306880

@_julesh_ Ah yes, “shallow” applied category theory, also known as “math.”

- Daniel Litt (@littmath)

Jules Hedges (Apr 11 2020 at 15:39):

If we ever draw any boundary of what's "allowed" to count as ACT, category theory applied to algebraic geometry, number theory etc shouldn't count, because that's what's normally called "category theory"

Jules Hedges (Apr 11 2020 at 15:40):

(There's also category theory applied to category theory, which I call "Australian rules")

John Baez (Apr 11 2020 at 15:52):

If we ever draw any boundary of what's "allowed" to count as ACT, category theory applied to algebraic geometry, number theory etc shouldn't count, because that's what's normally called "category theory"

Actually I think it's called algebraic geometry, number theory, etc. People in those subjects who use category theory typically don't think of themselves as doing "category theory".

John Baez (Apr 11 2020 at 15:53):

Of course the same chunk of category theory can often be applied both to algebraic geometry and the design of air traffic control systems. That's part of what's nice about category theory: it's a very general set of tools.

Jules Hedges (Apr 11 2020 at 15:55):

Yep. Plus I guess the boundary between "pure" and "applied" is extremely blurry sometimes anyway, eg. in analysis

John Baez (Apr 11 2020 at 16:14):

Jules Hedges said:

In type A ACT you take applied concepts and try to justify them as just an X in the category of Y. That's where the deep theory is, and I think that's what most people calling themselves ACTists aspire to do.

In type B ACT you treat categories much more as a language, to deal with coherence for graphical calculi and have functors as interdisciplinary translations, etc. But under the hood you're entirely happy to have things that aren't categorified (or justified).

I don't really like classifying scientists because it tends to lock people into boxes, and I'm always trying to get out of boxes. If these are the choices I definitely have a type A personality. But I guess I should say why I'm trying to understand electrical circuits, control theory, chemical reactions, Petri nets and other things using category theory.

First, I think it's bad for math to be cut off from applications: it has always drawn inspiration from the real world, and category theory has a big untapped source of inspiration available to it from engineering and science.

Second, I think it's bad for applications to be cut off from math. It takes a while for mathematical ways of thinking to influence what people are doing on the cutting edge of application, but it does happen - once there is a communication channel.

Third, I think these various "categories of networks" that I'm studying have a lot of commonalities, and by understanding these we'll be able to create new kinds of networks - things that are potentially just as useful as the ones I listed, but don't exist yet.

Fourth, the reason I want to do this is that we need a new kind of technology, which I call "ecotechnology", which is more like how living organisms work. Low energy use, little or no waste, self-reproducing, robust (so you can damage it and it still works, with graceful degradation), and adaptive.

Coming up with this is a big job, and since I'm not an engineer I don't expect to actually design things. I'm just trying to understand networks in a way that would make it easier for someone to make progress on this job.

John Baez (Apr 11 2020 at 16:17):

Of course I don't expect anyone else to go about things in this way; everyone should do what they like and are good at.

Jules Hedges (Apr 11 2020 at 16:32):

Fair enough. I think it's worthwhile to identify them as existing "boxes", the challenge is to not encourage people to fit themselves into exactly one box

John Baez (Apr 11 2020 at 16:40):

I didn't know these boxes existed until you invented them. I felt free to move around. :upside_down:

John Baez (Apr 11 2020 at 16:42):

There are lots of things I do, and lots of things I don't do. You can trace out a complicated curve surrounding all the things I'll ever do and say "you are trapped in these region - you can never leave". But I won't like it.

John Baez (Apr 11 2020 at 16:43):

But maybe it's good to do this if you're trying to encourage someone to escape from their habits!

Jules Hedges (Apr 11 2020 at 16:50):

Just what I think I observe from talking with lots of people. Bit of amateur anthropology

James Fairbanks (Apr 11 2020 at 16:51):

The thing that separates shallow ACT from regular math to me is the exploitation of the universal perspective coming from CT. Analyzing Markov Chains, that’s math. Using the CT tools to simultaneously analyze Automata, Markov Chains, Ergodic Systems, and Smooth Dynamical Systems, that’s ACT.

Philip Zucker (Apr 11 2020 at 16:55):

I do find this explicit discussion of the kinds of people helpful for understanding and don't think it is just for the purpose of finding our boxes. It is very often that I'm extremely confused by papers, presentations, and discussions around category theory (and mathematical topics in general). If I'm honest, I often have to fight down the belief that what I see as confusing, jargon filled, and overly complicated explanations of beautiful ideas as the result of malignancy on the part of the authors. This is almost certainly not the case. It probably mostly a difference of aesthetical desires, background, and abilities.

James Fairbanks (Apr 11 2020 at 16:55):

Any mathematician who sees the definition of those different types of Dynamical Systems will intuitively see their similarities. But it takes CT to rigorously understand the similarities by finding the thing they are all examples of. Once we have that new understanding, we can build techniques and software for working with all of them simultaneously. We don’t need a AutomataPack and MCPack and ErgoPack and DynoPack. We can just write OpenDynamicalSystemsPack and solve all of them with the same machinery.

Gershom (Apr 11 2020 at 19:22):

Fabrizio Genovese said:

One nice starting point could be this: Hask, the category of Haskell types and functions is not really a category, but something very close to it. Did someone try to define precisely what the real "Hask category" is?

Andrej once had a very nice suggestion (I think never followed up on in a promised blog post?) that we might want to look at a poset-enriched category or something to make precise the "categorical" constructs people do on Hask (modulo seq). In particular, we don't just have individual functions between types, but an ordering of those functions with regards to definedness: https://www.reddit.com/r/haskell/comments/4f47ou/why_does_haskell_in_your_opinion_suck/d3k9578/?context=3

It would be great if somebody appropriately skilled in both enriched category theory and denotational semantics picked up and ran with this.

Philip Zucker (Apr 11 2020 at 19:23):

He does have this post http://math.andrej.com/2016/08/06/hask-is-not-a-category/

Gershom (Apr 11 2020 at 19:24):

Right, but that post doesn't address the suggestion I just described, afaik?

Philip Zucker (Apr 11 2020 at 19:24):

Probably not, this precedes the reddit comment

Philip Zucker (Apr 11 2020 at 19:33):

Joachim Kock said:

John Baez said:

And they're hoping God will give them a pat on the back and say "yes, that's exactly how I think about it".

I think that is an ambitious and noble aspiration :-)

Sometimes one only hopes for the pat on the back from some prophet or guru. And sometimes one gives a talk hoping to get a nod from some expert sitting in the front row. Maybe one even hopes that other people in the audience will notice the nod. OK, that's a bit pessimistic and depressing to think about. What is probably more relevant to explain the technicality of talks is that after we struggle years with some technical point, we are induced to think it is a super-important point everybody should know about. (While the audience is reading the news on their laptops, or texting their friend in row 3 with some funny remark.)

This is an interesting topic to me because I often feel reflective about my own motivations for why I do the things I do or like the things I like. Best I can figure, it is some mix of idealism and shameful-feeling pragmatism. Seeking external and internal validation. I can understand seeking the nod of approval.

Gershom (Apr 11 2020 at 19:34):

Btw on Jules' "two cultures" thing, I think the distinction is real and needs some value-neutral designation, but the word "cultures" is too strong. Certainly both approaches are possible by the same people, sometimes in tandem, sometimes not. But there is certainly a big difference between working on various representation theorems, and between establishing a "universal" setting in which we can organize and manipulate and relate a fair number of categories of different mathematical objects. Rather than cultures, we may want to distinguish between "lines of research" " or "results" and talk about work on "representation results" vs. work on "embedding results" or "realization results" or the like? Sorry this is a bit vague... Perhaps another way to think about it is what h-level the results occur at :-)

Joe Moeller (Apr 11 2020 at 19:47):

I agree with Gershom that "cultures" doesn't feel right, since the two sorts of ACTists interact a ton, I think.

Jules Hedges (Apr 11 2020 at 19:50):

Yes, I had to translate the thought I had yesterday into language but was too impatient to do it properly. Everybody, come up with better words for the same thing

Jules Hedges (Apr 11 2020 at 19:50):

"2 cultures" is an existing canned phrase, which is probably why it came to mind first

Joe Moeller (Apr 11 2020 at 19:51):

I definitely count myself at type A, mostly because I simply don't have the skill set for type B. I'm working on it though :sob:

Sam Tenka (Apr 11 2020 at 19:53):

Joe Moeller said:

I agree with Gershom that "cultures" doesn't feel right, since the two sorts of ACTists interact a ton, I think.

How about the two adjoints? :tongue: :p

Jules Hedges (Apr 11 2020 at 19:55):

I like it

Jules Hedges (Apr 11 2020 at 19:56):

The knowledge transfer pipeline goes theory $\to$ applications, from left to right. So type A is the left adjoint because they act on the theory, and type B is the right adjoint because they act on the applications. And the results are isomorphic

Sam Tenka (Apr 11 2020 at 19:57):

Yes, that sounds very right. Likewise, (from introspection I find that) type A work involves a lot of freedom and type B work involves a lot of forgetfulness.

sarahzrf (Apr 11 2020 at 19:57):

ive always liked the idea of there being an adjunction between theory and practice, or between examples and generality, or between...

sarahzrf (Apr 11 2020 at 19:58):

or maybe it's a dialectic

sarahzrf (Apr 11 2020 at 19:58):

https://twitter.com/sarah_zrf/status/1225852804641755137

@infty_dril i call evbery adjunction I see a dialectic and I am correct more often than not so I will never stop

- n-sarahzrf where n ≤ (1, 1) (@sarah_zrf)

sarahzrf (Apr 11 2020 at 19:59):

there's definitely lots of actual formal adjunctions between syntax and semantics or between theories and models :D

Jules Hedges (Apr 11 2020 at 19:59):

Well. Examples are about $\exists$ quantifiers, and generality is about $\forall$ quantifiers. I think the rest is standard

Jules Hedges (Apr 11 2020 at 19:59):

Yep

(=_=) (Apr 12 2020 at 13:44):

Jules Hedges said:

The knowledge transfer pipeline goes theory $\to$ applications, from left to right. So type A is the left adjoint because they act on the theory, and type B is the right adjoint because they act on the applications. And the results are isomorphic

This is where you lose some people with CT, because you're imposing a structure that you find pleasing, without actually working out if it fits well. I'm not even sure if Sam was having a bit of a laugh, given his emoji reactions.

I'd suggest calling type A "late-stage abstraction" and type B "early-stage abstraction", which means that we're talking about some sort of order (or "spectrum" in the common vernacular) here.

Type A looks like they're acting on the "theory", but the "theory" is the product of early-stage abstraction. Type B looks like they're acting on the "applications" because that's what abstraction does in its early stages.

Furthermore, the "knowledge transfer pipeline" goes both ways: abstraction goes from right to left, and specialisation goes from left to right.

(=_=) (Apr 12 2020 at 13:47):

Philip Zucker said:

Joachim Kock said:

John Baez said:

And they're hoping God will give them a pat on the back and say "yes, that's exactly how I think about it".

Sometimes one only hopes for the pat on the back from some prophet or guru.

I can understand seeking the nod of approval.

This is because:

• We are learning machines, and we need some supervision, even if only a little, in order to make progress.
• We are conditioned in school to desire that pat on the back.

Nathanael Arkor (Apr 12 2020 at 13:52):

I don't think it's conditioning: only those most narcissistic believe that they alone understand the beauty of mathematics greater than any other. Approval from someone whom we understand to understand better than ourselves is evidence that we too have grasped that beauty. It's objective, not purely psychological.

(=_=) (Apr 12 2020 at 14:20):

Nathanael Arkor said:

I don't think it's conditioning: only those most narcissistic believe that they alone understand the beauty of mathematics greater than any other. Approval from someone whom we understand to understand better than ourselves is evidence that we too have grasped that beauty. It's objective, not purely psychological.

I had two points there: the practical factor and the psychological component. The praticality is, as you've rightly pointed out, the objective need for error correction. But there is also the psychological need of seeking approval from some "God", "prophet", "guru", etc. And in the context of John's quote, that approval-seeking behaviour comes in the form of the adoption of a style of writing that may not necessarily be the best for informing the reader.

Jake Gillberg (Apr 18 2020 at 19:49):

Fabrizio Genovese said:

I feel this is also the approach we at Statebox are pursuing, mostly. It can also result in things that may be deemed "heretic" from a pure point of view. For instance, we realized that much of the theory we were developing wasn't going to work as intended because we were desperately trying to preserve an adjunction (which is for sure the right thing to do theoretically). As soon as we dropped this, things worked flawlessly from an implementational perspective.

Can you say more about the specifics of this? What adjunction were you trying to preserve? Why did it make implementation hard? What made it the "right" thing to do theoretically but not practically?

Fabrizio Genovese (Apr 18 2020 at 20:25):

Well, in our case, for instace, we wanted a link between petri nets and symmetric monoidal categories. This is a mess because, essentially, petri nets are built on multisets and free SMCs on strings, and there isn't a unique way to order a multiset into a string. So if you want an adjunction, you either tweak the definition of petri net (e.g. by using pre-nets) or you tweak the definition of free SMC (e.g by requiring it to be commutative). Both things were very unsatisfying for us: pre nets are really cumbersome as a graphical tool, since they introduce limitations which are completely non intuitive; commutative SMCs do not allow to map nets executions in semantics such as idris types and functions, since cartesian products are never commutative. In the end, we realized that what breaks down is the composition law for the functor going from petri nets to free smcs, which is something we'll never really use. So we didn't care. :D

Fabrizio Genovese (Apr 18 2020 at 20:26):

This is because in our situation what really matters are the objects. You want to build a free SMC out of a petri net, but you don't want to necessarily be able to morph a net into another and have the free smc structure to follow along (even if you can, btw)

Fabrizio Genovese (Apr 18 2020 at 20:28):

So all in all the point is that chasing a compositional description of how morphisms of nets induce morphisms of free smcs is pleasing mathematically, but completely out of scope in our applications, and comes with a huge price to pay (namely either a very ugly graphical interface or the absence of a functorial mapping to other semantics). So in the end we didn't bother, and wrote a paper about why :slight_smile:

Jade Master (Apr 18 2020 at 22:19):

Fabrizio Genovese said:

This is because in our situation what really matters are the objects. You want to build a free SMC out of a petri net, but you don't want to necessarily be able to morph a net into another and have the free smc structure to follow along (even if you can, btw)

This sort of surprises me. It seems to me like you could use morphisms as edits to your Petri net and the corresponding mapping between the free SMCs would tell you how to change the compiled code.

Fabrizio Genovese (Apr 18 2020 at 22:20):

Yes, but in practice you can do so by just defining the functors between smcs

Fabrizio Genovese (Apr 18 2020 at 22:22):

Also, you can still lift a morphism of net to a functor between freesmcs. The problem is that this is non-compositional, so you don't have F(f;g) = Ff ; Fg if you go from Petri to SMCs. This is for utterly stupid reasons, that is, in doing so you have to insert some symmetries here and there and you end up doing so in different ways

Fabrizio Genovese (Apr 18 2020 at 22:22):

So you can still edit petri nets and reflect this in the compiled code, it's just that "doing it two times at once" and doing it first once and then again are not the same operation

Fabrizio Genovese (Apr 18 2020 at 22:23):

I don't think this is a severe limitation in our framework, and in any case it's the less severe limitation among all the ones we could pick from :D

Jade Master (Apr 18 2020 at 22:35):

Fabrizio Genovese said:

Yes, but in practice you can do so by just defining the functors between smcs

A nontrivial Petri net will have a free SMC with an infinite number of distinct morphisms. The only way to define something like this is on generators.

Fabrizio Genovese (Apr 18 2020 at 22:38):

This is exactly the way you do it, yes

Fabrizio Genovese (Apr 18 2020 at 22:40):

What I am saying is that if you have a transition $t$ in the first net and a transition $u$ in the second net, and you send $t \to u$, then you can send $T$ to $\sigma;U;\sigma'$, where $T,U$ are their corresponding generators in the respective SMCs, and $\sigma, \sigma'$ are some miserable symmetries you need to put in to have domains and codomain match, which is the price to pay if you are using multisets to manipulate strings.

Fabrizio Genovese (Apr 18 2020 at 22:41):

There is _not_ a canonical way to choose $\sigma$ and $\sigma'$, which is exactly why the functorial composition law fails.

Fabrizio Genovese (Apr 18 2020 at 22:42):

To see that there is not a canonical consider, for instance, the case in which t takes two tokens from the same place A. Then you can decide to slide an identiity or a swap somewhere, and you don't really have a canonical way to pick one of the two.

Fabrizio Genovese (Apr 18 2020 at 22:44):

As you keep composing, sending $t \to u$ and $u \to v$, these symmetries stack up. So in the composition you get $T \mapsto \sigma;U;\sigma' \mapsto \tau;\sigma;V;\sigma';\tau'$. Contrary, in the composite $T \mapsto \theta;V;\theta'$. There isn't a canonical assignment of symmetries such that $\tau;\sigma = \theta$ and $\tau';\sigma'=\theta'$.

Jade Master (Apr 18 2020 at 22:45):

Right. This is the approach of Sassone?

Jade Master (Apr 18 2020 at 22:45):

In "Strongly Concatenable Processes"

Fabrizio Genovese (Apr 18 2020 at 22:46):

The approach of Sassone to solve the problem is to take, as generating morphisms corresponding to $t$, all the possible permutations of stuff in domain and codomain, and to relate them via a supplementary axiom in the SMC

Fabrizio Genovese (Apr 18 2020 at 22:46):

It fixes most cases, but it still does not fix the case where t gets to tokens from the same place in input.

Fabrizio Genovese (Apr 18 2020 at 22:48):

So yes, if you take all of them at once you get the adjunction, but the bookkeeping is still very imperfect.

Jade Master (Apr 18 2020 at 22:48):

I see. Is there a specific paper that you would say your semantics is closest to?

Fabrizio Genovese (Apr 18 2020 at 22:49):

My semantics is exactly the prenet semantics

Fabrizio Genovese (Apr 18 2020 at 22:49):

It's just that instead of using prenets, I use nets where I have a total ordering on their set of places

Jade Master (Apr 18 2020 at 22:49):

Oh great. That's my favorite :)

Fabrizio Genovese (Apr 18 2020 at 22:49):

(which is a computationally ok assumption)

Fabrizio Genovese (Apr 18 2020 at 22:49):

And I use the ordering to order domain and codomain of a transition

Fabrizio Genovese (Apr 18 2020 at 22:50):

So I have a "canonical" way to elevating a transition t to a generating morphism T. this "canonical" way tho is non compositional because the ordering on places of different nets are independent from net to net :slight_smile:

Fabrizio Genovese (Apr 18 2020 at 22:51):

I guess that my paper feels absolutely disgusting to read for a mathematician btw

Fabrizio Genovese (Apr 18 2020 at 22:52):

It's full of this borderline hacky stuff that makes things more or less work but still feels very meh from an aesthetic perspective. What can I say, real applications suck T_T

Jade Master (Apr 18 2020 at 22:52):

I honestly think there is more opportunity to make the mathematical ideals a bit closer to the real applications. I understand why that wouldn't be a priority for statebox though :)

Fabrizio Genovese (Apr 18 2020 at 22:54):

I'm very happy if someone picks it up. I'd also like to collaborate. I basically really tried to establish a satisfying correspondence between nets and SMCs. I threw pretty much everything I knew at the problem, including trying with higher cats, but with no success whatsoever

Fabrizio Genovese (Apr 18 2020 at 22:55):

I am still _very_ annoyed that there isn't a formally satisfying way to link petri nets (and not pre-nets) with free SMCs (not commutative). I still think it should exists. Its absence is really a big disappointment for the whole world of maths really

Jade Master (Apr 18 2020 at 22:56):

Is the idea that the user specifies only Petri nets and Petri net morphims. Then statebox translates this to pre-nets and pre-net morphisms. This translation is not in the categorical framework once you get their however the rest is categorical?

John Baez (Apr 18 2020 at 22:56):

Jade Master said:

Oh great. That's my favorite :)

You really like nets where there's a total ordering on the set of places? Oh are you being sarcastic?

Fabrizio Genovese (Apr 18 2020 at 22:56):

Like, they are a couple of widespread, intimately related beautiful concepts. Very close, but not enough to have a formally satisfying link between the two. I mean WTF, this hurts my OCD soul badly :D

Fabrizio Genovese (Apr 18 2020 at 22:57):

Jade Master said:

Is the idea that the user specifies only Petri nets and Petri net morphims. Then statebox translates this to pre-nets and pre-net morphisms. This translation is not in the categorical framework once you get their however the rest is categorical?

Yes, I'd say this is a good way to put it. Yes.

Jade Master (Apr 18 2020 at 22:57):

John Baez said:

Jade Master said:

Oh great. That's my favorite :)

You really like nets where there's a total ordering on the set of places? Oh are you being sarcastic?

No I am not being sarcastic. It's also the left adjoint into strict symmetric monoidal categories that I like.

Fabrizio Genovese (Apr 18 2020 at 22:58):

The difference in giving directly prenets to the user is that if we do so then many morphisms are not allowed anymore. And all these morphisms look intuitively ok from a graphical perspective, so the whole interface becomes cumbersome

Fabrizio Genovese (Apr 18 2020 at 22:58):

So we instead decide to do it under the hood for you

Jade Master (Apr 18 2020 at 22:58):

That makes sense.

Fabrizio Genovese (Apr 18 2020 at 22:59):

But as I said, this is not something we are doing right now. For now we do not support morphing nets yet

Fabrizio Genovese (Apr 18 2020 at 22:59):

...Which also means we are very flexible if someone has a brilliant idea that saves the day :D

John Baez (Apr 18 2020 at 22:59):

Jade Master said:

John Baez said:

Jade Master said:

Oh great. That's my favorite :)

You really like nets where there's a total ordering on the set of places? Oh are you being sarcastic?

No I am not being sarcastic. It's also the left adjoint into strict symmetric monoidal categories that I like.

A total order on the set of places, or a total order on the set of inputs of each transition, and a total order on the set of outputs of each transition? I really thought Fab meant what he said: a total order on the whole set of places. Maybe he didn't mean it.

Fabrizio Genovese (Apr 18 2020 at 23:01):

I meant that you have a total order on the set of places, not on inputs and outputs

John Baez (Apr 18 2020 at 23:02):

Yeah, good, you meant what you said. I like that in a mathematician.

John Baez (Apr 18 2020 at 23:02):

Now is that really your favorite, Jade???

Fabrizio Genovese (Apr 18 2020 at 23:02):

An "ordered" petri net is a couple $(N, \mathcal{O})$, where $N$ is just a net and $\mathcal{O}$ is a total order on the places of $N$. Morphisms $(N, \mathcal{O}) \to (N', \mathcal{O}')$ are just morphisms $N \to N'$

John Baez (Apr 18 2020 at 23:02):

Is this really your favorite thing, Jade???

Fabrizio Genovese (Apr 18 2020 at 23:03):

So you get a category which is equivalent to Petri, but you use the orderings to pull the trick and turn them into prenets. I don't know if it's Jade's favourite thing. I personally hate it, but couldn't find anything better!

Jade Master (Apr 18 2020 at 23:03):

Fabrizio Genovese said:

I am still _very_ annoyed that there isn't a formally satisfying way to link petri nets (and not pre-nets) with free SMCs (not commutative). I still think it should exists. Its absence is really a big disappointment for the whole world of maths really

@Mike Shulman had an idea about this actually which I hope he doesn't mind sharing. The idea was that instead of having a free commutative monoid on the places...you could use the free symmetric monoidal category on the set of places.

Fabrizio Genovese (Apr 18 2020 at 23:04):

But this isn't similar to prenets?

Fabrizio Genovese (Apr 18 2020 at 23:04):

Oh no wait, it's more like you use nominal string diagrams basically?

Fabrizio Genovese (Apr 18 2020 at 23:05):

You attach to each trasition as input/output some places together with an entire structure that keeps track of the permutations for you, so that you can forget about them

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

John Baez said:

Is this really your favorite thing, Jade???

No lol whoops. I'm not sure why you would want to order all the places instead of just the inputs and outputs of each transition...probably this is easier computationally.

Fabrizio Genovese (Apr 18 2020 at 23:06):

The point is not necessarily if you order input/outputs or the set of places. The point is if you account for this in defining morphisms :slight_smile:

Fabrizio Genovese (Apr 18 2020 at 23:06):

If you do then you get prenets or something very close. If you don't then you get a category equivalent to Petri

Fabrizio Genovese (Apr 18 2020 at 23:07):

Computationally it's very easy to require that $P$, the type of places, is orderable, that's for sure

John Baez (Apr 18 2020 at 23:08):

The basic idea is that when you want to give up on being nice, you put a total ordering on every set in sight so that there are no automorphisms anymore and you can point at any element and say "Hey! You! Do what I tell you!"

Fabrizio Genovese (Apr 18 2020 at 23:08):

Precisely xD

Jade Master (Apr 18 2020 at 23:09):

Fabrizio Genovese said:

You attach to each trasition as input/output some places together with an entire structure that keeps track of the permutations for you, so that you can forget about them

Yeah. The inputs and outputs are equipped with an action of the appropriate symmetric group.

Jade Master (Apr 18 2020 at 23:10):

I don't know nominal sets well enough to say if it is the same.

Fabrizio Genovese (Apr 18 2020 at 23:10):

Yes, I thought about this at some point, when the paper about nominal string diagrams came out. But I never had the time or will to really dig deep into it

Jade Master (Apr 18 2020 at 23:11):

If he doesn't respond on here do you mind if I include you in an email to him regarding this?

John Baez (Apr 18 2020 at 23:12):

Fine with me, but maybe you meant Fab.

John Baez (Apr 18 2020 at 23:12):

I think some set of people should straighten out this stuff and make it categorically beautiful.

Fabrizio Genovese (Apr 18 2020 at 23:13):

Yes please!

John Baez (Apr 18 2020 at 23:13):

I'd be happy to be involved - and perhaps that's necessary for me to feel it's been made beautiful. :upside_down:

Fabrizio Genovese (Apr 18 2020 at 23:13):

And I agree with @John Baez , we should settle this business finally :D

Jade Master (Apr 18 2020 at 23:15):

Okay sounds good. I'll send an email later tonight.

Jade Master (Apr 18 2020 at 23:15):

Including you both.

Fabrizio Genovese (Apr 18 2020 at 23:16):

Cool! Thanks!

Daniel Geisler (Apr 18 2020 at 23:38):

Beyond type A and B? The book Combinatorial Analysis.

Mike Shulman (Apr 18 2020 at 23:42):

Jade Master said:

Mike Shulman had an idea about this actually which I hope he doesn't mind sharing. The idea was that instead of having a free commutative monoid on the places...you could use the free symmetric monoidal category on the set of places.

Actually now I don't remember having that idea. (-: Was it online or in a personal conversation?

sarahzrf (Apr 19 2020 at 01:12):

Jade Master said:

Fabrizio Genovese said:

I am still _very_ annoyed that there isn't a formally satisfying way to link petri nets (and not pre-nets) with free SMCs (not commutative). I still think it should exists. Its absence is really a big disappointment for the whole world of maths really

Mike Shulman had an idea about this actually which I hope he doesn't mind sharing. The idea was that instead of having a free commutative monoid on the places...you could use the free symmetric monoidal category on the set of places.

hmm, isn't this basically the same thing i was suggesting the other day :thinking:

sarahzrf (Apr 19 2020 at 01:12):

wait lmao did u misremember my idea as having been his

sarahzrf (Apr 19 2020 at 01:18):

well, what i was suggesting the other day in any case was something like, upgrade from the lawvere theory of commutative monoids to the 2-lawvere theory of "symmetric monoids" or something—this is, i guess, the same as the "doctrine of SMCs" for the right notion of "doctrine"?

John Baez (Apr 19 2020 at 02:17):

Mike told us that idea a long time ago, so I guess all sufficiently smart people have that idea.

John Baez (Apr 19 2020 at 02:20):

Yeah, there's a Lawvere 2-theory for "symmetric pseudomonoids". The "pseudo" means everything holds up to coherent isomorphisms, e.g. a pseudomonoid in Cat is a monoidal category.

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

It was Day and Street who wrote down the general definition of pseudomonoid.

sarahzrf (Apr 19 2020 at 02:23):

ah, pseudomonoid

sarahzrf (Apr 19 2020 at 02:23):

shoulda come up with that name myself :>

John Baez (Apr 19 2020 at 02:28):

A pseudomonoid is "just" a pseudomonad in a one-object tricategory. But pseudomonad also means something else!

sarahzrf (Apr 19 2020 at 02:29):

pfffthahhaha fully expecting an nlab link

Mike Shulman (Apr 19 2020 at 02:38):

That's surely the obvious thing to do, but I thought it doesn't work because a non-pre net doesn't distinguish between tokens in any way.