I’ve been thinking more about the diagonal argument this week, and realised my version for magmoidal cats with diagonals was insufficient to cover a massively important example: the category of partial recursive functions! This is because every partial endomorphism has a fixed global point, namely the undefined point: the partial function with empty domain. The same problem holds for arbitrary generalised points . So the diagonal argument can’t get started. Any general diagonal argument should be able to deal with the special case of partial recursive functions without special tweaks to deal with such behaviour. So while my magmoidal diagonal argument is valid, it needs more work to apply where one has partial functions.
Enter restriction categories, due to Robin Cockett and Steve Lack, one of a number of variants on the idea of defining partial morphisms abstractly, many of them from people looking for categorical frameworks for computability theory. It’s not so much the partial nature of morphisms that is important, but the idea one can identify ‘total’ functions using purely the restriction structure. And, every category can be equipped with trivial restriction structure so that all morphisms are total.
There is a notion of restriction functor respecting the restriction structure, and also strict natural transformations whose components are total morphisms, giving an embedding of into as a full sub-2-category. So now I can work with restriction categories, with plain categories as a special case.
As before, I want a magmoidal category: a magma object, but now in , giving a magmoidal restriction category with multiplication , and with diagonals, hence a strict natural transformation . It follows from this that if are total, then so is . For now, I also need a chosen object of (ie ), that replaces the terminal object in a cartesian category (as in Lawvere’s version). We can then talk about -valued generalised points, and, generalising Lawvere, basically identify functions if they agree on all points.
Digression: There’s an interesting point here, that I only recently appreciated: Lawvere’s diagonal argument is really about well-pointed cartesian categories—at least it is implied by a version (in an exercise!) in the book Conceptual Mathematics by Lawvere and Schanuel. For an arbitrary cartesian category , we have the factorisation of the ‘global sections’ functor into a bijective-on-objects+full functor followed by a faithful functor , both of which are cartesian. Further, in , the terminal object is now a separator, hence is well-pointed, and makes a representably concrete category. The definitions of fixed point (for Lawvere’s fixed point theorem), free endomorphism, and the result of the diagonal argument all really refer to what is happening in , the objects of which we can consider as structured sets via . End digression
The key idea is to make sure the definition of free endomorphism in a restriction category with a specified object captures the cases of categories of partial functions, be they arbitrary or partial recursive or what-have-you. To avoid the issue of the partial functions whose domain is empty, we demand that -points are total morphisms. This accords better with the intuition, since if is such that for all , we have , then it’s hard to see how we can tell maps out of apart!
So, I define an endomorphism in a restriction category with chosen object (a pointed restriction category) to be free (or to be more clear, -free) if for all total , we have . In a similar way, the key idea that a family of maps parametrised by an object is incomplete goes as follows: Given a morphism in a magmoidal restriction category with diagonals, it is an incomplete parametrisation of maps if there is a morphism such that for all total there is a total such that is not equal to .
The diagonal argument then runs as before, using the facts that total maps are closed under and composition. The proof works for cartesian categories, where we take the trivial restriction structure, the chosen element is a terminal object, and also for all the restriction categories of interest consisting of partial functions between sets, where we take some separator, for instance a one-element set, but this is not the only option. There is a restriction category with sole object and partial recursive functions as morphisms. By using pairing functions, this is magmoidal with diagonals, and the only object is a separator, but not terminal (or even ‘restriction terminal’, the correct notion in this setting)
The only part of this that I’m not happy with is the reliance on a specified object : the diagonal argument works using a kind of internal logic, where we are allowed to ‘base change’ along maps for the domain of our generalised points. This is what I did in my notes, before realising that I was missing some subtleties that ruled out natural and important examples. One option is to allow base change along total , but there is still a wrinkle in that if one is not careful about the definition of free endomorphism, there may be no examples whatsoever, since allowing arbitrary domains for generalised points means we might inadvertently have some initial, which is useless for specifying points! So one option is to only test on total where is not initial. This seems to capture the standard cateories of partial functions examples, but feels unnatural categorically speaking. Alternatively, one could ask that a free endomorphism is an endomorphism such that a generalised point is fixed if and only if its domain is initial. This also works for sets and partial functions. But then it is less clear how to define an incomplete parametrisation in a way that both captures the intuition, and the concrete examples, and also allows the diagonal argument to work, Still thinking about this one…