Realizability

Realizability is an interpretation (or rather, a whole family of interpretations) of constructive theories in terms of computable functions. Kleene's original realizability interpretation was very syntactical in nature, and provided an interpretation of constructive arithmetic in terms of codes of recursive functions. Intuitively, a formula is realizable if there is a code of an algorithm which gives us a constructive way of seeing why the formula is true. One of the important applications of this interpretation is that it gives consistency proofs not only of constructive arithmetic itself, but also of various extensions, some of which are classically inconsistent. A nice example is Church's Thesis: this is the statement that every total relation contains a computable function.

The Effective topos is a (non-Grothendieck) topos which naturally extends Kleene's original interpretation to all higher types; intuitively, this topos arises by taking the powerset of the natural numbers as the object of truth-values and performing a construction analogous to that of H-valued sets for a locale H. It turns out that there are many toposes similar to the Effective topos; for example, one may take any partial combinatory algebra A and construct from it a topos RT[A]. (This may be seen as analogous to the fact that to every space one associates its category of sheaves.) Also, one may modify the construction in various ways, and as a result we now have a rich stamp collection of realizability toposes.

One of the challenges is to create some order in this collection. In part, this is supposed to happen by analysing the basic building blocks (PCAs and related structures) for the constructions in more depth. The maps between PCAs which give rise to geometric morphisms are to be understood as simulations, or interpretations of one PCA in another. Originally, Longley defined these to be special kinds of relations, but in "Ordered partial combinatory algebras" it was shown that one may in fact regard this as a Kleisli category for a certain monad. More generally, one would like to understand the structural properties of the category of PCAs (rather, the order-enriched category), even though not many interesting constructions are known. By generalizing a result by Pitts, it can be shown that the category of PCAs admits certain comma objects, which in turn sheds some light on iteration of the realizability construction (see the paper "Iterated realizability as a comma construction").

From another angle, one may hope to understand what the minimum amount of structure needed is to construct a realizability topos. This line of approach was taken in "All realizability is relative", where it was proved that PCA-like properties are inevitable if one is to obtain a topos in the end. However, this is far from the end of the story, and a clear definition of what makes a topos a realizability topos is still missing.

Abstract computability

Together with Robin Cockett I'm developing a categorical approach to computability theory. The key concept is that of a Turing category; this is a weakly cartesian closed partial map category with a universal object, called a Turing object. One can show that such an object always carries the structure of a PCA, and that every map in the category is computable w.r.t. this PCA structure. In fact, the connection between (certain generalizations of) PCAs and Turing categories is much closer than that, and the main result from our paper "Introduction to Turing categories" explains how to pass back and forth between Turing categories and generalized PCAs.

The main feature of Turing categories is that one may develop elementary recursion theory. For example, standard results such as the S-m-n theorem and the universality theorem are almost immediate from the definition, but other results, such as the unsolvability of the Halting problem, and m-completeness of the Halting set, are also derived without much difficulty. Other results (or even definitions) require a bit more structure on the Turing category; for example, to define a recursive set one needs the notion of complement. Part of the goal is to understand what minimum structure is required for certain results.

In developing recursion theory in this setting, one may of course employ diagrammatic reasoning, but one soon finds that the diagrams chased to prove even pedestrian results may be quite complex. It is much better to employ the internal language of Turing categories: this results in proofs which are often almost literally the ones one may find in standard textbooks.

We have developed the internal language for cartesian partial map categories in quite a bit of detail, since it has many more uses than just giving concise proofs about Turing categories. The theory PCL (partial combinatory logic), whose models are precisely PCAs, has a classifying category, and one of the goals of our paper [] was to understand this category in a bit more detail. Interestingly enough, this led us to investigate a much wider class of categories called unitary categories. In turn, using techniques from functorial semantics combined with results about unitary categories yielded a better understanding of the problem of completability of partial algebraic structures, such as PCAs.

Another aspect of the internal language is rewriting theory. Just as rewriting presentations of, say, equational theories give us finer control and better understanding of the theories, the same is true for theories with partiality. Indeed, one of the main results of a forthcoming paper on this subject is to use rewriting techniques to understand, for example, what are the total maps in the classifying category of PCL. As a consequence, we can characterize the global sections of the generic PCA.

Logic and Homotopy

It has been known for a long time now that there are profound and fascinating connections between the areas of topology, logic and category theory. Topology and category theory meet not only in the study of sheaf toposes, but also in abstract homotopy, where Quillen model categories are nowadays part of the standard toolkit. Logic and category theory are of course united in categorical logic, while sheaf semantics provides a way of using spaces and related structures to build models validating or refuting various logical principles.

A more modern connection between logic and homotopy theory arises from Martin-Loef type theory. Originally intended as a foundational framework in which one may develop parts of constructive mathematics, this system is these days employed as a setting for programming as well. The crucial feature of ML type theory is that it has identity types: the inhabitants of such a type are identity proofs (i.e. proofs that two given objects are equal). Thus given objects a,b of a given type G, say, one has a type G(a,b), whose terms witness that a and b are provably equal. This can be iterated, and for f,g:G(a,b) one may form the identity type G(a,b)(f,g) whose inhabitants are the proofs that the identity proofs f and g are equal, et cetera. It was already noted in the work of Hofmann and Streicher that laws analogous to those for a groupoid hold (but instead of holding on the nose, they hold only up to higher identity proofs, and so on).

In work with Steve Awodey and Michael Warren we describe one of the ways in which the analogy between the higher identity types and the higher fundamental groupoid can be made more precise. We first show that there is a monad on the category of globular sets which freely adjoins cells in accordance to the rules of the type theory. When one truncates at dimension 1, it can be shown that every free algebra for this monad is equivalent to the free groupoid on the globular set. More generally, every algebra (which we call an ML-complex) has an underlying groupoid, but the category of algebras for the monad is not equivalent to the category of groupoids. However, it carries a Quillen model structure, and it is proved that this model category is Quillen equivalent to the category of groupoids, and hence to the category of homotopy 1-types.

Inverse semigroups, groupoids and toposes

Inverse semigroups describe partial symmetries of structures in the same way as groups describe global symmetries. It was already shown by Ehresmann that the category of inverse semigroups is equivalent to that of inductive groupoids; a further connection between semigroups and categories is given by the fact that every inverse semigroup S has a classifying topos B(S); many constructions and results in semigroup theory have natural and canonical topos-theoretic interpretation. For example, cohomology of inverse semigroups is just topos cohomology, MacAlister's P theorem (a structure theorem for unitary inverse semigroups) can be understood in terms of the torsion-free generator of B(S), and the maximum group image of S (the largest group onto which it maps) is the fundamental group of B(S).

In the paper "Topos-theoretic aspects of semigroup actions", Jonathon Funk and I explore semigroup actions and answer the question what B(S) actually classifies. It is seen that the theory of torsors for an inverse semigroup is richer and more subtle than that for groups; in particular, there are many non-isomorphic S-torsors even in the category of sets. We also define a classifying topos for arbitrary semigroups, overcoming the apparent obstruction that an arbitrary semigroup need not have any idempotents to split.