Infinitary initial algebra specifications for stream algebras

A stream is an infinite sequence of data from a set A. A wide variety of algorithms and architectures operate continuously in time, processing streams of data, for example: hardware systems, embedded systems and emergent systems. Also many models of real number computation use streams. In this paper we study the construction of an algebra (A) over bar of streams over a many-sorted algebra A of data. In particular, we show how an initial algebra specification for (A) over bar can be constructed from one for A. One problem is that (A) over bar is uncountable even when A is finite. To handle this, we work with infinitary terms called stream terms, and infinitary formulae that generalise conditional equations, called w-conditional stream equations. We state a Birkhoff-Mal'cev type theorem that shows conservativity for the many-sorted stream version of full infinitary first-order logic L-wlw over an co-conditional equational logic, and also that certain w-conditional stream equational theories have initial models that are complete for closed stream terms. As an application of the theory, we show that the real unit interval (or real line) can be characterised up to isomorphism by an infinitary term model, which is also an initial model of a suitable co-conditional equational theory.