2D5377 Algebras + Coalgebras = Data Types + Systems

Graduate Course

Dates: To start week 38.

Classes: 14 tutorials over 14 weeks, Once weekly, 2 * 45 minutes, each Friday 10.15-12.00 during weeks 38 (Friday 18th September) until 51 (Friday 18th December).

Location: School of Computer Science and Communications (CSC) KTH,

KTH Main Campus, Stockholm.

Room 1625 Lindstedtsvägen 3.

Lecturer: Karl Meinke <e-mail me>

Course Weighting: 6 points

Course Assessment: by individual project

Prerequisites: Either:

1. introductory mathematical logic and discrete mathematics. Abstract algebra and/or category theory are helpful but not necessary, or
2. a strong practical background in object-orientation or programming language/compiler design.

Suitable for:

• students pursuing semantics and logics of programs needing access to mathematical tools,
• students in algorithms and complexity who wish to broaden their understanding of theoretical computer science,
• students in practical software engineering who wish to develop their understanding of its mathematical foundations,
• students in mathematical logic who wish to understand computer science applications.

Course Summary.

This course will repeat the popular course given in 2004 and 2007, with only minor changes. Algebra and category theory have played a central role in the development of programming languages since the 1970s. From among the many contributions to these fields, we can discern two important lines of development:

1. algebraic systems and the explication of the concept of abstract data type, data encapsulation and parameterisation leading to the modern subject of object-orientation,
2. algebraic automata theory leading to such areas as operational semantics and concurrency theory.

Underlying these two broad lines of development are two closely related, and often dual theories, universal algebra and universal coalgebra. We take as our course theme the view that algebras and coalgebras model static and dynamic aspects of systems. (Hence the title of our course, though this view is not entirely accurate.) We shall discuss the main features of these theories with reference to some of their computing applications such as initial algebra semantics, term rewriting and Knuth Bendix completion, final coalgebra semantics, bisimulation and coinduction.

The course will focus on two main texts that we will attempt to cover:

1. K. Meinke and J.V. Tucker, Universal Algebra, pp 189-411 in: S. Abramsky, D. Gabbay and T.S.E. Maibaum (eds), Handbook of Logic in Computer Science, Volume 1, Oxford University Press, 1993.

2. J.J.M.M. Rutten, Universal Coalgebra: a Theory of Systems, CWI Report CS-R9652, CWI Amsterdam, 1996.

Course Content (Provisional).

Part I: Algebras

1. Background and Motivation

2. Fundamentals, sets, categories and functors, duality

3. Signatures, and algebras

4. Isomorphisms, homomorphisms, initial, free and final objects

5. Subalgebras, direct products

6. Equations, initial models, equational logic, term rewriting, completion, varieties, Horn clauses, quasivarieties

Part II: Coalgebras

7. Coalgebras and models of systems

8. Limits and colimits

9. Bisimulation

10. Subsystems

11. Coinductive definition and proof

Page last modified: 2009-09-07