There are two notions of stream in use, as an infinite sequence or as a potentially infinite list.
Accounts which take streams to be…
Let be a set. Then
the set of streams of in the sense of infinite sequences is the set of functions from the natural numbers to
the set of streams of in the sense of potentially infinite list is
the disjoint union of the set of infinite sequences in and the set of finite lists .
the set of all infinite sequences of the disjoint union such that if for any natural number . Finite lists are identified with a finite list of elements of followed by all s, while infinite sequences is identified with a sequence of all elements of .
In constructive mathematics only the second definition of potentially infinite list is a valid definition of stream. In dependent type theory, the two definitions of potentially infinite list also make sense
but if the type is not a set, will not be a set either.
Let be a set (or object of any category where the following makes sense). Then
the set of streams of in the sense of infinite sequences is the final coalgebra of the endofunctor .
the set of streams of in the sense of potentially infinite sequences is the final coalgebra of the endofunctor .
Jan Rutten, A coinductive calculus of streams, Mathematical Structures in Computer Science, Mathematical Structures in Computer Science, Volume 15, Issue 1, February 2005, pp. 93-147 (doi:10.1017/S0960129504004517)
Benedikt Ahrens, Paolo Capriotti, Régis Spadotti?, Non-wellfounded trees in Homotopy Type Theory, in 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 17-30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015) (doi:10.4230/LIPIcs.TLCA.2015.17, arXiv:1504.02949)
Bart Jacobs, Introduction to Coalgebra Towards Mathematics of States and Observation, Cambridge Tracts in Theoretical Computer Science. Cambridge: Cambridge University Press; 2016:i-iv. (ISBN:9781316823187, doi:10.1017/CBO9781316823187)
Last revised on January 3, 2024 at 02:44:14. See the history of this page for a list of all contributions to it.