The paper reports on an attempt to provide a more algebraic treatment of stream processing. We treat streams within an algebra of formal languages and show its use in reasoning about streams. In particular, we give a description of the alternating bit protocol and an algebraic correctness proof for it.
The basis is the prefix order on finite words. A set of words is directed w.r.t. this order iff it is totally ordered by it. Therefore ideals, i.e., prefix closed directed sets of words, are a suitable representation of finite and infinite streams.
It is well known that the space of streams under the prefix ordering is isomorphic to the ideal completion of the set of finite streams. Since, however, ideals are just particular trace languages, we can use all operations on formal languages for their manipulation. A large extent of this is covered by conventional regular algebra. Moreover, we can apply the tools we have developed for quite different purposes in a number of earlier papers on algebraic calculation of graph, pointer and sorting algorithms
Using regular expressions rather than automata or transition systems gives considerable gain in conciseness and clarity, both in specification and calculation. While this has long been known in the field of syntax analysis, most approaches to the specification of concurrency stay with the fairly detailed level of automata, thus leading to cumbersome and imperspicous expressions. Other approaches use logical formulas for describing sets of traces; these, too, can become very involved. By extracting a few important concepts and coming up with closed expressions for them one can express things in a more structured and concise form. This is done here using regular and regular-like expressions with their strong algebraic properties.
Another advantage of our approach is that we can do with simple
set-theoretic notions thus avoiding the overhead of domain theory
and
introduction of explicit 
-elements; also we obtain a simple
treatment
of non-determinacy. Finally, we do not need additional mechanisms
for
dealing with fairness; rather, fairness is made explicit within the
generating expressions for trace languages.
We investigate the existence of continuous models and fixpoint models of higher-order specifications. Particular attention is paid to the question of extensionality. We use ordered specifications, a particular case of Horn specifications. The main tool for obtaining continuous models is the ideal completion. Unfortunately, it may destroy extensionality. This problem is inherent: we show that there is no completion method which is guaranteed to preserve extensionality. To restore it, generally a quotient has to be taken. It is shown that under certain conditions this preserves the existence of least fixpoints. Examples of the specification method include the essential concepts of Backus's FP and Hoare's CSP.