Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: theory: applied category theory

Topic: ACT2020


view this post on Zulip John Baez (Mar 23 2020 at 22:01):

Due to the coronavirus outbreak, many universities are moving activities online. This is a great opportunity to open up ACT2020 to a broader audience, with speakers from around the world.

The conference will take place July 6-10 online, coordinated by organizers in Boston USA. Each day there will be around six hours of live talks, which will be a bit more spaced out than usual to accommodate the different time zones of our speakers. All the talks will be both live streamed and recorded on YouTube. We will also have chat rooms and video chats in which participants can discuss various themes in applied category theory.

We will give more details as they become available and post updates on our official webpage:

http://act2020.mit.edu

Since there is no need to book travel, we were able to postpone the acceptance notification, and hence the submission deadline. If you would like to speak, please prepare an abstract or a conference paper according to the instructions here:

http://act2020.mit.edu/#papers

Important dates (all in 2020)

• Submission of contributed papers: May 16
• Acceptance/Rejection notification: June 07
• Tutorial day: July 5
• Main conference: July 6-10

Registration will now be free; please register for the conference ahead of time here:

http://act2020.mit.edu/#registration

We will send registering participants links to the live stream, the recordings, and the chat rooms, and we’ll use the list to inform participants of any changes.

All the best,
The ACT committee

Here are the local organizers:

• Destiny Chen (administration)
• Brendan Fong
• David Jaz Myers (logistics)
• Paolo Perrone (publicity)
• David Spivak

Here is the committee running the school:

• Carmen Constantin
• Eliana Lorch
• Paolo Perrone

Here is the steering committee:

• John Baez
• Bob Coecke
• David Spivak
• Christina Vasilakopoulou

Here is the program committee:

• Mathieu Anel, CMU
• John Baez, University of California, Riverside
• Richard Blute, University of Ottawa
• Tai-Danae Bradley, City University of New York
• Andrea Censi, ETC Zurich
• Bob Coecke, University of Oxford
• Valeria de Paiva, Samsung Research America and University of Birmingham
• Ross Duncan, University of Strathclyde
• Eric Finster, University of Birmingham
• Brendan Fong, Massachusetts Institute of Technology
• Tobias Fritz, Perimeter Institute for Theoretical Physics
• Richard Garner, Macquarie University
• Fabrizio Romano Genovese, Statebox
• Amar Hadzihasanovic, IRIF, Université de Paris
• Helle Hvid Hansen, Delft University of Technology
• Jules Hedges, Max Planck Institute for Mathematics in the Sciences
• Kathryn Hess Bellwald, Ecole Polytechnique Fédérale de Lausanne
• Chris Heunen, The University of Edinburgh
• Joachim Kock, UAB
• Tom Leinster, The University of Edinburgh
• Martha Lewis, University of Amsterdam
• Daniel R. Licata, Wesleyan University
• David Jaz Myers, Johns Hopkins University
• Paolo Perrone, MIT
• Vaughan Pratt, Stanford University
• Peter Selinger, Dalhousie University
• Michael Shulman, University of San Diego
David I. Spivak, MIT (co-chair)
• Walter Tholen, York University
• Todd Trimble, Western Connecticut State University
Jamie Vicary, University of Birmingham (co-chair)
• Maaike Zwart, University of Oxford

view this post on Zulip Jules Hedges (Jun 07 2020 at 22:12):

Thread for everyone to talk about what they'll be presenting at ACT2020

view this post on Zulip Joe Moeller (Jun 07 2020 at 22:15):

I'll be talking about Petri nets with catalysts: https://compositionality-journal.org/papers/compositionality-1-4/

view this post on Zulip Joe Moeller (Jun 07 2020 at 22:17):

The basic idea is that if your Petri net has a "catalyst", then the category of executions is actually a disjoint union of a bunch of subcategories, each corresponding to the possibilities for a given amount of catalyst.

view this post on Zulip Joe Moeller (Jun 07 2020 at 22:20):

These subcategories inherit a premonoidal structure from the bigger category's monoidal structure, and you can modify the string diagrams to fit that setting to keep track of where the catalysts are being used.

view this post on Zulip Joe Moeller (Jun 07 2020 at 22:22):

This to me occupies a sort of corner case of the monoidal Grothendieck construction, since there we have a theorem that says that if you have a monoidal (op)fibration and the base category is (co)cartesian, you can transfer monoidal structures between the fibres and the total category.

view this post on Zulip Joe Moeller (Jun 07 2020 at 22:23):

But in this case we don't have a cartesian base, so the monoidal structure of the total category breaks on it's way to the fibres.

view this post on Zulip Fabrizio Genovese (Jun 07 2020 at 22:51):

