<p>I'm trying to understand how to implement corecursion in a total functional context. I've already implemented recursion using standard techniques (<code>for</code> loops) but I think I've misunderstood corecursion.</p>
<p>For our working example, consider the extended natural numbers (<a href="https://en.wikipedia.org/wiki/Extended_natural_numbers" rel="nofollow noreferrer">WP</a>, <a href="https://ncatlab.org/nlab/show/extended+natural+number" rel="nofollow noreferrer">nLab</a>); these are the natural numbers plus an extra <a href="https://en.wikipedia.org/wiki/Point_at_infinity" rel="nofollow noreferrer">element at infinity</a>. They are equipped with a natural operation <span class="math-container">$\operatorname{pred} : \tilde{\mathbb{N}} \to \tilde{\mathbb{N}} + 1$</span> 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 <span class="math-container">$\tilde{\mathbb{N}} \equiv \mathbb{N} + 1$</span>. All of this should be straightforward to implement.</p>
<p>However, the corecursion is not obvious. Quoting from nLab:</p>
<blockquote>
<p>[G]iven any set <span class="math-container">$S$</span> and map <span class="math-container">$p:S\to1+S$</span>, there is a unique map <span class="math-container">$\operatorname{corec}_{S}(p) :S \to \tilde{\mathbb{N}}$</span> such that [<span class="math-container">$p \circ \operatorname{id} + \operatorname{corec}_{S}(p) \equiv \operatorname{corec}_{S}(p) \circ \operatorname{pred}$</span>] [diagram omitted]. … You can think of <span class="math-container">$\operatorname{corec}_{S}(p)$</span> as mapping an element <span class="math-container">$a \in S$</span> to the maximum number of times that <span class="math-container">$p$</span> can be applied in succession, starting from <span class="math-container">$a$</span>, before being taken out of <span class="math-container">$S$</span>. Since this may never occur, we need ∞ as a possible value.</p>
</blockquote>
<p>But how is it possible to actually get ∞ as a result from evaluating <span class="math-container">$\operatorname{corec}_{S}$</span>? We could not arrive at ∞ without infinitely many evaluations of <span class="math-container">$p$</span>, which is unphysical. Instead, each time we evaluate <span class="math-container">$p$</span> in a row, we have a finite counter which is incremented. Is this an implementation detail or a serious misunderstanding?</p>

<implementation><functional-programming><recursion><algebraic-data-types><pure-functions>
Can total (primitive) corecursion be implemented?
CC BY-SA 4.0
2024-03-08T16:13:08.703Z
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.
David Young
CC BY-SA 4.0
2024-03-08T16:16:03.683Z
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.
David Young
CC BY-SA 4.0
2024-03-08T19:20:21.337Z
@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?
Corbin
CC BY-SA 4.0
2024-03-08T20:16:10.987Z
(1) Just the towers of applications. (2) I doubt you can get bisimilarity without proofs. Consider the case of infinite streams of `Char`s. 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).
David Young
<p>Such elements correspond to infinite constructor applications. In the case of <span class="math-container">$\tilde{\mathbb{N}}$</span>, the element at infinity will correspond to <code>succ(succ(succ(...)))</code>. 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).</p>
<p>For example, <code>map f</code> will always be productive for infinite streams. On the other hand, <code>filter p</code> is generally not productive.</p>
<p>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.</p>
<p>You don't have a separate, designated form for these &quot;infinite values&quot;. Those things will be represented as an infinite application of constructors.</p>
<p>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 <code>Char</code>s can also be thought of as a function of type <code>Nat -&gt; Char</code>. 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 <em>not</em> equal, you can figure this out eventually. But if they <em>are</em> equal, you will never know because maybe you just haven't gotten to the input where they are different yet.</p>
<h1>Further reading</h1>
<ul>
<li><a href="http://adam.chlipala.net/cpdt/html/Coinductive.html" rel="noreferrer">Coinduction from a Coq perspective</a></li>
<li><a href="https://agda.readthedocs.io/en/latest/language/coinduction.html" rel="noreferrer">Agda's manual on coinduction</a></li>
</ul>
<p>Both of those resources also talk, to some extent, about bisimulation (note that the bisimilarity relation is the largest bisimulation relation).</p>

CC BY-SA 4.0
2024-03-09T17:52:56.017Z
2024-03-09T17:52:56.017Z
David Young
<p>Your implementation <span class="math-container">$\tilde{\mathbb{N}} \equiv \mathbb{N} + 1$</span> can only work in the presence of classical principles like the <a href="https://ncatlab.org/nlab/show/principle+of+omniscience" rel="nofollow noreferrer">limited principle of omniscience</a>. In fact, LPO is <em>equivalent</em> to the statement that the obvious function <span class="math-container">$\mathbb{N} + 1 \to \tilde{\mathbb{N}}$</span> is a bijection, in constructive mathematics.</p>

CC BY-SA 4.0
2024-07-13T16:10:24.630Z
2024-07-13T16:10:24.630Z
Naïm Favier
CC BY-SA 4.0
2024-07-13T18:07:02.340Z
As it’s currently written, your answer is unclear. Please [edit] to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers [in the help center](/help/how-to-answer).
Community Compiler
CC BY-SA 4.0
2024-07-13T18:21:15.547Z
I don't obey or talk to bots, but if a human triggered this, please clarify *what* you think needs clarification.
Naïm Favier
# Can total (primitive) corecursion be implemented?
Posted by: username_0 on 2024-03-08
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](https://en.wikipedia.org/wiki/Extended_natural_numbers), [nLab](https://ncatlab.org/nlab/show/extended+natural+number)); these are the natural numbers plus an extra [element at infinity](https://en.wikipedia.org/wiki/Point_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?
**Tags:** implementation functional-programming recursion algebraic-data-types pure-functions
> **Comments:**
> **username_1**: 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.  
> **username_1**: 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.  
> **username_0**: @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?  
> **username_1**: (1) Just the towers of applications. (2) I doubt you can get bisimilarity without proofs. Consider the case of infinite streams of `Char`s. 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).  
---
## 2 answers
### Answer by username_2 on 2024-07-13. Score: 1 | Accepted answer
Your implementation $\tilde{\mathbb{N}} \equiv \mathbb{N} + 1$ can only work in the presence of classical principles like the [limited principle of omniscience](https://ncatlab.org/nlab/show/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.
> **Comments:**
> **username_3** (2024-07-13): As it’s currently written, your answer is unclear. Please [edit] to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers [in the help center](/help/how-to-answer).  
> **username_2** (2024-07-13): I don't obey or talk to bots, but if a human triggered this, please clarify *what* you think needs clarification.  
---
### Answer by username_1 on 2024-03-09. Score: 5
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 `Char`s 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](http://adam.chlipala.net/cpdt/html/Coinductive.html)
* [Agda's manual on coinduction](https://agda.readthedocs.io/en/latest/language/coinduction.html)

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