General Recursive Functions

In this post, I discuss one way of deriving the definition of general recursive functions, which comprise an important model of computation (which is equivalent to other major models of computation, such as Turing machines, the Lambda Calculus, register machines, etc.).

The general recursive functions are functions of natural numbers. First, the algebraic nature of the natural numbers is analyzed, resulting in the definition of primitive recursion, then this perspective is dualized to obtain a coalgebraic analysis of the extended natural numbers, resulting in the definition of primitive corecursion. Finally, primitive recursion and primitive corecursion are combined, resulting in general recursion.

Algebra

It is possible to characterize the natural numbers algebraically, that is, by the operations we may perform upon them in order to produce other natural numbers.

The natural numbers can be characterized by the fact that \(0\) is the "initial" natural number and that we may continually produce natural numbers by adding one to any given natural number. Thus, the natural numbers \(\mathbb{N}\) contain a designated constant \(0 \in \mathbb{N}\) and a successor operation \(s : \mathbb{N} \rightarrow \mathbb{N}\) which "adds one" to a number to produce another. This gives rise to a sequence

\[0,s(0),s(s(0)),s(s(s(0))),\dots\]

We may think of the natural numbers in the following manner: we begin with a set consisting of just \(0\), then add only what is strictly necessary according to the rules (namely, the successor): thus we must add \(s(0)\), and then \(s(s(0))\), etc. The natural numbers are the "smallest" set closed under the successor operation. In what follows, we will formalize this intuition.

Definition (Algebra). An algebra \(\mathcal{A}\) in a category \(\mathbf{C}\) consists of a functor \(\Sigma : \mathbf{C} \rightarrow \mathbf{C}\) called the signature of the algebra, an object \(A\) of \(\mathbf{C}\) called the carrier of the algebra, and a morphism \(f^{\mathcal{A}} : \Sigma(A) \rightarrow A\) called the operation of the algebra.

An algebra for a given signature \(\Sigma\) is often called a \(\Sigma\)-algebra, though mention of the signature may be omitted if it is clear from context. An algebra is often written as \(\mathcal{A} = (\Sigma,A,f^{\mathcal{A}})\), or, if the signature is implicit, simply as \(\mathcal{A} = (A,f^{\mathcal{A}})\).

The signature which characterizes the natural numbers is

\[\Sigma(A) = A + 1.\]

For now we work in the category \(\mathbf{Set}\). The set \(1\) is any terminal element in \(\mathbf{Set}\), i.e. any singleton set \(\{*\}\) whose sole element is denoted \(*\) since its definition is immaterial. A function \(c : 1 \rightarrow A\) models a constant within the set (since \(c(*) \in A\) is the given constant, i.e. \(c\) "selects" the constant). In particular, the constant \(z : 1 \rightarrow \mathbb{N}\) selects the element designated to represent zero (i.e. \(z(*) = 0\), where we write \(0\) to represent this element).

The notation \(A+1\) indicates the coproduct of \(A\) and \(1\), which represents the disjoint union \(A \sqcup 1\) of each set. Often, the disjoint union is defined to be \(A \sqcup B = \{l(a) : a \in A\} \cup \{r(b) : b \in B\}\) where \(l\) and \(r\) are some labeling functions which ensure disjointness by assigning distinct labels to each element which indicate their provenance, e.g. \(l(a) = (A,a)\) and \(r(b) = (B,b)\). However, if the sets are already disjoint, then their union \(A \cup B\) is isomorphic to their disjoint union, so the union can be take as their coproduct (coproducts, like any universal construction, are only defined up to isomorphism). Subsequently, since we work with disjoint sets, we will just designate their union as their coproduct.

For now, we assume that there is some set \(\mathbb{N}\) which carries an initial algebra (see below) for this signature.

The function \(s : \mathbb{N} \rightarrow \mathbb{N}\) indicates the successor of a natural number (i.e., \(s(n)\) is the successor of \(n\), the number \(n+1\)).

Any operation on this signature is thus a function \(f^{\mathcal{A}} : A+1 \rightarrow A\). In the initial algebra (see below), this operation will be the operation \([s,z] : \mathbb{N}+1 \rightarrow \mathbb{N}\) induced by the universal property of coproducts. In \(\mathbf{Set}\), this is typically defined as follows:

\[\begin{cases}[s,z](l(n)) = s(n) \\ [s,z](r(*)) = z(*) = 0.\end{cases}\]

Again, since we will assume that the sets are disjoint and use their union as their coproduct, the labels \(l\) and \(r\) can be suppressed, so that we simply write

\[[s,z](n) = \begin{cases}[s,z](n) = s(n) & \text{for}~n\in\mathbb{N} \\ [s,z](*) = z(*) = 0 & \text{for}~ * .\end{cases}\]

Thus, \([s,z]\) just applies the successor to natural numbers and selects \(0\) for \(*\).