My paper got rejected, but I think in particular one reviewer didn't understand anything about it. So I'm going to explain what we did anyway.
We started with finite state machines, and wanted to turn them into ZK-SNARKs. A ZK-SNARK is a type of zero knowledge proof. That is, it is a way to prove that I know or did something (e.g. I performed a computation) without revealing anything about it. We want to do this so that we can deploy an execution trace of a given FSM on the blockchain without revealing at all what the FSM does.
ZK-SNARK theory is difficult and non-compositional, but you can turn a boolean circuit into a zk-SNARK with already existing software, such as libsnark. So we bypassed the non-compositional part by looking at ways to compositionally turn a FSM into a boolean circuit.
We proceeded as follows: First, we noticed that the execution traces of a FSM are just the morphisms in the free category generated by its underlying graph. That is, every morphism in this category represents a possible path of the FSM.
We found a way to compositionally assemble circuits verifying that a given sequence of morphisms in a free category composes to a morphism. That is, if I give you f:ABf: A \to B and g:CDg: C \to D then the circuit will return "ok" iff B=CB = C.
We then generalized to circuits that can accept both a graph specification and a sequence of morphisms. These return "ok" only if the sequence of morphisms defines a valid path in the free category defined by the specification provided to the circuit.

Since what we need is actually a circuit implementation to pass to libsnark, we had to work in a bicategorical setting. That is, we couldn't identify extensionally equal circuits because, albeit doing the same thing, these would be different implementations, and libsnark would treat them differently. I think the major contribution of our work is that we weren't using category theory to study boolean circuits, but category theory to compositionally asseble circuits for a real world application. In particular we were working to actually implement this thing in a formally verified way using idris-ct, our formally verified category theory library.
Also, this outlined another possible approach to categorical cryptography: Instead of trying to describe/study cryptography compositionally, just use categories to compositionally map structures into cryptographic primitives, and let mainstream cryptography take care of the rest from there.

We presented this paper in a talk at DEVCON V in Osaka, and you can find it here: https://arxiv.org/abs/1909.02893

view this post on Zulip John Baez (Jun 08 2020 at 00:47):

I'll be talking about this paper:

It studies the relation between black-boxing an open Markov process and coarse-graining it, i.e. simplifying it by lumping a bunch of states into one. We do this using a double category where the horizontal morphsms are open Markov processes and coarse-grainings are 2-cells (squares).

There's some neat stuff required to make everything work. In addition to double categories we need a reasonable amount of linear algebra, which interacts with the category theory in a neat way. For example, to get everything to work we need to use a van Kampen cube, which is a funny (but fairly widespread) mixture of pushouts and pullbacks.

view this post on Zulip Jules Hedges (Jun 08 2020 at 12:41):

