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: bisimulation

Fabrizio Genovese (May 27 2020 at 11:51):

Bisimulation is a fundamental concept in concurrency and I've always felt I didn't understand it as deeply as I should have. This topic is about:

• Explaining the main ideas behind it
• Understanding why it is useful, and what applications it has
• Uderstanding how this translates in categorical terms
  Personally I'm in the Petri net crowd but I'm also interested in notions of bisimulation coming from other disciplines (e.g. FSMs, I guess). Bisimulation-aware peope, show yourselves! :heart:

Henry Story (May 27 2020 at 12:22):

I found this diagram on a quick search on Google from an asian paper (there are other similar ones). This helps
put the various pieces in context. Coalgebra-Algebra.png

Henry Story (May 27 2020 at 12:23):

I think the above is not so good. This one (I think) by D. Sangiorgi is better.
AlgebraColagebra.jpg. What these diagrams show is that bisimulation is as important to coalgebras as congruence to algebras. So that firmly nails the concept there.

Henry Story (May 27 2020 at 12:32):

In Bart Jacobs' recent book Introduction to Coalgebra - Towards a Mathematics of States and Observations there is only one reference to petri-nets right on the first page as an example of how category theory deals with dynamic systems. It's weird: there indeed seems to be some lack of communication between the Petri-net crowd and the coalgebra crowd. (perhaps a quick search on the two on google scholar will find something). I found an earlier introduction that is free on the web An Introduction to the Theory of Coalgebras by Dirk Pattinson that covers these areas too. Any work on coalgebras goes quite quickly into bisimulation.

Dan Doel (May 27 2020 at 12:56):

I only really know about it via type theory/coalgebra/programming, so I don't know if the answer to your questions is different in other domains. But it is basically the properly extensional notion of equality of coinductive values/processes. Two processes are equal if they will produce corresponding (non-well-founded) trees of observations, not merely when they have the same definition/internal mechanism (intensional equality).

I'm not sure what you're looking for with some of your questions, though. As a simple analogy (that goes quite far for the type theory case), it's like asking, "why is function extensionality useful?" One might say that's what it means to be considering functions rather than the specific algorithm that implements them. Functions are the same when all their points are the same, not merely when they are presented by β convertible algorithms (or something). In type theories that lack this principle, it can be quite frustrating to manually work with the desired extensional equality, because it doesn't work as nicely as equality.

Henry Story (May 27 2020 at 12:59):

