Category Theory
Zulip Server
Archive

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.

Stream: practice: software

Topic: Automated proving?

Jacques Carette (Nov 01 2022 at 17:07):

Anyone have recommendations for software (like say Prover9) that might let me experiment with for conjectures in category theory? More precisely, say I have a conjecture about equality of some morphisms in a new kind of category (ex: with a couple of monoidal structures, an involution, a couple more gadgets), and fiddling on paper leads nowhere. I'd like to throw this at an automated tool, just to see.

Most automated provers are untyped, which makes reasoning about morphisms hell (partiality is not fun, especially when you know for a fact that it's all total). Advice?

I've been thinking of seeing if something like one of Isabelle's sledgehammers might help. At least that would mostly hide the lack of types from me. But I find encoding category theory in HOL tedious, compared with doing it in dependent type theory, so I'm a little loath to pursue that route. [Plus I can only read Isabelle/HOL right now, I've never written any!]

Nathanael Arkor (Nov 01 2022 at 20:30):

Have you seen the work of Hamana on SOL (one paper with several examples is this one)? I've not yet tried it myself, but it seems pretty powerful.

Jacques Carette (Nov 01 2022 at 21:30):

I had not! Thanks, that does look intriguing.

Simon Burton (Nov 03 2022 at 13:25):

I've experimented with using Prover9 (and mace4) to prove category theory statements. You can see some of my mace files here. I was aiming to formalize rig categories, but I eventually gave up. It's pretty tricky, mainly because composition is a partial operation. The usual way to get around this is to have an "undefined" object, and this ends up polluting every (or most) predicates...

Jules Hedges (Nov 03 2022 at 15:59):

I think the Connexus tool can be used in this way, as a theorem prover for working with finite presentations of categories

Jacques Carette (Nov 03 2022 at 17:32):

@Simon Burton you do know that agda-categories does have a formalization of rig categories?

I was definitely afraid that "losing the types" would end up being a nightmare. This is what I learned from @Philip Zucker 's experience with E and experiments around Catlab. Christoph Benzmuller's experiments did not fill me with hope either! But then, this morning, I saw the paper Seventeen Provers under the Hammer which gave me renewed hope.

Jacques Carette (Nov 03 2022 at 17:36):

@Jules Hedges Thanks - but I'm not really working on presentations of categories, rather I'm trying to prove some equalities in something akin to special dagger rig categories. Specifically whether a model we've constructed satisfies axioms C1-C20 that Selinger et al enumerate on p.3 of this paper.

Philip Zucker (Nov 03 2022 at 18:25):

FYI The line of thinking that was kicked off by those experiments is still progressing. There is a new system in the works https://github.com/mwillsey/egg-smol (publication in progress, still not really intended for external users quite yet) that can be seen as a much more powerful and performant version of this prototype https://www.philipzucker.com/egglog/ in collaboration with some of the egg people at UW. The system is heavily based in the idea of partial functions, datalog, and equational (egraph based) rewriting with sophisticated guard conditions. Proof production is definitely in the roadmap and people are flirting with the question of how to do a sound CAS. I've also been wondering if I should revisit my E/Vampire encodings in light of a year or two of more experience. I think heavily leaning into a Maybe monad style encoding to make everything partial could work, especially with a metaprogramming environment to make it less burdensome. I know of a group of people attempting to integrate egg1 into lean and another into coq, but I am unaware of anyone trying to do something similar for Agda, which I know is your playground. Would be interested to understand good example problems in rig categories or otherwise if they are digestible by a mere mortal like myself, as we are always seeking more good applications of these systems.

Jacques Carette (Nov 03 2022 at 20:18):

@Philip Zucker We're in the middle of a paper where we need to see if C1-C20 of Selinger's paper (see link in response to Jules) hold. I think you'll get a good idea of the scope by just reading pages 1-3 of that paper.

Philip Zucker (Nov 03 2022 at 20:36):

If I'm reading this correctly, It is a pure group? Do you need n>2 or where n changes?

Jacques Carette (Nov 04 2022 at 07:36):

For that part, yes, actually, it is just the group. I've been so used to the general case that I did not notice that for this part, that's all we need. [We eventually want n>2, but n=2 is already hard.]

Simon Burton (Nov 04 2022 at 10:50):

Jacques Carette said:

Simon Burton you do know that agda-categories does have a formalization of rig categories?
...

