Category Theory for Computer Science

[ News | Lectures | Exercises | Material | Projects | People ]

News

• The course has terminated. Merry Christmas!

Lectures

December 9th

• A coalgebraic treatment of automata. Presented by Saurabh Agarwal.

December 2nd

• Infinite data structures, coalgebra, and coinduction. Presented by Michael Westergaard (slides).

November 25th

• Finite data structures, algebra, and induction. Presented by Henning Korsholm Rohde (slides).

November 18th

• Transition systems generalised into presheaves. Presented by Marco Carbone.

November 11th

• Exercises related to last week's lecture.
• Designing subtyping disciplines in programming languages. Presented by Branimir Lambov.

November 4th

• Exercise related to last week's lecture.
• Effects in functional programming handled by monads. Presented by Karl Kristian Krukow (slides).

October 28th

• Cartesian closed categories and the simply­typed lambda calculus. Presented by Jesper Torp Kristensen.
• Modelling recursive types. Presented by Mads Sig Ager (slides).

October 21st

October 14th

October 7th

September 30th

• summary of material so far (see the slides) by going through exercise sheet 4
• presentation of proposed projects by Mogens Nielsen, Bartek Klin, and Mikkel Nygaard
• matching people to projects

• Limit­preserving functor [Borceux, Def. 2.9.1]

• Equalisers are mono [Borceux, Prop. 2.4.3]
• Right adjoints preserve limits [Borceux, Prop. 3.2.2]

September 23rd

• limits and colimits
• adjoint functors

• equaliser, coequaliser [Borceux, Def. 2.4.1]
• pullback, pushout [Borceux, Def. 2.5.1]
• cone [Borceux, Def. 2.6.1]
• limit [Borceux, Def. 2.6.2]
• cocone [Borceux, Def. 2.6.5]
• colimit [Borceux, Def. 2.6.6]
• adjoint functor [Borceux, Def. 3.1.4, Thm. 3.1.5]

• equalisers in Set [Borceux, Ex. 2.4.6.a]
• pullbacks in Set [Borceux, Ex. 2.5.10.a]
• monos characterised by pullbacks [Borceux, Prop. 2.5.6]
• products as pullbacks from the terminal object
• initial objects, products, pullbacks, and equalisers as special kinds of limits [Borceux, Ex. 2.6.7a-c]
• the left adjoint of the forgetful functor from Mon to Set gives the free (list) monoid on a set
• the right adjoint of the inclusion functor from the category of (synchronisation) trees to the category of transition systems gives the unfolding of a transition system as a tree

September 16th

• hom functors [Borceux, Ex. 1.10.3.a]
• extended example (continued): ML type constructors as functors
• dogma 3: use natural transformations to understand how translations between different kinds of structure relate [Goguen, Sect. 3]
• Yoneda lemma
• exponentials and cartesian closed categories

• natural transformation [Borceux, Sect. 1.3]
• functor category
• exponential object
• cartesian closed category

• polymorphic functions seen as natural transformations
• the category of graphs seen as a functor category
• examples of cartesian closed categories: Set, Cat and many categories of domains used in semantics of programming languages
• applying proof technique from the Yoneda lemma to relate two definitions of cartesian closed categories

September 9th

• extended example: the category Aut of automata
• dogma 2: use functors to understand translations between different kinds of structure [Goguen, Sect. 2]
• functors [Borceux, Sect. 1.2,1.4,1.5,1.7-1.10]
• extended example: ML type constructors as functors (to be continued, see [Wadler] for more information)

• functor [Borceux, Def. 1.2.2]
• contravariant functor [Borceux, Def. 1.4.1]
• full functor, faithful functor [Borceux, Def. 1.5.1]
• subcategory [Borceux, Def. 1.5.3]
• full subcategory [Borceux, Def. 1.5.4]

• the category of automata (nondeterministic finite automata with one initial state and a set of accepting states) and automata morphisms (Aut)
• universal constructions in Aut (the one-state automaton accepting all strings is terminal, the one-state automaton accepting no strings is initial, the product is the usual product construction on automata accepting the intersection of languages, the coproduct is obtained by juxtaposing the automata and identifying the initial states - not the standard construction of automata theory because it possibly accepts more than the union of languages)
• the language functor L from Aut to the poset of languages ordered by inclusion; it preserves terminal and initial objects as well as products (intersection); coproduct is not preserved, this suggests changing the definition of automaton to have a set of initial states instead of just one
• the category of small categories and functors (Cat)
• monos, epis, isos in Cat are precisely the functors that are faithful+injective on objects, full+surjective on objects, full and faithful+bijective on objects
• universal constructions in Cat (the category 1 with one object and one arrow, the empty category 0, product category, sum of categories)
• type constructors in ML as functors on Set (list acts like map on arrows, * is a bifunctor, -> is a bifunctor which is contravariant in its first argument)

• full and faithful functors reflect isos

September 2nd

• motivation for studying category theory as computer scientists [Goguen, Sect. 0]
• dogma 1: use categories to understand structure [Goguen, Sect. 1]
• basic language of category theory [Borceux, Sects. 1.2,1.7-1.9]
• duality [Borceux, Sect. 1.10]
• universal constructions [Borceux, Sects. 2.1-2.3]

• category [Borceux, Def. 1.2.1]
• mono [Borceux, Def. 1.7.1]
• epi [Borceux, Def. 1.8.1]
• iso [Borceux, Def. 1.9.1]
• opposite (or dual) category [Borceux, Def. 1.10.1]
• product [Borceux, Def. 2.1.1]
• coproduct [Borceux, Def. 2.2.1]
• terminal and initial objects [Borceux, Def. 2.3.1]

• category of sets and functions (Set)
• category of posets and monotone functions (Pos)
• categories of monoids (Mon), groups (Grp), and rings (Rng) and homomorphisms
• category of graphs and graph morphisms (Gph)
• individual poset viewed as a category
• in Set, monos, epis, isos are precisely the injective, surjective, bijective functions
• universal constructions in Set (cartesian product, disjoint sum, singletons and the empty set)
• universal constructions in a poset viewed as a category (meet, join, top, bottom)

• identities are unique
• the composition of two monos (epis) is a mono (epi)
• the universal constructions are unique up to isomorphism

Exercises

• [ ps ] Exercise sheet 6 by Karl Kristian Krukow. We'll go through them on November 13th.
• [ ps ] Exercise sheet 5 by Mads Sig Ager. We'll go through them on November 4th.
• [ ps ] Exercise sheet 4. We'll go through them on September 30th.
• [ ps ] Exercise sheet 3. We'll go through them on September 23rd.
• [ ps ] Exercise sheet 2. We'll go through them on September 16th.
• [ ps ] Exercise sheet 1. We'll go through them on September 9th.

Material

1. [ ps ] Nick Benton, John Hughes, and Eugenio Moggi. Monads and Effects. In APPSEM'00 Summer School, LNCS 2395, 2002
2. Francis Borceux. Handbook of Categorical Algebra 1: Basic Category Theory. Number 50 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994.
3. Andrzej Filinski. Semantics of Functional Programming. Lecture notes (preliminary version), December 1998.
4. [ ps ] Joseph A. Goguen. A Categorical Manifesto. Mathematical Structures in Computer Science 1(1). 1991.
5. [ ps ] Bart Jacobs and Jan Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin 62, 1997.
6. André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from Open Maps. Information and Computation 127(2). 1996.
7. John C. Mitchell. Foundations for Programming Languages. Foundations of Computing Series. The MIT Press, 1996.
8. [ ps ] Mikkel Nygaard. Presheaf models and process calculi. Lecture notes, June 2002.
9. [ pdf ] John C. Reynolds. Using Category Theory to Design Implicit Conversions and Generic Operators. In Semantics­Directed Compiler Generation. LNCS 94, 1980.
10. [ ps ] John C. Reynolds. The Coherence of Languages with Intersection Types. In Proceedings of TACS'91. LNCS 526, 1991.
11. [ ps ] J.J.M.M. Rutten. Automata and Coinduction (An Exercise in Coalgebra). In Proceedings of CONCUR'98. LNCS 1466, 1998.
12. [ ps ] Philip Wadler. Theorems for free!. In Proceedings of ICFP'89.
13. [ ps ] Philip Wadler. Comprehending Monads. Mathematical Structures in Computer Science 2. 1992.
14. Glynn Winskel and Mogens Nielsen. Models for Concurrency. In Handbook of Logic in Computer Science. Volume 4: Semantics Modelling. Oxford University Press, 1995.
15. Glynn Winskel and Mogens Nielsen. Presheaves as Transition Systems. In DIMACS Series in Discrete Mathematics and Theoretical Computer Science. Volume 29, 1997.

Projects

Category theory in programming language semantics and design

• Cartesian closed categories and the lambda calculus [7]
• A model for the untyped lambda calculus (or: recursive types) [7]
• Designing subtyping disciplines in programming languages [9,10]
• Effects in functional programming handled by monads [1,3,13]

Category theory and models for concurrency

• Relating models for concurrency using adjunctions and/or giving semantics to process calculi using universal constructions and fibrations [14]
• A categorical definition of bisimulation [6]
• Processes seen as presheaves (setvalued functors) [6,8,15]

Category theory and data structures

• Finite data structures (lists, trees, ...) handled using algebras and induction [5]
• Infinite data structures (streams, infinite trees, ...) handled using coalgebra and coinduction [5]
• Automata theory in coalgebraic form [11]

People

• [ email | www ] Saurabh Agarwal
  
• [ email | www ] Mads Sig Ager
  
• [ email | www ] Marco Carbone
  
• [ email | www ] Jørgen Iversen
  
• [ email | www ] Bartek Klin
  
• [ email | www ] Sunil Kothari
  
• [ email | www ] Jesper Torp Kristensen
  
• [ email | www ] Karl Kristian Krukow
  
• [ email | www ] Branimir Lambov
  
• [ email | www ] Thomas Mailund
  
• [ email | www ] Mogens Nielsen
  
• [ email | www ] Mikkel Nygaard
  
• [ email | www ] Henning Korsholm Rohde
  
• [ email | www ] Pawel Sobocinski
  
• [ email | www ] Michael Westergaard
  

[ Top | News | Lectures | Exercises | Material | People ]