In every mathematical subject, there is a notion of a homomorphism, i.e. a "structure-preserving" map between objects. There is likewise such a notion for algebras.

Definition (Homomorphism of Algebras). A homomorphism between \(\Sigma\)-algebras \(\mathcal{A} = (A,f^{\mathcal{A}})\) and \(\mathcal{B} = (B,f^{\mathcal{B}})\) is a morphism \(\varphi : A \rightarrow B\) such that \(\varphi \circ f^{\mathcal{A}} = f^{\mathcal{B}} \circ \Sigma(\varphi)\), that is, the following diagram commutes:

\begin{CD} \Sigma(A) @>\Sigma(\varphi)>> \Sigma(B)\\ @Vf^{\mathcal{A}}VV @VVf^{\mathcal{B}}V\\ A @>>\varphi> B \end{CD}

Thus, for the signature \(\Sigma(A) = A + 1\), a homomorphism is a function \(\varphi : A \rightarrow B\) such that the following diagram commutes:

\begin{CD} A+1 @>\varphi+\mathrm{id}>> B+1\\ @Vf^{\mathcal{A}}VV @VVf^{\mathcal{B}}V\\ A @>>\varphi> B \end{CD}

In other words, it is a map between the respective carriers \(A\) and \(B\) which preserves the operations of the algebra. The map \(\varphi + \mathrm{id}\) is the "lifting" of the map \(\varphi\) by the functor \(\Sigma = (-)+1\). The map \(\varphi + \mathrm{id}\) is often written as \(\varphi + 1\) with the understanding that the object \(1\) in the context of a morphism represents the identity map \(id : 1 \rightarrow 1\).

Algebras for a given signature together with homomorphisms comprise a category.

Definition (Category of Algebras). The category of algebras \(\Sigma\)-\(\mathbf{Alg}\) for a signature \(\Sigma\) has as its objects all \(\Sigma\)-algebras and as its morphisms all \(\Sigma\)-algebra homomorphisms.

The initial algebra is an important algebra which is, in a certain sense, the "least" or "smallest" algebra (and it enjoys an important universal property).

Definition (Initial Algebra). An initial algebra is an initial object in the category \(\Sigma\)-\(\mathbf{Alg}\). Explicitly, an initial algebra is an algebra \(\mathcal{I}[\Sigma] = (I[\Sigma],f^{\mathcal{I}[\Sigma]})\) such that, for every \(\Sigma\)-algebra \(\mathcal{A} = (A,f^{\mathcal{A}})\), there exists a unique homomorphism \(\varphi : \mathcal{I}[\Sigma] \rightarrow \mathcal{A}\), that is, there exists a unique morphism \(\varphi : I[\Sigma] \rightarrow A\) such that the following diagram commutes:

\begin{CD} \Sigma(I[\Sigma]) @>\Sigma(\varphi)>> \Sigma(A)\\ @Vf^{\mathcal{I}[\Sigma]}VV @VVf^{A}V\\ I[\Sigma] @>>\exists!\varphi> A \end{CD}

Sometimes this is understood, in terms of sets, as a concise way of expressing two properties, sometimes called "no junk" and "no noise": "no junk" means that the carrier of the initial algebra should contain only the natural numbers are nothing else. "No noise" means that the natural numbers should be freely generated (i.e. there should be no extraneous relations imposed on the natural numbers, such as \(s(s(0)) = s(0)\), so that each application of \(s\) generates a "new" number). The uniqueness of the induced homomorphism \(\varphi\) guarantees the "no junk" condition, and the existence of \(\varphi\) ensures the "no noise" condition.

Consider again the following signature:

\[\Sigma(A) = A + 1\]

Now, suppose, for the moment, that there exists an initial algebra

\[\mathcal{N} = (\Sigma, \mathbb{N}, [s,z]).\]

This means that, for any other algebra \(\mathcal{A} = (A,f^{\mathcal{A}})\), the following diagram commutes:

\begin{CD} \mathbb{N}+1 @>\varphi+1>> A+1\\ @V[s,z]VV @VVf^{\mathcal{A}}V\\ \mathbb{N} @>>\exists!\varphi> A \end{CD}

This means that

• \(\varphi(0) = c\)
• \(\varphi(s(n)) = f^{\mathcal{A}}(\varphi(n)),\)

where \(c = f^{\mathcal{A}}(*)\) is some constant.

This is sometimes called "structural recursion". When the other algebra is also carried by \(\mathbb{N}\) but has a different operation, say, it is the algebra

\[\mathcal{A} = (\Sigma, \mathbb{N}, f^{\mathcal{A}}),\]

then this yields the following:

\begin{CD} \mathbb{N}+1 @>\varphi+1>> \mathbb{N}+1\\ @V[s,z]VV @VVf^{\mathcal{A}}V\\ \mathbb{N} @>>\exists!\varphi> \mathbb{N} \end{CD}

Again, this means that

• \(\varphi(0) = c\),
• \(\varphi(s(n)) = f^{\mathcal{A}}(\varphi(n))\),

but, this time, the codomain of this function is \(\mathbb{N}\). Such functions are called primitive recursive functions.

We will later extend this definition to permit additional arguments.

Here we will give a few examples of primitive recursive functions. Addition is a prime example; the function \(m+(-)\), i.e. the map \(n \mapsto m + n\) can be defined by primitive recursion as follows:

\[\begin{cases}m+0 = m \\ m+(s(n)) = s(m+n).\end{cases}\]

In this example, the operation is \(f^{\mathcal{A}} = [s,c]\) (where \(c\) is the constant map \(c(*) = m\)) so that the commutative diagram is

\begin{CD} \mathbb{N}+1 @>(m+(-)) + \mathrm{id}>> \mathbb{N}+1\\ @V[s,z]VV @VV[s,c]V\\ \mathbb{N} @>>\exists!m+(-)> \mathbb{N} \end{CD}

Thus, for instance, the following calculation expresses the fact that \(3+2=5\):

\begin{align}s(s(s(0)))+s(s(0)) &= s(s(s(s(0)))+s(0)) \\&= s(s(s(s(s(0)))+0)) \\&= s(s(s(s(s(0))))).\end{align}

Because the map \(\varphi\) is always completely determined by the operation \(f^{\mathcal{A}}\), it is often written as \(\mathrm{rec}_{\mathbb{N}}(f^{\mathcal{A}})\) ("rec" is short for "recursion") or \(\mathrm{fold}(f^{\mathcal{A}})\) ("fold" colloquially refers to a structurally-recursive operation in computer science terminology). Thus, the commutative diagram becomes:

\begin{CD} \mathbb{N}+1 @>\mathrm{rec}_{\mathbb{N}}(f^{\mathcal{A}}) + \mathrm{id}>> \mathbb{N}+1\\ @V[s,z]VV @VVf^{\mathcal{A}}V\\ \mathbb{N} @>>\exists!\mathrm{rec}_{\mathbb{N}}(f^{\mathcal{A}})> \mathbb{N} \end{CD}

The universal property of the initial algebra only determines the natural numbers up to isomorphism. However, in set theory, a constructive definition of the natural numbers is usually given which arbitrarily designates a particular set as the definition of the natural numbers. The usual definition (due to John von Neumann) is that a natural number \(n\) is the set of all natural numbers less than \(n\), i.e.:

• \(0 = \emptyset\),
• \(s(n) = n \cup \{n\}\)

Thus,

• \(0 = \emptyset\),
• \(1 = s(0) = 0 \cup \{0\} = \{0\}\),
• \(2 = s(1) = 1 \cup \{ 1 \} = \{0, 1\}\)
• \(3 = s(2) = 2 \cup \{2\} = \{0,1,2\}\)
• ...etc.

Coalgebra

Every construction in category theory can be "dualized" essentially by "inverting the arrows". Thus, algebras can be dualized to coalgebras.

Definition (Coalgebra). A coalgebra \(\mathcal{A}\) in a category \(\mathbf{C}\) consists of a functor \(\Sigma : \mathbf{C} \rightarrow \mathbf{C}\) called the signature of the coalgebra, an object \(A\) of \(\mathbf{C}\) called the carrier of the coalgebra, and a morphism \(f_{\mathcal{A}} : A \rightarrow \Sigma(A)\) called the operation of the coalgebra.

Notice that the operation is inverted: it is a map with signature \(A \rightarrow \Sigma(A)\). Algebraic operations are often called constructors since they "construct" terms of the algebra by successively applying the operations of the algebra to the constants of the algebra, such as \(s(s(s(0)))\). Coalgebraic operations are often called destructors since they can be conceived as operations which "take apart" a term of the coalgebra; in the case of the extended natural numbers \(\bar{\mathbb{N}}\) (the dual of the natural numbers), the operation has signature \(\bar{\mathbb{N}} \rightarrow \bar{\mathbb{N}}+1\); as we will determine below, this operation either produces the predecessor of an (extended) natural number or the term \(*\).

Likewise, we can define the appropriate notion of a homomorphism for coalgebras.

Definition (Homomorphism of Coalgebras). A homomorphism between \(\Sigma\)-coalgebras \(\mathcal{A} = (A,f_{\mathcal{A}})\) and \(\mathcal{B} = (B, f_{\mathcal{B}})\) is a morphism \(\varphi : A \rightarrow B\) such that \(f_{\mathcal{B}} \circ \varphi = \Sigma(\varphi) \circ f_{\mathcal{A}}\), that is, the following diagram commutes:

\begin{CD} \Sigma(A) @>\Sigma(\varphi)>> \Sigma(B) \\ @Af_{\mathcal{A}}AA @AAf_{\mathcal{B}}A\\ A @>>\varphi> B \end{CD}