Thanks for that overview. I did review the work done in agda. One thing that's fun about using Prover9 is that the sister program mace4 looks for models that provide a counterexample to statements. But I see now that I ran into many of the same issues that @Philip Zucker had: "Just because it says proved is not very convincing. It is very easy to have your axioms and/or conjecture stated incorrectly. Forall ! and Exists ? bind tighter than I naively expect them to in the syntax. I ended up putting parenthesis nearly everywhere. I had a lot of very difficult to debug problems due to bad binding assumptions."

Proving things in CT is often as easy as falling off a log. The arrows already tell you what to do. So the feeling is that a prover tailored to CT should work well. Even classical logic seems to be overkill for most CT, we only need very weak logic. Coherence results are more subtle, those are more like proving confluence of a rewrite system. But otherwise, we should be able to solve the word problem in various free higher-categories, such as a monoidal bicategory. Using stuff like Lean just seems like an impedance mismatch. So anyway, I'm pretty excited to see other people are working on this. I should probably let the professionals sort it out and stop shooting myself in the foot repeatedly, even though I still have some foot leftover...

Jacques Carette (Nov 04 2022 at 12:24):

Yeah, I might get around to working on that. Might happen in the second quarter of 2023 even.

Patrick Nicodemus (Jan 06 2024 at 17:54):

@Jacques Carette The KWARC research group has implemented an IDE for an extensional dependent type theory which translates the dependent type theory to HOL under the hood and then uses the automated theorem prover Leo III to try and solve theorems automatically. https://arxiv.org/abs/2305.15382

Jacques Carette (Jan 06 2024 at 19:21):

Thanks @Patrick Nicodemus . I guess neither Florian nor Christoph had seen my query here, as I would have expected to mention this when we were all in the same place last October. But test results of section 6.1 of the paper do not leave me optimistic.

Patrick Nicodemus (Jan 06 2024 at 23:01):

@Jacques Carette The tests don't reflect the way I imagine the software being most useful to category theorists. A more modest goal would be to assess only the purely equational reasoning involved in category theory. For example, the category theorist should supply the definition of a functor on objects and morphisms and let the HOL prover check that the functor preserves identity and composition. Equational reasoning should be trivial indeed but in Coq and Agda category theory libraries there are long chains of equational reasoning that require user knowledge of the library to solve, it would be good if this could be limited. Really by this point equational reasoning in a category should be a solved problem and there should be off the shelf tooling available.

Patrick Nicodemus (Jan 06 2024 at 23:03):

The tests in the paper all involve existential reasoning, which I think is a high bar to clear in general - there exists an isomorphism... I would be more than happy with a formal proof system which realistically allows us to only define things and takes care of the coherence conditions for us automatically.
For a more complex example, when building a bifunctor i think it's realistic for the user to manually supply the unitor and associator isomorphisms and ask that the coherence isomorphisms like the mac lane pentagon are manually checked.

Patrick Nicodemus (Jan 06 2024 at 23:10):

Simon Burton said:

Using stuff like Lean just seems like an impedance mismatch.

Yes, I really agree. It's strange that category theory is at once so simple and so complicated. Simple in that it is merely equational reasoning in large part, and seems to not need too many alternating quantifiers at its worst - universal properties are usually "for all, there exist".
Yet because we talk about classes we want type theories with universes, and because we talk about partially defined functions like composition we reach for dependent types as a principled solution to this, and now we stumble into all the problems with intensional equality.

Patrick Nicodemus (Jan 06 2024 at 23:14):

@Jules Hedges Do you think that the Connexus software could prove the simplicial identities for the simplex category automatically if i specified it as the free monoidal category with distinguished monoid and wrote down the presentation by the generating object and the rules for a monoid

Patrick Nicodemus (Jan 06 2024 at 23:16):

Simon Burton said:

Thanks for that overview. I did review the work done in agda. One thing that's fun about using Prover9 is that the sister program mace4 looks for models that provide a counterexample to statements.

Isabelle has nitpick now, which is a very good counterexample tool. Honestly, I don't know much about automated theorem proving but why not use Isabelle instead of Prover9? this is uninformed here but I would expect to be able to do anything you can do in Prover9 in Isabelle and Sledgehammer's portfolio strategy seems like it would work better than using a single theorem prover.

Patrick Nicodemus (Jan 06 2024 at 23:19):

More generally my uninformed assumption is that Isabelle probably has a more developed interface for specifying your theory. And I don't find the syntax confusing generally. (Well, using = for iff results in weird binding conventions.)

Ryan Wisnesky (Jan 07 2024 at 02:14):

Conexus CQL provides decision procedures for the word problem in finitely presented categories using an algorithm that is complete for equational theories which admit length non-decreasing re-write systems. It also provides decision procedures for the word problem in product categories, for example "entropic groupoid presentations", although those are a lot tougher. I'd be happy to work together to try to formalize the result about simplex categories you are looking for

