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.
David Corfield (Dec 17 2024 at 11:15):@Mike Shulman brought up on another thread the work of Harper et al. on a language for computational cost. Three relevant articles are:
David Corfield (Dec 17 2024 at 11:16):The first and the second of these take an ‘algebraic’ approach to provide a language which captures the ‘cost’ of a program via, in turn, a graded cost monad and then an ordered graded cost monad. The third article then looks at coalgebras within categories of cost algebras. One can provide cost (amortized) analysis via coalgebra morphisms to simpler cost algebras.
David Corfield (Dec 17 2024 at 11:16):The authors hint at the end that a more even-handed bialgebraic approach might be fruitful. I know a little about this in terms of Bartek Klin’s Bialgebras for Structural Operational Semantics
So via a [[distributivity law]] between the relevant algebra and coalgebra functors, and , one may study “the interplay between the structure (syntax) and the dynamics (behavior) of systems” via bialgebras, .
David Corfield (Dec 17 2024 at 11:17):So my question: What do people see as the best results of this bialgebraic outlook? Of course, I can hunt out articles that have referred to Klin’s, but I’d be interested in assessments of this approach.
David Corfield (Dec 17 2024 at 11:27):I know many people around these parts have taken the study of systems in a Spivakian direction. But even here, of course, a coalgebraic framing is possible, e.g.,
Stelios Tsampas (Dec 19 2024 at 16:03):There's plenty of nice work on bialgebraic semantics. They've been a popular medium to study (various phenomena on) various flavors of process calculi at an abstract level, or come up with new flavors altogether. Few highlights:
My biggest gripe with bialgebraic semantics semantics used to be that they can't do higher-order at all, as well as imperative languages in a satisfactory way. Luckily, in 2023 we extended the original bialgebraic framework to higher-order languages:
HIgher-order bialgebraic semantics is what I mostly do on my research time these days. Since the nice result above, we have been unifying and simplifying important "operational" (i.e. methods that apply to operational semantics) reasoning methods in higher-order languages, as well as applying them to new languages e.g.
Stelios Tsampas (Dec 19 2024 at 16:05):Generally speaking, if a certain class of coalgebras accurately model a certain type of dynamical systems (in this case cost-awareness I suppose), then the bialgebraic perspective should be useful in studying programming languages of said type.
David Corfield (Dec 24 2024 at 08:19):Great, thanks for this @Stelios Tsampas. As a newcomer to this topic, it feels like this approach should have very wide application, outside computing too.
Stelios Tsampas (Dec 24 2024 at 08:41):Yeah, might as well! After all, bialgebras, be it higher-order or first-order, broadly express something fundamental: the compositional interaction between a syntax and a behavior (or semantics).
Personally speaking, so far I am enjoying generalizing and simplifying operational phenomena; I have also caught myself wondering just how many mathematical phenomena are operational to begin with. This might be a pretty deep rabbit hole, one I would be excited to dig into. Currently I am working on parametricity within HO Abstract GSOS, and at some point I am looking to do dependent types within the framework. If this happens, then it would open interesting foundational possibilities.
Stelios Tsampas (Dec 24 2024 at 08:42):@David Corfield Are you working on bialgebras as part of a thesis or?
David Corfield (Dec 24 2024 at 10:50):@Stelios Tsampas No, I'm just a philosopher (co-founder of the n-Category Cafe) whose department was closed, and who has been lucky enough to find some ARIA safeguarded AI funding.
I'm working with a couple of guys on amortization and graded monads, and through the references I mentioned have seen a larger story.
Stelios Tsampas (Dec 24 2024 at 11:36):David Corfield said:
Stelios Tsampas No, I'm just a philosopher (co-founder of the n-Category Cafe) whose department was closed, and who has been lucky enough to find some ARIA safeguarded AI funding.
I'm working with a couple of guys on amortization and graded monads, and through the references I mentioned have seen a larger story.
Geez, the least I could have done is know the co-founder of the website I am visiting multiple times a day! Guess I live under a rock :man_facepalming:.
My current group at FAU Erlangen-Nuremberg (although I'm leaving next month) does a lot of work on graded monads, e.g. Lutz Schröder and Stefan Milius. I have been thinking about bialgebraic semantics on graded monads but I never found the time to give it a closer look. To me, it looks like a natural question.
David Corfield (Dec 24 2024 at 11:57):Well, my focus moved more to the nForum/nLab after around 2014 (my nCafe posts).
I think the graded cost monad story works best by taking a 2-functor from the delooped thin monoidal category corresponding to an ordered monoid. Then the graded algebras for this graded monad are the things Uustalu is talking about in these slides.
Then presumably it would need some form of distributivity with the program coalgebra endofunctors that Grodin and Harper are studying in Amortized Analysis via Coalgebra.
David Corfield (Dec 24 2024 at 12:15):Post-2014, I was focusing more on modal HoTT, and potential applications in physics (the Urs Schreiber program). But even here there are probably opportunities from what we're talking about.
Something that's been worked out in linear HoTT is the [[deferred measurement principle]], establishing that in
any quantum circuit involving quantum measurement of some of the qbits followed by quantum gates controlled by the respective measurement outcomes
is equivalent as a function from given input to output as
a quantum circuit in which all quantum measurement happens “at the end”.
The nLab page states
The principle can be useful in practice for optimizing quantum circuits.
Wikipedia adds this detail:
Thanks to the deferred measurement principle, measurements in a quantum circuit can often be shifted around so they happen at better times. For example, measuring qubits as early as possible can reduce the maximum number of simultaneously stored qubits; potentially enabling an algorithm to be run on a smaller quantum computer or to be simulated more efficiently. Alternatively, deferring all measurements until the end of circuits allows them to be analyzed using only pure states.
Maybe something for a later date when you've worked through dependent type theory.
Stelios Tsampas (Dec 24 2024 at 12:48):David Corfield said:
I think the graded cost monad story works best by taking a 2-functor from the delooped thin monoidal category corresponding to an ordered monoid. Then the graded algebras for this graded monad are the things Uustalu is talking about in these slides.
I see. This is the dual take to what I had in mind; I was thinking of ordinary algebras mixing with coalgebras for a graded monad. Either way, I have not encountered any definition of a distributive law/GSOS law of a graded monad over an endofunctor or a distributive law of an endofunctor over a graded monad. I expect one will be able to come up with a definition for either, but I wonder how strong the underlying commutativity conditions would be. They might even be unrealistic.
David Corfield said:
Then presumably it would need some form of distributivity with the program coalgebra endofunctors that Grodin and Harper are studying in Amortized Analysis via Coalgebra.
From what I can tell, they have coalgebras in a category of algebras, which immediately raises the question if there is something bialgebraic going on (they are also acknowledging this in the last section).
David Corfield (Dec 24 2024 at 14:38):Stelios Tsampas said:
...they are also acknowledging this in the last section
Yes, that's what prompted me to look in this direction.
Think I'd better go and do some holiday reading on bialgebras.
Stelios Tsampas (Dec 24 2024 at 17:48):David Corfield said:
Think I'd better go and do some holiday reading on bialgebras.
I forgot to add one of my favorite papers on the topic:
M. Lenisa, J. Power, H. Watanabe: Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads (link)
I suggest this for your holiday reading. It gives a much more complete, bird's eye view on the kind of categories that bialgebras form. Distributive laws are, as expected, crucial.
John Baez (Dec 24 2024 at 19:06):David Corfield said:
Stelios Tsampas No, I'm just a philosopher (co-founder of the n-Category Cafe) whose department was closed, and who has been lucky enough to find some ARIA safeguarded AI funding.
Do you interact at all with the Oxford branch of the Topos Institute, who are apparently getting million from ARIA for "Double Categorical Systems Theory for Safeguarded AI"? The people who wrote this proposal are @David Jaz Myers, @Sophie Libkind and @Owen Lynch.
David Corfield (Dec 24 2024 at 22:17):I met all three in Berkeley last year and have spoken a bit with David Jaz. There's no doubt a way to bring what Stelios and I were discussing in a double categorical direction. Indeed, Grodin and Harper write:
In the pioneering works on amortized analysis, Sleator and Tarjan [28,25] describe the “move-to-front” paging algorithm and prove that it is competitive relative to any other algorithm. This argument, while also using amortization, does not immediately appear to fit into our coalgebraic framework. The potential is computed by comparing the move-to-front algorithm to another algorithm; we conjecture that the potential is behaving like a generalized bisimulation relation rather than a morphism. While we view amortized analysis as a directed simulation here (i.e., a morphism of coalgebras), we suspect that a double categorical approach may be valuable for understanding a symmetric generalization more akin to bisimulation. Cospans of coalgebras have been used to generalize bisimulations [27], which can serve as vertical morphisms to add to the bicategory of colax coalgebras. Additionally, Goncharov et al. [7] propose a double category of (co)lax coalgebras of a lax-double functor, generalizing from a fundamentally double categorical perspective.
John Baez (Dec 24 2024 at 22:44):Nice! Also, on a less technical level, it would be good for all category theorists getting paid by ARIA to develop safeguarded AI to talk a lot with each other - because those are three quite unusual things to have in common! You all have to deal with ARIA, you all like to talk about similar sorts of math, and I hope you're all eager to save the world from nasty AI.
Owen Lynch (Dec 25 2024 at 04:19):I'm not sure what the exact amount is, but I'm fairly sure it's not £10 million...
John Baez (Dec 25 2024 at 06:19):Okay, maybe dollars? I heard it somewhere....
David Jaz Myers (Dec 25 2024 at 17:04):We got under £1m for DCST this year. But Topos is looking towards further funding for using double categories in systems modelling and modelling software
John Baez (Dec 25 2024 at 19:24):Don't tell me I accidentally slipped an extra zero in there. Sorry, folks!
John Baez (Dec 25 2024 at 19:36):While I remove my foot from my mouth.... my main point was that I hope you can dream up an excuse to talk to @David Corfield about safeguarded AI, category theory... and many other things. Much good could come from this.
David Corfield (Dec 31 2024 at 12:45):I realise now that there people on Zulip I should have tagged whose papers I've mentioned: @Harrison Grodin, @Robert Harper, @Jon Sterling, @Tarmo Uustalu.
David Corfield (Dec 31 2024 at 12:56):There are plenty of good ideas in the slides of @Tarmo Uustalu that I mentioned:
David Corfield said:
Then the graded algebras for this graded monad are the things Uustalu is talking about in these slides.
His 'matching pair of actions' (slide 16) allows for a dual to the graded cost monad, which appears in
as a graded 'potential' type operator.
Tori Vollmer (Dec 31 2024 at 18:13):Stelios Tsampas said:
Either way, I have not encountered any definition of a distributive law/GSOS law of a graded monad over an endofunctor or a distributive law of an endofunctor over a graded monad. I expect one will be able to come up with a definition for either, but I wonder how strong the underlying commutativity conditions would be. They might even be unrealistic.
@David Corfield
Re a definition for distributive laws to do with a graded monad:
You can just look at the category of graded monads, similar to monads but with the added condition that you need to map the grade index as well. That is no so important because if you just look at endomorphisms in this category , say for some graded monad (better know as ), you should get things like where and The direction of is a bit arbitrary (as in you can define your category such that points the other way). From here, just playing around in that category should tell you everything you need to know about what distributive laws for graded monads are. (My gut tells me that distributive laws are just graded monads intenal to this category)