Definition (Category of Coalgebras). The category \(\mathbf{CoAlg}(\Sigma)\) consists of all \(\Sigma\)-coalgebras and homomorphisms between them.

Definition (Final Coalgebra). A final coalgebra is a final object in the category \(\mathbf{CoAlg}(\Sigma)\). Explicitly, a final coalgebra is a \(\Sigma\)-coalgebra \(\mathcal{F}[\Sigma] = (F[\Sigma],f_{\mathcal{F}[\Sigma]})\) such that, for every \(\Sigma\)-coalgebra \(\mathcal{A} = (A,f_{\mathcal{A}})\) there exists a unique homomorphism \(\varphi : \mathcal{A} \rightarrow \mathcal{F}[\Sigma]\), that is, there exists a unique morphism \(\varphi : A \rightarrow F[\Sigma]\) such that the following diagram commutes:

\begin{CD} \Sigma(A) @>\Sigma(\varphi)>> \Sigma(F[\Sigma]) \\ @Af_{\mathcal{A}}AA @AAf_{\mathcal{B}}A\\ A @>>\exists!\varphi> F[\Sigma] \end{CD}

We may think of the extended natural numbers (the dual of the natural numbers) as follows: we apply the predecessor operation (the "inverse" of the successor operation). An extended natural number might not have any predecessor (intuitively, \(0\) has no predecessor), so, sometimes, after a finite number of applications \(p(p(\dots(p(n))))\) of the predecessor function to an extended natural number \(n\), the predecessor operation yields some token value \(*\) which indicates that there is no predecessor. Thus, for instance, the number \(3\) would be represented by the fact that it takes \(3\) applications of the predecessor operation to "escape" from the set of extended natural numbers and finally produce \(*\). However, there is nothing which requires this process to terminate, so there is a special extended natural number \(\infty\) such that \(p(\infty) = \infty\), such that the chain of applications \(p(p(\dots p(\infty)))\) continues indefinitely.

Next, we will define the extended natural numbers \(\bar{\mathbb{N}}\) (also called the co-natural numbers). We will use the same signature as the natural numbers, but we will define the extended natural numbers as the carrier of the final coalgebra for this signature together with a coalgebraic operation which is essentially the inverse of the algebraic operation. In particular, this means that the following diagram commutes:

\begin{CD} \bar{\mathbb{N}}+1 @>\varphi+1>> \bar{\mathbb{N}}+1 \\ @Af_{\mathcal{A}}AA @AAf_{\mathcal{N}}A\\ \bar{\mathbb{N}} @>>\exists!\varphi> \bar{\mathbb{N}} \end{CD}

The induced homormorphism is often called \(\mathrm{corec}_{\bar{\mathbb{N}}}(f_{\mathcal{A}})\) or \(\mathrm{unfold}(f_{\mathcal{A}})\), so that the diagram becomes

\begin{CD} \bar{\mathbb{N}}+1 @>\mathrm{corec}_{\bar{\mathbb{N}}}(f_{\mathcal{A}})+1>> \bar{\mathbb{N}}+1 \\ @Af_{\mathcal{A}}AA @AAf_{\mathcal{N}}A\\ \bar{\mathbb{N}} @>>\exists!\mathrm{corec}_{\bar{\mathbb{N}}}(f_{\mathcal{A}})> \bar{\mathbb{N}} \end{CD}

Each induced function \(\mathrm{corec}_{\bar{\mathbb{N}}}(f_{\mathcal{A}})\) is called a primitive corecursive function.

What should the operation \(f_{\bar{\mathcal{N}}}\) be? Loosely speaking, the operation will be the "inverse" of the operation \([s,z]\) defined for the natural numbers. Thus, it should map each extended natural number to its predecessor (since the predecessor is the inverse of the successor) and it should map \(0\) to \(*\). We can thus define the mapping \(f_{\bar{\mathcal{N}}}\) as follows, where \(p\) is the predecessor map:

\[f_{\bar{\mathcal{N}}}(n) = \begin{cases}* & \text{if}~n=0 \\ p(n) & \text{otherwise.}\end{cases}\]

Our goal is to determine the form of \(\varphi\). First, note that

\[f_{\bar{\mathcal{N}}}(\varphi(n)) = \begin{cases}* & \text{if}~\varphi(n) = 0 \\ p(\varphi(n)) & \text{otherwise.}\end{cases}\]

Next, note that

\[(\varphi+1)(f_{\mathcal{A}}(n)) = \begin{cases}* & \text{if}~f_{\mathcal{A}}(n) = * \\ \varphi(f_{\mathcal{A}}(n)) & \text{otherwise.}\end{cases}\]

Since \(f_{\bar{\mathcal{N}}} \circ \varphi = (\varphi + 1) \circ f_{\mathcal{A}}\), it follows that

\[\begin{cases}\varphi(n) = 0 & \text{if}~ f_{\mathcal{A}}(n)=* \\ p(\varphi(n)) = \varphi( f_{\mathcal{A}}(n)) & \text{otherwise.}\end{cases}\]

