Algebraïsche Specificaties 2004

Hoorcollege op woensdag 12.45 - 14.30, zaal M129, docent prof.dr. J. Rutten.
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.

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.