nLab stream

Streams

Streams

Idea

There are two notions of stream in use, as an infinite sequence or as a potentially infinite list.

Accounts which take streams to be…

Definitions

Explicit definitions

Let AA be a set. Then

  • the set of streams of AA in the sense of infinite sequences is the set of functions A A^\mathbb{N} from the natural numbers to AA

  • the set of streams of AA in the sense of potentially infinite list A *A_* is

    • the disjoint union of the set A A^\mathbb{N} of infinite sequences in AA and the set A * nA nA^* \coloneqq \biguplus_{n \in \mathbb{N}} A^n of finite lists AA.

    • the set of all infinite sequences of the disjoint union A{*}A \uplus \{*\} such that a i+1=*a_{i + 1} = * if a i=*a_i = * for any natural number ii. Finite lists are identified with a finite list of elements of AA followed by all **s, while infinite sequences is identified with a sequence of all elements of AA.

A *{a(A{*}) |i.(a i=*)(a i+1=*)}A_* \coloneqq \{a \in (A \uplus \{*\})^\mathbb{N} \vert \forall i \in \mathbb{N}.(a_i = *) \implies (a_{i + 1} = *)\}

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

A *A+ n:(Fin(n)A)A_* \coloneqq \mathbb{N} \to A + \sum_{n:\mathbb{N}} (\mathrm{Fin}(n) \to A)
A * a:(A+1) i:(a(i)=inr(*))(a(i+1)=inr(*))A_* \coloneqq \sum_{a:\mathbb{N} \to (A + 1)} \prod_{i:\mathbb{N}} (a(i) = \mathrm{inr}(*)) \to (a(i + 1) = \mathrm{inr}(*))

but if the type AA is not a set, A *A_* will not be a set either.

Coalgebraic definitions

Let AA be a set (or object of any category CC where the following makes sense). Then

  • the set of streams of AA in the sense of infinite sequences is the final coalgebra of the endofunctor XA×XX \mapsto A \times X.

  • the set of streams of AA in the sense of potentially infinite sequences is the final coalgebra of the endofunctor X1+A×XX \mapsto 1 + A \times X.

Examples

References

  • 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.