Note that, if \(f_{\mathcal{A}}\) has any fixed point, i.e. an extended natural number \(a\) such that \(f_{\mathcal{A}}(a) = a\), then so must \(p\), since \(p(\varphi(a)) = \varphi( f_{\mathcal{A}}(a))\) implies that \(p(\varphi(a)) = \varphi(a)\) and thus \(\varphi(a)\) is a fixed point of \(p\). This fixed point is typically denoted \(\infty\) (since we think of an extended natural number which is its own predecessor as somehow "infinite") and so \(p(\infty)=\infty\). Thus, we may now define the predecessor function:

\[p(n) = \begin{cases}* & \text{if}~n=0 \\ n-1 & \text{if}~n>0 \\ \infty & \text{if}~n=\infty.\end{cases}\]

Note again that we informally write \(n-1\) here, although, technically, we have not defined subtraction and it would be circular to define the predecessor in terms of subtraction. Instead, formally, \(n-1\) represents \(\mathrm{PRED}(n)\), where \(\mathrm{PRED}\) is whatever we designate as the definition of the predecessor. In set theory, the usual definition is that

\[\mathrm{PRED}(n) = \bigcup n\]

so that

• \(\mathrm{PRED}(0) = \bigcup 0 = 0\),
• \(\mathrm{PRED}(1) = \bigcup 1 = \bigcup \{0\} = 0\),
• \(\mathrm{PRED}(2) = \bigcup 2 = \bigcup \{0,1\} = 1\),
• ...etc.

Note also that if we define \(\infty = \mathbb{N}\) so that \(\bar{\mathbb{N}} = \mathbb{N} \cup \{\mathbb{N}\}\) then \(\mathrm{PRED}(\infty) = \bigcup \mathbb{N} = \mathbb{N}\). It is in this sense that \(\infty\) is "infinite" also: we can model it by the infinite set \(\mathbb{N}\). The operation \(p\) is distinct from \(\mathrm{PRED}\) since it maps \(0\) to \(*\) and \(\mathrm{PRED}\) is has as its codomain the extended natural numbers (so it maps \(0\) to \(0\)).

Note, however, that the usual definition of the successor \(s\) no longer works for \(\infty\), since \(s(\infty) = \infty \cup \{\infty\} = \mathbb{N} \cup \{\mathbb{N}\} = \bar{\mathbb{N}}\), but we want \(s(\infty) = \infty\). If we permit non-well-founded sets, i.e. sets that are elements of themselves, then we could let \(\bar{\mathbb{N}} \in \bar{\mathbb{N}}\) and define \(\infty = \bar{\mathbb{N}}\) and thus \(s(\infty) = \bar{\mathbb{N}} \cup \{\bar{\mathbb{N}}\} = \bar{\mathbb{N}}\), which works. However, when working in a set theory (e.g. ZFC) which requires well-founded sets, we would have to redefine the successor operation such that \(s(\infty) = \infty\). Thus, for instance, we could define \(\bar{\mathbb{N}} = \mathbb{N} \cup \{\infty\}\), keep the definition of \(s\) and \(\mathrm{PRED}\) for elements other than \(\infty\), and declare that \(s(\infty) = \mathrm{PRED}(\infty) = \infty\) (where \(\infty\) is any distinct element).

We could also write

\[\varphi(n) = \begin{cases}0 & \text{if}~ f_{\mathcal{A}}=* \\ \varphi( f_{\mathcal{A}}(n)) + 1 & \text{otherwise,}\end{cases}\]

where \(n+1\) here informally refers to the successor of \(n\).

Let's consider what this function \(\varphi\) represents. Often, it is convenient to think of coalgebraic definitions in terms of states. Each extended natural number is an individual state. We can think of \(n\) as the initial state, and we can think of \(f_{\mathcal{A}}\) as a function which indicates the next state in a state machine (i.e., \(f_{\mathcal{A}}\) is the transition function). Then, the sequence of invocations

\[n, f_{\mathcal{A}}(n), f_{\mathcal{A}}(f_{\mathcal{A}}(n)),\dots\]

indicates the evolution of this state machine. The element \(*\) indicates that the terminal state of the state machine has been encountered. Thus, if the state machine evolves and reaches the terminal state, then \(\varphi\) outputs a count of how many state transitions occurred. If, however, the state machine never terminates, then it outputs \(\infty\).

Now, although this "counting" function is the canonical primitive corecursive function, it is often much more convenient to express it as a minimization function \(\mu(f)\). We can define this as a primitive corecursive function as follows:

\[\mu(f) = \hat{\mu}(f)(0),\]

where

\[\hat{\mu}(f)(n) = \begin{cases}n & \text{if}~\hat{f}(n) = * \\ \hat{\mu}(f)(\hat{f}(n))+1 & \text{otherwise,}\end{cases}\]

