nLab stream

Streams

Streams

Idea

In computer science, a stream is a finite or infinite sequence, distinguished from a list (usually assumed finite) or a sequence (usually assumed infinite).

Definition

Let AA be a set (or object of any category CC where the following makes sense). Consider the functor FF from Set (or CC) to itself that maps XX to X×A+1X \times A + 1, where 11 is the singleton set (or terminal object of CC) and ++ is the operation of disjoint union (or coproduct in CC). It is well known that the initial algebra A *A^* of FF is the set (or object) of lists on AA, which is the free monoid (or free monoid object in CC) on AA. Less well known is the final coalgebra A *A_* of FF; it is the set (or object) of streams on AA.

Properties

Classically, A *=A *+A A_* = A^* + A^{\mathbb{N}}, where =1 *\mathbb{N} = 1^* is the set of natural numbers, in Set; that is, the set of streams is the disjoint union of the set of (finite) lists and the set of (infinite) sequences. In other categories, as well as in SetSet in constructive mathematics, this need not hold. Intuitively, we cannot necessarily decide whether a given stream is a finite list or an infinite sequence until we reach the end, and we may never reach the end. (Of course, if we know that we will never reach the end, then we know that it is infinite, but we do not know this just because we haven’t reached the end so far.) In categories very different from SetSet, A *A^* will not even be a subobject of A *A_* (although there will always be a morphism from A *A^* to A *A_*, indeed a unique such FF-morphism, since these are initial and final objects of the category of FF-algebras).

Examples

An extended natural number is an element of 1 *1_* (much as a natural number is an element of 1 *1^*). Classically, such an element is either a natural number or infinity (the unique element of 1 1^{\mathbb{N}}).

Last revised on November 5, 2022 at 13:34:08. See the history of this page for a list of all contributions to it.