Here is my beginners take on this. Given a Polynomial Functor $F$ an algebra is a morphism $f: F(A) \to A$. So if our functor is $F(X) = 1 + A \times X$ then we have an algebra for Lists of $A$. The coalgebra is a dual morphism $f: S \to F(S)$ this takes a state S to a structure that either describes the state or gives a function that allows one to move to the another state. (So that resembles objects in OO programming, which one can manipulate with getters and setters (the functor acts like an interface in Java) and where one can change state. An example would be a functor $F(X) = Z \times X^{Z}$, where the coalgebra would allow us to observe our balance but also give us a function to add money to our account. Given two such coalgebras one would want to know if they are in some sense the same, and bisimulation says that they are if one can get the same observation at two states, and all possible successor states, arrived at by using the same transformations on both sides. So one can have two Objects in OO implemented differently that look exactly the same to the outside world. Eg. one could have a bank account DB that contains the whole history of transactions and another that contains only the balance. If the interface to access that data only allows you to observe the balance and add or remove money, then you would not be able to tell the difference between both databases and so they are bisimilar.

Now one thing I have been wondering about is that coalgebras only allow one to move one state forward at a time. So it is a way of describing one machine. But it may be that it is problematic when describing the interaction of many machines. That is a problem that one finds in OO, namely that it is not easy to work with concurrency. So it may be that petri nets have something here additionally to offer which would explain why Martin Oderski coming from working on Java in the late 1990s, but with previous experience in Haskell, moved to petri-nets. (just speculating here)

Henry Story (May 27 2020 at 14:00):

Intuitively how does this relate to modal logic? I think that is quite simple. You have a coalgebra that describes a machine (the simplest one is an infinite stream, but that is not so interesting). A machine like a bank account, that can change state, can have properties such as the balance never going below 0. That is to say one would like to say, necessarily all future states are in the black. Or if you reach above 100 thousand savings you are from then on gold member (whatever happens next).
I mention modal logic because I think it is work in modal logic where the importance of bisimiarities were first discovered. Though I think it was bisimilarity was first discovered in non-well-founded sets

Rich Hilliard (May 27 2020 at 14:50):

@Henry Story I am reminded of Joe Goguen's "hidden algebra" line of work.
Perhaps worth revisiting :
https://cseweb.ucsd.edu/~goguen/projs/halg.html

Fabrizio Genovese (May 27 2020 at 15:08):

So, how is this related to, say, bisimulation of labelled transition systems? In the coalgebra definition it seems to me that bisimulation is formulated by saying that two different coalgebras are/aren't bisimilar, while in labelled transition systems the bisimulation is a relation over a particular LTS. I guess the bisimulation between different LTSs is obtained by first taking their coproduct, and then defining a bisimulation relation on it

Henry Story (May 27 2020 at 15:23):

A labelled transition system is a coalgebra on the functor $\mathscr{P}(S)^A$. Bisimulations between two coalgebras $S \to \mathscr{P}(S)^A$ is described by Jacobs on p118 of "Introduction to coalgebra". It's a relation on the subset $\mathscr{P}(S)^A \times \mathscr{P}(S)^A$. I don't have time now to re-write it here, though it would be a good exercise for me. You can find the details on Google Books here

Fabrizio Genovese (May 27 2020 at 15:34):

But then again, this is a bisimulation between two different systems, while in principle you could have a bisimulation relation over any LTS.

Dan Doel (May 27 2020 at 15:36):

Bisimulation is a relation on values/points of a coalgebra. If two values are bisimilar they are taken to the same value of the terminal coalgebra via the universal map.

Joshua Meyers (May 27 2020 at 15:46):

Here's the definition in Rutten's paper:

Given two $F$-coalgebras $(S,\alpha:S\rightarrow FS)$ and $(T,\beta:T\rightarrow FT)$, a bisimulation between them is a relation $R\subseteq S\times T$ such that there exists a function $\gamma: R\rightarrow FR$ making the natural maps $R\rightarrow S$, $R\rightarrow T$ coalgebra-homomorphisms.

Ralph Sarkis (May 27 2020 at 15:46):

You can also have a bisimulation between two different coalgebras. Two states $x$ and $y$ are bisimilar if there is a bisimulation between the LTS and itself containing $(x,y)$. Taking the largest bisimulation on the LTS makes this an if and only if.

Shameless plug here: I gave a lecture to introduce the theory behind coalgebras (and algebras) in very basic terms and I have notes here: https://ralphs16.github.io/src/CatLectures/Lect102019.pdf

Jules Hedges (May 27 2020 at 15:47):

Unhelpful non-answer: Bisimulation is one of those things that looks like it shouldn't be hard, but it won't click no matter how many times I read about it

Henry Story (May 27 2020 at 15:47):

Fabrizio Genovese said:

But then again, this is a bisimulation between two different systems, while in principle you could have a bisimulation relation over any LTS.

I just corrected what I wrote from $\mathscr{P}(S)^A \times \mathscr{P}(S)^B$ to $\mathscr{P}(S)^A \times \mathscr{P}(S)^A$

Joshua Meyers (May 27 2020 at 15:49):

I have a problem with this definition actually. I think that the function $\gamma$ should be part of the content of the bisimulation, not just something that must exist. So I would say rather that a bisimulation between $(S,\alpha:S\rightarrow FS)$ and $(T,\beta:T\rightarrow FT)$ is another $F$-coalgebra $(R,\gamma:R\rightarrow FR)$ equipped with jointly monic coalgebra-homomorphisms $(R,\gamma)\rightarrow (S,\alpha)$, $(R,\gamma)\rightarrow (T,\beta)$.

Joshua Meyers (May 27 2020 at 15:50):

In other words, a jointly monic span in the category of $F$-coalgebras.

Joshua Meyers (May 27 2020 at 15:50):

This is not to say I really understand what the point of bisimulations are. It would be nice to see a key theorem which arrives at them in some canonical way, uses them as a crucial assumption, etc.

Ralph Sarkis (May 27 2020 at 15:55):

From what I've studied, $R$ should really be a relation between $S$ and $T$, that is, a subset of $S\times T$ and the monic coalgebra-homomorphisms must then be the projections. Also, the coalgebra $\gamma$ is a witness of $R$ being a bisimulation, so I would not necessarily put it in the definition. In my opinion, a bisimulation is first and foremost a relation between states of two LTSs satisfying some properties. These properties are here stated in coalgebraic terms, but they have other characterizations.

Joshua Meyers (May 27 2020 at 15:56):

Perhaps it makes more semantic sense to not say that $\gamma$ is part of the definition, but it does make for a much simpler definition from a CT standpoint!

Joshua Meyers (May 27 2020 at 15:57):

Can we give an example of two different $\gamma\text{s}$ so we can see if there is a semantic difference?

Henry Story (May 27 2020 at 16:01):

I went to a security conference in Cambridge three year ago and someone presented a project with Facebook. FB had written an optimized PhP compiler, but they wanted to prove that it was bisimilar to the standard one. The project proved that. I can't work out which talk it was though.

Dan Doel (May 27 2020 at 16:05):

Wasn't that an answer to the 'key theorem' part?

Joshua Meyers (May 27 2020 at 16:09):

Not really, I was looking for something abstract that could be stated concisely and completely. That's pretty cool because it means to me that bisimulation is a concept that people care a lot about, but it isn't abstract enough to be called a "key theorem", and you can't state it concisely and completely because it involves many incompressible idiosyncrasies about PhP and the particular implementation of that compilier.

Dan Doel (May 27 2020 at 16:09):

The point of bisimilarity is that it is what people care about in many cases. The two internally different things are identical with respect to their (relevant) observable behavior. That is also one interpretation behind the 'universal map' statement above. If two values are bisimilar, they are mapped to equal values of the terminal coalgebra, which is the coalgebra consisting of 'all possible observation trees'.

Joshua Meyers (May 27 2020 at 16:13):

Are you saying that whenever a bisimulation exists between two coalgebras, they are identical w.r.t. (relevant) observable behavior? That can't be true because for every two coalgebras $S$ and $T$ the null bisimulation $\varnothing\subseteq S\times T$ exists between them. So what is your claim?

Ralph Sarkis (May 27 2020 at 16:23):

Joshua Meyers said:

Can we give an example of two different $\gamma\text{s}$ so we can see if there is a semantic difference?

Here's what I've got: Let $S$ be a set with more than one element, $\gamma = (x,y) \mapsto S \times \{x\} \cup \{y\} \times S$ and $\gamma = (x,y) \mapsto S\times S$ both make the following diagram commute.
image.png

Ralph Sarkis (May 27 2020 at 16:26):

Joshua Meyers said:

Are you saying that whenever a bisimulation exists between two coalgebras, they are identical w.r.t. (relevant) observable behavior? That can't be true because for every two coalgebras $S$ and $T$ the null bisimulation $\varnothing\subseteq S\times T$ exists between them. So what is your claim?

It is not the coalgebras that are identical (w.r.t. the observable behaviour) but the bisimilar states. The empty relation does not imply any state are bisimilar.

Gershom (May 27 2020 at 16:35):

I've found a lot of good material for understanding why one might care about different notions of bisimilarity is in the paper "bisimulation can't be traced": http://www.lix.polytechnique.fr/~catuscia/teaching/DEA/General/BloomIstrailMeyer.pdf

I also agree with Dan that it is better to first understand why people care about bisimilarity by using concrete examples and then later understand "oh, this stuff is captured very neatly by examining coalgebras" rather than start with the general categorical setup first.

Dan Doel (May 27 2020 at 16:41):

The point is that the terminal coalgebra contains exactly the things we care about, by definition. So, if two states are mapped to the same value of the terminal coalgebra, they are interchangeable from this perspective. There may be reasons for choosing one coalgebra/state over another that is abstracted over by only considering the coalgebra structure, but the point is to know that they are 'the same' with respect to the coalgebra structure.

This is similar to only caring about the points/graph of a function, and using extensional equality of functions. There may be many ways to implement a function on a computer (say), with different reasons for choosing one over another, but when we consider the specific abstraction of functions, we are only concerned with the mapping between inputs and outputs. You could do a similar thing where you consider 'functional coalgebras', and the exponential would be the terminal coalgebra (although the presentation as a coalgebra is kind of trivial).

Henry Story (May 27 2020 at 16:44):

(I should not be hanging out here, but it's really too fun!)
I wish I could find that project with FB documented somewhere, as that really made me go Wow! It may have been during a conversation that that came up, when I asked how CT was used. I'll keep looking...
For OO programmers these articles by Bart Jacobs are really helpful, essentially explaining how to think of interfaces in Java

• Objects and Classes, Co-Algebraically
• Coalgebraic Reasoning about Classes in OO Languages

Christian Williams (May 27 2020 at 18:37):

Joshua Meyers said:

Are you saying that whenever a bisimulation exists between two coalgebras, they are identical w.r.t. (relevant) observable behavior? That can't be true because for every two coalgebras $S$ and $T$ the null bisimulation $\varnothing\subseteq S\times T$ exists between them. So what is your claim?

A bisimulation is a relation in a category of coalgebras. Then they define bisimilarity to be the colimit of all such bisimulations. https://en.wikipedia.org/wiki/Bisimulation

Then if two things are bisimilar, they have the same observable behavior. I picture them as agents which make actions to change state, and bisimilarity means that they can "match each other's moves".

Joshua Meyers (May 27 2020 at 18:43):

So from that wikipedia page, seems like bisimulation is between systems and bisimilarity is between states in a single system. Are you thinking of systems or states as agents?

Christian Williams (May 27 2020 at 18:55):

Good question. I think it's mainly a matter of perspective. More literally I think about an element of a labelled transition system as a program, and the edges are computation steps.

Now there's two main kinds of LTS: in the simple one, the edges are just reductions -- steps that the program could take by itself. But there is one which is more expressive, in which you also include edges for "if the program were put into this context, then it could take this step".

Christian Williams (May 27 2020 at 18:56):

The latter is important for concurrency, because we also want to record potential for interaction -- on which channels can this program communicate? This introduces a more refined kind of bisimulation called "barbed bisimulation".

Joshua Meyers (May 27 2020 at 20:04):

What's a good interpretation of the coalgebra $(R,\gamma)$? What is a good way of thinking of $FR$? It seems like people here are really thinking about transition systems of some sort, rather than coalgebras in general, is that true? Is there a way that every coalgebra is in some sense a transition system?

Henry Story (May 27 2020 at 20:05):

Yes. That is the idea.

Joshua Meyers (May 27 2020 at 20:11):

Can you elaborate? If I hand you an arbitrary set functor $F$, how are $F$-coalgebras transition systems?

Henry Story (May 27 2020 at 20:15):

You can think of the full memory layout in a computer or virtual machine as the state of the machine. The a procedural program changes that state from one instruction to the next. But you can transform the same coalgebra into a monad, and you then get the functional view on programming. Coalgebras and monads in the semantics of Java.

Christian Williams (May 27 2020 at 20:18):

Transition systems are coalgebras of $\mathscr{P}(A\times -):\mathrm{Set\to Set}$ for a set of labels $A$. The insight that these are coalgebras of an endofunctor leads to huge generalization -- we can think about any endofunctor on any category. It seems like people like to think of them as transition systems, but in reality they could be all sorts of structures.

Henry Story (May 27 2020 at 20:19):

$t: S \to F(S)$ is the coalgebra (S, F), with state $S$ and Functor $F$. It's a function that gives you something with another $S$ from which you can call the function t again. If you don't have a S in your result but some type A, then that is your observable. If you have a function that returns an $S$ then that can be used to choose the next transition by the one running the program.

Henry Story (May 27 2020 at 20:23):

But yes, it does not have to be states. There is work on thinking of real numbers coalgebraically. That allows you to think of infinite sequences as being produced. @dusko wrote this article On coalgebras of real numbers

Joshua Meyers (May 27 2020 at 20:28):

If $F$ has an equational presentation (cf) then I can kind of see how an $F$-coalgebra could be thought of as a transition system, maybe someone can make this more precise?

Joshua Meyers (May 27 2020 at 20:32):

OK, if $F$ has an equational presentation $(\Sigma, E)$, then we could consider each $\sigma\in \Sigma$ as a transition action which regards $\text{ar}(\sigma)$ multiple states in different roles. Equations $E$ would represent equivalences of actions.

Joshua Meyers (May 27 2020 at 20:35):

If someone wants I can explain what I mean by "equational presentation".

Henry Story (May 27 2020 at 20:39):

I think you have to remember this diagram. AlgebraColagebra.jpg. What identity is to algebras so bisimilarity is to coalgebras.

Henry Story (May 27 2020 at 20:44):

but I should probably leave this for people with more experience with CT to explain this...

Joshua Meyers (May 27 2020 at 20:49):

I should probably elaborate more. But I do want to acknowledge that people on this forum are coming from lots of different disciplines so communicating will take some trial and error, and asking and giving clarification is very important because it is hard to know what concepts and vocabulary is okay to assume.

Joshua Meyers (May 27 2020 at 20:51):

So let $\Sigma$ be a signature, that is, a set of operators, each equipped with an arity. We define a functor $H_\Sigma$ which sends a set $S$ to the set $\{\sigma(x_1,\ldots x_n) | \sigma\in\Sigma, \text{ar}(\sigma)=n\}$. This is called a polynomial functor with signature $\Sigma$.

Joshua Meyers (May 27 2020 at 20:52):

(The notation $\sigma(x_1,\ldots, x_n)$ is purely formal, by which I mean that it is a string, not something which can be evaluated.)

Henry Story (May 27 2020 at 20:52):

What is your background? I was tricked into writing up some of my background here which in short is philosophy, computing, and the semantic web. ;-)

Joshua Meyers (May 27 2020 at 20:52):

Math mainly

Henry Story (May 27 2020 at 20:54):

I have been discovering that Maths is a huge field. :upside_down:

Joshua Meyers (May 27 2020 at 20:54):

Also some chemistry and physics, coding but not much theoretical CS, and philosophy through discussion but not much reading

John Baez (May 27 2020 at 20:54):

What you said makes perfect sense to me so far, Joshua. A polynomial functor given by a signature - yup!

John Baez (May 27 2020 at 20:55):

Never suspected bisimulation was connected to those.

Joshua Meyers (May 27 2020 at 20:56):

Yeah the math I am familiar with is roughly equal to the proof-based math in the undergraduate curriculum for pure math majors

Joshua Meyers (May 27 2020 at 20:57):

Oh I was talking several steps away from bisimulation atm. I was just trying to think about how to interpret a large class of coalgebras as transition systems, because everyone seems to think in terms of transition systems when thinking about coalgebras and bisimulation.

John Baez (May 27 2020 at 20:58):

Okay. I don't understand any of this stuff (except the general idea of coalgebras of functors).

John Baez (May 27 2020 at 20:59):

But I think we're stopping you from saying what you're trying to say!

Joshua Meyers (May 27 2020 at 21:00):

So to continue, let $E$ be a bunch of formal equations $\sigma(x_1,\ldots,x_m)=\tau(y_1,\ldots,y_n)$ where $x_1,\ldots,x_m, y_1,\ldots,y_n\in X$ for some set $X$ and $\text{ar}(\sigma)=m$, $\text{ar}(\tau)=n$.

Henry Story (May 27 2020 at 21:00):

I came to coalgebras looking for modern views on modal logics, and found @Alexander Kurz 's Modal Logics are coalgebraic also written by my supervisor Corina Cirstea. So that led me to wonder what mathematicians understood by algebras, and found your explanation in terms of signatures is the standard one @Joshua Meyers . CT simplifies/unifies that by thinking in terms of polynomial functors, as I understand.

Joshua Meyers (May 27 2020 at 21:02):

We can now define a functor $F$ by saying that the natural transformation $H_\Sigma\Rightarrow F$ is universal w.r.t sending things that $E$ equates to the same thing.

Joshua Meyers (May 27 2020 at 21:04):

then $(\Sigma, E)$ is an equational presentation of $F$.

John Baez (May 27 2020 at 21:04):

Can I try to rephrase this so I understand it? Or do you want to march on?

Joshua Meyers (May 27 2020 at 21:04):

I think that every accessible functor has an equational presentation.

Joshua Meyers (May 27 2020 at 21:04):

Sure

John Baez (May 27 2020 at 21:06):

So I'm guessing maybe $\Sigma$ is a functor $\Sigma : \mathsf{S} \to \mathsf{Set}$ where $\mathsf{S}$ is the groupoid of finite sets and bijections, or if you prefer a skeleton thereof.

John Baez (May 27 2020 at 21:07):

That is for each finite set of "variables" $\Sigma$ gives a set of "operations".

John Baez (May 27 2020 at 21:08):

Or if you prefer, for each natural number "arity" $\Sigma$ gives a set of operations - here I'm using a skeleton, to work with natural numbers instead of "finite sets of variables"

Joshua Meyers (May 27 2020 at 21:09):

Sure, but let's use a different symbol because your $\Sigma$ is my $\text{ar}^{-1}$

John Baez (May 27 2020 at 21:09):

But the main thing I'm checking is that the permutation groups $S_n$ acts on the set of n-ary operations.

John Baez (May 27 2020 at 21:09):

Well, you said the "signature" was $\Sigma$, and I'm saying what I think a signature is.

John Baez (May 27 2020 at 21:09):

It's a set of operations for each arity.

John Baez (May 27 2020 at 21:10):

I'll let you use your notation as you see fit; I'm just trying to say how I think about what you're saying.

Joshua Meyers (May 27 2020 at 21:10):

Sure it's equivalent. I'm thinking of a signature as a set $\Sigma$ with a function $\text{ar}:\Sigma\rightarrow \text{Card}$

Joshua Meyers (May 27 2020 at 21:10):

OK sorry go on

John Baez (May 27 2020 at 21:11):

Well, my way of thinking gives a permutation action, but you could say no, you don't want the ability to permute variables in operations.

John Baez (May 27 2020 at 21:12):

Anyway, $\Sigma$ gives a functor $H_\Sigma : \mathsf{Set} \to \mathsf{Set}$.

John Baez (May 27 2020 at 21:12):

And this is

$H_\Sigma(X) = \sum_{n \ge 0} \Sigma(n) \times_{S_n} X^n$

John Baez (May 27 2020 at 21:13):

Note $S_n$ acts on both $\Sigma(n)$ and on $X^n$, so we're modding out by that action here. Another notation is

John Baez (May 27 2020 at 21:14):

$\displaystyle{ H_\Sigma(X) = \sum_{n \ge 0} \frac{ \Sigma(n) \times X^n}{S_n}}$

John Baez (May 27 2020 at 21:15):

Either way, what I'm doing is letting $n$ range over natural numbers, i.e. my favorite finite sets, and the sum is a coproduct, i.e. disjoint union.

John Baez (May 27 2020 at 21:15):

And this formula, esp. the second version, looks a whole lot like a Taylor series.

John Baez (May 27 2020 at 21:15):

The $S_n$ is like the $n!$ you see in a Taylor series.

John Baez (May 27 2020 at 21:16):

Okay, now you're gonna get another functor by imposing equations.

John Baez (May 27 2020 at 21:17):

Hmm, you're imposing equations that depend on what $X$ is?

Joshua Meyers (May 27 2020 at 21:18):

Yeah.

John Baez (May 27 2020 at 21:18):

Actually I'm completely confused now because your concept of "equation" seems to involve choosing a specific set $X$, but in the end you're getting a functor $F$.

Joshua Meyers (May 27 2020 at 21:19):

Oh

Joshua Meyers (May 27 2020 at 21:19):

I just meant that each equation must be drawn from a single $X$

John Baez (May 27 2020 at 21:20):

How are you going to wrangle all these choices of $X$'s into a functor $F: \mathsf{Set} \to \mathsf{Set}$?

Joshua Meyers (May 27 2020 at 21:20):

But $E$ can totally contain equations from different $X\text{s}$, you just can't equate things in different $X\text{s}$

Joshua Meyers (May 27 2020 at 21:20):

So here's how we could construct $F$

John Baez (May 27 2020 at 21:21):

I don't get this at all, esp. since we're trying to make $F$ a functor in the end, so it shouldn't care about individual choices of $X$ at all, like {3,4} versus {1,7}.

John Baez (May 27 2020 at 21:22):

I was (and am) hoping that you'll get $F$ by starting with $H_\Sigma$ and doing a coequalizer in the category of functors from $\mathsf{Set}$ to $\mathsf{Set}$.

Nathanael Arkor (May 27 2020 at 21:23):

$H_\Sigma$ is the functor of operations, so presumably you'll take the free monad on $H_\Sigma$, to get the terms, and then take a coequaliser of that.

Joshua Meyers (May 27 2020 at 21:25):

[Note Let's bracket size issues.] So $E$ is a relation on $\coprod_{X\in\text{Set}} H_\Sigma X$. Let $\sim$ be the congruence generated by $E$, i.e. the smallest congruence containing $E$. By "congruence" I mean an equivalence relation which also satisfies the property that whenever $x,y\in H_\Sigma(X)$ with $x\sim y$ and $f:X\rightarrow Y$ is a morphism, $H_\Sigma f(x)\sim H_\Sigma f(y)$.

Joshua Meyers (May 27 2020 at 21:28):

Then let $FX=H_\Sigma X / \sim_X$ where $\sim_X=\sim \cap (H_\Sigma X)^2$.

John Baez (May 27 2020 at 21:32):

Zounds! I find this terrifying. I think there must be a way to rephrase it that I could tolerate better.

Joshua Meyers (May 27 2020 at 21:33):

Sorry let me try

Nathanael Arkor (May 27 2020 at 21:33):

This is the equational presentation of an algebraic theory, no? In which case you can simply pick your favourite definition.

John Baez (May 27 2020 at 21:33):

I was trying to determine what Joshua was doing.

John Baez (May 27 2020 at 21:34):

If he's doing an equational presentation of an algebraic theory, I know ways to do that that I like. But I'm having trouble being sure he's doing that.

Dan Doel (May 27 2020 at 21:34):

It seems like this is just trying to do the same thing as algebra, but this is coalgebra, so you should instead do the opposite thing.

Joshua Meyers (May 27 2020 at 21:35):

I'm doing an equational presentation of a set functor, not an algebraic theory. Unless it's equivalent somehow and I don't realize

John Baez (May 27 2020 at 21:36):

It could be quite different... you say in the end you're gonna get all accessible functors Set -> Set this way?

Joshua Meyers (May 27 2020 at 21:36):

Yeah

Joshua Meyers (May 27 2020 at 21:36):

How about I give some examples?

Henry Story (May 27 2020 at 21:37):

It may be easier if one starts before bringing in congruence, since coalgebras have a dual of it.
I think in algebras and coalgebras we are dealing with polynomial endofunctors $F$ of a category $\mathbb{C}$ if that helps. The functors can be divided into three inclusive groups, quoting Bart Jacobs:

• simple ploynomial functors: identity, constants, finite products, arbitrary coproduces
• exponent polynomial: additionally with $(-)^A$ with infinite A
• Kripke polynomials: Additionally the powerset $\mathscr{P}$ functor

Then an coalgebra is a choice in $\mathbb{C}$ of a $X \in \mathbb{C}$ together with a morphism $c: X \to F(X)$. $X$ is called the state space and $c$ the transition or coalgebra structure.

Dan Doel (May 27 2020 at 21:38):

Like, for algebra, you don't present a functor F by generators and equations and then do the F-algebra, you present a monad T that way, and F-algebras are algebras of the free monad (on F). But, coalgebras are related to comonads, and F-coalgebras are coalgebras of the cofree comonad (on F).

John Baez (May 27 2020 at 21:38):

Anyway, I have to do some work now, but my preferred method of proceeding would have been to rephrase what Joshua was doing in a way that didn't require a large coproduct. And this other way (if it exists) would with luck be something I find much easier to understand.

Joshua Meyers (May 27 2020 at 21:39):

Oh that was the problem

John Baez (May 27 2020 at 21:39):

No, that was just the usual sign that something terrible was happening.

Joshua Meyers (May 27 2020 at 21:39):

Lol

John Baez (May 27 2020 at 21:40):

I don't mind large things, but I've seen other cases where when you're tempted to use them it means you're doing something suboptimally.

John Baez (May 27 2020 at 21:40):

It seems in the end you're getting a functor $F$ as a "quotient" of the functor $H_\Sigma$.

John Baez (May 27 2020 at 21:41):

So that to me would suggest you're getting $F$ as a coequalizer in the category of functors from Set to Set.

Joshua Meyers (May 27 2020 at 21:41):

So the way to get around that is to say that a congruence on a functor $F$ is a family of equivalence relations $(\sim_X)_{X\in\text{Set}}$ such that whenever $x,y\in X$ and $x\sim_X y$ and $f:X\rightarrow Y$ is a morphism, $Ff(x)\sim_Y Ff(y)$.

John Baez (May 27 2020 at 21:43):

I can't think about that - it breaks my brain. I really think you must be taking a coequalizer as I'm suggesting.

Joshua Meyers (May 27 2020 at 21:43):

Congruences on $F$ are in 1-1 correspondence with "epitransformations", that is, natural transformations $F\Rightarrow G$ which are epi in each component.

Joshua Meyers (May 27 2020 at 21:43):

OK how does this coequalizer work?

John Baez (May 27 2020 at 21:43):

Oh, now you're starting to talk English!

John Baez (May 27 2020 at 21:44):

An "epitransformation" is just an epimorphism in the functor category I'm talking about: the category of functors from Set to Set.

John Baez (May 27 2020 at 21:45):

I feel sure you're just doing a coequalizer in this category - a coequalizers of two natural transformations from some $X$ to your $H_\Sigma$.

John Baez (May 27 2020 at 21:46):

If you did such a coequalizer (annoying to draw the diagram here), you'd wind up with an epimorphism

$H_\Sigma \Rightarrow F$

Joshua Meyers (May 27 2020 at 21:46):

Huh maybe I can make that work

John Baez (May 27 2020 at 21:47):

But okay, instead of doing a coequalizer you're "modding out by a congruence".

Joshua Meyers (May 27 2020 at 21:48):

Yeah

John Baez (May 27 2020 at 21:49):

I think the process of building up that congruence was freaking me out. Usually when you take a coequalizer diagram (where you just say what you want to be equal to what) and turn it into a congruence (a very nice sort of "equivalence relation") you have to do a lot of work.

Joshua Meyers (May 27 2020 at 21:49):

I don't see right now how to figure out what $X$ could be, seeing as $E$ is completely arbitrary

John Baez (May 27 2020 at 21:50):

Like I can take a group and just say "I want to make x equal to y, and z equal to w", and that's easy to do with a coequalizer.

John Baez (May 27 2020 at 21:50):

Or I can explicitly describe the smallest congruence with x ~ y and z ~ w, and that's a pain in the butt.

John Baez (May 27 2020 at 21:51):

Of course in the first approach all the work is buried in showing that the category of groups has coequalizers.

John Baez (May 27 2020 at 21:51):

X would depend on what E you want.

John Baez (May 27 2020 at 21:52):

Like if I have a group G and I want to mod out in a way that sets x equal y and z equal to w, I pick two homomorphisms

$\mathbb{Z}^2 \to G$

John Baez (May 27 2020 at 21:52):

one of which sends the two generators of $\mathbb{Z}^2$ to x and z, the other of which sends them to y and w.

John Baez (May 27 2020 at 21:53):

Yes. Then I do the coequalizer of these two homomorphisms.

Joshua Meyers (May 27 2020 at 21:53):

Right

Nathanael Arkor (May 27 2020 at 21:53):

Joshua Meyers said:

I'm doing an equational presentation of a set functor, not an algebraic theory. Unless it's equivalent somehow and I don't realize

Finitary polynomial functors correspond to non-equational presentations; and finitary monads correspond to equational presentations, as @Dan Doel points out. So I would have thought one of the two was close to equivalent to what you were doing.

John Baez (May 27 2020 at 21:54):

Anyway, I'll be happy, @Joshua Meyers, if you're talking about functors that can be built from polynomial functors by taking a coequalizer.

Joshua Meyers (May 27 2020 at 21:55):

So let's say $E$ equates two elements of $H_\Sigma A$ and two elements of $H_\Sigma B$ and that's it.

John Baez (May 27 2020 at 21:55):

Okay. But surely if you have a map $A \to A'$ you're gonna want to equate two elements of $H_\Sigma A'$ too, right?

Joshua Meyers (May 27 2020 at 21:56):

Seems like to follow your group analogy, $X$ would need to have two "free generators", one for $A$ and one for $B$, and nothing else. But I'm not sure how to build a functor like that.

Joshua Meyers (May 27 2020 at 21:56):

Right

John Baez (May 27 2020 at 21:57):

What freaks me out is that you're running around the world saying stuff like "let A = {dog, cat}, then let me equate two things in $H_\Sigma(A)$.... then let B = {7,9, pi}..."

John Baez (May 27 2020 at 21:57):

It's just so unsystematic! And then you're repairing this somehow.

John Baez (May 27 2020 at 21:58):

Category theorists try not to let themselves do such unfunctorial things.

Dan Doel (May 27 2020 at 21:58):

I don't really understand why we're going through all this effort to describe the functors, personally. :)

John Baez (May 27 2020 at 21:58):

I'm just trying to understand what Joshua is saying, that's all.

John Baez (May 27 2020 at 21:59):

I should probably get some work done, so I'll stop and let him carry on.

Joshua Meyers (May 27 2020 at 21:59):

Well that's the whole idea of "presenting the functor". You just say the minimal amount of equations necessary. You don't need to say anything about A'= {bird, wolf} because talking about A suffices

John Baez (May 27 2020 at 22:00):

Okay. You come from a different tradition, I guess. I'm happier saying what happens to all 2-element sets at once. For one thing, if I understand what you're doing, nothing can depend on who is the dog and who is the cat - not in the end, anyway.

Joshua Meyers (May 27 2020 at 22:01):

Right it doesn't matter in the end

John Baez (May 27 2020 at 22:03):

Okay, so to me it's a distracting "gambit" to describe things in a massively asymmetrical way and then restore the symmetry later. Sometimes you have to, but if you don't have to I'd rather not. It's just like describing some construction in linear algebra using a basis and then showing it didn't depend on the choice of a basis.

John Baez (May 27 2020 at 22:03):

Anyway, I will bow out now.... thanks, and sorry for the huge digression.

Joshua Meyers (May 27 2020 at 22:03):

I see

Joshua Meyers (May 27 2020 at 22:04):

Thanks for your patience with my strange exposition

Joshua Meyers (May 27 2020 at 22:04):

So anyway, a huge class of functors can be described this way

Joshua Meyers (May 27 2020 at 22:04):

I think it's possible to coalgebras of these functors as transition systems in some sense

Joshua Meyers (May 27 2020 at 22:08):

So, like... if $\Sigma=\{\alpha,\beta,\gamma\}$ with arities $0,1,2$ respectively, say, we could give some interpretations to these like, $\alpha()$ is the null transition, we don't go anywhere, $\beta(x)$ goes to state $x$, and $\gamma(x,y)$ asks the user for their favorite color and goes to $x$ if it's red and $y$ otherwise

Joshua Meyers (May 27 2020 at 22:08):

and then we might want to impose some relations like $\beta(x)=\gamma(x,x)$ because the latter throws out the info about the user's birthday anyway so we might as well not even ask

Joshua Meyers (May 27 2020 at 22:09):

So then a coalgebra $S\rightarrow FS$ would be an assignment of a transition to each state.

Joshua Meyers (May 27 2020 at 22:09):

And I think you could do something like this for any equationally presented functor

Joshua Meyers (May 27 2020 at 22:10):

Also sorry I've been ignoring everyone else let me try to respond

Henry Story (May 27 2020 at 22:11):

yes, but I think you need to take into account that coalgebras are duals of algebras. As I understand you get your equational theories in algebras using monads. And with coalgebras it is using co-monads. So everything is really upside down in this weird way that things are in CT for duals (eg addition is upside down multiplication, who would have thought!) Especially equational thinking has a dual. So if you bring equational thinking too early everything will seem weird.

Joshua Meyers (May 27 2020 at 22:13):

Hm I haven't really studied algebra, only coalgebra. The stuff I'm talking about is simply about set functors, but they came up in a coalgebra paper I was reading.

Henry Story (May 27 2020 at 22:14):

which paper?

Joshua Meyers (May 27 2020 at 22:15):

https://www.semanticscholar.org/paper/Presentation-of-Set-Functors%3A-A-Coalgebraic-Ad%C3%A1mek-Gumm/0638f4cccc0fe20fe7868d8e2d84af2301863dcd

John Baez (May 27 2020 at 22:18):

Thanks, that paper answers some of my questions.

John Baez (May 27 2020 at 22:20):

First, they are not looking at permutation group actions (the way you do in the theory of "species"); their polynomial functors are just

$H_\Sigma(X) = \sum_n \Sigma(n) \times X^n$

and furthermore $n$ ranges over all cardinals, so there's no finiteness constraint on the "arities".

Joshua Meyers (May 27 2020 at 22:21):

Yes. Sorry, I should have linked to it more obviously sooner, would have cleared up a lot of confusion

John Baez (May 27 2020 at 22:22):

Then they're looking at all functors $F$ for which there's an epimorphism $H_\Sigma \Rightarrow F$.

John Baez (May 27 2020 at 22:23):

I would normally only say that a gadget $F$ is a "quotient" of a gadget $H_\Sigma$ when there was a regular epi from $H_\Sigma$ to $F$ (the kind of epi you get from a coequalizer), but in the category we're working in here, namely $\mathsf{Set}^\mathsf{Set}$, all epis are regular.

John Baez (May 27 2020 at 22:24):

So as soon as we've got an epimorphism (what you called an "epitransformation") $H_\Sigma \Rightarrow F$ we know it comes from some coequalizer.

Joshua Meyers (May 27 2020 at 22:24):

Oh wow, how can we prove that?

John Baez (May 27 2020 at 22:25):

My proof would be pretty indirect: in any presheaf category all epis are regular.

Joshua Meyers (May 27 2020 at 22:25):

Also I am not convinced right now that an epimorphism of functors must be epi in each component

John Baez (May 27 2020 at 22:25):

Umm, hmm, interesting.

John Baez (May 27 2020 at 22:25):

I think so, actually.

John Baez (May 27 2020 at 22:27):

I think the relevant buzzwords are "in a presheaf category colimits are computed pointwise, and epis can be defined using pushouts, so whether something is an epi can be determined pointwise."

Joshua Meyers (May 27 2020 at 22:28):

Hm I'll think about it

John Baez (May 27 2020 at 22:29):

Sorry to be so jargonesque, there's probably a more direct proof but this stuff is individually good to know.

John Baez (May 27 2020 at 22:30):

Anyway, one big theorem that this paper proves about this stuff is: every accessible functor Set -> Set can be described as a "quotient" (in the sense we're talking about) of a polynomial functor Set -> Set.

Joshua Meyers (May 27 2020 at 22:31):

Yes. It also assumes soundness but that is not necessary.

John Baez (May 27 2020 at 22:31):

I don't have much intuition for accessible functors, so I'm wondering if this is an "iff" - whether every quotient of a polynomial functor is accessible.

John Baez (May 27 2020 at 22:31):

Maybe this is much easier!

John Baez (May 27 2020 at 22:31):

I have no idea.

Joshua Meyers (May 27 2020 at 22:32):

Yes it is iff

John Baez (May 27 2020 at 22:33):

Nice! So this is one way for me to start understanding accessible functors.

Joshua Meyers (May 27 2020 at 22:42):

In section 3.1, the "Accessible Set Functors" section, I see why conditions (3.1) and (3.2) are equivalent to each other, but not why they are equivalent to the given definition of accessible functor. The references don't actually show this either. That's something I'd like to understand. But it probably doesn't belong in this topic.

Dan Doel (May 27 2020 at 23:20):

Incidentally, I at least don't really think about these as labelled transition systems. I think about coalgebras as ways to define the non-well-founded trees (values of the terminal coalgebra). Probably you can couch everything in terms of a LTS, but it might not be the most obvious motivation for thinking about the trees in every case.

Dan Doel (May 27 2020 at 23:24):

For instance, the extended natural numbers are the final coalgebra of $1 + -$.

Dan Doel (May 27 2020 at 23:26):

And importantly, they have the right sort of 'computability topology' that other definitions you might think of don't (and you'd need to work harder to correctly define it in other ways).

Dan Doel (May 27 2020 at 23:29):

That's a pretty boring LTS, though, because it's just something that beeps possibly forever, I think.

Kyle Raftogianis (May 28 2020 at 00:13):

I'm not sure that coalgebras have the right "computability topology" to be honest. If $n$ is an extended natural number, it's decidable whether $n \geq k$ for any finite $k$. But if you watch a program that beeps possibly forever, to be sure whether there's a kth beep or not you might have to wait forever, which suggests it shouldn't be decidable whether there's a kth beep.

The thing I've been playing with instead is: there's a set $\mathsf{Beep}$ and an injection $\mathsf{index} : \mathsf{Beep} \to \mathbb{N}$ (the unique index of a beep) such that if there exists a beep with index $n + 1$, there exists a beep of index $n$ too. This is the same thing as a functor $\mathbb{N}^{\mathsf{op}} \to \mathsf{Prop}$ where $\mathsf{Prop}$ is the category of truth values (and this definition inspired by this nlab definition of a tree/forest). Now you can't decide whether or not there's an kth beep, so I think this matches my intuition about streams in programming better (and it's not uncategorical either).

Dan Doel (May 28 2020 at 00:21):

It is the right computability for the extended natural numbers. Like I said, I think about the trees. If you want to model some other idea with the trees, you have to choose the right type of trees.

Kyle Raftogianis (May 28 2020 at 00:23):

Sure. But maybe not for a program that beeps possibly forever (or programs that takes streams as input and produce streams as output) which is often what coalgebras are used for

Dan Doel (May 28 2020 at 00:26):

Okay, but then it seems like you're also complaining that a labelled transition system with one possible label also doesn't model this, because it doesn't account for some additional aspect that is not included in just the labels that will be observed.

Kyle Raftogianis (May 28 2020 at 00:28):

I don't really know what a labelled transition system is, but maybe. I'm not trying to pick a fight, I'm just trying to get a better understanding of what a stream is for computers

Kyle Raftogianis (May 28 2020 at 00:29):

Maybe the extended nats models a "pull-based" stream, whereas the $\mathsf{index}$ thing models a "push-based" stream?

Gershom (May 28 2020 at 06:01):

What you seem to be describing is the fact that coinductive types ("M-types") can be built out of inductive types ("W-types") in a variety of cases, in the presence of a natural number object. This is not more expressive than direct coalgebraic methods -- in some settings it is about the same, and in some settings it is less expressive. C.f. https://arxiv.org/abs/math/0409158 and https://hott.github.io/M-types/

Henry Story (May 28 2020 at 10:44):

please record it! :pray:

Kyle Raftogianis (May 28 2020 at 15:53):

@Gershom yeah good point. If you build the extended nats this way, I think you get something like infinite binary sequences $\mathbb{N} \to 2$ that are increasing, or equivalently downward-closed decidable subsets of $\mathbb{N}$ (from the sequence description, the subset where the sequence is 0). But I want to consider all downward-closed subsets of the naturals, not just decidable ones. (This distinction only makes sense in constructive logic, which I totally forgot to mention I'm working in here...sorry). Is there a way to encode that as a coalgebra?

Todd Schmid (he/they) (May 29 2020 at 14:03):

Dammit, there was a > 200 message convo about coalgebra and I missed it? I need to check Zulip more often...

Todd Schmid (he/they) (May 29 2020 at 16:33):

Fabrizio Genovese said:

Bisimulation is a fundamental concept in concurrency and I've always felt I didn't understand it as deeply as I should have. This topic is about:

• Explaining the main ideas behind it
• Understanding why it is useful, and what applications it has
• Uderstanding how this translates in categorical terms
  Personally I'm in the Petri net crowd but I'm also interested in notions of bisimulation coming from other disciplines (e.g. FSMs, I guess). Bisimulation-aware peope, show yourselves! <3

Was this question answered? It's hard to tell from reading the ensuing conversation as a third party.

Valeria de Paiva (May 29 2020 at 16:55):

Todd Schmid said:

Fabrizio Genovese said:

Bisimulation is a fundamental concept in concurrency and I've always felt I didn't understand it as deeply as I should have. This topic is about:

• Explaining the main ideas behind it
• Understanding why it is useful, and what applications it has
• Uderstanding how this translates in categorical terms
  Personally I'm in the Petri net crowd but I'm also interested in notions of bisimulation coming from other disciplines (e.g. FSMs, I guess). Bisimulation-aware peope, show yourselves! <3

Was this question answered? It's hard to tell from reading the ensuing conversation as a third party.

hmm, I have not followed the conversation and maybe someone already mentioned that bisimulation was independently "invented" by both Robin Milner for concurrency in CCS and by Johan van Benthem to relate Kripke models of modal logic. I find it one of nice new coincidences of our area of work!

Jules Hedges (May 29 2020 at 16:59):

Dan Doel said:

Bisimulation is a relation on values/points of a coalgebra. If two values are bisimilar they are taken to the same value of the terminal coalgebra via the universal map.

This is a neat answer, and might even stick in my head

Dan Doel (May 29 2020 at 17:12):

Good. :slight_smile:

Dan Doel (May 29 2020 at 17:18):

Theoretically that is just dualizing things from algebra, but the dual things kind of end up playing different roles in each.

Dan Doel (May 29 2020 at 17:35):

Like, the terminal/cofree coalgebra is 'all the relevant things that can be observed,' and usually the reason for studying things this way is that you only care about distinguishing two things if they can yield different observations. But initial/free algebras are 'all the relevant ways you can build things'. So, there is a dual relation of 'these two values of algebras were built the same way.' That kind of gives you an intensional notion of equality (these two things were built the same way, so they must be equal in some sense).

But in an algebra, there may be values that aren't constructed purely out of algebraic operations, and this intensional equality has nothing to say about those (I think). Also, people generally want to consider things equal if they 'behave the same,' not merely if 'they were built exactly the same way.' So, 'the image in the terminal coalgebra is the same,' is the thing they actually care about in some sense.

Ralph Sarkis (May 29 2020 at 17:49):

Dan Doel said:

But in an algebra, there may be values that aren't constructed purely out of algebraic operations, and this intensional equality has nothing to say about those (I think).

I was wondering what this means for arguments by induction when thinking of $\mathbb{N}$ as the initial algebra of $\mathbf{1}+\cdot$. I recently learned that $\mathbb{N}$ is not really a set and we should really use $\omega$ (the ordinal) which might contain transfinite numbers finite limit ordinals, but I don't see any logic dealing with limit cases when arguing by induction with initiality of $[0, \textsf{succ}]: \mathbf{1}+\omega \rightarrow \omega$.

Dan Doel (May 29 2020 at 18:17):

Well, I do type theory, not set theory, so I'm not really sure what details you're talking about. But $ω$ is an initial algebra of $1 + -$ in that way exactly because it doesn't contain any transfinite ordinals, just all and only the finite ordinals.

Dan Doel (May 29 2020 at 18:19):

Are you thinking of $\aleph_0$, which is defined as some kind of isomorphism class of countable sets or something?

Ralph Sarkis (May 29 2020 at 18:36):

I meant finite limit ordinal instead of transfinite numbers (I'll edit my previous message). I am trying to find a reference to the statement that $\omega$ might (I remember that it is independent of ZF) contain finite limit ordinals (finite is defined as contained in $\omega$, so might be redundant here), but for now, Wikipedia says:

there is a smallest infinite limit ordinal; denoted by ω (omega).

Cody Roux (May 29 2020 at 18:39):

Constructively, it's possible to have an ordinal less than $\omega$ which is neither a successor nor a weak limit... but classically, no.

Ralph Sarkis (May 29 2020 at 18:41):

What is a weak limit ?

Cody Roux (May 29 2020 at 18:45):

In J. Lipton "Realizability in Set Theory", it's defined to be an ordinal $\alpha$ such that $\forall \beta\in\alpha, \exists \gamma\in\alpha, \beta\in\gamma$. I think it's to contrast the "classical" definition, which is simply "not a successor ordinal".

Nikolaj Kuntner (May 29 2020 at 18:51):

"Constructively, it's possible" here means "when you drop standard non-constructive axioms, then it's consistent"?

Dan Doel (May 29 2020 at 19:03):

You could define a totally ordered sub-finite set that is not provably equal to a successor ordinal, but also not a limit in that sense.

Dan Doel (May 29 2020 at 19:12):

Anyhow, I think worrying about ordinals is probably unnecessary. It should be possible to construct the initial algebra $ℕ$ as a set, and it doesn't matter if it happens to be the same set as the ordinal $ω$ or not.

Ralph Sarkis (May 29 2020 at 19:13):

Yeah... Thanks for this digression anyway !

EDIT (the day after this discussion): I just want to come back here and clear things up in my head without disturbing the discussion.

FIrst, a (categorical) proof that $\omega$ has no limit ordinals: Since $[0, \textsf{succ}]:\mathbf{1}+\omega \rightarrow \omega$ is an initial algebra, Lambek's lemma tells us that it is an isomorphism. In particular, it is surjective, thus every element in $\omega$ is either $0$ or $\textsf{succ}(x)$ for $x \in \omega$.

Second, what is still not clear in my head: I messed up with terminology twice, but I was right in saying that there are elements in $\omega$ which are not natural numbers (which are defined as finite successors of $0$. There are models of ZFC where $\omega$ contains non-standard natural numbers, which are not limit ordinals, but they are not (finite) successors of $0$. Now, this means that standard induction is not enough in $\omega$ and we should really use transfinite induction (right?), but I don't see how induction arguments with initiality of $\omega$ can do transfinite induction.

Fabrizio Genovese (May 29 2020 at 20:02):

Todd Schmid said:

Fabrizio Genovese said:

Bisimulation is a fundamental concept in concurrency and I've always felt I didn't understand it as deeply as I should have. This topic is about:

• Explaining the main ideas behind it
• Understanding why it is useful, and what applications it has
• Uderstanding how this translates in categorical terms
  Personally I'm in the Petri net crowd but I'm also interested in notions of bisimulation coming from other disciplines (e.g. FSMs, I guess). Bisimulation-aware peope, show yourselves! :heart:

Was this question answered? It's hard to tell from reading the ensuing conversation as a third party.

Well, I got a lot of "formal" answers, especially using coalgebra. I guess I can follow the mathematics, but I still feel the main idea behind simulation is eluding me. I've seen it presented game-theoretically, something like "you can match your opponent moves and vice-versa", and that seemed to make sense conceptually. But no, I still can't say that I really understand bisimulation or that I would feel confident in using it in my research work

Fabrizio Genovese (May 29 2020 at 20:03):

Obviously the fault for not understanding is basically mine, if that wasn't clear from the previous message :slight_smile:

Henry Story (May 29 2020 at 20:21):

The simplest and famous example is the coffee machines example. You are given two differently implemented coffee machines, with the same buttons, coins slots, but built differently giving you the same coffee. Can you tell them apart just from observing their behavior? If not, they are bisimilar: As far as your interaction with the machine goes you make the same moves to get the coffee.

Cody Roux (May 29 2020 at 22:20):

This is a bit weaker than bisimulation though: this would typically be referred to as trace equivalence. Though it is weaker (or perhaps because it is weaker) it is harder to decide trace equivalence, but there are polynomial (even quasi-linear) algorithms for bisimilarity.

Fabrizio Genovese (May 30 2020 at 00:38):

Henry Story said:

The simplest and famous example is the coffee machines example. You are given two differently implemented coffee machines, with the same buttons, coins slots, but built differently giving you the same coffee. Can you tell them apart just from observing their behavior? If not, they are bisimilar: As far as your interaction with the machine goes you make the same moves to get the coffee.

So, this is something that actually clicks. But as @Cody Roux says this is not exactly bisimulation. Can we state the difference between bisimulation and trace equivalence in terms of coffee machines?

Fabrizio Genovese (May 30 2020 at 00:49):

@Henry Story I'm reading the notes you referenced. Thigs are starting to make sense :slight_smile:

Cody Roux (May 30 2020 at 01:23):

Right, there's a difference between "sequences of behaviors" and "sequences of interactions" if certain actions are "user actions" and others are "machine actions". In the second case, bisimulation can distinguish them.

Dan Doel (May 30 2020 at 03:18):

Does the distinction make sense without non-determinism? From the example I found, it seems difficult to interpret trace equivalence as the thing you'd want without the magic behavior of non-deterministic automata.

Like, one coffee machine lets you put in a coin, and then non-deterministically moves to one of two states, one of which allows you to press a button to get iced coffee, and the other which allows you to press a different button to get hot coffee. The other machine lets you put in a coin, then moves to a state where you can press either button to get the corresponding coffee.

These are trace equivalent, because the same paths exist for both machines (coin,iced and coin,hot), but not bisimilar, because the second button press is not controlling the choice in the first case. But this only works for a coffee machine if the machine somehow always chooses to enable the style of coffee you would have wanted anyway.

I think trace equivalence might be what you get automatically from a terminal coalgebra-like approach using $\mathcal P(Σ×-)$ (although the paper doesn't do that; I suppose because $\mathcal P$ would have size issues). But that isn't a very good way of thinking about equivalent use of a coffee machine.

Todd Schmid (he/they) (May 30 2020 at 12:52):

Fabrizio Genovese said:

Todd Schmid said:

Fabrizio Genovese said:

Bisimulation is a fundamental concept in concurrency and I've always felt I didn't understand it as deeply as I should have. This topic is about:

• Explaining the main ideas behind it
• Understanding why it is useful, and what applications it has
• Uderstanding how this translates in categorical terms
  Personally I'm in the Petri net crowd but I'm also interested in notions of bisimulation coming from other disciplines (e.g. FSMs, I guess). Bisimulation-aware peope, show yourselves! <3

Was this question answered? It's hard to tell from reading the ensuing conversation as a third party.

Well, I got a lot of "formal" answers, especially using coalgebra. I guess I can follow the mathematics, but I still feel the main idea behind simulation is eluding me. I've seen it presented game-theoretically, something like "you can match your opponent moves and vice-versa", and that seemed to make sense conceptually. But no, I still can't say that I really understand bisimulation or that I would feel confident in using it in my research work

Okay, so it's briefly mentioned far, far above, but I think it's important enough to restate what a bisimulation (in the general sense) _actually is._ A bisimulation of two systems X and Y (or machines, or coalgebras) is a third machine, say R, in which the processes present in X and Y can be simulated. Formally, by simulation I mean coalgebra homomorphism (and actually, for coalgebras in SET at least, a function is a coalgebra homomorphism iff its graph is a bisimulation).

Fabrizio Genovese (May 30 2020 at 13:33):

This is actually relevant, thanks

Fabrizio Genovese (May 30 2020 at 13:34):

This "third machine" is often left implicit in many definitions I saw. I just assumed they were actually taking a coproduct of two machines and define a bisimulation relation there

Fabrizio Genovese (May 30 2020 at 13:34):

Like when they say "two coffee machines are bisimilar"

Cody Roux (May 30 2020 at 14:44):

Yes, the "third machine" is similar to the minimal automaton in regular language theory, in that its states are equivalence classes of pairs of states.

Cody Roux (May 30 2020 at 14:47):

sorry, it's actually equivalence classes of the states of the disjoint union of the machines, I think.

Mike Stay (Jul 06 2020 at 17:32):

Milner defines barbed bisimilarity of P and Q in his "polyadic pi calculus tutorial" at the top of page 23. P ≡ Q if the following hold:

1. If P -> P', then there exists Q' such that Q -> Q' and P' ≡ Q'.
2. If P↓α then Q↓α.
   (Downarrow is a relation between processes and names that captures the idea that a context could interfere with a process on a name; see the paper for details. The names α are called "barbs".)

Category theorists define bisimulation to be a relation in a category of D-coalgebras, where D is some endofunctor. The relation gives us a span of sets that we want to extend to a span of coalgebras. Is there a way to take a relation like this and derive the functor D on Set and the coalgebra maps? If not on Set, then on some other relevant category?

GhaS Shee (Feb 26 2021 at 14:16):

I have a question. If we see the evaluation of a term in STL as a coalgebra, does anyone know what the counterpart of "normalization property" in algebra is?

GhaS Shee (Feb 26 2021 at 15:45):

Is it semi-decidable set?

GhaS Shee (Feb 26 2021 at 16:59):

I do not know what are semi-decidable sets and co-semi-decidable sets, and I am confused by them.
The counterpart of normalization seems to be the set of terms defined as they normalize.
Does anyone know where (co-)semi-decidable set is defined well and who defined them?

Christian Williams (Feb 26 2021 at 19:31):

Can you expand on what you mean by "algebraic counterpart"?

John Baez (Feb 26 2021 at 19:35):

A "semi-decidable set" is the same as a recursively enumerable set - in other words, a set $X$ for which there is an algorithm such that if $x \in X$ then the algorithm will prove this.

A "co-semi-decidable set" is the complement of a recursively enumerable set. In other words, it's a set $X$ for which there's an algorithm such that if $x \notin X$ then the algorithm will prove that.

GhaS Shee (Feb 27 2021 at 00:37):

@Christian Williams
Yes. As a $constructor_X : X \leftarrow F(X)$ (and the morphism from the least fixed point of $F$ to it i.e. the pair $(constructor_X, fold_{FX} )$ ) is an object of the category of $F$-Algebras , an $evaluation_X : X \leftarrow (X \leftarrow F(X))$ ( with the embedding of the $evaluation$ to Terminal Coalgebra i.e. the greatest fixed point of $F$ ) can be seen as that of the category of $F$-Coalgebras. the "normalization" is a predicate on objects of the category $F$-Coalgebras, while the "algebraic counterpart of normalization" is a predicate on objects of the category of $F$-Algebras.

(Edit: I was thinking of a particular $F$-Algebra , where $F(X) = Tm × ( 1+ Tm × (\frac{1}{1 - X}))$ and $Tm$ is the type of term constructors, and $\frac{1}{1 - T} = \mu X. 1 + T × X)$ . I was confused thinking that it might be generalized to all $F$-Algebra. Then, I should restrict the category $F$-Alg such that its dual category consists of susystems and its embeddings i.e. proper subsets of evaluation trees contained by the terminal object. That is, we might not see the detail of an algebra precisely until we define the coalgebra. )

@John Baez
Thank you very much for describing the definitions! They seem very meaningful.

GhaS Shee (Feb 27 2021 at 04:05):

In the above setting, I am not sure it is true, but I regarded fold maps as module homomorphisms and system embeddings as ring homomorphisms in terms of algebraic geometry. Then, what is the corresponding of rng homomorphism?

Jade Master (Mar 15 2021 at 17:11):

The article

• Bisimulation from open maps, André Joyal, Mogens Nielsen, and Glynn Winskel, Information and Computation 127:2 (1996) 164-185.

defines a bisimilarity between two objects $X$ and $Y$ of a category $M$ to be a span of open maps
$X \leftarrow A \to Y$
connecting them. Here's the definition of open map: Let $\mathcal{P} \hookrightarrow M$ be a full subcategory whose objects are regarded as paths. A morphism $f: X \to Y$ is open if for every commutative square
Screenshot-from-2021-03-15-10-09-01.png
with $P$ and $Q$ objects of $\mathcal{P}$, there is a morphism $p' : Q \to X$ making the following triangles commute
Screenshot-from-2021-03-15-10-09-36.png

Jade Master (Mar 15 2021 at 17:15):

My question is about the terminology "open". A map $f :X \to Y$ between topological spaces is open if for every open $U \subseteq X$, $f(U)$ is open in $Y$. Is the above definition an analogy for open maps of spaces? If so how?

Jade Master (Mar 15 2021 at 17:21):

To me it seems more like "continuous" because it says roughly that every path in $Y$ lifts to a path in $X$.

Fabrizio Genovese (Mar 15 2021 at 17:21):

What do you mean when you say "a full subcategory whose objects are regarded as paths"?

Fabrizio Genovese (Mar 15 2021 at 17:22):

Also, are $X, f, Y$ in $\mathcal{P}$?

Tom Hirschowitz (Mar 15 2021 at 17:23):

@Jade Master Have you looked into "A completeness theorem for open maps" by Joyal and Moerdijk? Don't have time right now but it is probably related.

Jade Master (Mar 15 2021 at 17:28):

Fabrizio Genovese said:

What do you mean when you say "a full subcategory whose objects are regarded as paths"?

$\mathcal{P}$ can be in principle whatever you like. I think the idea is that they represent a single execution so that a morphism $P \to X$ represents an execution of $X$. I'm a bit confused about what they should be for Petri nets....I don't think they're the same as Sassone's definition of execution.

Jade Master (Mar 15 2021 at 17:28):

Fabrizio Genovese said:

Also, are $X, f, Y$ in $\mathcal{P}$?

No not in general.

Jade Master (Mar 15 2021 at 17:29):

Tom Hirschowitz said:

Jade Master Have you looked into "A completeness theorem for open maps" by Joyal and Moerdijk? Don't have time right now but it is probably related.

Thank you that is a paper I am working on and it is definitely relevant :)

Fabrizio Genovese (Mar 15 2021 at 17:53):

Jade Master said:

Fabrizio Genovese said:

What do you mean when you say "a full subcategory whose objects are regarded as paths"?

$\mathcal{P}$ can be in principle whatever you like. I think the idea is that they represent a single execution so that a morphism $P \to X$ represents an execution of $X$. I'm a bit confused about what they should be for Petri nets....I don't think they're the same as Sassone's definition of execution.

Then I have trouble understanding what are the morphisms of $\mathcal{P}$ and what does it mean to have a morphism $X \to Y$ in $\mathcal{M}$ when $X$ is also in $\mathcal{P}$

Fabrizio Genovese (Mar 15 2021 at 17:53):

I agree, I feel their definition of execution is not "a string diagram in the category generated by a net"...

Jade Master (Mar 15 2021 at 18:09):

@Fabrizio Genovese X and Y are not in general in $\mathcal{P}$, they could be arbitrary Petri nets for example.

Fabrizio Genovese (Mar 15 2021 at 18:10):

I'm not talking about the ones in the diagram

Jade Master (Mar 15 2021 at 18:11):

So in words the path-lifting condition says that whenever there is a path in Y whose shape extends a path in X, then the path in Y lifts to a nice path in X.

Fabrizio Genovese (Mar 15 2021 at 18:12):

I'm saying, you have $\mathcal{M}$, a category, and $\mathcal{P}$, a subcategory of $\mathcal{M}$ whose objects are interpreted as paths. So, what is a morphism in $\mathcal{P}$? And if there is a morphism $X \to Y$ with $X$ object of $\mathcal{P}$ and $Y$ object of $\mathcal{M}$, how should I interpret these?

Fabrizio Genovese (Mar 15 2021 at 18:13):

So, for instance, $\mathcal{M}$ can be the category of Petri nets, and I can take a subcategory of it where the objects are interpreted as "paths of Petri nets"?

Jade Master (Mar 15 2021 at 18:14):

P is a full subcategory so the morphisms are the same as the morphisms in M. A morphism like you said should represent a path in Y.

Fabrizio Genovese (Mar 15 2021 at 18:14):

And then, a morphism $X \to Y$ with $X$ in the subcategory means "$X$ is a path of the net $Y$?

Fabrizio Genovese (Mar 15 2021 at 18:14):

Jade Master said:

P is a full subcategory so the morphisms are the same as the morphisms in M. A morphism like you said should represent a path in Y.

What? Paths were the objects, no?

Fabrizio Genovese (Mar 15 2021 at 18:15):

I'm really not understanding what's going on lol

Jade Master (Mar 15 2021 at 18:17):

Objects of P are like "walking paths" or "platonic paths" and then morphisms from an object of P to another object are like instances of that platonic path in another object.

Fabrizio Genovese (Mar 15 2021 at 18:18):

Ok, so objects of P are paths, and morphisms of P are ways of turning paths into other paths?

Jade Master (Mar 15 2021 at 18:19):

In "concatenable processes" Sassone defines a process to be a morphism of Petri nets $T \to P$ where T is a finite 1-safe acyclic deterministic net iirc.

Fabrizio Genovese (Mar 15 2021 at 18:19):

Ok, so the span conditions above reads: There's a way to reduce paths of $X$ and $Y$ to paths of some common object $A$

Fabrizio Genovese (Mar 15 2021 at 18:19):

Common object is not the right wording here

Fabrizio Genovese (Mar 15 2021 at 18:19):

But I guess you got what I mean

Jade Master (Mar 15 2021 at 18:20):

It's the same idea here as Sassone except I think the platonic paths are different

Jade Master (Mar 15 2021 at 18:21):

Yeah so open maps are morphisms which lift paths. So the common object has to lift paths from the two objects it's relating.

Fabrizio Genovese (Mar 15 2021 at 18:21):

Yep

Jade Master (Mar 15 2021 at 18:21):

Note that it's also a morphism so it also needs to preserve paths.

Fabrizio Genovese (Mar 15 2021 at 18:22):

Who is also a morphism? A?

Jade Master (Mar 15 2021 at 18:23):

An open morphism is in particular a morphism

Fabrizio Genovese (Mar 15 2021 at 18:24):

Oh, in that sense! Yep

Chad Nester (Mar 15 2021 at 18:33):

Haha the authors write “biproduct” when they mean “byproduct”.

Chad Nester (Mar 15 2021 at 18:34):

This is really interesting.

Jade Master (Mar 15 2021 at 19:15):

Chad Nester said:

Haha the authors write “biproduct” when they mean “byproduct”.

Where is that?

Chad Nester (Mar 15 2021 at 19:30):

First paragraph of section 4.

John Baez (Mar 15 2021 at 19:31):

I've seen other people who have studied too much category theory and not enough English who have made that mistake....

Chad Nester (Mar 15 2021 at 19:35):

@Jade Master thanks for linking that paper. I’ve been reading about these sorts of process equivalence recently and this is extremely clean. I like it!

John Baez (Mar 15 2021 at 19:39):

Fabrizio Genovese said:

So, for instance, $\mathcal{M}$ can be the category of Petri nets, and I can take a subcategory of it where the objects are interpreted as "paths of Petri nets"?

What's a "path of Petri nets" supposed to be? My guess is that in this bisimulation business it's really an execution history, i.e. a morphism in the commutative monoidal category generated by a specific Petri net.

This is just my wild guess. It could be completely wrong, since I haven't looked at the paper you're talking about. So, what's a "path of Petri nets"?

Chad Nester (Mar 15 2021 at 19:45):

I think that’s the right idea, although I suspect that taking the underlying category collapses too many things.

Chad Nester (Mar 15 2021 at 19:47):

If your monoidal category is freely generated by boxes then I think forming the free monoidal graph generated by those boxes and considering paths in it is closer.

Chad Nester (Mar 15 2021 at 19:47):

(Disclaimer: I don’t know much about Petri nets)

Jade Master (Mar 16 2021 at 02:17):

Chad Nester said:

Jade Master thanks for linking that paper. I’ve been reading about these sorts of process equivalence recently and this is extremely clean. I like it!

Thank you, for what it's worth I'm pretty sure this one of the more well-established definitions of bisimulation.

dusko (Mar 16 2021 at 02:31):

i don't know whether this will help or add to the confusion, but the problem might be that:

** the idea is that two systems should be bisimilar when they are observationally indistinguishable. (the idea of the semantics of computation observing not just the input-output relations, but also some computational effects goes back to milner's "processes" paper in the early 70s. what is observable varies. the first formalization of bisimilarity as a relation between systems in terms of a suitable relation between the states, viz a bisimulation, goes back to david park, also in the 70s. the concept got rediscovered several times in the next 15 years or so.)

** which processes are bisimilar thus does not depend on the processes alone, but also on how you observe them. more specifically, the various concepts of bisimulation do not necessarily arise within a category of coalgebras alone, but using a semantic functor into algebras of tests. ((in the CSP, tony hoare explicitly spelled out a gamut of bisimulation relations for the same CSP processes: depending on whether there are silent actions, refusals, failures... i think maybe 2 dozen bisimulations for the same family of process coalgebras. then in the 90s, rob van glabbeek spelled out in his famed thesis i think 133 notions of bisimulation for CCS processes, which could be viewed as vanilla mealy or moore machines IF you were only interested in their extensional behavior, and not in any side effects. i think rob spelled this out again in lengthy papers in the late 90s.))

** it so happens that the strongest possible concept of bisimilarity, which is sometimes referred to as "the" bisimulation, can be realized as indistinguishability by the anamorphisms. that is, in a sense, the least interesting concept semantically, but it got popular as a justification for working with coalgebras, since it comes out very simply. however, it led to this confusion that all bisimulations should come up like that. ((that can often be achieved, but for the price of a lot of avoidable and unenlightening work, which some poor people did invest. i had 2 or 3 papers in the mid 90s, massaging various interesting notions of bisimulation into coalgebras. once i followed what the native speakers of process algebra do, and specified the systems and the tests separately, as coalgebras and algebras, all fell in place much more easily. many people did that in the meantime.))

** petri nets are a system model, and there are also many different ways of interpreting/observing them, reflected in many different families of morphisms. this was an area of active research (and some controversy) also in the 90s, maybe early 2000s.

if you are in pisa, @Fabrizio, then ugo montanari might still be by far the best person to tell you about the various petri nets semantics. many of ugo's students could also provide the account. it is a rich story, and probably much easier to listen than to rediscover.

Jade Master (Mar 16 2021 at 03:00):

John Baez said:

Fabrizio Genovese said:

So, for instance, $\mathcal{M}$ can be the category of Petri nets, and I can take a subcategory of it where the objects are interpreted as "paths of Petri nets"?

What's a "path of Petri nets" supposed to be? My guess is that in this bisimulation business it's really an execution history, i.e. a morphism in the commutative monoidal category generated by a specific Petri net.

This is just my wild guess. It could be completely wrong, since I haven't looked at the paper you're talking about. So, what's a "path of Petri nets"?

This is something that I'm still trying to figure out...I'm not sure the answer.

Jade Master (Mar 16 2021 at 03:11):

dusko said:

i don't know whether this will help or add to the confusion, but the problem might be that:

** the idea is that two systems should be bisimilar when they are observationally indistinguishable. (the idea of the semantics of computation observing not just the input-output relations, but also some computational effects goes back to milner's "processes" paper in the early 70s. what is observable varies. the first formalization of bisimilarity as a relation between systems in terms of a suitable relation between the states, viz a bisimulation, goes back to david park, also in the 70s. the concept got rediscovered several times in the next 15 years or so.)

** which processes are bisimilar thus does not depend on the processes alone, but also on how you observe them. more specifically, the various concepts of bisimulation do not necessarily arise within a category of coalgebras alone, but using a semantic functor into algebras of tests. ((in the CSP, tony hoare explicitly spelled out a gamut of bisimulation relations for the same CSP processes: depending on whether there are silent actions, refusals, failures... i think maybe 2 dozen bisimulations for the same family of process coalgebras. then in the 90s, rob van glabbeek spelled out in his famed thesis i think 133 notions of bisimulation for CCS processes, which could be viewed as vanilla mealy or moore machines IF you were only interested in their extensional behavior, and not in any side effects. i think rob spelled this out again in lengthy papers in the late 90s.))

** it so happens that the strongest possible concept of bisimilarity, which is sometimes referred to as "the" bisimulation, can be realized as indistinguishability by the anamorphisms. that is, in a sense, the least interesting concept semantically, but it got popular as a justification for working with coalgebras, since it comes out very simply. however, it led to this confusion that all bisimulations should come up like that. ((that can often be achieved, but for the price of a lot of avoidable and unenlightening work, which some poor people did invest. i had 2 or 3 papers in the mid 90s, massaging various interesting notions of bisimulation into coalgebras. once i followed what the native speakers of process algebra do, and specified the systems and the tests separately, as coalgebras and algebras, all fell in place much more easily. many people did that in the meantime.))

** petri nets are a system model, and there are also many different ways of interpreting/observing them, reflected in many different families of morphisms. this was an area of active research (and some controversy) also in the 90s, maybe early 2000s.

if you are in pisa, @Fabrizio, then ugo montanari might still be by far the best person to tell you about the various petri nets semantics. many of ugo's students could also provide the account. it is a rich story, and probably much easier to listen than to rediscover.

Thanks for the reply. Why is indistinguishability by anamorphisms the least interesting sort of bisimulation?

Jade Master (Mar 16 2021 at 03:13):

If I understand you correctly, there are many choices of path subcategories and they all lead to different notions of bisimilarity and the choice depends on what you want to test for?

dusko (Mar 16 2021 at 03:31):

Jade Master said:

Thanks for the reply. Why is indistinguishability by anamorphisms the least interesting sort of bisimulation?

i guess because the assumption is that you can observe everything: there are no silent actions, no failures. but what is interesting is also in the eye of the observer. it is considered to be the least interesting by concurrency theorists, and i think milner says that somewhere in his CCS book, before he starts refining it. but joyal's view bisimulations as open maps is of course far from uninteresting if we are slightly interested in topology.

come to think, there was this conversation about tangent and cotangent bundles on another thread. there we have differential forms as coalgebras, and vector fields, and the usual dynamical systems workflow is reconstructed categorically by the system being observed along the curves on the manifold, i.e. by evaluating the coalgebra structure along the algebra structure. so it is the same approach like in concurrency: there is a description of the system, and there is a description of what is observable. there are probably variations in what can be observable here as well...

Tom Hirschowitz (Mar 16 2021 at 05:51):

@Fabrizio Genovese Path morphisms are thought of as path extensions. The easiest setting is the category of forests (= families of trees = presheaves on the ordinal $\omega$ viewed as a category), and paths are "branches" $\bullet \to \bullet \ldots \to \bullet$, which are determined by their length (the representables). By Yoneda, path extensions are just pairs $n \leq p$, and a morphism $n \to X$ merely picks a path of length $n$ in $X$.

Joachim Kock (Mar 16 2021 at 08:40):

Hi Jade, Fabrizio, and all,

just a few comments on open and etale maps. In the axiomatic setting of Joyal and Moerdijk, the notion of open map is just a weak version of etale, where 'weak' is meant in the technical sense: something defined in terms of weak pullback instead of true pullback. In turn this means that the the universal map into a pullback is merely required to exist but not to be unique. In the category of sets, this just means surjective over the true pullback. (A better terminology might be 'submersion' rather than 'open', but that's another discussion.)

Joachim Kock (Mar 16 2021 at 08:43):

As you say, the notion of open maps is a kind of path-lifting property: an open map is defined as one that has the (non-unique) right lifting property with respect to certain maps of paths, whereas an etale map is one that is right orthogonal (unique lifting) to that same class of path maps. If one digs into what these lifting properties mean, it boils down to some pullback conditions on mapping spaces, which are weak pullback condition in the case of open maps, and true pullbacks in the case of etale maps.

Joachim Kock (Mar 16 2021 at 08:46):

I do not think Joyal, Nielsen and Winskel apply the notion of open maps directly to Petri nets, but of course it makes sense to try figure out, as you do, what should be the notion of path to get a reasonable notion of open map. Since it is the weak version of etale map, it is better to get hold of the paths in terms of etale maps. Furthermore, you already know what the etale maps are: they are the maps simply called maps in Baez-Genovese-Master-Shulman! Namely, those maps of Petri nets that send (m,n)-ary transitions to (m,n)-ary transitions. You see immediately that it is a condition about bijections: they are those maps that are locally an isomorphism at each transition. (Well, to make sense of these bijections, it is probably necessary to abandon the classical notion of Petri net. For whole-grain Petri nets it is true that it is about bijections.)

Joachim Kock (Mar 16 2021 at 08:50):

Once we look locally, we can even restrict attention to either inputs or outputs. Then we are just talking about finite sets, and the strict orthogonality now boils down to this: in the category of sets, the etale maps are the bijections, and we know well that the class of bijections is right orthogonal to the class of all maps! But this refers locally to the transitions, so the class of path maps (the left-hand class) should be 'arbitrary on transitions', and it should remain something local. Of course it is difficult to say what these maps should be if the whole category of Petri nets we work in only has the etale maps to start with, but in the whole-grain formalism there is an obvious bigger category, namely the presheaf category of SITOS diagrams. In here the etale maps are precisely the standard etale maps of Joyal and Moerdijk. In here it is natural to take as the notion of path (which you may think of as infinitesimal path) simply the notion of arbitrary maps between transitions, or in graph language, maps between corollas. If you think of the node of a corolla as a point, and the small adjacent edges as an infinitesimal path or neighbourhood, then the left-hand class can be taken to be the class of maps between corollas, and the right-hand class will be those maps (in the presheaf category of SITOS diagrams) for which: for every node upstairs, and every corolla downstairs, there is a unique way to lift to a corolla upstairs. In other words, we do in fact recover the usual notion of transition-arity-preserving maps of Petri nets.

I do not understand completely how this argument should work for classical Petri nets. But all the arguments are precise and rigorous for whole-grain Petri nets. In fact it is exactly the same argument as for directed graphs, and the right-orthogonal-to-corolla-maps description of etale maps is Lemma 1.3.5 in my paper [Graphs, hypergraphs and properads].

Joachim Kock (Mar 16 2021 at 08:51):

Now, that notion of path is really more like an 'infinitesimal' version of path. To extend the left-hand class to bigger objects, the important point is that the bigger objects remain contractible. So instead of just corollas, one can take trees, or just linear trees. But it does not work if one allows anything with loops. This is precisely what one expects from geometry: for example the double cover of the circle is an etale map, and it does indeed have the path lifting property, but that does not mean one can lift a loop! A Petri-net version of the double-cover of a circle is given in Example 5.6 of [Elements of Petri nets and processes].

Joachim Kock (Mar 16 2021 at 08:53):

An alternative terminology for 'etale' would be a 'cover'. Just as in topology it is interesting to find the universal covering of a space, such as a 1-dimensional CW-complex, it is interesting to study the universal cover of a Petri net. As far as I understand, this is the notion of unfolding of a Petri net. It is a structure that contains all possible 'paths' of a Petri net (emanating from a fixed initial state) or all possible 'execution histories'. In the individual-token philosophy one would like to keep track of every token in every state. To do this (cf. van Glabbeek), one annotates every token with the complete history of the transition firings that produced it. In other words, a token occurrence is essentially the same thing as a point in the unfolding.

Joachim Kock (Mar 16 2021 at 08:55):

As far as I know, Winskel was interested in open maps because he needed to fix a problem with symmetries in unfolding semantics: something that looked like it should be an adjunction was simply not an adjunction, and it ended up being only a weak adjunction, or an adjunction up to some equivalence given by spans of open maps. In my opinion the whole problem is caused by the lack of control over symmetries in the classical notion of Petri nets. In fact, the problem goes away for whole-grain Petri nets, leading to a clean adjunction without the need of corrections in terms of open maps. This is Section 8 of my Petri-net paper. I think it is another good selling point of whole-grain Petri nets :-)

Joachim Kock (Mar 16 2021 at 09:00):

I don't want to say anything bad about open maps, and of course submersions are extremely important in geometry. But often weak pullbacks (and thereby notions of open maps, etc.) appear as a work-around for some homotopy structure that has been suppressed.

Here are three more examples of this, relevant to the present discussion: one is that operads and analytic functors in the category of sets are endofunctors that preserve weak pullbacks, not strict pullbacks. But once you upgrade to groupoids, the correct and natural notion is true pullback (which then means homotopy pullback).

Similarly, in recent work in probability, Constantin, Fritz, Perrone and Shapiro work out some interesting theory of partial evaluations, and end up with weak-pullback versions of the decomposition-space axioms. I think the reason is that they take their bar constructions to be simplicial sets. If they considered simplicial groupoids instead, I think the conditions would be true pullbacks.

Finally, weak orthogonality is of course a key ingredient in Quillen model categories. But I think one can argue that they are there because it is a 1-categorical approach to something homotopical. If you pass to the native \infty-categorical setting, it is the true orthogonality that is the correct notion again.

(Maybe I should not call it a work-around, but just call it an interesting different approach to some homotopy stuff. After all, all these cases lead to super-interesting mathematics, and I do not doubt that open maps are important in process calculi. I am always worried I say something that sounds like criticism...)

Nathanael Arkor (Mar 16 2021 at 09:38):

I don't want to say anything bad about open maps, and of course submersions are extremely important in geometry. But often weak pullbacks (and thereby notions of open maps, etc.) appear as a work-around for some homotopy structure that has been suppressed.

This is a very helpful insight!

Fabrizio Genovese (Mar 16 2021 at 10:10):

Tom Hirschowitz said:

Fabrizio Genovese Path morphisms are thought of as path extensions. The easiest setting is the category of forests (= families of trees = presheaves on the ordinal $\omega$ viewed as a category), and paths are "branches" $\bullet \to \bullet \ldots \to \bullet$, which are determined by their length (the representables). By Yoneda, path extensions are just pairs $n \leq p$, and a morphism $n \to X$ merely picks a path of length $n$ in $X$.

This is helpful, thanks!

Fabrizio Genovese (Mar 16 2021 at 10:11):

@dusko I am still in Pisa, but I'm really not in Pisa. Given the COVID mess I've been working from home since my postdoc started, and I still didn't manage to go there to say hi T_T

Fabrizio Genovese (Mar 16 2021 at 10:11):

@Joachim Kock This is very detailed and helpful, thanks. Still, at least for me, it will take a bit to unpack. :smile:

Tom Hirschowitz (Mar 16 2021 at 10:29):

@Joachim Kock A difference in spirit between concurrency and homotopy is that path extensions are not at all meant to become equivalences: the idle process • should remain different from the non-idle • → •. So I'm curious about what the suppressed homotopy structure is in this case! Maybe it has to do with directed topology?

Joachim Kock (Mar 16 2021 at 13:12):

Thanks, Fabrizio. I actually wanted to expand on these things. I do realise there is some intuition and background here not really coming from Petri-net theory. I would like to go through the whole yoga of shapes and elementary shapes and etale maps and so on, step by step, starting with directed graphs and categories, then trees and operads, then (open) graphs and properads/props, and finally (whole-grain) Petri nets. I hope to get around to it over the coming days...

Joachim Kock (Mar 16 2021 at 13:26):

Hi Tom, I am afraid I caused confusion with my various homotopy analogies. Maybe I should not have mentioned model categories. The suppressed homotopy theory in combinatorics is only about symmetries. Classical Petri nets have a lot of suppressed symmetries: namely, instead of having a set of incoming or outgoing arcs of a transition (from a given place), there is only a number of them. So there is no way of keeping track of symmetries of input args. If you want to probe Petri nets by mapping into them, for example with paths or occurrence nets, in the spirit of Goltz-Reisig processes, the symmetries of these maps are lost. It leads to the rather surprising fact that Goltz-Reisig processes cannot be composed! This makes geometric and algebraic semantics of classical Petri nets different. My viewpoint is that this is a self-inflicted problem, due to the multiset definition of Petri nets. The problem goes away with whole-grain Petri nets.

The other example I mentioned is that unfoldings of Petri nets ought to be terminal objects in a certain category -- that should be their universal property. But it turns out (Winskel et al.) that the candidate for this terminal object (namely the unfolding in the usual sense) has symmetries, and therefore cannot be a terminal object. The symmetries are caused by the fact that they are maps into Petri nets, and if the sets of incoming or outgoing arcs are collapsed to a number instead of being a set, then the maps into them get too many symmetries. As I mentioned, the problem goes away when considering whole-grain Petri nets instead of ordinary Petri nets.

Fabrizio Genovese (Mar 16 2021 at 13:37):

Joachim Kock said:

Thanks, Fabrizio. I actually wanted to expand on these things. I do realise there is some intuition and background here not really coming from Petri-net theory. I would like to go through the whole yoga of shapes and elementary shapes and etale maps and so on, step by step, starting with directed graphs and categories, then trees and operads, then (open) graphs and properads/props, and finally (whole-grain) Petri nets. I hope to get around to it over the coming days...

That would be great! Homotopy theory is very far from my background so anything that can help is appreciated!

Fabrizio Genovese (Mar 16 2021 at 13:39):

If some other people are interested and you have time, would it make sense to have some open-access zoom conversations that we can then record and share? I don't know which way you prefer, I often feel that writing something in detail takes longer than actually telling a story on video

Jade Master (Mar 16 2021 at 14:36):

Fabrizio Genovese said:

Joachim Kock said:

Thanks, Fabrizio. I actually wanted to expand on these things. I do realise there is some intuition and background here not really coming from Petri-net theory. I would like to go through the whole yoga of shapes and elementary shapes and etale maps and so on, step by step, starting with directed graphs and categories, then trees and operads, then (open) graphs and properads/props, and finally (whole-grain) Petri nets. I hope to get around to it over the coming days...

That would be great! Homotopy theory is very far from my background so anything that can help is appreciated!

I would also very much enjoy hearing about this :)

Tom Hirschowitz (Mar 16 2021 at 15:51):

Me too!

Jade Master (Mar 16 2021 at 16:08):

@Joachim Kock
After reading and thinking a bit more I am starting to really appreciate this analogy to covering spaces which you have figured out. Just like a cover $E \to B$ of topological spaces, a morphism $P \to Q$ is a covering if it is locally an isomorphism and it is surjective. The local isomorphism part is covered by being an etale map (the pullback squares guarantee this). To recover a definition of open map like I wrote above we want to prove a version of the path-lifting lemma but in the context of Petri nets instead of spaces. I think that this part should follow without much work...a path in P can be lifted to a path in Q by chaining together the lifts guaranteed by the local isomorphisms in the covering $P \to Q$. Does that sound right to you?

Jade Master (Mar 16 2021 at 16:10):

By the way the idea that the unfolding of a net is its universal cover is really beautiful. I read it when your paper came out but I haven't really appreciated it until now.

Joachim Kock (Mar 16 2021 at 19:32):

Fabrizio Genovese said:

If some other people are interested and you have time, would it make sense to have some open-access zoom conversations that we can then record and share? I don't know which way you prefer, I often feel that writing something in detail takes longer than actually telling a story on video

I will certainly write something, but this week is a bit busy because of the polynomial workshop.
On the other hand, it sounds like fun to organise a little discussion session! And I also have many questions myself.

Joachim Kock (Mar 16 2021 at 19:43):

@Jade Master , yes that sounds right. The main question is what it means to chain together lifts. This has to be subject to some kind of simply-connectedness, because there are certainly loop-like shapes that should not be required liftable. Another question is that I was probably too fast to equate etale maps and coverings. At least, I think it is practical not to demand etale maps to be surjective, because it is nice to have the members of a covering family (in the sense of a Grothendieck topology) not to be surjective individually. Maybe I am at odds with standard terminology?

Jade Master (Mar 16 2021 at 20:04):

I don't know much about Grothendieck topologies or etale maps but the definition of cover that I have in mind is surjective.

John Baez (Mar 16 2021 at 20:31):

In topology a cover can have any number of sheets, including zero. So a cover doesn't need to surjective. One style of definition goes roughly

$p: E \to B$ is a cover if given a path $\gamma : [0,1] \to B$ in the base and a point $e \in E$ with $p(e) = \gamma(0)$, there is a unique lift of $\gamma$ to $E$

and this is automatically true if $E$ is empty.

Another style of definition goes roughly

$p: E \to B$ is a cover if given any point $b \in B$ there is a neighborhood $U$ of $b$ such that $p^{-1}(U)$ is a disjoint union of copies of $U$, with the projection $p$ being a homeomorphism on each copy

and again this is automatically true if there are no copies of $U$.

But a nonempty cover of a connected space is surjective!

John Baez (Mar 16 2021 at 20:33):

People usually don't care much about empty covers, of course.

Jade Master (Mar 16 2021 at 20:54):

The definition in May's book on algebraic topology requires that the map be surjective Screenshot-from-2021-03-16-13-51-58.png

Jade Master (Mar 16 2021 at 20:55):

The assumption here is that all spaces are path connected.

John Baez (Mar 16 2021 at 21:01):

Okay. He's demanding surjectivity "by hand" to eliminate the empty cover, since a cover of a path connected space (using my definitions of cover) is nonempty iff $p$ is surjective.

John Baez (Mar 16 2021 at 21:02):

And this makes some sense, because one thing people like to do is think about $\pi_1$ of a covering space, and this makes no sense if the space is empty - there's no basepoint!

John Baez (Mar 16 2021 at 21:05):

Oh, and another very good reason to demand that a covering space of a path connected space be nonempty (and thus surjective) is to make sure the initial object in the category of covers is interesting!

If you rule out the empty cover, the usual "universal cover" is initial in the category of covers!

If you allow the empty cover, then it is the initial cover!

John Baez (Mar 16 2021 at 21:06):

So okay: all the usual theory of universal covers and $\pi_1$ works better if we exclude the empty cover.

John Baez (Mar 16 2021 at 21:08):

I guess the "rational" explanation for ruling out the empty cover is this: as algebraic topologists studying $\pi_1$ and such, we are working in the category of pointed spaces.

Reid Barton (Mar 16 2021 at 21:11):

Right, you also need to fix a basepoint for the universal cover in order for it to be an initial object (otherwise it has automorphisms, the deck transformations). And then the covering map will at least be surjective onto the component of the base space that contains its basepoint.

John Baez (Mar 16 2021 at 21:48):

So, from what I can see from that one passage, Peter May should not have stuck in "surjective" by hand. He should have said he was working in the category of pointed path-connected spaces.

But maybe he was wanting to explore the consequences of changing the basepoint: seeing how that affects $\pi_1$.

Uli Fahrenberg (Mar 18 2021 at 16:42):

Sorry I'm late to this discussion, I'm only now starting to figure out this zulip thing because of the Very Nice Workshop.
So no, "open maps" have nothing to do with topological notions of open-ness, but everything with path liftings and weak fibrations. There's a nice paper by Kurz and Rosický on bisimulations and weak fibration systems, and people have tried things with model categories (Tom?).
Logicians seem to say "bounded morphism" instead of "open map", and these briefly made an appearance in Helle's nice talk yesterday.

Tom Hirschowitz (Mar 18 2021 at 16:54):

@Uli Fahrenberg Haha, yes, tried. Kris Worytkiewicz and I gave it an unsuccsessful go at some point.

Uli Fahrenberg (Mar 18 2021 at 17:16):

@Tom Hirschowitz It seems the idea is not yet dead: Eric is still thinking about this :)

Tom Hirschowitz (Mar 18 2021 at 17:23):

Yeah, me too, sometimes.

Naso (Mar 19 2021 at 03:57):

@Jade Master I had looked at that paper "Bisimulation from Open Maps" before and got confused about a few things, since you are discussing it maybe someone can help me.

First, I'm confused about why bisimilarity is defined as a span of open maps rather than just an open map or maybe a pair of open maps in opposite directions...

E.g. in the proof of Theorem 2 (p170), it says:

"If transition systems are connected by a $Bran_L$-open morphism then because its function on states
satisfies the ``zig-zag'' condition (Proposition 1) its graph is a strong bisimulation. Strong bisimilarity is an equivalence relation. Hence a span of $Bran_L$-open morphisms between two transition systems makes them strong bisimilar"

Is this implying the existence of a (strong) bisimulation $X \to Y$ makes $X$ and $Y$ (strong) bisimilar? If so why do we need a span of bisimulations instead of just one open map?

Second, if we say bisimulation is a span of open maps $X_1 \leftarrow X \to X_1$, what stops us from settings $X = 0$ to be the empty transition system: it seems the empty function can be an open-map? That would mean all systems are bisimilar...

Edit: it seems they require the transition system to have an initial state: I guess that answers my second question?

Uli Fahrenberg (Mar 19 2021 at 05:39):

@Nasos Evangelou-Oost The intuition is that you want bisimulations to be relations. The morphisms in your category are thought of as functional simulations, so open maps would be functional bisimulations; but what we're really interested in are not functions, but relations. Relating the states in a transition system so that related states have similar behavior.