and

\[\hat{f} = \begin{cases}* & \text{if}~f(n)=0 \\ n+1 & \text{otherwise}.\end{cases}\]

Thinking in terms of state machines, this state machine transitions sequentially to states

\[0,1,2,3,\dots\]

The machine stops once a terminal state (i.e., one for which \(f(n) = 0\) is reached. Thus, the minimization function computes the least number \(n\) for which \(f(n)=0\), or \(\infty\) if there is no such element.

Thus, we can implement the \(\mu\) operator using primitive corecursion. Conversely, we can also implement primitive corecursion using the \(\mu\) operator as follows:

\[(\mathrm{corec}_{\bar{\mathbb{N}}}f)(n) = \mu(f^{(n)}),\]

where \(f^{(n)}(m)\) is defined by primitive recursion as \(f^{(0)}(m) = m\) and \(f^{(n+1)}(m) = \hat{f}(f^{(n)}(m))\), where

\[\hat{f}(n) = \begin{cases}0 & \text{if}~f(n)=* \\ f(n) & \text{otherwise}.\end{cases}\]

Thus, in this sense, \(\mathrm{corec}_{\bar{\mathbb{N}}}f\) and \(\mu(f)\) are equivalent: each can be implemented in terms of the other, so every primitive corecursive function which can be defined in terms of one can be defined in terms of the other.

Definition (Bisimulation). A bisimulation between \(\Sigma\)-coalgebras \(\mathcal{A} = (A,f_{\mathcal{A}})\) and \(\mathcal{B} = (B,f_{\mathcal{B}})\) is a relation \(R\) (i.e. a subobject \(R\) of \(A \times B\) with monomorphism \(i_R : R \rightarrow A \times B\) and projections \(\pi_A : R \rightarrow A\) and \(\pi_B : R \rightarrow B\)) that carries a \(\Sigma\)-coalgebra \(\mathcal{R} = (R,f_{\mathcal{R}})\) such that the following diagram commutes:

\begin{CD} \Sigma(A) @<\Sigma(\pi_A)<< \Sigma(R) @>\Sigma(\pi_B)>> \Sigma(B) \\ @Af_{\mathcal{A}}AA @Af_{\mathcal{R}}AA @AAf_{\mathcal{B}}A\\ A @<<\pi_A< R @>>\pi_B> B\end{CD}

In particular, a bisimulation on \(\bar{\mathbb{N}}\) is a relation \(R \subseteq \bar{\mathbb{N}} \times \bar{\mathbb{N}}\) such that the following diagram commutes:

\begin{CD} \bar{\mathbb{N}}+1 @<\pi_1+1<< R+1 @>\pi_2+1>> \bar{\mathbb{N}}+1 \\ @ApAA @Af_{\mathcal{R}}AA @AApA\\ \bar{\mathbb{N}} @<<\pi_1< R @>>\pi_2> \bar{\mathbb{N}}\end{CD}

This means that

• if \((x,y) \in R\) then \((p(x),p(y)) \in R\),
• if \((0,0) \in R\) then \(f_{\mathcal{R}}(0,0) = *\), which just means that \(0\) has no predecessor (as an extended natural number), so we don't have to demonstrate that \((p(0),p(0)) \in R\).

Thus, we just need to define a relation \(R\) which is closed under the predecessor operation.

We say that two extended natural numbers are bisimilar and write \(x \sim y\) if there exists a bisimulation \(R\) on \(\bar{\mathbb{N}}\) such that \((x,y) \in R\).

Next, we want to demonstrate that \(x \sim y\) implies \(x=y\) (in fact, since the identity relation is a bisimulation, the converse is true also, and thus \(x \sim y\) if and only if \(x=y\)). To see this, consider the following diagram:

\begin{CD} \bar{\mathbb{N}}+1 @<\pi_1+1<< R+1 @>\pi_2+1>> \bar{\mathbb{N}} \\ @ApAA @Af_{\mathcal{R}}AA @AApA \\ \bar{\mathbb{N}} @<<\pi_1< R @>>\pi_2> \bar{\mathbb{N}} \end{CD}

Since \(\bar{\mathbb{N}}\) carries the final coalgebra, there must be a unique homomorphism from \(R\) to \(\bar{\mathbb{N}}\) and thus \(\pi_1=\pi_2\). Thus, for any \((x,y) \in R\), \(\pi_1(x,y)=x=\pi_2(x,y)=y\), so \(x=y\).

This yields a proof technique (for coalgebras in general, and the extended natural numbers in particular): to prove that \(x=y\) for two extended natural numbers \(x\) and \(y\), simply show that \(x \sim y\), i.e. show that there exists at least one bisimulation \(R\) such that \((x,y) \in R\).

We proved this principle under the assumption that the extended natural numbers already carry the final coalgebra. To prove that they do, we would need a coinductive proof principle in the first place. Thus, we adopt the coinductive proof principle as a basic principle.

As an example of a proof by bisimulation, we will prove that the induced map \(\varphi = \mathrm{corec}_{\bar{\mathbb{N}}}(f)\) is indeed unique. Suppose that there are two maps \(\varphi_1\) and \(\varphi_2\) such that

\[\begin{cases}\varphi_1(n) = 0 & \text{if}~ f_{\mathcal{A}}(n)=* \\ p(\varphi_1(n)) = \varphi_1( f_{\mathcal{A}}(n)) & \text{otherwise}\end{cases}\]

and

\[\begin{cases}\varphi_2(n) = 0 & \text{if}~ f_{\mathcal{A}}(n)=* \\ p(\varphi_2(n)) = \varphi_2( f_{\mathcal{A}}(n)) & \text{otherwise.}\end{cases}\]

We define a bisimulation \(R\) as follows:

\[R = \{(\varphi_1(n),\varphi_2(n)) : n \in \bar{\mathbb{N}}\}.\]

To see that \(R\) is indeed a bisimulation, consider any element \((\varphi_1(n),\varphi_2(n)) \in R\) for any \(n \in \bar{\mathbb{N}}\). We want to show that \((p(\varphi_1(n)),p(\varphi_2(n))) \in R\). If \(f_{\mathcal{A}}(n)=*\), then \((\varphi_1(n),\varphi_2(n)) = (0,0)\) and, since \(0\) has no predecessor, there is nothing further to show). If \(f_{\mathcal{A}}(n)\ne*\), then \(f_{\mathcal{A}}(n) \in \bar{\mathbb{N}}\), and thus \((p(\varphi_1(n)),p(\varphi_2(n))) = (\varphi_1( f_{\mathcal{A}}(n)),\varphi_2( f_{\mathcal{A}}(n))) \in R\). Thus, \(R\) is closed under the operation \(p\) and is a bisimulation. It follows that \(\varphi_1(n)\sim\varphi_2(n)\) and hence \(\varphi_1(n)=\varphi_2(n)\). Since \(n\) was arbitrary, it follows that \(\varphi_1 = \varphi_2\).

