Defining primitive recursive functions over general data types

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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

From Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire:

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}