Defining computable functions categorically

Computable functions may be defined in terms of Turing machines or recursive functions, or some other model of computation. We normally say that the choice doesn't matter, because all models of computation are equivalent. However, something about this bothers me.

Turing machines, for example, operate on strings of tokens, taking strings as input and giving strings as output. If we have another model of computation that also operates on strings then we have no problem saying formally whether it's equivalent to a Turing machine. However, if our model of computation operates on something other than strings then we have to define a mapping from its inputs and outputs to strings, and it seems there is no way to formally define whether that mapping is computable or not. (If I am wrong about this, please correct me.) So whenever we talk about equivalence between Turing machines and some non-string based model of computation, we are invoking an informal step; this seems unsatisfying.

It occurs to me that category theory might offer a way out of this, and I'm wondering if this has been done. For example, suppose we define a category with one object, to be interpreted as the set of all strings on some alphabet. We draw an arrow from this set to itself for every (partial) function that can be computed with a Turing machine, and define composition of arrows as function composition.

It is clear that this forms a category. My question is whether this category by itself (i.e. just the morphisms and their relationships, without reference to the underlying string type) tells us everything we need to know about computable functions. In other words, would it make sense to define Turing equivalence in terms of isomorphism to this category?

What I have in mind here is something like this: suppose we're given a model of computation that computes partial functions from some set $S$ to itself. We can then form a category of all partial functions that can be computed by this system and check whether this category is isomorphic to the similar category for Turing machines as defined above. This is appealing, if it works, because we never needed to define a mapping between the elements of $S$ and the elements of the set of strings. (But I'm worried it might not work, due to the possibility of the category isomorphism itself being uncomputable, in some sense.)

Finally, if this idea doesn't work, is there some way to fix it so that it does? I would be interested to hear about any work on defining or reasoning about the set of computable partial functions from a purely categorical point of view, so that it can be characterised without reference to a particular underlying model of computation.

