![[BRICS logo]](http://www.brics.dk//GIF/BRICSlogoM.GIF)
![[DAIMI logo]](http://www.brics.dk//GIF/DAIMI/logo10mm.GIF)
SET THEORY FOR COMPUTER SCIENCE (August-September 2010)
Times and place: Tue 11-13, Wed 14-16, starting Aug 24 2010, Lecture Room 129 Incuba Science Park, 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. A brief discussion of the axiomatisation of set theory.
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. Coinduction.
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.
Inductively defined properties and classes: Extending inductive definitions to properties and classes. An inductive definition of the Ordinals. The Burali-Forti paradox. Transfinite induction and recursion. The Axiom of Choice and the Well-Ordering Principle. The cumulative (von Neumann) hierarchy of sets.
Fraenkel-Mostowski set theory and nominal sets: Their role in the syntax and semantics of name-generation and freshness assumptions in Computer Science and Logic. (Not yet written, and possibly only very briefly)
Set Theory for Computer Science
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.