A Coinductive Representation of Computable Functions

Tang, Alvin; Pattinson, Dirk

doi:10.4230/LIPIcs.CALCO.2025.7

A Coinductive Representation of Computable Functions

Alvin Tang

The Australian National University, Canberra, Australia Dirk Pattinson

The Australian National University, Canberra, Australia

Abstract

We investigate a representation of computable functions as total functions over $2^{\infty}$ , the set of finite and infinite sequences over $\{0,1\}$ . In this model, infinite sequences are interpreted as non-terminating computations whilst finite sequences represent the sum of their digits. We introduce a new definition principle, function space corecursion, that simultaneously generalises minimisation and primitive recursion. This defines the class of computable corecursive functions that is closed under composition and function space corecursion. We prove computable corecursive functions represent all partial recursive functions, and show that all computable corecursive functions are indeed computable by translation into the untyped $\lambda$ -calculus.

Keywords and phrases:

Computability, Coinduction

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Models of computation ; Theory of computation

\rightarrow

Streaming models ; Theory of computation

\rightarrow

Recursive functions

Acknowledgements:

The term “hiaton” to describe a token that symbolises a computational step without visible observations was suggested by Thomas Streicher.

DOI:

10.4230/LIPIcs.CALCO.2025.7

Event:

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Editors:

Corina Cîrstea and Alexander Knapp

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Partial recursive functions as a model of computation intuitively operate on natural numbers, and therefore have been used as a foundation of recursion theory. A notable drawback, however, is that they are partial – function values may be undefined. This complicates their use for formal reasoning, especially with the lack of support for partial functions in many interactive theorem provers [8], and the embedding of types into partial (recursive) functions require restrictions to assert well-definedness of values [15].

Coprogramming [2, 7] has been proposed as a way to deal with non-terminating computations. The main idea here is that functions progressively reveal an increasing part of their possibly infinite output. There are plenty of models tailored to specific programming paradigms and even type theories to ensure the coherence of corecursive function definitions [13]. Partial recursive functions, on the other hand, appear to be on the opposite side of the spectrum as they do not produce infinite function values – the result of an infinite computation is simply undefined.

Conceptually, the partiality in the theory of recursive functions arises from the minimisation operator. Given a function $f$ , we compute $\mu f$ by successively evaluating $f(0),f(1),\dots$ and return $n$ once we find that $f(n)=0$ . Nonetheless, once it is known that $f(0)>0$ , we can be sure $\mu f$ must be no less than $1$ if it is defined. Using a unary representation of natural numbers, it is already safe to emit the digit $1$ . This process can then be repeated for $n=2,3,\dots$ and emit more $1$ ’s whenever we find that $f(n)>0$ . Once we find that $f(n)=0$ , the computation terminates.

This leads to the idea of regaining totality by representing partial recursive functions as functions that operate on the set of finite and infinite sequences of $1$ ’s, where $1^{\omega}=(1,1,1,\dots)$ represents the result of an infinite computation, such as the case for $\mu f$ where $f(n)>0$ for all $n\in\mathbb{N}$ .

This unary representation of natural numbers, albeit an intuitive coinductive data structure, would not suffice for expressing all computations, at least if we aim for computable functions to be closed under composition. Furthermore, it is necessary to consider the implications when the infinite sequence $1^{\omega}$ is taken as a function argument. As an example, consider the function $\mathsf{even}$ that determines the parity of its argument, where we represent $\mathsf{false}$ by the empty sequence and $\mathsf{true}$ by any non-empty sequence. In order to be total, the computation of $\mathsf{even}(1^{\omega})$ must, after finitely many steps, either emit the empty sequence as a result and terminate, whence $\mathsf{even}(1^{\omega})=\mathsf{false}$ , or output an initial digit $1$ , which indicates $\mathsf{even}(1^{\omega})=\mathsf{true}$ . At this point, $\mathsf{even}$ will have only read a finite section of its input, say the first $k$ digits. This entails $\mathsf{even}(1^{\omega})=\mathsf{even}(1^{k})=\mathsf{even}(1^{k+1})$ , which is an obvious contradiction. This demonstrates $\mathsf{even}$ does not have a representation as a total computable function on the set of finite and infinite sequences of $1$ ’s. In fact, this exemplifies that “computable functions are continuous” [20, page 73].

We solve this problem by considering computations over $2^{\infty}$ , the set of finite and infinite sequences over $\{0,1\}$ . Here, the digit $0$ represents a hiaton that can be read as “we do not know yet”. The computation of $\mathsf{even}(1^{\omega})$ would then be expected to yield the value $0^{\omega}$ , consistent with the intuition that at any finite stage of computing $\mathsf{even}(1^{\omega})$ , the result is yet unknown.

This provides the starting point of this computation model – considering functions as programs operating on the coinductive data structure of binary sequences. Our main contribution is a new definition principle that we call function space corecursion, allowing us to represent precisely all partial recursive functions. We show that function space corecursion can be used to express both primitive recursion and minimisation. The interpretation of binary sequences is formally defined using mixed induction-coinduction, which is essential for correlating the behaviour of these corecursive functions with that of partial recursive functions.

Analogous to partial recursive functions, the class of computable corecursive functions contains the zero, successor and projection functions, and is closed under composition and function space corecursion. A principal result of this work is the representation theorem proving the Turing completeness of this model. This involves the completeness theorem which proves that any computable program can be represented in this functional model, and the soundness theorem asserting the fact that every computable corecursive function is indeed computable by encoding them in the untyped $\lambda$ -calculus.

Whilst this paper focuses on the (co)algebraic foundations of the corecursive model and its expressive power, it opens up a large number of new lines of investigation, some of which are discussed in the conclusion.

Related Work

The interpretation of computable functions over the set $2^{\infty}$ is closely related to lazy computation, which intuitively allows partial outputs to be emitted before the end result of the computation is known. More formally, identifying whether two sequences have the same number of $1$ ’s leads to the lazy natural numbers, and the aspects of computability have been studied in [1, 9]. Function space corecursion, the key principle this paper contributes, is nevertheless novel. Computation on possibly infinite sequences is the domain of type-2 Turing machines [19] but the interpretation is different – each sequence is a representation of a point in a topological space, rather than a trace of an intensional computation process. Infinite-time Turing machines [10] are also different as they are machine models of computation where ordinal-many steps can be taken.

2 Preliminaries and Notation

We use the standard set-theoretic notation and basic facts about algebras and coalgebras of set-endofunctors that do not go beyond the tutorial on (co)algebras and (co)induction [11]. We write $\times$ for the Cartesian product, and $+$ for the coproduct in the category of sets and functions. Our universal algebra is similarly basic and is covered by [4, 6, 18]. In particular, we use algebraic signatures (i.e., sets of function symbols with arities) and write $T_{\Sigma}(X)$ for the set of terms with variables in $X$ that can be constructed from a signature $\Sigma$ .

We presuppose familiarity with partial recursive functions (see [16]) that we conceptualise as the least class that contains the constant zero, the unary successor function ( $\mathsf{suc}$ ), all $k$ -ary projections to the $i^{\text{th}}$ element ( $\pi_{i}^{k}$ ) and is closed under primitive recursion as well as minimisation. We write $f(x_{1},\dots,x_{k})\downarrow$ if $f(x_{1},\dots,x_{k})$ is defined, and $f(x_{1},\dots,x_{k})\uparrow$ otherwise. To be precise, we take the composition of a partial function $f:\mathbb{N}^{n}\rightharpoonup\mathbb{N}$ with a tuple $\langle g_{1},\dots,g_{n}\rangle$ of $k$ -ary partial recursive functions to be the function $f\circ\langle g_{1},\dots,g_{n}\rangle:\mathbb{N}^{k}\rightharpoonup\mathbb{N}$ where $f\circ\langle g_{1},\dots,g_{n}\rangle(x_{1},\dots,x_{k})=f(g_{1}(x_{1},\dots,% x_{k}),\dots,g_{n}(x_{1},\dots,x_{k}))$ if all of $g_{1}(x_{1},\dots,x_{k}),\dots,g_{n}(x_{1},\dots,x_{k})$ are defined, and otherwise undefined. Note that even if all $g_{i}(x_{1},\dots,x_{k})$ are defined, $f$ might be undefined at $(g_{1}(x_{1},\dots,x_{k}),\dots,g_{n}(x_{1},\dots,x_{k}))$ . In this case, $f\circ\langle g_{1},\dots,g_{n}\rangle(x_{1},\dots,x_{k})\uparrow$ holds. Similarly, if $g:\mathbb{N}^{k}\rightharpoonup\mathbb{N}$ and $h:\mathbb{N}^{k+2}\rightharpoonup\mathbb{N}$ are partial recursive functions, $\mathsf{PR}(g,h):\mathbb{N}^{k+1}\rightharpoonup\mathbb{N}$ is given by:

	$\displaystyle\mathsf{PR}(g,h)(0,x_{1},\dots,x_{k})$	$\displaystyle=g(x_{1},\dots,x_{k})$
	$\displaystyle\mathsf{PR}(g,h)(n+1,x_{1},\dots,x_{k})$	$\displaystyle=h(n,\mathsf{PR}(g,h)(n,x_{1},\dots,x_{k}),x_{1},\dots,x_{k})$

in case all arguments of $h$ above are defined.

A similar caveat applies to minimisation, where $\mu(f)(x_{1},\dots,x_{k})=n$ if:

$\blacksquare$

$f(m,x_{1},\dots,x_{k})\downarrow$ and $f(m,x_{1},\dots,x_{k})>0$ for all $m=0,\dots,n-1$ , and
$\blacksquare$

$f(n,x_{1},\dots,x_{k})=0$ .

Our conventions for the untyped $\lambda$ -calculus, including natural numbers and if-then-else conditionals, follow Barendregt’s encoding [3]. We write $\Lambda$ for the set of all untyped $\lambda$ -terms and denote $\beta$ -reduction by $\longrightarrow_{\beta}$ . Two $\lambda$ -terms are considered equal by $\beta$ -equality.