• I like this question a lot. I wonder one can answer it by showing that pointwise evaluation of the functions can be defined in the monoid structure, with finitely many parameters (for the zero functions, succssor and perhaps a few others, such as the pairing function projections). From this, it would follow that in any isomorphic copy of that category, one can "compute" the function by translating through the isomorphism. This would show a sense in which that category captures computability. I am a little worried, however, about the fact that your category has only unary composition. Feb 28, 2018 at 2:53
• This is formalized in the notion of a realizability topos, and Frey's theorem characterizes such toposes axiomatically. See ncatlab.org/nlab/show/realizability%20topos Feb 28, 2018 at 6:23
• @DmitriPavlov great, fantastic! I don't yet have the background to understand that page, but I'm happy to know what I should be aiming for. (Answers are welcome that gently outline how this approach works, in the context of my question. I'll look into it in my own time also of course.) Feb 28, 2018 at 7:03
• Oh, I had understood the question to be specifically about the category that was mentioned there. Obviously one can capture the notion of computability with a richer category. Feb 28, 2018 at 14:33

You are looking for realizability toposes and related categories, as was already pointed out in the comments. Let me make a quick summary of how things work and why we can completely circumvent the dilemmas involving arbitrary codings of objects with strings.

To understand what is going on we do not need realizability toposes, as these are quite technically involved. We can use the much simpler assemblies. First we fix a model of computation $A$. Formally, $A$ should be a partial combinatory algebra, but informally you can just imagine Turing machines, or programs in a general-purpose programming language. An assembly $(S, \Vdash_S)$ is a set $S$ together with a realizability relation ${\Vdash_S} \subseteq A \times S$. We read $p \Vdash_S x$ as "program $p$ is a code of element $x \in S$". We require that $\Vdash_S$ have the property $\forall x \in S . \exists p \in A . p \Vdash_S x$, i.e., every element has to have at least one code. (But the same code may be shared between elements.) The notion of an assembly is very natural and it precisely captures the idea the the elements of an abstract set are encoded in some way by programs.

A morphism of assemblies $f : (S, \Vdash_S) \to (T, \Vdash_T)$ is map $f : S \to T$ which is realized, by which we mean that there is a program $q \in A$ such that $$p \Vdash_S x \implies q \cdot p \Vdash_T f(x).$$ This again is a completely natural idea which captures precisely the fact that the program $q$ operates on codes the way $f$ operates on the corresponding elements. It is what programmers do when you ask them to implement a mathematical function.

The category of assemblies is not a topos, but it is good enough to allow interpretation of lots of constructions and of intuitionistic first-order logic. The interpretation is completely standard (predicates are interpreted as subobjects, and everything else follows from that).

Here is the punch line: take an object of interest, say the real numbers. Characterize the real numbers in the language of first-order logic (or higher-order logic if needed, but then we have to use the topos), for instance "the Cauchy-complete archimedean ordered field". Up to isomorphism there is at most one assembly which satisfies this characterization. Therefore, there is no question about how real numbers should be represented! As soon as we say precisely what structure we expect of the reals, the encoding is imposed by the ambient category of assemblies (or the topos).

This trick works over and over again. You can start with the natural numbers, for example take $\mathbb{N}$ to be the free algebra for the signature $(0, 1)$, i.e., the free structure with one constant and one unary operation. Since initial algebras are unique up to unique isomorphisms, the assembly of natural numbers is determined.

We can go on:

• interegers are the free commutative unital ring
• raitonals are the field of fractions of the integers
• complex numbers are the algebraic closure of the reals

Eventually it gets a bit tricky, for instance $L^p[0,1]$ is doable for $p < \infty$, it is not really doable for $L^\infty[0,1]$ (because this space is intuitionistically problematic anyhow), and I don't know whether spaces of distributions have been handled properly. As a rule of thumb, anything that constructive mathematicians can do, you can interpret in realizaiblity to obtain a computable version.

So your hunch was correct: categorical logic (which is just model theory in categories instead of sets) and realizaibility provide the answer.

• I'm pretty sure the NNO in a topos is also characterized by the Peano axioms. Are you saying that the Peano axioms are wrong because assemblies aren't a topos, or maybe because the relevant Peano axioms are second-order or something? May 16, 2018 at 17:19
• Ah good, I wasn’t sure of the top of my head. I edited the answer. May 17, 2018 at 4:56
• The second-order Peano axioms, at least. May 17, 2018 at 5:06
• Yes, I am still wondering what Mike had in mind. @MikeShulman, how precisely would show that all models of PA are isomorphic? (Note that you can only apply induction of formulas expressible in the language of PA, and these cannot refer to objects in the topos.) May 17, 2018 at 6:31
• Ah, that's what I was asking. So what you had originally wasn't wrong, but the emphasis was (to me) misleading: it's not the Peano-ness of the axioms that's wrong but their first-order nature. The NNO in a topos is characterized by the second-order Peano axioms, but not by the first-order ones. And maybe you can't even express the second-order Peano axioms in assemblies (as opposed to the whole realizability topos) because you don't have a truth-value object to quantify over? May 17, 2018 at 17:00

A more directed answer are Joyal's arithmetic universes. It was once quite difficult to find a description of these, but Maria Maietti has proposed an official description.

Maietti, Maria Emilia, Joyal’s arithmetic universe as list-arithmetic pretopos, Theory Appl. Categ. 24, 39-83 (2010). ZBL1245.03111.

However, for your particular question, I think an arithmetic pretopos suffices. The basic idea is as follows.

First, if $\boldsymbol{1} \xrightarrow{o} \mathbf{N} \xleftarrow{\sigma} \mathbf{N}$ is parameterized natural number object in a a category $\mathcal{A}$ with finite products and disjoint coproducts, then all the $k$-ary primitive recursive functions $f$ are representable in $\mathcal{A}$ in the sense that there is a morphism $\mathbf{N}^k \xrightarrow{\phi} \mathbf{N}$ such that $$\require{AMScd}\begin{CD} \boldsymbol{1} @>(\sigma^{n_1}o,\ldots,\sigma^{n_k}o)>> \mathbf{N}^k \\ @| & @VV{\phi}V \\ \boldsymbol{1} @>>{\sigma^{f(n_1,\ldots,n_k)}o}> \mathbf{N} \end{CD}$$ commutes for all $n_1,\ldots,n_k$. In fact, we can build such a category where all the arrows $\mathbb{N}^k \to \mathbb{N}$ represent primitive recursive functions and nothing more.

Since not all computable functions are primitive recursive, this is not sufficient. To get all computable functions, we need to add unbounded search and then close under composition. That is, given a $k+1$-ary primitive recursive $f$ such that $$(\forall n_1,\ldots,n_k)(\exists m)[f(n_1,\ldots,n_k,m) = 0]$$ the function $$g(n_1,\ldots,n_k) = \min\{m : f(n_1,\ldots,n_k,m) = 0\}$$ is computable.

On the categorical side, this can be achieved by requiring the category to be a pretopos. The image factorization, which comes with pretoposes being regular categories, allows one to prove that the category is closed under unbounded search in the internal sense. Namely, if $G \hookrightarrow \mathbf{N}^k \times \mathbf{N}$ is a subobject such that $G \hookrightarrow \mathbf{N}^k \times \mathbf{N} \to \mathbf{N}^k$ is monic and regular epi, then $G$ is isomorphic the graph of a morphism $\mathbf{N}^k \xrightarrow{\gamma} \mathbf{N}$. One recovers unbounded search by taking $G \hookrightarrow \mathbf{N}^k\times\mathbf{N}$ to be the pullback of $\mathbf{N}^k \times \mathbf{N} \xrightarrow{\phi} \mathbf{N}$ along $\boldsymbol{1} \xrightarrow{o} \mathbf{N},$ where $\phi$ represents the primitive recursive function $$\hat{f}(n_1,\ldots,n_k,m) = \begin{cases} 0 & \text{if f(n_1,\ldots,n_k,m) = 0 and \prod_{i=0}^{m-1} f(n_1,\ldots,n_k,i) \neq 0,} \\ 1 & \text{otherwise.} \end{cases}$$

• Is there a k missing in your commutative square? May 17, 2018 at 20:52
• Yes, @DavidRoberts, fixed now. May 17, 2018 at 21:25
• The $G$ described in the last sentence of your answer seems to be the relation defined by $f(\vec n,m)=0$, which need not be the graph of a function. You need to cut down $G$ to contain only one point per fiber; in other words, the projection from $G$ to $\mathbf N^k$ needs to be an isomorphism, not just a regular epi. May 18, 2018 at 0:27
• I think one has to say a bit more to fully answer the OP's question. Here's a start: suppose you have two PNNOs in a suitable category. Since PNNOs are defined by a universal property there is a unique isomorphism between them compatible with the inclusion of $1$ and the successor function. I think the OP's question is something like: what does it mean for this isomorphism itself to be computable? Or is this even a useful / interesting / meaningful question? May 18, 2018 at 6:29

I know this is kind of a trivial answer but I think it's relevant if I understood you.

Ultimately (understanding computability as a property of sets of integers), whether or not a set of rationals is computable depends on how I choose to code them. For instance if I decide to code n/m by the pair (f(n), f(m)) rather than (n,m) where $f(2n)$ is the $n$-th element in $0'$ and $f(2n+1)$ is the $n$-th element not in $0'$ then all the sudden the set of rationals of the form $\frac{1}{o}$ with $o$ odd becomes non-computable.

Now this is a silly example because there is no good reason to use this coding. However, there are examples (representations of measures comes to mind but I'm sure there are better ones) where there are different codings we want to use for different purposes. So there just isn't a fact of the matter as to whether the set of rationals I gave above is computable...it is on one coding and not on another. So I don't see how what you are asking for could possibly work.

It's just that we usually gloss over the fact that the choice of coding also matter because the Church-Turing thesis tells us that in normal circumstances any way we might be inclined to regard as an algorithmic manipulation will correspond to a computable operation if we choose a coding that we also regard as algorithmic (i.e. something humans can do with pen and paper). But that's a contingent philosophical thesis not a mathematically formalizeable claim.

But I worry I'm misunderstanding you and didn't give a good response.

EDIT: I was misunderstanding the question...see the comments below.

• Indeed, coding or some other form of interpretation performed on the putative category needs to be done in order for computable to have meaning. One has to start with declaring some functions as computable (usually successor and at least one constant which may be "unnatural", and projection functions which in a universal algebra context seem "natural") and closing them under some special forms of composition, which forms and functions may be arbitrary but represent some aspects of computability. Gerhard "Thinks Your Response Is Good" Paseman, 2018.05.16. May 16, 2018 at 15:19
• Coding problems exist only for as long as one thinks of coding of bare sets. But as soon as you think of coding in a larger context, and you ask about coding of structures, the problem disappears. See my answer. May 16, 2018 at 16:47
• But the problem is that this isn't a definition of what computability means for a given collection of objects but rather (something like) a particular way to uniquely specify a kind of computability using a choice of relations. In particular, if I understand what you said correctly, I won't get the same answers about what sets of rationals are computable if I consider the rationals under the normal +, * structure or under some structure with very different operations (speaking loosely). I'd regard this as just a sneaky way of specifying a choice of coding. May 16, 2018 at 21:19
• Ok, sneaky is unfair. Notions like this are certainly interesting and mathematically useful but my sense of the original question was a desire to have a unique rigorous notion of computability for binary trees...not the structure of binary trees under operations x,y and z since that question introduces exactly the same kind of judgement about appropriate choices that motivated the desire to avoid specifying a coding. In some sense this comes down to a question of interpretation of the question. May 16, 2018 at 21:27
• @PeterGerdes in your first comment you say, "I won't get the same answers about what sets of rationals are computable if I consider the rationals under the normal +, * structure or under some structure with very different operations (speaking loosely)". This is a good description, I think, of what I was asking for. In category theory (speaking loosely) those two things would be considered different categories - it doesn't really matter that the underlying set is considered to be the rational numbers in both cases. May 17, 2018 at 8:14