6
$\begingroup$

It is (I believe) a very easy exercise to prove that the general recursive functions over the natural number object $N$ form a category. But what sort of category is it? From the fact that one can prove the Recursion Theorem one might surmise that the category of general recusive functions over $N$ is cartesian closed, but what other category-theoretic properties does it have?

Question 1: Is it possible (for example) to characterize the category of general recursive functions over $N$ without having to deem specific functions as 'recursive' (as Kleene does in his papers)?

Furthermore, we now have types of 'recursiveness' over various structures, i.e. $\alpha$-recursive functions, $\beta$-recursive functions ($\alpha$-,$\beta$-recurision over the ordinals); Koepke and Koerwien's $\ast$-recursive functions over the ordinals (which characterize the constructible universe $L$), and Infinite Time Turing Machines; Sacks' $E$-recursion; Recursive functionals and quantifiers of finite type (Kleene); primitive recursive set functions and rudimentary set functions (Jensen, and others for studying the fine structure of $L$); abstract first-order computability (Moschovakis), to name but a few.

Question 2: Can (or has) category theory (been able to) elucidate the structural interrelations between the various types of recursion?

Since I am certain that there is a subfield of category theory devoted to answering these types of questions (and probably already have answered some of these questions), I would be interested in obtaining a list of survey articles devoted to this subdiscipline, and (of course) the answers to the two questions I asked (the second can be answered from the survey articles by giving a few concrete examples).

Thanks in advance for any and all help given.

$\endgroup$
  • $\begingroup$ It may be that arithmetic universes are a candidate, or at least the arithmetic pretoposes of Maietti, which seem like the sort of structure engineered to allow a structural version of Gödel coding. $\endgroup$ – David Roberts Feb 27 '17 at 11:06
  • $\begingroup$ @DavidRoberts: Would the class $Ord$ of all ordinals be deemed an 'arithmetic universe'? $\endgroup$ – Thomas Benjamin Feb 27 '17 at 12:31
  • $\begingroup$ An arithmetic universe is a kind of category. Just specifying the objects is insufficient. That said, I don't know if there is one with objects the ordinals. $\endgroup$ – David Roberts Feb 27 '17 at 20:03
  • $\begingroup$ @DavidRoberts: (Silly question, maybe); If one considers the proper class of well-ordered sets and the morphisms between them as a category ($WO$), then is the proper class $Ord$ and its requisite morphisms the skeletal subcategory of $WO$ (sorry if I am not formulating the concept correctly--I just need advice on how to properly formulate the concept, thanks)? $\endgroup$ – Thomas Benjamin Mar 3 '17 at 8:23
  • $\begingroup$ Yes, I believe so. There is an isomorphism of well-ordered sets between a pair of ordinal iff the ordinals (I assume you have picked a construction, say the von Neumann one) are identical, if I'm not mistaken. I don't know how this helps your original question, though. $\endgroup$ – David Roberts Mar 3 '17 at 10:24
7
$\begingroup$

I am not sure this is what you are looking for but I think that the following paper may provide an answer to your question 1:

J. Robin B. Cockett, Pieter J. W. Hofstra: Introduction to Turing categories. Ann. Pure Appl. Logic 156(2-3): 183-209 (2008)

It gives a categorical axiomatization of computability in arbitrary categories (not just sets and partial maps). The basic notion is that of Turing category which, in a nutshell, is:

  • a restriction category, that is, a "category of partial maps": for every $f:A\to B$, there is a monic $\overline f:A\to A$ which morally represents the domain of $f$ as a "partial identity map" (subject to some axioms); total maps are arrows $f:A\to B$ such that $\overline f=\mathrm{id}_A$;

  • it has a notion of product that interacts well with the partiality structure;

  • it has a Turing object, which is morally an "object of programs"; technically, it is a sort of "universal internal hom": it is an object $T$ together with a map $\mathrm{eval}_{A,B}:T\times A\to B$ for every objects $A,B$, such that, for all $f:\Gamma\times A\to B$, there is a total map $f^\bullet:\Gamma\to T$ such that $$\mathrm{eval}_{A,B}\circ (f^\bullet\times \mathrm{id}_A)=f.$$ The map $f^\bullet$ is called a code of $f$ and is not required to be unique (morally, it is a program parametric in $\Gamma$).

The category whose objects are powers of $\mathbb N$ and whose arrows are partial recursive functions is the prototypical example of Turing category ($\mathbb N$ is a Turing object, seen as the set of codes of recursive functions).

Apart from the above paper, there is also this survey by Robin Cockett in which he shows how some of the basic theorems of computability theory may be proved in the framework of Turing categories.

By the way, Turing categories are not the only proposal to axiomatize computability categorically; Cockett and Hofstra mention previous work in the introduction to their paper, which you may also find of interest.

As far as your question 2 is concerned, I don't think Cockett and coauthors studied the extensions of recursive functions that you mention. However, they did turn their attention to sub-recursive settings (i.e., complexity theory), and found out that there are Turing categories whose total maps correspond to well-known complexity classes (polynomial time, logspace). If I am not mistaken, this is done in the following two papers:

Robin Cockett, Joaquín Díaz-Boïls, Jonathan Gallagher, Pavel Hrubes: Timed Sets, Functional Complexity, and Computability. Electr. Notes Theor. Comput. Sci. 286: 117-137 (2012)

J. Robin B. Cockett, Pieter J. W. Hofstra, Pavel Hrubes: Total Maps of Turing Categories. Electr. Notes Theor. Comput. Sci. 308: 129-146 (2014)

$\endgroup$
  • $\begingroup$ Actually, if you read the Introduction to the Cockett-Hofstra paper you mention, they state that the Uniformly Reflexive Structures of Wagner and Strong; and Moschovakis' work on abstract first-order computability and his work on (pre)computation theories..."single out a class of well-behaved combinatory structures and prove the elementary recursion theoretic results for the objects in this class...in hindsight, this may be seen as the study of the class of decidable partial combinatory algebras in the category of sets; as such, they are examples of the kind of structures $\endgroup$ – Thomas Benjamin Feb 28 '17 at 12:05
  • $\begingroup$ (cont.) we shall be considering in this paper". This shows (and Cockett discusses recursion categories in the survey article you provide in your answer) that Turing categories probably relate (in some sense) all the variants of 'recursiveness' I mention in my question (how, and how not, have the makings of a nice research programme....). Thanks. $\endgroup$ – Thomas Benjamin Feb 28 '17 at 12:16
  • $\begingroup$ Good to know! I'm glad you found the paper interesting. $\endgroup$ – Damiano Mazza Feb 28 '17 at 20:36
  • 1
    $\begingroup$ Conjecture: The category $Set$ has a unique large subcategory that is a Turing category, and that is the constructible universe $L$. $\endgroup$ – Thomas Benjamin Mar 3 '17 at 7:57
  • $\begingroup$ @ThomasBenjamin Why on earth should that be true? Just because $L$ and computability have a certain affinity? $\endgroup$ – Noah Schweber Aug 14 '17 at 16:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.