The empty sequence is denoted by $[\,]$ . If $A$ is a set, we write $A^{n}$ for the $n$ -fold Cartesian product of $A$ , $A^{*}$ for the set of finite sequences with elements in $A$ , and $A^{\omega}$ for the set of infinite sequences over $A$ . The set of finite and infinite sequences with elements in $A$ is denoted by $A^{\infty}=A^{*}\cup A^{\omega}$ . For $\alpha\in A^{*}$ , we write $\alpha^{n}$ for the $n$ -fold concatenation of $\alpha$ with itself, and $\alpha^{\omega}$ for the infinite sequence $\alpha\cdot\alpha\cdot\alpha\dots$ that arises by concatenating $\alpha$ with itself countably many times.

3 Natural Number and Function Representations

To establish the relationship between partial recursive functions and the new corecursive model, the representation of natural numbers and functions operating on them is formally defined with respect to binary sequences.

Definition 1 (Coinductive Representation of Numbers).

We write $2=\{0,1\}$ for the set of binary digits, and $\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu=2^{\infty}$ for the set of finite and infinite sequences over $2$ that we call the intensional natural numbers. For $\alpha\in\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ , we write $\alpha\uparrow$ if $\alpha$ is infinite, and $\alpha\downarrow$ if $\alpha\in\{0,1\}^{*}$ is finite. A finite intensional natural number $\alpha=(a_{0},\dots a_{k})\in 2^{*}$ represents the number $n\in\mathbb{N}$ if $\sum_{i=0}^{k}a_{i}=n$ , and we write $\alpha\mathrel{\underline{\mathsf{r}}}n$ in this case. A function $f:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ represents a partial numeric function $\hat{f}:\mathbb{N}^{k}\rightharpoonup\mathbb{N}$ if

$\blacksquare$

$f(\alpha_{1},\dots,\alpha_{k})\downarrow$ iff $\hat{f}(n_{1},\dots,n_{k})\downarrow$ whenever each $\alpha_{i}\mathrel{\underline{\mathsf{r}}}n_{i}$ for $i=1,\dots,k$ , and
$\blacksquare$

$f(\alpha_{1},\dots,\alpha_{k})\mathrel{\underline{\mathsf{r}}}\hat{f}(n_{1},% \dots,n_{k})$ in this case.

Clearly, every natural number has countably many representations, and a finite sequence represents a terminating computation. We think of infinite sequences as non-terminating computations, but do not identify them with a single symbol or value, as they can be non-terminating in many different ways. The sequence $(1,1,1,\dots)$ intuitively represents a point at infinity, whereas $(0,0,0,\dots)$ is a non-terminating computation that never reveals any information.

It is well known that $\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ arises as the final coalgebra for the set-endofunctor $FX=1+2\times X$ (see e.g., [11]). As such, it supports coinductive definitions and proof principles. In particular, we are going to use primitive corecursion in the sequel.

Proposition 2.

Let $\sigma:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu% \to 1+2\times\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1% .5mu$ be the structure map of the final coalgebra with $FX=1+2\times X$ and let $C$ be a set. Then, for all $\phi:C\to F(C+\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1% .5mu)$ , there exists a unique $f:C\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ such that $\sigma\circ f=F[f,\mathsf{id}]\circ\phi$ .

For the proof, see [17]. The unique function $u$ in the proposition above is known as an apomorphism in the literature. Spelling this out, this means that for every pairwise disjoint partition $C=C_{0}\cup C_{1}\cup C_{2}$ and all functions $f_{0}:C_{0}\to C$ , $f_{1}:C_{1}\to C$ and $f_{2}:C_{2}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1% .5mu$ , there is a uniquely defined function $u:C\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ that satisfies the equations on the left below.

$\displaystyle u(c)$	$\displaystyle=0:u(f_{0}(c))\ \text{if $c\in C_{0}$}$	$\displaystyle\mathsf{add}(0:\alpha,\beta)$	$\displaystyle=0:\mathsf{add}(\alpha,\beta)$
$\displaystyle u(c)$	$\displaystyle=1:u(f_{1}(c))\ \text{if $c\in C_{1}$}$	$\displaystyle\mathsf{add}(1:\alpha,\beta)$	$\displaystyle=1:\mathsf{add}(\alpha,\beta)$
$\displaystyle u(c)$	$\displaystyle=f_{2}(c)\ \text{if $c\in C_{2}$}$	$\displaystyle\mathsf{add}([\,],\beta)$	$\displaystyle=\beta$

This allows us to define a version of addition for intensional natural numbers by concatenating both sequences by the equations on the right. We note that the addition defined above is extensional in the sense that if arguments just differ in zeros, the same is true for the result.

Figure 1: Commutative diagram for the apomorphism with

F\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu=1+2% \times\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu

.

More formally, we have the following notion of extensional equivalence.

Definition 3 (Extensional equivalence).

The relation $\simeq$ of extensional equivalence is given as the mixed fixpoint defined by the inductive rules (indicated with single-line fractions) and the co-inductive rules (written with double-line fractions) below where $\alpha,\beta\in\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1% .5mu$ .

\frac{}{[\,]\simeq[\,]}\qquad\frac{\alpha\simeq\beta}{0:\alpha\simeq\beta}% \qquad\frac{\alpha\simeq\beta}{\alpha\simeq 0:\beta}\qquad\ooalign{$\genfrac{}% {}{1.2pt}{0}{\alpha\simeq\beta}{0:\alpha\simeq 0:\beta}$\cr$\color[rgb]{1,1,1}% \genfrac{}{}{0.8pt}{0}{\phantom{\alpha\simeq\beta}}{\phantom{0:\alpha\simeq 0:% \beta}}$}\qquad\ooalign{$\genfrac{}{}{1.2pt}{0}{\alpha\simeq\beta}{1:\alpha% \simeq 1:\beta}$\cr$\color[rgb]{1,1,1}\genfrac{}{}{0.8pt}{0}{\phantom{\alpha% \simeq\beta}}{\phantom{1:\alpha\simeq 1:\beta}}$}

More precisely, extensional equivalence is the mixed fixpoint $\nu R.\mu S.I(S)\cup C(R)$ such that

I(S)=\{(\alpha,\beta)\mid(\alpha,\beta)\mbox{ is a conclusion of an inductive rule with premisses in $S$}\}

and $C(R)$ as the analogously defined operator using the coinductive rules, where $\nu X.O(X)$ and $\mu X.O(X)$ are the greatest and least fixpoints of a monotone operator $O$ .

We say that a function $f:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ is extensional if $f(\alpha_{1},\dots,\alpha_{k})\simeq f(\beta_{1},\dots,\beta_{k})$ whenever $\alpha_{i}\simeq\beta_{i}$ for $i=1,\dots,k$ , and a functional $\Phi:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k% }\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)\to(% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)$ is extensional if $\Phi(f)$ is extensional whenever $f$ is extensional.

One way to read this definition is that two intensional natural numbers are extensionally equal if there is a possibly infinite derivation, using both inductive and coinductive rules, where there are only finitely many applications of inductive rules between any two coinductive rules. For finite sequences, extensionally equal numbers represent the same natural numbers.

Proposition 4.

Let $\alpha,\beta\in\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1% .5mu$ with $\alpha\simeq\beta$ . Then, $\alpha$ is finite if and only if $\beta$ is finite. Moreover, if $\alpha\mathrel{\underline{\mathsf{r}}}n$ and $\beta\mathrel{\underline{\mathsf{r}}}k$ for finite $\alpha$ and $\beta\in\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ and $n,k\in\mathbb{N}$ , then $n=k$ .

Proof.

The sequence $\alpha$ is finite only if the inductive and coinductive rules are applied finitely many times and ultimately the axiom $\alpha=[\,]\simeq[\,]=\beta$ is applicable. This is analogous when $\beta$ is finite.

Assuming $\alpha\simeq\beta$ for finite $\alpha,\beta\in\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1% .5mu$ , the coinductive rule stipulating $\alpha\simeq\beta$ implies $1:\alpha\simeq 1:\beta$ is applied finitely many times. The same number of $1$ ’s must be observed in $\alpha$ and $\beta$ . Hence, $\alpha$ and $\beta$ must represent the same natural number. $\hfill\blacktriangleleft$ For extensional functions, we can safely use the intensional natural numbers interchangeably with any of the corresponding binary sequences.

4 Function Space Corecursion

Function space corecursion is a definition principle similar to primitive recursion which allows us to generalise both primitive recursion and minimisation operating on intensional natural numbers. The intuition is best explained in comparison to primitive recursion. A definition of $f=\mathsf{PR}(g,h):\mathbb{N}^{k+1}\rightharpoonup\mathbb{N}$ by primitive recursion relies on two auxiliary (or already defined) functions $g:\mathbb{N}^{k}\rightharpoonup\mathbb{N}$ (that defines $f$ when the first argument is zero), and $h:\mathbb{N}^{k+2}\rightharpoonup\mathbb{N}$ (that is used in the successor case).

Function space corecursion defines a function $f$ of type $\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ in terms of $k+1$ functions $(f_{0},\dots,f_{k})$ that are all of the arity $k$ . The first function $f_{0}$ yields the result if the first argument is the empty sequence $[\,]\in\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ :

f([\,],\alpha_{2},\dots,\alpha_{k})=f_{0}([\,],\alpha_{2},\dots,\alpha_{k}).

The remaining functions simultaneously transform all arguments in a recursive call, where $\mathsf{suc}\ \alpha=1:\alpha$ :

f(\mathsf{suc}\ \alpha_{1},\alpha_{2},\dots,\alpha_{k})=0:f(f_{1}(\alpha_{1},% \dots,\alpha_{k}),\dots,f_{k}(\alpha_{1},\dots,\alpha_{k}))

The crucial point of function space corecursion, and its main difference to primitive recursion, is that all functions $f_{0},\dots,f_{k}$ can change in every recursive call. That means, we stipulate the equations

	$\displaystyle\mathsf{FCR}(f_{0},\dots,f_{k})([\,],\alpha_{2},\dots,\alpha_{k})$	$\displaystyle=f_{0}([\,],\alpha_{2},\dots,\alpha_{k})$
	$\displaystyle\mathsf{FCR}(f_{0},\dots,f_{k})(0:\alpha_{1},\alpha_{2},\dots,% \alpha_{k})$	$\displaystyle=0:\mathsf{FCR}(f_{0},\dots,f_{k})(\alpha_{1},\dots\alpha_{k})$
	$\displaystyle\mathsf{FCR}(f_{0},\dots,f_{k})(1:\alpha_{1},\alpha_{2},\dots,% \alpha_{k})$	$\displaystyle=0:\mathsf{FCR}(f_{0}^{\prime},\dots,f_{k}^{\prime})(\alpha_{1}^{% \prime},\dots\alpha_{k}^{\prime})$

