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.
Alex Kreitzberg (Mar 20 2025 at 17:57):After asking a bunch of questions, I convinced myself that if a category is freely generated by a graph of computable arrows, whose compositions were also computable, then the generated category itself is computable.
Although I may have messed something up in that line of thought, it clarified I had a more general question.
In general how do we show a given category is "computable"? I'm vaguely aware that there are certain Toposes that are built specifically to be computable foundations of mathematics, but I'm also curious - can we explore computability in more modest categories?
Nathanael Arkor (Mar 20 2025 at 18:29):What does it mean for an arrow to be "computable"? What does it mean for a category to be "computable"?
Ryan Wisnesky (Mar 20 2025 at 18:37):One may ask if a finite presentation of a category, considered as an equational theory, is decidable. Turns out presentations without equations, which denote free categories, are decidable. One may also ask if various constructions on categories are computable, for example, checking if two presentations are equivalent (turns out this one isn't computable in general). There's a lot of related work on computability for finitely presented groups that transfers to finitely presented categories. Check out "the word problem for groups" for more. The CQL software (categoricaldata.net) creates decision procedures for finite presentations of categories internally to do pretty much anything interesting with categories.
Alex Kreitzberg (Mar 20 2025 at 18:43):Thank you! Maybe this follow up question is too broad, can you ask similar questions about categories that you know aren't finitely presentable?
It just occured to me that "computable" = "constructable" in my intuition, that's probably a really bad error.
Aren't certain Topos models of constructive mathematics? Is such a Topos necessarily finitely presentable?
Alex Kreitzberg (Mar 20 2025 at 18:50):Gosh I just found this in the article [[Topos]]
Any result in ordinary mathematics whose proof is finitist and constructive automatically holds in any topos. If one removes the restriction that the proof be finitist, then the result holds in any topos with a natural numbers object.
I guess my follow up question is does this mean you can always represent a Topos on a computer, or am I conflating constructability with computability?
Alex Kreitzberg (Mar 20 2025 at 18:53):(where constructable just means the usual we're not allowed to use the law of the excluded middle etc.)
Ryan Wisnesky (Mar 20 2025 at 18:59):Most categories are infinite - have infinitely many morphisms, infinitely many objects, etc - so to represent them on a computer you need some kind of encoding. Use of "presentations" is one encoding, but there are others ("Godel numbering" for example). I usually think of an elementary topos as the same thing as a Henkin model of higher order logic, so to me that claim you cite is saying that finitist constructive proofs will tend to be expressible in higher order logics, which is true - there are many proof assistants for higher order logic in which you can formalize most math, constructive or otherwise.
Ryan Wisnesky (Mar 20 2025 at 19:00):Take a look at the "effective topos" and "realizability topos" for topoi that are built from computable functions, rather than arbitrary functions; these make great models of various programming languages
Alex Kreitzberg (Mar 20 2025 at 19:05):Thank you, this is a great answer.
You partially answered this already, but do you have references for learning various ways to encode simple abstract categories, or do you think it's a good idea to invest more/most energy in understanding finitely presentable categories?
Ryan Wisnesky (Mar 20 2025 at 19:12):I'm actually only aware of three ways to encode infinite algebraic structures on a computer: Godel numbering (to be avoided if possible, it's very low level), deep embeddings (corresponding to the presentation approach), and shallow embeddings, where you might for example represent a specific cartesian closed category using another one such as the simply typed lambda calculus. CQL (or any computer algebra system, such as Mathematica) is a good representative of the deep approach; the category theory library in Haskell or Coq would be an example of the shallow approach. Certainly, if your goal is to do computational category theory, you should think carefully about the three approaches, as they have different trade-offs, but I'm not aware of say a survey paper about the topic... I'll look for one. There's stuff like this: https://decomposition.al/blog/2015/06/02/embedding-deep-and-shallow/ and https://proofassistants.stackexchange.com/questions/2499/what-is-a-deep-embedding-vs-a-shallow-embedding-with-examples
Alex Kreitzberg (Mar 20 2025 at 19:19):Wonderful answer thank you! You've clarified for me that I've been trying to understand that I'm thinking about finite presentations for months now :laughter_tears:
I really appreciate your answers thank you!
Alex Kreitzberg (Mar 20 2025 at 19:20):(I will, of course, take all of these representations seriously)
Notification Bot (Mar 20 2025 at 19:33):Alex Kreitzberg has marked this topic as resolved.