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

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

<p>$$ c_i : T_1^i\rightarrow T_2^i\rightarrow \ldots\rightarrow T_{k_1}^i\rightarrow D\rightarrow\ldots\rightarrow D$$</p>

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

<p>$$\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$$</p>

<p>and the operational semantics will be:</p>

<p>$$\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) $$</p>

<p>for each $i$.</p>

<p>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 $$</p>

<p>$$\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)$$</p>

<p>as hoped for (note that the zero constructor has zero arguments!).</p>

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

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

<hr>

<p>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 <a href="https://en.wikipedia.org/wiki/Initial_algebra" rel="nofollow noreferrer">initial algebras</a> of certain functors, often called <em>polynomial functors</em>. The recursor is then just (a variant of) the initial morphism of this algebra, sometimes called a <a href="https://en.wikipedia.org/wiki/Catamorphism" rel="nofollow noreferrer">catamorphism</a> by people trying to confuse things. This morphism exists by construction of the initial algebra.</p>

<p>A <em><a href="https://en.wikipedia.org/wiki/Paramorphism" rel="nofollow noreferrer">paramorphism</a></em> is just the particular variant I described above.</p>

CC BY-SA 3.0
2016-12-17T02:37:35.200Z
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?
N. Virgo
CC BY-SA 3.0
2016-12-17T18:29:58.433Z
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
CC BY-SA 3.0
2016-12-17T18:49:59.927Z
I don't have any elementary references offhand, though I guess [these](https://www.cs.cmu.edu/~fp/courses/15317-f00/handouts/primrec.pdf) slides give a nice soft introduction, and chapter 3 of Ralph Mattes' [thesis](https://www.irit.fr/~Ralph.Matthes/dissertation/matthesdiss.pdf) goes into huge technical detail, though it allows non "first order" inductive types.
cody
CC BY-SA 3.0
2016-12-15T23:26:55.467Z
2016-12-17T18:41:05.380Z
2016-12-17T18:41:05.380Z
cody
<p>I was recently asking this very question, and I found several articles of interest:</p>

<p><a href="http://math.stanford.edu/~feferman/papers/presentedlogics.pdf" rel="nofollow noreferrer">Finitary Inductively Presented Logics</a>: (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.</p>

<p><a href="https://dl.acm.org/citation.cfm?id=806014" rel="nofollow noreferrer">The Complexity of Loop Programs</a>: proves their notion of loop program is equivalent to the primitive recursive functions.</p>

<p><a href="https://academic.oup.com/logcom/article/3/4/401/969823" rel="nofollow noreferrer">Logic Programs for Primitive Recursive Sets</a>: proves their class of logic programs is equivalent to primitive recursive functions.</p>

<p><a href="https://doi.org/10.2307/2275441" rel="nofollow noreferrer">A proof-theoretic characterization of the primitive recursive set functions</a>: proves all primitive recursive functions over a given set are just those definable in a very weak set theory.</p>

CC BY-SA 4.0
2019-03-28T20:17:38.817Z
2019-04-01T01:33:05.450Z
2019-04-01T01:33:05.450Z
Stephen Skeirik
<p>Perhaps you're thinking of the concept of a <strong>paramorphism</strong>?</p>

<p>From <a href="http://maartenfokkinga.github.io/utwente/mmf91m.pdf" rel="nofollow noreferrer">Functional Programming with Bananas, Lenses,
Envelopes and Barbed Wire</a>:</p>

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

<p>\begin{align}
h\; 0 &amp;= b \\
h\; (n + 1) &amp;= n \oplus (h\; n)
\end{align}</p>

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

<p>For lists, a paramorphism would be a function $h$ of the form</p>

<p>\begin{align}
h\; \textsf{nil} &amp;= b \\
h\; (\textsf{cons}\; a\; b) &amp;= a \oplus (b, h\; b)
\end{align}</p>

CC BY-SA 3.0
2016-11-15T00:47:00.903Z
2016-11-15T00:47:00.903Z
user76284
<p>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.</p>

<p>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?</p>

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

<p><strong>update:</strong> I may have found an answer, in a <a href="http://people.csail.mit.edu/kostas/papers/CADE1996.pdf" rel="nofollow noreferrer">paper called Walther Recursion</a>, by McAllester and Arkoudas. (Proceedings of <a href="https://dblp.org/db/conf/cade/cade96" rel="nofollow noreferrer">CADE 1996</a>.) 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.</p>

CC BY-SA 3.0
2016-12-15T08:29:43.930Z
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
CC BY-SA 3.0
2016-08-30T12:18:23.777Z
It's not clear to me what precisely you're looking for. It seems like you're just trying to find [W-types](https://ncatlab.org/nlab/show/W-type), but that may not be it.
Andrej Bauer
CC BY-SA 3.0
2016-08-30T12:39:02.687Z
@AndrejBauer no, that isn't it. I appreciate the comment. I wish I knew how to make my question clearer. I guess I'm looking for something like the Church-Turing thesis, only regarding "models of primitive recursion" instead of models of computation.
N. Virgo
CC BY-SA 3.0
2016-09-02T18:04:00.123Z
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](http://gregorulm.com/godels-system-t-in-agda/) extended to the strictly positive first-order data types with the "usual" recursors.
cody
CC BY-SA 3.0
2016-09-03T01:15:08.533Z
@cody I thought of the approach of mapping data structures onto the natural numbers. It seemed to me that for that to work you'd have to make sure the mapping itself was primitive recursive -- but that would require already having a notion of what it means for a mapping between natural numbers and some other type, thus putting in what I was hoping to get out. It also seems not to give a lot of intuitive insight into what the primitive recursive functions "really are", which is part of what I was hoping to get from this.
N. Virgo
CC BY-SA 3.0
2016-09-03T01:16:16.647Z
@cody as for System T, I don't know about that, and I'll look into it. It seems like that might be part of what I'm looking for.
N. Virgo
CC BY-SA 3.0
2016-09-03T01:22:36.893Z
Hmm, according to http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf , terms in System T always normalise, but it can express functions that are not primitive recursive functions, such as the Ackermann function.
N. Virgo
CC BY-SA 3.0
2016-09-03T14:10:05.553Z
You can restrict the types of the output of the eliminators to be **basic types** if you want to eliminate this "feature".
cody
CC BY-SA 4.0
2018-10-28T17:58:57.190Z
The CADE conference 1996 visit here: https://dblp.org/db/conf/cade/cade96
John Fisher
CC BY-SA 4.0
2018-10-29T13:10:22.460Z
@AndrejBauer: From the question, I think he's just looking for initial algebra semantics of polynomial functors.
Neel Krishnaswami
<computability>
Defining primitive recursive functions over general data types
N. Virgo
# Defining primitive recursive functions over general data types

(Asked by: username_0 on 2016-08-27)

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](http://people.csail.mit.edu/kostas/papers/CADE1996.pdf), by McAllester and Arkoudas. (Proceedings of [CADE 1996](https://dblp.org/db/conf/cade/cade96).) 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.

**Tags:** computability

> **Comments:**
> **username_1**: It's not clear to me what precisely you're looking for. It seems like you're just trying to find [W-types](https://ncatlab.org/nlab/show/W-type), but that may not be it.  
> **username_0**: @AndrejBauer no, that isn't it. I appreciate the comment. I wish I knew how to make my question clearer. I guess I'm looking for something like the Church-Turing thesis, only regarding "models of primitive recursion" instead of models of computation.  
> **username_2**: 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](http://gregorulm.com/godels-system-t-in-agda/) extended to the strictly positive first-order data types with the "usual" recursors.  
> **username_0**: @username_2 I thought of the approach of mapping data structures onto the natural numbers. It seemed to me that for that to work you'd have to make sure the mapping itself was primitive recursive -- but that would require already having a notion of what it means for a mapping between natural numbers and some other type, thus putting in what I was hoping to get out. It also seems not to give a lot of intuitive insight into what the primitive recursive functions "really are", which is part of what I was hoping to get from this.  
> **username_0**: @username_2 as for System T, I don't know about that, and I'll look into it. It seems like that might be part of what I'm looking for.  
> **username_0**: Hmm, according to http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf , terms in System T always normalise, but it can express functions that are not primitive recursive functions, such as the Ackermann function.  
> **username_2**: You can restrict the types of the output of the eliminators to be **basic types** if you want to eliminate this "feature".  
> **username_1**: 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.  
> **username_3**: The CADE conference 1996 visit here: https://dblp.org/db/conf/cade/cade96  
> **username_4**: @AndrejBauer: From the question, I think he's just looking for initial algebra semantics of polynomial functors.  

---

## 3 answers

### Answer by username_2 on 2016-12-15. Score: 5

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](https://en.wikipedia.org/wiki/Initial_algebra) 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](https://en.wikipedia.org/wiki/Catamorphism) by people trying to confuse things. This morphism exists by construction of the initial algebra.

A *[paramorphism](https://en.wikipedia.org/wiki/Paramorphism)* is just the particular variant I described above.

> **Comments:**
> **username_0**: 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?  
> **username_2**: 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.  
> **username_2**: I don't have any elementary references offhand, though I guess [these](https://www.cs.cmu.edu/~fp/courses/15317-f00/handouts/primrec.pdf) slides give a nice soft introduction, and chapter 3 of Ralph Mattes' [thesis](https://www.irit.fr/~Ralph.Matthes/dissertation/matthesdiss.pdf) goes into huge technical detail, though it allows non "first order" inductive types.  

---

### Answer by username_5 on 2019-03-28. Score: 2

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

[Finitary Inductively Presented Logics](http://math.stanford.edu/~feferman/papers/presentedlogics.pdf): (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](https://dl.acm.org/citation.cfm?id=806014): proves their notion of loop program is equivalent to the primitive recursive functions.

[Logic Programs for Primitive Recursive Sets](https://academic.oup.com/logcom/article/3/4/401/969823): proves their class of logic programs is equivalent to primitive recursive functions.

[A proof-theoretic characterization of the primitive recursive set functions](https://doi.org/10.2307/2275441): proves all primitive recursive functions over a given set are just those definable in a very weak set theory.


---

### Answer by username_6 on 2016-11-15. Score: 0

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

From [Functional Programming with Bananas, Lenses,
Envelopes and Barbed Wire](http://maartenfokkinga.github.io/utwente/mmf91m.pdf):

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}


---

