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.
Martin (Aug 13 2024 at 12:03):I'm working on complexity theory for databases, which is what led me to ACT: I'm trying to see whether category theory can say something interesting about my problems.
There is a notion of dynamic complexity formulated by Immermann and Patnaik. Essentially, for a relational database that is subject to change, auxiliary relations are maintained in another database over the same domain with the intention to help answering a query. When an update to the database (for simplicity, an insertion or deletion of a tuple) occurs, every auxiliary relation is updated through a first-order query that can refer to the database as well as to the auxiliary relations. The typical example is maintaining an st- graph (say, representing users of a social network who follow and unfollow one another over time) and trying to answer the query "is t reachable from s"?
The class of all queries maintainable in this way with first-order update formulas, is called Dyn-FO.
The actual formalization can be a bit finicky: see e.g. the introductory sections of this survey for one approach.
I believe this complexity class may admit a good categorical interpretation, and this would allow questions like the inexpressibility of certain problems within this class to be formulated and perhaps answered via sheaf theory and such, but I don't yet see how to carry this out. Am I barking up the wrong tree?
Emilio Minichiello (Aug 13 2024 at 12:53):This is the kind of question I am very interested in! I’ve been studying categorical database theory, but have been learning some complexity theory lately. Feel free to DM me
Emilio Minichiello (Aug 13 2024 at 13:31):Some possibly related work that may be of some interest:
babu (Mar 10 2025 at 17:18):Hi! I am reading about CQL and a point I keep coming across is that CQL checks for data integrity at compile time using automated theorem provers. How exactly does this work and what are these provers?
Ryan Wisnesky (Mar 10 2025 at 17:29):The document https://arxiv.org/abs/1503.03571 describes how CQL is implemented in terms functional programmers would understand, but the basic idea is that CQL is pluggable: it can use any theorem prover to accomplish its tasks, and we have implemented both our own provers and use open-source ones such as E and Vampire and Egglog. The need to check functoriality abounds in computational category theory; if people write what they think is a functor, that needs to be check to actually be a functor; not all assignments of objects to objects and morphisms to morphisms that people can write down actually define functors. But this functoriality check is undecidable, because categories can represent so many kinds of algebraic structure. Hence, CQL uses a theorem prover to tackle this undecidable problem as best it can
Ryan Wisnesky (Mar 10 2025 at 17:31):to elaborate a little bit, if you can decide the "word problem" (entailment) associated to a presentation of a category, then you can do pretty much anything with that category on a computer; but if you can't do that, then it is really hard (But not impossible) to get a computer to manipulate your category. So every category input into CQL has an associated decision procedure constructed for it (which fails sometimes dues to undecidability, but not usually on real world examples)
Ryan Wisnesky (Mar 10 2025 at 17:34):oh, and of course, in the context of co-pre-sheaves (categorical databases) functoriality of a functor C->Set indicates adherence to the "data integrity constraints" of C, that's how data integrity comes in
babu (Mar 10 2025 at 17:53):thank you so much! it is very interesting, I'll take a look