Diagonal arguments: once more with feeling

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 \mathbb{N} \to \mathbb{N} has a fixed global point, namely the undefined point: the partial function 1 \to \mathbb{N} with empty domain. The same problem holds for arbitrary generalised points X \to \mathbb{N}. 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 \mathbf{Cat} into \mathbf{restrCat} 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 \mathbf{restrCat}, giving a magmoidal restriction category C with multiplication \#\colon C\times C \to C, and with diagonals, hence a strict natural transformation \delta\colon \mathrm{id}_C \Rightarrow \# \circ \Delta. It follows from this that if f,g are total, then so is f\# gFor now, I also need a chosen object t of C (ie 1 \to C), that replaces the terminal object 1 in a cartesian category (as in Lawvere’s version). We can then talk about t-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 D, we have the factorisation of the ‘global sections’ functor \Gamma = D(1,-)\colon D\to \mathbf{Set} into a bijective-on-objects+full functor D \to D_{wp} followed by a faithful functor D_{wp}\to \mathbf{Set}, both of which are cartesian. Further, in D_{wp}, the terminal object 1 is now a separator, hence D_{wp} is well-pointed, and U := D_{wp}(1,-)\colon D_{wp} \to \mathbf{Set} makes D_{wp} 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 D_{wp}, the objects of which we can consider as structured sets via UEnd digression
The key idea is to make sure the definition of free endomorphism in a restriction category with a specified object t 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 t-points x\colon t \to X are total morphisms. This accords better with the intuition, since if x is such that for all f,g\colon X\to Y, we have f\circ x = g\circ y, then it’s hard to see how we can tell maps out of X apart!
So, I define an endomorphism \sigma\colon X\to X in a restriction category with chosen object t (a pointed restriction category) to be free (or to be more clear, t-free) if for all total x\colon t\to X, we have \sigma\circ x \neq x. In a similar way, the key idea that a family of maps parametrised by an object is incomplete goes as follows: Given F\colon A\# X \to Y a morphism in a magmoidal restriction category with diagonals, it is an incomplete parametrisation of maps X\to Y if there is a morphism f\colon X\to Y such that for all total a\colon t \to A there is a total x\colon t\to X such that t\stackrel{\delta_t} t \# t \stackrel{a\# x}{\to} A\# X \to Y is not equal to f\circ x\colon t\to X \to Y.
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 \mathbb{N} and partial recursive functions \mathbb{N} \to \mathbb{N} 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 t: the diagonal argument works using a kind of internal logic, where we are allowed to ‘base change’ along maps t' \to t 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 t' \to t, 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 t for generalised points means we might inadvertently have some t' initial, which is useless for specifying points! So one option is to only test on total t\to X where t 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…
Addendum: I should have specified some more interesting examples of magmoidal restriction categories with diagonals, which are not cartesian. I will just give one, namely the Turing categories of Cockett and Hofstra (see this recent blog post for a discussion).

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.