I am studying what coinduction is. In particular, I am reading that coinductive datatypes can be defined as elements of a final coalgebra for a given polynomial endofunctor on $\tt Set$. I've seen that $A^w$, infinite streams over an alphabet $A$, is the final coalgebra of the functor $FX \rightarrow A \times X$, and similarly $A^\infty$ (finite and infinity streams over $A$) is the is the final coalgebra of $FX = {\tt id} + A × X$.

I'm wondering if the set of finite streams over $A$ is a final coalgebra for some polynomial endofunctor on $\tt Set$. In other words, if there is a way to apply coinduction over the set of finite streams over $A$. I've seen that there must exist a so called $\textit{structure map}$ that maps $X \rightarrow A \times X$ and such that for $X=$our coalgebra, the previous map is an isomorphism (Lambek’s lemma).

Our object of study is $\bigoplus A$ and clearly $A \times \bigoplus A$ is isomorphic to it, so in principle $\bigoplus$ could be a coalgebra (Lambek’s lemma is currently my only source for providing counterexamples).

I find the notion of coinduction a bit counterintuitive because I don't know yet why it is well founded, but I think it would be a bit enlightening to know if you can use coinduction over streams of finite length.

  • 2
    $\begingroup$ I'm really not an expert but my intuition tells me that any coinductive type containing infinitely many elements contains an infinite one. The argument would be something like this: If you look at elements as trees labelled by constructors, you have finitely labels and infinitely many trees so at least one tree contains the same constructor twice, and you can use that to iterate the path between both infinitely many times. $\endgroup$
    – xavierm02
    Feb 8, 2017 at 9:59
  • $\begingroup$ I wouldn't say that $\oplus A$ (if that is the finite words over $A$) is iso to $B = A \times \oplus A$, but only to $1 + A \times A$. This is because $B$ does not contain the empty word. Anyway, this looks impossible. Intuitively, if you can recurse once (i.e. if $X$ appears in your polynomial), you can corecurse infinitely many times. $\endgroup$
    – chi
    Feb 8, 2017 at 19:53
  • $\begingroup$ @xavierm02 Ah, the Koenig's Lemma approach! Nice. $\endgroup$
    – chi
    Feb 8, 2017 at 19:54


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.