Thus, we have proved that the induced homomorphism is unique (if it exists).

As another example, we will show that \(\varphi(n) = \infty\) whenever \(f_{\mathcal{A}}(n)\uparrow\) (that is, when \(f_{\mathcal{A}}\) "diverges" starting from \(n\), i.e., there is no finite number of repeated applications such that \(f_{\mathcal{A}}(f_{\mathcal{A}}(\dots(f_{\mathcal{A}}(n)))) = *\)). Suppose we define the rule

\[\frac{f_{\mathcal{A}}(n)\uparrow}{f_{\mathcal{A}}(f_{\mathcal{A}}(n))\uparrow}\]

This rule is also an example of a coinductive definition, but for now we will just accept it and proceed with a proof by bisimulation. We then define a relation as follows:

\[R = \{(\varphi(n),\infty) : n \in \bar{\mathbb{N}}, f_{\mathcal{A}}(n)\uparrow\}.\]

Next, note that \((p(\varphi(n)),p(\infty)) = (\varphi(f_{\mathcal{A}}(n)),\infty) \in R\) since, according to the rule for divergence, \(f_{\mathcal{A}}(f_{\mathcal{A}}(n))\uparrow\). Thus, \(\varphi(n) \sim \infty\), and hence \(\varphi(n) = \infty\).

For one more example of a proof by bisimulation, we will prove that the element \(\infty\) is the unique fixed point of the predecessor function \(p\). Suppose that there are (at least) two such fixed points \(\infty_1\) and \(\infty_2\). We define the following relation:

\[R = \{(\infty_1,\infty_2)\}.\]

Observe that this is trivially closed under the predecessor operation: \((p(\infty_1),p(\infty_2)) = (\infty_1,\infty_2) \in R\). Thus \(\infty_1 \sim \infty_2\) and thus \(\infty_1 = \infty_2\), so there is a unique fixed point \(\infty\).

The Definition

Now we are prepared to state the definition of the general recursive functions. First, we will extend the definitions above to permit more than one argument to each function. Note that, for any function \(f : \bar{\mathbb{N}}^k \rightarrow \bar{\mathbb{N}}\), we can define a function \(\hat{f}\) as follows:

\[\bar{f}(n_1,\dots,n_{k-1}) = \mathrm{rec}(n \mapsto f(n,n_1,\dots,n_{k-1})).\]

Since we can freely permute the arguments of \(f\), this definition (with \(n\) in the first argument) suffices without loss of generality. This is what it means for a function with more than one argument to be primitive recursive.

Likewise, we can do the same for the minimization operation; we can extend it to a new operation defined as follows:

\[\mu(f)(n_1,\dots,n_{k-1}) = \mu(n \mapsto f(n,n_1,\dots,n_{k-1})).\]

This is what is means to minimize a function with more than one argument.