Patrick Nicodemus (Jan 07 2024 at 05:29):

@Ryan Wisnesky I guess what I'm asking is whether it would be reasonable to extend this to finitely presented monoidal categories, where "finitely presented" refers to the fact that only finitely many objects and morphisms need to be specified, although the category may have infinitely many objects.

Ryan Wisnesky (Jan 07 2024 at 05:42):

I think the completion algorithm in question throws the sorts/objects away, so that seems reasonable, you'd need to provide an equational theory over a single sort. The monoidal aspect you'd similarly need to encode, using e.g. extra morphisms. I don't know much about the simplex equations but I was able to write and have CQL decide a toy theory that looks like my erroneous understanding of it for a small N:

schema simplicial = literal : empty {
entities
S
foreign_keys
d1 d2 s0 s1 : S -> S
path_equations
S.d2.d1 = S.d1.d1
S.s1.s0 = S.s0.s0
S.d2.s1 = S.s0.d2
}

Ryan Wisnesky (Jan 07 2024 at 05:43):

fwiw, to decide the word problem CQL generated a system that includes length-preserving re-write rules, so this isn't an "easy" theory to decide

Jacques Carette (Jan 07 2024 at 19:43):

Using software for mere categorical reasoning wouldn't really help that much - it's so easy humans can do it easily too.

Where things get hairy are when you get to bicategories and (separately) to say symmetric rig groupoids. The number of coherences (i.e. rewrites) get crazy (somewhat over 100). That's what I'd like automation for!

Ryan Wisnesky (Jan 07 2024 at 20:39):

When we deploy CQL at companies to do data integration, it routinely decides equational theories with thousands of equations or more in seconds. Most of these theories are never seen by people, they are induced by e.g. SQL schemas and OWL ontologies and datalog programs and ... .

Patrick Nicodemus (Jan 07 2024 at 22:14):

Jacques Carette said:

Using software for mere categorical reasoning wouldn't really help that much - it's so easy humans can do it easily too.

Where things get hairy are when you get to bicategories and (separately) to say symmetric rig groupoids. The number of coherences (i.e. rewrites) get crazy (somewhat over 100). That's what I'd like automation for!

Sure, I meant bicategories and stuff like that. The point is it's equational.

Jacques Carette (Jan 08 2024 at 12:59):

Patrick Nicodemus said:

Sure, I meant bicategories and stuff like that. The point is it's equational.

It's typed equational - I think if you throw away the types, might it not be an inequivalent theory?

Patrick Nicodemus (Jan 08 2024 at 13:58):

Jacques Carette said:

Patrick Nicodemus said:

Sure, I meant bicategories and stuff like that. The point is it's equational.

It's typed equational - I think if you throw away the types, might it not be an inequivalent theory?

Yeah it's a good question. I alluded to this earlier when I said that it was "simple in some ways and complicated in others." I would really like to know what kind of soundness theorems exist for trying to embed an equational theory with partially defined functions into an untyped theory as it's obviously relevant here. Note that of course all equations of category theory are well typed and so one side is well typed iff the other one is. This suggests to me that equational rewriting between two well typed expressions of category theory will not go wrong in an untyped logic, as you should be able to carefully express the rewriting rules so that well typed terms are always rewritten to well typed terms and maybe you can get a soundness theorem this way

Ryan Wisnesky (Jan 08 2024 at 16:35):

Goguen studied the reduction of many-sorted FOL to single-sorted FOL and gave conditions for when that is sound https://dl.acm.org/doi/pdf/10.1145/24714.24719 . FWIW, dealing with empty sorts in current FOL provers that are singly typed is pretty annoying

John Baez (Jan 08 2024 at 16:50):

Jacques Carette said:

Where things get hairy are when you get to bicategories and (separately) to say symmetric rig groupoids. The number of coherences (i.e. rewrites) get crazy (somewhat over 100). That's what I'd like automation for!

How are you getting the figure of over 100 coherence laws?

Jacques Carette (Jan 08 2024 at 17:38):

$\otimes$ and $\oplus$ as bifunctors add a few, that they are in fact part of a monoidal structure a bunch more, braiding + symmetry some more, that the various equational laws of rigs are not just natural transformations but natural isomorphisms add quite a few more, then a whole bunch more for the Laplaza coherences.

In other words, you get that many when you 'flatten out' everything you need, separate out the structure from the things that need to commute - you end up with > 100 conditions.