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.
dusko (Sep 13 2022 at 20:56):i updated this draft book on arxiv:
https://arxiv.org/abs/2208.03817
the TITLE CHANGED to:
Programs as Diagrams: From Categorical Computability to Computable Categories
i think i improved the text, not just the grammar but also the explanations. i am not a good writer, but i am doing my best. the story deserves it.
maybe i should mention that this string diagram approach evolved through teaching. it makes it possible to prepare students to study crypto within a term. the standard approach takes at least 3, in most places 4 terms of prerequisites.
the last two chapters are not for teaching, but the POINT of it all. while computability is normally presented as the Church-Turing equivalence of the various computer structures (abacus, turing machines, lambda calculus, etc), computability in a monoidal category becomes a property. and then the categories themselves become computable.
ok, i hate to advertise, but i keep coming back to advertise this not as my work, but as a law of nature.
Spencer Breiner (Sep 14 2022 at 00:52):I'm only ~2 1/2 chapters in, but I'm loving it! The pictures clarify some of the diagonalization that is hard to keep track of in substitution-based syntax. I am working with an undergrad at UMD this semester who will be tackling (part of) it.
dusko (Sep 15 2022 at 05:30):Spencer Breiner said:
I'm only ~2 1/2 chapters in, but I'm loving it! The pictures clarify some of the diagonalization that is hard to keep track of in substitution-based syntax. I am working with an undergrad at UMD this semester who will be tackling (part of) it.
nice! if it is useful, i can send a link to the version with exercises and background. and pointing me to the places where things are still not clear or don't come across would be great.
Simonas Tutlys (Sep 16 2022 at 06:41):Typos at the bottom of 12th page (stRict monoidal laws) and 11th (cartesian functionS can be paired).loving it so far as well-could be an intro this monoidality stuff for CS background people.I'm not graphically minded but this makes the diagrammatic stuff easy to understand
dusko (Sep 16 2022 at 08:49):thanks much! i appreciate this on any channel, but if anyone wants to reach me directly, it's dusko@hawaii.edu or dusko@dusko.org :)
Patrick Nicodemus (Sep 17 2022 at 20:22):Hi Dusko, I'm looking at it now.
At the beginning of section 1.2 you say "We assume that any type is equipped with such operations", i.e., in your category every object is a commutative comonoid in a canonoical way. Is this assumption meant to be enforced throughout the entire book? Where does this assumption apply?
https://ncatlab.org/nlab/show/cartesian+monoidal+category
Moreover, one can show (e.g. Fox 1976 or Heunen-Vicary 2012, p. 79 (p. 85 of the pdf)) that any symmetric monoidal category equipped with suitably well-behaved diagonals and augmentations must in fact be cartesian monoidal. More precisely: suppose C is a symmetric monoidal category equipped with monoidal natural transformations (...)
The paragraph I highlighted from the linked nlab page seems to suggest that any symmetric monoidal category where every object is a comonoid in a natural way is a Cartesian monoidal category. Later on that you will be considering both arbitrary maps and Cartesian maps (i.e. comonoid homomorphisms) between two objects. Now this seems to suggest that you are not actually working in a Cartesian monoidal category because every morphism between objects in a Cartesian monoidal category is always a comonoid homomorphism. There is some subtlety here, you are working in a category where every object has a comonoid structure but yet the category is not Cartesian monoidal, so maybe you could discuss which hypotheses of the theorems I mentioned are not satisfied.
Patrick Nicodemus (Sep 17 2022 at 20:31):There are no examples of categories given in the section titled "Categories." I would like to see a short list of the most representative examples of categories which are semantic models. What are you thinking of, the category of pointed sets, the category of dcpo's? What categories model the salient features of permitting nontotal functions or functions which are not single valued?
I understand that the book is meant to be accessible to undergraduate students and so the examples might complicate things. For example maybe the Kleisli category of the finite powerset monad is an example of a category which models nondeterministic computation but it would be unfair to expect undergraduate students to understand this comment. Perhaps you can mark the examples with a warning saying it's OK if this is not understood upon first read and one can come back to it later.
Patrick Nicodemus (Sep 17 2022 at 20:37):Similarly I think the book is made harder to read because it chooses to avoid some established terminology to avoid intimidating students. I understand that the phrase "morphism of comonoids" may be intimidating for students who are not familiar with the terminology but I find it more understandable to say "A Cartesian map is a map which is a morphism with respect to the canonical comonoid structure" than to say "A Cartesian map is a map which is both total and single valued." Again, I am not sure how to handle the issue of intimidating students with scary algebra terminology but you could say in a footnote / aside "Different books use different terminology. So-and-so would call our Cartesian maps a "morphism of comonoids". The book by XYZ refers to our program evaluators as "ABC's." "
dusko (Sep 18 2022 at 01:02):Patrick Nicodemus said:
Hi Dusko, I'm looking at it now.
At the beginning of section 1.2 you say "We assume that any type is equipped with such operations", i.e., in your category every object is a commutative comonoid in a canonoical way. Is this assumption meant to be enforced throughout the entire book? Where does this assumption apply?
https://ncatlab.org/nlab/show/cartesian+monoidal+category
Moreover, one can show (e.g. Fox 1976 or Heunen-Vicary 2012, p. 79 (p. 85 of the pdf)) that any symmetric monoidal category equipped with suitably well-behaved diagonals and augmentations must in fact be cartesian monoidal. More precisely: suppose C is a symmetric monoidal category equipped with monoidal natural transformations (...)
The paragraph I highlighted from the linked nlab page seems to suggest that any symmetric monoidal category where every object is a comonoid in a natural way is a Cartesian monoidal category.
Fox 1976 constructs the cofree cartesian category over a given symmetric monoidal. That is the category of abelian comonoids and comonoid homomorphisms. Heunen and Vicary surely mention somewhere that the hierarchy of categories of comonoids and of Frobenius algebras in monoidal categories with various kinds of homomorphisms was studied in detail in https://arxiv.org/abs/0904.1997
(unless they forgot to mention it :)))
Look at the monoidal category . Every set comes with various data services. One is inherited from the cartesian structure of . Moreover, for any set , any abelian group structure induces an additional data service in defined by whenever . See https://arxiv.org/abs/0812.2266. There are lots of data services in , supporting nondeterministic computation. And isn't a cartesian category.
It is a general phenomenon. In , the data services are provided by the bases (https://arxiv.org/abs/0810.0812) but the linear operators do not preserve the bases. The subcategory of the linear operators that are cartesian in the sense that they preserve the bases is the category of sets.
(Btw, why are you calling them "cartesian monoidal categories". Isn't cartesian structure always monoidal? I.e., are ther cartesian non-monoidal categories?)
The confusion probably stems from the "suitably well-behaved" part of the "suitably well-behaved diagonals and augmentations must in fact be cartesian monoidal". The natural diagonals and projections are a part of the standard definition of cartesian categories. I think I specifically define the cartesian functions to be those with respect to which the data services are natural. That is the cartesian subcategory, in which the programs live. The outputs of computation are deletable when they exist, and copiable when they are unique, so there are data services. But computations may not terminate, and they may not be deterministic, so the data services may not be natural with respect to the computations. There are lots of interesting "well-behaved" structures that are not natural, and many natural structures that are neither interesting nor "well-behaved".
But thank you for reading. While I don't think this is an error, I am sure that there are some to be found :)
Zhen Lin Low (Sep 18 2022 at 01:14):"Cartesian category" is (unfortunately) ambiguous and sometimes refers to categories with not only finite products but also finite limits.
dusko (Sep 18 2022 at 01:26):Zhen Lin Low said:
"Cartesian category" is (unfortunately) ambiguous and sometimes refers to categories with not only finite products but also finite limits.
oh my. is there anyone except peter freyd who used the term "cartesian" to include equalizers? Cartesius certainly didn't. even freyd i think used "cartesian" in the usual sense until a certain point. in any case, he would be the last person to say "call categories with products but no equalizers cartesian monoidal". should we use the word "monoidal" whenever we want to avoid the assumption that a category has equalizers?
Zhen Lin Low (Sep 18 2022 at 01:26):PTJ uses it throughout the Elephant...
dusko (Sep 18 2022 at 01:38):Patrick Nicodemus said:
Similarly I think the book is made harder to read because it chooses to avoid some established terminology to avoid intimidating students. I understand that the phrase "morphism of comonoids" may be intimidating for students who are not familiar with the terminology but I find it more understandable to say "A Cartesian map is a map which is a morphism with respect to the canonical comonoid structure" than to say "A Cartesian map is a map which is both total and single valued." Again, I am not sure how to handle the issue of intimidating students with scary algebra terminology but you could say in a footnote / aside "Different books use different terminology. So-and-so would call our Cartesian maps a "morphism of comonoids". The book by XYZ refers to our program evaluators as "ABC's." "
these are all completely fair points. they are not just a matter of who we talk to, but also of personal taste. it is well-documented that mine is not always good. but running from it is futile.
i tried to do some of the referencing that you are suggesting in the earlier versions. the cost of adding more words is that the text becomes longer. some people who would find it all easier to read with more references end up never touching it because it is too long, and trying to do to many things.
the way i see this book is that it is telling the story that absolutely needs to be told, and all i can do is my best to make it tolearbly readable for good writers, who will then produce better versions.
dusko (Sep 18 2022 at 01:41):Zhen Lin Low said:
PTJ uses it throughout the Elephant...
ah why did they remove the emoji where a nuclear bomb explodes out of my head?
dusko (Sep 18 2022 at 10:23):dusko said:
Zhen Lin Low said:
PTJ uses it throughout the Elephant...
ah why did they remove the emoji where a nuclear bomb explodes out of my head?
i think the reasoning behind calling pullbacks the "cartesian squares" was that they are the cartesian liftings with respect to the principal fibration. they are the slice-wise cartesian products. in a topos theory book, all structures should be slice-wise, shouldn't they? but if "cartesian" is a slice-wise concept, then "cartesian closed" should also be slice-wise, i.e. what used to be called locally closed cartesian closed. the old relatively closed cartesian categories should presumably be cartesian relatively closed. and it goes on... ("man gave name to all the animals" comes to mind. the Little Mo' McCoury version comes to my twisted mind :)))
Nathanael Arkor (Sep 18 2022 at 11:42):but if "cartesian" is a slice-wise concept, then "cartesian closed" should also be slice-wise, i.e. what used to be called locally closed cartesian closed.
This is something that particularly irritates me about the terminology in the Elephant. (Johnstone even acknowledges his terminology is inconsistent, but justifies it by saying the terminology "cartesian closed" is "well-established", entirely ignoring the fact that "cartesian" was also well-established for categories with finite products.)
John Baez (Sep 18 2022 at 12:47)::anguish:
Henry Story (Sep 23 2022 at 07:56):dusko said:
Spencer Breiner said:
I'm only ~2 1/2 chapters in, but I'm loving it! The pictures clarify some of the diagonalization that is hard to keep track of in substitution-based syntax. I am working with an undergrad at UMD this semester who will be tackling (part of) it.
nice! if it is useful, i can send a link to the version with exercises and background. and pointing me to the places where things are still not clear or don't come across would be great.
Over the past 5 years I have been growing to the underserstanding of the importance of symmetric monoidal categories, so I am enjoying this already (just read chapter 1). The examples are likely going to be much more accessible than those in Coeke's "Picturing Quantum Processes".
I guess my interest started when I found your Tracing the Man in the Middle in Monoidal Categories article some 5 years ago (which I should soon be able to really understand when I get through this book). Then finding that monoidal categories maps to RDF with the "Bicategories of relations" article, and recent work on the pi calculus, indicating that those should indeed be the right space to massively parallel systems like the Web... Also the non-maathematical introduction by Baez on monoidal categories linking them to open systems helped a lot. So now I know it's important and why I won't have trouble learning it :-).
Great introduction from examples to Symmetric Monoidal Categories by @johncarlosbaez : their use in electrical engineering, quantum theory, programming, logic, ecology and other *open* systems with some thoughts on the 3rd law of thermodynamics. https://www.youtube.com/watch?v=DAGJw7YBy8E&t=18s
- The 🐠 BabelFish (@bblfish)I am surprised that the arxiv has size limits on books (I read that in the thread somewhere). I would be happy if you could send me the link to the full version ( henry.story@bblfish.net ).
dusko (Sep 25 2022 at 01:41):Henry Story said:
I would be happy if you could send me the link to the full version ( henry.story@bblfish.net ).
done. comments appreciated
John van de Wetering (Sep 29 2022 at 15:26):@Henry Story I'm surprised you don't find the examples in Picturing Quantum Processes accessible. Is it because they rely on too much physics intuition?
Henry Story (Sep 29 2022 at 15:36):John van de Wetering said:
Henry Story I'm surprised you don't find the examples in Picturing Quantum Processes accessible. Is it because they rely on too much physics intuition?
Actually I think I read all the way up to chapter 3 or so without problem. But from time to time there are ties to quantum theory made - completely reasonable given the name of the book - which is teaching me something about quantum mechanics, rather than drawing on my knowledge of it.
Dusko's book on computing on the other hand, draws on knowledge from computing which I should know about, so that it is helping me build from something I know. (or fill in unavowable gaps in my knowledge).
Reading Dusko's book should give me a good basis to then later learn about quantum physics. :-)
Henry Story (Sep 29 2022 at 15:54):But the "Picturing quantum Processes" book was particularly useful in that it makes really clear the relation of symmetric monoidal categories to quantum mechanics.
This reminds me: It was whispered in my ear that some think Carl Hewitt the author of the Actor model was going crazy with age. Reading his 2012 article "Actor Model of Computation: Scalable Robust information Systems" I think I can guess where the suspicion could come from. He writes:
• The Actor Model is founded on physics whereas the π–calculus is founded
on algebra.
• Semantics of the Actor Model is based on message orderings in the
Computational Representation Theorem. Semantics of the π–calculus is based on structural congruence in various kinds of bi-simulations and equivalences.
and
The Actor Model was inspired by the laws of physics and depends on them for its fundamental axioms in contrast with the process calculi being inspired by algebra [Milner 1993].
But it looks like recent work discussed here on Zulip on the pi-calculus does bring in symmetric monoidal categories into the mix. So perhaps Hewitt's intuitions were right all along...
https://twitter.com/bblfish/status/1567089378010304514
2018 paper comparing two different game semantics approaches to the non-deterministic lambda calculus and the pi calculus using string diagrams and showing how they come together. https://twitter.com/bblfish/status/1567089378010304514/photo/1
- The 🐠 BabelFish (@bblfish) dusko (Sep 30 2022 at 21:24):Henry Story said:
John van de Wetering said:
Henry Story I'm surprised you don't find the examples in Picturing Quantum Processes accessible. Is it because they rely on too much physics intuition?
Actually I think I read all the way up to chapter 3 or so without problem. But from time to time there are ties to quantum theory made - completely reasonable given the name of the book - which is teaching me something about quantum mechanics, rather than drawing on my knowledge of it.
Dusko's book on computing on the other hand, draws on knowledge from computing which I should know about, so that it is helping me build from something I know. (or fill in unavowable gaps in my knowledge).Reading Dusko's book should give me a good basis to then later learn about quantum physics. :-)
the only objective way to compare the two is to say that the author of one of the books is much better looking than the first author of the other one. beyond that, everything else is a matter of taste. and even that changes when the first author of the other book is considered with a guitar.
dusko (Sep 30 2022 at 21:45):Henry Story said:
But the "Picturing quantum Processes" book was particularly useful in that it makes really clear the relation of symmetric monoidal categories to quantum mechanics.
This reminds me: It was whispered in my ear that some think Carl Hewitt the author of the Actor model was going crazy with age. Reading his 2012 article "Actor Model of Computation: Scalable Robust information Systems" I think I can guess where the suspicion could come from. He writes:
• The Actor Model is founded on physics whereas the π–calculus is founded
on algebra.
• Semantics of the Actor Model is based on message orderings in the
Computational Representation Theorem. Semantics of the π–calculus is based on structural congruence in various kinds of bi-simulations and equivalences.and
The Actor Model was inspired by the laws of physics and depends on them for its fundamental axioms in contrast with the process calculi being inspired by algebra [Milner 1993].
But it looks like recent work discussed here on Zulip on the pi-calculus does bring in symmetric monoidal categories into the mix.
the person who brought symmetric monoidal categories into the mix with the pi-calculus was robin milner, sometime in the 90s. he first developed action calculus which was sort of an algebraic/coalgebraic framework for specifying process calculi where messages can create and shut channels (the first of which was the pi-calculus), and then formalized it in fully monoidal framework, with john power... was it called action structures? forgetting things is not too bad if it makes room for inventing something else.
re the physics roots, maybe carl hewitt was inspired by the fact that carl-adam petri was definitely talking about physics when he presented the petri nets. in almost every paper. but programmers want to program processes, and few people besides petri himself interpreted petri nets as physical systems.
the physics of aging is that the amount of time behind you is getting bigger whereas the amount of time in front of you is getting smaller. that disturbs the symmetry of hawking's question "why is it that we don't remember future the same way we remember past?" as you age, the amount of stuff that you forgot surpasses the amount of stuff that you will every learn. it can happen halfway if you don't pay attention. some people give up on the future and start pumping up the past. if you let them, they blow up both.
dusko (Sep 30 2022 at 21:56):dusko said:
but programmers want to program processes, and few people besides petri himself interpreted petri nets as physical systems.
this is also not completely true. i think samson had a paper about petri nets as physical systems. and i am probably unaware of most petri net research. and also of most of physics :)) so i shouldn't have said that.
John Baez (Nov 24 2022 at 13:57):(Btw, why are you calling them "cartesian monoidal categories". Isn't cartesian structure always monoidal? I.e., are ther cartesian non-monoidal categories?)
I'm not sure anyone gave the answer to this that I'd give. There are two subtly different but roughly equivalent notions:
To get from the former to the latter we have to choose a terminal object and a specific cartesian product for each pair of objects. We might do this using the axiom of choice, for example.
The latter is called a cartesian monoidal category.
John Baez (Nov 24 2022 at 14:00):As most people here know, there are a couple of nice ways to characterize which monoidal categories are cartesian without saying the word "cartesian product". They are described here.
dusko (Jan 25 2023 at 11:23):John Baez said:
(Btw, why are you calling them "cartesian monoidal categories". Isn't cartesian structure always monoidal? I.e., are ther cartesian non-monoidal categories?)
I'm not sure anyone gave the answer to this that I'd give. There are two subtly different but roughly equivalent notions:
- a category with finite products
- a monoidal category where the tensor product is the cartesian product and the unit object is terminal
To get from the former to the latter we have to choose a terminal object and a specific cartesian product for each pair of objects. We might do this using the axiom of choice, for example.
The latter is called a cartesian monoidal category.
thanks for explaining this, john.
a couple of people responded this earlier, but differently. they said that the difference between cartesian and cartesian monoidal was that cartesian categories have all finite limits. (back in the 90s, there was precisely one person who used the term in that sense: peter freyd. apparently ptj also adopted it in the elephants, to keep all structures slicewise as they are in toposes. but then the cartesian closed structure is also slicewise and becomes what used to be called locally cartesian closed and all hell breaks loose...)
now you go back to cartesian = existence of finite products (a property) and cartesian monoidal = choice of finite product functors (a structure). fair enough. the idea that we should signal whenever we use the AC to pick representatives of a universal construction is something that many of us would subscribe to.
an equivalence of categories is a functor that is full and faithful and essentially surjective. it is also a pair of adjoint functors where the unit and the counit are invertible. getting from one to the other requires that we choose representatives of the equivalence classes along the essential surjection and prove a lemma. should we distinguish the two notions of equivalence? it might be ok.
but the thread goes deeper into the sweater.
in cartesian closed categories, the finite product functors have right adjoints. so the 50 years of books and papers about cartesian closed categories were not about cartesian categories but about cartesian monoidal closed categories. to talk about cartesian closed categories, we should never say "functor" only that this and that is representable.
on the other hand, in cartesian monoidal closed categories, presumably not only the products but also the exponents should be chosen as functors. maclane worked out the coherences for the closed structure and found pairs of non-canonical isomorphisms. very clumsy to carry around. did he even state it as a failure of coherence? but they arise from using universal constructions in different orders. so if the closure is treated as a property, whenever you encounter the noncoherence, the construction tells you which of the isomorphisms you are using. someone at the time claimed that this was necessary when working with triangulations...
should we somehow signal that the cartesian monoidal structure in cartesian monoidal closed categories is chosen structure, but that its closure is not cartesian monoidal but only cartesian, since it is treated as a property (representability of some functors)?
god probably invented math when he was fed up with giving things names. naming things can get risky. that is why the lambda-calculus people say that the world is modulo the alpha-conversion :))
Fabrizio Genovese (Jan 25 2023 at 13:33):For me it's a matter of perspective. 'Cartesian monoidal category' is not telling me something more about a 'Cartesian category', but something more about a 'monoidal category'. Simply put, if I'm working with a monoidal category and you tell me 'oh, actually this is cartesian monoidal' then I know I get natural copy and delete for free on every object.
Fabrizio Genovese (Jan 25 2023 at 13:34):So, in this sense, I find it like a useful notation for people working heavily with monoidal categories. This is especially important in categorical quantum mechanics, as having copy and delete around is usually taken to signify that whatever you are dealing with behaves classically :grinning:
Tobias Fritz (Jan 25 2023 at 14:07):Along similar lines, I think that it's usually good practice if phrases like "gobbledygook category" specify a 2-category of such categories. In other words, every such term comes with a canonical notion of functor between them. For cartesian categories, I would think that the canonical notion of functor is just a plain functor; while for cartesian monoidal categories, I would think that you actually want to consider them as monoidal categories, so the relevant functors are strong monoidal functors.
Nathanael Arkor (Jan 25 2023 at 14:21):For cartesian categories, I would think that the canonical notion of functor is just a plain functor
The appropriate notion of functor is one that preserves finite products.
Mike Shulman (Jan 25 2023 at 14:34):For most kinds of structured category, there are three different kinds of "appropriate" morphism between them: lax, colax, and strong/pseudo. For cartesian categories, the colax morphisms are arbitrary functors (abstractly this is because the monad for cartesian structure is "colax-idempotent"), while the lax and strong morphisms are product-preserving functors.
Tobias Fritz (Jan 25 2023 at 16:09):Nathanael Arkor said:
For cartesian categories, I would think that the canonical notion of functor is just a plain functor
The appropriate notion of functor is one that preserves finite products.
That's certainly true in many situations, but it seems like an overly restrictive moral provision to me. For example, it already precludes considering functors of the form as functors between cartesian categories (on sufficiently nontrivial cartesian categories that is).
But yes, I should weaken my claim a bit and just say that "cartesian monoidal category" makes it clear that you consider the category under consideration explicitly as a monoidal category. When you merely say "cartesian category", then it doesn't have that connotation; and if somewhere else you use the term "monoidal category" to refer to the same category, then I will not assume that the monoidal structure is the cartesian one. In both cases, there are several natural choices of functor, and the terminology can also be used to reflect which one you have in mind.