Either me or Philipp Zahn will be doing a tool demo for open games with some application to (probably) auction theory (code is https://github.com/jules-hedges/open-games-hs)

view this post on Zulip Jules Hedges (Jun 08 2020 at 12:42):

I'll also be presenting this extended abstract (which I talked about somewhere on here at some point), "Non-compositionality in categorical systems theory" https://obsoletewallstreet.files.wordpress.com/2020/05/categorical-systems-theory-3.pdf

view this post on Zulip Morgan Rogers (he/him) (Jun 08 2020 at 13:28):

I've just been told by @Lachlan McPheat that he (or perhaps one of his coauthors) will be presenting their recent paper on Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality. I'll encourage him to post on here with an overview of what that's about :tada:

view this post on Zulip Jade Master (Jun 08 2020 at 17:05):

I'll be presenting the first paper that John and I wrote Open Petri Nets. It's been a few years since we wrote this and I'm really happy to see how the ideas have matured and the motivations have shifted. It has been selected for a longer talk, so I intend on really getting into it (as well as getting into the motivation).

This paper is about applying operational semantics to open Petri nets. In particular, there is a symmetric monoidal (double) category where the morphisms are open Petri nets and the composition is gluing. Each Petri net has an associated category whose morphisms represent executions of your Petri net. The construction of this category can be viewed as a symmetric monoidal (double) functor from the (double) category of open Petri nets. Because composition is gluing, this provides a compositional theory for computing the process of your Petri net. This operational semantics can be deflated further to give a reachability semantics for open Petri nets. The reachability semantics sends an open Petri net to the reachability relation on its inputs and outputs. However, this semantics is only laxly functorial.

view this post on Zulip Bobby T (Jun 10 2020 at 11:55):

Hi everybody: I submitted a form to register for the tutorial day and still haven't gotten any kind of confirmation or rejection or anything - I assumed that the June 07 deadline @John Baez posted was referring to both paper submissions and tutorial day stuff, but now I'm beginning to wonder whether that's the case. Does anyone know if I should be expecting some kind of confirmation, or will I just get emails shortly before to participate?

view this post on Zulip John Baez (Jun 10 2020 at 18:25):

Bobby T said:

Hi everybody: I submitted a form to register for the tutorial day and still haven't gotten any kind of confirmation or rejection or anything - I assumed that the June 07 deadline John Baez posted was referring to both paper submissions and tutorial day stuff, but now I'm beginning to wonder whether that's the case. Does anyone know if I should be expecting some kind of confirmation, or will I just get emails shortly before to participate?

Paper submissions are completely different from tutorial day. I'll ask the people who run the tutorial day what people should expect. There was limited seating back before COVID-19 struck, but now tutorial day is happening online, so plans have changed.

view this post on Zulip Morgan Rogers (he/him) (Jun 10 2020 at 19:09):

@David Spivak and co. are still in the process of re-organizing how tutors will contribute to the tutorial day. It's hoped (based on discussion this evening/morning depending on time zones) that it will be as inclusive as possible, and so even if it's short notice - the tutorial day is next month - I expect that more people will be able to contribute in some form to make the event more accessible. I expect he will post an update here when decisions are made.

view this post on Zulip Bobby T (Jun 13 2020 at 16:45):

Alright, excellent, thank you both - I'll keep an eye out for updates!

view this post on Zulip John Baez (Jun 17 2020 at 19:09):

Here is an update on the ACT2020 tutorial day.

Applied category theory offers a rigorous mathematical language and toolset for relating different concepts from across math, science, and technology. For example, category theory finds common patterns between geometry (shapes), algebra (equations), numbers, logic, probability, etc. Applied category theory (ACT) looks for how those very same patterns extend outward to data, programs, processes, physics, linguistics, and so on—things we see in the real world. The field is currently growing, as new applications and common patterns are being found all the time. When you understand these ideas, more of your intuitions about the world can be made rigorous and thus be communicated at a larger scale. This in turn gives our community a chance to solve larger and more complex scientific, technological, and maybe even societal problems.

This year's international applied category theory conference ACT2020 is having a tutorial day, meant to introduce newcomers to applied category theory. Tutorial day will take place on July 5 and will include a few main topics that will be taught semi-traditionally (via presentation, exercises, and discussion) over Zoom, as well as mentors who will be available throughout the day to work with smaller groups and/or individuals. We invite you to sign up [here](Text for students:
Applied category theory offers a rigorous mathematical language and toolset for relating different concepts from across math, science, and technology. For example, category theory finds common patterns between geometry (shapes), algebra (equations), numbers, logic, probability, etc. Applied category theory (ACT) looks for how those very same patterns extend outward to data, programs, processes, physics, linguistics, and so on—things we see in the real world. The field is currently growing, as new applications and common patterns are being found all the time. When you understand these ideas, more of your intuitions about the world can be made rigorous and thus be communicated at a larger scale. This in turn gives our community a chance to solve larger and more complex scientific, technological, and maybe even societal problems.

This year's international applied category theory conference ACT2020 is having a tutorial day, meant to introduce newcomers to applied category theory. Tutorial day will take place on July 5 and will include a few main topics that will be taught semi-traditionally (via presentation, exercises, and discussion) over Zoom, as well as mentors who will be available throughout the day to work with smaller groups and/or individuals. We invite you to sign up here if you're interested, so we can keep you posted. Hope to see you there!

The four courses will be roughly as follows:

I think this means they're still just trying to get as many students as possible.

view this post on Zulip Tomáš Gonda (Jul 02 2020 at 23:30):

Let's revive this thread now that the conference is around the corner!

I will be talking about a project tentatively titled:

It is a work in collaboration with Tobias Fritz, Paolo Perrone, and Eigil Rischel; in which we study what can one do with Markov categories that have distribution objects, which one can think of as spaces of measures. With this kind of structure, we can prove abstract versions of results such as:

  1. The equivalence between the existence of partial evaluations between two measures and the second-order stochastic dominance relation of the two measures. The latter is a common way to compare measures in terms of how "spread out" they are and the former is the lowest level of the bar construction.

  2. Blackwell-Sherman-Stein Theorem. This result characterizes the "informativeness" order relation of statistical models in terms of the existence of a post-processing that simulates one from the other. In particular, it shows that this relation is isomorphic to the second-order stochastic dominance relation of measures over the space of posterior distributions over the tested hypotheses that a Bayesian agent would assign having performed the statistical experiment. That is, a statistical experiment is more informative iff the posteriors are more spread out (so that doing the experiment allows one to distinguish between the hypotheses better), in a precise sense that we can now make use of in any suitable Markov category.

Apart from generalizing some known results from mathematical statistics, we also advance the theoretical understanding of Markov categories relevant to these concepts. Specifically, we elucidate the relation between Markov categories and monoidal monads - showing under what conditions can we think of a Markov category as the Kleisli category of a probability monad (and vice versa).

blackwell_act.pdf

view this post on Zulip Morgan Rogers (he/him) (Jul 03 2020 at 10:49):

@Tomáš Gonda are you aware of the dedicated #ACT 2020 stream? It has a dedicated topic for each talk, so it will be much easier to keep track of conversations there.
I'll take this opportunity to suggest that @everyone interested subscribe to the stream #ACT 2020, since not everyone was subscribed automatically.

view this post on Zulip Paolo Perrone (Jul 03 2020 at 14:51):

Tomáš Gonda said:

...
I will be talking about a project tentatively titled:

Here is the dedicated thread, by the way.