We now characterize the general recursive functions as the combination of the primitive recursive functions and the minimization operation (which represents the primitive corecursive functions). General recursion is thus the synthesis of primitive recursion and primitive corecursion.

Each of the operations \(\mathrm{rec}(f)\) and \(\mathrm{corec}(f)\) make reference to a function \(f\) which itself is assumed to be a general recursive function. In order for this definition to be non-trivial, we need to define a stock of basic general recursive functions from which other functions may be built using \(\mathrm{rec}\) and \(\mathrm{corec}\). This inventory of functions is taken from the algebraic definition of the natural numbers: it is either a constant function (which can be built from zero and the successor function), the successor function, or a projection function (i.e., \(\pi_i : \bar{\mathbb{N}}^k \rightarrow \bar{\mathbb{N}}\)).

Note also that most definitions of the general recursive functions define them as partial functions on the set \(\mathbb{N}\) (functions whose domain is a subset of \(\mathbb{N}\)) instead of total functions on the set \(\bar{\mathrm{N}}\). Both approaches are essentially equivalent, since an undefined input \(n \not \in \mathrm{dom}(f)\) for a partial function \(f\) is equivalent to \(f(n) = \infty\) for a related total function \(\hat{f}\): just map all elements in \(\mathbb{N} \setminus \mathrm{dom}(f)\) to \(\infty\).

Definition (General Recursive Functions). The class of general recursive functions \(f : \mathbb{N}^k \rightarrow \mathbb{N}\) consists of the following functions:

Primitive Functions

• All constant functions \(C^k_n\) defined such that

\[C^k_n(x_1,\dots,x_k) = n\]

for some constant \(n \in \mathbb{N}\) and for some arity (number of arguments) \(k \in \mathbb{N}\).

• The successor function \(S : \mathbb{N} \rightarrow \mathbb{N}\) defined as

\[S(x) = x + 1,\]

where it is assumed that the notion of \(x+1\) is defined somehow (e.g. in set theory using the von Neumann ordinals).

• All projection functions \(P^k_i\) defined as

\[P^k_i(x_1,\dots,x_i,\dots,x_k) = x_i\]

for all arities \(k \in \mathbb{N}\) and all indices \(1 \le i \le k\).

Composition

• For every general recursive function \(f : \mathbb{N}^m \rightarrow \mathbb{N}\) and a list of \(m\) functions \(g_m : \mathbb{N}^k \rightarrow \mathbb{N}\), the function \(f \circ g : \mathbb{N}^k \rightarrow \mathbb{N}\) defined as follows is general recursive:

\[(f \circ g)(x_1,\dots,x_k) = f(g_1(x_1,\dots,x_k),\dots,g_m(x_1,\dots,x_k))\]

Primitive Recursion

• For all general recursive functions \(f : \mathbb{N}^k \rightarrow \mathbb{N}\) and \(g : \mathbb{N}^{k+2} \rightarrow \mathbb{N}\), the general recursive function \(\rho(f,g) : \mathrm{N}^{k+2} \rightarrow \mathbb{N}\) is defined as follows:
  • \(\rho(f,g)(0,x_1,\dots,x_k) = f(0,x_1,\dots,x_k)\),
  • \(\rho(f,g)(S(y),x_1,\dots,x_k) = g(y,\rho(f,g)(y,x_1,\dots,x_n),x_1,\dots,x_k)\)

Primitive Corecursion

• For all general recursive functions \(f : \mathrm{N}^{k+1} \rightarrow \mathbb{N}\), the function \(\mu(f) : \mathrm{N}^k \rightarrow \mathbb{N}\) defined as follows is general recursive:

\[\mu(f)(x_1,\dots,x_k) = \mathrm{min}\{y : f(y,x_1,\dots,x_k) = 0\}.\]

This function is thus undefined whenever \(\{y : f(y,x_1,\dots,x_k) = 0\} = \emptyset\).

This may also be characterized as follows:

\[\mu(f)(x_1,\dots,x_k) = \hat{\mu}(f)(x_1,\dots,x_k)(0),\]

where

\[\hat{\mu}(f)(x_1,\dots,x_k)(y) = \begin{cases} y & \text{if}~f(y,x_1,\dots,x_k) = 0 \\ \hat{\mu}(f)(x_1,\dots,x_k)(f(S(y),x_1,\dots,x_k)) & \text{otherwise,}\end{cases}\]

which is undefined whenever there is no natural number \(y\) such that \(f(y,x_1,\dots,x_k) = 0\).

Conclusion

Thus, there are two types of computable functions on the natural numbers: those that start at a number \(n\) and "go downward" toward \(0\), hence always terminating after \(n\) "steps", and those that start at \(0\) and "go upward" until a number satisfying some criterion is met, either terminating after the first such number is encountered, or else never terminating. The former arises from algebra, the latter from coalgebra. The combination of these two types of computation yields a model of computation equivalent to all other known models of computation.