8
$\begingroup$

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?

$\endgroup$
4
  • 2
    $\begingroup$ 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). map f will always be productive for infinite streams. On the other hand, filter p is generally not productive. $\endgroup$ Mar 8 at 16:13
  • 1
    $\begingroup$ 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. $\endgroup$ Mar 8 at 16:16
  • $\begingroup$ @DavidYoung: Makes sense, thanks. Two issues, though. First: do I need to represent the point at infinity, or only represent towers of succ applications (which are isomorphic to counters)? Second, closely related: can I compute bisimilarity without proofs, or am I limited to a (strict) less-than comparison? $\endgroup$
    – Corbin
    Mar 8 at 19:20
  • 1
    $\begingroup$ (1) Just the towers of applications. (2) I doubt you can get bisimilarity without proofs. Consider the case of infinite streams of Chars. An infinite stream can also be thought of as a function Nat -> Char. Determining whether two functions with that type are pointwise equal is not possible in general. In the case of $\tilde{\mathbb{N}}$ you will not, in general, be able to tell if a function produces succ applications forever or if it eventually stops somewhere far down the line. You'll only know if it does stop somewhere, not if it doesn't stop (it's semi-decidable). $\endgroup$ Mar 8 at 20:16

1 Answer 1

5
$\begingroup$

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

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

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .