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.
(=_=) (May 29 2020 at 04:16):Peter Arndt said:
Hi, I did a PhD in motivic homotopy theory, but have been skipping around Homotopy type theory, non-classical propositional logics, the outskirts of number theory, like quadratic forms and the field with one element. [...] I want to learn about Topological Data Analysis, and all kinds of applications of category theory in computer science. Especially if they are AI or data science related. I don't think many people in my department know what a category is, so I am grateful for story lines that start in very concrete computer science situations and lead naturally and/or successfully to category theory...
Hi Peter! I have similar mathematical interests and have been rediscovering the joy of recently. For AI-related category theory, I think what got me really excited was this paper (the link is to arXiv: the paper appeared in LICS19, but this is the longer version) by Brendan Fong, David Spivak and Rémy Tuyéras, which sparked a flurry of work that's still in progress. The locus of ideas behind that is reviewed in this piece by Jules Hedges, who's working with Bruno Gavranovic and many others to extend the framework of Fong et al. to eventually cover most neural network architectures. It's a great time to be here.
Peter Arndt (May 29 2020 at 10:17):Cool, hi! The Backprop paper is on my reading list, but Corona teaching is eating up my time. Thanks for the second link, i hadn't heard about lenses, but I guess I will...
(=_=) (May 29 2020 at 12:52):Peter Arndt said:
I am grateful for story lines that start in very concrete computer science situations and lead naturally and/or successfully to category theory...
There's been a lot of category theory done in computer science, but mostly in the programming language community. I had a look at the programming language team at Düsseldorf, but it seems like they're more interested in working with Prolog, so no luck there.
There's actually a story that's adjacent to your interest in HoTT: container/polynomial functors, defined by Abbott et al. using Martin-Löf type theory to support generic programming in a dependently typed language, and then brought back to category theory by Joachim Kock and others.
Jacques Carette (May 29 2020 at 13:00):The specification language community, which is entirely separate from the PL community (it's complicated, don't ask) has also been using category theory for a long time. Their use of cospans for doing architecture diagram wiring goes back at least 20 years, for example. Then there's a huge cottage industry of people doing rewriting via double-pushout formulations. The models people (you can blame Zinovy Diskin and Tom Maibaum there) have also started to really get categorical.
(=_=) (May 29 2020 at 13:08):Jacques Carette said:
The specification language community, which is entirely separate from the PL community (it's complicated, don't ask) has also been using category theory for a long time. Their use of cospans for doing architecture diagram wiring goes back at least 20 years, for example. Then there's a huge cottage industry of people doing rewriting via double-pushout formulations. The models people (you can blame Zinovy Diskin and Tom Maibaum there) have also started to really get categorical.
Good to know. I was more interested in looking at the group that's at Peter Arndt's institution, which is this one. I'm not really familiar with the work of the specification language community, so I didn't know how to see if they're using category theory in their research.
Jacques Carette (May 29 2020 at 13:11):They're probably anti-category-theorists. B and Event-B are very firmly attached to set theory, and that's what this lab mostly works on.
(=_=) (May 29 2020 at 13:12):Jacques Carette said:
They're probably anti-category-theorists. B and Event-B are very firmly attached to set theory, and that's what this lab mostly works on.
Ah, that might explain why Peter said nobody in his department seems to know category theory. Oh well. :shrug:
(=_=) (May 29 2020 at 13:22):Peter Arndt said:
I am not much of a computer scientist yet, but I am trying to become a valuable member of my department (or at least not the lamest duck) - so I want to learn about Topological Data Analysis, and all kinds of applications of category theory in computer science.
So I had another look at the presentation of your team, and it seems they're interested in NLP. So stuff to do with string diagrams may be helpful: Bob Coecke and others have been using "categorical quantum mechanics" (CQM) to do semantics and "QNLP". Valeria de Paiva is also a research scientist working on NLP in the industry, as well as having developed the theory of Dialectica categories.
Peter Arndt (May 29 2020 at 15:50):Wow, cool, a whole thread on what I am looking for. And thanks for this very specific help tailored to my situation!
QNLP might really be a thing for me - I will look into it!
In general, researchwise, I don't have to do what the others at the department are doing, although it would of course be nice not to sit alone on my connected component. But realistically I will mostly be teaching in the next time, and ideally I would like to teach stuff that gets me into possible research directions. I think I have quite some freedom to offer courses about anything AI-related that is sufficiently applied. And I can also come up with other CS-related courses, but I may have to justify if I want to teach courses containing CT, and concrete applications are the most convincing, I guess...
Since I like topos theory: Is domain theory still a thing that people work on? And specifically synthetic domain theory?
Peter Arndt (May 29 2020 at 15:55):Jacques Carette said:
The specification language community, which is entirely separate from the PL community (it's complicated, don't ask) has also been using category theory for a long time. Their use of cospans for doing architecture diagram wiring goes back at least 20 years, for example. Then there's a huge cottage industry of people doing rewriting via double-pushout formulations. The models people (you can blame Zinovy Diskin and Tom Maibaum there) have also started to really get categorical.
Sounds cool! This connects to my propositional logic interests, I think. Would you know where to start reading on specification languages?
Joshua Grochow (May 29 2020 at 17:07):A couple references:
Kyle Raftogianis (May 29 2020 at 18:02):David Spivak also has some cool stuff on modeling structured data with category theory. For example, in Functorial Data Migration, a SQL database is a functor from a "schema category" to the category of sets, and then you can talk about queries and transforming data by moving between these schema categories! Might be related to data science and maybe AI
Jacques Carette (May 29 2020 at 19:32):@Peter Arndt you could certainly start with the pre-history:
Goguen's 1991 Categorical Manifesto https://ncatlab.org/nlab/show/A+Categorical+Manifesto had a lot of influence
Going more modern:
the modern avatar of CASL is Hets - http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/src-distribution/versions/Hets/docs/ which is very categorical
Personally, I'm a big fan of using dependently typed theorem provers to work with category theory, so I like
Valeria de Paiva (May 29 2020 at 20:00):Jacques Carette said:
Peter Arndt you could certainly start with the pre-history:
[...]
Personally, I'm a big fan of using dependently typed theorem provers to work with category theory, so I like
- Agda - https://wiki.portal.chalmers.se/agda/pmwiki.php ; there are Agda people 'not too far' from you.
- but I'm biased... - https://github.com/agda/agda-categories
hmm, we're all biased, but my early history has many more other projects like:
CONM/092 Categories in Computer Science and Logic - John W. Gray and Andre Scedrov, Editors https://www.ams.org/books/conm/092/
the sequence of meeting CTCS (Categories in Computer Science)
https://dblp.org/db/conf/ctcs/index.html
the two European projects CLiCS (Categorical Logic in Computer Science)
https://cordis.europa.eu/project/id/1668
Applied Semantics APPSEM https://books.google.com/books?id=KbBqCQAAQBAJ&dq=application+of+semantics+APPSEM&source=gbs_navlinks_s
and APPSEM 2: https://www2.le.ac.uk/departments/informatics/research/projects/appsemii
All th TYPES projects and Working Groups use Category Theory for Computer Science
Jacques Carette (May 29 2020 at 20:49):Never claimed that my list was exhaustive - just a rough sample between Google and my memory. I'm glad that my incompleteness caused you to add to it... :laughing:
Peter Arndt (May 29 2020 at 23:56):Thanks a lot, Jacques and Valeria! I have spent hours following your links! Gotta get back to work, but there is a lot to take with me here.
Valeria de Paiva (May 30 2020 at 03:15):Peter Arndt said:
Thanks a lot, Jacques and Valeria! I have spent hours following your links! Gotta get back to work, but there is a lot to take with me here.
you're welcome, Peter! I was reacting to the idea that we need to preserve the old histories because the digital ones are sometimes harder to preserve than the printed ones--like the examples of PSSLs, Hypatia and the categories mailing list archives discussed in other channels here show. But I am sure that there are plenty of other nice examples of connections between CT and logic programming that I don't know much about.
(=_=) (May 30 2020 at 08:06):Peter Arndt said:
Since I like topos theory: Is domain theory still a thing that people work on? And specifically synthetic domain theory?
There's #theory: topos theory if you want to find the topos theorists here.
sarahzrf (Jun 04 2020 at 21:08):Peter Arndt said:
Since I like topos theory: Is domain theory still a thing that people work on? And specifically synthetic domain theory?
oh man ive been linking this paper a lot lately but check this out https://arxiv.org/abs/1208.3596
sarahzrf (Jun 04 2020 at 21:09):i dunno if i can tell you whether "people" work on domain theory but i know that i think it's pretty cool :halo:
Dan Doel (Jun 04 2020 at 21:19):Paul Taylor, at least, moved from synthetic domain theory to "abstract stone duality" I think. And I suppose I'm not sure if he still works on that, but I think it's newer than his work on synthetic domain theory, for people looking for 'new' stuff to look at. (I'm also not sure why he didn't call it 'synthetic stone duality.')