where $\alpha_{i}^{\prime}=f_{i}(\alpha_{1},\dots,\alpha_{k})$ and $f_{0}^{\prime},\dots,f_{k}^{\prime}$ are the changed versions of $f_{0},\dots,f_{k}$ . We express this change by postulating that $f_{i}^{\prime}=\Phi_{i}(f_{i})$ for an operator $\Phi_{i}:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5% mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu% )\to(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}% \to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)$ . The functionals $\Phi_{0},\dots,\Phi_{k}$ then become parameters of a definition by function space corecursion. The following definition makes this precise in terms of intensional natural numbers.

Definition 5 (Function space corecursion).

Let $k>0$ and fix functionals $\Phi_{0},\dots,\Phi_{k}:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.% 5mu}\mkern 1.5mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5% mu}\mkern 1.5mu)\to(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu)$ . We say that the function $\mathsf{FCR}(\Phi_{0},\dots,\Phi_{k}):(\mkern 1.5mu\overline{\mkern-1.5mu% \mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu% \mathbb{N}\mkern-1.5mu}\mkern 1.5mu)^{k+1}\to\mkern 1.5mu\overline{\mkern-1.5% mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu% \mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ is defined by

\begin{array}[]{r@{}r@{\,}l@{\ }c@{\ }l}\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(&[% \,],&\vec{\alpha})&=&f_{0}([\,],\vec{\alpha})\\ \mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(&0:\alpha_{1},&\vec{\alpha})&=&0:\mathsf{% FCR}\,\vec{\Phi}\,\vec{f}\,(\alpha_{1},\vec{\alpha})\\ \mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(&1:\alpha_{1},&\vec{\alpha})&=&0:\mathsf{% FCR}\,\vec{\Phi}\,\vec{f}^{\prime}\,(f_{1}(\alpha_{1},\vec{\alpha}),\dots,f_{k% }(\alpha_{1},\vec{\alpha}))\end{array}

where $\vec{\Phi}=(\Phi_{0},\dots,\Phi_{k})$ , $\vec{f}=(f_{0},\dots,f_{k})$ , $\vec{\alpha}=(\alpha_{2},\dots,\alpha_{k})$ and $\vec{f}^{\prime}=(f^{\prime}_{0},\dots,f^{\prime}_{k})$ such that $f^{\prime}_{j}=\Phi_{j}(f_{j})$ is defined by function space corecursion using the functionals $\Phi_{0},\dots,\Phi_{k}$ and initial functions $f_{0},\dots,f_{k}$ .

$\blacktriangleright$ Remark 6 (Variations).

There are many different possible ways to define function space corecursion. Some variations are to limit the number of functionals, possibly hard-coding the transformation of some of the arguments or being more liberal about the arities of the $f_{i}$ . It may also allow $\Phi_{i}$ to depend on all of $f_{0},\dots,f_{k}$ , i.e., to change the type of $\Phi_{i}$ to $(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)^{k+1}% \to(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}% \to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)$ . Another variation is isotone function space corecursion defined like function space corecursion, but with the last line (and the name) changed to

\begin{array}[]{r@{}c@{\,}l@{\ }c@{\ }l}\mathsf{ICR}\,\vec{\Phi}\,\vec{f}\,(&1% :\alpha_{1},&\vec{\alpha})&=&1:\mathsf{ICR}\,\vec{\Phi}\,\vec{f}^{\prime}\,(f_% {1}(\alpha_{1},\vec{\alpha}),\dots,f_{k}(\alpha_{1},\vec{\alpha}))\end{array}

whilst the remaining clauses remain the same as in Definition 5. This operator is isotone, as it evidently increases the number of $1$ ’s in the function value, but clearly not complete in the sense of being able to define all partial recursive functions. The constant zero function, for instance, is not definable. Other variations include mixed function space corecursion that combines both plain and isotone function space corecursion. Here we stipulate that:

\begin{array}[]{r@{}r@{\,}r@{}l@{\ }c@{\ }l@{}r}\mathsf{MCR}\,\vec{\Phi}\,\vec% {f}\,(&[\,],&\beta,\vec{\gamma})&\ =&&f_{0}([\,],\beta,\vec{\gamma})\\ \mathsf{MCR}\,\vec{\Phi}\,\vec{f}\,(&0:\alpha,&\beta,\vec{\gamma})&\ =&0:&% \mathsf{MCR}\,\vec{\Phi}\,\vec{f}\,(\alpha,\beta,\vec{\gamma})\\ \mathsf{MCR}\,\vec{\Phi}\,\vec{f}\,(&\alpha,&0:\beta,\vec{\gamma})&\ =&0:&% \mathsf{MCR}\,\vec{\Phi}\,\vec{f}\,(\alpha,\beta,\vec{\gamma})\\ \mathsf{MCR}\,\vec{\Phi}\,\vec{f}\,(&1:\alpha,&[\,],\vec{\gamma})&\ =&1:&% \mathsf{MCR}\,\vec{\Phi}\,\vec{f}^{\prime}\,(f_{1}(\alpha,[\,],\vec{\gamma}),% \dots,f_{k+2}(\alpha,[\,],\vec{\gamma}))\\ \mathsf{MCR}\,\vec{\Phi}\,\vec{f}\,(&1:\alpha,&1:\beta,\vec{\gamma})&\ =&0:&% \mathsf{MCR}\,\vec{\Phi}\,\vec{f}^{\prime}\,(f_{1}(\alpha,\beta,\vec{\gamma}),% \dots,f_{k+2}(\alpha,\beta,\vec{\gamma}))\end{array}

The second argument controls whether a non-zero digit will be emitted, and $\mathsf{MCR}$ generalises both $\mathsf{FCR}$ and $\mathsf{ICR}$ by fixing the second argument. We mainly focus on $\mathsf{FCR}$ as this suffices to represent all partial recursive functions. Nevertheless, all our arguments are easily adapted to $\mathsf{MCR}$ .

We make two simple observations before we turn to (lots of) examples. First, function space corecursion is indeed uniquely defined.

Proposition 7.

The function $\mathsf{FCR}\,\vec{\Phi}$ is total and uniquely defined by the equations in Definition 5.

Proof.

We use Proposition 2. Let $C=((\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}% \to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)\to(% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu))^{k+1}% \times(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{% k}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)^{k% +1}\times\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu% ^{k}$ , which is the uncurried domain of $\mathsf{FCR}$ . Suppose $\vec{\Phi}=(\Phi_{0},\dots,\Phi_{k})$ , $\vec{f}=(f_{0},\dots,f_{k})$ and $\vec{f}^{\prime}=(f^{\prime}_{0},\dots,f^{\prime}_{k})$ where $f^{\prime}_{i}=\Phi_{i}(f_{i})$ . Let $\phi:C\to 1+2\times(C+\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu% }\mkern 1.5mu)$ be defined as follows:

	$\displaystyle\phi(\vec{\Phi},\vec{f},[\,],\vec{\alpha})$	$\displaystyle=\begin{cases}\mathrm{in}_{L}(*)&\text{if $f_{0}(\vec{\alpha})=[% \,]$}\\ \mathrm{in}_{R}(0,\mathrm{in}_{R}(\alpha^{\prime}))&\text{if $f_{0}(\vec{% \alpha})=0:\alpha^{\prime}$}\\ \mathrm{in}_{R}(1,\mathrm{in}_{R}(\alpha^{\prime}))&\text{if $f_{0}(\vec{% \alpha})=1:\alpha^{\prime}$}\end{cases}$
	$\displaystyle\phi(\vec{\Phi},\vec{f},0:\alpha_{1},\vec{\alpha})$	$\displaystyle=\mathrm{in}_{R}(0,\mathrm{in}_{L}(\vec{\Phi},\vec{f},\alpha_{1},% \vec{\alpha}))$
	$\displaystyle\phi(\vec{\Phi},\vec{f},1:\alpha_{1},\vec{\alpha})$	$\displaystyle=\mathrm{in}_{R}(0,\mathrm{in}_{L}(\vec{\Phi},\vec{f}^{\prime},% \alpha_{1}^{\prime},\vec{\alpha}^{\prime}))$

where $\vec{\alpha}^{\prime}=(\alpha_{2}^{\prime},\dots,\alpha_{k}^{\prime})$ and $\alpha_{i}^{\prime}=f_{i}^{\prime}(\alpha_{1},\vec{\alpha})$ for any $i=1,\dots,k$ . Proposition 2 now guarantees the unique existence of a function that satisfies the equations stipulated in Definition 5. $\hfill\blacktriangleleft$ The proof readily adapts to show the uniqueness of $\mathsf{ICR}$ and $\mathsf{MCR}$ where $C_{1}\neq\emptyset$ . The fact that $0$ ’s in the definition of $\mathsf{FCR}$ are just passed through and do not affect the computation implies that functions defined using function space corecursion are always extensional (Definition 3).

Proposition 8.

If $k>0$ and all of $\Phi_{0},\dots,\Phi_{k}$ and $f_{0},\dots,f_{k}$ are extensional, then so is $\mathsf{FCR}\,\vec{\Phi}\,\vec{f}$ where $\vec{\Phi}=(\Phi_{0},\dots,\Phi_{k})$ and $\vec{f}=(f_{0},\dots,f_{k})$ .

Proof.

Let $B=\{(\alpha,\beta)\mid\alpha,\beta\in\mkern 1.5mu\overline{\mkern-1.5mu\mathbb% {N}\mkern-1.5mu}\mkern 1.5mu\mbox{ and }\alpha\simeq\beta\}$ be the set of all extensional equivalence relations. Consider the set

