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: coinductive free things

Naso (Mar 02 2021 at 00:47):

Question about coinductive free things:

For a fixed set $A$ , $A^*$ is the free monoid on $A$ where elements are finite strings in $A$ and multiplication is concatenation.
There is also the monoid $A^\omega$ of finite or infinite strings in $A$ that contains $A^*$ as a submonoid, where $a * b = a$ if a is infinite, .
In computer science I think it is called the 'coinductive list monoid'.
Another well known example is the conatural numbers (that is the coinductive free monoid on a singleton set) which is the natural numbers + infinity.

In category theory these free structure come from left adjoints to a forgetful functor.
Where do the coinductive free structures come from? Is it actually the right adjoint??

Also, is there any reason why coinductive structures seem to be uncommon in maths since in computer science they seem to be quite important?

Christian Williams (Mar 02 2021 at 01:05):

Yes, the "cofree" structures come from having a right adjoint to the forgetful $Coalg\to Set$ . I haven't yet gotten a solid intuition of coinduction, but it seems very powerful. Bart Jacobs' book http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf is a good introduction.

Christian Williams (Mar 02 2021 at 01:05):

As for why it's become prominent in CS and not math, that is a very good question.

Naso (Mar 02 2021 at 01:09):

Thank you Christian

John Baez (Mar 02 2021 at 01:21):

For some reasons (which we could get into) mathematicians like to describe algebraic structures - like groups, rings, etc. - using Lawvere theories, and then it's very handy that any structure of a given kind can be described using free ones, either directly as an algebra of a monad on Set, or as a coequalizer of free algebras (which is almost the same thing).

What would happen to math if took the other path and tried to use coalgebras of comonads on Set?

Mike Shulman (Mar 02 2021 at 01:25):

One possible reason is that mathematicians are generally happy to work directly with infinite things, whereas programmers are forced to encode infinite things with finite information. One of the uses of coinductive structures is to do the latter, but mathematicians don't need them as much for this. Sometimes what the mathematicians are doing would be clarified by a coinductive perspective, but coinduction also has limitations relative to explicit infinity, so the mathematicians aren't hugely motivated to pick it up.

John Baez (Mar 02 2021 at 01:29):

mathematicians are generally happy to work directly with infinite things

:muscle: It's interesting how we convince ourselves that we can do this.

John Baez (Mar 02 2021 at 01:30):

It's not as if our brains are infinitely big.

Mike Shulman (Mar 02 2021 at 01:55):

Another possible reason is that mathematics is generally static whereas programming can be dynamic. For instance, variables in mathematics don't change their values; if we let $x=3$ then we don't go back later and say let $x = x+1$ , and there's no analogue of a for-loop in mathematics: we only use recursion and induction, never iteration. The relevance of this here is that inductive definitions are datatypes that describe what something is, in a static way, whereas coinductive definitions are interfaces or behaviors that a dynamic process can implement.

Mike Shulman (Mar 02 2021 at 02:00):

The usual description of a coinductive definition as an infinite object is the "trace" of all possible execution paths of a process, but since a corecursively defined function doesn't evaluate until it's "forced", I sometimes find it helpful to instead think of the definition of such a function as creating an "object" or "process" that you can "communicate" with by applying a destructor, thereby getting a response and/or changing its "state".

Mike Shulman (Mar 02 2021 at 02:14):

John Baez said:

What would happen to math if took the other path and tried to use coalgebras of comonads on Set?

Of course, coalgebraic structures do pop up in mathematics. But it's true that they generally tend to play second fiddle to algebraic ones. I wonder how much of that can be blamed on the nature of our base categories like Set.

What are some good examples of categories that are comonadic over Set? Here are two simple ones:

If $M$ is a monoid, then the category of $M$ -sets is both monadic and comonadic. The comonad is $X \mapsto X^M$ .
If $A$ is any set, then the slice category $\mathrm{Set}/A$ is comonadic. The comonad is $X \mapsto X\times A$ .

Mike Shulman (Mar 02 2021 at 02:15):

Here are some relevant old discussions from the n-Cafe: https://golem.ph.utexas.edu/category/2008/11/coalgebraically_thinking.html, https://golem.ph.utexas.edu/category/2008/12/the_status_of_coalgebra.html. Maybe John can find more.

Naso (Mar 04 2021 at 00:21):

Thank you all for the references.
I still have some basic questions maybe someone can help me clear up.

