![[BRICS logo]](http://www.brics.dk//GIF/BRICSlogoM.GIF)
![[DAIMI logo]](http://www.brics.dk//GIF/DAIMI/logo10mm.GIF)
CATEGORY THEORY FOR COMPUTER SCIENCE (August-September 2009)
Times and places: Tue 11-13 in Lecture Room 129 IT-Huset, Thu 14-16 in ***Shannon-157***, starting Aug 25 2009.
Prerequisites:
The main is an interest in mathematics underlying Computer Science. Specific courses which would be helpful are those on or including parts of Discrete Mathematics, Semantics or Concurrency.
Contents: Category theory with examples from Computer Science
Why Category Theory? A first encounter, giving a broad motivational sweep over examples of why Category Theory is important in Computer Science and Logic.
Categories, Functors and Natural Transformations. Examples, the Category of Sets, Category of Complete Partial Orders CPO, Category Transition Systems TS, Petri Nets PN.
Constructions in Categories: products, coproducts, equalizers, coequalizers motivated through the example categories above.
Constructions on Categories. Product and functor categories.
Yoneda Lemma and Universal Properties. Limits and Colimits in general. Examples in the categories above.
Adjunctions. Examples from models used in Computer Science.
Monads and Algebras. Monads as type constructors.
Cartesian and Monoidal-Closed Categories. Intuitionistic and Linear Logic, very briefly, and their roles in Computer Science.
The tempo and topics of the course will be to some extent determined by the knowledge and interest of the participants. The examples are drawn from Types, Logic, Domain Theory and Denotational Semantics, and Concurrency. Additional motivational background will be provided where needed. I will try each week to devote the first 2 hrs to fundamental concepts in Category Theory and the second 2 hrs to Computer-Science examples and applications.
Lecture materials:
The main course notes are Jaap van Oosten's lecture notes Basic Category Theory.
Supplementary material: Jaap van Oosten's notes also contain useful book references, including to the classic text by MacLane. Benjamin Pierce's book `Basic Category Theory for Computer Scientists' is probably the most elementary. Steve Awodey's book `Category Theory' looks good, but is very expensive. Online, you should find Daniele Turi's Edinburgh Category Theory Lecture Notes helpful. A more advanced and rapid approach based on `representability' is followed in Lecture Notes in Category Theory, notes with Mario Caccamo, based on Martin Hyland's lectures at Cambridge followed by my lectures in Aarhus. Wikipedia although unbalanced can also be helpful. For charming live presentations on various topics in category theory see TheCatsters on YouTube. You might find the following Danish notes helpful in providing supplementary motivation: Kategorier for den stakkels studerende. It may however sometimes be difficult to match the Danish and English terms.
Chapter 1: 2, 3[for Algebraists], 4[for the keen], 6, 8[for Topologists], 9, 10, 12, 13, 14, 15. I recommend that you do all the uncommented exercises in the list above and the commented ones if you have an interest. Additional exercise: show that in the category of sets a function is mono iff it is injective, and epi iff it is surjective.
Chapter 2, selected exercises: 16, 17,18, 20, 24. Additional exercises: (1) Fill in the details in JvO's proof of the Yoneda lemma P.11: show `conversely any element of F(C) determines a natural transformation' 2nd paragraph of the proof. (2) Fill in the details of proof of Corollary 2.3.
Chapter 3 has lots of good exercises. Here's a slight cut-down: 29,30,31,32,33,34,40,41(a),42,43,44,46,48,49,50,51,52.
Chapter 5, selected exercises: 74,75,76,77[a revision of my lecture],81,82,83,84,85.
SET THEORY FOR COMPUTER SCIENCE(August-September 2008)
Times and place: Tue 14-16, Thu 14-16, starting Aug 26 2008, IT Huset Lokale 112, Abaagade 15
This course, a book in the making, introduces the set theory every computer scientist should know. The material, here presented in a unified way, often lies scattered across many different courses and books. Comprehensive notes, examples of applications in computer science, some history, and exercises will be provided. The tempo and to some extent the coverage of the course can be adjusted according to the experience and wishes of the class. The topics of the course notes:
A quick resume of Mathematical argument: Basic mathematical notation and argument, including proof by contradiction, mathematical induction and its variants.
Sets and logic: Subsets of a fixed set as a Boolean algebra. Venn diagrams. Propositional logic and its models. Validity, entailment, and equivalence of boolean propositions. Truth tables. Structural induction. Simplification of boolean propositions and set expressions.
Relations and functions: Product of sets. Relations, functions and partial functions. Composition and identity relations. Injective, surjective and bijective functions. Direct and inverse image of a set under a relation. Equivalence relations and partitions. Directed graphs and partial orders. Size of sets, especially countability. Cantor's diagonal argument to show the reals are uncountable.
Sets and constructions on sets: Russell's paradox. Basic sets, comprehension, indexed sets, unions, intersections, products, disjoint unions, powersets. Characteristic functions. Sets of functions. Lambda notation for functions. Cantor's diagonal argument to show powerset strictly increases size.
Introduction to inductive definitions: Using rules to define sets. Reasoning principles: rule induction and its instances; induction on derivations. Applications, including transitive closure of a relation. Inductive definitions as least fixed points. Tarski's fixed point theorem for monotonic functions on a powerset.
Well-founded induction: Well-founded relations and well-founded induction. Examples. Constructing well-founded relations, including product and lexicographic product of well-founded relations. Applications, including to Euclid's algorithm for hcf (gcd). Well-founded recursion.
(Not yet written and only if there is time and demand) Inductively defined properties and classes: Ordinals and transfinite induction. Fraenkel-Mostowski set theory and nominal sets --- their role in the syntax and semantics of name generation.
Set Theory for Computer Science
Week one: 1.3, 1.5, 1.13, 1.16, 1.17, 2.4, 2.10, 2.17, 2.18, 2.24.
Week two: 3.11, 3.12, 3.16, 3.18, 3.21, 3.22, 3.33, 3.35, 3.41 [For Exercise 3.35 you may assume that the rationals are dense in the reals in the sense that there is a rational between any two distinct reals. For the Exercise 3.41 you may use the result of Exercise 3.40.]
First Graded Hand-in: 1.15, 2.9, 2.19, 2.20, 2.25, 3.6, 3.20, 3.34, 3.36, 3.42, 4.2, 4.6, 4.7, 4.9, 5.6, 5.7, 5.9, 5.20, 5.23, 5.24, 5.25, 6.7, 6.14. Please attempt all the exercises. No proofs are needed in exercises 4.6 and 4.7. Exercise 3.42 guides you through a proof of the Schroeder-Bernstein theorem. Exercise 4.2 illustrates a little Category Theory. Exercise 5.20 gives the rudiments of continuous functions and their least fixed points, used in Denotational Semantics to give meaning to recursive definitions. Exercises 3.20 and 5.24 introduce the important equivalence relation of bisimulation, its properties and its understanding as a maximum fixed point.
Second Graded Hand-in (!!!DEADLINE 20 OCT 2008!!!): This second and last hand-in has a more open-ended character. You are asked to go through each chapters Ch.2 to Ch.6 of the lecture notes and find applications for the material in that chapter. Each application should be accompanied by a brief explanation for that application (enough that I can see you understand at least in broad terms what that application is). For example, in Ch.2 one application (which you may include) is to automatic theorem proving, where the normal forms for boolean propositions (conjunctive and disjunctive) can be used to establish the equivalence for propositions. In discovering the applications you can use any resources, books, the internet (including Wikipedia), that you like. Ideally your hand-in will resemble a dictionary or encyclopedia-like list of entries, one for each application. When to stop? I suggest you try to find: 3 applications for Ch.2; 3 applications for Ch.3; 4 applications for Ch.4; 5 applications for Ch.5; and 3 applications for Ch.6.