E=B\cup\{(\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,\vec{\alpha},\mathsf{FCR}\,\vec{% \Phi}\,\vec{f}\,\vec{\beta})\mid\vec{\alpha}\simeq\vec{\beta}\}

where $\vec{\Phi}=(\Phi_{0},\dots,\Phi_{k})$ , $\vec{f}=(f_{0},\dots,f_{k})$ , $\vec{\alpha}=(\alpha_{1},\dots,\alpha_{k})$ and $\vec{\beta}=(\beta_{1},\dots\beta_{k})$ . The goal is to prove $E\subseteq B$ . By the Knaster-Tarski theorem [12], it suffices to show $E\subseteq\mu S.I(S)\cup C(E)$ with $I$ and $C$ as in Definition 3. Let $(\gamma,\delta)\in E$ . This proof goal clearly holds if $(\gamma,\delta)\in B$ .

Now consider $\gamma=\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,\vec{\alpha}$ and $\delta=\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,\vec{\beta}$ with $\vec{\alpha}\simeq\vec{\beta}$ , that is, $\alpha_{i}\simeq\beta_{i}$ for all $i=1,\dots,k$ . We have $B=\mu S.I(S)\cup C(B)$ , that is, we can perform induction on the inductive part of extensional equivalence $\alpha_{1}\simeq\beta_{1}$ to show that $(\gamma,\delta)\in\mu S.I(S)\cup C(E)$ , with $b:\alpha_{1}\simeq 1:\beta$ for $b\in\{0,1\}$ and $\alpha_{1}\simeq\beta_{1}$ as base cases in addition to $\alpha_{1}=\beta_{1}=[\,]$ .

If $\alpha_{1}=\beta_{1}=[\,]$ , we have $\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,\vec{\alpha}=f_{0}(\vec{\alpha})$ and $\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,\vec{\beta}=f_{0}(\vec{\beta})$ . By assumption, $f_{0}$ is extensional so $(f_{0}(\vec{\alpha}),f_{0}(\vec{\beta}))\in E$ as required.

If $\alpha_{1}=0:\alpha_{1}^{\prime}$ and $\beta_{1}=0:\beta_{1}^{\prime}$ with $\alpha_{1}^{\prime}\simeq\beta_{1}^{\prime}$ , we have

(\gamma,\delta)=(0:\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(\alpha_{1}^{\prime},% \alpha_{2},\dots,\alpha_{k}),0:\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(\beta_{1}^{% \prime},\beta_{2},\dots,\beta_{k}))\in C(E)

by definition of $\mathsf{FCR}$ and $E$ . Similarly, if $\alpha_{1}=1:\alpha_{1}^{\prime}$ and $\beta_{1}=1:\beta_{1}^{\prime}$ with $\alpha_{1}^{\prime}\simeq\beta_{1}^{\prime}$ , we have

(\gamma,\delta)=(0:\mathsf{FCR}\,\vec{\Phi}\,\vec{f}^{\prime}\,(\tilde{\alpha}% _{1}^{\prime},\tilde{\alpha}_{2},\dots,\tilde{\alpha}_{k}),0:\mathsf{FCR}\,% \vec{\Phi}\,\vec{f}^{\prime}\,(\tilde{\beta}_{1}^{\prime},\tilde{\beta}_{2},% \dots,\tilde{\beta}_{k}))\in C(E)

with $f^{\prime}_{i}=\Phi_{i}(f_{i})$ for $i=0,\dots,k$ , $\tilde{\alpha}_{i}^{\prime}=f_{i}(\alpha_{1}^{\prime},\alpha_{2},\dots,\alpha_% {k})$ , and $\tilde{\beta}^{\prime}_{i}=f_{i}(\beta_{1}^{\prime},\beta_{2},\dots,\beta_{k})$ . By definition of $\mathsf{FCR}$ as well as the extensionality of $\Phi_{i}$ and $f_{i}$ , this implies $(\gamma,\delta)\in C(E)$ .

If $\alpha_{1}=0:\alpha_{1}^{\prime}$ , we have by induction hypothesis that

(\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(\alpha_{1}^{\prime},\alpha_{2},\dots,% \alpha_{k}),\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(\beta_{1},\beta_{2},\dots,% \beta_{k}))\in\mu S.I(S)\cup C(E).

Unfolding the definition of $\mathsf{FCR}$ , and applying an inductive rule, this also implies

(0:\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(\alpha_{0}^{\prime},\alpha_{1},\dots,% \alpha_{k}),\mathsf{FCR}\,\vec{\Phi}\,\vec{f}\,(\beta_{0},\beta_{1},\dots,% \beta_{k}))\in\mu S.I(S)\cup C(E).

The case where $\beta_{0}=0:\beta_{0}^{\prime}$ is symmetric. $\hfill\blacktriangleleft$

Example 9.

The addition of intensional natural numbers can be defined in two different ways. Using isotone function space corecursion, we stipulate $f(\alpha,\beta)=\beta$ , $g(\alpha,\beta)=\alpha$ and $h(\alpha,\beta)=\beta$ . With the identity functionals $\Phi=\Psi=\Gamma=\mathsf{Id}:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}% \mkern-1.5mu}\mkern 1.5mu^{2}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}% \mkern-1.5mu}\mkern 1.5mu)\to(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}% \mkern-1.5mu}\mkern 1.5mu^{2}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}% \mkern-1.5mu}\mkern 1.5mu)$ and $\mathsf{add}=\mathsf{ICR}(\Phi,\Psi,\Gamma)(f,g,h)$ , we have:

	$\displaystyle\mathsf{add}([\,],\beta)$	$\displaystyle=\mathsf{ICR}(\Phi,\Psi,\Gamma)(f,g,h)([\,],\beta)=f([\,],\beta)=\beta$
	$\displaystyle\mathsf{add}(0:\alpha,\beta)$	$\displaystyle=\mathsf{ICR}(\Phi,\Psi,\Gamma)(f,g,h)(0:\alpha,\beta)$
		$\displaystyle\simeq\mathsf{ICR}(\Phi,\Psi,\Gamma)(f,g,h)(\alpha,\beta)=\mathsf% {add}(\alpha,\beta)$
	$\displaystyle\mathsf{add}(1:\alpha,\beta)$	$\displaystyle=\mathsf{ICR}(\Phi,\Psi,\Gamma)(f,g,h)(1:\alpha,\beta)$
		$\displaystyle=1:\mathsf{ICR}(\Phi,\Psi,\Gamma)(f,g,h)(g(\alpha,\beta),h(\alpha% ,\beta))=1:\mathsf{add}(\alpha,\beta).$

In other words, $\mathsf{add}$ is the coinductive version of the usual definition of natural numbers addition. It resembles the primitive recursive addition function $\mathit{Add}:\mathbb{N}^{2}\rightharpoonup\mathbb{N}$ where $\mathit{Add}(0,m)=m$ and $\mathit{Add}(n+1,m)=1+\mathit{Add}(n,m)$ by recursion on the first argument.

Alternatively, we can use the plain function space corecursion where occurrences of $1$ ’s in the first argument are accumulated in the second argument in every recursive call. That is, we consider $\Phi=\Psi=\Gamma=\mathsf{Id}$ as above, $f(\alpha,\beta)=\beta$ and $g(\alpha,\beta)=\alpha$ as before, but put $h(\alpha,\beta)=1:\beta$ instead. Consequently, $\mathsf{delay}=\mathsf{FCR}(\Phi,\Psi,\Gamma)(f,g,h)$ satisfies the equations:

	$\displaystyle\mathsf{delay}([\,],\beta)$	$\displaystyle=f([\,],\beta)=\beta$
	$\displaystyle\mathsf{delay}(0:\alpha,\beta)$	$\displaystyle\simeq\mathsf{delay}(\alpha,\beta)$
	$\displaystyle\mathsf{delay}(1:\alpha,\beta)$	$\displaystyle\simeq\mathsf{delay}(\alpha,1:\beta).$

This presents $\mathsf{delay}$ as an alternative version of the coinductive addition, defined by $a(0,m)=m$ and $a(n+1,m)=a(n,1+m)$ . In functional programming terms, $\mathsf{add}$ is a little more lazy, as for any infinite sequence $\alpha$ , we have $\mathsf{add}(\alpha,\beta)=\alpha$ whereas $\mathsf{delay}(\alpha,\beta)=0^{\omega}$ .

The example above is rather trivial as the function parameters are not changing in recursive calls. We had $\Phi_{i}(f_{i})=f_{i}$ for all the functionals. The next example makes use of changing parameters.

Example 10.

Consider the functionals $\Phi,\Psi,\Gamma$ where $\Phi(f)(\alpha,\beta)=\beta$ and $\Psi,\Gamma$ are arbitrary. Then, for $g(\alpha,\beta)=[\,]$ and $h(\alpha,\beta)=f(\alpha,\beta)=\alpha$ we have

	$\displaystyle\mathsf{FCR}(\Phi,\Psi,\Gamma)(f,g,h)([\,],\beta)$	$\displaystyle=f([\,],\beta)=[\,]$
	$\displaystyle\mathsf{FCR}(\Phi,\Psi,\Gamma)(f,g,h)(1:\alpha,\beta)$	$\displaystyle\simeq\mathsf{FCR}(\Phi,\Psi,\Gamma)(f^{\prime},g^{\prime},h^{% \prime})(g(\alpha,\beta),h(\alpha,\beta))$
		$\displaystyle=\mathsf{FCR}(\Phi,\Psi,\Gamma)(f^{\prime},g^{\prime},h^{\prime})% ([\,],\alpha)$
		$\displaystyle=f^{\prime}([\,],\alpha)=\alpha$

where $f^{\prime}=\Phi(f)$ , $g^{\prime}=\Psi(g)$ and $h^{\prime}=\Gamma(h)$ .

In other words, $\mathsf{pred}(\alpha)=\mathsf{FCR}(\Phi,\Psi,\Gamma)(f,g,h)(\alpha,[\,])$ is the predecessor function that removes the first occurrence of $1$ from $\alpha$ if it exists. It is intriguing to note that the complexity of $\mathsf{pred}$ , unlike its primitive recursive counterpart, is not linear but instead depends on the representation of $\alpha$ .

Example 11.

