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: deprecated: concurrency

Topic: proarrow equipments in concurrency

Chad Nester (Jan 28 2021 at 14:11):

Hi everyone. I'd like to share an idea I've been excited about recently.

The idea is that single object proarrow equipments (from the double categorical perspective) are an algebra of 'concurrent resource transformations' in the same way that monoidal categories are an algebra of 'resource transformations'.

I've written a short (not very technical) paper explaining how this is so. Its been rejected from one conference, and I'm going to submit an ever shorter version to another, but I have a feeling that the idea is going to wind up as a small part of a larger paper, instead of being presented on its own.

I think some of you might be interested, so I'll link the preprint of the short paper here: https://arxiv.org/abs/2010.08233

(I know its got a few typos in. I've fixed them locally, but won't update the arxiv version just yet).

Chad Nester (Jan 28 2021 at 14:13):

I'd love to talk about this, so please don't be shy about questions / comments / connections.

Chad Nester (Jan 28 2021 at 14:20):

(I hope this stream is still alive! :skull_and_crossbones:)

Jade Master (Jan 28 2021 at 15:35):

Cool! It seems to me like you are using double categories to represent concurrency with multiple agents, where the corners represent passing or receiving a resource from another agent. Is this how you think of it @Chad Nester

Jade Master (Jan 28 2021 at 15:38):

I wonder if there are concurrent process languages, like the pi-calculus for example which could be modeled in this framework

Chad Nester (Jan 28 2021 at 15:42):

That's basically right, yes!

Chad Nester (Jan 28 2021 at 15:46):

I'm not necessarily thinking of each cell as an "agent" (I don't really know what that means, so I could be wrong here), but I think that what distinguishes a concurrent system from, say, one in which processes unfold in parallel, is that the material histories of its components are interleaved.

Chad Nester (Jan 28 2021 at 15:47):

The corners make it possible to represent this interleaving, while still being able to separate out the individual components.

Chad Nester (Jan 28 2021 at 15:48):

(Exactly as you say, the corners allow something like "sending" and "receiving" of resources.)

Chad Nester (Jan 28 2021 at 15:55):

Regarding things like the pi-calculus, I've been thinking of this more as a way to "situate" process calculi in the material world than as a process calculus in its own right.

Chad Nester (Jan 28 2021 at 15:55):

... I realise that's a bit cryptic. (There's a draft paper about this but it's too young right now!)

Chad Nester (Jan 28 2021 at 15:59):

For example, it would be nice if we could write down biological processes in some calculus, and then have them generate 'resource transformations' explaining, say, how the biomolecules involved have changed (the "material history" part) as they unfold. I think we need both perspectives (process calculus + material effects) to get a satisfying account.

John Baez (Jan 28 2021 at 16:04):

What's the difference between "biological processes" and "how the molecules have changed"? Is the former a more abstract description that doesn't talk about molecules?

John Baez (Jan 28 2021 at 16:04):

