"Largest set" in coinductive definitions

Question

In several explanations of coinductive definitions (for example, in the answers to What is coinduction?), we're told that while an inductive definition gives us the smallest set with a specified set of properties (the constructors), coinduction gives us the largest set such with a specified set of properties (the destructors).

I'm having trouble understanding this because the notion of "largest set" doesn't seem like it should be well-defined. Clearly I'm thinking about this wrongly, but it would be helpful to know what my mistake is.

As a simple example that I've picked up from a few introductions, let's consider infinite streams over some alphabet $\Sigma$. We consider some set $\mathcal{E}$, such that if an element of $\mathcal{E}$ is of the form $\sigma{:}s$ for $\sigma\in\Sigma$, then $s\in \mathcal{E}$.

This makes some intuitive sense, even though it's a bit informal. (What does it mean for an element of an arbitrary set to "be of the form" $\sigma{:}s$?) But then the next part of the story is that we want the largest set $\mathcal{E}$ such that this is the case.

Here's my problem: surely the set $\Sigma^\infty$ of infinite streams does obey the specified property. But then surely so do other, larger sets such as $\Sigma^\infty\cup \mathbb{R}$. An element of this set is either an infinite stream (hence it's of the form $\sigma{:}s$ and we can conclude $s\in \Sigma^\infty\cup \mathbb{R}$), or it's a real number (in which case it's not of the form $\sigma{:}s$, but that's ok because we never introduced a rule saying it has to be). So it seems I can make the set as big as I want just by adding arbitrary members to it, and $\Sigma^\infty$ isn't actually the biggest set that satisfies the given property at all.

So where's my mistake? How can I think about the "largest set" in this context in a way where it's actually well-defined?

Note: I know that coinductive definitions can be formalised as final coalgebras of polynomial functors on $\mathbf{Set}$, and I actually understand that reasonably well. But I'm coauthoring a paper aimed at an audience who won't know anything about that, so my aim is to understand the more informal motivation for coinductive definitions, so that I can explain to the reader what's going on without requiring a lot of technical background. It would be quite helpful for me to know how this informal idea of "largest set" relates to the more formal notion of a terminal coalgebra.

Answer 1

Here is a tentative self-answer.

I think it must just be that there is an additional requirement that wasn't mentioned in the tutorials I read, namely that one of the destructors must apply to each element of the set.

So in the case of infinite streams we are looking at a set $\mathcal{E}$ such that

• every member of $\mathcal{E}$ is of the form $\sigma{:}s$ for some $\sigma$, and $s\in \mathcal{E}$.

When we ask for the largest set of this form it makes sense. (At least it does intuitively - it still seems a bit formally iffy to me, but it's hard to put my finger on why.)

It then becomes much more clear how this relates to the terminal coalgebra idea. A set where every member is of the form $\sigma{:}s$ can be modelled as a set $\mathcal{E}$ equipped with a function $\operatorname{decompose}\colon \mathcal{E}\to \mathcal{\Sigma}\times\mathcal{E}$, which we think of as splitting a stream up into its head and tail. If we think of this as a coalgebra of $\Sigma\times{-}$ then when we ask for a "larger set", we're asking for a new pair $(\mathcal{E}',\operatorname{decompose}')$ and a monomorphism $m\colon \mathcal{E}\to\mathcal{E}'$ such that $m$ is a coalgebra homomorphism. So then it's not so hard to imagine that the notions of "largest set" and "final coalgebra" are the same.

Answer 2

I think the precise definition of a final coalgebra might help.

Fix a set of symbols $\Sigma$. For any set $X$ define $F(X) = \Sigma \times X$, and for any $f : X \to Y$ let $F(f) : F(X) \to F(Y)$ be the map $(s, x) \mapsto (s, f(x))$. Then $F : \mathsf{Set} \to \mathsf{Set}$ is a functor.

An $F$-coaglebra is a pair $(A, a)$ where $A$ is a set and $a : A \to F(A)$ is a map, called the structure map. Such a structure map is equivalent to having two maps $\mathsf{hd}_a : A \to \Sigma$ and $\mathsf{tl}_a : A \to A$, commonly called the head and the tail operations. The relationship with with $a$ is characterized by $a(x) = (\mathsf{hd}_a(x), \mathsf{tl}_a(x))$.

A homomorphism of $F$-coalgebras $h : (A, a) \to (B, b)$ is a map $h : A \to B$ between their underlying sets that respects the structure maps: for all $x \in A$ we require $\mathsf{hd}_b(h(x)) = \mathsf{hd}_a(x)$ and $\mathsf{tl}_b(h(x)) = h(\mathsf{tl}_a(x))$.

$F$-coalgebras and homomorphisms form a category. A terminal object in this category is the terminal $F$-coalgebra. Concretely, it is an $F$-coalgebra $(E, e)$ such that for any coalgebra $(A, a)$ there is a unique homomorphism $h : A \to E$.

Let us show that $E = \Sigma^\omega$ with $e(s_0s_1s_2s_3\cdots) = (s_0, s_1s_2s_3\cdots)$ is a final $F$-coalgebra. For an arbitrary $A$, there is a unique map $h : A \to E$ satisfying $h(x) = (\mathsf{hd}_a(x), h(\mathsf{tl}_a(x))$ for all $x \in A$. It is easy to verify that this is the only one.

The unique homomorphism $h : A \to E$ need not be injective. For example, take $A = \Sigma \times \{0,1\}$ and let $a : A \to F(A)$ be $a(s, d) = (s, (s, d))$. Then $h(s,0) = h(s, 1)$ as they are both the infinite sequence of $s$'s. It is therefore somewhat imprecise to call $E$ the “largest” $F$-coalgebra – which is why officially it is called the “terminal” one. But it is helpful to think of it as being “large” in the sense that every other $F$-coalgebra maps into it.