Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 19 of 19
About a year ago I created a github repository listing some notable endofunctors and their initial algebras and terminal coalgebras, as I couldn’t find anything like this already. This helped me get a better understanding of the landscape of these concepts.
I decided to put that list in a more prominent place, and encourage edits.
I want to mention that this is a compendium over a few twitter threads (https://twitter.com/bgavran3/status/1513217904191410190), and there might be slight errors, or inaccuracies. At this point my only goal was to get it on nLab, so these can be ironed out.
Just to mention that David Corfield and myself have added more hyperlinks to the keywords in the entry. There is room to add yet more e.g. for binary tree, list, and Moore machine. With these added, maybe the rightmost column of the table is superfluous and could be deleted to save space.
If the entry is meant to remain a bare table, then I would be inclined to not have it as a stand-alone entry but to eventually !include
it into the Examples-section at initial algebra of an endofunctor and terminal coalgebra of an endofunctor, so that it becomes part of these entries.
Just to mention that David Corfield and myself have added more hyperlinks to the keywords in the entry. There is room to add yet more e.g. for binary tree, list, and Moore machine. With these added, maybe the rightmost column of the table is superfluous and could be deleted to save space.
Thanks. I agree with the hypothesis. Perhaps we can see how the page evolves.
If the entry is meant to remain a bare table, then I would be inclined to not have it as a stand-alone entry but to eventually !include it into the Examples-section at initial algebra of an endofunctor and terminal coalgebra of an endofunctor, so that it becomes part of these entries.
I understand. The goal was to have a side-by-side comparison of initial-vs-terminal, which is the reason why I did not put the table in the examples section of either page.
The goal was to have a side-by-side comparison
Yes. All the more would it be worthwhile to include the table into these entries.
No worries, I can do this.
Maybe to clarify: This would mean your entry here remains a separate page just as it is, but that we use the !include
-command to have it display inside these other entries, too.
The only prerequisite for this is that you keep it a bare table as it is at the moment, without adding much page-infrastructure to it (which apparently you don’t intend to add anyways), which was my question in #3 (“If the entry is meant to remain a bare table,…”)
Rather, there is already a example of , which is the same as the endofunctor where is the finite set with two elements, and has initial algebra and terminal algebra according to this list. If this entry on this list are correct, then generalizing from to any set , the terminal coalgebra of the endofunctor is the sequence set .
Robert Fain
Maybe to clarify: This would mean your entry here remains a separate page just as it is, but that we use the !include-command to have it display inside these other entries, too. The only prerequisite for this is that you keep it a bare table as it is at the moment, without adding much page-infrastructure to it (which apparently you don’t intend to add anyways), which was my question in #3 (“If the entry is meant to remain a bare table,…”)
I see. That aligns with my plans; I wasn’t planning anything more than a bare table.
As defined in the stream article on the nLab, streams are the terminal coalgebra of the functor X↦1+A×X, not the functor X↦A×X. So streams belong in the same row as lists
I’ve never checked the definition of stream on nLab, but it does not agree with what I learned to be a stream from functional programming (specifically, Idris, though I believe there are more easily found resources), which that it’s a productive function, i.e. one which will never terminate.
(So I believe I think we agree that there is a distinction to be made between a potentially infinite list (i.e. one which could terminate) given by the functor X ↦ 1 + A x X and an infinite “list” (I call that streams, but not sure what’s a good name otherwise) (i.e. one which always goes on forever) given by the functor X↦A×X, it’s just a matter of naming them)
The nLab’s current definition of stream comes from Toby Bartels in 2011, who had a habit of writing definitions without referencing the existing literature. In many cases the already existing definition in the literature is different from Bartels’s definition, so it might be the case that streams are indeed defined as the final coalgebra of the action monad.
In Agda, streams are defined as:
record Stream (A : Set) : Set where
coinductive
field
hd : A
tl : Stream A
https://agda.readthedocs.io/en/latest/language/coinduction.html
My memory accords with bgravan’s and (I take it) Madeleine’s. If I were tasked with naming the elements of the terminal coalgebra of (or of ), I might call them “behaviors” – but there’s a good chance that term is already taken.
For the endofunctor , in place of stream I put “cofree coalgebra of ” and linked to cofree coalgebra.
Thomas Wilson
(I take it) Madeleine’s
I don’t really know myself, since I don’t work in the subfields of mathematics which use the word “stream”, however defined. For me, is just the set of (infinite) sequences in , and I don’t encounter the other kind of stream in the wild so I have no need to use it.
But Toby Bartels has introduced other usages of mathematical terminology in the nLab which do not really correspond to the usage elsewhere in the world (cf. linear order - which are reflexive elsewhere but irreflexive in the nLab).
It is likely, judging by the reaction of Hurkyl and other nLab members here and in https://nforum.ncatlab.org/discussion/17572/stream/#Item_0, that both definitions are used in different areas of mathematics - which probably warrants turning stream into a disambiguation page of some sort or mentioning both definitions in the article.
This would make stream similar to setoid, which for the longest time on the nLab was defined by Toby Bartels as a set equipped with an pseudo-equivalence relation, but is also used to refer to a set equipped with an equivalence relation - and both definitions are used in the literature.
My familiarity with streams comes more from the applied than theoretical context (i.e. when I’m acting as a programmer rather than as a mathematician). I’m sure I’ve seen it in mathematical contexts too, but I don’t really recall where; I can only comment that when I read “coalgebra for ” my reaction is that’s obviously right, and “coalgebra for ” my reaction is that’s obviously wrong.
(The main point of this caveat is that the nLab might have been the context where I encountered it. I’m pretty sure it’s not the only place, but I can’t say so definitively)
The main connotation of a stream is that it’s a sequence of data, but the actual data type need not actually store the data. Instead, it provides an interface letting you progress through the sequence, and it will obtain/generate more data as needed, or signal that you’ve reached the end of the stream.
While the typical application is I/O of some sort, it is also one way to provide access to an infinite sequence of data. So, given my understanding, I don’t find it surprising that someone would decide to call an infinite sequence data type a “stream”.
I will note that the code in the Agda reference page linked above has a comment noting that Stream is a type representing infinite streams (emphasis mine). So, I do think the author of that page had the similar understanding that streams can be finite sequences as well.
Regarding the question mark in the entry for the endofunctor on a closed symmetric monoidal category: I doubt one can can give a snappy uniform description for all cases, and so it’s unclear what should be put in the table. But (assuming for simplicity that the underlying category is complete): whenever the coproduct functor preserves limits of inverse -chains, for example when the coproduct preserves connected limits, which is the case for example on any extensive category , then also preserves inverse limit of -chains for any object , and so by Adamek’s theorem, the terminal coalgebra of will, as an object of , be the inverse limit of the diagram
where the map for is . For , you can think of the inverse limit as . In this case , given a coalgebra , the coalgebra map sends to when the iterate [viewing as given by a partial map together with a partial map ] is defined in but , and sends to the point if is defined in for all .
I expect the same description can be formulated and holds if is infinitary extensive, but I’ve not examined this carefully. (Meanwhile, the inverse limit description should hold in considerable generality even outside the extensive context, but by no means in absolute generality.)
None of this has anything really to do with closed symmetric monoidal structure mentioned in the entry.
I have adjusted the lead-in sentence to work within any ambient entry
and then, as discussed in #3 and following, I have !include
-ed this list of examples into the Examples-sections at initial algebra of an endofunctor and terminal coalgebra for an endofunctor
1 to 19 of 19