(I'm really interested in these biological questions. Are you?)

Chad Nester (Jan 28 2021 at 16:06):

John Baez said:

(I'm really interested in these biological questions. Are you?)

Extremely. Although It's more of a hobby at the moment.

Chad Nester (Jan 28 2021 at 16:08):

John Baez said:

What's the difference between "biological processes" and "how the molecules have changed"? Is the former a more abstract description that doesn't talk about molecules?

I would say that how the molecules change is an important aspect of these processes, but not the only one. We also need to capture the way in which the parts of a system constrain each other.

Chad Nester (Jan 28 2021 at 16:09):

... I'm not terribly happy with that answer

Fabrizio Genovese (Jan 28 2021 at 16:11):

Chad Nester said:

John Baez said:

What's the difference between "biological processes" and "how the molecules have changed"? Is the former a more abstract description that doesn't talk about molecules?

I would say that how the molecules change is an important aspect of these processes, but not the only one. We also need to capture the way in which the parts of a system constrain each other.

Me, @fosco and @Daniele Palombi have another perspective on this, coming from the work of Rosen, and this is what we based the ManaNets paper on. Biological processes are a bunch of chemical reactions such that:

• Some reactions require some metabolytes to happen
• These metabolytes degrade over time
• These metabolytes are produced by other reactions in the process, so that the system kinda self-sustains.

Fabrizio Genovese (Jan 28 2021 at 16:11):

The emphasis here is on the fact that the real difference between "chemistry" and "life" is that life arranges chemical reactions so that they repair themselves.

Fabrizio Genovese (Jan 28 2021 at 16:12):

We're throwing quite a lot of stuff at this problem now, mana nets was a thing, we have another description in terms of fixed point theorems that we'll release at some point I hope. :smile:

Fabrizio Genovese (Jan 28 2021 at 16:16):

In any case, back to the original issue: I am not a fan of describing concurrent processes in terms of messages. There are very deep reasons for this, but in a nutshell: A concurrent system is made of two layers:

• A network layer, where messages get exchanged. The network can also dynamically change in time, and you should also take into account things like latencies etc to model race conditions.
• A local layer, that is, the computation that each machine executes locally.
  All the frameworks I've seen so far either ignore the network layer (e.g. lambda calculus, FSMs) or ignore the local layer (e.g. pi calculus, Petri nets). We won't go anywhere until we merge the two approaches into a unique condition. I've tried to do so using sheaves for two years and with the help of many people (lately mainly @Matteo Capucci (he/him) ), but it's effing hard, and I'm not anymore convinced that sheaves are the right way to tackle this. If someone is interested in pursuing this line of research, or to suggest any possible mathematical tool to model this, please let me know, I'm ->Super<- interested in this.

Fabrizio Genovese (Jan 28 2021 at 16:17):

When you try to get deeper into this you realize that this problem is "slimy". Everywhere you turn there's something that evades you, or that you aren't modelling.. In the end, it's very difficult to come up with a model that formalizes this correctly while being manageable enough to crunch some numbers.

Fabrizio Genovese (Jan 28 2021 at 16:18):

Chad Nester said:

Fabrizio Genovese I think this might be close to what I mean by "situating" process calculi.

In this respect, I agree that you could see this as a bunch of process calculi happening locally, and coordinated by a network layer. Still, very difficult to properly frame it

Chad Nester (Jan 28 2021 at 16:19):

(sorry I deleted that message!)

Fabrizio Genovese (Jan 28 2021 at 16:19):

no worries xD

Fabrizio Genovese (Jan 28 2021 at 16:20):

Just to give an estimate of how hard this is: You network may not be (usually it is not) stable even vertex-wise: New nodes can join/ef off the protocol ad libitum

Chad Nester (Jan 28 2021 at 16:45):

I agree that that's a slippery problem. I'm certainly not claiming to have solved it!

John Baez (Jan 28 2021 at 16:50):

Fabrizio Genovese said:

When you try to get deeper into this you realize that this problem is "slimy". Everywhere you turn there's something that evades you, or that you aren't modelling. In the end, it's very difficult to come up with a model that formalizes this correctly while being manageable enough to crunch some numbers.

Hey, biology is slimy. If life were simple to describe, other life would emerge that would take advantage of this simplicity to eat it up.

John Baez (Jan 28 2021 at 16:50):

Every possible loophole or "leaky abstraction" gets exploited.

Daniele Palombi (Jan 28 2021 at 17:14):

Hi Chad,
Really cool paper! Can't wait to hear/read more about this!

Jade Master (Jan 28 2021 at 18:07):

Fabrizio Genovese said:

In any case, back to the original issue: I am not a fan of describing concurrent processes in terms of messages. There are very deep reasons for this, but in a nutshell: A concurrent system is made of two layers:

• A network layer, where messages get exchanged. The network can also dynamically change in time, and you should also take into account things like latencies etc to model race conditions.
• A local layer, that is, the computation that each machine executes locally.
  All the frameworks I've seen so far either ignore the network layer (e.g. lambda calculus, FSMs) or ignore the local layer (e.g. pi calculus, Petri nets). We won't go anywhere until we merge the two approaches into a unique condition. I've tried to do so using sheaves for two years and with the help of many people (lately mainly Matteo Capucci (he/him) ), but it's effing hard, and I'm not anymore convinced that sheaves are the right way to tackle this. If someone is interested in pursuing this line of research, or to suggest any possible mathematical tool to model this, please let me know, I'm ->Super<- interested in this.

I suppose that I don't entirely understand this distinction. I would say that Petri nets can do both, either model the computations on a specific machine or model the coordination between machines. Similarly, FSM's can also model on both levels. Is your point that they don't model at both levels at the same time? If so there are various ways to make Petri nets Hierarchical which I think you might already be aware of... .

Jade Master (Jan 28 2021 at 18:10):

In some sense open Petri nets can model this type of hierarchy, each open Petri net can represent an individual machine which can be joined along various message passing channels to form the larger system. There are also elementary object systems which I am personally a fan of.

fosco (Jan 28 2021 at 18:11):

I'll reply to this soon-ish, today I'm out of the games, not feeling well

fosco (Jan 28 2021 at 18:13):

...oh, well, I can copypaste a message that I sent on the ACT4E zulip channel

fosco (Jan 28 2021 at 18:19):

My interest in Rosen's work can be summarised in the fact that some of the properties of living systems that Rosen tried to express in categorical language can indeed be expressed as such, just relying not on 1-categories, but on 2- or bi-categories. (This is where some form of proarrow-equipmentish-calculus could turn out to be useful)

It was an intuition of Cǎzǎnescu and Baianu that a category of (M,R)-systems can be expressed as a category of automata in a cartesian closed category. I suspect one can extract a more faithful description of (M,R)-systems by performing the same categorical construction of Cǎzǎnescu-Baianu but in a linearly distributive category. After all, chemical reactions are linear. (I found there's already a very enticing paper on a "$\lambda$-calculus for chemical reactions", weeks ago, but in the end I didn't enter the white rabbit hole).

Another compelling connection I've found is with untyped $\lambda$-calculus: when interpreted in cartesian closed categories, (M,R)-systems tend to generate reflexive objects, i.e. types $A$ that are isomorphic to their type of endofunction $A^A$. This is not by chance, and it's a feature of "equations" in a cartesian closed category that is tightly linked to Lawvere's fixed point theory in a CCC, in a way I'm trying to understand better: in fact, I've found that to every "admissible" (M,R)-system (with respect to a notion of "admissibility" that Rosen never spells out in a comprehensible manner, at least for a mathematician :grinning: ) one can associate a system of "type equations"

$\begin{cases} F_1(X_1)\cong X_1\\ \vdots \\ F_k(X_k)\cong X_k \end{cases}$

whose solutions will be the "stable states" of the (M,R)-system. [Insert here related work by Leinster]

I would also like to get rid of the cartesian closed assumption and interpret (M,R)-systems in some kind of bicategory modeled on $\sf Prof$ (the equipment of profunctors); most of the definitions in Rosen-Louie are inherently relational/profunctorial, and in fact some ugly uniqueness that Rosen is forced to require because he's working in the category of sets can be more elegantly avoided passing to the bicategory of relations; again, this is something that Louie sketched, but -afaicu- didn't fully exploit (mostly because he didn't know anything about the internal language of bicategories of profunctors, I guess?)

dan pittman (Jan 28 2021 at 19:25):

Jade Master said:

I suppose that I don't entirely understand this distinction. I would say that Petri nets can do both, either model the computations on a specific machine or model the coordination between machines. Similarly, FSM's can also model on both levels. Is your point that they don't model at both levels at the same time? If so there are various ways to make Petri nets Hierarchical which I think you might already be aware of... .

I work on a system that generates traces of communicating “threads of execution”, some of which is open sourced here. The distinction, to me, w/r/t the “levels” is that depending on how we structure the trace data, we get one version where we see things as independent agents or actors with points of synchronization, I call this the timeline view. Something like

type Timelines = HashMap<ProcessId, Vec<Event>>;

Or in a graph view where the notion of “threads of execution” are erased; usually represented in the usual node and edge list way. I say this all to say that we can model both, just not at the same time.

Jade Master (Jan 28 2021 at 20:06):

dan pittman said:

Jade Master said:

I suppose that I don't entirely understand this distinction. I would say that Petri nets can do both, either model the computations on a specific machine or model the coordination between machines. Similarly, FSM's can also model on both levels. Is your point that they don't model at both levels at the same time? If so there are various ways to make Petri nets Hierarchical which I think you might already be aware of... .

I work on a system that generates traces of communicating “threads of execution”, some of which is open sourced here. The distinction, to me, w/r/t the “levels” is that depending on how we structure the trace data, we get one version where we see things as independent agents or actors with points of synchronization, I call this the timeline view. Something like

type Timelines = HashMap<ProcessId, Vec<Event>>;

Or in a graph view where the notion of “threads of execution” are erased; usually represented in the usual node and edge list way. I say this all to say that we can model both, just not at the same time.

Interesting. Do you think that your system would benefit from modeling both at the same time?

dan pittman (Jan 28 2021 at 20:19):

Maybe? Our commercial offering does analysis against these graphs, things like satisfiability &c, and depending on which form the particular analysis at hand needs, we build one graph type or the other. This seems fine from an engineering standpoint because we're going to optimize the structure of the data as needed anyway, but in terms of having a cohesive way to express to a user what her system did, I'd say that'd be very interesting. I probably can't hang with most of the CT in this paper, but I'm going to give it a read anyway, for sure—if only to see what intuitions shake out.

Eric Forgy (Jan 28 2021 at 20:23):

(btw, Auxon looks cool :+1:)

Fabrizio Genovese (Jan 28 2021 at 22:41):

Petri nets can represent concurrency well, but they are nowhere close to representing what I'm talking about. Few reasons for this:

Fabrizio Genovese (Jan 28 2021 at 22:44):

• You can use Petri nets to represent local, multi-threaded computation. This works reasonably well.
• You can use Petri nets to represent information flow in a network. This works really not well, mainly because the network varies dynamically, and also because to be of any practical use you cannot model message passing as a point-to-point event. Messages on real network get broadcasted, that is, send to many machines at the same time. Representing this by adding a lot of transitions around that copy resources is not going to fly.
• Representing both things at the same time requires some level of hiearchy, but in this framework you want the places of a net to be Petri nets themselves. This is not exactly what the literature has been doing so far.

Fabrizio Genovese (Jan 28 2021 at 22:45):

By the way, my sheaf-theoretic approach to this problem (that went nowhere) was mainly motivated by point 2 above: Nearly all examples of connectivity/compositionality in ACT are point to point. This includes open petri nets, wiring diagrams, string diagrams, quantum stuff. I don't think this approach is really insightful in describing big networks of computers and P2P protocols, that work on completely different assumptions.

Fabrizio Genovese (Jan 28 2021 at 22:47):

For instance, if I request a file in a P2P network I'm sending a message around saying "hey, who has this file?" Every machine having it will maybe reply to me. Others will just discard the message. The message is broadcasted around until the network is saturated. In this case describing things as a sequence of point-to-point communication just makes things murky.

Fabrizio Genovese (Jan 28 2021 at 22:48):

There are a ton of protocols - heavily used ones - that work this way (parse what matters to you, discard the rest), e.g. MQTT or the CAN bus. These are easier to describe because they are not decentralized.

Fabrizio Genovese (Jan 28 2021 at 22:51):

What I'm saying is that from an engineering perspective the idea of compositionality as "the act of composing two systems" won't fly if the system described is really big. I was thinking about writing a non-technical paper about this for the next ACT, and submitting it as non-proceeding. "compositionality for big systems" is definitely something we will have to think about a few years from now :smile:

Matteo Capucci (he/him) (Jan 28 2021 at 22:53):

Fab you keep describing my future PhD thesis, I'm starting to think you are me from the future :grinning_face_with_smiling_eyes: in that case I have some questions

Matteo Capucci (he/him) (Jan 28 2021 at 22:54):

What I mean is, we ask the same questions and poke the same holes; not that I currently have answers

Matteo Capucci (he/him) (Jan 28 2021 at 22:57):

A thought I had somewhen last week, since we often spoke about sheaves in this context. Sheaves might not be the right tools for this job, at least not naively, because sheaves talk about local things. As soon as you want to be able to talk about non-local phenomena (see mana nets) you gotta abandon the sheaf condition.
Implicitly, I also realized this when I gave my talk about sheaves and I described cohomology of behaviour as the cohomology of the augmented Cech complex. In layman terms, this means not taking separation and glueing for granted by measuring their failures as well.

Jade Master (Jan 28 2021 at 23:05):

This conversation is motivating me to write a blog post about elementary object systems :thinking:

Fabrizio Genovese (Jan 28 2021 at 23:14):

Matteo Capucci (he/him) said:

Fab you keep describing my future PhD thesis, I'm starting to think you are me from the future :grinning_face_with_smiling_eyes: in that case I have some questions

We should start talking about this stuff again at some point. Atm I'm really working on too many different things, but I hope to be able to get back to the stuff I wrote above in the future.

Matteo Capucci (he/him) (Jan 29 2021 at 06:57):

Fabrizio Genovese said:

Matteo Capucci (he/him) said:

Fab you keep describing my future PhD thesis, I'm starting to think you are me from the future :grinning_face_with_smiling_eyes: in that case I have some questions

We should start talking about this stuff again at some point. Atm I'm really working on too many different things, but I hope to be able to get back to the stuff I wrote above in the future.

Same... I feel like a week enclosed in a constrained space without other projects to bring about would greatly benefit these thoughts... but pandemic

Fabrizio Genovese (Jan 29 2021 at 10:00):

T_T

Christian Williams (Jan 31 2021 at 02:39):

I'm catching up here. great paper! the drawings and explanations are nice.

Christian Williams (Jan 31 2021 at 02:41):

at first I thought that Tile Logic could be related https://www.researchgate.net/publication/2498696_Tile_Logic_for_Synchronized_Rewriting_of_Concurrent_Systems
but they seem to be different.

Christian Williams (Jan 31 2021 at 02:44):

it seems like you started with wondering "how can we break up these string diagrams into distinct processes?" and found this nice proarrow "corner" structure as a result. how did you get into this?

Christian Williams (Jan 31 2021 at 02:46):

I'm definitely wondering how the $\pi$-calculus might relate to this, but I've come to see that its categorical semantics is pretty elusive. (mainly from what makes it so expressive, the idea of binding on a channel, which enables dynamic network topology)

Christian Williams (Jan 31 2021 at 02:55):

so a square represents a process with top input, bottom output, and sides allow passing of resources. this is very intuitive. but it's a bit funny how this "left and right" come into play; on the surface one might think you can share resources with arbitrary processes in the system. but I suppose it's somehow significant that the horizontal monoid is noncommutative, giving some kind of order to the parallel processes. probably if I knew more about interleaving this would be clear.

Chad Nester (Feb 01 2021 at 09:14):

Christian Williams said:

it seems like you started with wondering "how can we break up these string diagrams into distinct processes?" and found this nice proarrow "corner" structure as a result. how did you get into this?

I was reading about limits in double categories and figured we could probably use the extra dimension to make the string diagrams from https://arxiv.org/abs/math/0703713 a bit more reasonable. I started with many more assumptions, but slowly realized that I could get rid of all of them!

Chad Nester (Feb 01 2021 at 09:15):

... It doesn't really connect back up to the 'logic of message passing' as I'd initially hoped (at least, not yet), but I like the result.

Chad Nester (Feb 01 2021 at 09:17):

Christian Williams said:

I'm catching up here. great paper! the drawings and explanations are nice.

Thanks!

Chad Nester (Feb 01 2021 at 09:18):

RE Tile logic, as far as I can tell it's completely different. I had a look at some of the papers on it, but it didn't seem like they were trying to do the same thing.

Chad Nester (Feb 01 2021 at 09:28):

Christian Williams said:

so a square represents a process with top input, bottom output, and sides allow passing of resources. this is very intuitive. but it's a bit funny how this "left and right" come into play; on the surface one might think you can share resources with arbitrary processes in the system. but I suppose it's somehow significant that the horizontal monoid is noncommutative, giving some kind of order to the parallel processes. probably if I knew more about interleaving this would be clear.

I've managed to convince myself that the "left and right" thing is pretty natural. I think you're talking about what I would call the 'vertical monoid' (occupying the left and right boundaries), in which case the noncommutativity comes from not being able to give something away before you have it (in general, anyway).

Chad Nester (Feb 01 2021 at 09:37):

More visually, the noncommutativity comes from being able to bend wires 'down', but not 'up'. Since we're thinking of events as unfolding from top to bottom, this is like insisting that we must have a thing in order to use it.

Chad Nester (Feb 01 2021 at 09:56):

dan pittman said:

Our commercial offering does analysis against these graphs, things like satisfiability &c, and depending on which form the particular analysis at hand needs, we build one graph type or the other. This seems fine from an engineering standpoint because we're going to optimize the structure of the data as needed anyway, but in terms of having a cohesive way to express to a user what her system did, I'd say that'd be very interesting. I probably can't hang with most of the CT in this paper, but I'm going to give it a read anyway, for sure—if only to see what intuitions shake out.

I'd be pretty interested to hear your thoughts about this. I mostly talk to theoreticians but I'd be happy if my work was helping people outside of my bubble. Feel free to message me if you get stuck with the paper!

Alex Gryzlov (Mar 19 2021 at 01:03):

Fabrizio Genovese said:

In any case, back to the original issue: I am not a fan of describing concurrent processes in terms of messages. There are very deep reasons for this, but in a nutshell: A concurrent system is made of two layers:

• A network layer, where messages get exchanged. The network can also dynamically change in time, and you should also take into account things like latencies etc to model race conditions.
• A local layer, that is, the computation that each machine executes locally.
  All the frameworks I've seen so far either ignore the network layer (e.g. lambda calculus, FSMs) or ignore the local layer (e.g. pi calculus, Petri nets). We won't go anywhere until we merge the two approaches into a unique condition. I've tried to do so using sheaves for two years and with the help of many people (lately mainly Matteo Capucci (he/him) ), but it's effing hard, and I'm not anymore convinced that sheaves are the right way to tackle this. If someone is interested in pursuing this line of research, or to suggest any possible mathematical tool to model this, please let me know, I'm ->Super<- interested in this.

"Concurrency" is a pretty overloaded term, but in programming it usually means local computation, and what you get by adding various network effects (dynamic topology, partitions, crashes/byzantine behaviour etc) is usually grouped under the term "distributed systems". The border between the two is of course pretty fuzzy because of stuff like weak memory models, where each CPU core and its cache is essentially a separate agent which must negotiate with others, which sometimes introduces some bizzare side-effects in the execution.

Tom Hirschowitz (Mar 19 2021 at 06:18):

Jade Master said:

Fabrizio Genovese said:

In any case, back to the original issue: I am not a fan of describing concurrent processes in terms of messages. There are very deep reasons for this, but in a nutshell: A concurrent system is made of two layers:

• A network layer, where messages get exchanged. The network can also dynamically change in time, and you should also take into account things like latencies etc to model race conditions.
• A local layer, that is, the computation that each machine executes locally.
  All the frameworks I've seen so far either ignore the network layer (e.g. lambda calculus, FSMs) or ignore the local layer (e.g. pi calculus, Petri nets). We won't go anywhere until we merge the two approaches into a unique condition. I've tried to do so using sheaves for two years and with the help of many people (lately mainly Matteo Capucci (he/him) ), but it's effing hard, and I'm not anymore convinced that sheaves are the right way to tackle this. If someone is interested in pursuing this line of research, or to suggest any possible mathematical tool to model this, please let me know, I'm ->Super<- interested in this.

I suppose that I don't entirely understand this distinction. I would say that Petri nets can do both, either model the computations on a specific machine or model the coordination between machines. Similarly, FSM's can also model on both levels. Is your point that they don't model at both levels at the same time? If so there are various ways to make Petri nets Hierarchical which I think you might already be aware of... .

Sorry I'm late on this one, but I don't understand either, in a different way: I would say that $\pi$-calculus also does both. Obviously, messages implement the network layer, but the $\pi$-calculus is also Turing complete (there are quite a few faithful translations from the $\lambda$-calculus out there), so it may also represent the local layer. Am I missing something?

Fabrizio Genovese (Mar 19 2021 at 12:38):

No, you are totally right. $\pi$ calculus, being turing complete, can represent any computation _in terms of messages_, and that's my point! What I mean is that networks and local computations, in my opinion, are conceptually very different. Networks are best explained using messages, local computations using stuff like lambda calculus. All the models I've seen so far throw everything in the same bucket: pi calculus describes everything in terms of messages for instance, which makes it cumbersome to do some of the things that lambda calculus does easily. lambda calculus does not have a notion of message or channel, and so network models become difficult to express in that framework. All these models are pretty extreme, meaning that you are looking at everything using the same conceptual filter.

Fabrizio Genovese (Mar 19 2021 at 12:39):

In ordinary infrastructure we have a network layer and a local layer. These are both ultimately the same if you describe them as "electrons going around" but really have much much different conceptual flavors, and all the models I've seen so far discard one of these flavors to favor the other. I don't think this makes real justice to the task of describing what things like consensus protocols are

Fabrizio Genovese (Mar 19 2021 at 12:41):

So, Ideally, I would like something that has enough depth so that we can talk about networks and local computations using different dictionaries, but in a way so that these different dictionaries end up being compatible. BTW, my work with @Matteo Capucci (he/him) on this has stalled for now, saying something meaningful ended up proving much harder than we expected.

Fabrizio Genovese (Mar 19 2021 at 12:47):

Maybe, to clarify, try to invert things: As (I think) Samson Abramsky once asked, "which function does the Internet compute?"
Theoretically, you _could_ come up with something a program for a Turing machine that computes the internet. You can for sure because of Turing completeness. We all know that this approach won't fly tho.
I think pi calculus didn't really become popular among programmers for a similar reason: It is great to model messaging infrastructure, but it is incredibly cumbersome for modelling task that are menial in other languages. All in all I think all these paradigms fall short of something when you employ them to model mixed systems where local computations, messaging and (maybe) data storage/retrieve are all happening at the same time.

Tom Hirschowitz (Mar 19 2021 at 12:52):

Aha, this is starting to make sense to me. Are you looking for something like Leroy's modular module system, but for $\pi$-calculus? Explicitly, are you attempting to view $\pi$-calculus as a language fragment, interacting with another, more local fragment, in a way that is perhaps parametric in the latter?

In passing, @Clovis Eberhart, @Thomas Seiller, and I did some work on a sheaf-based model for $\pi$-calculus, in case you're interested. There, the sheaf condition says that the future behaviour of each node in the network from some point in time should depend only on its own history, which in particular entails that each node behaves independently from others.

Fabrizio Genovese (Mar 19 2021 at 12:57):

So, I didn't look at calculi, the approach we were taking was mainly semantic. This is basically due to the fact that I (and I guess Matteo) know categories better than I know calculi. But yes, I think we are basically saying the same thing

Jake Gillberg (Mar 19 2021 at 13:55):

Fabrizio Genovese said:

In any case, back to the original issue: I am not a fan of describing concurrent processes in terms of messages. There are very deep reasons for this, but in a nutshell: A concurrent system is made of two layers:

• A network layer, where messages get exchanged. The network can also dynamically change in time, and you should also take into account things like latencies etc to model race conditions.
• A local layer, that is, the computation that each machine executes locally.
  All the frameworks I've seen so far either ignore the network layer (e.g. lambda calculus, FSMs) or ignore the local layer (e.g. pi calculus, Petri nets). We won't go anywhere until we merge the two approaches into a unique condition. I've tried to do so using sheaves for two years and with the help of many people (lately mainly Matteo Capucci (he/him) ), but it's effing hard, and I'm not anymore convinced that sheaves are the right way to tackle this. If someone is interested in pursuing this line of research, or to suggest any possible mathematical tool to model this, please let me know, I'm ->Super<- interested in this.

@Fabrizio Genovese Have you looked into Milner's later work on "bigraphs"? They were created to subsume process calculi and have exactly the two layers you describe: A DAG to represent locality, and a graph to represent network connections.

Alex Gryzlov (Mar 19 2021 at 15:16):

Fabrizio Genovese said:

So, Ideally, I would like something that has enough depth so that we can talk about networks and local computations using different dictionaries, but in a way so that these different dictionaries end up being compatible. BTW, my work with Matteo Capucci (he/him) on this has stalled for now, saying something meaningful ended up proving much harder than we expected.

Sounds like you're looking for models that combine shared-state and message-passing concurrency, so some recent dist-systems literature on state machine replication could be relevant here, e.g. Aguilera, Ben-David, Calciu, Guerraoui, Petrank, Toueg, [2018] "Passing Messages while Sharing Memory"

Alex Gryzlov (Mar 19 2021 at 15:31):

Tom Hirschowitz said:

Aha, this is starting to make sense to me. Are you looking for something like Leroy's modular module system, but for $\pi$-calculus? Explicitly, are you attempting to view $\pi$-calculus as a language fragment, interacting with another, more local fragment, in a way that is perhaps parametric in the latter?

In passing, Clovis Eberhart, Thomas Seiller, and I did some work on a sheaf-based model for $\pi$-calculus, in case you're interested. There, the sheaf condition says that the future behaviour of each node in the network from some point in time should depend only on its own history, which in particular entails that each node behaves independently from others.

Game-semantical models also seem to be tied to module systems, and there has been some separate work on GS for both modules and distributed execution.

Fabrizio Genovese (Mar 19 2021 at 16:02):

So, my main idea/hope was this: Sheaves are a way to globally organize a bunch of local information. Here, if I take "local information" to be what happens on a single machine, the it should be possible to express this local vs global thing using the language of sheaves. One would organize a bunch of machines into a (pre)sheaf, which would represent the act of consistently organizing those machines (by sharing messages and resources). We tried to investigate this point of view for quite a while but got absolutely nothing out of it, so I am afraid I cannot be more precise as of now...

Uli Fahrenberg (Mar 22 2021 at 13:53):

So, I'm also late on this one :shrug:
@Chad Nester are your cornerings related to connections in double cats, in the sense of Brown-Mosa? I guess they did connections only for symmetric double cats, but this should be easy to extend to your non-symmetric case?

Chad Nester (Mar 22 2021 at 14:02):

My understanding of the terminological situation is that "proarrow equipment", "connection structure", "companion and conjoint structure", and "framed bicategory" can all be construed to mean the same thing (I would love to be corrected). This thing is the same as having "corners", which I personally find to be much saner terminology in light of the string diagrams.

Chad Nester (Mar 22 2021 at 14:04):

The main reason I've used symmetric monoidal categories here is that the "crossing cells" in the free cornering arise from the braidings.

Chad Nester (Mar 22 2021 at 14:06):

I expect that "has crossing cells" is nearly the same thing as "is a monoidal double category" in the single-object case, so you can probably get rid of the assumption of symmetry and just ask for it to be a monoidal double category directly.

Chad Nester (Mar 22 2021 at 14:06):

Ah I see that you're actually asking something different. Give me a minute!

Chad Nester (Mar 22 2021 at 14:15):

Following appendix A of Mike Shulman's paper on framed bicategories, it looks like the connection structure of Brown-Mosa was in fact only conjoint structure, in the special case of double categories that are edge symmetric.

Chad Nester (Mar 22 2021 at 14:16):

So the analogue of connection structure in that sense should be the $\circ$-corner structure. (or possibly the $\bullet$-corner structure, I get confused about this sometimes).

Uli Fahrenberg (Mar 24 2021 at 08:30):

Ah thank you, also for the pointer to Mike's paper. I dabbled in those things some 15 years ago, I can see that my terminology is outdated :smile:

Chad Nester (Apr 01 2021 at 20:32):

For anyone keeping tabs, a truncated version of this paper (no compact closed part) has been accepted for publication in a conference called COORDINATION. :surprise: :tada:

Chad Nester (May 11 2021 at 08:04):

I made a few intentionally vague remarks in the discussion above about “situated” transition systems. There is now a preprint (of my ACT submission :sweat:) that explains what I mean by this. The corner structure from the initial post in this thread is the key idea, so I think it makes sense to keep talking here.

I’d love to hear any thoughts, and would be happy to respond to any questions.

Fabrizio Genovese (May 11 2021 at 11:40):

Very nice! I read the paper where you did the corner stuff using double categories with one object and it was nice

Fabrizio Genovese (May 11 2021 at 11:40):

I skimmed through this and I see that you are using that machinery to say things about transition systems. It is going to be an interesting read

Fabrizio Genovese (May 11 2021 at 11:42):

BTW, it is possible me, Fosco and Daniele have already an application for this stuff. We planned to submit to CALCO so we formalized things using different stuff and the deadline is too soon to change things now, but I'd be happy to see if with your work things can be made better. Maybe we can talk as soon as this hellish deadline season ends?

Chad Nester (May 11 2021 at 11:49):

Thanks. I'd certainly be interested in collaborating. No hurry though. :smile:

Robin Piedeleu (May 11 2021 at 13:33):

I'd also read the first version and enjoyed it. The connection with transition systems in this one seems like a nice addition! In particular it seems to give another really nice motivation for the distinction between the horizontal and vertical axes (which was the key conceptual contribution of the first version, if I understood correctly).

Chad Nester (May 11 2021 at 14:17):

Thanks. I think that's a fair summary of the first part. The direction I'm hoping to go next uses techniques from your PhD thesis. :grinning:

Robin Piedeleu (May 11 2021 at 20:40):

Cool! I suppose what I focused on in my thesis was a rather restricted subcategory of Span(Graph). I only skimmed the new version of your paper but could some of your situated transition systems be described concisely by Petri nets with boundaries or, conversely, couldn't Petri nets with boundaries be seen as generating free cornerings? This might provide a nice point of contact between the work on Petri nets as generators of free SMCs and the work on Petri nets with boundaries.

Chad Nester (May 12 2021 at 09:10):

I confess to knowing essentially nothing about Petri nets. My understanding is that a Petri net is essentially a monoidal signature, with the places giving the atomic objects and the transitions giving the generating morphisms. Then the associated symmetric monoidal category is called the category of "executions" of the Petri net. I had a look at the decorated cospans version of open Petri nets, thinking it might be an instance of the corner structure, but as far as I can tell this isn't the case. Is there a different version of Petri nets with boundaries?

A related question, open to anyone reading this: I'm under the impression that people don't usually impose equations on the monoidal signature associated with a Petri net. From the resource theory view of monoidal signatures this is extremely natural, which seems like an advantage. Am I wrong?

Chad Nester (May 12 2021 at 09:12):

I get the impression that the category of executions of a Petri net is usually treated more like a transition system, so maybe it would be a better fit with the existing literature to use them to define the $\mathsf{span(RGraph)}$ part of a situated system. It seems plausible that the decorated cospan version of open Petri nets (or indeed, the version of open Petri nets in your thesis) would work well here.

Fabrizio Genovese (May 12 2021 at 09:53):

Chad Nester said:

I confess to knowing essentially nothing about Petri nets. My understanding is that a Petri net is essentially a monoidal signature, with the places giving the atomic objects and the transitions giving the generating morphisms. Then the associated symmetric monoidal category is called the category of "executions" of the Petri net. I had a look at the decorated cospans version of open Petri nets, thinking it might be an instance of the corner structure, but as far as I can tell this isn't the case. Is there a different version of Petri nets with boundaries?

Yes, there is. The open Petri nets defined by people like @Pawel Sobocinski , @Robin Piedeleu , Fabio Gadducci and others from the school of Pisa generaly glue along transitions instead than on places

Fabrizio Genovese (May 12 2021 at 09:55):

This is very hand-wavy said this way, but if you wish this is a "synchronous" gluing, meaning that if a transition fires, the transition it is glued with has to fire as well. This definition is way more manageable in terms of studying the reachability relation of a net from its components, whereas gluing on places, albeit more intuitive, is problematic because it is asynchronous: When you put a token in a place, you never know which transition will use it, and when

Fabrizio Genovese (May 12 2021 at 09:56):

Chad Nester said:

A related question, open to anyone reading this: I'm under the impression that people don't usually impose equations on the monoidal signature associated with a Petri net. From the resource theory view of monoidal signatures this is extremely natural, which seems like an advantage. Am I wrong?

Actually we do, depending on how you want to obtain categories from nets. In the paper @John Baez , me, @Jade Master and @Mike Shulman published recently, we show how if, say, you want to generate a symmetric monoidal category from a Petri net, you need to impose some equations

Fabrizio Genovese (May 12 2021 at 09:56):

https://arxiv.org/abs/2101.04238

Fabrizio Genovese (May 12 2021 at 09:58):

Chad Nester said:

I get the impression that the category of executions of a Petri net is usually treated more like a transition system, so maybe it would be a better fit with the existing literature to use them to define the $\mathsf{span(RGraph)}$ part of a situated system. It seems plausible that the decorated cospan version of open Petri nets (or indeed, the version of open Petri nets in your thesis) would work well here.

Here I don't think I agree, the most important thing of the category of executions of a Petri net is that it is monoidal, and as such you have an interchange law given by the functoriality of the tensor product. This basically models concurrency, that is, the idea that if two boxes (transitions) are causally independent, it doesn't matter which one comes first (which transition fires first)

Fabrizio Genovese (May 12 2021 at 09:59):

All in all, I think that the main way you can think of a Petri net is as a state machine where:

• You can be in more than one state at the same time (given by where are your tokens, in contrast with FSMs where you can be in one vertes of the graph at best)
• You can walk multiple paths of the graph at the same time

Chad Nester (May 12 2021 at 10:09):

Fabrizio Genovese said:

Actually we do, depending on how you want to obtain categories from nets. In the paper John Baez , me, Jade Master and Mike Shulman published recently, we show how if, say, you want to generate a symmetric monoidal category from a Petri net, you need to impose some equations

Do you impose the same equations every time in order to obtain the same categorical structure? The point I'm trying to make is that by imposing equations on my resource theory, I can insist that certain sequences of events have the same material effect (see the part of the situated systems writeup about $\mathfrak{B}_\mathsf{sift}$ and equality). It's "user-facing", in that if I want to use the machinery this is a parameter I can fiddle with.

Chad Nester (May 12 2021 at 10:11):

I'll look into Petri nets glued along transitions -- thanks!

Chad Nester (May 12 2021 at 10:12):

I know "concurrency" is a loaded word but I don't think that interchange / functoriality of $\otimes$ models it. I agree that it models a kind of independence, but I think this is a different thing.

Chad Nester (May 12 2021 at 10:22):

Fabrizio Genovese said:

All in all, I think that the main way you can think of a Petri net is as a state machine where:

• You can be in more than one state at the same time (given by where are your tokens, in contrast with FSMs where you can be in one vertes of the graph at best)
• You can walk multiple paths of the graph at the same time

I will have to think about this. It feels like a pretty strange way of putting things :dizzy:

Fabrizio Genovese (May 12 2021 at 10:50):

Chad Nester said:

Fabrizio Genovese said:

All in all, I think that the main way you can think of a Petri net is as a state machine where:

• You can be in more than one state at the same time (given by where are your tokens, in contrast with FSMs where you can be in one vertes of the graph at best)
• You can walk multiple paths of the graph at the same time

I will have to think about this. It feels like a pretty strange way of putting things :dizzy:

It is the most natural, Petri nets done categorically are the niche, not the other way around

Fabrizio Genovese (May 12 2021 at 10:51):

Chad Nester said:

Fabrizio Genovese said:

Actually we do, depending on how you want to obtain categories from nets. In the paper John Baez , me, Jade Master and Mike Shulman published recently, we show how if, say, you want to generate a symmetric monoidal category from a Petri net, you need to impose some equations

Do you impose the same equations every time in order to obtain the same categorical structure? The point I'm trying to make is that by imposing equations on my resource theory, I can insist that certain sequences of events have the same material effect (see the part of the situated systems writeup about $\mathfrak{B}_\mathsf{sift}$ and equality). It's "user-facing", in that if I want to use the machinery this is a parameter I can fiddle with.

The point is that you do this if you want to use Petri nets to present monoidal category. Traditionally, this is not what Petri nets are made for. You can do it in any case, I just don't think it is too interesting for people studying Petri nets

Fabrizio Genovese (May 12 2021 at 10:52):

Chad Nester said:

I know "concurrency" is a loaded word but I don't think that interchange / functoriality of $\otimes$ models it. I agree that it models a kind of independence, but I think this is a different thing.

There is much more to concurrency than this, clearly. Still, this is a pretty important property, it's not by chance that nearly all theories exhibiting some form of non-trivial causality are monoidal

Robin Piedeleu (May 12 2021 at 14:47):

Chad Nester said:

I had a look at the decorated cospans version of open Petri nets, thinking it might be an instance of the corner structure, but as far as I can tell this isn't the case. Is there a different version of Petri nets with boundaries?

@Fabrizio Genovese already answered some of your questions so I'll only try to develop a bit what I hinted at earlier and answer this question of yours. My vision may be extremely naive at this point because I've never worked properly on the Petri net-as-SMC view. More knowledgeable people in this area should definitely correct me if they think there's a fundamental obstacle to developing what I had in mind.

If you only care about reachability, you can view a Petri net as just a collection transitions, i.e. of $|P|$ dimensional $\mathbb Z$-vectors, where $P$ is the set of places Then valid runs are sequences of points in the lattice $\mathbb N^P$ such that, starting at any of them one can reach the next adding (i.e. firing) one of the transition to it.

But if you care about how you get from one state to another, you can also name your transitions and view them as a set of generators of some SMC. Now instead of points in a $|P|$-dimensional lattice, each dimension is a generating object of the corresponding SMC and each transition a generating morphism. Instead of a sequence of points, a run is now a morphism of the free SMC on these generators. From the point of view of reachability, this is the same. But now you're keeping track of much more information in each run, namely how (with what combination of transitions) you transformed some resources (the objects of the category) into others, modulo the laws of SMCs which factor out irrelevant ordering of transitions that can be fired concurrently (this is the interchange law Fabrizio was talking about).

Petri nets with boundaries are Petri nets with potentially open transitions, which require synchronising with their environment to be fired. In some sense, they are orthogonal to the the Petri-net-as-SMC perspective. Together they form an SMC (this is different form how each standard Petri net can generate an SMC) and their semantics in all previous work I know of has been given in terms of sets and (so called additive) relations. But that's just an extension of the first perspective on Petri nets that I sketched above, to account for open transitions. If we wanted to keep track more precisely of how one gets from one state to another in Petri-net-as-SMC style we would need another dimension and your double-categorical framework seems like a natural candidate.

When I first learnt about Petri nets-as-SMC, I knew about Petri nets with boundaries and wondered what sort of mathematical object these would generate but no real answer. Seeing your work, I conjectured above that cornerings could be it. Maybe cornerings are overkill and a simpler double-categorical structure is sufficient but one should definitely have some sort of correspondence between the objects in the vertical (resource) and horizontal (boundary) dimensions.

Robin Piedeleu (May 12 2021 at 15:03):

Hmm... now that I think about this idea on some small examples, there is a mismatch between the two notions so maybe something else is needed.

Spencer Breiner (May 12 2021 at 16:07):

I'd like to hear more about gluing along transitions.

• Do they need to have the same input/output interface to allow gluing?
• Can the resulting nets be described by colimits of generating data?

I assume that the reachability issues are analogous to the recent discussion on emergence.

• Is there an easy example to show how this approach ameliorates the problem?
• Can we construe this condition terms of fullness of the maps from the shared overlap into each component net (full on the poset reflection, if we only care about reachability)?

Jade Master (May 12 2021 at 16:37):

@Chad Nester If you want to impose extra equations, of a more ad-hoc sort, on the free smc generated by a Petri net then I think the best way to do that is with semantics. I.e. you can impose equations by taking a symmetric monoidal functor into a category C where the equations you want to hold do hold.

John Baez (May 12 2021 at 18:18):

Fabrizio Genovese said:

Chad Nester said:

A related question, open to anyone reading this: I'm under the impression that people don't usually impose equations on the monoidal signature associated with a Petri net. From the resource theory view of monoidal signatures this is extremely natural, which seems like an advantage. Am I wrong?

Actually we do, depending on how you want to obtain categories from nets. In the paper John Baez , me, Jade Master and Mike Shulman published recently, we show how if, say, you want to generate a symmetric monoidal category from a Petri net, you need to impose some equations.

I'm not quite sure what that means, so I'll try to say it more carefully. A Petri net generates a free commutative monoidal category. This has extra equations as compared with a free symmetric strict monoidal category, since "commutative" says that all the symmetries, aka braidings, are identities:

$B_{x,y} = \mathrm{id}_{x,y}$

But those are the only extra equations we need to impose, to get the free commutative monoidal category from the free symmetric strict monoidal category.

John Baez (May 12 2021 at 18:19):

Chad wrote:

I'm under the impression that people don't usually impose equations on the monoidal signature associated with a Petri net. From the resource theory view of monoidal signatures this is extremely natural, which seems like an advantage. Am I wrong?

John Baez (May 12 2021 at 18:21):

They often don't. If one wanted to, one should really prove my conjecture:

Conjecture. The category of commutative monoidal categories is monadic over Petri nets.

In other words, the adjunction between free commutative monoidal categories and Petri nets gives a monad on $\mathsf{Petri}$ whose Eilenberg-Moore category is equivalent to $\mathsf{ComMonCat}$.

John Baez (May 12 2021 at 18:23):

If we had this fact, we could describe arbitrary commutative monoidal categories in a "generators and relations" way, just like people do for groups: that is, describe an arbitrary one as an equalizer of free ones.

John Baez (May 12 2021 at 18:25):

If you don't like "commutative monoidal categories", the same issues show up for symmetric strict monoidal categories: in our paper we construct an adjunction between symmetric strict monoidal categories and a variant of Petri nets that we call $\Sigma$-nets.

John Baez (May 12 2021 at 18:25):

So again it would be nice to know if this adjunction is monadic, because that would instantly give us access to a lot of results about "generators and relations" descriptions of symmetric strict monoidal categories.

John Baez (May 12 2021 at 18:27):

I guess while I'm at it, I should advertise that @Brandon Coya and Franciscus Rebro and I came up with a nice monadic adjunction between PROPs and certain "signatures", which allows us to get generators and relations descriptions of PROPs. See:

• Props in network theory, Appendix B.

John Baez (May 12 2021 at 18:31):

In practice people have been describing PROPs using generators and relations since the Late Bronze Age. But our results justify this and - perhaps more importantly - give access to all sorts of nice results. For example, if you take a PROP and throw in some extra relations, you get a new PROP and an epimorphism from the original PROP to this new one. Or, if you thrown in some new generators, you get a new PROP and a monomorphism from the original PROP to the new one.

John Baez (May 12 2021 at 18:35):

My conjecture would imply some similar results for Petri nets.

Chad Nester (May 20 2021 at 15:07):

Thanks Robin, Jade, and John. I've been sick, hence the delayed response.

Chad Nester (May 20 2021 at 15:10):

I do prefer the symmetric version of all of this over the commutative one. Still I see why your conjecture is interesting.

Chad Nester (May 20 2021 at 15:21):

... for the time being I personally will just keep working with arbitrary monoidal categories, often freely generated, but I'd be interested to hear about any developments.

Chad Nester (May 03 2022 at 07:08):

So: it turns out that the category of optics in a monoidal category is a full subcategory of the horizontal cells of the free cornering of that category (the free proarrow equipment constructed from it by adding corners).

Chad Nester (May 03 2022 at 07:08):

We've written a paper about this: https://categorytheory.zulipchat.com/#narrow/stream/258900-practice.3A-our-papers/topic/Cornering.20Optics/near/280974423