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.
Philip Zucker (Apr 07 2020 at 03:47):http://www.philipzucker.com/computational-category-theory-in-python-i-dictionaries-for-finset/ I thought this a pleasant example of how one might implement something with a categorical interface at the value level in a more mundane language. I feel like there is lots of wide open space for such things
Philip Zucker (Apr 13 2020 at 00:25):Part two where I build pullbacks in numpy with the help of @James Fairbanks and @Evan Patterson http://www.philipzucker.com/computational-category-theory-in-python-ii-numpy-for-finvect/
James Fairbanks (Apr 13 2020 at 01:13):
James Fairbanks (Apr 13 2020 at 01:13):That’s awesome @Philip Zucker, I had a question about this code example. Where is v on the drawing above it?
James Fairbanks (Apr 13 2020 at 01:14):I’m thinking that u,v should be q1, q2?
James Fairbanks (Apr 13 2020 at 01:14):Or I’m totally misunderstanding based on reading fast on my phone.
Philip Zucker (Apr 13 2020 at 02:05):That is correct. u and v correspond to q1 and q2
Philip Zucker (Apr 13 2020 at 02:05):On the phone to code formats weird too
Philip Zucker (Apr 13 2020 at 02:06):I pulled diagrams from wikipedia with different naming conventions, which was aa little lazy and dumb
Philip Zucker (Apr 13 2020 at 02:13):I should edit that
Philip Zucker (Apr 13 2020 at 02:36):fixed
Philip Zucker (May 02 2020 at 14:45):A pretty simple educational post on how to encode monoids and preorders as categories in python http://www.philipzucker.com/computational-category-theory-in-python-3-monoids-groups-and-preorders/
Simon Burton (May 02 2020 at 15:25):Looking at this book by Walters, it all seems to be building up to the last chapter where they show how to implement computations in categories given by generators and relations... very cool.
Simon Burton (May 02 2020 at 15:29):There's also this older book by Rydeheard & Burstall, called "computational category theory" http://www.cs.man.ac.uk/~david/categories/ they use ML , and do nice stuff like compute term unifications as a coequalizer .
Simon Burton (May 02 2020 at 15:37):Philip Zucker said:
Part two where I build pullbacks in numpy with the help of James Fairbanks and Evan Patterson http://www.philipzucker.com/computational-category-theory-in-python-ii-numpy-for-finvect/
This stuff gets much more interesting when the constructions of (co-)limits also build the universal arrow from/to a given cone... that is what allows you to build more constructions by composing these (co-)limits...
Philip Zucker (May 02 2020 at 15:50):Yea, The Rydeheard and Burstall book is great. It was the impetus to start the series.
Philip Zucker (May 02 2020 at 15:51):I'm intrigued by your second comment but I'm not sure what you mean. Are you talking about span composition?
Philip Zucker (May 02 2020 at 15:55):Or that being able to compute pushouts and pullbacks allows you to compute arbitrary limits/colimits?
Simon Burton (May 02 2020 at 16:48):Philip Zucker said:
Or that being able to compute pushouts and pullbacks allows you to compute arbitrary limits/colimits?
Yes, for example, going from co-equalizers & pushouts to give arbitrary co-limits, i forgot the exact theorem.
The example I have actually implemented I used the universality of pushouts in FinVect to give a pushout in the category of chain complexes (over finite dim vector spaces.)
This universality business is the "API" of category theory. It's all very nice to see it implemented... It works very well and does not need functional programming.. argh, i can feel a rant coming on.. FP is good and all, but I do get annoyed at all the implicit "CT == FP" sloganism that goes on. So anyway, I'm happy to meet someone else that is interested in a python take on category theory.
Philip Zucker (May 02 2020 at 16:58):I do feel that the insistence of strong typing is not ubiquitously the most useful perspective on category theory. How many well typed linear algebra libraries are actually usable. Hard line formalness often has a mind and drudgery tax. Have you ever checked out Catlab.jl ? There's a similar minded crew over there.
Philip Zucker (May 02 2020 at 16:59):I do use functional programming in the sense of first class functions though. The universal property is encoded as a function that computes the appropriate universal morphism.
Philip Zucker (May 02 2020 at 17:00):I have shied away from using python functions as morphisms themselves since they aren't inspectable the way data is
Simon Burton (May 02 2020 at 17:16):Philip Zucker said:
I do use functional programming in the sense of first class functions though. The universal property is encoded as a function that computes the appropriate universal morphism.
Oh right, sorry I missed that. :+1:
Simon Burton (May 02 2020 at 17:22):Philip Zucker said:
I have shied away from using python functions as morphisms themselves since they aren't inspectable the way data is
Yes, this keeps nagging at me. At one point I wrote a python compiler based on llvm, and also have dabbled with pypy. All of that, more than 10 years ago now, was so horrifying that I'm not likely to try it again, although I do keep fantasizing about it.
Simon Burton (May 02 2020 at 17:31):yes I have looked at Catlib.jl ...
Philip Zucker (Jul 05 2020 at 17:10):Some thoughts on using automatic theorem provers for category theory https://www.philipzucker.com/category-theory-in-the-e-automated-theorem-prover/
Eduardo Ochs (Jul 05 2020 at 19:58):Philip Zucker said:
Some thoughts on using automatic theorem provers for category theory https://www.philipzucker.com/category-theory-in-the-e-automated-theorem-prover/
Very nice!!!
Btw, there's a big list of implementations of CT on proof assistants here:
https://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants
maybe you'd like to add that to your list of links...
Philip Zucker (Jul 06 2020 at 03:54):Thanks, I will!
Thomas Read (Jul 06 2020 at 06:38):Thanks - this is something I've been curious about! It would be interesting to find out the limit of the sort of problems these provers can practically solve at the moment
Philip Zucker (Jul 06 2020 at 14:00):That is a good question, and I don't know the answer. Basically if these tools scale to the nasty encodings necessary to express what you want, they seem incredibly useful, but if they don't, then they aren't. And the only way to know is to try.
Simon Burton (Jul 07 2020 at 11:37):Assembling some notes here about symmetric monoidal bla bla categories, and dagnabit, why isn't there a canonical reference for this stuff? Or much better: theorem prover verified list of axioms for ones chosen collection of adjectives, and associated latex pls. Ok, thanks bye.
Jules Hedges (Jul 07 2020 at 12:16):The canonical reference is Selinger's survey
Jules Hedges (Jul 07 2020 at 12:16):"A survey of graphical languages for monoidal categories"
Simon Burton (Jul 07 2020 at 12:34):Thanks for reminding me, that is a good reference. I guess my point is there is never going to be a canonical reference for "symmetric monoidal bla bla categories" for some choice of bla bla, as there are just too many different combinations of the various qualifiers...
Philip Zucker (Jul 07 2020 at 20:18):Catlab has an interesting list https://algebraicjulia.github.io/Catlab.jl/latest/apis/theories/
Simon Burton (Jul 08 2020 at 00:27):Nice.. Is there any example code that uses this ? I don't really understand anything about what this is doing.
James Fairbanks (Jul 08 2020 at 01:06):That code is just encoding the theories out of that Sellinger survey paper into a DSL for specifying doctrines. It doesn’t do anything with them. The Catlab read me points to some docs with examples. My ACT talk tomorrow will also show some examples
Keith Elliott Peterson (Aug 06 2021 at 20:38):I don't see any implementations of function sets yet, so I'm going to give mine (though, this is in Racket):
(define (function-set src tgt #:as-functions? [as-funcs #f])
(list->set
(map
(if as-funcs
(compose (λ (x) (function x src tgt))
fgraph->procedure list->set)
list->set)
(apply
cartesian-product
(for/list ; src = (set a b ...) ↦ (list (list ... '(a x) '(a y) '(a z)) (list ... '(b x) '(b y) '(b z)) ...)
([i src])
(for/list ; tgt = (set ... x y z) ↦ (list ... '(i x) '(i y) '(i z))
([j tgt])
(list i j)))
))))
It works by finding all possible graphs of functions and then either keep it as is or converts them to actual functions.
For instance:
> (function-set (set 1 2)(set 1 2 3))
(set
(set '(1 3) '(2 2))
(set '(1 2) '(2 1))
(set '(1 1) '(2 3))
(set '(1 2) '(2 3))
(set '(1 1) '(2 1))
(set '(1 3) '(2 3))
(set '(1 1) '(2 2))
(set '(1 2) '(2 2))
(set '(2 1) '(1 3)))
And as functions:
> (function-set (set 1 2)(set 1 2 3) #:as-functions? #t)
(set
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3))
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3))
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3))
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3))
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3))
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3))
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3))
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3))
(function #<procedure:...nite-set-theory.rkt:14:2> (set 1 2) (set 1 2 3)))
I've been experimenting with making a prolog-like language powered by egraphs https://egraphs-good.github.io/ under the hood for the purposes of categorical automated proving. Still has some very rough edges, but here's some examples that I think make sense and work. I compiled it to the web, so it works in browser.
Jacques Carette (Aug 19 2021 at 14:13):That's very cool. But I was kind of hoping that the result would be a proof, not a bare []. For pullback of monic is monic, what are the rewriting steps to go from p to q ?
Philip Zucker (Aug 19 2021 at 14:54):Work in progress (not by me) https://github.com/egraphs-good/egg/pull/115
Philip Zucker (Aug 19 2021 at 14:54):When this lands, it should be possible to enable proof output
Philip Zucker (Aug 19 2021 at 14:55):It does produce some useful information in the sense of finding certain morphisms
Philip Zucker (Aug 19 2021 at 14:56):It is to some degree a black box. An output that I can inspect but have not enabled on the web version is a graphviz dump of the final egraph, which represents all inferred equalities. It at least did not seem to infer a false equality to my eye
Jacques Carette (Aug 19 2021 at 15:00):Being able to see the final egraph does sound really cool.
Philip Zucker (Aug 19 2021 at 15:00):It's actually in the blog post https://www.philipzucker.com/assets/egglog_monic.png
Philip Zucker (Aug 19 2021 at 15:01):It's very busy and only going to get worse with harder problems. I suppose it might be possible to filter or compress it using domain specific information
Philip Zucker (Aug 19 2021 at 15:06):A mode I've considered implementing is a handwritten proof mode, which might be nice both to confirm it's taking a path I expect, and to help it along when the problem gets too hard to do all in one go. The idea was to take each step of the proof, run the egraph saturation, seek the current lemma. If found, clear the egraph and insert the lemma. Repeat.
Jacques Carette (Aug 19 2021 at 15:42):I missed that link, so for others like me, Egglog 2: Automatically Proving the Pullback of a Monic is Monic is the blog post in question.