Let $f:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k+1}% \to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ be extensional. Consider the $k+2$ functionals $\vec{\Phi}=(\Phi_{0},\Phi_{1},\dots,\Phi_{k+1})$ and functions $\vec{f}=(f_{0},f_{1},\dots f_{k+1})$ such that:

f_{0}(\vec{\alpha})=\alpha_{2}\qquad f_{1}(\vec{\alpha})=f(1:\alpha_{2},\vec{% \alpha})\qquad f_{2}(\vec{\alpha})=1:\alpha_{2}\qquad f_{i}(\vec{\alpha})=% \alpha_{i}\mbox{ for $i>2$}

where $\vec{\alpha}=(\alpha_{1},\dots,\alpha_{k+1})$ and $\Phi_{i}(f_{i})=f_{i}$ for $i=0,\dots,k+1$ .
It follows that:

	$\displaystyle\mathsf{FCR}\,\vec{\Phi}\,\vec{f}(f([\,],\vec{\alpha}),[\,],\vec{% \alpha})$	$\displaystyle\simeq[\,]\mathrel{\underline{\mathsf{r}}}0$	if $f([\,],\vec{\alpha})\mathrel{\underline{\mathsf{r}}}0$
	$\displaystyle\mathsf{FCR}\,\vec{\Phi}\,\vec{f}(f([\,],\vec{\alpha}),[\,],\vec{% \alpha})$	$\displaystyle\simeq\mathsf{FCR}\,\vec{\Phi}\,\vec{f}(f([1],\vec{\alpha}),[1],% \vec{\alpha})$	otherwise

Continuing in the same way, we have:

	$\displaystyle\mathsf{FCR}\,\vec{\Phi}\,\vec{f}(f([1],\vec{\alpha}),[1],\vec{% \alpha})$	$\displaystyle\mathrel{\underline{\mathsf{r}}}1$	if $f([1],\vec{\alpha})\mathrel{\underline{\mathsf{r}}}0$
	$\displaystyle\mathsf{FCR}\,\vec{\Phi}\,\vec{f}(f([1],\vec{\alpha}),[1],\vec{% \alpha})$	$\displaystyle\simeq\mathsf{FCR}\,\vec{\Phi}\,\vec{f}(f([1,1],\vec{\alpha}),[1,% 1],\vec{\alpha})$	otherwise

By observing that $\alpha_{2}$ is incremented at each iteration, we see and could easily prove by induction that the function

\mathsf{min}f(\vec{\alpha})=\mathsf{FCR}\,\vec{\Phi}\,\vec{f}(f([\,],\vec{% \alpha}),[\,],\vec{\alpha})

satisfies the pattern $\mathsf{min}f(\vec{\alpha})\simeq n$ whenever:

$\blacksquare$

$f(n,\vec{\alpha})\mathrel{\underline{\mathsf{r}}}0$ ,
$\blacksquare$

$f(k,\vec{\alpha})\downarrow$ for all $k<n$ , and
$\blacksquare$

$f(k,\vec{\alpha})$ represents a non-zero value for all $k<n$ .

If $f:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k+1}% \to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ is a representation of a possibly partial numeric function $\hat{f}:\mathbb{N}^{k+1}\rightharpoonup\mathbb{N}$ , it follows that $\mathsf{min}f$ is a representation of $\mu\hat{f}$ , and therefore $\mathsf{min}f$ is extensional by Proposition 8. Using isotone function space corecursion, we obtain a lazy and slightly simpler variant of minimisation, given by

\mathsf{min}^{\prime}f(\alpha)=\mathsf{ICR}\,\vec{\Phi}\,\vec{f}(f([\,],\vec{% \alpha}),[\,],\vec{\alpha})

where all functionals and functions are the same as above with the exception of $f_{2}(\vec{\alpha})=\alpha_{2}$ .

Our next, last, and most complex example shows how to obtain primitive recursion from function space corecursion.

Example 12.

Assume that $r:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k+2}% \to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ and $s:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ are given and extensional representations of total numeric functions $\hat{r}:\mathbb{N}^{k+2}\rightharpoonup\mathbb{N}$ and $\hat{s}:\mathbb{N}^{k}\rightharpoonup\mathbb{N}$ . We construct a representation of $\mathsf{PR}(\hat{s},\hat{r})$ , that is, a function $\phi:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k+% 1}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ . We do this by defining a $(k+2)$ -ary function $\theta$ by function space corecursion, and then putting $\phi(\alpha,\vec{\beta})=\theta(\alpha,[\,],\beta)$ . For the definition of $\theta$ , consider the functionals $\Phi,\Psi,\Gamma:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu^{k+2}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu)\to(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu^{k+2}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu)$ given by

\Phi(f)(\alpha_{1},\alpha_{2},\vec{\beta})=r(\alpha_{2},f([\,],\mathsf{pred}(% \alpha_{2}),\vec{\beta}),\vec{\beta})\qquad\Psi(g)=g\qquad\Gamma(h)=\mathsf{% suc}\circ h

where $\mathsf{suc}(\alpha)=1:\alpha$ is prefixing of $\alpha$ with $1$ , and $\mathsf{pred}$ is the predecessor function from Example 10. Now consider the initial functions

f_{0}(\alpha_{1},\alpha_{2},\vec{\beta})=s(\vec{\beta})\qquad g_{0}(\alpha_{1}% ,\alpha_{2},\vec{\beta})=\alpha_{1}\qquad h_{0}(\_)=[\,]

and let $\theta=\mathsf{FCR}(\Phi,\Psi,\Gamma,\vec{\mathsf{Id}})(f_{0},g_{0},h_{0},\vec% {\mathsf{id}})$ . If $f_{n+1}=\Phi(f_{n})$ , $g_{n+1}=\Psi(g_{n})$ and $h_{n+1}=\Gamma(h_{n})$ , whereas $\vec{\mathsf{id}}$ and $\vec{\mathsf{Id}}$ are sequences of $k$ identity functions and functionals, we have $\phi(\alpha,\vec{\beta})=\mathsf{FCR}(\Phi,\Psi,\Gamma,\vec{\mathsf{Id}})(f_{0% },g_{0},h_{0},\vec{\mathsf{id}})(\alpha,[\,],\vec{\beta})$ :

	$\displaystyle\phi([\,],\beta)$	$\displaystyle=\mathsf{FCR}(\Phi,\Psi,\Gamma,\vec{\mathsf{Id}})(f_{0},g_{0},h_{% 0},\vec{\mathsf{id}})([\,],[\,],\vec{\beta})=f_{0}([\,],[\,],\vec{\beta})=s(% \vec{\beta})$
	$\displaystyle\phi(\mathsf{suc}\ \alpha,\vec{\beta})$	$\displaystyle=\mathsf{FCR}(\Phi,\Psi,\Gamma,\vec{\mathsf{Id}})(f_{0},g_{0},h_{% 0},\vec{\mathsf{id}})(\mathsf{suc}\ \alpha,[\,],\vec{\beta})$
		$\displaystyle\simeq\mathsf{FCR}(\Phi,\Psi,\Gamma,\vec{\mathsf{Id}})(f_{1},g_{1% },h_{1},\vec{\mathsf{id}})(\alpha,[\,],\vec{\beta})\simeq\dots\simeq$
		$\displaystyle\simeq\mathsf{FCR}(\Phi,\Psi,\Gamma,\vec{\mathsf{Id}})(f_{n+1},g_% {n+1},h_{n+1},\vec{\mathsf{id}})([\,],\alpha,\vec{\beta})$
		$\displaystyle=f_{n+1}([\,],\alpha,\vec{\beta})$
		$\displaystyle=r(n,f_{n}([\,],\mathsf{pred}(\alpha),\beta),\beta)=r(\alpha,\phi% (\alpha,\beta),\beta).$

In other words, $\phi$ satisfies the equations of the function $\mathsf{PR}(\hat{s},\hat{r})$ defined by primitive recursion, i.e., $\phi([\,],\vec{\beta})=s(\vec{\beta})$ and $\phi(\mathsf{suc}(\alpha),\vec{\beta})=r(\alpha,\phi(\alpha,\vec{\beta}),\vec{% \beta})$ . That is, the function $\mathsf{FCR}(\Phi,\Psi,\Gamma,\vec{\mathsf{id}})(f,g,h,\vec{\mathsf{id}})(% \alpha,[\,],\vec{\beta})$ is a representation of $\mathsf{PR}(\hat{s},\hat{r})$ ,

In the example above, we obtain a representation of $\mathsf{PR}(\hat{s},\hat{r})$ as we have assumed that $\hat{r}$ and $\hat{s}$ are total. For partial functions, this is not necessarily true as $f\circ g$ does not in general represent $\hat{f}\circ\hat{g}$ , even if $f$ and $g$ represent $\hat{f}$ and $\hat{g}$ , respectively. We return to this when we show that function space corecursion indeed defines all computable functions.

5 Computable Corecursive Functions

The function space corecursion operator offers a lot of flexibility for how the functionals and functions are constructed. To define the class of computable corecursive functions, we need to be precise about how, and in particular with what functionals, the operator is used. Similar to partial recursive functions, computable corecursive functions are an inductively defined class, and every element of this class denotes a $k$ -ary function of type $\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ . As for primitive recursive functions, we often identify a $k$ -ary function symbol with an actual function. The challenge in the definition of computable corecursive functions is precisely which functionals to permit in the definition of function space corecursion. An operator is permissible if it can be “written” in terms of its arguments and previously defined computable corecursive functions.

The definition of computable corecursive functions makes this precise by representing the functionals $\Phi$ in the definition of $\mathsf{FCR}$ by terms. To define a functional $\Phi:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k% }\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)\to(% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)$ , we need to specify $\Phi(\phi)$ for $\phi:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}% \to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ , and to define $\Phi(\phi)$ we need to prescribe $\Phi(\phi)(\vec{\alpha})$ for a generic $\vec{\alpha}\in\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1% .5mu^{k}$ . In other words, we stipulate that $\Phi(\phi)(\vec{\alpha})$ is an expression that uses already defined functions, the function $\phi$ and the arguments $\alpha_{1},\dots,\alpha_{k}$ . That is, we can represent $\Phi(\phi)(\vec{\alpha})$ , and hence $\Phi$ itself, by a term in $k$ variables over a signature that contains symbols for already defined computable corecursive functions, plus an extra $k$ -ary symbol $\phi$ .

