Dialectica Categories in Computing

 

In the first half of the year we had an AMS Mathematical Research Community (MRC) on Applied Category Theory, in Beaver Hollow, NY. John Baez blogged about it in “Learn Applied Category Theory!” Here’s a poster advertising the whole program.

We also had a paper in the Notices of American Mathematical Society, describing our proposal:

Applied Category Theory in Chemistry, Computing, and Social Networks John Baez, Simon Cho, Daniel Cicala, Nina Otter, and Valeria de Paiva.

An MRC is a bit like a version “on steroids” of the ACT Adjoint School, as there are many more researchers in a research subgroup in the MRC than in a Adjoint School group. While my ACT Adjoint School group had four students and a TA, my MRC group had thirteen researchers. So from four to thirteen people you have more than three times the number of people to do interesting research with. Plenty of fun, but it can be unsettling to think about research problems for so many people you don’t know, especially for me (well, I haven’t had that much experience directing other people’s research).

I was very worried to begin with, but when we got going, it was exhilarating. Great fun to discuss serious math problems with people interested in similar problems, with similar tastes to yours and with plenty of ideas of their own. The program had three mentors (John, Nina and myself), and I ended up with a group of 13, subdivided into 4 smaller groups. Things were going very well (you can check some of the discussions in the Zulip channel [practice:Dialectica]) until two days before the meeting in upper New York state I got ill, and ended up in the ER in the Stanford hospital. Twice.

I couldn’t go to the research meeting in Beaver Hollow, but Jérémie Koenig, my trusted deputy, managed to get everyone working well together into the four groups we had established before:

1. Dialectica and Polynomials,
2. Dialectica and Games,
3. Dialectica and Lenses,
4. Dialectica Petri net Processes.

They sent me a lovely picture from Beaver Hollow.

The neat thing about MRCs is that they give the participants some funds to make academic visits and I was very touched when my group decided to come and visit me in California, using their funds. This meant that we had another smaller meeting in Cupertino, in the middle of the Summer. Well, it was already September and usually the weather over here is good most of the time, but we had some bad luck, and this week was a heatwave, the worst one this summer. But we had some fun. Now the problem is reworking what happened in the many discussions.

A third component of the MRC program is still to come. Of course we all hope that the math we discussed during the summer will mature nicely into preprints and papers and programs, and these are supposed to be presented in the AMS Joint Mathematics Meetings (JMM) in Boston in early January. So one organizer was chosen from each mentor’s group and I am very happy that Charlotte Aten accepted to be the organizer for our group, despite being in the last weeks of her PhD and interviewing for jobs. Then sometime in September we were told everyone needed to write up some ideas that they hoped could make solid papers before January 2023. I’m glad to report that every one of our four subgroups was able to produce an abstract and I hope the papers are in the process of being written as I write this.

Now this post was meant to be about the four subgroups above and why I am so excited for the mathematics we’re doing. But I am a bit behind with my processing of the knowledge we shared when people visited here (and over Zulip!). So, while I could possibly wait for the JMM to get to grips with more of the new math that people are producing, I think I will try to explain, at least a little, how the themes above interact.

I started my research career working on Gödel’s Dialectica Interpretation. On bad days I think not only have I never left the dialectica, but even today I hardly understand the stuff, after all these many years. Then I console myself with the thought that the stuff is really fascinating and full of surprising consequences and applications!

Someone else who’s awed by the Dialectica Interpretation is Jules Hedges. His blog post Lenses for Philosophers shows some of the badly understood consequences and connections of the work on categorical dialectica construction. In some ways the MRC Dialectica categories for Computing is an attempt to clarify some of the interrelations described in Hedges’ post.

Gödel’s Dialectica Interpretation is a proof interpretation of intuitionistic arithmetic into a quantifier-free theory of functionals of finite type, called System T.

The interpretation’s original use was to show the consistency of Heyting (or intuitionistic) arithmetic. When combined with Gödel’s double-negation interpretation, which reduces classical arithmetic to intuitionistic arithmetic, the Dialectica interpretation yields a reduction of the classical theory as well.

As explained by Fernando Ferreira,

The stated purpose of Gödel’s Dialectica paper is to present a consistency proof of first-order Peano arithmetic PA by way of an extension of the finitary viewpoint according to which the requirement that constructions must be of and over “concrete” objects is relaxed to be of and over certain abstracta, namely computable functionals of finite type over the natural numbers.

Thus the Dialectica interpretation can be considered a relaxed (or liberalized) form of Hilbert’s program, where instead of insisting on the finitary viewpoint, we accept ‘computable functionals of finite type’ as (sort-of) concrete objects. To understand the interpretation itself, I recommend A.S. Troelstra’s “Introductory Note to the Dialectica paper” in Gödel’s Collected works, volume II, where we can read that “Gödel presents his results as a contribution to a liberalized version of Hilbert’s program: to justify classical systems, in particular arithmetic, in terms of notions as intuitively clear as possible.” From there one can graduate to more complete work of Troelstra himself (Metamathematical investigation of intuitionistic arithmetic and analysis (1973)), of Avigad and Feferman (Godel’s Functional (“Dialectica”) Interpretation) and of Kohlenbach and his school.

The categorical internal versions of the Dialectica construction, starting in de Paiva’s thesis in 1988 (out as a technical report in 1991), have spelled out some of the requirements and consequences of the interpretation, especially its connection to Linear Logic. The categorical dialectica construction was generalized to fibrations, by Hyland (2002), Biering (2008) and Hofstra (2011). Generalizations to dependent type theories appeared in van Glehn (2016) and Moss (2018) and then together (2018). More recently Trotta et al, building on this work introduced Gödel fibrations and Gödel doctrines, rekindling the connections of the categorical dialectica construction to logic and making sure that the three dialectica principles (Independence of Premise, Markov Principle and Axiom of Choice) get their categorical explanation.

The main connections of the Dialectica construction discussed in the MRC, as anticipated above, are between ‘lenses’ and dialectica categories, between ‘polynomials’ and dialectica categories (see Nelson Niu’s blog post and Sean Moss’ talk), between ‘games’ and dialectica categories (already hinted at in Blass’ original paper on games for linear logic) and between concurrency theories and dialectica categories in the shape of Dialectica Petri nets Processes and their implementation in Agda. I hope the abstracts for the extended discussions of these four sets of connections will be available soon.

But it is clear that we’re only scratching the surface of this rich story of interconnections. Hopefully much more will come to light in the near future.