First, what is it that makes coalgebras about 'processes' and algebras about 'structures'? Is it simply because given an algebra $a : FA \to A$ and $x \in FA$ we can only apply $a$ once to $x$ , but if we have a coalgebra $c : A \to FA$ and a $y \in A$ we can do it many times to get a sequence $y, cy, Fc(cy),...$ ?

Second, for the examples I mentioned I don't see how the monoid operation is determined by the coalgebra. E.g., the set of (co)natural numbers are defined as an initial (terminal) algebra (on Set) to $F X = 1 + X$ which determine them as sets with a zero and successor (predecessor) function. But do those functions canonically determine the monoid operations $+$ on the natural and conatural numbers?

Third, Christian mentioned the cofree structures are coming from a right adjoint to the forgetful $Coalg \to Set$ . What about e.g. the right adjoint to the forgetful $Monoid \to Set$ --does it exist? and if so, when applied to a singleton set does it give the conatural numbers?

Fourth, what does it mean and what is the significance of a category being (co)monadic? I only found the definitions for (co)monadic functors but I don't really see the connection to all of this.

Mike Shulman (Mar 04 2021 at 03:31):

Nasos Evangelou-Oost said:

First, what is it that makes coalgebras about 'processes' and algebras about 'structures'? Is it simply because given an algebra $a : FA \to A$ and $x \in FA$ we can only apply $a$ once to $x$ , but if we have a coalgebra $c : A \to FA$ and a $y \in A$ we can do it many times to get a sequence $y, cy, Fc(cy),...$ ?

That's part of it. Another aspect is how they are implemented in a programming language. Suppose you define an infinite stream of ones by ones := 1 :: ones. We can't try to evaluate this completely right away, the way we could with the definition of a finite list, or we would go into an infinite spin. So instead the computer stores the definition of ones as a sort of "thunk" or "callback" (or "lazy list"), and only evaluates it further when some other part of the program tries to inspect the elements of ones (necessarily some finite initial segment thereof). In general, the definition of an element of a coinductive type could be quite a complicated function, and instead of being evaluated right away it is saved and "called" when the destructors are applied. Thus, we can think of the destructors of a coinductive type as defining an "interface" -- the things that other parts of the program can "call" -- and the definition of an element of the coinductive type as creating an object that implements that interface, by specifying the "methods" that instantiate the interface.

Mike Shulman (Mar 04 2021 at 03:31):

Second, for the examples I mentioned I don't see how the monoid operation is determined by the coalgebra. E.g., the set of (co)natural numbers are defined as an initial (terminal) algebra (on Set) to $F X = 1 + X$ which determine them as sets with a zero and successor (predecessor) function. But do those functions canonically determine the monoid operations $+$ on the natural and conatural numbers?

Yes, in that you can use the (co)recursion principles to construct the monoid operations. But that's something special to these examples: an arbitrary (co)inductive type doesn't come with a monoid operation.

Mike Shulman (Mar 04 2021 at 03:32):

Third, Christian mentioned the cofree structures are coming from a right adjoint to the forgetful $Coalg \to Set$ . What about e.g. the right adjoint to the forgetful $Monoid \to Set$ --does it exist? and if so, when applied to a singleton set does it give the conatural numbers?

It does not exist. That forgetful functor does not preserve colimits.

Mike Shulman (Mar 04 2021 at 03:33):

Fourth, what does it mean and what is the significance of a category being (co)monadic? I only found the definitions for (co)monadic functors but I don't really see the connection to all of this.

Roughly speaking, a monadic category is one whose objects are sets (or whatever other base category you have) equipped with "algebraic structure", while in a comonadic category they are equipped with "coalgebraic structure".

Mike Shulman (Mar 04 2021 at 03:50):