Definition 13 (Computable corecursive functions).

The class of computable corecursive functions is the least class that contains the constant zero function $0$ of arity $0$ , the successor function $\mathsf{suc}$ of arity $1$ , the projection functions $\pi_{i}^{k}$ of arity $k$ for $1\leq i\leq k$ and is closed under

function composition,: i.e., if $f$ is $n$ -ary and $g_{1},\dots g_{n}$ are $k$ -ary, and all of $f,g_{1},\dots,g_{n}$ are computable corecursive, then so is $f\circ\langle g_{1},\dots,g_{n}\rangle$ , and
function space corecursion,: that is, if $\Sigma$ is a set of computable corecursive functions and $\Phi_{0},\dots,\Phi_{k}\in T_{\Sigma^{\prime}}(\{x_{1},\dots,x_{k}\})$ , then $\mathsf{FCR}(\Phi_{0},\dots,\Phi_{k})(f_{0},\dots,f_{k})$ is a computable corecursive function of arity $k$ , provided all of $f_{0},\dots,f_{k}$ are $k$ -ary and computably corecursive, and $\Sigma^{\prime}=\Sigma\cup\{\phi\}$ where $\phi\notin\Sigma$ is a fresh $k$ -ary function symbol.

Every $k$ -ary computable corecursive function $f$ is a term that we often identify with its denotation $\llbracket f\rrbracket:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5% mu}\mkern 1.5mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu% }\mkern 1.5mu$ given as follows. We have $\llbracket 0\rrbracket=[\,]$ , $\llbracket\mathsf{suc}\rrbracket(\alpha)=1:\alpha$ , $\llbracket\pi_{i}^{k}\rrbracket(\alpha_{1},\dots,\alpha_{k})=\alpha_{i}$ and $\llbracket f\circ\langle g_{1},\dots,g_{k}\rangle\rrbracket(\alpha_{1},\dots,% \alpha_{n})=\llbracket f\rrbracket(\llbracket g_{1}\rrbracket(\alpha_{1},\dots% ,\alpha_{n}),\dots,\llbracket g_{k}\rrbracket(\alpha_{1},\dots,\alpha_{k}))$ . For function space corecursion, the denotation of $\Phi\in T_{\Sigma^{\prime}}(x_{1},\dots,x_{k})$ is given in the standard way by induction on the structure of $\Phi$ , that is

\llbracket\Phi\rrbracket(g)(\vec{\alpha})=\begin{cases}\alpha_{i},&\Phi=x_{i}% \mbox{ is a variable}\\ f(\llbracket\Phi_{1}\rrbracket(g)(\vec{\alpha}),\dots,\llbracket\Phi_{n}% \rrbracket(g)(\vec{\alpha})),&\Phi=f(\Phi_{1},\dots,\Phi_{n})\mbox{ and }f\in% \Sigma\\ g(\llbracket\Phi_{1}\rrbracket(g)(\vec{\alpha}),\dots,\llbracket\Phi_{n}% \rrbracket(g)(\vec{\alpha})),&\Phi=\phi(\Phi_{1},\dots,\Phi_{k})\mbox{ and }% \phi\in\Sigma^{\prime}\setminus\Sigma\\ \end{cases}

where we use $f\in\Sigma$ homonymously as a function symbol and its interpretation, $g:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ and $\vec{\alpha}=\alpha_{1},\dots,\alpha_{k}\in\mkern 1.5mu\overline{\mkern-1.5mu% \mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}$ . With this,

\llbracket\mathsf{FCR}(\Phi_{0},\dots,\Phi_{k})(f_{0},\dots,f_{k})\rrbracket=% \mathsf{FCR}(\llbracket\Phi_{0}\rrbracket,\dots,\llbracket\Phi_{k}\rrbracket)(% f_{0},\dots,f_{k})

where function space corecursion is the same as in Definition 5.

When requiring that $\Phi\in T_{\Sigma^{\prime}}(\{x_{1},\dots,x_{k}\})$ , we use already defined, $n$ -ary computable corecursive functions $f\in\Sigma$ as $n$ -ary function symbols. Unfolding the definition of the term algebra $T_{\Sigma^{\prime}}(\{x_{1},\dots,x_{k}\})$ , we have that $\Phi$ is either a variable, or $\Phi$ is of the form $\sigma(\Phi_{1},\dots,\Phi_{n})$ where $\sigma\in\Sigma^{\prime}$ is a function symbol. All $\Phi_{i}$ are already defined terms $\Phi_{i}\in T_{\Sigma^{\prime}}(\{x_{1},\dots,x_{n}\})$ . When interpreting $\Phi$ as a functional $\llbracket\Phi\rrbracket:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1% .5mu}\mkern 1.5mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5% mu}\mkern 1.5mu)\to(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu)$ , we interpret a function symbol $\phi\in\Sigma^{\prime}\setminus\Sigma$ as the argument of the interpretation of $\Phi$ , and a function symbol $f\in\Sigma$ as $f$ (conceived as a function).

We have seen that function space corecursion can simulate both minimisation and primitive recursion. This does not suffice to show that every partial recursive function can be represented by a computable corecursive function – the composition of partial recursive functions differs from the composition of computable corecursive functions as the latter are total. Consider as an example the constant zero function $z(\alpha)=[\,]$ that represents the function $\hat{z}(n)=0$ . The unary function $f(\alpha)=(0,0,\dots)$ represents the totally undefined function $\hat{f}$ where $\hat{f}(n)\uparrow$ for all $n\in\mathbb{N}$ . It is however not the case that $z\circ f$ represents $\hat{z}\circ\hat{f}$ as $z\circ f([\,])\downarrow$ but $\hat{z}\circ\hat{f}(0)\uparrow$ .

To establish a representation theorem, we therefore need to make the somewhat unnatural manoeuvre, which deliberately limits the definedness of a function, to represent the composition of partial functions using function space corecursion. The key observation is that the constant zero function $\hat{z}$ also has a different representation $z^{\prime}$ where $z^{\prime}(\alpha)\simeq 0$ for any finite sequence $\alpha\in 2^{*}$ and $z^{\prime}(\alpha)=(0,0,\dots)$ for any infinite sequence $\alpha\in 2^{\omega}$ . We start by showing that $z^{\prime}$ is computable corecursive.

Lemma 14.

The function $z^{\prime}:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5% mu\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ defined by $z^{\prime}(\alpha)=0^{n}$ if $\alpha\in 2^{n}$ and $z^{\prime}(\alpha)=0^{\omega}$ otherwise is computable corecursive.

Proof.

Let $z^{\prime}=\mathsf{FCR}(\mathsf{Id},\mathsf{Id})(\mathsf{id},\mathsf{id})$ where $\mathsf{Id}:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1% .5mu\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)% \to(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)$ is the identity functional, and $\mathsf{id}:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.% 5mu\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ is the identity function. Then

$\displaystyle z^{\prime}([\,])$	$\displaystyle=\mathsf{FCR}(\mathsf{Id},\mathsf{Id})(\mathsf{id},\mathsf{id})([% \,])$	$\displaystyle\ =\$	$\displaystyle[\,]$
$\displaystyle z^{\prime}(0:\alpha)$	$\displaystyle=\mathsf{FCR}(\mathsf{Id},\mathsf{Id})(\mathsf{id},\mathsf{id})(0% :\alpha)$	$\displaystyle\ =\$	$\displaystyle 0:\mathsf{FCR}(\mathsf{Id},\mathsf{Id})(\mathsf{id},\mathsf{id})% (\alpha)$
$\displaystyle z^{\prime}(1:\alpha)$	$\displaystyle=\mathsf{FCR}(\mathsf{Id},\mathsf{Id})(\mathsf{id},\mathsf{id})(1% :\alpha)$	$\displaystyle\ =\$	$\displaystyle 0:\mathsf{FCR}(\mathsf{Id},\mathsf{Id})(\mathsf{id},\mathsf{id})% (\alpha).$

It is evident that $z^{\prime}$ is the denotation of a computable corecursive function, and we have $z^{\prime}=\llbracket\mathsf{FCR}(\mathsf{Id},\mathsf{Id})(\mathsf{id},\mathsf% {id})\rrbracket$ where formally $\mathsf{Id}=\phi(x)\in T_{\emptyset^{\prime}}(\{x\})$ is the required term representation, and $\mathsf{id}$ is the evidently computable corecursive identity function $\pi^{1}_{1}$ . $\hfill\blacktriangleleft$ Our strategy, to show that the composition of partial recursive functions can again be represented by a computably corecursive function, is to prefix the concatenation $z^{\prime}(g_{1}(\vec{\alpha}))\cdot\dots\cdot z^{\prime}(g_{n}(\vec{\alpha}))$ to the composition $f\circ\langle g_{1},\dots,g_{n}\rangle$ and so making sure that the composition is undefined (i.e., an infinite sequence) if one of the arguments is undefined.

Lemma 15.

Suppose that $f:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{n}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ and $g_{1},\dots,g_{n}:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu^{k}\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}% \mkern 1.5mu$ are computably corecursive. If $f$ represents $\hat{f}$ and $g_{i}$ represents $\hat{g}_{i}$ , then there is a computably corecursive function $h$ that represents $\hat{f}\circ\langle\hat{g}_{1},\dots,\hat{g}_{n}\rangle$ .

Proof.

We write $\alpha\cdot\beta$ for $\mathsf{delay}(\alpha,\beta)$ and put $h(\alpha_{1},\dots,\alpha_{n})=z^{\prime}(g_{1}(\vec{\alpha})\cdot\dots\cdot g% _{n}(\vec{\alpha}))\cdot f(g_{1}(\vec{\alpha}),\dots,g_{n}(\vec{\alpha}))$ . Here, $z^{\prime}$ is as in Lemma 14 and it is clear that $h$ represents $\hat{f}\circ\langle g_{1},\dots,g_{k}\rangle$ . $\hfill\blacktriangleleft$ We have now collected all the ingredients for our representation theorem.

Theorem 16.

Every partial recursive function has a computable corecursive representation.

Proof.

For total functions $\hat{f}$ and $\hat{g}_{1},\dots,\hat{g}_{n}$ that are represented by $f,g_{1},\dots,g_{n}$ , we have that $f\circ\langle g_{1},\dots,g_{n}\rangle$ represents $\hat{f}\circ\langle\hat{g}_{1},\dots\hat{g}_{n}\rangle$ . It then follows from Example 12 that all primitive recursive functions have a representation. To obtain a representation for all partial recursive functions, we use Kleene’s normal form theorem and Example 11 where we implement the composition of partial functions using Lemma 15. $\hfill\blacktriangleleft$

6 Soundness

We have shown that every partial recursive function is represented by the denotation of a computable corecursive function. We could argue that this implies computable corecursive functions represent the class of all computable functions by Church’s thesis, as they are intuitively computable. Indeed, it is obvious how we implement an instance of function space corecursion in the Haskell programming language. The following shows an example of how $\mathsf{FCR}$ can be defined.

-- finite and infinite lists
data Bit = Zero | One deriving (Eq, Show); type Seq = [Bit]

-- functions and functionals for an instance of FCR with two arguments
type Fn = Seq -> Seq -> Seq
type Fnl = Fn -> Fn

-- function space corecursion for binary functions
fcr2 :: Fnl -> Fnl -> Fnl -> Fn -> Fn -> Fn -> Fn
fcr2 phi psi gamma f g h a b = case a of
  []     -> f [] b
  Zero:a -> Zero:(fcr2 phi psi gamma f g h a b)
  One:a  -> Zero:(fcr2 phi psi gamma f’ g’ h’ a’ b’) where
    f’ = phi f; g’ = psi g; h’ = gamma h; a’ = g a b; b’ = h a b

The $\mathsf{delay}$ and $\mathsf{pred}$ functions in the previous section are then easily defined as follows.

-- delayed addition
delay :: Fn
delay = fcr2 id id id (\a b -> b) (\a b -> a) (\a b -> One:b)
-- auxiliary function to define predecessor
pred’ :: Fn
pred’ = fcr2 (\f -> \a b -> b) id id (\a b -> a) (\a b -> []) (\a b -> a)

While the argument is certainly convincing, we instead show that all computable corecursive functions are $\lambda$ -representable, starting with the encoding of finite and infinite sequences of digits as untyped $\lambda$ -terms. In addition to the binary digits, we introduce a blank symbol ( $B$ ) to mark the end of a binary sequence.

Definition 17.

Define $\llceil\cdot\rrceil:2\cup\{B\}\to\Lambda$ such that $\llceil B\rrceil=\lambda xyz.x$ , $\llceil 0\rrceil=\lambda xyz.y$ and $\llceil 1\rrceil=\lambda xyz.z$ . A term $M$ encodes a finite binary sequence $\alpha=(a_{0},\dots,a_{k-1})$ whenever $M\ \lceil i\rceil=\llceil a_{i}\rrceil$ for all $0\leq i<k$ , and $M\ \lceil i+1\rceil=\llceil B\rrceil$ for $i=k$ . A term $M$ encodes an infinite binary sequence $(\alpha_{0},\alpha_{1},\dots)$ whenever $M\ \lceil i\rceil=\llceil a_{i}\rrceil$ for all $i\in\mathbb{N}$ .

As mentioned previously, $\lceil\cdot\rceil:\mathbb{N}\to\Lambda$ is a mapping from natural numbers to their $\lambda$ -encoding. Barendregt’s formulation [3] or any alternative encoding that provides basic functionalities (e.g., predecessor and successor functions) works the same way.

Example 18.

The empty sequence $[\,]$ can be encoded as $\lambda x.\llceil B\rrceil$ because $(\lambda x.\llceil B\rrceil)\ \lceil 0\rceil\longrightarrow_{\beta}\llceil B\rrceil$ . An infinite sequence of $1$ ’s can be encoded as $\lambda x.\llceil 1\rrceil$ . In fact, we can define a concatenation operator $\mathsf{cons}$ by

\mathsf{cons}\ x\ y\equiv\lambda w.\mathsf{if}\ (\mathsf{isZero}\ w)\ \mathsf{% then}\ x\ \mathsf{else}\ y\ (\mathsf{pred}\ w)

where $\mathsf{isZero}$ checks whether $w$ encodes the natural number zero, and $\mathsf{pred}$ decrements a natural number. The $\mathsf{head}$ and $\mathsf{tail}$ functions are simply $\lambda x.x\ \lceil 0\rceil$ and $\lambda xy.x\ (\mathsf{suc}\ y)$ , respectively.

To facilitate case distinctions with the binary digits and the blank symbol, let the notation $\mathsf{switch}\ W\ \mathsf{caseB}\ X\ \mathsf{case0}\ Y\ \mathsf{case1}\ Z$ be the syntactic sugar of $W\ X\ Y\ Z$ . The encoding of the blank symbol and the binary digits effectively function as truth values for the case distinction. For example,

		$\displaystyle\mathsf{switch}\ \llceil B\rrceil\ \mathsf{caseB}\ X\ \mathsf{% case0}\ Y\ \mathsf{case1}\ Z$
	$\displaystyle\equiv\$	$\displaystyle\llceil B\rrceil\ X\ Y\ Z$
	$\displaystyle\longrightarrow_{\beta}^{*}\$	$\displaystyle(\lambda xyz.x)\ X\ Y\ Z$
	$\displaystyle\longrightarrow_{\beta}^{*}\$	$\displaystyle X.$

Definition 19 ( $\lambda$ -definability of functions).

A computable corecursive function $f:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ is $\lambda$ -definable if there exists $F\in\Lambda$ such that $F\ R_{1}\ \dots\ R_{k}$ is the encoding of $f(\alpha_{1},\dots,\alpha_{k})$ as per Definition 17 whenever $R_{i}$ is a $\lambda$ -encoding of $\alpha_{i}$ . A functional $\Phi:(\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k% }\to\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)\to(% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu)$ is $\lambda$ -definable if there exists $P\in\Lambda$ such that $P\ F$ is an encoding of $\Phi(f)$ whenever $F$ is the encoding of $f:\mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu^{k}\to% \mkern 1.5mu\overline{\mkern-1.5mu\mathbb{N}\mkern-1.5mu}\mkern 1.5mu$ .

Example 20.

If functionals $\Phi_{1},\dots,\Phi_{k}$ and functions $f_{1},\dots,f_{k}$ are $\lambda$ -definable, then so is $\mathsf{FCR}(\Phi_{0},\dots,\Phi_{k})(f_{0},\dots,f_{k})$ . Suppose $P_{1},\dots,P_{k}$ are the $\lambda$ -encodings of the functionals $\Phi_{0},\dots,\Phi_{k}$ , and $F_{0},\dots,F_{k}$ are the encodings of the functions $f_{0},\dots,f_{k}$ . Devise $F$ as

	$\displaystyle\lambda f.P_{0}\cdots P_{k}\ F_{0}\cdots F_{k}\ R_{1}\cdots R_{k}.$
	$\displaystyle\quad\mathsf{switch}\ (\mathsf{head}\ R_{1})$
	$\displaystyle\quad\mathsf{caseB}\ (f\ F_{0}\ R_{1}\cdots R_{k})$
	$\displaystyle\quad\mathsf{case0}\ (\mathsf{cons}\ \llceil 0\rrceil\ (f\ P_{0}% \cdots P_{k}\ F_{0}\cdots F_{k}\ (\mathsf{tail}\ R_{1})\ R_{2}\cdots R_{k}))$
	$\displaystyle\quad\mathsf{case1}\ (\mathsf{cons}\ \llceil 0\rrceil\ (f\ P_{0}% \dots P_{k}\ F^{\prime}_{0}\cdots F^{\prime}_{k}\ (F_{1}\ (\mathsf{tail}\ R_{1% }))\ R^{\prime}_{2}\cdots R^{\prime}_{k}))$

where $F^{\prime}_{i}\equiv P_{i}\ F_{i}$ and $R^{\prime}_{i}\equiv F_{i}\ R_{i}$ . It follows that $Y\ F$ is the encoding of the function $\mathsf{FCR}(\Phi_{0},\dots,\Phi_{k})(f_{0},\dots,f_{k})$ with $Y$ being the $Y$ -combinator.

Theorem 21.

All computable corecursive functions are $\lambda$ -definable.

Proof.

By induction on the class of computable corecursive functions, replacing the interpretation $\llbracket\cdot\rrbracket$ in Definition 5 with $\llbracket\cdot\rrbracket_{\lambda}$ that maps the terms to their $\lambda$ -encodings. The base cases are evident while the encoding of $\mathsf{FCR}$ is shown in Example 20. $\hfill\blacktriangleleft$

7 Conclusions and Further Work

We have seen how function space corecursion and its variants can be used to represent exactly the class of all computable functions. This (co)algebraic approach offers a mathematically elegant way to represent computer programs. This computation model avoids the intricacies of state transitions and side effects such as tape manipulations found in Turing machines; it also enables certain programming features (e.g., lazy evaluation) that cannot be reflected in partial recursive functions to be introduced. Mixed induction-coinduction has been used for interpreting the coinductive data structure of binary sequences, providing extensionality and allowing us to correlate the data structure to program non-termination.

The major result of this paper has been formally investigating the (co)algebraic foundations of the model, along with proving its expressive power in relation to existing models of computation. It is envisioned to open a number of intriguing research perspectives.

The first open question is, can we establish the standard results of recursion theory also with computable corecursive functions? For example, if $\phi$ is an enumeration of all computable corecursive functions and $f$ is total and recursive, do we have $e$ such that $\phi_{e}\simeq\phi_{f(e)}$ ? The main difference from the standard formulation of the recursion theorem is that for computable corecursive functions, $\phi_{e}$ and $\phi_{f(e)}$ also need to agree on all infinite values (modulo extensional equality $\simeq$ ) as $\simeq$ does not identify all infinite sequences. Similar comments apply to the second recursion theorem and to the $s$ - $m$ - $n$ theorem. Does the normal form theorem extend to computable corecursive functions?

The second intriguing avenue is to explore an equational calculus for asserting extensional equality of computable corecursive functions. Given that the denotation of computable corecursive functions are total functions on intensional natural numbers, the main barrier for the design of an equational calculus has been removed. On the other hand, equality between computable functions is not recursively enumerable. We, therefore, expect this calculus to be non-wellfounded, similar to the exercise conducted for Turing machines [14]. This question is closely related to that of induction principles for intensional natural numbers that we would employ in a calculus for equality. In other words, how can we show that $f(\alpha)\simeq g(\alpha)$ for all intensional natural numbers $\alpha$ ? We hypothesise that any principle will combine induction and coinduction with reference to comparable systems [5].

Another orthogonal angle is that of the computational complexity of a recursive function. Can we establish a linkage between the complexity of a function $f$ , that is, the number of steps it takes to evaluate $f(\alpha)$ , with the length of the representation of $f(\alpha)$ ? To do this, we would move from a unary to a binary coding of natural numbers, and still retain a hiaton, i.e., a token that symbolises a computational step that has not (yet) yielded an observable result. Are there definition principles that relate the length $|f(\alpha)|$ to the number of steps it takes to compute $f(\alpha)$ ? Partial recursive functions are rarely used for computational complexity analysis; we envision computable corecursive functions can bridge this gap.

Finally, what is the “right” set of computable functions on $2^{\infty}$ ? In this paper, we have identified a class of functions on $2^{\infty}$ that represents all partial recursive functions. We have shown that for this purpose, the function space corecursion operator $\mathsf{FCR}$ suffices. This operator is special, for example, when representing $\mu f$ using $\mathsf{FCR}$ , no digits of outputs are produced until a zero of $f$ has been found, as we have discussed in Example 11. A small set of functions based on functional space corecursion may suffice to achieve Turing completeness, and thus further simplify the foundational theory.

References

[1] Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Inf. Comput., 105(2):159–267, 1993. doi:10.1006/inco.1993.1044.
[2] Robert Atkey and Conor McBride. Productive coprogramming with guarded recursion. ACM SIGPLAN Notices, 48(9):197–208, 2013. doi:10.1145/2500365.2500597.
[3] Henk Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985.
[4] Michael Barr and Charles Wells. Category Theory for Computing Science. Prentice Hall, 1989.
[5] Henning Basold and Helle Hvid Hansen. Well-definedness and observational equivalence for inductive-coinductive programs. Journal of Logic and Computation, 29(4):419–468, 2019. doi:10.1093/logcom/exv091.
[6] George Mark Bergman. An Invitation to General Algebra and Universal Constructions. Universitext. Springer, Cham, 2nd edition, 2015. doi:10.1007/978-3-319-11478-1.
[7] Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Foundational extensible corecursion: a proof assistant perspective. In Kathleen Fisher and John Reppy, editors, Proc. ICFP 2015, pages 192–204. Association for Computing Machinery, 2015. doi:10.1145/2784731.2784732.
[8] Ana Bove, Alexander Krauss, and Matthieu Sozeau. Partiality and recursion in interactive theorem provers — an overview. Mathematical Structures in Computer Science, 26(1):38–88, 2014. doi:10.1017/S0960129514000115.
[9] Martín Hötzel Escardó. On lazy natural numbers with applications to computability theory and functional programming. SIGACT News, 24(1):61–67, 1993. doi:10.1145/152992.153008.
[10] Joel David Hamkins. A survey of infinite time turing machines. In Jérôme Olivier Durand-Lose and Maurice Margenstern, editors, Proc. MCU 2007, volume 4664 of Lecture Notes in Computer Science, pages 62–71. Springer, 2007. doi:10.1007/978-3-540-74593-8_5.
[11] Bart Jacobs and Jan Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin, 62:222–259, 1997.
[12] Dexter Kozen. Theory of Computation. Texts in Computer Science. Springer, London, 2006. doi:10.1007/1-84628-477-5_7.
[13] Rasmus Ejlers Møgelberg. A type theory for productive coprogramming via guarded recursion. In Proc. CSL-LICS 2014, pages 1–10, New York, 2014. Association for Computing Machinery. doi:10.1145/2603088.2603132.
[14] Dirk Pattinson and Lutz Schröder. Program Equivalence is Coinductive. In Proc. LICS 2016, pages 337–346, New York, 2016. Association for Computing Machinery. doi:10.1145/2933575.2934506.
[15] Anton Setzer. Partial Recursive Functions in Martin-Löf Type Theory. In Proc. CiE 2006, volume 3988 of Lecture Notes in Computer Science, pages 505–515. Springer, 2006. doi:10.1007/11780342_51.
[16] Joseph Robert Shoenfield. Recursion Theory. Lecture Notes in Logic. Springer, 1993.
[17] Tarmo Uustalu and Varmo Vene. Primitive (Co)Recursion and Course of Value (Co)Iteration, Categorically. INFORMATICA (IMI, Lithuania), 10:5–26, 1999. doi:10.3233/INF-1999-10102.
[18] Wolfgang Wechler. Universal Algebra for Computer Scientists, volume 25 of EATCS Monographs on Theoretical Computer Science. Springer, 1992. doi:10.1007/978-3-642-76771-5.
[19] Klaus Weihrauch. Computable Analysis. Springer, 2000.
[20] Glynn Winskel. The formal semantics of programming languages: an introduction. MIT Press, 1993.

[bib.bib1] [1] Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Inf. Comput., 105(2):159–267, 1993. doi:10.1006/inco.1993.1044.

[bib.bib2] [2] Robert Atkey and Conor McBride. Productive coprogramming with guarded recursion. ACM SIGPLAN Notices, 48(9):197–208, 2013. doi:10.1145/2500365.2500597.

[bib.bib3] [3] Henk Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985.

[bib.bib4] [4] Michael Barr and Charles Wells. Category Theory for Computing Science. Prentice Hall, 1989.

[bib.bib5] [5] Henning Basold and Helle Hvid Hansen. Well-definedness and observational equivalence for inductive-coinductive programs. Journal of Logic and Computation, 29(4):419–468, 2019. doi:10.1093/logcom/exv091.

[bib.bib6] [6] George Mark Bergman. An Invitation to General Algebra and Universal Constructions. Universitext. Springer, Cham, 2nd edition, 2015. doi:10.1007/978-3-319-11478-1.

[bib.bib7] [7] Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Foundational extensible corecursion: a proof assistant perspective. In Kathleen Fisher and John Reppy, editors, Proc. ICFP 2015, pages 192–204. Association for Computing Machinery, 2015. doi:10.1145/2784731.2784732.

[bib.bib8] [8] Ana Bove, Alexander Krauss, and Matthieu Sozeau. Partiality and recursion in interactive theorem provers — an overview. Mathematical Structures in Computer Science, 26(1):38–88, 2014. doi:10.1017/S0960129514000115.

[bib.bib9] [9] Martín Hötzel Escardó. On lazy natural numbers with applications to computability theory and functional programming. SIGACT News, 24(1):61–67, 1993. doi:10.1145/152992.153008.

[bib.bib10] [10] Joel David Hamkins. A survey of infinite time turing machines. In Jérôme Olivier Durand-Lose and Maurice Margenstern, editors, Proc. MCU 2007, volume 4664 of Lecture Notes in Computer Science, pages 62–71. Springer, 2007. doi:10.1007/978-3-540-74593-8_5.

[bib.bib11] [11] Bart Jacobs and Jan Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin, 62:222–259, 1997.

[bib.bib12] [12] Dexter Kozen. Theory of Computation. Texts in Computer Science. Springer, London, 2006. doi:10.1007/1-84628-477-5_7.

[bib.bib13] [13] Rasmus Ejlers Møgelberg. A type theory for productive coprogramming via guarded recursion. In Proc. CSL-LICS 2014, pages 1–10, New York, 2014. Association for Computing Machinery. doi:10.1145/2603088.2603132.

[bib.bib14] [14] Dirk Pattinson and Lutz Schröder. Program Equivalence is Coinductive. In Proc. LICS 2016, pages 337–346, New York, 2016. Association for Computing Machinery. doi:10.1145/2933575.2934506.

[bib.bib15] [15] Anton Setzer. Partial Recursive Functions in Martin-Löf Type Theory. In Proc. CiE 2006, volume 3988 of Lecture Notes in Computer Science, pages 505–515. Springer, 2006. doi:10.1007/11780342_51.

[bib.bib16] [16] Joseph Robert Shoenfield. Recursion Theory. Lecture Notes in Logic. Springer, 1993.

[bib.bib17] [17] Tarmo Uustalu and Varmo Vene. Primitive (Co)Recursion and Course of Value (Co)Iteration, Categorically. INFORMATICA (IMI, Lithuania), 10:5–26, 1999. doi:10.3233/INF-1999-10102.

[bib.bib18] [18] Wolfgang Wechler. Universal Algebra for Computer Scientists, volume 25 of EATCS Monographs on Theoretical Computer Science. Springer, 1992. doi:10.1007/978-3-642-76771-5.

[bib.bib19] [19] Klaus Weihrauch. Computable Analysis. Springer, 2000.

[bib.bib20] [20] Glynn Winskel. The formal semantics of programming languages: an introduction. MIT Press, 1993.

A Coinductive Representation of Computable Functions

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Related Work

2 Preliminaries and Notation

3 Natural Number and Function Representations

Definition 1 (Coinductive Representation of Numbers).

Proposition 2.

Definition 3 (Extensional equivalence).

Proposition 4.

Proof.

4 Function Space Corecursion

Definition 5 (Function space corecursion).

▶ Remark 6 (Variations).

Proposition 7.

Proof.

Proposition 8.

Proof.

Example 9.

Example 10.

Example 11.

Example 12.

5 Computable Corecursive Functions

Definition 13 (Computable corecursive functions).

Lemma 14.

Proof.

Lemma 15.

Proof.

Theorem 16.

Proof.

6 Soundness

Definition 17.

Example 18.

Definition 19 (λ-definability of functions).

Example 20.

Theorem 21.

Proof.

7 Conclusions and Further Work

References

$\blacktriangleright$ Remark 6 (Variations).

Definition 19 ( $\lambda$ -definability of functions).