Can total (primitive) corecursion be implemented?

Question

I'm trying to understand how to implement corecursion in a total functional context. I've already implemented recursion using standard techniques (for loops) but I think I've misunderstood corecursion.

For our working example, consider the extended natural numbers (WP, nLab); these are the natural numbers plus an extra element at infinity. They are equipped with a natural operation $\operatorname{pred} : \tilde{\mathbb{N}} \to \tilde{\mathbb{N}} + 1$ which takes each number to its predecessor, sending 0 to the extra point and ∞ to ∞. If we already have a way of representing the natural numbers and sums, then the extended natural numbers are represented in the obvious way, as a sum $\tilde{\mathbb{N}} \equiv \mathbb{N} + 1$. All of this should be straightforward to implement.

However, the corecursion is not obvious. Quoting from nLab:

[G]iven any set $S$ and map $p:S\to1+S$, there is a unique map $\operatorname{corec}_{S}(p) :S \to \tilde{\mathbb{N}}$ such that [$p \circ \operatorname{id} + \operatorname{corec}_{S}(p) \equiv \operatorname{corec}_{S}(p) \circ \operatorname{pred}$] [diagram omitted]. … You can think of $\operatorname{corec}_{S}(p)$ as mapping an element $a \in S$ to the maximum number of times that $p$ can be applied in succession, starting from $a$, before being taken out of $S$. Since this may never occur, we need ∞ as a possible value.

But how is it possible to actually get ∞ as a result from evaluating $\operatorname{corec}_{S}$? We could not arrive at ∞ without infinitely many evaluations of $p$, which is unphysical. Instead, each time we evaluate $p$ in a row, we have a finite counter which is incremented. Is this an implementation detail or a serious misunderstanding?

Answer 1

Your implementation $\tilde{\mathbb{N}} \equiv \mathbb{N} + 1$ can only work in the presence of classical principles like the limited principle of omniscience. In fact, LPO is equivalent to the statement that the obvious function $\mathbb{N} + 1 \to \tilde{\mathbb{N}}$ is a bijection, in constructive mathematics.

Answer 2

Such elements correspond to infinite constructor applications. In the case of $\tilde{\mathbb{N}}$, the element at infinity will correspond to succ(succ(succ(...))). You can manipulate things like this without actually going into an infinite loop if you are careful. For one thing, functions producing a type like that should be productive: they should always produce more and more of their output in a finite amount of time (or finish completely).

For example, map f will always be productive for infinite streams. On the other hand, filter p is generally not productive.

Total languages that implement coinduction/corecursion (like Agda and Coq) have a productivity/guardedness checker to verify that functions have this property. Also, these values that consist of infinite constructor applications themselves can exist without a problem if you have a lazy/non-strict evaluation order.

You don't have a separate, designated form for these "infinite values". Those things will be represented as an infinite application of constructors.

As far as bisimilarity goes, you will not be able to automatically show bisimilarity in general. It will typically require a proof. Consider the case of infinite streams. An infinite stream of Chars can also be thought of as a function of type Nat -> Char. Checking bisimilarity of streams corresponds to checking pointwise equality of those functions, which is not possible in general. It is semi-decidable: if they are not equal, you can figure this out eventually. But if they are equal, you will never know because maybe you just haven't gotten to the input where they are different yet.

Further reading

• Coinduction from a Coq perspective
• Agda's manual on coinduction

Both of those resources also talk, to some extent, about bisimulation (note that the bisimilarity relation is the largest bisimulation relation).