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: theory: category theory

Topic: Logic programming

Patrick Nicodemus (Feb 03 2024 at 23:12):

From a purely logical point of view, category theory is "easy" in some sense, a lot of the reasoning is just equational reasoning. There are universal quantifiers in universal properties, $\forall x. \exists! y.R(x,y)$ but these are rarely nested in a way that leads to deep chains of alternating quantifiers. On another hand, it is hard in the sense that it seems to fundamentally involve dependent types. This makes it unfortunately seemingly not a good candidate for automated theorem provers using first order logic because an explosion of predicates is necessary to control the type dependency.

It seems very plausible that, for example, some of the theory of pure categories or bicategories is decidable, i.e., we can write down a theory encompassing much of of pure non-applied elementary theory of categories or bicategories, and there is an algorithm to decide whether this is a theorem.

This led me to ask a more specific question. Mathematicians have a notion of a "follow-your-nose" proof, where the next step is obvious from the current one, and the proof is merely a mechanical matter of doing the obvious next thing. For example, to prove $A \lor B$ you should pick one of $A, B$ and try to prove it (trying to prove $A$ first and then $B$ if this fails); to prove $A\implies B$ you should assume $A$ and try to prove $B$; to prove $A\land B$ you should try and prove $A, B$ separately, and so on. Of course this does not always work, for example if you try to prove $A\lor B \implies B \lor A$ by following these rules, you will assume $A\lor B$ and then try to either prove $B$ or $A$, which is a dead-end. But it is of interest to write down exactly the logical structure of formulas for which the "naive" proof procedure does work, and the field of logic programming is in part about identifying a good class of logical formulas for which the naive "follow-your-nose" method works, and trying to encode interesting practical algorithms into the direct proof-search procedure for this class of formulas. So my question is, is there a known fragment of category theory which falls into the logic fragment supported by a logic programming language such as Lambda Prolog or Twelf? If such a fragment was identified it would give a very simple and easy to implement proof procedure for theorems in the fragment, just by essentially writing down the axioms and the goal to be proved and telling Lambda Prolog / Twelf to prove it.

Patrick Nicodemus (Feb 03 2024 at 23:16):

As a starting point, although we commonly say that category theory uses only intuitionistic reasoning, we can probably say something stronger: it uses only minimal logic, i.e., most category theory proofs do not rely on the principle of explosion in a fundamental way.

Patrick Nicodemus (Feb 03 2024 at 23:19):

(Twelf is unique in being a dependently typed logic programming language, and it is tempting to try and encode a decision procedure for category theory theorems in it.)

Mike Shulman (Feb 03 2024 at 23:48):

FWIW, Coq's typeclass-search mechanism is also a kind of dependently typed logic programming language.

Patrick Nicodemus (Feb 03 2024 at 23:54):

Mike Shulman said:

FWIW, Coq's typeclass-search mechanism is also a kind of dependently typed logic programming language.

Yes, that's a good point. I think that understanding Coq's typeclasses helped me to understand logic programming better. It seems like Enrico Tassi, one of the Coq developers, has really bought into the idea expressed by Dale Miller here https://link.springer.com/article/10.1007/s10817-018-9483-3 that for things like type inference and type class resolution it is best to have a dedicated logic programming language to explicitly write such functionality, viewing it as a natural generalization of typeclass resolution and canonical structures. I think that a long term goal is to implement a full elaborator for the calculus of inductive constructions in Lambda Prolog, ideally giving users the ability to extend the elaborator with additional unification hints.
https://github.com/LPCIC/
I'm not sure it's practical to manually assemble functors in Coq using the typeclass system, but with a dedicated user extensible language for the elaborator I feel like it might be.

Mike Shulman (Feb 04 2024 at 00:03):

I'm fond of that idea as well.

Evan Washington (Feb 04 2024 at 03:08):

Patrick Nicodemus said:

It seems very plausible that, for example, some of the theory of pure categories or bicategories is decidable, i.e., we can write down a theory encompassing much of of pure non-applied elementary theory of categories or bicategories, and there is an algorithm to decide whether this is a theorem.

I was struck by this seeming rather implausible, since one-object categories aren't even decidable (because the theory of groups isn't decidable). Then I came across this paper draft which skirts around the worry by considering equational theories of categories without any automorphisms (so that you cannot interpret the theory of groups).

Patrick Nicodemus (Feb 04 2024 at 14:15):

That's a good point, yeah. The example in the paper of a localization in a model category was more complicated than I had in mind, obviously a localization often gives categories for which the word problem is impossible to solve, along with other foundational issues. Maybe one way to make the problem more tractable would be to eliminate arbitrary equalities from the list of possible hypotheses, considering only equality hypotheses of the form "a morphism with this universal property is unique", so one does not have the ability to encode arbitrary problems from group theory.

Patrick Nicodemus (Feb 04 2024 at 14:19):

The functor laws and naturality laws aren't of this form, it's not obvious that there's a subset of equational reasoning which includes these without including much more complicated things.

Patrick Nicodemus (Feb 04 2024 at 16:52):

I don't mean to trivialize your point here by saying "well, pathological examples aside...". I did make a mistake in conflating equational reasoning with easy. But, I think experience does tell us that categorical proofs are often straightforward and direct, even if it is not obvious what would be a convenient formal language which is capable of expressing many of these arguments and does not encode the halting problem.

Ryan Wisnesky (Feb 04 2024 at 21:28):

there's a fast decision procedure from the 1980s for the word problem for any finitely presented category that admits an equivalent non-length-increasing re-write/Thue system. https://www.proquest.com/openview/1e022b58b2f1b944c3bb775cdf98f98d/