(By the way, regarding the rarity of coinduction in mathematics, there's probably also an interesting story to be told regarding the foundation axiom of ZFC and the much less well-known anti-foundation axioms of Aczel, Finsler, etc.)

Ralph Sarkis (Mar 04 2021 at 09:27):

I wanted to add that Paolo's notes give different intuitions about comonads.

Ralph Sarkis (Mar 04 2021 at 09:27):

After quickly reading it before posting, I thought it might be good to emphasize here that coalgebras of an endofunctor and coalgebras of a comonad are different things (I am not sure how much though). Paolo shows in Example 5.4.8 that coalgeberas of the stream comonad $(-)^{\mathbb{N}}$ are streams that look like $(a,f(a),ff(a),\dots)$ which is a big restriction over the arbitrary streams that are coalgebras of the endofunctor $(-)^{\mathbb{N}}$ .

Ralph Sarkis (Mar 04 2021 at 09:27):

Another thing mentioned in Example 5.3.7 is that a co-Kleisli morphism for the stream comonad, being a function $X^{\mathbb{N}} \rightarrow Y$ , may depend on the whole stream which is not very CS-friendly. What that tells me is that cofree structures should be less relevant in CS, but I don't know if that is true.

JS PL (he/him) (Mar 04 2021 at 09:41):

Ralph Sarkis said:

What that tells me is that cofree structures should be less relevant in CS, but I don't know if that is true.

I'll defend comonads in CS here and say that comonads are fundamental to categorical semantics of linear logic. In particular, the comonad captures the exponential modality $!$ . Futhermore, the coKleisli category in this case is going to be Cartesian closed category, and therefore a model of the $\lambda$ -calculus. The idea being that coKleisli maps $! A \to B$ should be thought of as smooth maps, while the maps in the base category $A \to B$ are the linear maps.

JS PL (he/him) (Mar 04 2021 at 09:42):

(I don't know if my comment is useful to the conversation above, but thought it was worth mentionning. I apologies if it's not!)

Mike Shulman (Mar 04 2021 at 14:56):

The relation between endofunctor-coalgebras and comonad-coalgebras is that if cofree coalgebras for an endofunctor exist, then they are the values of a comonad whose comonad-coalgebras coincide with the original endofunctor-coalgebras. So, at least under niceness hypotheses, comonad-coalgebras are a more general concept, as they include all endofunctor-coalgebras as well as other things.

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

What do you mean @Mike Shulman? If $F$ is an endofunctor and $T\to FT$ is a cofree coalgebra of $F$ , then what is the comonad whose comonad-coalgebras coincide with $F$ 's endofunctor-coalgebras?

Fawzi Hreiki (Mar 04 2021 at 16:22):

This is a special case of the fact that an action $A \otimes B \rightarrow B$ of an object $A$ on another object $B$ in a monoidal category is the same thing as an action of the free monoid $F(A)$ on $B$ .

Fawzi Hreiki (Mar 04 2021 at 16:23):

Well, its a special case of the dual statement.

Fawzi Hreiki (Mar 04 2021 at 16:24):

Unfortunately, the monoidal category of endofunctors does not have free (co)monoids in general, but when a given endofunctor has a free co-monad, the co-algebras of the co-monad will correspond to the co-algebras of the underlying endofunctor.

Mike Shulman (Mar 04 2021 at 16:25):

Right. Explicitly, the comonad is the functor that sends $X$ to the cofree coalgebra on $X$ .

Fawzi Hreiki (Mar 04 2021 at 16:26):

Is there a general criterion for when this assembles into a co-monad?

John Baez (Mar 04 2021 at 16:35):

Mike made it sound like it always does, given that the cofree coalgebra on any object exists:

if cofree coalgebras for an endofunctor exist, then they are the values of a comonad whose comonad-coalgebras coincide with the original endofunctor-coalgebras.

Fawzi Hreiki (Mar 04 2021 at 16:36):

Ah I missed that. Thanks

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

I'm currently trying to verify this...so far I've got that given an endofunctor $F:C\to C$ , the existence of cofree coalgebras on all objects $X:C$ is equivalent to each comma category $X/U$ having a terminal object, where $X:C$ and $U:\text{Coalg-}F\to C$ is the forgetful functor, which by a standard theorem, is in turn equivalent to $U$ having a right adjoint $G$ sending $X$ to the terminal object of $X/U$ . So the functor it seems that Mike is talking about is $UG:C\to C$ . So then this is a comonad.

Joshua Meyers (Mar 04 2021 at 17:13):

So given an endofunctor-coalgebra $(X,f:X\to FX)$ , there is a unique coalgebra-morphism $g: (X,F)\to GX$ , which gives a morphism $Ug: X\to UGX$ . So we just need to verify that $Ug$ is a comonad-coalgebra and that $(X,f)\mapsto (X,Ug)$ is a bijection between $F$ -endofunctor-coalgebras and $UG$ -comonad-coalgebras.

Mike Shulman (Mar 04 2021 at 18:14):

One place the dual argument is written out is https://maciejcs.wordpress.com/2012/04/17/free-monads-and-their-algebras/