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.
Julius (Jul 22 2023 at 14:43):Curious if there’s a dense, pure definition of category theoretic objects as a tight, rigorous language - could be like an extended Bacchus Naur Form description of category theory, axiomatically / as a formal language?
I’m personally try to make sure I have some basic definitions solidified. Seven Sketches of Compositionality, the book I’m working with, does not provide definitions of sets or logical concepts, beyond “a collection of things”.
But my early attempt would be something like this (maybe to come, in Python).
We could take the Python set object as the mathematical concept of a set. To add structure we can define new classes.
What might a list of definitions look like?
We probably need products and subsets next?
Products are tuples in Python.
A subset is a set, the parent / superset set, and the “subset function” that tests the truth condition “is subset”: so its signature is actually a triple, A, B, f. Right? def subset(A, B): condition = False; for element in B: if element not in A: condition = False; return condition
I imagine there’s a more pythonic way using a list processing method like a map or filter or something.
And then? I’ll see what is needed next. I know a relation is actually a subset of a product set. A function is a relation with a certain condition expressed in logical quantifiers, I think? two sets A B, for each b in B, there exists one and only one a in A such that the tuple in the subset of the product set of A and B has b in second place.
So we skipped over sets and logic, but it doesn’t matter since we already roughly have it in Python. We define a preorder as a binary relation which is reflexive and transitive. Like subsets, perhaps, all concepts can be defined as a signature of objects and functions they have to pass - their conditions?
Morgan Rogers (he/him) (Jul 22 2023 at 17:06):Are you asking whether there exists a Python implementation of categories? In any case, you might be interested in the book Category theory for computer science if you're interested in how categories are both conceptually and practically useful in CS. Or if you just want a formal mathematical definition, pick up any mathematically oriented book on the subject.
Ryan Wisnesky (Jul 22 2023 at 17:42):Yes: you can axiomatize the theory of a category using "regular logic" (existential Horn clauses); we have for example done this in CQL. You can also also axiomatize categories more directly using first-order logic with dependent sorts (https://ncatlab.org/nlab/show/FOLDS). Finally, there are many python implementations of category theory; here's one: https://www.philipzucker.com/computational-category-theory-in-python-i-dictionaries-for-finset/ . However, the biggest category theory libraries are in e.g. Coq, Agda, Lean, etc.
David Egolf (Jul 22 2023 at 17:54):Specifically regarding the topic of "what is a set?", looking at a book on set theory would be one way to get more detail. I have not read this book, but "Naive Set Theory" by Halmos looks like it might be a reasonable starting point.
Interestingly, the very start of that book says this:
One thing that the development will not include is a definition of sets. The situation is analogous to the familiar axiomatic approach to elementary geometry. That approach does not offer a definition of points and lines; instead it describes what it is that one can do with those objects.
For example, the author then goes on to talk about how sets can "have elements", and how sets can "be equal", and that the axiom of extensionality says that two sets are equal exactly when they have all the same elements. So, one can begin to work with sets without really defining what a set itself is.
Nico Beck (Jul 28 2023 at 10:48):Julius said:
Curious if there’s a dense, pure definition of category theoretic objects as a tight, rigorous language - could be like an extended Bacchus Naur Form description of category theory, axiomatically / as a formal language?
I’m personally try to make sure I have some basic definitions solidified. Seven Sketches of Compositionality, the book I’m working with, does not provide definitions of sets or logical concepts, beyond “a collection of things”.
But my early attempt would be something like this (maybe to come, in Python).
We could take the Python set object as the mathematical concept of a set. To add structure we can define new classes.
What might a list of definitions look like?
We probably need products and subsets next?
Products are tuples in Python.
A subset is a set, the parent / superset set, and the “subset function” that tests the truth condition “is subset”: so its signature is actually a triple, A, B, f. Right? def subset(A, B): condition = False; for element in B: if element not in A: condition = False; return condition
I imagine there’s a more pythonic way using a list processing method like a map or filter or something.
And then? I’ll see what is needed next. I know a relation is actually a subset of a product set. A function is a relation with a certain condition expressed in logical quantifiers, I think? two sets A B, for each b in B, there exists one and only one a in A such that the tuple in the subset of the product set of A and B has b in second place.
So we skipped over sets and logic, but it doesn’t matter since we already roughly have it in Python. We define a preorder as a binary relation which is reflexive and transitive. Like subsets, perhaps, all concepts can be defined as a signature of objects and functions they have to pass - their conditions?
In a dependently typed language such as FOLDS , which was already mentioned above, the concepts category, object and morphism are primitives and you don't have to ever say "set" in such a language if you don't want to. You can of course add a category "Set" to such a language and axiomatise some of its categorical properties in the spirit of ETCS for example.
John Baez (Jul 28 2023 at 10:55):I'm changing the title of this post from "Bacchus Naur" to "Backus Naur" even though I really love the idea that the Roman god of wine and festivity has a computer science concept named after him.
Ryan Wisnesky (Jul 28 2023 at 17:15):heh, there's always the "Ballmer peak": https://xkcd.com/323/
Patrick Nicodemus (Jul 29 2023 at 02:05):I don't mean to pick on your choice of example but Python is not a good choice of formal language to make this comparison. Python, like Javascript or other interpreted scripting languages, is a very rich and complex language to the point where giving a semantics for it is impossible. If you try to translate math into Python to make it more rigorous, you will quickly run into the problem that Python itself is not very rigorous.
It would be better for you to look into other formal languages like ZFC set theory, higher order logic (see "Simple Type Theory" by W. Farmer), dependent type theory ("Type theory and formal proof" by Geuvers and Nederpelt)
Coq, Agda, Lean, etc. But really an informal mathematical book on set theory like the one by Halmos would be more practical.
Josh Chen (Aug 13 2023 at 16:02):Julius said:
Curious if there’s a dense, pure definition of category theoretic objects as a tight, rigorous language - could be like an extended Bacchus Naur Form description of category theory, axiomatically / as a formal language?
There's also recent work by New and Licata: A Formal Logic for Formal Category Theory.