Coalgebra for Computer Scientists, Summer semester 2011/2012

E184 Institute of Information Systems, Faculty of Informatics, Vienna University of Technology, Official reference 184.731

Lecturer:      Dr. Ana Sokolova, anas"at"cs.uni-salzburg.at

Schedule:      Thursdays 2:00pm-4:00pm (then 2:30-4:00 pm, with slight adjustments when needed) Seminarraum Goedel. Check the detailed schedule below.

First meeting:    Thursday, 8.3.2011, 2:00pm, Seminarraum Goedel

Language:      English

Course aim and description: The goal is to get acquainted with the theory of coalgebra and its use in computer science. Also, along the way, the students will get to know some category theory notions that are needed for basic constructions and results in coalgebra. The course is meant for computer science students (possibly also some mathematics students) interested in computer science theory. If you are a student interested in formal methods, concurrency theory, and/or automata, and/or you always wondered what is category theory good for, then this may be the right course for you. The teaching consists of lectures interspersed with exercises.

The theory of coalgebra is a relatively recent (20 years old) unifying theory at the abstract end of formal methods. It is a (one could say "the") theory of dynamic systems, of states and observations. Coalgebras allow for a uniform treatment of many different types of automata (e.g. deterministic, nondeterministic, probabilistic, and weighted), their behavior, and their corresponding modal logics. These topics will be covered within the course.

Prerequisites: Basics of theoretical computer science like logic, sets, and automata theory are needed to follow this course. For the rest, the course will be self-contained.

Exam: This is a VU course. There will be an exam at the very end of the semester. The exam is written and it consists of several questions/excersises from the material covered during the course. Additionally, the homework and paper presentation will also contribute to the final grade.
Exam dates: Paper presentations, Monday, July 16, 2012, starting at 2pm, room Manger (see schedule below).
Written exam, Thursday, July 19, 2012, starting at 2pm, Seminarraum Goedel.
Extra meeting for questions and answers before the exam, Tuesday, July 17, 2012, starting at 2pm, Seminarraum Goedel.

Literature:

Draft book: Introduction to Coalgebra. Towards Mathematics of States and observations by Bart Jacobs. Two-thirds of a book in preparation.
Other lecture notes that we may sometimes use (in alphabetical order of author names):
Papers to start with:
- Jan Rutten, Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1), 2000, pp. 3-80 (an extended version of the original report from 1995).
- Bart Jacobs and Jan Rutten, An introduction to (co)algebra and (co)induction. Advanced topics in bisimulation and coinduction. Cambridge Tracts in Theoretical Computer Science Volume 52, Cambridge University Press, 2011, book chapter, p.38-99 (an extended version of the 1997 tutorial in Bulletin of EATCS Vol. 62, 1997, pp. 222--259)
Filippo Bonchi, Marcello Bonsangue, Jan Rutten, Alexandra Silva, Brzozowski's minimization algorithm (co)algebraically. Essays dedicated to Dexter Kozen on the occasion of his 60th Birthday. LNCS 7230, pp. 12-23, 2012.
Additional literature links will be assembled here as needed, during the semester.

Announcements and important news:

8.3.2012: Due to overlap with another course and the possibility that some students take both, we will shift the starting time of the lectures to 2:30pm for 22.3.2012 and 19.4.2012. Please check the schedule below. After these dates, we will always start at 2:30pm, but room availability must be confirmed, therefore "exact time t.b.a.".

Homework and paper assignements: HW week 1: task 1.1.1 from the book; HW week 2: task 1.2.8 from the book; no HW week 3 (more things to read); no HW week 4; HW week 5: task 2.2.5 from the book (and a more involved finality task as a preparation for what comes next); Instead of a HW week 6, please read the paper(s) by Barr ref.[31] in the book. If you have a problem with accessing the paper, send me an email. HW week 7: fill in the missing details of the coalgebraic proof of correctness of Brzozowski's minimization algorithm (Lemma 1 - Lemma 5, formulated in class). HW week 8: prove that for LTS a relation is a coalgebraic bisimulation (Aczel and Mendler) if and only if it is a (concrete) bisimulation (Park). HW week 9: (1) Is bisimilarity an equivalence for the Sets functor that does not preserve weak pullbacks? The functor can be found in the paper by Aczel and Mendler from 1989 or in Example 4.3.7 in my PhD thesis --- download pdf from my webpage, link "papers" scroll down to 2005. (2) Prove that behavioral equivalence on a single coalgebra is indeed an equivalence (without any additional assumptions). HW week 10: Prove that the construction of a coequilizer in Sets provides a coequilizer in CoAlg(F). HW week 11: Prove (directly, without using behavioral equivalence, or find an existing proof) that in the presence of a final coalgebra for a weak pullback preserving functor, bisimilarity and final coalgebra semantics coincide.

Schedule: More detailed information will appear here after each meeting.

Week 1, Thursday 8.3.12, 2pm-4pm, Seminarraum Goedel. This was an introductory lecture with informal discussion of coalgebras, their appearance in computer science, and their connection to algebras. Then we made a sneak-preview into coalgebra theory by showing finality of finite and infinite sequences (streams) and discussing coinduction on this concrete example. We will continue with this next time. Reading material: the introduction/preface of the draft book and all of the literature links above--do not worry if you do not understand all. In addition you may want to read Section 1.1. and (part of) 1.2. of the draft book (containing the streams result).

