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.
Gabriel Goren Roig (Apr 05 2020 at 17:02):Lately I've been learning about computability/recursion theory, and how it relates to propositional and first-order logic. I'm also aware that there are connections between computational complexity and logic, more specifically the theory of finite models of variants of first- and second-order logic (such as Fagin's theorem: "the set of all properties expressible in existential second-order logic is precisely the complexity class NP").
I know nothing about categorical logic, but given that I'm loving everything I learn about logic, I'm interested in learning about it too. My question is: can I expect these links with complexity and computability to be approachable or at least expressible from the point of view of categorical logic? Or is the latter about completely different stuff?
Nathanael Arkor (Apr 05 2020 at 17:36):I think categorical descriptive complexity is very much a new area of research: as far as I'm aware, The pebbling comonad in finite model theory (https://arxiv.org/abs/1704.05124) is one of the first forays into the area
Nathanael Arkor (Apr 05 2020 at 17:36):so this is very much an open question
Matteo Capucci (he/him) (Apr 05 2020 at 17:44):Yes, it's the Saint Graal of categorical computability
Matteo Capucci (he/him) (Apr 05 2020 at 17:44):I know the group studying Turing categories is trying to develop some complexity theory in that framework, but it's been a long time since I last checked the progress
Jules Hedges (Apr 05 2020 at 18:51):Yes, I think this is almost entirely an open question, that quite a lot of people are interested in. There's the Canadian approach with Turing categories, and there's a rival approach by Dusko Pavlovic, the "monoidal computer"
Fabrizio Genovese (Apr 05 2020 at 19:06):Capturing complexity theory categorically is really, really hard. I am not familiar with Turing categories but I am not a fan of the monoidal computer approach. It feels like complexity concepts have been translated to category theory, but in a way that does not give any categorical insight on what is happening. I see no clear advantage coming from using categories in that approach. This said, the question may even be unsolvable by state-of-the-art CT. Complexity theory is highly non-compositional, and we are not able to answer even many super basic questions in complexity, nor to say much about the complexity of an algorithm looking at its parts. Given that these are the circumstances, and that (A)CT amounts to be the study of compositionality, at the moment I see very little room for categorical techniques in complexity
Fabrizio Genovese (Apr 05 2020 at 19:07):That's a field with very few low hanging fruits and we really need a big breakthrough to make progress there, imho.
Joachim Kock (Apr 05 2020 at 19:10):Jules Hedges said:
Yes, I think this is almost entirely an open question
Closed questions are so 20th Century.
James Wood (Apr 05 2020 at 20:31):Fabrizio Genovese said:
Complexity theory is highly non-compositional
I feel that there's some truth to this, but people have managed to make type systems which capture exactly the polynomial-time algorithms, which suggests some basic level of compositionality.
Fabrizio Genovese (Apr 05 2020 at 21:45):Yes, it's very difficult to say if this means "really non-compositional" or "compositional, but in a way we are in no way close to grasp at the moment"
sarahzrf (Apr 06 2020 at 02:02):a little bit tangential, but ive wondered before whether itd be possible to do like
sarahzrf (Apr 06 2020 at 02:02):"synthetic complexity theory"
sarahzrf (Apr 06 2020 at 02:02):in some kind of radically intensional setting
sarahzrf (Apr 06 2020 at 02:03):where you can prove that two functions agree at all points, but you can also prove that they're non-equal, because they have different time complexities
Gabriel Goren Roig (Apr 06 2020 at 04:06):Thank you for all these very interesting answers! Based on them, I will try to turn the question around (or rather, focus on the last part of my original question).
If describing complexity classes from a categorical perspective is hard and an open question, then I expect categorical logic to be about completely different stuff. That is, I expect it would be hard to capture categorically the aspects of traditional logic that have more or less clear correspondences with complexity classes. So, from that perspective, what is it that categorical logic is about, instead of those that? Maybe categorical logic is more about proof theory than about models, or something like that?
(This is a super vague question and I feel that, therefore, it might be very hard to answer)
Matteo Capucci (he/him) (Apr 06 2020 at 07:41):It's also likely CT alone cannot capture complexity theory, and that we'll need more of an hybrid approach
Matteo Capucci (he/him) (Apr 06 2020 at 07:41):I'm each day more convinced this is the answer to many applications
Jules Hedges (Apr 06 2020 at 09:38):@Gabriel Goren Yes, categorical logic is kind of more about proofs than models, and it tends to be about logics that are much, much stronger than the ones that are used in descriptive complexity, in particular they tend to be higher order logics. It's not my field, but I'd say that the 2 main branches of categorical logic are (1) the study of internal logic of toposes, which is higher order intuitionistic logic, and (2) the other sort that has lots of fibrations in it, which builds up to intuitionistic type theory
Nathanael Arkor (Apr 06 2020 at 11:53):Maybe categorical logic is more about proof theory than about models, or something like that?
my understanding is that descriptive complexity theory is a branch of finite model theory, and finite model theory in particular has not been tackled in category theory to a significant extent
Nathanael Arkor (Apr 06 2020 at 11:54):though from what I've seen, there are a number of results in finite model theory that look like they could have a category theoretic flavour, if finite model theorists decided that was useful
Bob Atkey (Apr 06 2020 at 13:45):The field of Implicit computational complexity is concerned with finding programing languages / proof systems such that execution or cut-reduction lies in some complexity class. This is often done directly on the syntax, but there is some work by Martin Hofmann and Ugo Dal Lago that works towards using categorical definitions, though not quite getting to the level of having an axiomatic presentation in CT. See, for instance, their paper "Realizability models and implicit complexity" https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/publikationen-pdfs/j32-RealizabilityModelsImplicitComplexity.pdf which considers various extensions of SMCCs with modalities that capture elementary and polynomial time.
Bob Atkey (Apr 06 2020 at 13:45):I've been working on extending this work to dependent types.
Gershom (Apr 06 2020 at 20:15):There is interesting and suggestive work on _algebraic topology_ and complexity theory https://arxiv.org/pdf/1701.02302.pdf
Jules Hedges (Apr 06 2020 at 20:18):Wow!!
Jules Hedges (Apr 06 2020 at 20:21):As a total outsider to both AT and complexity theory, it's easy and fun to daydream about the big conjectures being solved with some crazy topological machinery
Fabrizio Genovese (Apr 06 2020 at 20:41):Gershom said:
There is interesting and suggestive work on _algebraic topology_ and complexity theory https://arxiv.org/pdf/1701.02302.pdf
Woa, the idea seems really interesting