Defining computable functions categorically

Question

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.

Answer 1

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.

Answer 2

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}$$

Answer 3

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.