Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: intuition about cofree things

Joshua Meyers (Mar 10 2021 at 13:56):

The cofree coalgebra on the signature $\{s,0\}$ (where $s$ is a unary function and $0$ is a constant is the extended natural numbers $\mathbb{N}^*\coloneqq \{0,1,2\ldots,\infty\}$ with $sn=n+1$ for $n<\infty$ and $s\infty=\infty$.

So I totally see why this is the final coalgebra of the endofunctor corresponding to this signature.

But the other intuition I am supposed to have about cofree things, that they are the largest things closed under certain operations, seems not to work. This intuition tells me I should also have $\infty'$ distinct from $\infty$ with $s\infty'=\infty'$, because that would make it larger, for instance. If we're really trying to make it as large as possible, why not have a proper class of 1-cycles, a proper class of 2-cycles, etc. Why not have $a\neq b$ with $sa=sb$? Why not have everything that can happen happen? How is this intuition supposed to work?

Kenji Maillard (Mar 10 2021 at 14:28):

Isn't it the case that any additional $\infty'$ such that $s\infty' = \infty'$ will be bisimilar to $\infty$ (all the operations map these two points to bisimilar points, coinductively so) ? So even if you could add more points, you already have all the possible observable behaviours

Joshua Meyers (Mar 10 2021 at 14:36):

That's helpful...why don't we have an additional $x,y$ with $sx=y$ and $sy=x$ then? That seems like a new behavior

Kenji Maillard (Mar 10 2021 at 14:53):

I don't think so : you could define a relation $R \subseteq \mathbb{N}^* \times (\mathbb{N}^* \cup \{x,y\})$ relating both $x$ and $y$ to $\infty$ that is a witness of the bisimilarity of $x$ and $y$ with $\infty$. Since you do not have an operation observing the equality of elements, you cannot distinguish the cycle $\{x,y\}$ from just $\{\infty\}$.

Jules Hedges (Mar 10 2021 at 14:54):

A common intuition is something like "algebras are, coalgebras do". The final coalgebra on this signature can be usefully thought of as a sort of state machine. If you press the "s" button it will do a state change where it reduces the state variable by 1, or stays in the same state if it was in the "infinity" state

Joshua Meyers (Mar 10 2021 at 14:59):

Don't we have a bisimulation $R\subseteq \mathbb{N}^*\times \{\infty\}$ relating everything in $\mathbb{N}^*$ to $\infty$ then?

Joshua Meyers (Mar 10 2021 at 15:00):

Or maybe the problem with that it is wouldn't preserve the $0$ constant

Joshua Meyers (Mar 10 2021 at 15:31):

How can you describe a cofree object for a given signature in terms of bisimulation?

Mike Shulman (Mar 10 2021 at 16:23):

I think "largest things closed under certain operations" isn't a good intution for coinductive types. First of all, it should really be "largest things COclosed under certain COoperations". But also, I think "largest" is misleading except when the ambient category is a poset, such as for a coinductively defined predicate. When working with a category that's not a poset, it's better to replace "largest" with "terminal" wherever you see it.

Joshua Meyers (Mar 10 2021 at 16:26):

With inductive types, the intuition "smallest thing closed under certain operations" works great! What is the dual intuition for coinductive types?

Joshua Meyers (Mar 10 2021 at 16:30):

I guess you said it, "largest things COclosed under certain COoperations". So what does "coclosed" mean?

Kenji Maillard (Mar 10 2021 at 17:37):

Joshua Meyers said:

Don't we have a bisimulation $R\subseteq \mathbb{N}^*\times \{\infty\}$ relating everything in $\mathbb{N}^*$ to $\infty$ then?

I got puzzled by your question because that sounded plausible. Actually I think it is indeed the case that any point in $\mathbb{N}^*$ would be bisimilar to $\infty$ if we take the $s$ you provided as the coalgebra structure. But at least according to wikipedia that's not the right coalgebra structure on $\mathbb{N}^* = \mathbb{N} \cup \{\infty\}$ making that set into the final coalgebra on the signature $\{s : [1] \to [1], 0 : [0] \to [1]\}$. The coalgebra structure given there is $\alpha : \mathbb{N}^* \to \mathbb{N}^* \uplus \{\ast\}$ defined by $\alpha~0 = \ast$, $\alpha~n = n -1$ if $0 < n < \infty$ and $\alpha \infty = \infty$. So you can observe $0$ and distinguish any finite number from $\infty$ by sufficient applications of the coalgebra map.

Mike Shulman (Mar 10 2021 at 23:53):

Well, the emphasis is probably on the co- in co-operations rather than co-closed. The point is that a coinductive type is defined by destructors, not constructors. For instance, a coalgebra for the "natural numbers" functor $X\mapsto X+1$ doesn't have a "zero operation" and "successor operation" the way an algebra does; it has a single destructor $X\to X+1$ that either returns a predecessor or says "I'm zero, I have no precedessor".

Joshua Meyers (Mar 11 2021 at 00:18):

Mike Shulman said:

Well, the emphasis is probably on the co- in co-operations rather than co-closed. The point is that a coinductive type is defined by destructors, not constructors. For instance, a coalgebra for the "natural numbers" functor $X\mapsto X+1$ doesn't have a "zero operation" and "successor operation" the way an algebra does; it has a single destructor $X\to X+1$ that either returns a predecessor or says "I'm zero, I have no precedessor".

OK that clarifies things substantially. Since we want the largest structure with this destructor, we would like to have elements with every possible "destructor profile" --- an element with no predecessor, an element which has a predecessor but whose predecessor has no predecessor, and element whose predecessor has a predecessor but whose predecessor's predecessor has no predecessor, etc., as well as an element which has an $$n$$th predecessor for all $n\in\mathbb{N}$.

However, we do want to avoid redundancy: the cofree structure should not ever have two elements with the same destructor profile --- is this a general rule for cofree structures on equational (co)signatures?

It seems like this avoidance of redundancy is dual to the absence of equalities in free structures on equational signatures. How can this be made precise?

Martti Karvonen (Mar 11 2021 at 00:43):

It's the terminality of the coalgebra mentioned earlier: if you had e.g. two elements with the same "destructor profile", then a coalgebra built from just such an element would map into ours in two ways.

Joshua Meyers (Mar 11 2021 at 00:50):

Right, the picture of cofree coalgebras as terminal coalgebras makes a lot of sense to me. But I'm wondering if it's possible to dualize the picture of free algebras as smallest sets closed under operations.

Mike Shulman (Mar 11 2021 at 01:14):

I just don't have that picture. In my head, for something to be "closed under" some operations, it has to be a subset of some larger structure on which those operations are defined. An abstract group, for instance, isn't "closed under" multiplication; what's "closed under" multiplication is a subgroup of some given group.

Martti Karvonen (Mar 11 2021 at 01:17):

Also: absence of equations should give you weak initiality, and adding "no extra junk" promotes this to initiality, and similarly, having each destructor profile present should give weak terminality, and the "no redundancy" above should promote this to terminality.

Joshua Meyers (Mar 11 2021 at 04:09):

Martti Karvonen said:

Also: absence of equations should give you weak initiality, and adding "no extra junk" promotes this to initiality, and similarly, having each destructor profile present should give weak terminality, and the "no redundancy" above should promote this to terminality.

Nice!

Joshua Meyers (Mar 11 2021 at 04:12):

having each destructor profile present should give weak terminality

Here's a counterexample: Let $[n]\coloneqq \{0,1,2,\ldots n\}$ with $[n]\to [n]+1$ given by $x\mapsto \text{inl}(x-1)$ for $x>0$ and $0\mapsto \text{inr}(0)$. Then $\sum_{n=0}^\infty [n] + \{\infty\}$ (where $\infty\mapsto\infty$) has every destructor profile, but there is no morphism from $\mathbb{N}$ to it.

Joshua Meyers (Mar 11 2021 at 04:16):

Mike Shulman said:

I just don't have that picture. In my head, for something to be "closed under" some operations, it has to be a subset of some larger structure on which those operations are defined. An abstract group, for instance, isn't "closed under" multiplication; what's "closed under" multiplication is a subgroup of some given group.

Sure, so let's say that a free magma on $\{x,y\}$ is the smallest subset of $\{x,y,(,)\}^*$ (where ${}^*$ is Kleene star) which contains $x$ and $y$ and is closed under the operation taking two strings $s$ and $t$ and outputting $(st)$.

Naso (Mar 11 2021 at 04:17):

Mike Shulman said:

Well, the emphasis is probably on the co- in co-operations rather than co-closed. The point is that a coinductive type is defined by destructors, not constructors. For instance, a coalgebra for the "natural numbers" functor $X\mapsto X+1$ doesn't have a "zero operation" and "successor operation" the way an algebra does; it has a single destructor $X\to X+1$ that either returns a predecessor or says "I'm zero, I have no precedessor".

I understood what you said in this comment from 2011 as saying that the coinductive naturals ARE defined with the zero and successor: https://golem.ph.utexas.edu/category/2011/07/coinductive_definitions.html#c038996 . Similarly I've heard people say e.g. that types defined in Haskell are coinductive rather than inductive, yet they're defined by constructors, and not destructors. Could you clarify this point please? (Edit: rereading my comment it sounds like I may be accusing you of being unclear--please know that is totally not my intention, I'm 100% sure it is just my being confused/dense :) )

Martti Karvonen (Mar 11 2021 at 04:58):

Joshua Meyers said:

having each destructor profile present should give weak terminality

Here's a counterexample: Let $[n]\coloneqq \{0,1,2,\ldots n\}$ with $[n]\to [n]+1$ given by $x\mapsto \text{inl}(x-1)$ for $x>0$ and $0\mapsto \text{inr}(0)$. Then $\sum_{n=0}^\infty [n] + \{\infty\}$ (where $\infty\mapsto\infty$) has every destructor profile, but there is no morphism from $\mathbb{N}$ to it.

You're right, I was being too optimistic.

Mike Shulman (Mar 11 2021 at 16:37):

Joshua Meyers said:

Sure, so let's say that a free magma on $\{x,y\}$ is the smallest subset of $\{x,y,(,)\}^*$ (where ${}^*$ is Kleene star) which contains $x$ and $y$ and is closed under the operation taking two strings $s$ and $t$ and outputting $(st)$.

That's not the definition of "free magma"; it's one particular construction of it.

Martti Karvonen (Mar 11 2021 at 16:41):

To drive the point home, if you're compiling this construction in standard material set theory, and your friend is using a different construction of ordered pairs, they'll end up with a different set as the free magma (using otherwise the same construction). Neither of the end results is smaller than the other, and it's the initiality of the end result that really matters.

Mike Shulman (Mar 11 2021 at 16:46):

Nasos Evangelou-Oost said:

I understood what you said in this comment from 2011 as saying that the coinductive naturals ARE defined with the zero and successor: https://golem.ph.utexas.edu/category/2011/07/coinductive_definitions.html#c038996 . Similarly I've heard people say e.g. that types defined in Haskell are coinductive rather than inductive, yet they're defined by constructors, and not destructors.

This is actually a long-standing confusion about coinductive types, which has only recently started to be resolved. So while there is something to that comment of mine from 2011, its phrasing is based on that old confusion. In particular, the constructor-based ("positive") Coq syntax for coinductive types that I used in that comment is now deprecated in favor of a destructor-based ("negative") one.

Mike Shulman (Mar 11 2021 at 17:01):

The categorical definition of coinductive type is as a terminal coalgebra, and if you translate this directly into syntax you get a definition in terms of destructors. So a destructor-based definition is the only one that's semantically justified, and recently people realized that it's also the only one that's syntactically well-behaved: at least in the presence of dependent types, constructor-based coinductive types break subject reduction. (See for instance the appendix of these slides.)

Mike Shulman (Mar 11 2021 at 17:06):

It is true that destructor-based coinductive types have constructors, because the structure map $X \to T X$ of a terminal coalgebra is an isomorphism by Lambek's lemma, hence it has an inverse $TX \to X$. And the informal description of coinductive types that I gave in that comment is correct. But it doesn't work syntactically (at least in dependent type theory) to allow "matching" against those constructors, and we shouldn't think of a coinductive type as defined by constructors rather than destructors.

Mike Shulman (Mar 11 2021 at 17:17):

The status of Haskell is less clear to me. Certainly its laziness means that its "datatypes" can be infinite, like coinductive types and unlike inductive ones. Haskell does permit matching against datatype constructors, but since Haskell isn't dependently typed, it's possible that constructor-based coinductive types aren't problematic. So I guess the thing to say is that Haskell's datatypes are positive coinductive types, but be aware that at least in dependent type theory it's more correct to view coinductive types negatively.

Joshua Meyers (Mar 11 2021 at 17:30):

Mike Shulman said:

Joshua Meyers said:

Sure, so let's say that a free magma on $\{x,y\}$ is the smallest subset of $\{x,y,(,)\}^*$ (where ${}^*$ is Kleene star) which contains $x$ and $y$ and is closed under the operation taking two strings $s$ and $t$ and outputting $(st)$.

That's not the definition of "free magma"; it's one particular construction of it.

Sure, I like this method of construction because I like to think in terms of syntax. Is there a similar, very concrete, syntactic construction (or maybe, "destruction") of cofree things?

Mike Shulman (Mar 12 2021 at 01:46):

In some cases at least, you can define the elements of a coinductive type to be compatible streams of elements of a corresponding inductive type that are its "finite approximations".

GhaS Shee (Mar 12 2021 at 13:54):

Mike Shulman said:

Well, the emphasis is probably on the co- in co-operations rather than co-closed. The point is that a coinductive type is defined by destructors, not constructors. For instance, a coalgebra for the "natural numbers" functor $X\mapsto X+1$ doesn't have a "zero operation" and "successor operation" the way an algebra does; it has a single destructor $X\to X+1$ that either returns a predecessor or says "I'm zero, I have no precedessor".

I have been holding one question. ( It might be a silly question! )
For the case of natural number, I cannot find why $X → X + 1$ is the coalgebra rather than $X → X × 1$ is.
That is, my question is, " why cannot the category be an abelian cateogory ? "

D.G. Berry (Mar 12 2021 at 13:58):

Surely X×1 is isomorphic with just X?

Kenji Maillard (Mar 12 2021 at 14:02):

You can ask what are the initial algebra and final coalgebra for the endofunctor $X \mapsto X + 1$ in an abelian category (which is then isomorphic to $X \mapsto X \times 1$ but also to $X \to X$), and the answer is just that both are the zero object $1 \cong 0$ I think

GhaS Shee (Mar 12 2021 at 14:03):

@D.G. Berry @Kenji Maillard
Ah, yes! Thank you very much. Really, it is!
( Now I modified my intuition about products and coproducts.
I now start to think it is abelian categories that are strange! )

Joshua Meyers (Mar 12 2021 at 14:11):

Well the coalgebras $X\to X+1$ and $X\to X\times 1$ are both valid things to consider, it's not that one is right and the other is wrong.

Mike Shulman (Mar 12 2021 at 15:54):

But the terminal coalgebra of $X\mapsto X$ is always just the terminal object, so despite its validity, it's not usually the thing you want to consider. (-: