Streams and coinduction in mathematics and computer scienceJan Rutten (janr@cwi.nl) Abstract Iakov Romanovski and Peter E. Caines Based on the presence of a final coalgebra structure on the set of streams (infinite sequences), a coinductive calculus of streams is developed. The main ingredient is the notion of stream derivative, with which both coinductive proofs and definitions can be formulated. In close analogy to classical analysis, the latter are presented as behavioural differential equations. We shall (1) explain the basics of coinductive definitions and proofs for streams over an arbitrary set of elements. We then (2) study streams of real numbers, for which we develop an algebraic calculus of operators, making intensive use of coinductive reasoning. An initial application of this calculus will be the solution of difference equations. Next we deal with two more mathematical applications: (3) (analytical) differential equations and (4) counting problems from enumerative combinatorics. Finally, we give an application in computer science, on: (5) a coinductive calculus of component (as in component software engineering) connectors. The numbers (1)--(5) correspond (roughly) to five lectures of one hour each. The material of the lectures is (at this very moment) being collected into a set of lecture notes. It is based on the following papers, of which all but the last one are available at www.cwi.nl/~janr. (The titles of these papers mercilessly reveal an obsession with coinduction.) J.J.M.M. Rutten Automata and coinduction (an exercise in coalgebra). Proceedings of CONCUR '98 (D. Sangiorigi and R. de Simone eds.), LNCS 1466, Springer, 1998, pp. 194-218. J.J.M.M. Rutten Automata, power series, and coinduction: taking input derivatives seriously (extended abstract). In proceedings of ICALP '99 (J. Wiedermann, P. van Emde Boas and M. Nielsen, eds.), LNCS 1644, Springer, 1999, pp. 645-654. J.J.M.M. Rutten Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Technical Report SEN-R0023, CWI, Amsterdam, 2000. To appear in Theoretical Computer Science. J.J.M.M. Rutten Elements of stream calculus (an extensive exercise in coinduction). Proceedings of the 17th Annual Conference on Mathematical Foundations of Programming Semantics (MFPS '01), Aarhus, Denmark, 2001, ENTCS Volume 45 , Elsevier Science B.V., 2001. J.J.M.M. Rutten Coinductive counting: bisimulation in enumerative combinatorics. Proceedings of Coalgebraic Methods in Computer Science (CMCS '02), ENTCS Volume 65 , Elsevier Science B.V., 2002. F. Arbab and J.J.M.M. Rutten A coinductive calculus of component connectors. Technical Report SEN-R02??, CWI, Amsterdam, 2002, to appear. |