It is still not late to join the course next week! If you plan to do so, it is particularly good if you read the suggested reading material.
Week 2, Thursday 15.3.12, 2pm-4pm, Seminarraum Goedel. We briefly repeated some introduction and what we did last time, using these slides. Then we finished the proof of finality of sequences and proceeded with examples of coinduction (definitions and proofs). Reading material: Section 1.2. of the book.
Week 3, Thursday 22.3.12, 2:30pm-5pm, Seminarraum Goedel. Basics of category theory, abstract coalgebras. Coalgebra homomorphisms for sequences in concrete terms. Examples of functors and their coalgebras. Reading material: Section 1.4. of the book. Until next time, please read yourself Section 2.1. (as a preparation for the next class). It would be good if you take the time yourself to get acquainted with it. As a test, you may wish to try out the excercises to Section 2.1. (also those to Section 1.4.). It is also good to read Section 3 of the paper Universal Coalgebra: a theory of systems, by Jan Rutten (see link above) introducing many examples of coalgebras.
Week 4, Thursday 19.4.12, 2:30pm-4pm, Seminarraum Goedel. Functorial constructions in Sets, limits and colimits categorically. Classes of polynomial functors, examples of coalgebras. Reading material: Section 2.1 and Section 2.2. of the book, Section 3 of the paper Universal Coalgebra: a theory of systems by Jan Rutten.
Week 5, Thursday 26.4.12, 2:30pm-4pm, Seminarraum Goedel. Examples of coalgebras of polynomial functors, in particular (deterministic and Moore) automata as coalgebras and their homomorphisms. Reading material: All of Section 2.2.
Week 6, Thursday 3.5.12, 2:30pm-4pm, Seminarraum Goedel. Final coalgebras. Basic results and some constructions. Section 2.3 (read in particular the interesting example beyond Sets in 2.3.1) from the book, and instead of a HW (see also above) read the paper(s) by Barr, ref.[31] from the book. If you have a problem accessing the papers, send me an email.
Week 7, Thursday 10.5.12, 2:30pm-4pm, Seminarraum Goedel. Brzozowski's minimization algorithm (co)algebraically, a nice recent result employing elementary (co)algebra theory. Read the corresponding paper by Bonchi, Bonsangue, Rutten, and Silva (see link above). Check also the suggested papers for reading/presenting and make decisions soon.
Week 8, Thursday 24.5.12, 2:30pm-4pm, Seminarraum Goedel. Bisimulations and their properties. We are diverging from the book. Read Section 2 (in particular page 10-13), and parts of Section 5 (as long as no weak pullbacks appear) of the paper Universal Coalgebra: a theory of systems by Jan Rutten.
Week 9, Thursday 31.5.12, 2:30pm-4pm, Seminarraum Goedel. Weak pullbacks and their preservation, further properties of bisimilarity. Read Section 4 and the rest of Section 5 from the paper Universal Coalgebra: a theory of systems by Jan Rutten. We also started a bit on the topic of behavioral equivalence (via cospans).
Week 10, Thursday 14.6.12, 2:30pm-4pm, Seminarraum Goedel. Since there were very few students we used quite some time to discusss questions and anything that was not clear so far. We then proceeded with properties of behavioral equivalence. Lecture notes will be sent to you by email soon. Reading material: Section 4 of the paper Universal Coalgebra: a theory of systems by Jan Rutten.
Week 11, Thursday 21.6.12, 12:00noon-1:30pm, Besprechungsraum 101, 3. floor, Freihaus (green area) --- change of schedule because of an overlap with a guest lecture.
Relating final coalgebra semantics, behavioral equivalence, and bisimilarity. Lecture notes of last week and this week have been sent to you by email. Reading material: what we covered in class is scattered through literature. Some of the results can be found in my PhD thesis (Chapter 4). Additionally, please read Chapter 3 of the book (bisimilarity of polynomial functors via relation liftings) and browse through Chapter 4 of the book. This is certainly a lot to read, you may want to skip the details of the proofs and/or read a condensed version on relation liftings in Section 3.6 of my PhD thesis and additionally Theorem 4.2.1 that illustrates a modular way of deriving trasfer conditions for bisimilarity (using the relation lifting approach).
Week 12, Thursday 28.6.12, 2:30pm-4pm, Seminarraum Goedel. The very basics of coalgebraic modal logics (examples of modal logics, predicate liftings, modal logics coalgebraically, the Hennessy-Milner property). Lecture notes of this week have been sent to you by email. Reading material: the first two chapters of the lecture notes "COALA: Coalgebraic logics and applications" by Dirk Pattinson (see link above). We did not manage to prove the Hennessy-Milner property in class, you could read/browse through the proof yourself. (Watch out for typos! Some typos in the basic definitions are corrected in the class lecture notes.)
Additional meeting, Monday 16.7.12, 2pm-5pm, Room Menger, 3rd Floor, "Stiege 3". Paper presentations.
Additional meeting, Tuesday 17.7.12, 2pm-4pm, Seminarraum Goedel. Questions and answers, anything that you may still want to ask before the exam.
Additional meeting, Thursday 19.7.12, 2pm-5pm, Seminarraum Goedel. Written exam.