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.
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.