# "Largest set" in coinductive definitions

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.

• The missing piece is that every element of the set is supposed to be of the specified form ($σ:s$ or what have you). So, you cannot just union with $\mathbb R$ and get another set meeting the specification, because its elements are not of the form $σ:s$. Oct 14, 2022 at 16:33

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.

• Actually this doesn't make sense, does it? The unique map into the final coalgebra can be many-to-one, so the final one doesn't have to be the largest one at all. I think this idea of "largest set" might actually just be wrong. Oct 14, 2022 at 7:53
• The point here is that for elements to be 'of the form $σ:s$,' means not just that there is any old function of type $\mathcal{E} → Σ×\mathcal{E}$. The point is to characterize it in such a way that bisimilarity coincides with set theoretic equality. For examples like this, some amount of encoding is going to be necessary unless non-well-founded sets are allowed. But the point is to be considering sets of traces, not carrier sets of any algebra. Oct 14, 2022 at 19:45

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.