Werkcollege op donderdag 13.45 - 15.30, zaal M143, docent drs. C. Grabmayer.

Colleges: 7 april, 14 april, 21 april, 28 april, (5 mei: geen college),
12 mei, 19 mei.

Werkcolleges: 8 april, 15 april, 22 april, 29 april,
(6 mei: geen werkcollege),
13 mei,
24 mei.

The last practicum (werkcollege)
takes place on
Monday, May 24th,
14:00-15:45 in seminar-room
KA223.

Tentamen: donderdag 27 mei 2004, 13.30 - 16.30, Q105.

Er zal het volgende engelstalige dictaat worden gebruikt:

J.J.M.M. Rutten.

An application of coinductive stream calculus to signal flow graphs.

Technical Report SEN-E0305.

Centrum voor Wiskunde en Informatica (CWI), Amsterdam, 2003, pp. 1--53.

Dit dictaat is -- als pdf file -- op het web te vinden via de
home page
van de docent, danwel
rechtstreeks
in de rapporten-database van het CWI.

Tevens zal op het eerste college
op 7 april een afdruk van het eerste hoofdstuk
worden uitgedeeld.
Hieronder treft u de `preface'
aan van dit dictaat, dat een samenvatting geeft van de
te behandelen stof.

Preface:

Infinite sequences or streams
occur at many different places
in both mathematics and computer science.
For the latter, think of bit streams flowing through
the chips of your computer, or through the ether carrying
messages from your mobile telephone. More generally,
signals in the theory of signal processing are
commonly represented by streams of real numbers.
Also functions on streams are relevant in that setting,
as they are the building blocks for filters and
converters (such as the digital to analog
converter in cd-players).
Yet another example in computer science where streams
appear is dataflow, which studies networks
consisting of nodes and channels, through
which streams of data elements flow.
Such stream-based dataflow models have recently also
been used in the area of component-based
software engineering, where a process or software component
can be specified in terms of a relation on the
streams of ingoing and outgoing messages (or data elements)
at each of its communication ports.

Streams occur also in various areas of mathematics. Examples are the use of streams in analysis: the basic notion of limit is formulated in terms of streams, and the Taylor series of analytical functions (such as (0,1,0,-1,0,1,0,-1, ...) for sin(x)) are streams; in combinatorics, streams are often defined by recurrence relations or difference equations, for instance representing the solution of counting problems (such as the stream of Fibonacci numbers (1,1,2,3,5,8, ... )); streams are used to model trajectories in dynamical systems.

Many more examples exist. These notes intend to study streams as such, in principle independent of any of the afore mentioned areas, but often taking examples from some of them, mostly from computer science. We shall develop systematic ways for:

(1) defining and specifying streams (and functions on streams);

(2) reasoning about streams, notably proving equalities between them; and

(3) implementing streams, in particular using some basic form of (stream) circuits.

All of this will involve a bit of elementary but not so standard mathematics, which will be explained in all detail along the way. In short, because streams form an infinite datatype, the mathematical techniques of algebraic specification that are traditionally used for finite data types, are not really appropriate. Instead, we shall use a new proof and definition principle called coinduction (which is based on a recently developed general theory of dynamical systems called coalgebra). Underlying the use of coinduction is the view of streams as dynamical entities, whose behaviour consists of the repeatedly offering of the next element of the stream. We can define streams by specifying their behaviour, and the equality of two streams can be established by proving that they have the same behaviour (in other words, that they are `behaviourally' equivalent). Although this may sound a bit mysterious at first, we hope that much of this will become clear already in the first chapter.