# Defining primitive recursive functions over general data types

The primitive recursive functions are defined over the natural numbers. However, it seems as if the concept should generalise to other data types, allowing one to talk about primitive recursive functions that map lists to binary trees, for example. By analogy, partial recursive functions over the natural numbers generalise nicely to computable functions on any data type, and I'd like to understand how to make the same kind of generalisation for primitive recursive functions.

Intuitively, if I were to define a simple imperative language that allowed basic operations on, say lists (such as concatenation, taking the head and tail, comparison of elements) and a form of iteration that requires knowing in advance how many iterations will occur (such as iterating over the elements in an immutable list), then such a language should at most be able to compute the primitive recursive functions over lists. But how can I understand this formally, and more specifically, how would I go about proving that my language computes all primitive recursive functions over lists and not just a subset of them?

To be clear, I'm interested in understanding primitive recursive functions as a well-defined class of functions (if indeed they are), rather than just in the operation of primitive recursion itself, which seems straightforward. I'd be interested in pointers to anything that's been written on primitive recursion over general data structures, or indeed in any context other than the natural numbers.

update: I may have found an answer, in a paper called Walther Recursion, by McAllester and Arkoudas. (Proceedings of CADE 1996.) This seems to contain a generalised version of primitive recursion as well as the more powerful Walther recursion. I intend to write a self-answer once I've digested this, but in the meantime this note might be helpful to others with the same question.

• It's not clear to me what precisely you're looking for. It seems like you're just trying to find W-types, but that may not be it. – Andrej Bauer Aug 30 '16 at 12:18
• It's probably useful to note that "ordinary" (tree-like) datatypes can be encoded in a pretty straightforward way into natural numbers, and then the PR functions over the naturals are a pretty good representation of what you might want. Alternately, you could use Gödel’s System T extended to the strictly positive first-order data types with the "usual" recursors. – cody Sep 2 '16 at 18:04
• You can restrict the types of the output of the eliminators to be basic types if you want to eliminate this "feature". – cody Sep 3 '16 at 14:10
• It still seems to me that a form of restricted W-types is what you're looking for. Something like W-types with finite branching and the recursors limited to eliminating into other restricted W-types. – Andrej Bauer Dec 15 '16 at 8:29

In general, in a language with datatypes (like lists, trees, etc) it's easy to describe a language of functions which behave exactly like we expect primitive recursion to behave.

For example if the datatype is $D$, and the constructors $c_1,\ldots, c_n$ have type

$$c_i : T_1^i\rightarrow T_2^i\rightarrow \ldots\rightarrow T_{k_1}^i\rightarrow D\rightarrow\ldots\rightarrow D$$

then the recursor $\mathrm{rec}_D^O$ for output type $O$ will have type

$$\mathrm{rec}^O_D:(T_1^1\rightarrow\ldots T^1_{k_1}\rightarrow D\rightarrow \ldots\rightarrow D\rightarrow O\rightarrow \ldots\rightarrow O)\rightarrow\ldots\rightarrow D\rightarrow O$$

and the operational semantics will be:

$$\mathrm{rec}^O_D\ f_1\ \ldots\ f_n\ (c_i\ t_1\ldots t_{k_i}\ d_1\ldots d_m)\rightarrow\\ f_i\ t_1\ldots t_{k_i}\ (\mathrm{rec}^O_D\ f_1\ldots\ f_n\ d_1)\ldots (\mathrm{rec}^O_D\ f_1\ldots f_n\ d_m)$$

for each $i$.

Something of a mouth-full! At least for natural numbers, we indeed get $$\mathrm{rec}_{\mathbb{N}}^O:(\mathbb{N}\rightarrow O\rightarrow O)\rightarrow O\rightarrow\mathbb{N}\rightarrow O$$

$$\mathrm{rec}^O_{\mathbb{N}}\ f_0\ f_1\ 0 \rightarrow f_1\ 0$$ and $$\mathrm{rec}^O_{\mathbb{N}}\ f_0\ f_1\ (S\ n)\rightarrow f_0\ n\ (\mathrm{rec}^O_{\mathbb{N}}\ f_0\ f_1\ n)$$

as hoped for (note that the zero constructor has zero arguments!).

If now we allow for constant functions and projections, and allow arbitrary uses of $\mathrm{rec}^O_D$ for non-function types $O$, then you have exactly primitive recursion.

Reassuringly, if all the $T^j_i$s are non-functional as well, then the usual Gödel encoding of the datatype gives the same primitive recursive functions.

It would be nice to have a more elegant description of this process though. That's were Carlos' answer comes in: these datatypes can be described more elegantly in category theory as the initial algebras of certain functors, often called polynomial functors. The recursor is then just (a variant of) the initial morphism of this algebra, sometimes called a catamorphism by people trying to confuse things. This morphism exists by construction of the initial algebra.

A paramorphism is just the particular variant I described above.

• I'm afraid this is somewhat beyond me. Why were we hoping to get $\mathrm{rec}_{\mathbb{N}}^O:(\mathbb{N}\rightarrow O\rightarrow O)\rightarrow O\rightarrow\mathbb{N}\rightarrow O$ as the type signature? Does that automatically mean it represents primitive recursiveness? (I have a hard time imagining how that could be read off from only the type of a function.) I'm familiar with type theory to the extent that I can program in Haskell, but I'm not familiar with the formalism you're using here. Where can I go to read enough background to understand what you wrote? – Nathaniel Dec 17 '16 at 2:37
• The type of $\mathrm{rec}_{\mathbb{N}}$ follows from the more general schema above. It represents primitive recursiveness because the operational semantics represents the recursion operation from the definition of PR functions. I haven't explained the operational semantics though, so I'll expand my comment. – cody Dec 17 '16 at 18:29
• I don't have any elementary references offhand, though I guess these slides give a nice soft introduction, and chapter 3 of Ralph Mattes' thesis goes into huge technical detail, though it allows non "first order" inductive types. – cody Dec 17 '16 at 18:49

I was recently asking this very question, and I found several articles of interest:

Finitary Inductively Presented Logics: (a) defines a logic which provides a generic notion of primitive recursion over any datatype satisfying certain requirements (b) proves this logic is a conservative extension of primitive recursive arithmetic.

The Complexity of Loop Programs: proves their notion of loop program is equivalent to the primitive recursive functions.

Logic Programs for Primitive Recursive Sets: proves their class of logic programs is equivalent to primitive recursive functions.

A proof-theoretic characterization of the primitive recursive set functions: proves all primitive recursive functions over a given set are just those definable in a very weak set theory.

Perhaps you're thinking of the concept of a paramorphism?

For natural numbers a paramorphism is a function $h = (b, \oplus)$ of the form

\begin{align} h\; 0 &= b \\ h\; (n + 1) &= n \oplus (h\; n) \end{align}

For example, the factorial function has $b = 1$ and $n \oplus m = (n + 1) \times m$.

For lists, a paramorphism would be a function $h$ of the form

\begin{align} h\; \textsf{nil} &= b \\ h\; (\textsf{cons}\; a\; b) &= a \oplus (b, h\; b) \end{align}