| Summary: | In 2009, Hancock, Pattinson and Ghani gave a coalgebraic characterisation of
stream processors $A^\mathbb{N} \to B^\mathbb{N}$ drawing on ideas of
Brouwerian constructivism. Their stream processors have an intensional
character; in this paper, we give a corresponding coalgebraic characterisation
of extensional stream processors, i.e., the set of continuous functions
$A^\mathbb{N} \to B^\mathbb{N}$. Our account sites both our result and that of
op. cit. within the apparatus of comodels for algebraic effects originating
with Power-Shkaravska. Within this apparatus, the distinction between
intensional and extensional equivalence for stream processors arises in the
same way as the the distinction between bisimulation and trace equivalence for
labelled transition systems and probabilistic generative systems.
|
|---|