As an extensive exercise in the use of coinductive techniques, the set of all streams (here: infinite sequences of real numbers) is turned into a calculus in two ways:

the operation of `tail' of a stream is taken as a formal notion of derivative: (s0, s1, s2, ...) ' = (s1, s2, s3, ...)

a set of operators on streams is fixed, including convolution product, shuffle product, and their inverse, and a number of algebraic identities (laws) are proved.

In the stream calculus that is thus obtained, it is possible to solve so-called behavioural differential equations (equations for defining streams, formulated in terms of stream derivatives and the operators) in an algebraic fashion. The calculus will then be applied to (giving at the same time a unified perspective on):

the solution of difference equations (recurrence relations)

the solution of (certain families of) analytical differential equations

coinductive counting

generalized nondeterministic automata (including probabilistic ones)

The work presented builds on and extends my recent report:

Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Technical Report SEN-R0023, CWI, Amsterdam, 2000.